From dd0dcd25d894024bce91ad59962fb6da48730653 Mon Sep 17 00:00:00 2001 From: Wolfgang Grieskamp Date: Sun, 15 Dec 2024 19:43:52 -0800 Subject: [PATCH] [move-prover] Fix a bug in treatment of type reflection in spec funs (#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 #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. --- third_party/move/move-model/src/model.rs | 11 ++++++++ .../boogie-backend/src/spec_translator.rs | 28 +++++++++++++------ .../src/verification_analysis.rs | 4 +-- .../src/verification_analysis_v2.rs | 2 +- .../sources/functional/type_reflection.move | 14 +++++++++- .../move/tools/move-cli/src/base/prove.rs | 2 +- 6 files changed, 48 insertions(+), 13 deletions(-) diff --git a/third_party/move/move-model/src/model.rs b/third_party/move/move-model/src/model.rs index e7a87dd266c74..63e4749401965 100644 --- a/third_party/move/move-model/src/model.rs +++ b/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 { + let mut target_modules: Vec = 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. diff --git a/third_party/move/move-prover/boogie-backend/src/spec_translator.rs b/third_party/move/move-prover/boogie-backend/src/spec_translator.rs index d3157c01a7161..9ef7a69bf9fe3 100644 --- a/third_party/move/move-prover/boogie-backend/src/spec_translator.rs +++ b/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. diff --git a/third_party/move/move-prover/bytecode-pipeline/src/verification_analysis.rs b/third_party/move/move-prover/bytecode-pipeline/src/verification_analysis.rs index 722077bf3f186..1bcdb94afc03d 100644 --- a/third_party/move/move-prover/bytecode-pipeline/src/verification_analysis.rs +++ b/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(); diff --git a/third_party/move/move-prover/bytecode-pipeline/src/verification_analysis_v2.rs b/third_party/move/move-prover/bytecode-pipeline/src/verification_analysis_v2.rs index def589a6d3ecf..5808200509499 100644 --- a/third_party/move/move-prover/bytecode-pipeline/src/verification_analysis_v2.rs +++ b/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> = target_modules .iter() .flat_map(|mod_env| mod_env.get_functions()) diff --git a/third_party/move/move-prover/tests/sources/functional/type_reflection.move b/third_party/move/move-prover/tests/sources/functional/type_reflection.move index 0149dd4cc572a..0f5ae8e30edc8 100644 --- a/third_party/move/move-prover/tests/sources/functional/type_reflection.move +++ b/third_party/move/move-prover/tests/sources/functional/type_reflection.move @@ -110,12 +110,24 @@ module 0x42::test { type_info::type_of() } spec generic_type_info_verification_target { - ensures result == generic_type_info_spec_fun(); + ensures result == generic_type_info_spec_fun() + && result == generic_type_info_spec_fun_2(); } spec fun generic_type_info_spec_fun(): type_info::TypeInfo { type_info::type_of() } + + spec fun generic_type_info_spec_fun_2(): type_info::TypeInfo { + takes_2() + } + + spec fun takes_2(): type_info::TypeInfo { + // Pass on the 2nd type parameter to be sure the instantiation + // of B is correctly handled + type_info::type_of() + } + } module 0x43::test { diff --git a/third_party/move/tools/move-cli/src/base/prove.rs b/third_party/move/tools/move-cli/src/base/prove.rs index 27a499c3db82f..4b029ddf5be39 100644 --- a/third_party/move/tools/move-cli/src/base/prove.rs +++ b/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() )?;