Skip to content

Commit

Permalink
Extend ghost operation encoding for multiset and seq
Browse files Browse the repository at this point in the history
  • Loading branch information
@aakp10
aakp10 committed Dec 21, 2020
1 parent d82354c commit 3895c62
Show file tree
Hide file tree
Showing 6 changed files with 192 additions and 57 deletions.
108 changes: 80 additions & 28 deletions prusti-common/src/vir/ast/expr.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,7 @@ pub enum Expr {
FieldAccessPredicate(Box<Expr>, PermAmount, Position),
UnaryOp(UnaryOpKind, Box<Expr>, Position),
BinOp(BinOpKind, Box<Expr>, Box<Expr>, Position),
SetOp(SetOpKind, Box<Expr>, Box<Expr>, Position),
ContainerOp(ContainerOpKind, Box<Expr>, Box<Expr>, Position),
/// Unfolding: predicate name, predicate_args, in_expr, permission amount, enum variant
Unfolding(String, Vec<Expr>, Box<Expr>, PermAmount, MaybeEnumVariantIndex, Position),
/// Cond: guard, then_expr, else_expr
Expand Down Expand Up @@ -82,12 +82,20 @@ pub enum BinOpKind {
}

#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Serialize, Deserialize)]
pub enum SetOpKind {
Contains,
Push,
Union,
Intersection,
Remove,
pub enum ContainerOpKind {
SetContains,
SetPush,
SetUnion,
SetIntersection,
SetRemove,
MultiSetContains,
MultiSetPush,
MultiSetUnion,
MultiSetIntersection,
MultiSetRemove,
SeqAppend,
SeqChain,
SeqDrop,
}

#[derive(Debug, Clone, PartialEq, Eq, Hash, Serialize, Deserialize)]
Expand All @@ -110,7 +118,7 @@ impl fmt::Display for Expr {
Expr::BinOp(op, ref left, ref right, ref _pos) => {
write!(f, "({}) {} ({})", left, op, right)
}
Expr::SetOp(op, ref left, ref right, ref _pos) => {
Expr::ContainerOp(op, ref left, ref right, ref _pos) => {
write!(f, "({}) {} ({})", left, op, right)
}
Expr::UnaryOp(op, ref expr, ref _pos) => write!(f, "{}({})", op, expr),
Expand Down Expand Up @@ -243,14 +251,22 @@ impl fmt::Display for BinOpKind {
}
}

impl fmt::Display for SetOpKind {
impl fmt::Display for ContainerOpKind {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
match self {
&SetOpKind::Contains => write!(f, "contains"),
&SetOpKind::Push => write!(f, "push"),
&SetOpKind::Union => write!(f, "union"),
&SetOpKind::Intersection => write!(f, "intersection"),
&SetOpKind::Remove => write!(f, "remove"),
&ContainerOpKind::SetContains => write!(f, "set contains"),
&ContainerOpKind::SetPush => write!(f, "set push"),
&ContainerOpKind::SetUnion => write!(f, "set union"),
&ContainerOpKind::SetIntersection => write!(f, "set intersection"),
&ContainerOpKind::SetRemove => write!(f, "set remove"),
&ContainerOpKind::MultiSetContains => write!(f, "multiset contains"),
&ContainerOpKind::MultiSetPush => write!(f, "multiset push"),
&ContainerOpKind::MultiSetUnion => write!(f, "multiset union"),
&ContainerOpKind::MultiSetIntersection => write!(f, "multiset intersection"),
&ContainerOpKind::MultiSetRemove => write!(f, "multiset remove"),
&ContainerOpKind::SeqAppend => write!(f, "sequence append"),
&ContainerOpKind::SeqDrop => write!(f, "sequence drop"),
&ContainerOpKind::SeqChain => write!(f, "sequence chain"),
}
}
}
Expand Down Expand Up @@ -279,7 +295,7 @@ impl Expr {
Expr::FieldAccessPredicate(_, _, p) => p,
Expr::UnaryOp(_, _, p) => p,
Expr::BinOp(_, _, _, p) => p,
Expr::SetOp(_, _, _, p) => p,
Expr::ContainerOp(_, _, _, p) => p,
Expr::Unfolding(_, _, _, _, _, p) => p,
Expr::Cond(_, _, _, p) => p,
Expr::ForAll(_, _, _, p) => p,
Expand All @@ -306,7 +322,7 @@ impl Expr {
Expr::FieldAccessPredicate(x, y, _) => Expr::FieldAccessPredicate(x, y, pos),
Expr::UnaryOp(x, y, _) => Expr::UnaryOp(x, y, pos),
Expr::BinOp(x, y, z, _) => Expr::BinOp(x, y, z, pos),
Expr::SetOp(x, y, z, _) => Expr::SetOp(x, y, z, pos),
Expr::ContainerOp(x, y, z, _) => Expr::ContainerOp(x, y, z, pos),
Expr::Unfolding(x, y, z, perm, variant, _) => {
Expr::Unfolding(x, y, z, perm, variant, pos)
},
Expand Down Expand Up @@ -445,19 +461,47 @@ impl Expr {
}

pub fn set_contains(left: Expr, right: Expr) -> Self {
Expr::SetOp(SetOpKind::Contains, box left, box right, Position::default())
Expr::ContainerOp(ContainerOpKind::SetContains, box left, box right, Position::default())
}

pub fn set_union(left: Expr, right: Expr) -> Self {
Expr::SetOp(SetOpKind::Union, box left, box right, Position::default())
Expr::ContainerOp(ContainerOpKind::SetUnion, box left, box right, Position::default())
}

pub fn set_intersection(left: Expr, right: Expr) -> Self {
Expr::SetOp(SetOpKind::Intersection, box left, box right, Position::default())
Expr::ContainerOp(ContainerOpKind::SetIntersection, box left, box right, Position::default())
}

pub fn set_remove(left: Expr, right: Expr) -> Self {
Expr::SetOp(SetOpKind::Remove, box left, box right, Position::default())
Expr::ContainerOp(ContainerOpKind::SetRemove, box left, box right, Position::default())
}

pub fn multiset_contains(left: Expr, right: Expr) -> Self {
Expr::ContainerOp(ContainerOpKind::MultiSetContains, box left, box right, Position::default())
}

pub fn multiset_union(left: Expr, right: Expr) -> Self {
Expr::ContainerOp(ContainerOpKind::MultiSetUnion, box left, box right, Position::default())
}

pub fn multiset_intersection(left: Expr, right: Expr) -> Self {
Expr::ContainerOp(ContainerOpKind::MultiSetIntersection, box left, box right, Position::default())
}

pub fn multiset_remove(left: Expr, right: Expr) -> Self {
Expr::ContainerOp(ContainerOpKind::MultiSetRemove, box left, box right, Position::default())
}

pub fn seq_append(left: Expr, right: Expr) -> Self {
Expr::ContainerOp(ContainerOpKind::SeqAppend, box left, box right, Position::default())
}

pub fn seq_drop(left: Expr, right: Expr) -> Self {
Expr::ContainerOp(ContainerOpKind::SeqDrop, box left, box right, Position::default())
}

pub fn seq_chain(left: Expr, right: Expr) -> Self {
Expr::ContainerOp(ContainerOpKind::SeqChain, box left, box right, Position::default())
}

pub fn forall(vars: Vec<LocalVar>, triggers: Vec<Trigger>, body: Expr) -> Self {
Expand Down Expand Up @@ -935,13 +979,21 @@ impl Expr {
}
}
}
Expr::SetOp(ref kind, box ref base1, box ref base2, _pos) => {
Expr::ContainerOp(ref kind, box ref base1, box ref base2, _pos) => {
match kind {
SetOpKind::Contains|
SetOpKind::Push|
SetOpKind::Union|
SetOpKind::Intersection|
SetOpKind::Remove => {
ContainerOpKind::SetContains|
ContainerOpKind::SetPush|
ContainerOpKind::SetUnion|
ContainerOpKind::SetIntersection|
ContainerOpKind::SetRemove|
ContainerOpKind::MultiSetContains|
ContainerOpKind::MultiSetPush|
ContainerOpKind::MultiSetUnion|
ContainerOpKind::MultiSetIntersection|
ContainerOpKind::MultiSetRemove|
ContainerOpKind::SeqAppend|
ContainerOpKind::SeqChain|
ContainerOpKind::SeqDrop => {
let typ1 = base1.get_type();
typ1
}
Expand Down Expand Up @@ -1293,7 +1345,7 @@ impl Expr {
}

Expr::BinOp(..)
| Expr::SetOp(..)
| Expr::ContainerOp(..)
| Expr::MagicWand(..)
| Expr::Unfolding(..)
| Expr::Cond(..)
Expand Down Expand Up @@ -1514,7 +1566,7 @@ impl Hash for Expr {
Expr::FieldAccessPredicate(box ref base, perm, _) => (base, perm).hash(state),
Expr::UnaryOp(op, box ref arg, _) => (op, arg).hash(state),
Expr::BinOp(op, box ref left, box ref right, _) => (op, left, right).hash(state),
Expr::SetOp(op, box ref left, box ref right, _) => (op, left, right).hash(state),
Expr::ContainerOp(op, box ref left, box ref right, _) => (op, left, right).hash(state),
Expr::Cond(box ref cond, box ref then_expr, box ref else_expr, _) => {
(cond, then_expr, else_expr).hash(state)
}
Expand Down
16 changes: 8 additions & 8 deletions prusti-common/src/vir/ast/expr_transformers.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -132,12 +132,12 @@ pub trait ExprFolder: Sized {

fn fold_set_op(
&mut self,
kind: SetOpKind,
kind: ContainerOpKind,
first: Box<Expr>,
second: Box<Expr>,
pos: Position
) -> Expr {
Expr::SetOp(kind, self.fold_boxed(first), self.fold_boxed(second), pos)
Expr::ContainerOp(kind, self.fold_boxed(first), self.fold_boxed(second), pos)
}

fn fold_unfolding(
Expand Down Expand Up @@ -263,7 +263,7 @@ pub fn default_fold_expr<T: ExprFolder>(this: &mut T, e: Expr) -> Expr {
Expr::FieldAccessPredicate(x, y, p) => this.fold_field_access_predicate(x, y, p),
Expr::UnaryOp(x, y, p) => this.fold_unary_op(x, y, p),
Expr::BinOp(x, y, z, p) => this.fold_bin_op(x, y, z, p),
Expr::SetOp(x, y, z, p) => this.fold_set_op(x, y, z, p),
Expr::ContainerOp(x, y, z, p) => this.fold_set_op(x, y, z, p),
Expr::Unfolding(x, y, z, perm, variant, p) => {
this.fold_unfolding(x, y, z, perm, variant, p)
},
Expand Down Expand Up @@ -334,7 +334,7 @@ pub trait ExprWalker: Sized {
self.walk(arg1);
self.walk(arg2);
}
fn walk_set_op(&mut self, _op: SetOpKind, arg1: &Expr, arg2: &Expr, _pos: &Position) {
fn walk_set_op(&mut self, _op: ContainerOpKind, arg1: &Expr, arg2: &Expr, _pos: &Position) {
self.walk(arg1);
self.walk(arg2);
}
Expand Down Expand Up @@ -435,7 +435,7 @@ pub fn default_walk_expr<T: ExprWalker>(this: &mut T, e: &Expr) {
Expr::FieldAccessPredicate(ref x, y, ref p) => this.walk_field_access_predicate(x, y, p),
Expr::UnaryOp(x, ref y, ref p) => this.walk_unary_op(x, y, p),
Expr::BinOp(x, ref y, ref z, ref p) => this.walk_bin_op(x, y, z, p),
Expr::SetOp(x, ref y, ref z, ref p) => this.walk_set_op(x, y, z, p),
Expr::ContainerOp(x, ref y, ref z, ref p) => this.walk_set_op(x, y, z, p),
Expr::Unfolding(ref x, ref y, ref z, perm, ref variant, ref p) => {
this.walk_unfolding(x, y, z, perm, variant, p)
},
Expand Down Expand Up @@ -539,12 +539,12 @@ pub trait FallibleExprFolder: Sized {

fn fallible_fold_set_op(
&mut self,
kind: SetOpKind,
kind: ContainerOpKind,
first: Box<Expr>,
second: Box<Expr>,
pos: Position
) -> Result<Expr, Self::Error> {
Ok(Expr::SetOp(
Ok(Expr::ContainerOp(
kind,
self.fallible_fold_boxed(first)?,
self.fallible_fold_boxed(second)?,
Expand Down Expand Up @@ -696,7 +696,7 @@ pub fn default_fallible_fold_expr<U, T: FallibleExprFolder<Error=U>>(
Expr::FieldAccessPredicate(x, y, p) => this.fallible_fold_field_access_predicate(x, y, p),
Expr::UnaryOp(x, y, p) => this.fallible_fold_unary_op(x, y, p),
Expr::BinOp(x, y, z, p) => this.fallible_fold_bin_op(x, y, z, p),
Expr::SetOp(x, y, z, p) => this.fallible_fold_set_op(x, y, z, p),
Expr::ContainerOp(x, y, z, p) => this.fallible_fold_set_op(x, y, z, p),
Expr::Unfolding(x, y, z, perm, variant, p) => {
this.fallible_fold_unfolding(x, y, z, perm, variant, p)
},
Expand Down
27 changes: 21 additions & 6 deletions prusti-common/src/vir/to_viper.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -388,20 +388,35 @@ impl<'v> ToViper<'v, viper::Expr<'v>> for Expr {
ast.implies_with_pos(left.to_viper(ast), right.to_viper(ast), pos.to_viper(ast))
}
},
&Expr::SetOp(op, ref left, ref right, ref pos) => match op {
SetOpKind::Contains => {
&Expr::ContainerOp(op, ref left, ref right, ref pos) => match op {
ContainerOpKind::SetContains|
ContainerOpKind::MultiSetContains => {
ast.any_set_contains(right.to_viper(ast), left.to_viper(ast))
}
SetOpKind::Push|
SetOpKind::Union => {
ContainerOpKind::SetPush|
ContainerOpKind::SetUnion|
ContainerOpKind::MultiSetPush|
ContainerOpKind::MultiSetUnion => {
ast.any_set_union(left.to_viper(ast), right.to_viper(ast))
}
SetOpKind::Intersection => {
ContainerOpKind::SetIntersection|
ContainerOpKind::MultiSetIntersection => {
ast.any_set_intersection(left.to_viper(ast), right.to_viper(ast))
}
SetOpKind::Remove => {
ContainerOpKind::SetRemove|
ContainerOpKind::MultiSetRemove=> {
ast.any_set_minus(left.to_viper(ast), right.to_viper(ast))
}
ContainerOpKind::SeqAppend => {
ast.seq_append(left.to_viper(ast), right.to_viper(ast))
}
ContainerOpKind::SeqChain => {
// closure?
ast.seq_append(left.to_viper(ast), right.to_viper(ast))
}
ContainerOpKind::SeqDrop => {
ast.seq_drop(left.to_viper(ast), right.to_viper(ast))
}
},
&Expr::Unfolding(
ref predicate_name,
Expand Down
4 changes: 2 additions & 2 deletions prusti-viper/src/encoder/foldunfold/permissions.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -246,7 +246,7 @@ impl RequiredPermissionsGetter for vir::Expr {
vec![left, right].get_required_permissions(predicates)
}

vir::Expr::SetOp(_, box left, box right, _) => {
vir::Expr::ContainerOp(_, box left, box right, _) => {
vec![left, right].get_required_permissions(predicates)
}

Expand Down Expand Up @@ -384,7 +384,7 @@ impl ExprPermissionsGetter for vir::Expr {
&right.get_permissions(predicates),
),

vir::Expr::SetOp(_, box left, box right, _) => union(
vir::Expr::ContainerOp(_, box left, box right, _) => union(
&left.get_permissions(predicates),
&right.get_permissions(predicates),
),
Expand Down
20 changes: 14 additions & 6 deletions prusti-viper/src/encoder/mir_encoder.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -485,16 +485,24 @@ impl<'p, 'v: 'p, 'tcx: 'v> MirEncoder<'p, 'v, 'tcx> {

pub fn encode_set_op_expr(
&self,
op: vir::SetOpKind,
op: vir::ContainerOpKind,
left: vir::Expr,
right: vir::Expr
) -> EncodingResult<vir::Expr> {
Ok(match op {
vir::SetOpKind::Contains => vir::Expr::set_contains(left, right),
vir::SetOpKind::Push|
vir::SetOpKind::Union => vir::Expr::set_union(left, right),
vir::SetOpKind::Intersection => vir::Expr::set_intersection(left, right),
vir::SetOpKind::Remove => vir::Expr::set_remove(left, right),
vir::ContainerOpKind::SetContains => vir::Expr::set_contains(left, right),
vir::ContainerOpKind::SetPush|
vir::ContainerOpKind::SetUnion => vir::Expr::set_union(left, right),
vir::ContainerOpKind::SetIntersection => vir::Expr::set_intersection(left, right),
vir::ContainerOpKind::SetRemove => vir::Expr::set_remove(left, right),
vir::ContainerOpKind::MultiSetContains => vir::Expr::multiset_contains(left, right),
vir::ContainerOpKind::MultiSetPush|
vir::ContainerOpKind::MultiSetUnion => vir::Expr::multiset_union(left, right),
vir::ContainerOpKind::MultiSetIntersection => vir::Expr::multiset_intersection(left, right),
vir::ContainerOpKind::MultiSetRemove => vir::Expr::multiset_remove(left, right),
vir::ContainerOpKind::SeqAppend => vir::Expr::seq_append(left, right),
vir::ContainerOpKind::SeqDrop => vir::Expr::seq_drop(left, right),
vir::ContainerOpKind::SeqChain => vir::Expr::seq_chain(left, right),
})
}

Expand Down
Loading

0 comments on commit 3895c62

Please sign in to comment.