From 4caee3a001712cd4e8b38da382f8fbdffd64a36a Mon Sep 17 00:00:00 2001 From: Jonas Hansen Date: Wed, 27 Apr 2022 00:39:52 +0200 Subject: [PATCH 01/38] Adjust copy check in environment to better handle regions --- .../environment/mir_dump/graphviz/to_text.rs | 4 ++-- prusti-interface/src/environment/mod.rs | 19 ++++++------------- .../tests/verify_overflow/pass/copy/refs.rs | 17 +++++++++++++++++ 3 files changed, 25 insertions(+), 15 deletions(-) create mode 100644 prusti-tests/tests/verify_overflow/pass/copy/refs.rs diff --git a/prusti-interface/src/environment/mir_dump/graphviz/to_text.rs b/prusti-interface/src/environment/mir_dump/graphviz/to_text.rs index 239f1a216a9..6fe004a64ac 100644 --- a/prusti-interface/src/environment/mir_dump/graphviz/to_text.rs +++ b/prusti-interface/src/environment/mir_dump/graphviz/to_text.rs @@ -149,8 +149,8 @@ impl<'tcx> ToText for rustc_middle::ty::Ty<'tcx> { impl<'tcx> ToText for rustc_middle::ty::Region<'tcx> { fn to_text(&self) -> String { match self.kind() { - rustc_middle::ty::ReEarlyBound(_) => { - unimplemented!("ReEarlyBound: {}", format!("{}", self)); + rustc_middle::ty::ReEarlyBound(reg) => { + format!("lft_early_bound_{}", reg.index) } rustc_middle::ty::ReLateBound(debruijn, bound_reg) => { format!("lft_late_{}_{}", debruijn.index(), bound_reg.var.index()) diff --git a/prusti-interface/src/environment/mod.rs b/prusti-interface/src/environment/mod.rs index c66a35ee65f..315aa160e65 100644 --- a/prusti-interface/src/environment/mod.rs +++ b/prusti-interface/src/environment/mod.rs @@ -504,19 +504,12 @@ impl<'tcx> Environment<'tcx> { } pub fn type_is_copy(&self, ty: ty::Ty<'tcx>, param_env: ty::ParamEnv<'tcx>) -> bool { - let copy_trait = self.tcx.lang_items().copy_trait(); - if let Some(copy_trait_def_id) = copy_trait { - // We need this check because `type_implements_trait` - // panics when called on reference types. - if let ty::TyKind::Ref(_, _, mutability) = ty.kind() { - // Shared references are copy, mutable references are not. - matches!(mutability, mir::Mutability::Not) - } else { - self.type_implements_trait(ty, copy_trait_def_id, param_env) - } - } else { - false - } + // Erase all free regions. + // Having weird regions in `ty` can cause ICEs in `type_is_copy_modulo_regions` + let ty = self.tcx.erase_regions(ty); + self.tcx.infer_ctxt().enter(|infcx| + infcx.type_is_copy_modulo_regions(param_env, ty, rustc_span::DUMMY_SP) + ) } /// Checks whether the given type implements the trait with the given DefId. diff --git a/prusti-tests/tests/verify_overflow/pass/copy/refs.rs b/prusti-tests/tests/verify_overflow/pass/copy/refs.rs new file mode 100644 index 00000000000..9f0be9a256c --- /dev/null +++ b/prusti-tests/tests/verify_overflow/pass/copy/refs.rs @@ -0,0 +1,17 @@ +// Checking whether the params of pure methods are copy or not +use prusti_contracts::*; + +#[pure] +#[trusted] +fn foo<'a, T: Copy>(val: T) -> Option<&'a T> { + unimplemented!() +} + +#[pure] +#[trusted] +fn bar<'a, T: Copy>(val: T) -> &'a Option<&'a T> { + unimplemented!() +} + +fn main() { +} \ No newline at end of file From ed7dffd577e27835ea765eb8b76d656639995e8d Mon Sep 17 00:00:00 2001 From: Jonas Hansen Date: Wed, 27 Apr 2022 01:01:43 +0200 Subject: [PATCH 02/38] Maybe we need to handle TyKind::Ref differently? --- prusti-interface/src/environment/mod.rs | 19 +++++++++++++------ 1 file changed, 13 insertions(+), 6 deletions(-) diff --git a/prusti-interface/src/environment/mod.rs b/prusti-interface/src/environment/mod.rs index 315aa160e65..80f0ea5a850 100644 --- a/prusti-interface/src/environment/mod.rs +++ b/prusti-interface/src/environment/mod.rs @@ -504,12 +504,19 @@ impl<'tcx> Environment<'tcx> { } pub fn type_is_copy(&self, ty: ty::Ty<'tcx>, param_env: ty::ParamEnv<'tcx>) -> bool { - // Erase all free regions. - // Having weird regions in `ty` can cause ICEs in `type_is_copy_modulo_regions` - let ty = self.tcx.erase_regions(ty); - self.tcx.infer_ctxt().enter(|infcx| - infcx.type_is_copy_modulo_regions(param_env, ty, rustc_span::DUMMY_SP) - ) + // We need this check because `type_is_copy_modulo_regions` + // panics when called on reference types. + if let ty::TyKind::Ref(_, _, mutability) = ty.kind() { + // Shared references are copy, mutable references are not. + matches!(mutability, mir::Mutability::Not) + } else { + // First erase all free regions. + // Having weird regions in `ty` can cause ICEs in `type_is_copy_modulo_regions` + let ty = self.tcx.erase_regions(ty); + self.tcx.infer_ctxt().enter(|infcx| + infcx.type_is_copy_modulo_regions(param_env, ty, rustc_span::DUMMY_SP) + ) + } } /// Checks whether the given type implements the trait with the given DefId. From 03b36403160a1f70f94d8e0608e1d677c2a93d35 Mon Sep 17 00:00:00 2001 From: Jonas Hansen Date: Wed, 27 Apr 2022 11:33:32 +0200 Subject: [PATCH 03/38] Support associated types in copy check --- prusti-interface/src/environment/mod.rs | 10 +++++- .../pass/copy/associated-types.rs | 33 +++++++++++++++++++ 2 files changed, 42 insertions(+), 1 deletion(-) create mode 100644 prusti-tests/tests/verify_overflow/pass/copy/associated-types.rs diff --git a/prusti-interface/src/environment/mod.rs b/prusti-interface/src/environment/mod.rs index 80f0ea5a850..eece76199c7 100644 --- a/prusti-interface/src/environment/mod.rs +++ b/prusti-interface/src/environment/mod.rs @@ -504,15 +504,23 @@ impl<'tcx> Environment<'tcx> { } pub fn type_is_copy(&self, ty: ty::Ty<'tcx>, param_env: ty::ParamEnv<'tcx>) -> bool { + if ty.is_trivially_pure_clone_copy() { + return true; + } + // We need this check because `type_is_copy_modulo_regions` // panics when called on reference types. if let ty::TyKind::Ref(_, _, mutability) = ty.kind() { // Shared references are copy, mutable references are not. matches!(mutability, mir::Mutability::Not) } else { - // First erase all free regions. + // Erase all free regions. // Having weird regions in `ty` can cause ICEs in `type_is_copy_modulo_regions` let ty = self.tcx.erase_regions(ty); + + // Normalize the type to account for associated types + let ty = self.normalize_to(ty); + self.tcx.infer_ctxt().enter(|infcx| infcx.type_is_copy_modulo_regions(param_env, ty, rustc_span::DUMMY_SP) ) diff --git a/prusti-tests/tests/verify_overflow/pass/copy/associated-types.rs b/prusti-tests/tests/verify_overflow/pass/copy/associated-types.rs new file mode 100644 index 00000000000..aa26a90a431 --- /dev/null +++ b/prusti-tests/tests/verify_overflow/pass/copy/associated-types.rs @@ -0,0 +1,33 @@ +use prusti_contracts::*; + +trait Foo { + type Type; + + #[pure] + fn foo(&self) -> Self::Type; +} + +struct Bar; +impl Foo for Bar { + type Type = i32; + + #[pure] + fn foo(&self) -> Self::Type { + 42 + } +} + +struct Baz(std::marker::PhantomData); +impl Foo for Baz { + type Type = T; + + #[pure] + #[trusted] + fn foo(&self) -> Self::Type { + unimplemented!() + } +} + +fn main() { + +} \ No newline at end of file From 138d98ede348587197215f14c8de814b6fa45d4f Mon Sep 17 00:00:00 2001 From: Jonas Hansen Date: Wed, 27 Apr 2022 15:08:10 +0200 Subject: [PATCH 04/38] Pass type with binder to type_is_copy to better account for regions --- prusti-interface/src/environment/mod.rs | 35 +++++---------- .../tests/verify_overflow/pass/copy/refs.rs | 12 ++--- .../src/encoder/mir/places/interface.rs | 17 ------- .../mir/pure/pure_functions/encoder.rs | 45 ++++++++++--------- .../mir/pure/pure_functions/new_encoder.rs | 15 +++---- 5 files changed, 49 insertions(+), 75 deletions(-) diff --git a/prusti-interface/src/environment/mod.rs b/prusti-interface/src/environment/mod.rs index eece76199c7..51f765eed68 100644 --- a/prusti-interface/src/environment/mod.rs +++ b/prusti-interface/src/environment/mod.rs @@ -492,8 +492,8 @@ impl<'tcx> Environment<'tcx> { .unwrap_or((called_def_id, call_substs)) } - pub fn type_is_allowed_in_pure_functions(&self, ty: ty::Ty<'tcx>, param_env: ty::ParamEnv<'tcx>) -> bool { - match ty.kind() { + pub fn type_is_allowed_in_pure_functions(&self, ty: ty::Binder<'tcx, ty::Ty<'tcx>>, param_env: ty::ParamEnv<'tcx>) -> bool { + match ty.skip_binder().kind() { ty::TyKind::Never => { true } @@ -503,28 +503,15 @@ impl<'tcx> Environment<'tcx> { } } - pub fn type_is_copy(&self, ty: ty::Ty<'tcx>, param_env: ty::ParamEnv<'tcx>) -> bool { - if ty.is_trivially_pure_clone_copy() { - return true; - } - - // We need this check because `type_is_copy_modulo_regions` - // panics when called on reference types. - if let ty::TyKind::Ref(_, _, mutability) = ty.kind() { - // Shared references are copy, mutable references are not. - matches!(mutability, mir::Mutability::Not) - } else { - // Erase all free regions. - // Having weird regions in `ty` can cause ICEs in `type_is_copy_modulo_regions` - let ty = self.tcx.erase_regions(ty); - - // Normalize the type to account for associated types - let ty = self.normalize_to(ty); - - self.tcx.infer_ctxt().enter(|infcx| - infcx.type_is_copy_modulo_regions(param_env, ty, rustc_span::DUMMY_SP) - ) - } + /// Checks whether `ty` is copy. + /// The type is wrapped into a `Binder` to handle regions correctly. + pub fn type_is_copy(&self, ty: ty::Binder<'tcx, ty::Ty<'tcx>>, param_env: ty::ParamEnv<'tcx>) -> bool { + // Normalize the type to account for associated types + let ty = self.normalize_to(ty); + let ty = self.tcx.erase_late_bound_regions(ty); + self.tcx.infer_ctxt().enter(|infcx| + infcx.type_is_copy_modulo_regions(param_env, ty, rustc_span::DUMMY_SP) + ) } /// Checks whether the given type implements the trait with the given DefId. diff --git a/prusti-tests/tests/verify_overflow/pass/copy/refs.rs b/prusti-tests/tests/verify_overflow/pass/copy/refs.rs index 9f0be9a256c..62869d9c675 100644 --- a/prusti-tests/tests/verify_overflow/pass/copy/refs.rs +++ b/prusti-tests/tests/verify_overflow/pass/copy/refs.rs @@ -3,15 +3,15 @@ use prusti_contracts::*; #[pure] #[trusted] -fn foo<'a, T: Copy>(val: T) -> Option<&'a T> { - unimplemented!() -} +fn foo<'a, T: Copy>(val: T) -> Option<&'a T> { unimplemented!() } #[pure] #[trusted] -fn bar<'a, T: Copy>(val: T) -> &'a Option<&'a T> { - unimplemented!() -} +fn bar<'a, T: Copy>(val: T) -> &'a Option<&'a T> { unimplemented!() } + +#[pure] +#[trusted] +fn baz<'a, T>(val: &'a T) -> Option<&'a T> { unimplemented!() } fn main() { } \ No newline at end of file diff --git a/prusti-viper/src/encoder/mir/places/interface.rs b/prusti-viper/src/encoder/mir/places/interface.rs index d14b66e2e08..d906388e176 100644 --- a/prusti-viper/src/encoder/mir/places/interface.rs +++ b/prusti-viper/src/encoder/mir/places/interface.rs @@ -21,13 +21,6 @@ trait PlacesEncoderInterfacePrivate<'tcx> {} impl<'v, 'tcx: 'v> PlacesEncoderInterfacePrivate<'tcx> for super::super::super::Encoder<'v, 'tcx> {} pub(crate) trait PlacesEncoderInterface<'tcx> { - fn is_local_copy( - &self, - mir: &mir::Body<'tcx>, - local: mir::Local, - param_env: ty::ParamEnv<'tcx>, - ) -> SpannedEncodingResult; - fn get_local_span( &self, mir: &mir::Body<'tcx>, @@ -116,16 +109,6 @@ pub(crate) trait PlacesEncoderInterface<'tcx> { } impl<'v, 'tcx: 'v> PlacesEncoderInterface<'tcx> for super::super::super::Encoder<'v, 'tcx> { - fn is_local_copy( - &self, - mir: &mir::Body<'tcx>, - local: mir::Local, - param_env: ty::ParamEnv<'tcx>, - ) -> SpannedEncodingResult { - let mir_type = self.get_local_type(mir, local)?; - Ok(self.env().type_is_copy(mir_type, param_env)) - } - fn get_local_span( &self, mir: &mir::Body<'tcx>, diff --git a/prusti-viper/src/encoder/mir/pure/pure_functions/encoder.rs b/prusti-viper/src/encoder/mir/pure/pure_functions/encoder.rs index eebc37067ef..8c38885d3cb 100644 --- a/prusti-viper/src/encoder/mir/pure/pure_functions/encoder.rs +++ b/prusti-viper/src/encoder/mir/pure/pure_functions/encoder.rs @@ -45,7 +45,7 @@ pub(super) struct PureFunctionEncoder<'p, 'v: 'p, 'tcx: 'v> { /// Span of the function declaration. span: Span, /// Signature of the function to be encoded. - sig: ty::FnSig<'tcx>, + sig: ty::PolyFnSig<'tcx>, /// Spans of MIR locals, when encoding a local pure function. local_spans: Option>, } @@ -106,8 +106,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> PureFunctionEncoder<'p, 'v, 'tcx> { .env() .tcx() .fn_sig(proc_def_id) - .subst(encoder.env().tcx(), substs) - .skip_binder(); + .subst(encoder.env().tcx(), substs); PureFunctionEncoder { encoder, @@ -135,7 +134,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> PureFunctionEncoder<'p, 'v, 'tcx> { ); self.local_spans = Some( - (0..=self.sig.inputs().len()) + (0..=self.sig.skip_binder().inputs().len()) .map(|idx| { interpreter .mir_encoder() @@ -268,7 +267,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> PureFunctionEncoder<'p, 'v, 'tcx> { .encoder .encode_type_bounds( &vir::Expr::local(pure_fn_return_variable), - self.sig.output(), + self.sig.skip_binder().output(), ) .into_iter() .map(|p| p.set_default_pos(res_value_range_pos)) @@ -284,18 +283,18 @@ impl<'p, 'v: 'p, 'tcx: 'v> PureFunctionEncoder<'p, 'v, 'tcx> { .type_is_copy(typ, self.encoder.env().tcx().param_env(self.proc_def_id))); let mut bounds = self .encoder - .encode_type_bounds(&vir::Expr::local(formal_arg.clone()), typ); + .encode_type_bounds(&vir::Expr::local(formal_arg.clone()), typ.skip_binder()); bounds.extend(precondition); precondition = bounds; } } else if config::encode_unsigned_num_constraint() { - if let ty::TyKind::Uint(_) = self.sig.output().kind() { + if let ty::TyKind::Uint(_) = self.sig.skip_binder().output().kind() { let expr = vir::Expr::le_cmp(0u32.into(), pure_fn_return_variable.into()); postcondition.push(expr.set_default_pos(res_value_range_pos)); } for (formal_arg, local) in formal_args.iter().zip(self.args_iter()) { let typ = self.get_local_ty(local); - if let ty::TyKind::Uint(_) = typ.kind() { + if let ty::TyKind::Uint(_) = typ.skip_binder().kind() { precondition.push(vir::Expr::le_cmp(0u32.into(), formal_arg.into())); } } @@ -347,10 +346,13 @@ impl<'p, 'v: 'p, 'tcx: 'v> PureFunctionEncoder<'p, 'v, 'tcx> { let span = self.get_local_span(arg); let target_place = self .encoder - .encode_value_expr(vir::Expr::local(self.encode_mir_local(arg)?), arg_ty) + .encode_value_expr( + vir::Expr::local(self.encode_mir_local(arg)?), + arg_ty.skip_binder(), + ) .with_span(span)?; let mut new_place: vir::Expr = self.encode_local(arg)?.into(); - if let ty::TyKind::Ref(_, _, _) = arg_ty.kind() { + if let ty::TyKind::Ref(_, _, _) = arg_ty.skip_binder().kind() { // patch references with an explicit snap app // TODO: this probably needs to be adjusted when snapshots of // references are implemented @@ -362,7 +364,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> PureFunctionEncoder<'p, 'v, 'tcx> { } fn args_iter(&self) -> impl Iterator { - (0..self.sig.inputs().len()).map(|idx| mir::Local::from_usize(1 + idx)) + (0..self.sig.skip_binder().inputs().len()).map(|idx| mir::Local::from_usize(1 + idx)) } /// Encode the precondition with two expressions: @@ -375,7 +377,9 @@ impl<'p, 'v: 'p, 'tcx: 'v> PureFunctionEncoder<'p, 'v, 'tcx> { let mut type_spec = vec![]; for &local in contract.args.iter() { let local_ty = self.get_local_ty(local.into()); - let fraction = if let ty::TyKind::Ref(_, _, hir::Mutability::Not) = local_ty.kind() { + let fraction = if let ty::TyKind::Ref(_, _, hir::Mutability::Not) = + local_ty.skip_binder().kind() + { vir::PermAmount::Read } else { vir::PermAmount::Write @@ -479,7 +483,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> PureFunctionEncoder<'p, 'v, 'tcx> { let var_span = self.get_local_span(local); let var_type = self .encoder - .encode_snapshot_type(self.get_local_ty(local)) + .encode_snapshot_type(self.get_local_ty(local).skip_binder()) .with_span(var_span)?; Ok(vir::LocalVar::new(var_name, var_type)) } @@ -490,16 +494,16 @@ impl<'p, 'v: 'p, 'tcx: 'v> PureFunctionEncoder<'p, 'v, 'tcx> { let var_span = self.get_local_span(local); let var_type = self .encoder - .encode_type(self.get_local_ty(local)) + .encode_type(self.get_local_ty(local).skip_binder()) .with_span(var_span)?; Ok(vir::LocalVar::new(var_name, var_type)) } - fn get_local_ty(&self, local: mir::Local) -> ty::Ty<'tcx> { + fn get_local_ty(&self, local: mir::Local) -> ty::Binder<'tcx, ty::Ty<'tcx>> { if local.as_usize() == 0 { self.sig.output() } else { - self.sig.inputs()[local.as_usize() - 1] + self.sig.input(local.as_usize() - 1) } } @@ -531,7 +535,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> PureFunctionEncoder<'p, 'v, 'tcx> { } self.encoder - .encode_snapshot_type(ty) + .encode_snapshot_type(ty.skip_binder()) .with_span(self.get_return_span()) } @@ -543,13 +547,14 @@ impl<'p, 'v: 'p, 'tcx: 'v> PureFunctionEncoder<'p, 'v, 'tcx> { fn encode_formal_args(&self) -> SpannedEncodingResult> { let mut formal_args = vec![]; - for (local_idx, local_ty) in self.sig.inputs().iter().enumerate() { + for local_idx in 0..self.sig.skip_binder().inputs().len() { + let local_ty = self.sig.input(local_idx); let local = rustc_middle::mir::Local::from_usize(local_idx + 1); let var_name = format!("{:?}", local); let var_span = self.get_local_span(local); let param_env = self.encoder.env().tcx().param_env(self.proc_def_id); - if !self.encoder.env().type_is_copy(*local_ty, param_env) { + if !self.encoder.env().type_is_copy(local_ty, param_env) { return Err(SpannedEncodingError::incorrect( "pure function parameters must be Copy", var_span, @@ -558,7 +563,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> PureFunctionEncoder<'p, 'v, 'tcx> { let var_type = self .encoder - .encode_snapshot_type(*local_ty) + .encode_snapshot_type(local_ty.skip_binder()) .with_span(var_span)?; formal_args.push(vir::LocalVar::new(var_name, var_type)) } diff --git a/prusti-viper/src/encoder/mir/pure/pure_functions/new_encoder.rs b/prusti-viper/src/encoder/mir/pure/pure_functions/new_encoder.rs index 046cfa32af0..a223139515d 100644 --- a/prusti-viper/src/encoder/mir/pure/pure_functions/new_encoder.rs +++ b/prusti-viper/src/encoder/mir/pure/pure_functions/new_encoder.rs @@ -147,7 +147,7 @@ pub(super) struct PureEncoder<'p, 'v: 'p, 'tcx: 'v> { /// Span of the function declaration. span: Span, /// Signature of the function to be encoded. - sig: ty::FnSig<'tcx>, + sig: ty::PolyFnSig<'tcx>, /// Spans of MIR locals, when encoding a local pure function. local_spans: Option>, } @@ -177,8 +177,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> PureEncoder<'p, 'v, 'tcx> { .env() .tcx() .fn_sig(proc_def_id) - .subst(encoder.env().tcx(), substs) - .skip_binder(); + .subst(encoder.env().tcx(), substs); Self { encoder, @@ -318,7 +317,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> PureEncoder<'p, 'v, 'tcx> { )); } - self.encoder.encode_type_high(ty) + self.encoder.encode_type_high(ty.skip_binder()) } fn encode_precondition_expr( @@ -393,7 +392,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> PureEncoder<'p, 'v, 'tcx> { } fn args_iter(&self) -> impl Iterator { - (0..self.sig.inputs().len()).map(|idx| mir::Local::from_usize(1 + idx)) + (0..self.sig.inputs().skip_binder().len()).map(|idx| mir::Local::from_usize(1 + idx)) } /// Encodes a VIR local with the original MIR type. @@ -411,18 +410,18 @@ impl<'p, 'v: 'p, 'tcx: 'v> PureEncoder<'p, 'v, 'tcx> { )); } let var_name = format!("{:?}", local); - let var_type = self.encoder.encode_type_high(ty)?; + let var_type = self.encoder.encode_type_high(ty.skip_binder())?; Ok(vir_high::VariableDecl { name: var_name, ty: var_type, }) } - fn get_local_ty(&self, local: mir::Local) -> ty::Ty<'tcx> { + fn get_local_ty(&self, local: mir::Local) -> ty::Binder<'tcx, ty::Ty<'tcx>> { if local.as_usize() == 0 { self.sig.output() } else { - self.sig.inputs()[local.as_usize() - 1] + self.sig.input(local.as_usize() - 1) } } From a408861269dc203742489b3fc8208ebc0cd1a7e9 Mon Sep 17 00:00:00 2001 From: Jonas Hansen Date: Thu, 28 Apr 2022 11:48:07 +0200 Subject: [PATCH 05/38] Normalize function signature in PureFunctionEncoder to account for associated types --- .../normalize-associated-types.rs | 44 +++++++++++++++++++ .../mir/pure/pure_functions/encoder.rs | 1 + .../mir/pure/pure_functions/new_encoder.rs | 1 + 3 files changed, 46 insertions(+) create mode 100644 prusti-tests/tests/verify_overflow/pass/ghost-constraints/normalize-associated-types.rs diff --git a/prusti-tests/tests/verify_overflow/pass/ghost-constraints/normalize-associated-types.rs b/prusti-tests/tests/verify_overflow/pass/ghost-constraints/normalize-associated-types.rs new file mode 100644 index 00000000000..090fdac046f --- /dev/null +++ b/prusti-tests/tests/verify_overflow/pass/ghost-constraints/normalize-associated-types.rs @@ -0,0 +1,44 @@ +// compile-flags: -Penable_ghost_constraints=true + +use prusti_contracts::*; + +trait A { + type AType; + + #[pure] + fn foo(&self, arg1: &Self::AType) -> bool; +} + +trait B { + type BType; + + #[ghost_constraint(Self: A::BType> , [ + requires(self.foo(&arg)), + ensures(self.foo(&arg)) + ])] + #[trusted] + fn bar(&self, arg: Self::BType); +} + +struct S; +impl A for S { + type AType = i32; + #[pure] + fn foo(&self, arg1: &Self::AType) -> bool { + *arg1 > 42 + } +} + +impl B for S { + type BType = i32; + + #[trusted] + fn bar(&self, arg: Self::BType) { + + } +} + +fn main() { + let s = S; + s.bar(43); +} \ No newline at end of file diff --git a/prusti-viper/src/encoder/mir/pure/pure_functions/encoder.rs b/prusti-viper/src/encoder/mir/pure/pure_functions/encoder.rs index 8c38885d3cb..93cdd9bfae0 100644 --- a/prusti-viper/src/encoder/mir/pure/pure_functions/encoder.rs +++ b/prusti-viper/src/encoder/mir/pure/pure_functions/encoder.rs @@ -107,6 +107,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> PureFunctionEncoder<'p, 'v, 'tcx> { .tcx() .fn_sig(proc_def_id) .subst(encoder.env().tcx(), substs); + let sig = encoder.env().normalize_to(sig); PureFunctionEncoder { encoder, diff --git a/prusti-viper/src/encoder/mir/pure/pure_functions/new_encoder.rs b/prusti-viper/src/encoder/mir/pure/pure_functions/new_encoder.rs index a223139515d..a83eb4c8651 100644 --- a/prusti-viper/src/encoder/mir/pure/pure_functions/new_encoder.rs +++ b/prusti-viper/src/encoder/mir/pure/pure_functions/new_encoder.rs @@ -178,6 +178,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> PureEncoder<'p, 'v, 'tcx> { .tcx() .fn_sig(proc_def_id) .subst(encoder.env().tcx(), substs); + let sig = encoder.env().normalize_to(sig); Self { encoder, From dbbed0dd532646687b583112fe48b7a9847f0068 Mon Sep 17 00:00:00 2001 From: Jonas Hansen Date: Thu, 28 Apr 2022 14:56:30 +0200 Subject: [PATCH 06/38] Remove check for validity of pure function in process_encoding_queue --- ...associated-types.rs => associated-types-1.rs} | 0 .../pass/copy/associated-types-2.rs | 15 +++++++++++++++ prusti-viper/src/encoder/encoder.rs | 16 ---------------- 3 files changed, 15 insertions(+), 16 deletions(-) rename prusti-tests/tests/verify_overflow/pass/copy/{associated-types.rs => associated-types-1.rs} (100%) create mode 100644 prusti-tests/tests/verify_overflow/pass/copy/associated-types-2.rs diff --git a/prusti-tests/tests/verify_overflow/pass/copy/associated-types.rs b/prusti-tests/tests/verify_overflow/pass/copy/associated-types-1.rs similarity index 100% rename from prusti-tests/tests/verify_overflow/pass/copy/associated-types.rs rename to prusti-tests/tests/verify_overflow/pass/copy/associated-types-1.rs diff --git a/prusti-tests/tests/verify_overflow/pass/copy/associated-types-2.rs b/prusti-tests/tests/verify_overflow/pass/copy/associated-types-2.rs new file mode 100644 index 00000000000..8f5e1b8a917 --- /dev/null +++ b/prusti-tests/tests/verify_overflow/pass/copy/associated-types-2.rs @@ -0,0 +1,15 @@ +use prusti_contracts::*; + +trait Foo { + type Type; + + #[trusted] + #[pure] + fn foo(&self) -> Self::Type { + unimplemented!() + } +} + +fn main() { + +} \ No newline at end of file diff --git a/prusti-viper/src/encoder/encoder.rs b/prusti-viper/src/encoder/encoder.rs index e7ba9217822..89baa4ce8ac 100644 --- a/prusti-viper/src/encoder/encoder.rs +++ b/prusti-viper/src/encoder/encoder.rs @@ -795,22 +795,6 @@ impl<'v, 'tcx> Encoder<'v, 'tcx> { let proc_kind = self.get_proc_kind(proc_def_id, None); - if matches!(proc_kind, ProcedureSpecificationKind::Pure) { - // Check that the pure Rust function satisfies the basic - // requirements by trying to encode it as a Viper function, - // which will automatically run the validity checks. - - // TODO: Make sure that this encoded function does not end up in - // the Viper file because that would be unsound. - let identity_substs = self.env().identity_substs(proc_def_id); - if let Err(error) = self.encode_pure_function_def(proc_def_id, identity_substs) { - self.register_encoding_error(error); - debug!("Error encoding function: {:?}", proc_def_id); - // Skip encoding the function as a method. - continue; - } - } - match proc_kind { _ if self.is_trusted(proc_def_id, None) => { debug!( From 161b9566c98af8ef5a0a3abbb8e447b7500a22f9 Mon Sep 17 00:00:00 2001 From: Jonas Hansen Date: Thu, 28 Apr 2022 16:27:23 +0200 Subject: [PATCH 07/38] Erase all regions in copy check --- prusti-interface/src/environment/mod.rs | 1 + .../pass/copy/erase-regions.rs | 25 +++++++++++++++++++ 2 files changed, 26 insertions(+) create mode 100644 prusti-tests/tests/verify_overflow/pass/copy/erase-regions.rs diff --git a/prusti-interface/src/environment/mod.rs b/prusti-interface/src/environment/mod.rs index 51f765eed68..5f93d55d44c 100644 --- a/prusti-interface/src/environment/mod.rs +++ b/prusti-interface/src/environment/mod.rs @@ -508,6 +508,7 @@ impl<'tcx> Environment<'tcx> { pub fn type_is_copy(&self, ty: ty::Binder<'tcx, ty::Ty<'tcx>>, param_env: ty::ParamEnv<'tcx>) -> bool { // Normalize the type to account for associated types let ty = self.normalize_to(ty); + let ty = self.tcx.erase_regions(ty); let ty = self.tcx.erase_late_bound_regions(ty); self.tcx.infer_ctxt().enter(|infcx| infcx.type_is_copy_modulo_regions(param_env, ty, rustc_span::DUMMY_SP) diff --git a/prusti-tests/tests/verify_overflow/pass/copy/erase-regions.rs b/prusti-tests/tests/verify_overflow/pass/copy/erase-regions.rs new file mode 100644 index 00000000000..3c5d4759246 --- /dev/null +++ b/prusti-tests/tests/verify_overflow/pass/copy/erase-regions.rs @@ -0,0 +1,25 @@ +use prusti_contracts::*; +use std::slice::Iter; + +#[model] +struct Iter<'a, #[generic] T: Copy> { + position: usize, +} + +type SliceTy = [T]; +#[extern_spec] +impl SliceTy { + #[pure] + fn len(&self) -> usize; + + #[ensures( result.model().position == 0 )] + fn iter(&self) -> std::slice::Iter<'_, T>; +} + +fn verify_slice_iter(slice: &[i32]) { + let iter = slice.iter(); +} + +fn main() { + +} \ No newline at end of file From eda14452ae5db939079e3fd2f55abc15e61e25dc Mon Sep 17 00:00:00 2001 From: Jonas Hansen Date: Thu, 28 Apr 2022 16:27:57 +0200 Subject: [PATCH 08/38] Do not perform normalization when there are no projections --- prusti-interface/src/environment/mod.rs | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/prusti-interface/src/environment/mod.rs b/prusti-interface/src/environment/mod.rs index 5f93d55d44c..8603e507217 100644 --- a/prusti-interface/src/environment/mod.rs +++ b/prusti-interface/src/environment/mod.rs @@ -561,6 +561,11 @@ impl<'tcx> Environment<'tcx> { /// i.e. this resolves projection types ([ty::TyKind::Projection]s) pub fn normalize_to>(&self, normalizable: T) -> T { use rustc_trait_selection::traits; + + if !normalizable.has_projections() { + return normalizable + } + self.tcx.infer_ctxt().enter(|infcx| { let mut selcx = traits::SelectionContext::new(&infcx); // We do not really care about obligations that are constructed From 41aad379cea34ab57eaa0fd25f92be12dcf7c6ba Mon Sep 17 00:00:00 2001 From: Jonas Hansen Date: Thu, 28 Apr 2022 17:16:54 +0200 Subject: [PATCH 09/38] Partially undo removal of code in process_encoding_queue. --- prusti-viper/src/encoder/encoder.rs | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/prusti-viper/src/encoder/encoder.rs b/prusti-viper/src/encoder/encoder.rs index 89baa4ce8ac..e7ba9217822 100644 --- a/prusti-viper/src/encoder/encoder.rs +++ b/prusti-viper/src/encoder/encoder.rs @@ -795,6 +795,22 @@ impl<'v, 'tcx> Encoder<'v, 'tcx> { let proc_kind = self.get_proc_kind(proc_def_id, None); + if matches!(proc_kind, ProcedureSpecificationKind::Pure) { + // Check that the pure Rust function satisfies the basic + // requirements by trying to encode it as a Viper function, + // which will automatically run the validity checks. + + // TODO: Make sure that this encoded function does not end up in + // the Viper file because that would be unsound. + let identity_substs = self.env().identity_substs(proc_def_id); + if let Err(error) = self.encode_pure_function_def(proc_def_id, identity_substs) { + self.register_encoding_error(error); + debug!("Error encoding function: {:?}", proc_def_id); + // Skip encoding the function as a method. + continue; + } + } + match proc_kind { _ if self.is_trusted(proc_def_id, None) => { debug!( From e2a54676865e827be31f7c6d07bb35b07a0f492c Mon Sep 17 00:00:00 2001 From: Jonas Hansen Date: Thu, 28 Apr 2022 19:25:41 +0200 Subject: [PATCH 10/38] Rename normalize_to, return original value if normalized value contains infer types --- prusti-interface/src/environment/mod.rs | 20 +++++++++++++++---- .../pass/copy/associated-types-2.rs | 2 +- .../mir/pure/pure_functions/encoder.rs | 2 +- .../mir/pure/pure_functions/new_encoder.rs | 2 +- .../encoder/mir/specifications/constraints.rs | 2 +- 5 files changed, 20 insertions(+), 8 deletions(-) diff --git a/prusti-interface/src/environment/mod.rs b/prusti-interface/src/environment/mod.rs index 8603e507217..2bac2a735be 100644 --- a/prusti-interface/src/environment/mod.rs +++ b/prusti-interface/src/environment/mod.rs @@ -507,7 +507,7 @@ impl<'tcx> Environment<'tcx> { /// The type is wrapped into a `Binder` to handle regions correctly. pub fn type_is_copy(&self, ty: ty::Binder<'tcx, ty::Ty<'tcx>>, param_env: ty::ParamEnv<'tcx>) -> bool { // Normalize the type to account for associated types - let ty = self.normalize_to(ty); + let ty = self.resolve_assoc_types(ty); let ty = self.tcx.erase_regions(ty); let ty = self.tcx.erase_late_bound_regions(ty); self.tcx.infer_ctxt().enter(|infcx| @@ -559,7 +559,7 @@ impl<'tcx> Environment<'tcx> { /// A facade for [rustc_trait_selection::traits::normalize_to] /// Normalizes associated types in foldable types, /// i.e. this resolves projection types ([ty::TyKind::Projection]s) - pub fn normalize_to>(&self, normalizable: T) -> T { + pub fn resolve_assoc_types + Copy>(&self, normalizable: T) -> T { use rustc_trait_selection::traits; if !normalizable.has_projections() { @@ -572,13 +572,25 @@ impl<'tcx> Environment<'tcx> { // in the normalization process let mut obligations = vec![]; - traits::normalize_to( + let normalized = traits::normalize_to( &mut selcx, ty::ParamEnv::reveal_all(), traits::ObligationCause::dummy(), normalizable, &mut obligations, - ) + ); + + // We probably normalized a bit too much. + // When we normalize an "unnormalizable" associated type + // (e.g. an associated type on a trait whose projection can not be resolved), + // "normalize_to" returns a type which needs to be infered. + // This is not what we want for e.g. a check whether a type is `Copy` or not. + // We thus return the original type in this case. + if normalized.needs_infer() { + return normalizable + } + + normalized }) } } diff --git a/prusti-tests/tests/verify_overflow/pass/copy/associated-types-2.rs b/prusti-tests/tests/verify_overflow/pass/copy/associated-types-2.rs index 8f5e1b8a917..21d4f187d3e 100644 --- a/prusti-tests/tests/verify_overflow/pass/copy/associated-types-2.rs +++ b/prusti-tests/tests/verify_overflow/pass/copy/associated-types-2.rs @@ -1,7 +1,7 @@ use prusti_contracts::*; trait Foo { - type Type; + type Type: Copy; #[trusted] #[pure] diff --git a/prusti-viper/src/encoder/mir/pure/pure_functions/encoder.rs b/prusti-viper/src/encoder/mir/pure/pure_functions/encoder.rs index 93cdd9bfae0..4245f7b8dad 100644 --- a/prusti-viper/src/encoder/mir/pure/pure_functions/encoder.rs +++ b/prusti-viper/src/encoder/mir/pure/pure_functions/encoder.rs @@ -107,7 +107,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> PureFunctionEncoder<'p, 'v, 'tcx> { .tcx() .fn_sig(proc_def_id) .subst(encoder.env().tcx(), substs); - let sig = encoder.env().normalize_to(sig); + let sig = encoder.env().resolve_assoc_types(sig); PureFunctionEncoder { encoder, diff --git a/prusti-viper/src/encoder/mir/pure/pure_functions/new_encoder.rs b/prusti-viper/src/encoder/mir/pure/pure_functions/new_encoder.rs index a83eb4c8651..f80e4832e58 100644 --- a/prusti-viper/src/encoder/mir/pure/pure_functions/new_encoder.rs +++ b/prusti-viper/src/encoder/mir/pure/pure_functions/new_encoder.rs @@ -178,7 +178,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> PureEncoder<'p, 'v, 'tcx> { .tcx() .fn_sig(proc_def_id) .subst(encoder.env().tcx(), substs); - let sig = encoder.env().normalize_to(sig); + let sig = encoder.env().resolve_assoc_types(sig); Self { encoder, diff --git a/prusti-viper/src/encoder/mir/specifications/constraints.rs b/prusti-viper/src/encoder/mir/specifications/constraints.rs index 58c8cf70ea3..710a1f9b8e9 100644 --- a/prusti-viper/src/encoder/mir/specifications/constraints.rs +++ b/prusti-viper/src/encoder/mir/specifications/constraints.rs @@ -166,7 +166,7 @@ pub mod trait_bounds { // This needs to be done because ghost constraints might contain "deeply nested" // associated types, e.g. `T: A::OtherAssocType` // where `::OtherAssocType` can be normalized to some concrete type. - let normalized_predicate = env.normalize_to(predicate); + let normalized_predicate = env.resolve_assoc_types(predicate); env.evaluate_predicate(normalized_predicate, param_env_lookup) }); From 43a5387c51ec6a0f9836cf4c48afbb8fa0916c32 Mon Sep 17 00:00:00 2001 From: Jonas Hansen Date: Fri, 29 Apr 2022 11:03:20 +0200 Subject: [PATCH 11/38] Pass ParamEnv to resolve_assoc_types, make it fallible --- prusti-interface/src/environment/mod.rs | 53 ++++++------------- .../mir/pure/pure_functions/encoder.rs | 4 +- .../mir/pure/pure_functions/new_encoder.rs | 4 +- .../encoder/mir/specifications/constraints.rs | 2 +- 4 files changed, 23 insertions(+), 40 deletions(-) diff --git a/prusti-interface/src/environment/mod.rs b/prusti-interface/src/environment/mod.rs index 2bac2a735be..d6806a31038 100644 --- a/prusti-interface/src/environment/mod.rs +++ b/prusti-interface/src/environment/mod.rs @@ -507,12 +507,9 @@ impl<'tcx> Environment<'tcx> { /// The type is wrapped into a `Binder` to handle regions correctly. pub fn type_is_copy(&self, ty: ty::Binder<'tcx, ty::Ty<'tcx>>, param_env: ty::ParamEnv<'tcx>) -> bool { // Normalize the type to account for associated types - let ty = self.resolve_assoc_types(ty); - let ty = self.tcx.erase_regions(ty); + let ty = self.resolve_assoc_types(ty, param_env); let ty = self.tcx.erase_late_bound_regions(ty); - self.tcx.infer_ctxt().enter(|infcx| - infcx.type_is_copy_modulo_regions(param_env, ty, rustc_span::DUMMY_SP) - ) + ty.is_copy_modulo_regions(self.tcx.at(rustc_span::DUMMY_SP), param_env) } /// Checks whether the given type implements the trait with the given DefId. @@ -556,41 +553,23 @@ impl<'tcx> Environment<'tcx> { }) } - /// A facade for [rustc_trait_selection::traits::normalize_to] /// Normalizes associated types in foldable types, /// i.e. this resolves projection types ([ty::TyKind::Projection]s) - pub fn resolve_assoc_types + Copy>(&self, normalizable: T) -> T { - use rustc_trait_selection::traits; - - if !normalizable.has_projections() { - return normalizable - } + /// **Important:** Regions while be erased during this process + pub fn resolve_assoc_types + std::fmt::Debug + Copy>(&self, normalizable: T, param_env: ty::ParamEnv<'tcx>) -> T { + let norm_res = self.tcx.try_normalize_erasing_regions( + param_env, + normalizable + ); - self.tcx.infer_ctxt().enter(|infcx| { - let mut selcx = traits::SelectionContext::new(&infcx); - // We do not really care about obligations that are constructed - // in the normalization process - let mut obligations = vec![]; - - let normalized = traits::normalize_to( - &mut selcx, - ty::ParamEnv::reveal_all(), - traits::ObligationCause::dummy(), - normalizable, - &mut obligations, - ); - - // We probably normalized a bit too much. - // When we normalize an "unnormalizable" associated type - // (e.g. an associated type on a trait whose projection can not be resolved), - // "normalize_to" returns a type which needs to be infered. - // This is not what we want for e.g. a check whether a type is `Copy` or not. - // We thus return the original type in this case. - if normalized.needs_infer() { - return normalizable + match norm_res { + Ok(normalized) => { + debug!("Normalized {:?}: {:?}", normalizable, normalized); + normalized}, + Err(err) => { + debug!("Error while resolving associated types for {:?}: {:?}", normalizable, err); + normalizable } - - normalized - }) + } } } diff --git a/prusti-viper/src/encoder/mir/pure/pure_functions/encoder.rs b/prusti-viper/src/encoder/mir/pure/pure_functions/encoder.rs index 4245f7b8dad..73e17a784b3 100644 --- a/prusti-viper/src/encoder/mir/pure/pure_functions/encoder.rs +++ b/prusti-viper/src/encoder/mir/pure/pure_functions/encoder.rs @@ -107,7 +107,9 @@ impl<'p, 'v: 'p, 'tcx: 'v> PureFunctionEncoder<'p, 'v, 'tcx> { .tcx() .fn_sig(proc_def_id) .subst(encoder.env().tcx(), substs); - let sig = encoder.env().resolve_assoc_types(sig); + let sig = encoder + .env() + .resolve_assoc_types(sig, encoder.env().tcx().param_env(proc_def_id)); PureFunctionEncoder { encoder, diff --git a/prusti-viper/src/encoder/mir/pure/pure_functions/new_encoder.rs b/prusti-viper/src/encoder/mir/pure/pure_functions/new_encoder.rs index f80e4832e58..e923758c0c3 100644 --- a/prusti-viper/src/encoder/mir/pure/pure_functions/new_encoder.rs +++ b/prusti-viper/src/encoder/mir/pure/pure_functions/new_encoder.rs @@ -178,7 +178,9 @@ impl<'p, 'v: 'p, 'tcx: 'v> PureEncoder<'p, 'v, 'tcx> { .tcx() .fn_sig(proc_def_id) .subst(encoder.env().tcx(), substs); - let sig = encoder.env().resolve_assoc_types(sig); + let sig = encoder + .env() + .resolve_assoc_types(sig, encoder.env().tcx().param_env(proc_def_id)); Self { encoder, diff --git a/prusti-viper/src/encoder/mir/specifications/constraints.rs b/prusti-viper/src/encoder/mir/specifications/constraints.rs index 710a1f9b8e9..9315d3979dd 100644 --- a/prusti-viper/src/encoder/mir/specifications/constraints.rs +++ b/prusti-viper/src/encoder/mir/specifications/constraints.rs @@ -166,7 +166,7 @@ pub mod trait_bounds { // This needs to be done because ghost constraints might contain "deeply nested" // associated types, e.g. `T: A::OtherAssocType` // where `::OtherAssocType` can be normalized to some concrete type. - let normalized_predicate = env.resolve_assoc_types(predicate); + let normalized_predicate = env.resolve_assoc_types(predicate, param_env_lookup); env.evaluate_predicate(normalized_predicate, param_env_lookup) }); From b604cd4b861afa56937741d9fe79819e7b495707 Mon Sep 17 00:00:00 2001 From: Jonas Hansen Date: Fri, 29 Apr 2022 20:44:45 +0200 Subject: [PATCH 12/38] Small cleanups --- prusti-interface/src/environment/mod.rs | 12 +++--------- 1 file changed, 3 insertions(+), 9 deletions(-) diff --git a/prusti-interface/src/environment/mod.rs b/prusti-interface/src/environment/mod.rs index d6806a31038..f66449f26d1 100644 --- a/prusti-interface/src/environment/mod.rs +++ b/prusti-interface/src/environment/mod.rs @@ -493,14 +493,7 @@ impl<'tcx> Environment<'tcx> { } pub fn type_is_allowed_in_pure_functions(&self, ty: ty::Binder<'tcx, ty::Ty<'tcx>>, param_env: ty::ParamEnv<'tcx>) -> bool { - match ty.skip_binder().kind() { - ty::TyKind::Never => { - true - } - _ => { - self.type_is_copy(ty, param_env) - } - } + self.type_is_copy(ty, param_env) } /// Checks whether `ty` is copy. @@ -565,7 +558,8 @@ impl<'tcx> Environment<'tcx> { match norm_res { Ok(normalized) => { debug!("Normalized {:?}: {:?}", normalizable, normalized); - normalized}, + normalized + }, Err(err) => { debug!("Error while resolving associated types for {:?}: {:?}", normalizable, err); normalizable From 5dc9705cd69be751dfe5158b0563dde831d05b57 Mon Sep 17 00:00:00 2001 From: Jonas Hansen Date: Wed, 20 Apr 2022 19:31:27 +0200 Subject: [PATCH 13/38] Add custom iterator tests --- .../tests/verify/pass/iterators/custom-iter-counter.rs | 8 ++++++++ 1 file changed, 8 insertions(+) create mode 100644 prusti-tests/tests/verify/pass/iterators/custom-iter-counter.rs diff --git a/prusti-tests/tests/verify/pass/iterators/custom-iter-counter.rs b/prusti-tests/tests/verify/pass/iterators/custom-iter-counter.rs new file mode 100644 index 00000000000..d358fb502b5 --- /dev/null +++ b/prusti-tests/tests/verify/pass/iterators/custom-iter-counter.rs @@ -0,0 +1,8 @@ +// TODO iterators tbd +// ignore-test + +use prusti_contracts::*; + +fn main() { + +} \ No newline at end of file From f8f2859b73354e43585b560bdbc5c329d4a28b2d Mon Sep 17 00:00:00 2001 From: Jonas Hansen Date: Thu, 21 Apr 2022 16:29:29 +0200 Subject: [PATCH 14/38] Add flag to add experimental iterator support --- docs/dev-guide/src/config/flags.md | 7 +++++++ prusti-common/src/config.rs | 6 ++++++ prusti-viper/src/encoder/procedure_encoder.rs | 4 ++-- 3 files changed, 15 insertions(+), 2 deletions(-) diff --git a/docs/dev-guide/src/config/flags.md b/docs/dev-guide/src/config/flags.md index 91ca7a1bba6..5cdcbe35689 100644 --- a/docs/dev-guide/src/config/flags.md +++ b/docs/dev-guide/src/config/flags.md @@ -21,6 +21,7 @@ | [`DUMP_VIPER_PROGRAM`](#dump_viper_program) | `bool` | `false` | | [`ENABLE_CACHE`](#enable_cache) | `bool` | `true` | | [`ENABLE_GHOST_CONSTRAINTS`](#enable_ghost_constraints) | `bool` | `false` | +| [`ENABLE_ITERATORS`](#enable_iterators) | `bool` | `false` | | [`ENABLE_PURIFICATION_OPTIMIZATION`](#enable_purification_optimization) | `bool` | `false` | | [`ENABLE_VERIFY_ONLY_BASIC_BLOCK_PATH`](#enable_verify_only_basic_block_path) | `bool` | `false` | | [`ENCODE_BITVECTORS`](#encode_bitvectors) | `bool` | `false` | @@ -141,6 +142,12 @@ on a generic type parameter) is satisfied. **This is an experimental feature**, because it is currently possible to introduce unsound verification behavior. +## `ENABLE_ITERATORS` + +Enables support for iterators. + +**This is an experimental feature**, iterator support is still experimental. + ## `ENABLE_PURIFICATION_OPTIMIZATION` When enabled, impure methods are optimized using the purification optimization, which tries to convert heap operations to pure (snapshot-based) operations. diff --git a/prusti-common/src/config.rs b/prusti-common/src/config.rs index f9908c519c8..61abe686d86 100644 --- a/prusti-common/src/config.rs +++ b/prusti-common/src/config.rs @@ -113,6 +113,7 @@ lazy_static! { settings.set_default("print_hash", false).unwrap(); settings.set_default("enable_cache", true).unwrap(); settings.set_default("enable_ghost_constraints", false).unwrap(); + settings.set_default("enable_iterators", false).unwrap(); // Flags for debugging Prusti that can change verification results. settings.set_default("disable_name_mangling", false).unwrap(); @@ -599,4 +600,9 @@ pub fn intern_names() -> bool { /// Enables ghost constraint parsing and resolving. pub fn enable_ghost_constraints() -> bool { read_setting("enable_ghost_constraints") +} + +/// Enables (experimental) iterator support +pub fn enable_iterators() -> bool { + read_setting("enable_iterators") } \ No newline at end of file diff --git a/prusti-viper/src/encoder/procedure_encoder.rs b/prusti-viper/src/encoder/procedure_encoder.rs index af7e5b998d9..ef76d41f786 100644 --- a/prusti-viper/src/encoder/procedure_encoder.rs +++ b/prusti-viper/src/encoder/procedure_encoder.rs @@ -2196,9 +2196,9 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { } "std::iter::Iterator::next" | - "core::iter::Iterator::next" => { + "core::iter::Iterator::next" if !config::enable_iterators() => { return Err(SpannedEncodingError::unsupported( - "iterators are not fully supported yet", + "iterators are not fully supported yet, enable them with a feature flag", term.source_info.span, )); } From 0da3287b3807a6ee0d2ea06fd97b234601dc0725 Mon Sep 17 00:00:00 2001 From: Jonas Hansen Date: Wed, 27 Apr 2022 17:08:37 +0200 Subject: [PATCH 15/38] Move predicate normalization in constraint solver for better debugging --- .../encoder/mir/specifications/constraints.rs | 30 +++++++++++-------- 1 file changed, 17 insertions(+), 13 deletions(-) diff --git a/prusti-viper/src/encoder/mir/specifications/constraints.rs b/prusti-viper/src/encoder/mir/specifications/constraints.rs index 9315d3979dd..1a07eead801 100644 --- a/prusti-viper/src/encoder/mir/specifications/constraints.rs +++ b/prusti-viper/src/encoder/mir/specifications/constraints.rs @@ -143,10 +143,6 @@ pub mod trait_bounds { ) -> bool { debug!("Trait bound constraint resolving for {:?}", context); - let param_env_constraint = extract_param_env(env, proc_spec); - let param_env_constraint = - perform_param_env_substitutions(env, context, param_env_constraint); - // There is no caller when encoding a function. // We still resolve obligations to account for constrained specs on a trait // for which we encode its implementation. The corresponding encoding will @@ -158,18 +154,14 @@ pub mod trait_bounds { env.tcx().param_env(context.proc_def_id) }; + let param_env_constraint = extract_param_env(env, proc_spec); + let param_env_constraint = + perform_param_env_substitutions(env, context, param_env_constraint, param_env_lookup); + let all_bounds_satisfied = param_env_constraint .caller_bounds() .iter() - .all(|predicate| { - // Normalize any associated type projections. - // This needs to be done because ghost constraints might contain "deeply nested" - // associated types, e.g. `T: A::OtherAssocType` - // where `::OtherAssocType` can be normalized to some concrete type. - let normalized_predicate = env.resolve_assoc_types(predicate, param_env_lookup); - - env.evaluate_predicate(normalized_predicate, param_env_lookup) - }); + .all(|predicate| env.evaluate_predicate(predicate, param_env_lookup)); trace!("Constraint fulfilled: {all_bounds_satisfied}"); all_bounds_satisfied @@ -180,6 +172,7 @@ pub mod trait_bounds { env: &'env Environment<'tcx>, context: &ConstraintSolvingContext<'tcx>, param_env: ty::ParamEnv<'tcx>, + param_env_lookup: ty::ParamEnv<'tcx>, ) -> ty::ParamEnv<'tcx> { trace!("Unsubstituted constraints: {:#?}", param_env); @@ -208,6 +201,17 @@ pub mod trait_bounds { param_env ); + // Normalize any associated type projections. + // This needs to be done because ghost constraints might contain "deeply nested" + // associated types, e.g. `T: A::OtherAssocType` + // where `::OtherAssocType` can be normalized to some concrete type. + let param_env = env.resolve_assoc_types(param_env, param_env_lookup); + + trace!( + "Constraints after resolving associated types: {:#?}", + param_env + ); + param_env } From c1cbead24de663bb24c1fab04154bb1eb46c290d Mon Sep 17 00:00:00 2001 From: Jonas Hansen Date: Wed, 27 Apr 2022 17:20:50 +0200 Subject: [PATCH 16/38] Do not copy preconditions of base spec to constrained spec --- prusti-interface/src/specs/typed.rs | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/prusti-interface/src/specs/typed.rs b/prusti-interface/src/specs/typed.rs index f0e4c15728c..fb293080f65 100644 --- a/prusti-interface/src/specs/typed.rs +++ b/prusti-interface/src/specs/typed.rs @@ -247,7 +247,16 @@ impl SpecGraph { ) -> &mut ProcedureSpecification { self.specs_with_constraints .entry(constraint) - .or_insert_with(|| self.base_spec.clone()) + .or_insert_with(|| { + let mut base = self.base_spec.clone(); + + // Preconditions of the base spec do not appear in the constrained spec + // Any preconditions that exist on the base spec are thus pruned + // (see comment on impl block) + base.pres = SpecificationItem::Empty; + + base + }) } /// Gets the constraint of a spec function `spec`. From 59bc78cc3bdcdf361eb2142db85332108c7207a5 Mon Sep 17 00:00:00 2001 From: Jonas Hansen Date: Fri, 29 Apr 2022 11:41:50 +0200 Subject: [PATCH 17/38] Use predicate_must_hold_modulo_regions when resolving ghost constraints to account for references in associated types --- prusti-interface/src/environment/mod.rs | 2 +- .../ghost-constraints/associated-types-6.rs | 38 +++++++++++++++++++ 2 files changed, 39 insertions(+), 1 deletion(-) create mode 100644 prusti-tests/tests/verify_overflow/pass/ghost-constraints/associated-types-6.rs diff --git a/prusti-interface/src/environment/mod.rs b/prusti-interface/src/environment/mod.rs index f66449f26d1..5c50c8d844a 100644 --- a/prusti-interface/src/environment/mod.rs +++ b/prusti-interface/src/environment/mod.rs @@ -542,7 +542,7 @@ impl<'tcx> Environment<'tcx> { ); self.tcx.infer_ctxt().enter(|infcx| { - infcx.predicate_must_hold_considering_regions(&obligation) + infcx.predicate_must_hold_modulo_regions(&obligation) }) } diff --git a/prusti-tests/tests/verify_overflow/pass/ghost-constraints/associated-types-6.rs b/prusti-tests/tests/verify_overflow/pass/ghost-constraints/associated-types-6.rs new file mode 100644 index 00000000000..33a93a7b64e --- /dev/null +++ b/prusti-tests/tests/verify_overflow/pass/ghost-constraints/associated-types-6.rs @@ -0,0 +1,38 @@ +// compile-flags: -Penable_ghost_constraints=true + +use prusti_contracts::*; + +trait A<'a> { + type AType; +} + +trait B<'a> { + type BType; + + #[ghost_constraint(Self: A<'a, AType = >::BType> , [ + ensures(*result > 0) + ])] + #[trusted] + fn foo(&'a self) -> &'a i32; +} + +struct S { + val: i32, +} +impl<'a> A<'a> for S { + type AType = &'a i32; +} + +impl<'a> B<'a> for S { + type BType = &'a i32; + + #[trusted] + fn foo(&'a self) -> &'a i32 { &self.val } +} + +fn main() { + let s = S { + val: 42 + }; + assert!(*s.foo() > 0); +} \ No newline at end of file From 0af45d7fe2fdfe481dbdae9b2da50bf41b47fdb4 Mon Sep 17 00:00:00 2001 From: Jonas Hansen Date: Fri, 29 Apr 2022 11:58:24 +0200 Subject: [PATCH 18/38] Handle lifetimes in merge_generics --- prusti-specs/src/common.rs | 58 +++++++++++++++++++++++++++++--------- 1 file changed, 44 insertions(+), 14 deletions(-) diff --git a/prusti-specs/src/common.rs b/prusti-specs/src/common.rs index 5a85cd6b6dd..b68543760db 100644 --- a/prusti-specs/src/common.rs +++ b/prusti-specs/src/common.rs @@ -3,7 +3,7 @@ use std::borrow::BorrowMut; use std::collections::HashMap; use proc_macro2::Ident; -use syn::{GenericParam, parse_quote, TypeParam}; +use syn::{GenericParam, LifetimeDef, parse_quote, TypeParam}; use syn::punctuated::Punctuated; use syn::spanned::Spanned; use uuid::Uuid; @@ -328,7 +328,7 @@ mod receiver_rewriter { } /// Copies the [syn::Generics] of `source` to the generics of `target` -/// **Important**: Lifetimes and const params are currently ignored. +/// **Important**: Const params are currently ignored. /// If `source` has generic params which do not appear in `target`, they are added first. /// /// # Example @@ -347,25 +347,40 @@ pub(crate) fn merge_generics(target: &mut T, source: &T) { // Merge all type params let mut existing_target_type_params: HashMap = HashMap::new(); + let mut existing_target_lifetimes: HashMap = HashMap::new(); let mut new_generic_params: Vec = Vec::new(); for param_target in generics_target.params.iter_mut() { - if let GenericParam::Type(type_param_target) = param_target { - existing_target_type_params.insert(type_param_target.ident.clone(), type_param_target); + match param_target { + GenericParam::Type(t) => { + existing_target_type_params.insert(t.ident.clone(), t); + }, + GenericParam::Lifetime(lt) => { + existing_target_lifetimes.insert(lt.lifetime.ident.clone(), lt); + }, + _ => () // not supported } } for param_source in generics_source.params.iter() { - // Lifetimes and consts are currently not handled - if let GenericParam::Type(type_param_source) = param_source { - // We can remove the target type param here, because the source will not have the - // same type param with the same identifiers - let maybe_type_param_source = existing_target_type_params.remove(&type_param_source.ident); - if let Some(type_param_target) = maybe_type_param_source { - type_param_target.bounds.extend(type_param_source.bounds.clone()); - } else { - new_generic_params.push(GenericParam::Type(type_param_source.clone())); - } + // Consts are currently not handled + match param_source { + GenericParam::Type(type_param_source) => { + if let Some(type_param_target) = existing_target_type_params.remove(&type_param_source.ident) { + type_param_target.bounds.extend(type_param_source.bounds.clone()); + } else { + new_generic_params.push(GenericParam::Type(type_param_source.clone())); + } + }, + GenericParam::Lifetime(lifetime_source) => { + if let Some(lifetime_target) = existing_target_lifetimes.remove(&lifetime_source.lifetime.ident) { + lifetime_target.bounds.extend(lifetime_source.bounds.clone()); + } else { + new_generic_params.push(GenericParam::Lifetime(lifetime_source.clone())); + } + }, + _ => () // not supported } + } // Merge the new parameters with the existing ones. @@ -521,6 +536,21 @@ mod tests { [impl Foo for Bar where T: A {}] } } + + #[test] + fn lifetimes() { + test_merge! { + [impl<'b> Foo for Bar {}] into + [impl<'a> Foo for Bar {}] gives + [impl<'b, 'a> Foo for Bar {}] + } + + test_merge! { + [impl<'a: 'c, 'd> Foo for Bar {}] into + [impl<'a: 'b> Foo for Bar {}] gives + [impl<'d, 'a: 'b + 'c> Foo for Bar {}] + } + } } mod phantom_data { From c527dc1622fcd313659c860ee13400297b92ec0b Mon Sep 17 00:00:00 2001 From: Jonas Hansen Date: Mon, 2 May 2022 21:37:18 +0200 Subject: [PATCH 19/38] Support lifetimes in type models --- prusti-specs/src/common.rs | 11 +++- prusti-specs/src/type_model/mod.rs | 96 ++++++++++++++---------------- 2 files changed, 55 insertions(+), 52 deletions(-) diff --git a/prusti-specs/src/common.rs b/prusti-specs/src/common.rs index b68543760db..09423e749b2 100644 --- a/prusti-specs/src/common.rs +++ b/prusti-specs/src/common.rs @@ -14,6 +14,7 @@ pub(crate) use receiver_rewriter::*; /// Module which provides various extension traits for syn types. /// These allow for writing of generic code over these types. mod syn_extensions { + use proc_macro2::Ident; use syn::{Attribute, Generics, ImplItemMacro, ImplItemMethod, ItemFn, ItemImpl, ItemStruct, ItemTrait, Macro, Signature, TraitItemMacro, TraitItemMethod}; /// Trait which signals that the corresponding syn item contains generics @@ -129,6 +130,14 @@ mod syn_extensions { &self.attrs } } + + // Abstraction over everything that has a [syn::Ident] + pub(crate) trait HasIdent { + fn ident(&self) -> &Ident; + } + + impl HasIdent for ItemTrait { fn ident(&self) -> &Ident { &self.ident } } + impl HasIdent for ItemStruct { fn ident(&self) -> &Ident { &self.ident } } } /// See [SelfTypeRewriter] @@ -438,7 +447,7 @@ pub(crate) fn add_phantom_data_for_generic_params(item_struct: &mut syn::ItemStr } syn::GenericParam::Lifetime(lt_def) => { let lt = <_def.lifetime; - let ty: syn::Type = parse_quote!(&#lt ::core::marker::PhantomData<()>); + let ty: syn::Type = parse_quote!(::core::marker::PhantomData<&#lt ()>); Some(ty) } _ => None, diff --git a/prusti-specs/src/type_model/mod.rs b/prusti-specs/src/type_model/mod.rs index 44ec3db80a6..4023de7c9e1 100644 --- a/prusti-specs/src/type_model/mod.rs +++ b/prusti-specs/src/type_model/mod.rs @@ -23,8 +23,9 @@ use crate::{ }; use proc_macro2::{Ident, TokenStream}; use quote::ToTokens; -use syn::{parse_quote, punctuated::Punctuated, spanned::Spanned}; +use syn::{parse_quote, spanned::Spanned}; use uuid::Uuid; +use crate::common::{HasGenerics, HasIdent}; /// See module level documentation pub fn rewrite(item_struct: syn::ItemStruct) -> syn::Result { @@ -76,6 +77,14 @@ impl ModelStruct { struct #model_struct_ident {} }; + // Attach lifetimes + for gp in item_struct.generics.params.iter() { + if let syn::GenericParam::Lifetime(lt) = gp { + model_struct.generics.params.push(syn::GenericParam::Lifetime(lt.clone())); + } + } + + // Attach type params let params = item_struct .parse_user_annotated_type_params() .map_err(TypeModelGenerationError::NonParsableTypeParam)?; @@ -90,22 +99,9 @@ impl ModelStruct { model_struct.fields = item_struct.fields.clone(); add_phantom_data_for_generic_params(&mut model_struct); - let generic_idents = model_struct - .generics - .params - .iter() - .filter_map(|generic_param| match generic_param { - syn::GenericParam::Type(type_param) => Some(&type_param.ident), - _ => None, - }); - let model_path: syn::Path = parse_quote!( - #model_struct_ident < #(#generic_idents),* > - ); + let path = create_path(&model_struct); - Ok(Self { - item: model_struct, - path: model_path, - }) + Ok(Self { item: model_struct, path, }) } } @@ -124,18 +120,10 @@ impl ToModelTrait { ) -> Self { let generic_params: Vec = model_struct.item.generics.params.iter().cloned().collect(); - let generic_params_idents: Vec = generic_params - .iter() - .filter_map(|generic_param| match generic_param { - syn::GenericParam::Type(type_param) => Some(type_param.ident.clone()), - _ => None, - }) - .collect(); let model_path = &model_struct.path; - let to_model_trait_ident = &idents.to_model_trait_ident; - let item = parse_quote_spanned! {item_struct.span()=> + let item: syn::ItemTrait = parse_quote_spanned! {item_struct.span()=> #[allow(non_camel_case_types)] trait #to_model_trait_ident<#(#generic_params),*> { #[pure] @@ -145,9 +133,7 @@ impl ToModelTrait { } }; - let path: syn::Path = parse_quote!( - #to_model_trait_ident<#(#generic_params_idents),*> - ); + let path = create_path(&item); Self { item, path } } @@ -158,32 +144,18 @@ fn create_model_impl( model_struct: &ModelStruct, to_model_trait: &ToModelTrait, ) -> TypeModelGenerationResult { - let ident = &item_struct.ident; - - let mut rewritten_generics: Vec = Vec::new(); for param in &item_struct.generics.params { - match param { - syn::GenericParam::Lifetime(_) => rewritten_generics.push(parse_quote!('_)), - syn::GenericParam::Type(type_param) => { - let mut cloned = type_param.clone(); - cloned.attrs.clear(); - cloned.bounds = Punctuated::default(); - rewritten_generics.push(syn::GenericParam::Type(cloned)) - } - syn::GenericParam::Const(const_param) => { - return Err(TypeModelGenerationError::ConstParamDisallowed( - const_param.span(), - )) - } + if let syn::GenericParam::Const(const_param) = param { + return Err(TypeModelGenerationError::ConstParamDisallowed( + const_param.span(), + )) } } let generic_params: Vec = model_struct.item.generics.params.iter().cloned().collect(); - let impl_path: syn::Path = parse_quote!( - #ident < #(#rewritten_generics),* > - ); + let impl_path = create_path(item_struct); let to_model_trait_path = &to_model_trait.path; let model_struct_path = &model_struct.path; @@ -280,6 +252,22 @@ impl ToTokens for TypeModel { } } +fn create_path(pathable: &T) -> syn::Path { + let ident = &pathable.ident(); + + let generic_idents = pathable.generics().params.iter() + .filter_map(|generic_param| match generic_param { + syn::GenericParam::Lifetime(lt_def) => + Some(lt_def.lifetime.to_token_stream()), + syn::GenericParam::Type(type_param) => + Some(type_param.ident.to_token_stream()), + _ => None, + }); + parse_quote! { + #ident < #(#generic_idents),* > + } +} + #[cfg(test)] mod tests { use super::*; @@ -386,7 +374,7 @@ mod tests { } #[test] - fn ok_uses_inferred_lifetime() { + fn ok_uses_defined_lifetime() { let input: syn::ItemStruct = parse_quote!( struct Foo<'a, 'b>(i32, u32, usize); ); @@ -398,14 +386,20 @@ mod tests { let expected_struct: syn::ItemStruct = parse_quote!( #[derive(Copy, Clone)] #[allow(non_camel_case_types)] - struct #model_ident(i32, u32, usize); + struct #model_ident<'a, 'b>( + i32, + u32, + usize, + ::core::marker::PhantomData<&'a()>, + ::core::marker::PhantomData<&'b()> + ); ); let expected_impl: syn::ItemImpl = parse_quote!( #[prusti::type_models_to_model_impl] - impl #trait_ident<> for Foo<'_, '_> { + impl<'a, 'b> #trait_ident<'a, 'b> for Foo<'a, 'b> { #[trusted] #[pure] - fn model(&self) -> #model_ident<> { + fn model(&self) -> #model_ident<'a, 'b> { unimplemented!("Models can only be used in specifications") } } From c8081fbd1e94d5eac6fb48c706c9f0fedb96797d Mon Sep 17 00:00:00 2001 From: Jonas Hansen Date: Mon, 2 May 2022 23:02:43 +0200 Subject: [PATCH 20/38] Relax needs_infer check in Environment::resolve_method_call to ignore non-resolved lifetimes --- prusti-interface/src/environment/mod.rs | 39 +++++++++++++++++++++---- 1 file changed, 34 insertions(+), 5 deletions(-) diff --git a/prusti-interface/src/environment/mod.rs b/prusti-interface/src/environment/mod.rs index 5c50c8d844a..dc1b0e3feb7 100644 --- a/prusti-interface/src/environment/mod.rs +++ b/prusti-interface/src/environment/mod.rs @@ -477,10 +477,10 @@ impl<'tcx> Environment<'tcx> { called_def_id: ProcedureDefId, // what are we calling? call_substs: SubstsRef<'tcx>, ) -> (ProcedureDefId, SubstsRef<'tcx>) { - use crate::rustc_middle::ty::TypeFoldable; - - // avoids a compiler-internal panic - if call_substs.needs_infer() { + // Avoids a compiler-internal panic + // this check ignores any lifetimes/regions, which at this point would + // need inference. They are thus ignored. + if self.any_type_needs_infer(call_substs) { return (called_def_id, call_substs); } @@ -566,4 +566,33 @@ impl<'tcx> Environment<'tcx> { } } } -} + + fn any_type_needs_infer>(&self, t: T) -> bool { + // Helper + fn is_nested_ty(ty: ty::Ty<'_>) -> bool { + let mut walker = ty.walk(); + let first = walker.next().unwrap().expect_ty(); // This is known to yield t + assert!(ty == first); + walker.next().is_some() + } + + // Visitor + struct NeedsInfer; + impl<'tcx> ty::fold::TypeVisitor<'tcx> for NeedsInfer { + type BreakTy = (); + + fn visit_ty(&mut self, ty: ty::Ty<'tcx>) -> std::ops::ControlFlow { + use crate::rustc_middle::ty::TypeFoldable; + if is_nested_ty(ty) { + ty.super_visit_with(self) + } else if ty.needs_infer() { + std::ops::ControlFlow::BREAK + } else { + std::ops::ControlFlow::CONTINUE + } + } + } + + t.visit_with(&mut NeedsInfer).is_break() + } +} \ No newline at end of file From af55da2171ea80b1c726f635274f90a7fed9b771 Mon Sep 17 00:00:00 2001 From: Jonas Hansen Date: Tue, 3 May 2022 08:26:57 +0200 Subject: [PATCH 21/38] Support lifetimes in type models --- prusti-specs/src/common.rs | 14 ++++---------- 1 file changed, 4 insertions(+), 10 deletions(-) diff --git a/prusti-specs/src/common.rs b/prusti-specs/src/common.rs index 09423e749b2..eedecabaa50 100644 --- a/prusti-specs/src/common.rs +++ b/prusti-specs/src/common.rs @@ -664,16 +664,10 @@ mod tests { fn assert_phantom_ref_for(expected_lifetime: &str, actual_field: &syn::Field) { match &actual_field.ty { - syn::Type::Reference(type_ref) => { - let actual_lifetime = type_ref.lifetime.as_ref().expect("Expected lifetime"); - assert_eq!(expected_lifetime, actual_lifetime.to_string().trim()); - - let ty = type_ref.elem.as_ref(); - assert_eq!( - "::core::marker::PhantomData<()>", - ty.to_token_stream().to_string().replace(' ', "") - ); - } + syn::Type::Path(type_path) => { + let actual_type = type_path.path.to_token_stream().to_string().replace(" ", ""); + assert_eq!(format!("::core::marker::PhantomData<&{}()>", expected_lifetime), actual_type); + }, _ => panic!(), } } From 8c7a2abf334a1b801b4b8d41e831a17ad7631a06 Mon Sep 17 00:00:00 2001 From: Jonas Hansen Date: Tue, 3 May 2022 10:23:41 +0200 Subject: [PATCH 22/38] Add first tests --- .../pass/iterators/custom-iter-counter.rs | 8 - .../pass/iterators/custom-counter.rs | 272 ++++++++++++++++++ .../pass/iterators/slice-iter.rs | 231 +++++++++++++++ 3 files changed, 503 insertions(+), 8 deletions(-) delete mode 100644 prusti-tests/tests/verify/pass/iterators/custom-iter-counter.rs create mode 100644 prusti-tests/tests/verify_overflow/pass/iterators/custom-counter.rs create mode 100644 prusti-tests/tests/verify_overflow/pass/iterators/slice-iter.rs diff --git a/prusti-tests/tests/verify/pass/iterators/custom-iter-counter.rs b/prusti-tests/tests/verify/pass/iterators/custom-iter-counter.rs deleted file mode 100644 index d358fb502b5..00000000000 --- a/prusti-tests/tests/verify/pass/iterators/custom-iter-counter.rs +++ /dev/null @@ -1,8 +0,0 @@ -// TODO iterators tbd -// ignore-test - -use prusti_contracts::*; - -fn main() { - -} \ No newline at end of file diff --git a/prusti-tests/tests/verify_overflow/pass/iterators/custom-counter.rs b/prusti-tests/tests/verify_overflow/pass/iterators/custom-counter.rs new file mode 100644 index 00000000000..8f5b1481a2d --- /dev/null +++ b/prusti-tests/tests/verify_overflow/pass/iterators/custom-counter.rs @@ -0,0 +1,272 @@ +// compile-flags: -Penable_iterators=true +// compile-flags: -Penable_ghost_constraints=true + +extern crate prusti_contracts; +use prusti_contracts::*; + +type IterItemTy = usize; + +trait IteratorSpecExt { + type IterItem; + + predicate! { + fn enumerated(&self) -> bool; + } + + predicate! { + fn completed(&self) -> bool; + } + + predicate! { + fn two_state_postcondition(new_self: &Self, old_self: &Self) -> bool; + } + + predicate! { + fn describe_result(old_self: &Self, res: &Option) -> bool; + } +} + +pub struct Counter { + seen: Vec, + count: usize, + up_to: usize, +} + +#[extern_spec] +trait Iterator { + #[requires(false)] + #[ghost_constraint(Self: IteratorSpecExt::Item> , [ + requires(self.enumerated()), + ensures(self.enumerated()), + ensures( + (!old(self.completed()) == result.is_some()) && + (old(self.completed()) == result.is_none()) && + (old(self.completed()) ==> self.completed()) + ), + ensures(IteratorSpecExt::two_state_postcondition(self, old(self))), + ensures(IteratorSpecExt::describe_result(old(self), &result)) + ])] + fn next(&mut self) -> Option; +} + +#[refine_trait_spec] +impl IteratorSpecExt for Counter { + type IterItem = IterItemTy; + + predicate! { + fn enumerated(&self) -> bool { + self.count == vec_len(&self.seen) && + forall( + |i: usize| 0 <= i && i < vec_len(&self.seen) ==> ( + vec_lookup(&self.seen, i) == i && + vec_contains(&self.seen, i) + ) + ) + } + } + + predicate! { + fn completed(&self) -> bool { + self.count >= self.up_to + } + } + + predicate! { + fn two_state_postcondition(new_self: &Self, old_self: &Self) -> bool { + new_self.up_to == old_self.up_to && + vec_equals_up_to_idx(&new_self.seen, &old_self.seen, vec_len(&old_self.seen)) && + vec_is_subset(&old_self.seen, &new_self.seen) && + + old_self.completed() == (new_self.count == old_self.count) && + !old_self.completed() == (new_self.count == old_self.count + 1) + } + } + + predicate! { + fn describe_result(old_self: &Self, res: &Option) -> bool { + res.is_some() ==> res.peek() == old_self.count + } + } +} + +#[refine_trait_spec] +impl Iterator for Counter { + type Item = IterItemTy; + + // Note: The method body is verified against the ghost constraint! + #[trusted] + fn next(&mut self) -> Option { + if self.count < self.up_to { + let res = self.count; + self.count += 1; + vec_push(&mut self.seen, res); + return Some(res); + } + None + } +} + +fn verify_direct_traversal() { + let mut c = Counter { + count: 0, + up_to: 3, + seen: vec_create(), + }; + + let el = c.next(); + assert!(el.is_some()); + assert!(el.peek() == 0); + + let el = c.next(); + assert!(el.is_some()); + assert!(el.peek() == 1); + + let el = c.next(); + assert!(el.is_some()); + assert!(el.peek() == 2); + + let el = c.next(); + assert!(el.is_none()); + + let el = c.next(); + assert!(el.is_none()); +} + +#[requires( + c.count == 0 && + c.up_to == 3 && + vec_len(&c.seen) == 0 +)] +// #[ensures(is_max_of(result, &c.seen))] // TODO iterators: This causes a Prusti crash +fn verify_get_max(mut c: Counter) -> IterItemTy { + let mut el: Option = None; + el = c.next(); + assert!(el.is_some()); + let mut the_max = el.peek(); + + while { + el = c.next(); + el.is_some() + } { + let val = el.peek(); + if val >= the_max { + the_max = val; + } + + body_invariant!(c.enumerated()); + body_invariant!(vec_contains(&c.seen, the_max)); + body_invariant!(is_max_of(the_max, &c.seen)); + } + assert!(c.next().is_none()); + the_max +} + + +predicate! { + fn is_max_of(potential_max: IterItemTy, v: &VecType) -> bool { + forall( + |i: usize| (0 <= i && i < vec_len(v)) ==> potential_max >= vec_lookup(v, i) + ) + } +} + +fn main() {} + +// VEC +type VecInnerType = IterItemTy; +type VecType = Vec; + +#[trusted] +#[ensures(vec_len(v) == old(vec_len(v)) + 1)] +#[ensures(vec_contains(v, elem))] +#[ensures(vec_lookup(v, vec_len(v) - 1) == elem)] +#[ensures(vec_equals_up_to_idx(v, old(v), old(vec_len(v))))] +#[ensures(vec_is_subset(old(v), v))] +fn vec_push(v: &mut VecType, elem: VecInnerType) { + v.push(elem); +} + +#[pure] +#[trusted] +fn vec_contains(v: &VecType, elem: VecInnerType) -> bool { + v.contains(&elem) +} + +#[pure] +#[trusted] +fn vec_len(v: &VecType) -> usize { + v.len() +} + +#[pure] +#[trusted] +#[requires(i < vec_len(v))] +#[ensures(vec_contains(v, result))] +fn vec_lookup(v: &VecType, i: usize) -> VecInnerType { + v[i] +} + +#[trusted] +#[ensures(vec_len(&result) == 0)] +fn vec_create() -> VecType { + unimplemented!(); +} + +predicate! { + fn vec_equals(v1: &VecType, v2: &VecType) -> bool { + vec_len(v1) == vec_len(v2) && + forall( + |i: usize| i < vec_len(v1) ==> vec_lookup(v1, i) == vec_lookup(v2, i) + ) && + forall( + |el: usize| vec_contains(v1, el) == vec_contains(v2, el) + ) + } +} + +predicate! { + fn vec_equals_up_to_idx(v1: &VecType, v2: &VecType, up_to_idx: usize) -> bool { + vec_len(v1) >= up_to_idx && vec_len(v2) >= up_to_idx && + forall( + |i: usize| i < up_to_idx ==> vec_lookup(v1, i) == vec_lookup(v2, i) + ) + } +} + +predicate! { + fn vec_is_subset(subset: &VecType, superset: &VecType) -> bool { + forall( + |el: usize| vec_contains(subset, el) ==> vec_contains(superset, el) + ) + } +} + +// OPTION +#[extern_spec] +impl std::option::Option { + #[pure] + #[ensures(matches ! (* self, Some(_)) == result)] + pub fn is_some(&self) -> bool; + + #[pure] + #[ensures(self.is_some() == ! result)] + #[ensures(matches ! (* self, None) == result)] + pub fn is_none(&self) -> bool; +} + +trait OptionPeeker { + #[pure] + fn peek(&self) -> T; +} + +#[refine_trait_spec] +impl OptionPeeker for Option { + #[pure] + #[requires(self.is_some())] + fn peek(&self) -> T { + match self { + Some(v) => *v, + None => unreachable!(), + } + } +} \ No newline at end of file diff --git a/prusti-tests/tests/verify_overflow/pass/iterators/slice-iter.rs b/prusti-tests/tests/verify_overflow/pass/iterators/slice-iter.rs new file mode 100644 index 00000000000..f3fa4fae339 --- /dev/null +++ b/prusti-tests/tests/verify_overflow/pass/iterators/slice-iter.rs @@ -0,0 +1,231 @@ +// compile-flags: -Penable_iterators=true +// compile-flags: -Penable_ghost_constraints=true + +#![feature(associated_type_bounds)] +extern crate prusti_contracts; +use prusti_contracts::*; + +use std::slice::Iter; +use std::cmp::PartialEq; +use std::iter::Iterator; + +trait IteratorSpecExt { + type IterItem: Copy; + + #[pure] + #[trusted] + fn visited(&self) -> GhostSeq { + unimplemented!() + } + + predicate! { + fn enumerated(&self) -> bool; + } + + predicate! { + fn two_state_postcondition(new_self: &Self, old_self: &Self) -> bool; + } + + predicate! { + fn completed(&self) -> bool; + } +} + +#[model] +struct Iter<'a, #[generic] T: Copy+PartialEq+Sized> { + position: usize, + data: GhostSeq, +} + +type SliceTy = [T]; +#[extern_spec] +impl SliceTy { + #[pure] + fn len(&self) -> usize; + + // Initialize the model + #[requires(self.len() >= 0)] + #[ensures( result.model().position == 0 )] + #[ensures( result.model().data.len() == self.len() )] + #[ensures( + forall(|i: usize| 0 <= i && i < self.len() ==> ( + self[i] == result.model().data.lookup(i) + )) + )] + // Initialize ghost sequence of visited values + #[ensures( + result.visited().len() == 0 + )] + fn iter(&self) -> std::slice::Iter<'_, T>; +} + +#[extern_spec] +trait Iterator { + #[requires(false)] + #[ghost_constraint(Self: IteratorSpecExt::Item> , [ + requires(self.enumerated()), + ensures(self.enumerated()), + ensures( + (!old(self.completed()) == result.is_some()) && + (old(self.completed()) == result.is_none()) && + (old(self.completed()) ==> self.completed()) + ), + ensures(IteratorSpecExt::two_state_postcondition(old(self), self)) + ])] + fn next(&mut self) -> Option; +} + +#[refine_trait_spec] +impl<'a, T: Copy + PartialEq + 'a> IteratorSpecExt for std::slice::Iter<'a, T> { + type IterItem = &'a T; + + predicate! { + fn enumerated(&self) -> bool { + self.visited().len() <= self.model().data.len() && + self.visited().len() == self.model().position && + forall(|i: usize| (0 <= i && i < self.visited().len()) ==> + self.model().data.lookup(i) == *self.visited().lookup(i) + ) + } + } + + predicate! { + fn two_state_postcondition(old_self: &Self, new_self: &Self) -> bool { + // Data does not change + // TODO iterators: Using GhostSeq::equals here does not work + new_self.model().data.len() == old_self.model().data.len() && + forall(|i: usize| (0 <= i && i < new_self.model().data.len()) ==> ( + new_self.model().data.lookup(i) == old_self.model().data.lookup(i) + )) && + + // How does the position evolve + !old_self.completed() == (new_self.model().position == old_self.model().position + 1) && + old_self.completed() == (new_self.model().position == old_self.model().position) + } + } + + predicate! { + fn completed(&self) -> bool { + self.model().position >= self.model().data.len() + } + } +} + +#[requires(iter.model().position == pos)] +#[requires(iter.model().data.len() == data_len)] +#[requires(iter.visited().len() == vis_len)] +#[trusted] +fn verify_model(iter: &std::slice::Iter, pos: usize, data_len: usize, vis_len: usize) { + +} + +#[requires(0 <= idx && idx < iter.visited().len())] +#[requires(*iter.visited().lookup(idx) == val)] +#[trusted] +fn verify_visited(iter: &std::slice::Iter, idx: usize, val: T) { + +} + +#[requires(slice.len() == 2)] +#[requires(slice[0] == 42)] +#[requires(slice[1] == 777)] +fn verify_slice_iter(slice: &[i32]) { + let mut iter = slice.iter(); + + verify_model(&iter, 0, 2, 0); + + let el = iter.next(); + assert!(el.is_some()); + verify_model(&iter, 1, 2, 1); + verify_visited(&iter, 0, 42); + + let el = iter.next(); + assert!(el.is_some()); + verify_model(&iter, 2, 2, 2); + verify_visited(&iter, 0, 42); + verify_visited(&iter, 1, 777); + + let el = iter.next(); + assert!(el.is_none()); + verify_model(&iter, 2, 2, 2); + verify_visited(&iter, 0, 42); + verify_visited(&iter, 1, 777); +} + +// TODO iterators: How to reason about visited values? +// #[requires(slice.len() == 4)] +// #[requires(slice[0] == 42)] +// #[requires(slice[1] == 777)] +// #[requires(slice[2] == 888)] +// #[requires(slice[3] == 13)] +// #[requires(seen.len() == 0)] +// fn verify_while(slice: &[i32]) { +// let mut iter = slice.iter(); +// let mut el = None; +// while { +// el = iter.next(); +// el.is_some() +// } { +// +// body_invariant!(iter.enumerated()); +// } +// assert!(iter.next().is_none()); +// verify_visited(&iter, 0, 42); +// } + +fn main() { + +} + +// OPTION +#[extern_spec] +impl std::option::Option { + #[pure] + #[ensures(self.is_none() == !result)] + #[ensures(matches ! (* self, Some(_)) == result)] + pub fn is_some(&self) -> bool; + + #[pure] + #[ensures(self.is_some() == !result)] + #[ensures(matches ! (* self, None) == result)] + pub fn is_none(&self) -> bool; +} + +// GHOST SEQUENCE +struct GhostSeq { + phantom: std::marker::PhantomData, +} +#[refine_trait_spec] +impl std::clone::Clone for GhostSeq { + #[trusted] + fn clone(&self) -> Self { unimplemented!() } +} +impl Copy for GhostSeq {} +impl GhostSeq { + #[pure] + #[trusted] + #[requires( 0 <= i && i < self.len() )] + fn lookup(&self, i: usize) -> T { + unimplemented!() + } + + #[pure] + #[trusted] + fn len(&self) -> usize { + unimplemented!() + } + + predicate! { + fn equals(&self, other: &GhostSeq) -> bool { + self.len() == other.len() && + forall(|i: usize| (0 <= i && i < self.len()) ==> (self.lookup(i) == other.lookup(i))) + } + } + + predicate! { + fn is_prefix_of(&self, other: &GhostSeq) -> bool { + self.len() <= other.len() && + forall(|i: usize| (0 <= i && i < self.len()) ==> (self.lookup(i) == other.lookup(i))) + } + } +} \ No newline at end of file From fa1c14a00e14bd52ac54c9e15b95f421c54e50c3 Mon Sep 17 00:00:00 2001 From: Jonas Hansen Date: Wed, 4 May 2022 13:48:21 +0200 Subject: [PATCH 23/38] Verification of Iter in while loop --- .../pass/iterators/slice-iter.rs | 54 ++++++++++++------- 1 file changed, 34 insertions(+), 20 deletions(-) diff --git a/prusti-tests/tests/verify_overflow/pass/iterators/slice-iter.rs b/prusti-tests/tests/verify_overflow/pass/iterators/slice-iter.rs index f3fa4fae339..eb3542db5ee 100644 --- a/prusti-tests/tests/verify_overflow/pass/iterators/slice-iter.rs +++ b/prusti-tests/tests/verify_overflow/pass/iterators/slice-iter.rs @@ -93,6 +93,7 @@ impl<'a, T: Copy + PartialEq + 'a> IteratorSpecExt for std::slice::Iter<'a, T> { fn two_state_postcondition(old_self: &Self, new_self: &Self) -> bool { // Data does not change // TODO iterators: Using GhostSeq::equals here does not work + // new_self.model().data.equals(&old_self.model().data) && new_self.model().data.len() == old_self.model().data.len() && forall(|i: usize| (0 <= i && i < new_self.model().data.len()) ==> ( new_self.model().data.lookup(i) == old_self.model().data.lookup(i) @@ -152,27 +153,40 @@ fn verify_slice_iter(slice: &[i32]) { verify_visited(&iter, 1, 777); } -// TODO iterators: How to reason about visited values? -// #[requires(slice.len() == 4)] -// #[requires(slice[0] == 42)] -// #[requires(slice[1] == 777)] -// #[requires(slice[2] == 888)] -// #[requires(slice[3] == 13)] -// #[requires(seen.len() == 0)] -// fn verify_while(slice: &[i32]) { -// let mut iter = slice.iter(); -// let mut el = None; -// while { -// el = iter.next(); -// el.is_some() -// } { -// -// body_invariant!(iter.enumerated()); -// } -// assert!(iter.next().is_none()); -// verify_visited(&iter, 0, 42); -// } +#[trusted] +#[ensures(iter.model().position == result.model().position)] +#[ensures(iter.model().data.equals(&result.model().data))] +fn snap_iter<'a>(iter: &Iter<'a, i32>) -> Iter<'a, i32> { + unimplemented!() +} + +#[requires(slice.len() == 4)] +#[requires(slice[0] == 42)] +#[requires(slice[1] == 777)] +#[requires(slice[2] == 888)] +#[requires(slice[3] == 13)] +fn verify_while(slice: &[i32]) { + let mut iter = slice.iter(); + let mut el = None; + + let iter_snap = snap_iter(&iter); + while { + el = iter.next(); + el.is_some() + } { + body_invariant!(iter_snap.model().data.equals(&iter.model().data)); + body_invariant!(iter.enumerated()); + } + + assert!(iter.next().is_none()); + verify_visited(&iter, 0, 42); + verify_visited(&iter, 1, 777); + verify_visited(&iter, 2, 888); + verify_visited(&iter, 3, 13); +} + +#[trusted] fn main() { } From 5e396ffdcfd15065a6b3fc71fdeb6c56e3a5afd5 Mon Sep 17 00:00:00 2001 From: Jonas Hansen Date: Wed, 4 May 2022 21:32:04 +0200 Subject: [PATCH 24/38] Create custom Copy/Clone impls for type models (do not derive them) --- prusti-specs/src/type_model/mod.rs | 95 ++++++++++++++++++++---------- 1 file changed, 63 insertions(+), 32 deletions(-) diff --git a/prusti-specs/src/type_model/mod.rs b/prusti-specs/src/type_model/mod.rs index 4023de7c9e1..50eda05c10f 100644 --- a/prusti-specs/src/type_model/mod.rs +++ b/prusti-specs/src/type_model/mod.rs @@ -21,7 +21,7 @@ use crate::{ UserAnnotatedTypeParam, UserAnnotatedTypeParamParser, UserAnnotatedTypeParamParserError, }, }; -use proc_macro2::{Ident, TokenStream}; +use proc_macro2::{Ident, Span, TokenStream}; use quote::ToTokens; use syn::{parse_quote, spanned::Spanned}; use uuid::Uuid; @@ -46,15 +46,16 @@ fn rewrite_internal(item_struct: syn::ItemStruct) -> TypeModelGenerationResult - #[derive(Copy, Clone)] #[allow(non_camel_case_types)] struct #model_struct_ident {} }; // Attach lifetimes - for gp in item_struct.generics.params.iter() { - if let syn::GenericParam::Lifetime(lt) = gp { + for param in item_struct.generics.params.iter() { + if let syn::GenericParam::Lifetime(lt) = param { model_struct.generics.params.push(syn::GenericParam::Lifetime(lt.clone())); } } @@ -101,10 +101,32 @@ impl ModelStruct { let path = create_path(&model_struct); - Ok(Self { item: model_struct, path, }) + Ok(Self { input_span: item_struct.span(), item: model_struct, path, }) + } + + fn create_copy_impl(&self) -> syn::ItemImpl { + let path = &self.path; + let generics = self.item.generics.params.iter(); + parse_quote_spanned! {self.input_span=> + impl<#(#generics),*> Copy for #path {} + } + } + + fn create_clone_impl(&self) -> syn::ItemImpl { + let path = &self.path; + let generics = self.item.generics.params.iter(); + parse_quote_spanned! {self.input_span=> + impl<#(#generics),*> Clone for #path { + #[trusted] + fn clone(&self) -> Self { + unimplemented!() + } + } + } } } +#[derive(Clone)] struct ToModelTrait { item: syn::ItemTrait, @@ -234,11 +256,11 @@ impl std::convert::From for syn::Error { /// Type to represent generated code during expansion of the `#[model]` macro struct TypeModel { /// The struct which represents the model - model_struct: syn::ItemStruct, + model_struct: ModelStruct, /// A trait which will be implemented on the modelled type /// to return the [TypeModel::model_struct] - to_model_trait: syn::ItemTrait, + to_model_trait: ToModelTrait, /// The implementation of the [TypeModel::model_trait] on the modelled type. model_impl: syn::ItemImpl, @@ -246,8 +268,10 @@ struct TypeModel { impl ToTokens for TypeModel { fn to_tokens(&self, tokens: &mut TokenStream) { - self.to_model_trait.to_tokens(tokens); - self.model_struct.to_tokens(tokens); + self.to_model_trait.item.to_tokens(tokens); + self.model_struct.item.to_tokens(tokens); + self.model_struct.create_copy_impl().to_tokens(tokens); + self.model_struct.create_clone_impl().to_tokens(tokens); self.model_impl.to_tokens(tokens); } } @@ -274,12 +298,21 @@ mod tests { #[test] fn rewritten_model_to_tokens() { - let to_model_trait: syn::ItemTrait = parse_quote!( - trait PrustiFooToModel {} - ); - let model_struct: syn::ItemStruct = parse_quote!( - struct Foo {} - ); + let to_model_trait = ToModelTrait { + path: parse_quote!(PrustiFooToModel), + item: parse_quote!( + trait PrustiFooToModel {} + ) + }; + + let model_struct = ModelStruct { + path: parse_quote!(Foo), + item: parse_quote!( + struct Foo {} + ), + input_span: Span::call_site(), + }; + let trait_impl: syn::ItemImpl = parse_quote!(impl ToModel for Foo {}); let rewritten_model = TypeModel { @@ -290,8 +323,10 @@ mod tests { let actual_ts = rewritten_model.into_token_stream(); let mut expected_ts = TokenStream::new(); - to_model_trait.to_tokens(&mut expected_ts); - model_struct.to_tokens(&mut expected_ts); + to_model_trait.item.to_tokens(&mut expected_ts); + model_struct.item.to_tokens(&mut expected_ts); + model_struct.create_copy_impl().to_tokens(&mut expected_ts); + model_struct.create_clone_impl().to_tokens(&mut expected_ts); trait_impl.to_tokens(&mut expected_ts); assert_eq!(expected_ts.to_string(), actual_ts.to_string()); @@ -322,14 +357,13 @@ mod tests { let model_ident = check_model_ident(&model, "PrustiFooModel"); let expected: syn::ItemStruct = syn::parse_quote!( - #[derive(Copy, Clone)] #[allow(non_camel_case_types)] struct #model_ident { fld1: usize, fld2: i32, } ); - assert_eq_tokenizable(model.model_struct, expected); + assert_eq_tokenizable(model.model_struct.item, expected); } #[test] @@ -343,11 +377,10 @@ mod tests { let model_ident = check_model_ident(&model, "PrustiFooModel"); let expected: syn::ItemStruct = parse_quote!( - #[derive(Copy, Clone)] #[allow(non_camel_case_types)] struct #model_ident(i32, u32, usize); ); - assert_eq_tokenizable(model.model_struct, expected); + assert_eq_tokenizable(model.model_struct.item, expected); } #[test] @@ -384,7 +417,6 @@ mod tests { let trait_ident = check_trait_ident(&model, "PrustiFooToModel"); let expected_struct: syn::ItemStruct = parse_quote!( - #[derive(Copy, Clone)] #[allow(non_camel_case_types)] struct #model_ident<'a, 'b>( i32, @@ -405,7 +437,7 @@ mod tests { } ); - assert_eq_tokenizable(model.model_struct, expected_struct); + assert_eq_tokenizable(model.model_struct.item, expected_struct); assert_eq_tokenizable(model.model_impl, expected_impl); } @@ -420,7 +452,6 @@ mod tests { let trait_ident = check_trait_ident(&model, "PrustiFooi32TusizeUToModel"); let expected_struct: syn::ItemStruct = parse_quote!( - #[derive(Copy, Clone)] #[allow(non_camel_case_types)] struct #model_ident (i32,::core::marker::PhantomData , ::core::marker::PhantomData); ); @@ -446,8 +477,8 @@ mod tests { } ); - assert_eq_tokenizable(model.model_struct, expected_struct); - assert_eq_tokenizable(model.to_model_trait, expected_trait); + assert_eq_tokenizable(model.model_struct.item, expected_struct); + assert_eq_tokenizable(model.to_model_trait.item, expected_trait); assert_eq_tokenizable(model.model_impl, expected_impl); } @@ -462,7 +493,7 @@ mod tests { let model_ident = check_model_ident(&model, "PrustiFooModel"); let trait_ident = check_trait_ident(&model, "PrustiFooToModel"); - let actual = model.to_model_trait; + let actual = model.to_model_trait.item; let expected: syn::ItemTrait = parse_quote!( #[allow(non_camel_case_types)] trait #trait_ident { @@ -514,13 +545,13 @@ mod tests { } fn check_model_ident(model: &TypeModel, expected_prefix: &str) -> Ident { - let ident = &model.model_struct.ident; + let ident = &model.model_struct.item.ident; assert!(ident.to_string().starts_with(expected_prefix)); ident.clone() } fn check_trait_ident(model: &TypeModel, expected_prefix: &str) -> Ident { - let ident = &model.to_model_trait.ident; + let ident = &model.to_model_trait.item.ident; assert!(ident.to_string().starts_with(expected_prefix)); ident.clone() } From 3afba7cb4ed26cb57c5332b1695a3863a63d599d Mon Sep 17 00:00:00 2001 From: Jonas Hansen Date: Wed, 4 May 2022 21:39:31 +0200 Subject: [PATCH 25/38] Adjust flag docs for iterator killswitch --- docs/dev-guide/src/config/flags.md | 3 ++- prusti-common/src/config.rs | 3 ++- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/docs/dev-guide/src/config/flags.md b/docs/dev-guide/src/config/flags.md index 5cdcbe35689..f4abf1110ab 100644 --- a/docs/dev-guide/src/config/flags.md +++ b/docs/dev-guide/src/config/flags.md @@ -144,7 +144,8 @@ on a generic type parameter) is satisfied. ## `ENABLE_ITERATORS` -Enables support for iterators. +When enabled, calls to `Iterator::next` will be encoded in the Viper program. +Otherwise, an error is thrown during the encoding. **This is an experimental feature**, iterator support is still experimental. diff --git a/prusti-common/src/config.rs b/prusti-common/src/config.rs index 61abe686d86..67fa7966db5 100644 --- a/prusti-common/src/config.rs +++ b/prusti-common/src/config.rs @@ -602,7 +602,8 @@ pub fn enable_ghost_constraints() -> bool { read_setting("enable_ghost_constraints") } -/// Enables (experimental) iterator support +/// When enabled, calls to `Iterator::next` will be encoded in the Viper program. +/// Otherwise, an error is thrown during the encoding. pub fn enable_iterators() -> bool { read_setting("enable_iterators") } \ No newline at end of file From 70e5b0fbecd294cd0a0d049f12f20bd41a8d5cbd Mon Sep 17 00:00:00 2001 From: Jonas Hansen Date: Fri, 6 May 2022 14:13:03 +0200 Subject: [PATCH 26/38] Normalize substs in Environment::resolve_method_call to account for non-resolved associated types --- prusti-interface/src/environment/mod.rs | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/prusti-interface/src/environment/mod.rs b/prusti-interface/src/environment/mod.rs index eb44fd12dc7..1fa881654b5 100644 --- a/prusti-interface/src/environment/mod.rs +++ b/prusti-interface/src/environment/mod.rs @@ -486,6 +486,10 @@ impl<'tcx> Environment<'tcx> { } let param_env = self.tcx.param_env(caller_def_id); + + // `resolve_instance` below requires normalized substs. + let call_substs = self.tcx.normalize_erasing_regions(param_env, call_substs); + traits::resolve_instance(self.tcx, param_env.and((called_def_id, call_substs))) .map(|opt_instance| opt_instance .map(|instance| (instance.def_id(), instance.substs)) From ed1a7a5e871385bd61d0378b8321e890ca0522ba Mon Sep 17 00:00:00 2001 From: Jonas Hansen Date: Sun, 8 May 2022 16:48:23 +0200 Subject: [PATCH 27/38] Fix typo --- prusti-interface/src/environment/mod.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/prusti-interface/src/environment/mod.rs b/prusti-interface/src/environment/mod.rs index 1fa881654b5..1f1e19ed800 100644 --- a/prusti-interface/src/environment/mod.rs +++ b/prusti-interface/src/environment/mod.rs @@ -549,7 +549,7 @@ impl<'tcx> Environment<'tcx> { /// Normalizes associated types in foldable types, /// i.e. this resolves projection types ([ty::TyKind::Projection]s) - /// **Important:** Regions while be erased during this process + /// **Important:** Regions will be erased during this process pub fn resolve_assoc_types + std::fmt::Debug + Copy>(&self, normalizable: T, param_env: ty::ParamEnv<'tcx>) -> T { let norm_res = self.tcx.try_normalize_erasing_regions( param_env, From d1d49531a6108bce0dec2b81fe53ec653fc1255a Mon Sep 17 00:00:00 2001 From: Jonas Hansen Date: Mon, 9 May 2022 18:46:34 +0200 Subject: [PATCH 28/38] Support associated types in quantifiers --- prusti-interface/src/environment/mod.rs | 65 ++++++++++++++----- .../mir/pure/specifications/encoder_poly.rs | 15 ++++- .../encoder/mir/specifications/constraints.rs | 3 +- 3 files changed, 65 insertions(+), 18 deletions(-) diff --git a/prusti-interface/src/environment/mod.rs b/prusti-interface/src/environment/mod.rs index 1f1e19ed800..48d48d75fbb 100644 --- a/prusti-interface/src/environment/mod.rs +++ b/prusti-interface/src/environment/mod.rs @@ -290,7 +290,11 @@ impl<'tcx> Environment<'tcx> { body .monomorphised_bodies .entry(substs) - .or_insert_with(|| body.base_body.clone().subst(self.tcx, substs)) + .or_insert_with(|| { + let param_env = self.tcx.param_env(def_id); + let substituted = body.base_body.clone().subst(self.tcx, substs); + self.resolve_assoc_types(substituted.clone(), param_env) + }) .clone() } @@ -503,6 +507,7 @@ impl<'tcx> Environment<'tcx> { // Normalize the type to account for associated types let ty = self.resolve_assoc_types(ty, param_env); let ty = self.tcx.erase_late_bound_regions(ty); + let ty = self.tcx.erase_regions(ty); ty.is_copy_modulo_regions(self.tcx.at(rustc_span::DUMMY_SP), param_env) } @@ -549,23 +554,53 @@ impl<'tcx> Environment<'tcx> { /// Normalizes associated types in foldable types, /// i.e. this resolves projection types ([ty::TyKind::Projection]s) - /// **Important:** Regions will be erased during this process - pub fn resolve_assoc_types + std::fmt::Debug + Copy>(&self, normalizable: T, param_env: ty::ParamEnv<'tcx>) -> T { - let norm_res = self.tcx.try_normalize_erasing_regions( - param_env, - normalizable - ); + pub fn resolve_assoc_types + std::fmt::Debug>(&self, normalizable: T, param_env: ty::ParamEnv<'tcx>) -> T { + struct Normalizer<'a, 'tcx> { + tcx: &'a ty::TyCtxt<'tcx>, + param_env: ty::ParamEnv<'tcx>, + } + impl<'a, 'tcx> ty::fold::TypeFolder<'tcx> for Normalizer<'a, 'tcx> { + fn tcx(&self) -> ty::TyCtxt<'tcx> { + *self.tcx + } - match norm_res { - Ok(normalized) => { - debug!("Normalized {:?}: {:?}", normalizable, normalized); - normalized - }, - Err(err) => { - debug!("Error while resolving associated types for {:?}: {:?}", normalizable, err); - normalizable + fn fold_mir_const(&mut self, c: mir::ConstantKind<'tcx>) -> mir::ConstantKind<'tcx> { + // rustc by default panics when we execute this TypeFolder on a mir::* type, + // but we want to resolve associated types when we retrieve a local mir::Body + c + } + + fn fold_ty(&mut self, ty: ty::Ty<'tcx>) -> ty::Ty<'tcx> { + match ty.kind() { + ty::TyKind::Projection(_) => { + let normalized = self.tcx.infer_ctxt().enter(|infcx| { + use rustc_trait_selection::traits::{fully_normalize, ObligationCause, FulfillmentContext}; + + let normalization_result = fully_normalize( + &infcx, + FulfillmentContext::new(), + ObligationCause::dummy(), + self.param_env, + ty + ); + + match normalization_result { + Ok(res) => res, + Err(errors) => { + debug!("Error while resolving associated types: {:?}", errors); + ty + } + } + }); + normalized.super_fold_with(self) + } + _ => ty.super_fold_with(self) + } } } + + use crate::rustc_middle::ty::TypeFoldable; + normalizable.fold_with(&mut Normalizer {tcx: &self.tcx, param_env}) } fn any_type_needs_infer>(&self, t: T) -> bool { diff --git a/prusti-viper/src/encoder/mir/pure/specifications/encoder_poly.rs b/prusti-viper/src/encoder/mir/pure/specifications/encoder_poly.rs index 15b31a2d236..d78be1b4644 100644 --- a/prusti-viper/src/encoder/mir/pure/specifications/encoder_poly.rs +++ b/prusti-viper/src/encoder/mir/pure/specifications/encoder_poly.rs @@ -44,7 +44,7 @@ pub(super) fn inline_closure<'tcx>( let local_ty = mir.local_decls[arg_local].ty; body_replacements.push(( encoder - .encode_value_expr(vir_crate::polymorphic::Expr::local(local), local_ty) + .encode_value_expr(vir_crate::polymorphic::Expr::local(local.clone()), local_ty) .with_span(local_span)?, if arg_idx == 0 { cl_expr.clone() @@ -52,6 +52,15 @@ pub(super) fn inline_closure<'tcx>( vir_crate::polymorphic::Expr::local(args[arg_idx - 1].clone()) }, )); + + body_replacements.push(( + vir_crate::polymorphic::Expr::local(local), + if arg_idx == 0 { + cl_expr.clone() + } else { + vir_crate::polymorphic::Expr::local(args[arg_idx - 1].clone()) + }, + )); } Ok(encoder .encode_pure_expression(def_id, parent_def_id, substs)? @@ -111,6 +120,7 @@ pub(super) fn encode_quantifier<'tcx>( substs: ty::subst::SubstsRef<'tcx>, ) -> SpannedEncodingResult { let tcx = encoder.env().tcx(); + let param_env = encoder.env().tcx().param_env(parent_def_id); // Quantifiers are encoded as: // forall( @@ -123,13 +133,14 @@ pub(super) fn encode_quantifier<'tcx>( // ), // |qvars...| -> bool { }, // ) - let cl_type_body = substs.type_at(1); let (body_def_id, body_substs, body_span, args, _) = extract_closure_from_ty(tcx, cl_type_body); let mut encoded_qvars = vec![]; let mut bounds = vec![]; for (arg_idx, arg_ty) in args.into_iter().enumerate() { + let arg_ty = encoder.env().resolve_assoc_types(arg_ty, param_env); + let qvar_ty = encoder.encode_snapshot_type(arg_ty).with_span(body_span)?; let qvar_name = format!( "_{}_quant_{}", diff --git a/prusti-viper/src/encoder/mir/specifications/constraints.rs b/prusti-viper/src/encoder/mir/specifications/constraints.rs index e3f646390fb..535fe619f00 100644 --- a/prusti-viper/src/encoder/mir/specifications/constraints.rs +++ b/prusti-viper/src/encoder/mir/specifications/constraints.rs @@ -207,9 +207,10 @@ pub mod trait_bounds { // associated types, e.g. `T: A::OtherAssocType` // where `::OtherAssocType` can be normalized to some concrete type. let param_env = env.resolve_assoc_types(param_env, param_env_lookup); + let param_env = env.tcx().erase_regions(param_env); trace!( - "Constraints after resolving associated types: {:#?}", + "Constrai nts after resolving associated types and erasing regions: {:#?}", param_env ); From 7e7bde4689b1011909e1f08915043a089de093b9 Mon Sep 17 00:00:00 2001 From: Jonas Hansen Date: Mon, 9 May 2022 18:49:46 +0200 Subject: [PATCH 29/38] Remove dead comment in any_type_needs_infer --- prusti-interface/src/environment/mod.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/prusti-interface/src/environment/mod.rs b/prusti-interface/src/environment/mod.rs index 48d48d75fbb..e80b9bc9d44 100644 --- a/prusti-interface/src/environment/mod.rs +++ b/prusti-interface/src/environment/mod.rs @@ -607,7 +607,7 @@ impl<'tcx> Environment<'tcx> { // Helper fn is_nested_ty(ty: ty::Ty<'_>) -> bool { let mut walker = ty.walk(); - let first = walker.next().unwrap().expect_ty(); // This is known to yield t + let first = walker.next().unwrap().expect_ty(); assert!(ty == first); walker.next().is_some() } From e3bbbd9eb663dad2230ecd73085abbaaae876c9b Mon Sep 17 00:00:00 2001 From: Jonas Hansen Date: Wed, 11 May 2022 14:04:04 +0200 Subject: [PATCH 30/38] Remove dead code --- prusti-interface/src/specs/typed.rs | 80 ----------------------------- 1 file changed, 80 deletions(-) diff --git a/prusti-interface/src/specs/typed.rs b/prusti-interface/src/specs/typed.rs index fb293080f65..fa9b7c1801a 100644 --- a/prusti-interface/src/specs/typed.rs +++ b/prusti-interface/src/specs/typed.rs @@ -400,22 +400,6 @@ pub enum ProcedureSpecificationKindError { } impl SpecificationItem { - pub fn is_pure(&self) -> Result { - self.validate()?; - - Ok(matches!(self.extract_with_selective_replacement(), - Some(ProcedureSpecificationKind::Pure) | Some(ProcedureSpecificationKind::Predicate(_)))) - } - - pub fn is_impure(&self) -> Result { - self.validate()?; - - Ok(match self.extract_with_selective_replacement() { - Some(refined) => matches!(refined, ProcedureSpecificationKind::Impure), - _ => true, - }) - } - pub fn get_predicate_body(&self) -> Result, ProcedureSpecificationKindError> { self.validate()?; @@ -722,69 +706,5 @@ mod tests { assert!(matches!(result, ProcedureSpecificationKindError::InvalidSpecKindRefinement(_, _))); } } - - mod is_impure { - use super::*; - - macro_rules! impure_checks { - ($($name:ident: $value:expr,)*) => { - $( - #[test] - fn $name() { - let (item, expected) = $value; - let item: SpecificationItem = item; - let result = item.is_impure().expect("Expected impure"); - assert_eq!(result, expected); - } - )* - } - } - - impure_checks!( - empty: (Empty, true), - inherent_impure: (Inherent(Impure), true), - inherent_pure: (Inherent(Pure), false), - inherent_predicate: (Inherent(Predicate(None)), false), - inherited_impure: (Inherited(Impure), true), - inherited_pure: (Inherited(Pure), false), - inherited_predicate: (Inherited(Predicate(None)), false), - refined_impure_parent_impure_child: (Refined(Impure, Impure), true), - refined_impure_parent_pure_child: (Refined(Impure, Pure), false), - refined_pure_parent_with_pure_child: (Refined(Pure, Pure), false), - refined_predicate_parent_with_predicate_child: (Refined(Predicate(None), Predicate(None)), false), - ); - } - - mod is_pure { - use super::*; - - macro_rules! pure_checks { - ($($name:ident: $value:expr,)*) => { - $( - #[test] - fn $name() { - let (item, expected) = $value; - let item: SpecificationItem = item; - let result = item.is_pure().expect("Expected pure"); - assert_eq!(result, expected); - } - )* - } - } - - pure_checks!( - empty: (Empty, false), - inherent_impure: (Inherent(Impure), false), - inherent_pure: (Inherent(Pure), true), - inherent_predicate: (Inherent(Predicate(None)), true), - inherited_impure: (Inherited(Impure), false), - inherited_pure: (Inherited(Pure), true), - inherited_predicate: (Inherited(Predicate(None)), true), - refined_impure_parent_impure_child: (Refined(Impure, Impure), false), - refined_impure_parent_pure_child: (Refined(Impure, Pure), true), - refined_pure_parent_with_pure: (Refined(Pure, Pure), true), - refined_predicate_parent_with_predicate_child: (Refined(Predicate(None), Predicate(None)), true), - ); - } } } From f16f646ced91a5eeca86bc90edadcaec70bb2d51 Mon Sep 17 00:00:00 2001 From: Pointerbender Date: Tue, 7 Jun 2022 16:57:38 +0200 Subject: [PATCH 31/38] fix for #1033 with test cases --- .../tests/verify/fail/issues/issue-1033-2.rs | 13 +++++++++++++ .../tests/verify/fail/issues/issue-1033-3.rs | 17 +++++++++++++++++ .../tests/verify/pass/issues/issue-1033-1.rs | 13 +++++++++++++ prusti-viper/src/encoder/snapshot/decls.rs | 2 +- 4 files changed, 44 insertions(+), 1 deletion(-) create mode 100644 prusti-tests/tests/verify/fail/issues/issue-1033-2.rs create mode 100644 prusti-tests/tests/verify/fail/issues/issue-1033-3.rs create mode 100644 prusti-tests/tests/verify/pass/issues/issue-1033-1.rs diff --git a/prusti-tests/tests/verify/fail/issues/issue-1033-2.rs b/prusti-tests/tests/verify/fail/issues/issue-1033-2.rs new file mode 100644 index 00000000000..d3ed07bad60 --- /dev/null +++ b/prusti-tests/tests/verify/fail/issues/issue-1033-2.rs @@ -0,0 +1,13 @@ +use prusti_contracts::*; + +fn main() {} + +pub struct Foo(T); + +impl Foo { + #[pure] + #[ensures(result == (left == right))] + fn eq(left: T, right: T) -> bool { //~ ERROR pure function parameters must be Copy + left == right + } +} diff --git a/prusti-tests/tests/verify/fail/issues/issue-1033-3.rs b/prusti-tests/tests/verify/fail/issues/issue-1033-3.rs new file mode 100644 index 00000000000..27056c3351b --- /dev/null +++ b/prusti-tests/tests/verify/fail/issues/issue-1033-3.rs @@ -0,0 +1,17 @@ +use prusti_contracts::*; + +fn main() {} + +pub struct Foo(T); + +impl Foo { + #[ensures(result == (left == right))] + fn eq(left: T, right: T) -> bool { + left == right + } +} + +#[pure] +pub fn test() { + assert!(Foo::eq(0, 0)); //~ ERROR use of impure function +} diff --git a/prusti-tests/tests/verify/pass/issues/issue-1033-1.rs b/prusti-tests/tests/verify/pass/issues/issue-1033-1.rs new file mode 100644 index 00000000000..7bb647bb374 --- /dev/null +++ b/prusti-tests/tests/verify/pass/issues/issue-1033-1.rs @@ -0,0 +1,13 @@ +use prusti_contracts::*; + +fn main() {} + +pub struct Foo(T); + +impl Foo { + #[pure] + #[ensures(result == (left == right))] + fn eq(left: T, right: T) -> bool { + left == right + } +} diff --git a/prusti-viper/src/encoder/snapshot/decls.rs b/prusti-viper/src/encoder/snapshot/decls.rs index c84117419a7..84951e04222 100644 --- a/prusti-viper/src/encoder/snapshot/decls.rs +++ b/prusti-viper/src/encoder/snapshot/decls.rs @@ -93,7 +93,7 @@ impl Snapshot { use Snapshot::*; matches!( self, - Primitive(_) | Complex { .. } | Array { .. } | Slice { .. } + Primitive(_) | Complex { .. } | Array { .. } | Slice { .. } | Abstract { .. } ) } } From 96ee8b9d4425111365125b3b110de7aad40b3d5c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Aurel=20B=C3=ADl=C3=BD?= Date: Tue, 12 Jul 2022 16:08:30 +0200 Subject: [PATCH 32/38] snapshot equality --- prusti-contracts/src/lib.rs | 8 ++++++++ prusti-specs/src/specifications/preparser.rs | 2 +- .../src/encoder/mir/pure/pure_functions/interpreter.rs | 7 ++++--- .../src/encoder/mir/pure/specifications/interface.rs | 9 +++++++++ 4 files changed, 22 insertions(+), 4 deletions(-) diff --git a/prusti-contracts/src/lib.rs b/prusti-contracts/src/lib.rs index 80dc037e9b7..9566c42306e 100644 --- a/prusti-contracts/src/lib.rs +++ b/prusti-contracts/src/lib.rs @@ -223,4 +223,12 @@ pub fn exists(_trigger_set: T, _closure: F) -> bool { true } +pub fn snap(_x: &T) -> T { + unimplemented!() +} + +pub fn snapshot_equality(_l: T, _r: T) -> bool { + true +} + pub use private::*; diff --git a/prusti-specs/src/specifications/preparser.rs b/prusti-specs/src/specifications/preparser.rs index 93186a404c5..d93aa3e133c 100644 --- a/prusti-specs/src/specifications/preparser.rs +++ b/prusti-specs/src/specifications/preparser.rs @@ -802,7 +802,7 @@ impl PrustiBinaryOp { } Self::Or => quote_spanned! { span => #lhs || #rhs }, Self::And => quote_spanned! { span => #lhs && #rhs }, - Self::SnapEq => quote_spanned! { span => snapshot_equality(#lhs, #rhs) }, + Self::SnapEq => quote_spanned! { span => snapshot_equality(&#lhs, &#rhs) }, } } } diff --git a/prusti-viper/src/encoder/mir/pure/pure_functions/interpreter.rs b/prusti-viper/src/encoder/mir/pure/pure_functions/interpreter.rs index 52764c61359..a9bb2ac1624 100644 --- a/prusti-viper/src/encoder/mir/pure/pure_functions/interpreter.rs +++ b/prusti-viper/src/encoder/mir/pure/pure_functions/interpreter.rs @@ -563,11 +563,12 @@ impl<'p, 'v: 'p, 'tcx: 'v> BackwardMirInterpreter<'tcx> // Prusti-specific syntax // TODO: check we are in a spec function - "prusti_contracts::implication" - | "prusti_contracts::exists" + "prusti_contracts::exists" | "prusti_contracts::forall" | "prusti_contracts::specification_entailment" - | "prusti_contracts::call_description" => { + | "prusti_contracts::call_description" + | "prusti_contracts::snap" + | "prusti_contracts::snapshot_equality" => { let expr = self.encoder.encode_prusti_operation( full_func_proc_name, span, diff --git a/prusti-viper/src/encoder/mir/pure/specifications/interface.rs b/prusti-viper/src/encoder/mir/pure/specifications/interface.rs index 83ae6e11e35..11d0b19979b 100644 --- a/prusti-viper/src/encoder/mir/pure/specifications/interface.rs +++ b/prusti-viper/src/encoder/mir/pure/specifications/interface.rs @@ -244,6 +244,15 @@ impl<'v, 'tcx: 'v> SpecificationEncoderInterface<'tcx> for crate::encoder::Encod parent_def_id, substs, ), + "prusti_contracts::snap" => Ok( + vir_poly::Expr::snap_app(encoded_args[0].clone()), + ), + "prusti_contracts::snapshot_equality" => Ok( + vir_poly::Expr::eq_cmp( + vir_poly::Expr::snap_app(encoded_args[0].clone()), + vir_poly::Expr::snap_app(encoded_args[1].clone()), + ), + ), _ => unimplemented!(), } } From 414e0812053d4a9e8cccd786e69114a2baf482c8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Aurel=20B=C3=ADl=C3=BD?= Date: Mon, 18 Jul 2022 18:28:12 +0200 Subject: [PATCH 33/38] remove special Fn*::call* treatment --- prusti-viper/src/encoder/procedure_encoder.rs | 82 +++---------------- 1 file changed, 10 insertions(+), 72 deletions(-) diff --git a/prusti-viper/src/encoder/procedure_encoder.rs b/prusti-viper/src/encoder/procedure_encoder.rs index 537f979a648..22da3c27091 100644 --- a/prusti-viper/src/encoder/procedure_encoder.rs +++ b/prusti-viper/src/encoder/procedure_encoder.rs @@ -2279,7 +2279,6 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { .. } => { let ty = literal.ty(); - let func_const_val = literal.try_to_value(); if let ty::TyKind::FnDef(called_def_id, call_substs) = ty.kind() { let called_def_id = *called_def_id; debug!("Encode function call {:?} with substs {:?}", called_def_id, call_substs); @@ -2401,31 +2400,6 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { ); } - "std::ops::Fn::call" - | "core::ops::Fn::call" => { - let cl_type: ty::Ty = call_substs[0].expect_ty(); - match cl_type.kind() { - ty::TyKind::Closure(cl_def_id, _) => { - debug!("Encoding call to closure {:?} with func {:?}", cl_def_id, func_const_val); - stmts.extend(self.encode_impure_function_call( - location, - term.source_info.span, - args, - destination, - *cl_def_id, - call_substs, - )?); - } - - _ => { - return Err(SpannedEncodingError::unsupported( - format!("only calls to closures are supported. The term is a {:?}, not a closure.", cl_type.kind()), - term.source_info.span, - )); - } - } - } - "core::slice::::len" => { debug!("Encoding call of slice::len"); stmts.extend( @@ -2986,58 +2960,22 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { // .absolute_item_path_str(called_def_id); debug!("Encoding non-pure function call '{}' with args {:?} and substs {:?}", full_func_proc_name, mir_args, substs); - // First we construct the "operands" vector. This construction differs - // for closure calls, where we need to unpack a tuple into the actual - // call arguments. The components of the operands tuples are: + // First we construct the "operands" vector. The components of the + // operands tuples are: // - the original MIR Operand // - the VIR Local that will hold hold the argument before the call // - the type of the argument // - if not constant, the VIR expression for the argument - let mut operands: Vec<(&mir::Operand<'tcx>, Local, ty::Ty<'tcx>, Option)> = vec![]; let mut encoded_operands = mir_args.iter() .map(|arg| self.mir_encoder.encode_operand_place(arg)) .collect::>, _>>() .with_span(call_site_span)?; - if self.encoder.env().tcx().is_closure(called_def_id) { - // Closure calls are wrapped around std::ops::Fn::call(), which receives - // two arguments: The closure instance, and the tupled-up arguments - assert_eq!(mir_args.len(), 2); - - let cl_ty = self.mir_encoder.get_operand_ty(&mir_args[0]); - operands.push(( - &mir_args[0], - mir_args[0].place() - .and_then(|place| place.as_local()) - .map_or_else( - || self.locals.get_fresh(cl_ty), - |local| local.into() - ), - cl_ty, - encoded_operands[0].take(), - )); - - let arg_tuple_ty = self.mir_encoder.get_operand_ty(&mir_args[1]); - if let ty::TyKind::Tuple(arg_types) = arg_tuple_ty.kind() { - for (field_num, arg_ty) in arg_types.into_iter().enumerate() { - let arg = self.locals.get_fresh(arg_ty); - let value_field = self - .encoder - .encode_raw_ref_field(format!("tuple_{}", field_num), arg_ty) - .with_span(call_site_span)?; - operands.push(( - &mir_args[1], // not actually used ... - arg, - arg_ty, - Some(encoded_operands[1].take().unwrap().field(value_field)), - )); - } - } else { - unimplemented!(); - } - } else { - for (arg, encoded_operand) in mir_args.iter().zip(encoded_operands.iter_mut()) { + let operands: Vec<(&mir::Operand<'tcx>, Local, ty::Ty<'tcx>, Option)> = mir_args + .iter() + .zip(encoded_operands.iter_mut()) + .map(|(arg, encoded_operand)| { let arg_ty = self.mir_encoder.get_operand_ty(arg); - operands.push(( + ( arg, arg.place() .and_then(|place| place.as_local()) @@ -3047,9 +2985,9 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { ), arg_ty, encoded_operand.take(), - )); - } - }; + ) + }) + .collect(); // Arguments can be places or constants. For constants, we pretend they're places by // creating a new local variable of the same type. For arguments that are not just local From 2b6d632c00ea1681963d2e6cea66463b35fb378d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Aurel=20B=C3=ADl=C3=BD?= Date: Mon, 18 Jul 2022 18:39:37 +0200 Subject: [PATCH 34/38] test closures using type-dependent contracts --- .../verify/fail/closures/using-type-dep.rs | 65 ++++++++++++++++++ .../verify/pass/closures/using-type-dep.rs | 66 +++++++++++++++++++ 2 files changed, 131 insertions(+) create mode 100644 prusti-tests/tests/verify/fail/closures/using-type-dep.rs create mode 100644 prusti-tests/tests/verify/pass/closures/using-type-dep.rs diff --git a/prusti-tests/tests/verify/fail/closures/using-type-dep.rs b/prusti-tests/tests/verify/fail/closures/using-type-dep.rs new file mode 100644 index 00000000000..769b411aeca --- /dev/null +++ b/prusti-tests/tests/verify/fail/closures/using-type-dep.rs @@ -0,0 +1,65 @@ +// compiler-flags: -Penable_ghost_constraints=true + +#![feature(unboxed_closures, fn_traits)] + +use prusti_contracts::*; + +pub trait ClosureSpecExt : FnMut { + predicate! { fn call_pre(&self, args: &A) -> bool; } + predicate! { fn call_post(prev: &Self, curr: &Self, args: &A, res: &Self::Output) -> bool; } + predicate! { fn hist_inv(prev: &Self, curr: &Self) -> bool; } +} + +#[extern_spec] +trait FnMut<#[generic] A> { + #[ghost_constraint(Self: ClosureSpecExt , [ + requires(>::hist_inv(&self, &self)), + requires(>::call_pre(&self, &args)), + ensures(>::hist_inv(old(&self), &self)), + ensures(>::call_post(old(&self), &self, &args, &result)), + ])] + fn call_mut(&mut self, args: A) -> >::Output; +} + +// encoding of: +// #[requires(x >= 5)] +// #[ensures(result == x + val)] +// #[ensures(val == old(val) + 1)] +// #[invariant(val >= old(val))] +// |x: i32| { val += 1; x + val } + +struct MyClosure { + val: i32, +} + +impl FnOnce<(i32,)> for MyClosure { + type Output = i32; + extern "rust-call" fn call_once(mut self, args: (i32,)) -> i32 { + self.val += 1; + args.0 + self.val + } +} +impl FnMut<(i32,)> for MyClosure { + extern "rust-call" fn call_mut(&mut self, args: (i32,)) -> i32 { + self.val += 1; + args.0 + self.val + } +} +#[refine_trait_spec] +impl ClosureSpecExt<(i32,)> for MyClosure { + predicate! { fn call_pre(&self, args: &(i32,)) -> bool { + args.0 >= 5 + } } + predicate! { fn call_post(prev: &Self, curr: &Self, args: &(i32,), res: &i32) -> bool { + *res == args.0 + curr.val + && curr.val == prev.val + 1 + } } + predicate! { fn hist_inv(prev: &Self, curr: &Self) -> bool { + curr.val >= prev.val + } } +} + +fn main() { + let mut cl = MyClosure { val: 3 }; + cl(3); //~ ERROR precondition might not hold +} diff --git a/prusti-tests/tests/verify/pass/closures/using-type-dep.rs b/prusti-tests/tests/verify/pass/closures/using-type-dep.rs new file mode 100644 index 00000000000..b58e6a72519 --- /dev/null +++ b/prusti-tests/tests/verify/pass/closures/using-type-dep.rs @@ -0,0 +1,66 @@ +// compiler-flags: -Penable_ghost_constraints=true + +#![feature(unboxed_closures, fn_traits)] + +use prusti_contracts::*; + +pub trait ClosureSpecExt : FnMut { + predicate! { fn call_pre(&self, args: &A) -> bool; } + predicate! { fn call_post(prev: &Self, curr: &Self, args: &A, res: &Self::Output) -> bool; } + predicate! { fn hist_inv(prev: &Self, curr: &Self) -> bool; } +} + +#[extern_spec] +trait FnMut<#[generic] A> { + #[ghost_constraint(Self: ClosureSpecExt , [ + requires(>::hist_inv(&self, &self)), + requires(>::call_pre(&self, &args)), + ensures(>::hist_inv(old(&self), &self)), + ensures(>::call_post(old(&self), &self, &args, &result)), + ])] + fn call_mut(&mut self, args: A) -> >::Output; +} + +// encoding of: +// #[requires(x >= 5)] +// #[ensures(result == x + val)] +// #[ensures(val == old(val) + 1)] +// #[invariant(val >= old(val))] +// |x: i32| { val += 1; x + val } + +struct MyClosure { + val: i32, +} + +impl FnOnce<(i32,)> for MyClosure { + type Output = i32; + extern "rust-call" fn call_once(mut self, args: (i32,)) -> i32 { + self.val += 1; + args.0 + self.val + } +} +impl FnMut<(i32,)> for MyClosure { + extern "rust-call" fn call_mut(&mut self, args: (i32,)) -> i32 { + self.val += 1; + args.0 + self.val + } +} +#[refine_trait_spec] +impl ClosureSpecExt<(i32,)> for MyClosure { + predicate! { fn call_pre(&self, args: &(i32,)) -> bool { + args.0 >= 5 + } } + predicate! { fn call_post(prev: &Self, curr: &Self, args: &(i32,), res: &i32) -> bool { + *res == args.0 + curr.val + && curr.val == prev.val + 1 + } } + predicate! { fn hist_inv(prev: &Self, curr: &Self) -> bool { + curr.val >= prev.val + } } +} + +fn main() { + let mut cl = MyClosure { val: 3 }; + assert!(cl(6) == 10); + assert!(cl(6) == 11); +} From 186e97e888cf581373b25e2cc4d9d8dd5ae07b95 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Aurel=20B=C3=ADl=C3=BD?= Date: Tue, 19 Jul 2022 16:47:54 +0200 Subject: [PATCH 35/38] fix --- prusti-specs/src/specifications/preparser.rs | 2 +- prusti-tests/tests/verify/fail/closures/using-type-dep.rs | 2 +- prusti-tests/tests/verify/fail/unsupported/non_closure_call.rs | 3 +++ prusti-tests/tests/verify/pass/closures/using-type-dep.rs | 2 +- 4 files changed, 6 insertions(+), 3 deletions(-) diff --git a/prusti-specs/src/specifications/preparser.rs b/prusti-specs/src/specifications/preparser.rs index d93aa3e133c..39ce91ddfe7 100644 --- a/prusti-specs/src/specifications/preparser.rs +++ b/prusti-specs/src/specifications/preparser.rs @@ -899,7 +899,7 @@ mod tests { ); assert_eq!( parse_prusti(quote! { exists(|x: i32| a === b) }).unwrap().to_string(), - "exists (() , # [prusti :: spec_only] | x : i32 | -> bool { ((snapshot_equality (a , b)) : bool) })", + "exists (() , # [prusti :: spec_only] | x : i32 | -> bool { ((snapshot_equality (& a , & b)) : bool) })", ); assert_eq!( parse_prusti(quote! { forall(|x: i32| a ==> b, triggers = [(c,), (d, e)]) }).unwrap().to_string(), diff --git a/prusti-tests/tests/verify/fail/closures/using-type-dep.rs b/prusti-tests/tests/verify/fail/closures/using-type-dep.rs index 769b411aeca..fe526f7027b 100644 --- a/prusti-tests/tests/verify/fail/closures/using-type-dep.rs +++ b/prusti-tests/tests/verify/fail/closures/using-type-dep.rs @@ -1,4 +1,4 @@ -// compiler-flags: -Penable_ghost_constraints=true +// compile-flags: -Penable_ghost_constraints=true #![feature(unboxed_closures, fn_traits)] diff --git a/prusti-tests/tests/verify/fail/unsupported/non_closure_call.rs b/prusti-tests/tests/verify/fail/unsupported/non_closure_call.rs index 6830f318cf3..f79ea4f8f0b 100644 --- a/prusti-tests/tests/verify/fail/unsupported/non_closure_call.rs +++ b/prusti-tests/tests/verify/fail/unsupported/non_closure_call.rs @@ -1,3 +1,6 @@ +// ignore-test The function arguments (desugared to a 1-tuple of reference +// here) are probably the issue; then this is similar to #1077 ? + pub fn max_by_key(a: A, b: A, key: impl Fn(&A) -> B) -> A { if key(&a) > key(&b) { //~ Error: only calls to closures are supported a diff --git a/prusti-tests/tests/verify/pass/closures/using-type-dep.rs b/prusti-tests/tests/verify/pass/closures/using-type-dep.rs index b58e6a72519..37096357de2 100644 --- a/prusti-tests/tests/verify/pass/closures/using-type-dep.rs +++ b/prusti-tests/tests/verify/pass/closures/using-type-dep.rs @@ -1,4 +1,4 @@ -// compiler-flags: -Penable_ghost_constraints=true +// compile-flags: -Penable_ghost_constraints=true #![feature(unboxed_closures, fn_traits)] From dbd4d2dc58520162058acce787cb1d8ee5c36208 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Aurel=20B=C3=ADl=C3=BD?= Date: Fri, 22 Jul 2022 12:47:54 +0200 Subject: [PATCH 36/38] erase regions less eagerly for method calls --- prusti-interface/src/environment/mod.rs | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/prusti-interface/src/environment/mod.rs b/prusti-interface/src/environment/mod.rs index 7631b6c98f8..1f59cf692d5 100644 --- a/prusti-interface/src/environment/mod.rs +++ b/prusti-interface/src/environment/mod.rs @@ -510,10 +510,15 @@ impl<'tcx> Environment<'tcx> { let param_env = self.tcx.param_env(caller_def_id); // `resolve_instance` below requires normalized substs. - let call_substs = self.tcx.normalize_erasing_regions(param_env, call_substs); + let normalized_call_substs = self.tcx.normalize_erasing_regions(param_env, call_substs); - traits::resolve_instance(self.tcx, param_env.and((called_def_id, call_substs))) + traits::resolve_instance(self.tcx, param_env.and((called_def_id, normalized_call_substs))) .map(|opt_instance| opt_instance + // if the resolved instance is the same as what we queried for + // anyway, ignore it: this way we keep the regions in substs + // at least for non-trait-impl method calls + // TODO: different behaviour used for unsafe core proof + .filter(|instance| !config::unsafe_core_proof() || instance.def_id() != called_def_id) .map(|instance| (instance.def_id(), instance.substs)) .unwrap_or((called_def_id, call_substs))) .unwrap_or((called_def_id, call_substs)) From c74215b5c6e2db68f1d8687c68183ced6de3a316 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Aurel=20B=C3=ADl=C3=BD?= Date: Wed, 27 Jul 2022 13:26:41 +0200 Subject: [PATCH 37/38] fix --- prusti-specs/src/specifications/preparser.rs | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/prusti-specs/src/specifications/preparser.rs b/prusti-specs/src/specifications/preparser.rs index 7938914f99d..47950059d18 100644 --- a/prusti-specs/src/specifications/preparser.rs +++ b/prusti-specs/src/specifications/preparser.rs @@ -900,10 +900,9 @@ mod tests { parse_prusti("forall(|x: i32| a ==> b, triggers = [(c,), (d, e)])".parse().unwrap()).unwrap().to_string(), "forall (((# [prusti :: spec_only] | x : i32 | (c) ,) , (# [prusti :: spec_only] | x : i32 | (d) , # [prusti :: spec_only] | x : i32 | (e) ,) ,) , # [prusti :: spec_only] | x : i32 | -> bool { (((! (a) || (b))) : bool) })", ); - let expr: syn::Expr = syn::parse2("assert!(a === b ==> b)".parse().unwrap()).unwrap(); assert_eq!( - parse_prusti(quote! { #expr }).unwrap().to_string(), - "assert ! ((! (snapshot_equality (a , b)) || (b)))", + parse_prusti("assert!(a === b ==> b)".parse().unwrap()).unwrap().to_string(), + "assert ! ((! (snapshot_equality (& a , & b)) || (b)))", ); } From fa449f9798d4abacdc27e0eb79b8d42536ef6524 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Aurel=20B=C3=ADl=C3=BD?= Date: Fri, 29 Jul 2022 16:37:49 +0200 Subject: [PATCH 38/38] another unsafe core proof workaround for trait resolution --- prusti-interface/src/environment/mod.rs | 10 +++++++++- viper/src/silicon_counterexample.rs | 5 +++-- 2 files changed, 12 insertions(+), 3 deletions(-) diff --git a/prusti-interface/src/environment/mod.rs b/prusti-interface/src/environment/mod.rs index a969499ee32..a3e08d9c6cd 100644 --- a/prusti-interface/src/environment/mod.rs +++ b/prusti-interface/src/environment/mod.rs @@ -523,10 +523,18 @@ impl<'tcx> Environment<'tcx> { called_def_id: ProcedureDefId, // what are we calling? call_substs: SubstsRef<'tcx>, ) -> (ProcedureDefId, SubstsRef<'tcx>) { + use prusti_rustc_interface::middle::ty::TypeVisitable; + // Avoids a compiler-internal panic // this check ignores any lifetimes/regions, which at this point would // need inference. They are thus ignored. - if self.any_type_needs_infer(call_substs) { + // TODO: different behaviour used for unsafe core proof + let needs_infer = if config::unsafe_core_proof() { + call_substs.needs_infer() + } else { + self.any_type_needs_infer(call_substs) + }; + if needs_infer { return (called_def_id, call_substs); } diff --git a/viper/src/silicon_counterexample.rs b/viper/src/silicon_counterexample.rs index e1423356a98..3c9966ccb94 100644 --- a/viper/src/silicon_counterexample.rs +++ b/viper/src/silicon_counterexample.rs @@ -222,8 +222,9 @@ fn unwrap_model_entry<'a>( } "viper.silicon.reporting.LitPermEntry" => { let lit_perm_wrapper = silicon::reporting::LitPermEntry::with(env); - let value = jni.unwrap_result(lit_perm_wrapper.call_value(entry)); - Some(ModelEntry::LitPerm(value.to_string())) + let value_scala = jni.unwrap_result(lit_perm_wrapper.call_value(entry)); + let value = jni.to_string(value_scala); + Some(ModelEntry::LitPerm(value)) } "viper.silicon.reporting.RefEntry" => { let ref_wrapper = silicon::reporting::RefEntry::with(env);