Encode set operations

prusti-common/src/vir/ast/expr.rs

@@ -31,6 +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),
     /// 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
@@ -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<LocalVar>, triggers: Vec<Trigger>, 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)
             }

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<Expr>,
+        second: Box<Expr>,
+        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<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::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<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::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<Expr>,
+        second: Box<Expr>,
+        pos: Position
+    ) -> Result<Expr, Self::Error> {
+        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<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::Unfolding(x, y, z, perm, variant, p) => {
             this.fallible_fold_unfolding(x, y, z, perm, variant, p)
         },

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,

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),

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<vir::Stmt> {
+        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,