[move-prover] Fix a bug in treatment of type reflection in spec funs

third_party/move/move-model/src/model.rs

@@ -885,6 +885,17 @@ impl GlobalEnv {
         target_modules
     }
 
+    /// Find all primary target modules and return in a vector
+    pub fn get_primary_target_modules(&self) -> Vec<ModuleEnv> {
+        let mut target_modules: Vec<ModuleEnv> = vec![];
+        for module_env in self.get_modules() {
+            if module_env.is_primary_target() {
+                target_modules.push(module_env);
+            }
+        }
+        target_modules
+    }
+
     fn add_backtrace(msg: &str, _is_bug: bool) -> String {
         // Note that you need both MOVE_COMPILER_BACKTRACE=1 and RUST_BACKTRACE=1 for this to
         // actually generate a backtrace.

third_party/move/move-prover/boogie-backend/src/spec_translator.rs

@@ -314,11 +314,27 @@ impl<'env> SpecTranslator<'env> {
             }
         };
         let type_info_params = if type_reflection {
+            let mut covered = BTreeSet::new();
             (0..fun.type_params.len())
                 .map(|i| {
+                    // Apply type instantiation if present
+                    let ty = self
+                        .type_inst
+                        .get(i)
+                        .cloned()
+                        .unwrap_or_else(|| Type::TypeParameter(i as u16));
+                    // There can be name clashes after instantiation. Parameters still need
+                    // to be there but all are instantiated with the same type. We escape
+                    // the redundant parameters.
+                    let prefix = if !covered.insert(ty.clone()) {
+                        format!("_{}_", i)
+                    } else {
+                        "".to_string()
+                    };
                     format!(
-                        "{}_info: $TypeParamInfo",
-                        boogie_type(self.env, &Type::TypeParameter(i as u16))
+                        "{}{}_info: $TypeParamInfo",
+                        prefix,
+                        boogie_type(self.env, &ty)
                     )
                 })
                 .collect_vec()
@@ -1154,13 +1170,9 @@ impl<'env> SpecTranslator<'env> {
             .env
             .spec_fun_uses_generic_type_reflection(&module_id.qualified_inst(fun_id, inst.clone()))
         {
-            for i in 0..fun_decl.type_params.len() {
+            for ty in inst {
                 maybe_comma();
-                emit!(
-                    self.writer,
-                    "{}_info",
-                    boogie_type(self.env, &Type::TypeParameter(i as u16))
-                )
+                emit!(self.writer, "{}_info", boogie_type(self.env, ty))
             }
         }
         // Add memory parameters.

third_party/move/move-prover/bytecode-pipeline/src/verification_analysis.rs

@@ -96,7 +96,7 @@ impl FunctionTargetProcessor for VerificationAnalysisProcessor {
 
         // Rule 2: verify the function if it is within the target modules
         let env = fun_env.module_env.env;
-        let target_modules = env.get_target_modules();
+        let target_modules = env.get_primary_target_modules();
 
         let is_in_target_module = target_modules
             .iter()
@@ -162,7 +162,7 @@ impl FunctionTargetProcessor for VerificationAnalysisProcessor {
 
         writeln!(f, "invariant applicability: [")?;
         let target_invs: BTreeSet<_> = env
-            .get_target_modules()
+            .get_primary_target_modules()
             .iter()
             .flat_map(|menv| env.get_global_invariants_by_module(menv.get_id()))
             .collect();

third_party/move/move-prover/bytecode-pipeline/src/verification_analysis_v2.rs

@@ -661,7 +661,7 @@ impl FunctionTargetProcessor for VerificationAnalysisProcessorV2 {
             _ => {},
         }
 
-        let target_modules = global_env.get_target_modules();
+        let target_modules = global_env.get_primary_target_modules();
         let target_fun_ids: BTreeSet<QualifiedId<FunId>> = target_modules
             .iter()
             .flat_map(|mod_env| mod_env.get_functions())

third_party/move/move-prover/tests/sources/functional/type_reflection.move

@@ -110,12 +110,24 @@ module 0x42::test {
        type_info::type_of<A>()
     }
     spec generic_type_info_verification_target {
-        ensures result == generic_type_info_spec_fun<A>();
+        ensures result == generic_type_info_spec_fun<A>()
+            && result == generic_type_info_spec_fun_2<A>();
     }
 
     spec fun generic_type_info_spec_fun<A>(): type_info::TypeInfo {
         type_info::type_of<A>()
     }
+
+    spec fun generic_type_info_spec_fun_2<A>(): type_info::TypeInfo {
+        takes_2<A, A>()
+    }
+
+    spec fun takes_2<A, B>(): type_info::TypeInfo {
+        // Pass on the 2nd type parameter to be sure the instantiation
+        // of B is correctly handled
+        type_info::type_of<B>()
+    }
+
 }
 
 module 0x43::test {

third_party/move/tools/move-cli/src/base/prove.rs

@@ -230,7 +230,7 @@ pub fn run_move_prover(
             } else {
                 "FAILURE".bold().red()
             },
-            model.get_target_modules().len(),
+            model.get_primary_target_modules().len(),
             basedir,
             now.elapsed().as_secs_f64()
         )?;