From 3895c624ac0c009904a068e63fb7e9d615159e01 Mon Sep 17 00:00:00 2001 From: Karuna Grewal Date: Mon, 21 Dec 2020 18:41:00 +0530 Subject: [PATCH] Extend ghost operation encoding for multiset and seq --- prusti-common/src/vir/ast/expr.rs | 108 +++++++++++++----- .../src/vir/ast/expr_transformers.rs | 16 +-- prusti-common/src/vir/to_viper.rs | 27 ++++- .../src/encoder/foldunfold/permissions.rs | 4 +- prusti-viper/src/encoder/mir_encoder.rs | 20 +++- prusti-viper/src/encoder/procedure_encoder.rs | 74 ++++++++++-- 6 files changed, 192 insertions(+), 57 deletions(-) diff --git a/prusti-common/src/vir/ast/expr.rs b/prusti-common/src/vir/ast/expr.rs index 158a8bb4952..5b93f6a5348 100644 --- a/prusti-common/src/vir/ast/expr.rs +++ b/prusti-common/src/vir/ast/expr.rs @@ -31,7 +31,7 @@ pub enum Expr { FieldAccessPredicate(Box, PermAmount, Position), UnaryOp(UnaryOpKind, Box, Position), BinOp(BinOpKind, Box, Box, Position), - SetOp(SetOpKind, Box, Box, Position), + ContainerOp(ContainerOpKind, 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 @@ -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)] @@ -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), @@ -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"), } } } @@ -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, @@ -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) }, @@ -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, triggers: Vec, body: Expr) -> Self { @@ -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 } @@ -1293,7 +1345,7 @@ impl Expr { } Expr::BinOp(..) - | Expr::SetOp(..) + | Expr::ContainerOp(..) | Expr::MagicWand(..) | Expr::Unfolding(..) | Expr::Cond(..) @@ -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) } diff --git a/prusti-common/src/vir/ast/expr_transformers.rs b/prusti-common/src/vir/ast/expr_transformers.rs index 9d211ec0a37..389d742c299 100644 --- a/prusti-common/src/vir/ast/expr_transformers.rs +++ b/prusti-common/src/vir/ast/expr_transformers.rs @@ -132,12 +132,12 @@ pub trait ExprFolder: Sized { fn fold_set_op( &mut self, - kind: SetOpKind, + kind: ContainerOpKind, first: Box, second: Box, 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( @@ -263,7 +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::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) }, @@ -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); } @@ -435,7 +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::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) }, @@ -539,12 +539,12 @@ pub trait FallibleExprFolder: Sized { fn fallible_fold_set_op( &mut self, - kind: SetOpKind, + kind: ContainerOpKind, first: Box, second: Box, pos: Position ) -> Result { - Ok(Expr::SetOp( + Ok(Expr::ContainerOp( kind, self.fallible_fold_boxed(first)?, self.fallible_fold_boxed(second)?, @@ -696,7 +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::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) }, diff --git a/prusti-common/src/vir/to_viper.rs b/prusti-common/src/vir/to_viper.rs index cb0271212b7..77b7195ada5 100644 --- a/prusti-common/src/vir/to_viper.rs +++ b/prusti-common/src/vir/to_viper.rs @@ -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, diff --git a/prusti-viper/src/encoder/foldunfold/permissions.rs b/prusti-viper/src/encoder/foldunfold/permissions.rs index 22cdf106054..ac153039c8a 100644 --- a/prusti-viper/src/encoder/foldunfold/permissions.rs +++ b/prusti-viper/src/encoder/foldunfold/permissions.rs @@ -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) } @@ -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), ), diff --git a/prusti-viper/src/encoder/mir_encoder.rs b/prusti-viper/src/encoder/mir_encoder.rs index 387703f1d46..b65df146edb 100644 --- a/prusti-viper/src/encoder/mir_encoder.rs +++ b/prusti-viper/src/encoder/mir_encoder.rs @@ -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 { 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), }) } diff --git a/prusti-viper/src/encoder/procedure_encoder.rs b/prusti-viper/src/encoder/procedure_encoder.rs index 35ae958838d..f67038ff535 100644 --- a/prusti-viper/src/encoder/procedure_encoder.rs +++ b/prusti-viper/src/encoder/procedure_encoder.rs @@ -2033,7 +2033,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { &args[0], // ghost instance &args[1], // argument to the ghost method location, - vir::SetOpKind::Union, + vir::ContainerOpKind::SetUnion, dest_ty) .run_if_err(|| cleanup(&self))?); } @@ -2048,12 +2048,12 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { &args[0], // ghost instance &args[1], // argument to the ghost method location, - vir::SetOpKind::Remove, + vir::ContainerOpKind::SetRemove, dest_ty) .run_if_err(|| cleanup(&self))?); } - "prusti_contracts::ghost::GhostSeq::union" => { + "prusti_contracts::ghost::GhostSet::union" => { 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); @@ -2063,12 +2063,12 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { &args[0], // ghost instance &args[1], // argument to the ghost method location, - vir::SetOpKind::Union, + vir::ContainerOpKind::SetUnion, dest_ty) .run_if_err(|| cleanup(&self))?); } - "prusti_contracts::ghost::GhostSeq::is_element" => { + "prusti_contracts::ghost::GhostSet::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); @@ -2078,7 +2078,67 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { &args[0], // ghost instance &args[1], // argument to the ghost method location, - vir::SetOpKind::Contains, + vir::ContainerOpKind::SetContains, + dest_ty) + .run_if_err(|| cleanup(&self))?); + } + + "prusti_contracts::ghost::GhostMultiSet::push" => { + 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_operation( + dst.clone().field(value_field), // lhs + &args[0], // ghost instance + &args[1], // argument to the ghost method + location, + vir::ContainerOpKind::MultiSetUnion, + dest_ty) + .run_if_err(|| cleanup(&self))?); + } + + "prusti_contracts::ghost::GhostMultiSet::remove" => { + 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_operation( + dst.clone().field(value_field), // lhs + &args[0], // ghost instance + &args[1], // argument to the ghost method + location, + vir::ContainerOpKind::MultiSetRemove, + dest_ty) + .run_if_err(|| cleanup(&self))?); + } + + "prusti_contracts::ghost::GhostMultiSet::union" => { + 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_operation( + dst.clone().field(value_field), // lhs + &args[0], // ghost instance + &args[1], // argument to the ghost method + location, + vir::ContainerOpKind::MultiSetUnion, + dest_ty) + .run_if_err(|| cleanup(&self))?); + } + + "prusti_contracts::ghost::GhostMultiSet::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_operation( + dst.clone().field(value_field), // lhs + &args[0], // ghost instance + &args[1], // argument to the ghost method + location, + vir::ContainerOpKind::MultiSetContains, dest_ty) .run_if_err(|| cleanup(&self))?); } @@ -2265,7 +2325,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { left: &mir::Operand<'tcx>, right: &mir::Operand<'tcx>, location: mir::Location, - set_op: vir::SetOpKind, + set_op: vir::ContainerOpKind, ty: ty::Ty<'tcx>, ) -> SpannedEncodingResult> { trace!(