fix size_of

prusti-interface/src/environment/mod.rs

@@ -55,7 +55,10 @@ struct CachedBody<'tcx> {
     monomorphised_bodies: HashMap<SubstsRef<'tcx>, Rc<mir::Body<'tcx>>>,
     /// Cached borrowck information.
     borrowck_facts: Rc<BorrowckFacts>,
-
+    /// Copies of the MIR body with the given substs applied, called from the
+    /// given caller. This also allows for associated types to be correctly
+    /// normalised.
+    /// TODO: merge more nicely with monomorphised_bodies?
     monomorphised_bodies_with_caller: HashMap<(SubstsRef<'tcx>, LocalDefId), Rc<mir::Body<'tcx>>>,
 }
 

prusti-viper/src/encoder/mir/pure/pure_functions/interface.rs

@@ -17,13 +17,17 @@ use prusti_interface::specs::typed::ProcedureSpecificationKind;
 use std::cell::RefCell;
 use vir_crate::{common::identifier::WithIdentifier, high as vir_high, polymorphic as vir_poly};
 
-/// Key of stored call infos, consisting of the DefId of the called function
-/// and the signature of the function after type substitutions and normalisation
-/// have been applied. The latter is stored to account for different
-/// monomorphisations resulting from the function being called from callers
-/// with different parameter environments. Each variant of a pure function will
-/// be encoded as a separate pure function in Viper.
-type Key<'tcx> = (ProcedureDefId, &'tcx ty::List<ty::Ty<'tcx>>);
+/// Key of stored call infos, consisting of the DefId of the called function,
+/// the normalised type substitutions, and the function signature after type
+/// substitution and normalisation. The second and third components are stored
+/// to account for different monomorphisations resulting from the function
+/// being called from callers (with different parameter environments). Each
+/// variant of a pure function will be encoded as a separate Viper function.
+type Key<'tcx> = (
+    ProcedureDefId,
+    SubstsRef<'tcx>,
+    &'tcx ty::List<ty::Ty<'tcx>>,
+);
 
 /// Compute the key for the given call.
 fn compute_key<'v, 'tcx: 'v>(
@@ -38,8 +42,14 @@ fn compute_key<'v, 'tcx: 'v>(
     } else {
         tcx.fn_sig(proc_def_id)
     };
-    let sig = tcx.subst_and_normalize_erasing_regions(substs, tcx.param_env(caller_def_id), sig);
-    Ok((proc_def_id, sig.inputs_and_output().skip_binder()))
+    let param_env = tcx.param_env(caller_def_id);
+    let sig = tcx.subst_and_normalize_erasing_regions(substs, param_env, sig);
+    let substs = tcx.subst_and_normalize_erasing_regions(
+        substs,
+        param_env,
+        encoder.env().identity_substs(proc_def_id),
+    );
+    Ok((proc_def_id, substs, sig.inputs_and_output().skip_binder()))
 }
 
 type FunctionConstructor<'v, 'tcx> = Box<
@@ -411,7 +421,7 @@ impl<'v, 'tcx: 'v> PureFunctionEncoderInterface<'v, 'tcx>
             .pure_function_encoder_state
             .call_infos_poly
             .borrow_mut();
-        if !call_infos.contains_key(&key) {
+        if let std::collections::hash_map::Entry::Vacant(e) = call_infos.entry(key) {
             // Compute information necessary to encode the function call and
             // memoize it.
             let pure_function_encoder = PureFunctionEncoder::new(
@@ -443,7 +453,7 @@ impl<'v, 'tcx: 'v> PureFunctionEncoderInterface<'v, 'tcx>
                     substs,
                 });
 
-            call_infos.insert(key, function_call_info);
+            e.insert(function_call_info);
         }
         let function_call_info = &call_infos[&key];
 
@@ -471,7 +481,7 @@ impl<'v, 'tcx: 'v> PureFunctionEncoderInterface<'v, 'tcx>
             .pure_function_encoder_state
             .call_infos_high
             .borrow_mut();
-        if !call_infos.contains_key(&key) {
+        if let std::collections::hash_map::Entry::Vacant(e) = call_infos.entry(key) {
             // Compute information necessary to encode the function call and
             // memoize it.
             let function_call_info = super::new_encoder::encode_function_call_info(
@@ -499,7 +509,7 @@ impl<'v, 'tcx: 'v> PureFunctionEncoderInterface<'v, 'tcx>
                 let _ = self.encode_pure_function_use(proc_def_id, parent_def_id, substs)?;
             }
 
-            call_infos.insert(key, function_call_info);
+            e.insert(function_call_info);
         }
         let function_call_info = &call_infos[&key];
 

vir/defs/polymorphic/ast/function.rs

@@ -99,7 +99,7 @@ impl Function {
 
 pub fn compute_identifier(
     name: &str,
-    _type_arguments: &[Type],
+    type_arguments: &[Type],
     formal_args: &[LocalVar],
     return_type: &Type,
 ) -> String {
@@ -123,21 +123,17 @@ pub fn compute_identifier(
         }
     }
     identifier.push_str("__$TY$__");
-    for arg in formal_args {
-        identifier.push_str(&type_name(&arg.typ));
+    // Include the type parameters of the function in the function name
+    for arg in type_arguments {
+        identifier.push_str(&type_name(arg));
         identifier.push('$');
     }
-    identifier.push_str(&type_name(return_type));
-    /*
     // Include the signature of the function in the function name
-    if !type_arguments.is_empty() {
-        identifier.push_str("__$TY$__");
-    }
-    for arg in type_arguments {
-        identifier.push_str(&type_name(arg));
+    for arg in formal_args {
+        identifier.push_str(&type_name(&arg.typ));
         identifier.push('$');
     }
-    */
+    identifier.push_str(&type_name(return_type));
     identifier
 }