diff --git a/prusti-common/src/vir/ast/expr.rs b/prusti-common/src/vir/ast/expr.rs index bb3c5fad883..deed4a108b9 100644 --- a/prusti-common/src/vir/ast/expr.rs +++ b/prusti-common/src/vir/ast/expr.rs @@ -31,6 +31,7 @@ pub enum Expr { FieldAccessPredicate(Box, PermAmount, Position), UnaryOp(UnaryOpKind, Box, Position), BinOp(BinOpKind, Box, Box, Position), + SetOp(SetOpKind, Box, Box, Position), /// Unfolding: predicate name, predicate_args, in_expr, permission amount, enum variant Unfolding(String, Vec, Box, PermAmount, MaybeEnumVariantIndex, Position), /// Cond: guard, then_expr, else_expr @@ -80,6 +81,11 @@ pub enum BinOpKind { Implies, } +#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Serialize, Deserialize)] +pub enum SetOpKind { + Contains, +} + #[derive(Debug, Clone, PartialEq, Eq, Hash, Serialize, Deserialize)] pub enum Const { Bool(bool), @@ -100,6 +106,9 @@ 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) => { + write!(f, "({}) {} ({})", left, op, right) + } Expr::UnaryOp(op, ref expr, ref _pos) => write!(f, "{}({})", op, expr), Expr::PredicateAccessPredicate(ref pred_name, ref arg, perm, ref _pos) => { write!(f, "acc({}({}), {})", pred_name, arg, perm) @@ -230,6 +239,14 @@ impl fmt::Display for BinOpKind { } } +impl fmt::Display for SetOpKind { + fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { + match self { + &SetOpKind::Contains => write!(f, "contains"), + } + } +} + impl fmt::Display for Const { fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { match self { @@ -254,6 +271,7 @@ impl Expr { Expr::FieldAccessPredicate(_, _, p) => p, Expr::UnaryOp(_, _, p) => p, Expr::BinOp(_, _, _, p) => p, + Expr::SetOp(_, _, _, p) => p, Expr::Unfolding(_, _, _, _, _, p) => p, Expr::Cond(_, _, _, p) => p, Expr::ForAll(_, _, _, p) => p, @@ -280,6 +298,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::Unfolding(x, y, z, perm, variant, _) => { Expr::Unfolding(x, y, z, perm, variant, pos) }, @@ -417,6 +436,10 @@ impl Expr { Expr::BinOp(BinOpKind::Implies, box left, box right, Position::default()) } + pub fn contains(left: Expr, right: Expr) -> Self { + Expr::SetOp(SetOpKind::Contains, box left, box right, Position::default()) + } + pub fn forall(vars: Vec, triggers: Vec, body: Expr) -> Self { Expr::ForAll(vars, triggers, box body, Position::default()) } @@ -1193,6 +1216,7 @@ impl Expr { } Expr::BinOp(..) + | Expr::SetOp(..) | Expr::MagicWand(..) | Expr::Unfolding(..) | Expr::Cond(..) @@ -1413,6 +1437,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::Cond(box ref cond, box ref then_expr, box ref else_expr, _) => { (cond, then_expr, else_expr).hash(state) } diff --git a/prusti-common/src/vir/ast/expr_transformers.rs b/prusti-common/src/vir/ast/expr_transformers.rs index 5f5f29e611f..9d211ec0a37 100644 --- a/prusti-common/src/vir/ast/expr_transformers.rs +++ b/prusti-common/src/vir/ast/expr_transformers.rs @@ -129,6 +129,17 @@ pub trait ExprFolder: Sized { ) -> Expr { Expr::BinOp(kind, self.fold_boxed(first), self.fold_boxed(second), pos) } + + fn fold_set_op( + &mut self, + kind: SetOpKind, + first: Box, + second: Box, + pos: Position + ) -> Expr { + Expr::SetOp(kind, self.fold_boxed(first), self.fold_boxed(second), pos) + } + fn fold_unfolding( &mut self, name: String, @@ -252,6 +263,7 @@ pub fn default_fold_expr(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::Unfolding(x, y, z, perm, variant, p) => { this.fold_unfolding(x, y, z, perm, variant, p) }, @@ -322,6 +334,10 @@ pub trait ExprWalker: Sized { self.walk(arg1); self.walk(arg2); } + fn walk_set_op(&mut self, _op: SetOpKind, arg1: &Expr, arg2: &Expr, _pos: &Position) { + self.walk(arg1); + self.walk(arg2); + } fn walk_unfolding( &mut self, _name: &str, @@ -419,6 +435,7 @@ pub fn default_walk_expr(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::Unfolding(ref x, ref y, ref z, perm, ref variant, ref p) => { this.walk_unfolding(x, y, z, perm, variant, p) }, @@ -519,6 +536,22 @@ pub trait FallibleExprFolder: Sized { pos )) } + + fn fallible_fold_set_op( + &mut self, + kind: SetOpKind, + first: Box, + second: Box, + pos: Position + ) -> Result { + Ok(Expr::SetOp( + kind, + self.fallible_fold_boxed(first)?, + self.fallible_fold_boxed(second)?, + pos + )) + } + fn fallible_fold_unfolding( &mut self, name: String, @@ -663,6 +696,7 @@ pub fn default_fallible_fold_expr>( 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::Unfolding(x, y, z, perm, variant, p) => { this.fallible_fold_unfolding(x, y, z, perm, variant, p) }, diff --git a/prusti-common/src/vir/to_viper.rs b/prusti-common/src/vir/to_viper.rs index e36ec93c76c..5e739a898ca 100644 --- a/prusti-common/src/vir/to_viper.rs +++ b/prusti-common/src/vir/to_viper.rs @@ -388,6 +388,11 @@ 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 => { + ast.any_set_contains(right.to_viper(ast), left.to_viper(ast)) + } + }, &Expr::Unfolding( ref predicate_name, ref args, diff --git a/prusti-viper/src/encoder/mir_encoder.rs b/prusti-viper/src/encoder/mir_encoder.rs index 3c63be2c8eb..a7106b6a57f 100644 --- a/prusti-viper/src/encoder/mir_encoder.rs +++ b/prusti-viper/src/encoder/mir_encoder.rs @@ -481,6 +481,17 @@ impl<'p, 'v: 'p, 'tcx: 'v> MirEncoder<'p, 'v, 'tcx> { }) } + pub fn encode_set_op_expr( + &self, + op: vir::SetOpKind, + left: vir::Expr, + right: vir::Expr + ) -> vir::Expr { + match op { + vir::SetOpKind::Contains => vir::Expr::contains(left, right), + } + } + pub fn encode_unary_op_expr(&self, op: mir::UnOp, expr: vir::Expr) -> vir::Expr { match op { mir::UnOp::Not => vir::Expr::not(expr), diff --git a/prusti-viper/src/encoder/procedure_encoder.rs b/prusti-viper/src/encoder/procedure_encoder.rs index 0b549ba0fe7..ae83fbb9bd0 100644 --- a/prusti-viper/src/encoder/procedure_encoder.rs +++ b/prusti-viper/src/encoder/procedure_encoder.rs @@ -2046,6 +2046,26 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { stmts.extend(self.encode_assign_operand(&dst.clone().field(value_field), &args[0], location)); } + "prusti_contracts::ghost::GhostSet::push" => { + unimplemented!(); + } + + "prusti_contracts::ghost::GhostSet::remove" => { + unimplemented!(); + } + + "prusti_contracts::ghost::GhostSeq::union" => { + unimplemented!(); + } + + "prusti_contracts::ghost::GhostSeq::is_element" => { + let &(ref target_place, _) = destination.as_ref().unwrap(); + let (dst, dest_ty, _) = self.mir_encoder.encode_place(target_place).unwrap(); + let value_field = self.encoder.encode_value_field(dest_ty); + let arg_ty = self.mir_encoder.get_operand_ty(&args[0]); + //stmts.extend(self.encode_set_op(vir::SetOpKind::Contains)); + } + "std::cmp::PartialEq::eq" | "core::cmp::PartialEq::eq" if args.len() == 2 && @@ -2202,6 +2222,27 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { Ok(result) } + fn encode_set_operation( + &mut self, + lhs: &vir::Expr, + left: &mir::Operand<'tcx>, + right: &mir::Operand<'tcx>, + location: mir::Location, + set_op: vir::SetOpKind, + ty: ty::Ty<'tcx>, + ) -> Vec { + trace!( + "[enter] encode_set_operation(location={:?}, set_op={:?})", location, set_op); + let span = self.mir_encoder.get_span_of_location(location); + let encoded_left = self.mir_encoder.encode_operand_expr(left) + .with_span(span)?; + let encoded_right = self.mir_encoder.encode_operand_expr(right) + .with_span(span)?; + let encoded_value = self.mir_encoder.encode_set_op_expr(set_op, encoded_left, encoded_right) + .with_span(span)?; + self.encode_copy_value_assign(lhs, encoded_value, ty, location) + } + fn encode_cmp_function_call( &mut self, called_def_id: ProcedureDefId,