[move-prover] Fix a bug in treatment of type reflection in spec funs (aptos-labs#15606)

When calling a generic function in a specification expression which transitively uses type reflection, the function call type instantiation wasn't correctly treated for the type info parameters. The refined test generates this situation and failed before but passes now.

Removes the boogie compilation error in aptos-labs#15605, but after this the example in this bug times out, even though the package does not contain any specs. I verified that all verification conditions belong to functions in this package, but this does not change this. Should be fixed in subsequent PR before closing the bug.

Author: wrwg

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()
         )?;