diff --git a/docs/dev-guide/src/config/flags.md b/docs/dev-guide/src/config/flags.md index 3ef1c1686c3..0399aed280c 100644 --- a/docs/dev-guide/src/config/flags.md +++ b/docs/dev-guide/src/config/flags.md @@ -23,6 +23,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_TYPE_INVARIANTS`](#enable_type_invariants) | `bool` | `false` | | [`ENABLE_VERIFY_ONLY_BASIC_BLOCK_PATH`](#enable_verify_only_basic_block_path) | `bool` | `false` | @@ -174,6 +175,13 @@ on a generic type parameter) is satisfied. **This is an experimental feature**, because it is currently possible to introduce unsound verification behavior. +## `ENABLE_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. + ## `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 0f397433fb1..490010919f0 100644 --- a/prusti-common/src/config.rs +++ b/prusti-common/src/config.rs @@ -131,6 +131,7 @@ lazy_static::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 testing. settings.set_default::>("verification_deadline", None).unwrap(); @@ -884,3 +885,9 @@ pub fn enable_ghost_constraints() -> bool { pub fn enable_type_invariants() -> bool { read_setting("enable_type_invariants") } + +/// 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 diff --git a/prusti-contracts/src/lib.rs b/prusti-contracts/src/lib.rs index ba0b2c08ccc..990f5bed67a 100644 --- a/prusti-contracts/src/lib.rs +++ b/prusti-contracts/src/lib.rs @@ -351,4 +351,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-interface/src/environment/mod.rs b/prusti-interface/src/environment/mod.rs index f0cf90c3349..a3e08d9c6cd 100644 --- a/prusti-interface/src/environment/mod.rs +++ b/prusti-interface/src/environment/mod.rs @@ -12,10 +12,12 @@ use prusti_rustc_interface::hir::def_id::{DefId, LocalDefId}; use prusti_rustc_interface::middle::ty::{self, Binder, BoundConstness, ImplPolarity, TraitPredicate, TraitRef, TyCtxt}; use prusti_rustc_interface::middle::ty::subst::{Subst, SubstsRef}; use prusti_rustc_interface::trait_selection::infer::{InferCtxtExt, TyCtxtInferExt}; +use prusti_rustc_interface::middle::ty::TypeSuperFoldable; use prusti_rustc_interface::trait_selection::traits::{ImplSource, Obligation, ObligationCause, SelectionContext}; use std::path::PathBuf; use prusti_rustc_interface::errors::{DiagnosticBuilder, EmissionGuarantee, MultiSpan}; use prusti_rustc_interface::span::{Span, symbol::Symbol}; +use prusti_common::config; use std::collections::HashSet; use log::{debug, trace}; use std::rc::Rc; @@ -308,7 +310,11 @@ impl<'tcx> Environment<'tcx> { body .monomorphised_bodies .entry(substs) - .or_insert_with(|| ty::EarlyBinder(body.base_body.clone()).subst(self.tcx, substs)) + .or_insert_with(|| { + let param_env = self.tcx.param_env(def_id); + let substituted = ty::EarlyBinder(body.base_body.clone()).subst(self.tcx, substs); + self.resolve_assoc_types(substituted.clone(), param_env) + }) .clone() } @@ -519,14 +525,31 @@ impl<'tcx> Environment<'tcx> { ) -> (ProcedureDefId, SubstsRef<'tcx>) { use prusti_rustc_interface::middle::ty::TypeVisitable; - // 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. + // 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); } let param_env = self.tcx.param_env(caller_def_id); - traits::resolve_instance(self.tcx, param_env.and((called_def_id, call_substs))) + + // `resolve_instance` below requires normalized 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, 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)) @@ -538,6 +561,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(prusti_rustc_interface::span::DUMMY_SP), param_env) } @@ -577,28 +601,86 @@ impl<'tcx> Environment<'tcx> { ); self.tcx.infer_ctxt().enter(|infcx| { - infcx.predicate_must_hold_considering_regions(&obligation) + infcx.predicate_must_hold_modulo_regions(&obligation) }) } /// Normalizes associated types in foldable types, /// i.e. this resolves projection types ([ty::TyKind::Projection]s) - /// **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 - ); + 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 + } + + 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 prusti_rustc_interface::trait_selection::traits::{fully_normalize, 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) + } + } + } + + normalizable.fold_with(&mut Normalizer {tcx: &self.tcx, param_env}) + } + + 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(); + assert!(ty == first); + walker.next().is_some() + } - match norm_res { - Ok(normalized) => { - debug!("Normalized {:?}: {:?}", normalizable, normalized); - normalized - }, - Err(err) => { - debug!("Error while resolving associated types for {:?}: {:?}", normalizable, err); - normalizable + // Visitor + struct NeedsInfer; + impl<'tcx> ty::TypeVisitor<'tcx> for NeedsInfer { + type BreakTy = (); + + fn visit_ty(&mut self, ty: ty::Ty<'tcx>) -> std::ops::ControlFlow { + use prusti_rustc_interface::middle::ty::{TypeVisitable, TypeSuperVisitable}; + 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 diff --git a/prusti-interface/src/specs/typed.rs b/prusti-interface/src/specs/typed.rs index 501620b4692..d98fda2b8b7 100644 --- a/prusti-interface/src/specs/typed.rs +++ b/prusti-interface/src/specs/typed.rs @@ -318,7 +318,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`. @@ -462,24 +471,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> { @@ -806,69 +797,5 @@ mod tests { )); } } - - 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), - ); - } } } diff --git a/prusti-specs/src/common.rs b/prusti-specs/src/common.rs index 045cbb8e553..bc87dd1f829 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; @@ -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] @@ -329,7 +338,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 @@ -348,25 +357,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. @@ -424,7 +448,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, @@ -522,6 +546,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 { @@ -626,16 +665,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!(), } } diff --git a/prusti-specs/src/specifications/preparser.rs b/prusti-specs/src/specifications/preparser.rs index ff93f8a23d2..47950059d18 100644 --- a/prusti-specs/src/specifications/preparser.rs +++ b/prusti-specs/src/specifications/preparser.rs @@ -797,7 +797,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) }, } } } @@ -894,16 +894,15 @@ mod tests { ); assert_eq!( parse_prusti("exists(|x: i32| a === b)".parse().unwrap()).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("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)))", ); } diff --git a/prusti-specs/src/type_model/mod.rs b/prusti-specs/src/type_model/mod.rs index 9a6e4390b9f..c8fe4fee66d 100644 --- a/prusti-specs/src/type_model/mod.rs +++ b/prusti-specs/src/type_model/mod.rs @@ -21,10 +21,11 @@ use crate::{ UserAnnotatedTypeParam, UserAnnotatedTypeParamParser, UserAnnotatedTypeParamParserError, }, }; -use proc_macro2::{Ident, TokenStream}; +use proc_macro2::{Ident, Span, 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 { @@ -45,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 param in item_struct.generics.params.iter() { + if let syn::GenericParam::Lifetime(lt) = param { + 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,25 +99,34 @@ 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 { input_span: item_struct.span(), item: model_struct, path, }) + } - Ok(Self { - item: model_struct, - path: model_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, @@ -124,18 +142,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 +155,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 +166,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; @@ -262,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, @@ -274,24 +268,51 @@ 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); } } +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::*; #[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 { @@ -302,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()); @@ -334,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] @@ -355,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] @@ -386,7 +407,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); ); @@ -396,22 +417,27 @@ 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(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") } } ); - 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); } @@ -426,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); ); @@ -452,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); } @@ -468,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 { @@ -520,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() } 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..fe526f7027b --- /dev/null +++ b/prusti-tests/tests/verify/fail/closures/using-type-dep.rs @@ -0,0 +1,65 @@ +// compile-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/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 new file mode 100644 index 00000000000..37096357de2 --- /dev/null +++ b/prusti-tests/tests/verify/pass/closures/using-type-dep.rs @@ -0,0 +1,66 @@ +// compile-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); +} 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 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..eb3542db5ee --- /dev/null +++ b/prusti-tests/tests/verify_overflow/pass/iterators/slice-iter.rs @@ -0,0 +1,245 @@ +// 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.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) + )) && + + // 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); +} + +#[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() { + +} + +// 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 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 bd33cc9c5fb..28fc76d5e82 100644 --- a/prusti-viper/src/encoder/mir/pure/pure_functions/interpreter.rs +++ b/prusti-viper/src/encoder/mir/pure/pure_functions/interpreter.rs @@ -566,11 +566,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/encoder_poly.rs b/prusti-viper/src/encoder/mir/pure/specifications/encoder_poly.rs index b6a85bc9e6d..09436d31a2e 100644 --- a/prusti-viper/src/encoder/mir/pure/specifications/encoder_poly.rs +++ b/prusti-viper/src/encoder/mir/pure/specifications/encoder_poly.rs @@ -46,7 +46,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() @@ -54,6 +54,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)? @@ -121,6 +130,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( @@ -133,13 +143,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/pure/specifications/interface.rs b/prusti-viper/src/encoder/mir/pure/specifications/interface.rs index ab1ed95c12c..9a11a558f21 100644 --- a/prusti-viper/src/encoder/mir/pure/specifications/interface.rs +++ b/prusti-viper/src/encoder/mir/pure/specifications/interface.rs @@ -247,6 +247,11 @@ 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!(), } } diff --git a/prusti-viper/src/encoder/mir/specifications/constraints.rs b/prusti-viper/src/encoder/mir/specifications/constraints.rs index 4f6b9663448..fb81c6a2456 100644 --- a/prusti-viper/src/encoder/mir/specifications/constraints.rs +++ b/prusti-viper/src/encoder/mir/specifications/constraints.rs @@ -146,10 +146,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 @@ -161,18 +157,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 @@ -183,6 +175,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); @@ -211,6 +204,18 @@ 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); + let param_env = env.tcx().erase_regions(param_env); + + trace!( + "Constrai nts after resolving associated types and erasing regions: {:#?}", + param_env + ); + param_env } diff --git a/prusti-viper/src/encoder/procedure_encoder.rs b/prusti-viper/src/encoder/procedure_encoder.rs index 3e9fc6ad0ce..6164539b7ae 100644 --- a/prusti-viper/src/encoder/procedure_encoder.rs +++ b/prusti-viper/src/encoder/procedure_encoder.rs @@ -2283,7 +2283,6 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { .. } => { let ty = literal.ty(); - let func_const_val = literal.try_to_value(self.encoder.env().tcx()); 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); @@ -2406,32 +2405,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, - target, - *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( @@ -2445,9 +2418,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, )); } @@ -2988,7 +2961,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { destination: mir::Place<'tcx>, target: Option, called_def_id: ProcedureDefId, - mut substs: ty::subst::SubstsRef<'tcx>, + substs: ty::subst::SubstsRef<'tcx>, ) -> SpannedEncodingResult> { let full_func_proc_name = &self .encoder @@ -2998,66 +2971,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); - // Spans for fake exprs that cannot be encoded in viper - let mut fake_expr_spans: FxHashMap = FxHashMap::default(); - - // 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); - fake_expr_spans.insert(arg, call_site_span); - 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!(); - } - - // TODO: weird fix for closure call substitutions, we need to - // prepend the identity substs of the containing method ... - substs = self.encoder.env().tcx().mk_substs(self.substs.iter().chain(substs)); - } 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()) @@ -3067,9 +2996,12 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { ), arg_ty, encoded_operand.take(), - )); - } - }; + ) + }) + .collect(); + + // Spans for fake exprs that cannot be encoded in viper + let mut fake_expr_spans: FxHashMap = FxHashMap::default(); // 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