From 70db0798af34245d521458183042711fbcb5cf46 Mon Sep 17 00:00:00 2001 From: Wolfgang Grieskamp Date: Sat, 14 Dec 2024 20:51:26 -0800 Subject: [PATCH] [move-prover] Fix a bug in treatment of type reflection in spec funs 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 | 17 ++++++++--------- .../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, 36 insertions(+), 14 deletions(-) diff --git a/third_party/move/move-model/src/model.rs b/third_party/move/move-model/src/model.rs index e7a87dd266c742..63e47494019656 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 d3157c01a71612..65a96df9b74984 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 @@ -316,10 +316,13 @@ impl<'env> SpecTranslator<'env> { let type_info_params = if type_reflection { (0..fun.type_params.len()) .map(|i| { - format!( - "{}_info: $TypeParamInfo", - boogie_type(self.env, &Type::TypeParameter(i as u16)) - ) + // Apply type instantiation if present + let ty = self + .type_inst + .get(i) + .cloned() + .unwrap_or_else(|| Type::TypeParameter(i as u16)); + format!("{}_info: $TypeParamInfo", boogie_type(self.env, &ty)) }) .collect_vec() } else { @@ -1156,11 +1159,7 @@ impl<'env> SpecTranslator<'env> { { for i in 0..fun_decl.type_params.len() { maybe_comma(); - emit!( - self.writer, - "{}_info", - boogie_type(self.env, &Type::TypeParameter(i as u16)) - ) + emit!(self.writer, "{}_info", boogie_type(self.env, &inst[i])) } } // 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 722077bf3f1860..1bcdb94afc03d2 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 def589a6d3ecf3..58082005094998 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 0149dd4cc572a9..0f5ae8e30edc8f 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 27a499c3db82f3..4b029ddf5be391 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() )?;