WIP: Iterator tracking issues

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.

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")
 }

prusti-interface/src/environment/mod.rs

@@ -478,10 +478,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);
         }
 
@@ -539,7 +539,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)
         })
     }
 
@@ -563,4 +563,33 @@ impl<'tcx> Environment<'tcx> {
             }
         }
     }
-}
+
+    fn any_type_needs_infer<T: ty::TypeFoldable<'tcx>>(&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<Self::BreakTy> {
+                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()
+    }
+}

prusti-interface/src/specs/typed.rs

@@ -247,7 +247,16 @@ impl SpecGraph<ProcedureSpecification> {
     ) -> &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`.

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]
@@ -328,7 +337,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 +356,40 @@ pub(crate) fn merge_generics<T: HasGenerics>(target: &mut T, source: &T) {
 
     // Merge all type params
     let mut existing_target_type_params: HashMap<Ident, &mut TypeParam> = HashMap::new();
+    let mut existing_target_lifetimes: HashMap<Ident, &mut LifetimeDef> = HashMap::new();
     let mut new_generic_params: Vec<GenericParam> = 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.
@@ -423,7 +447,7 @@ pub(crate) fn add_phantom_data_for_generic_params(item_struct: &mut syn::ItemStr
             }
             syn::GenericParam::Lifetime(lt_def) => {
                 let lt = &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,
@@ -521,6 +545,21 @@ mod tests {
                 [impl<T> 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 {
@@ -625,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!(),
             }
         }