fix filter in prover

third_party/move/evm/move-to-yul/src/lib.rs

@@ -65,6 +65,7 @@ pub fn run_to_yul<W: WriteColor>(error_writer: &mut W, mut options: Options) ->
             paths: options.dependencies.clone(),
             named_address_map: addrs,
         }],
+        vec![],
         ModelBuilderOptions::default(),
         flags,
         &known_attributes,
@@ -122,6 +123,7 @@ pub fn run_to_abi_metadata<W: WriteColor>(
             paths: options.dependencies.clone(),
             named_address_map: addrs,
         }],
+        vec![],
         ModelBuilderOptions::default(),
         flags,
         &known_attributes,

third_party/move/evm/move-to-yul/tests/dispatcher_testsuite.rs

@@ -78,6 +78,7 @@ fn compile_yul_to_bytecode_bytes(filename: &str) -> Result<Vec<u8>> {
             paths: deps,
             named_address_map,
         }],
+        vec![],
         ModelBuilderOptions::default(),
         flags,
         &known_attributes,

third_party/move/evm/move-to-yul/tests/testsuite.rs

@@ -60,6 +60,7 @@ fn test_runner(path: &Path) -> datatest_stable::Result<()> {
             paths: deps,
             named_address_map,
         }],
+        vec![],
         ModelBuilderOptions::default(),
         flags,
         &known_attributes,

third_party/move/move-compiler-v2/src/lib.rs

@@ -197,6 +197,10 @@ pub fn run_checker(options: Options) -> anyhow::Result<GlobalEnv> {
             sources: options.dependencies.clone(),
             address_map: addrs.clone(),
         }],
+        PackageInfo {
+            sources: options.sources_deps_for_verification.clone(),
+            address_map: addrs.clone(),
+        },
         options.skip_attribute_checks,
         if !options.skip_attribute_checks && options.known_attributes.is_empty() {
             KnownAttribute::get_all_attribute_names()

third_party/move/move-compiler-v2/src/options.rs

@@ -97,6 +97,9 @@ pub struct Options {
     #[clap(skip)]
     pub sources_deps: Vec<String>,
 
+    #[clap(skip)]
+    pub sources_deps_for_verification: Vec<String>,
+
     /// Warn about use of deprecated functions, modules, etc.
     #[clap(long = cli::MOVE_COMPILER_WARN_OF_DEPRECATION_USE_FLAG,
            default_value=bool_to_str(move_compiler_warn_of_deprecation_use_env_var()))]

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

@@ -93,6 +93,7 @@ pub fn run_model_builder_in_compiler_mode(
     source: PackageInfo,
     source_deps: PackageInfo,
     deps: Vec<PackageInfo>,
+    deps_for_verification: PackageInfo,
     skip_attribute_checks: bool,
     known_attributes: &BTreeSet<String>,
     language_version: LanguageVersion,
@@ -113,6 +114,7 @@ pub fn run_model_builder_in_compiler_mode(
         vec![to_package_paths(source)],
         vec![to_package_paths(source_deps)],
         deps.into_iter().map(to_package_paths).collect(),
+        vec![to_package_paths(deps_for_verification)],
         ModelBuilderOptions {
             compile_via_model: true,
             language_version,
@@ -151,6 +153,7 @@ pub fn run_model_builder_with_options<
         move_sources,
         move_deps,
         deps,
+        vec![],
         options,
         flags,
         known_attributes,
@@ -165,6 +168,7 @@ pub fn run_model_builder_with_options_and_compilation_flags<
     move_sources_targets: Vec<PackagePaths<Paths, NamedAddress>>,
     move_sources_deps: Vec<PackagePaths<Paths, NamedAddress>>,
     deps: Vec<PackagePaths<Paths, NamedAddress>>,
+    deps_for_verification: Vec<PackagePaths<Paths, NamedAddress>>,
     options: ModelBuilderOptions,
     flags: Flags,
     known_attributes: &BTreeSet<String>,
@@ -188,6 +192,15 @@ pub fn run_model_builder_with_options_and_compilation_flags<
                 .to_owned()
         })
         .collect();
+    let filtered_target_sources_names: BTreeSet<String> = deps_for_verification
+        .iter()
+        .flat_map(|pack| pack.paths.iter())
+        .map(|sym| {
+            <Paths as Into<MoveSymbol>>::into(sym.clone())
+                .as_str()
+                .to_owned()
+        })
+        .collect();
 
     // Step 1: parse the program to get comments and a separation of targets and dependencies.
     let (files, comments_and_compiler_res) =
@@ -205,6 +218,7 @@ pub fn run_model_builder_with_options_and_compilation_flags<
                     fsrc,
                     /* is_target */ true,
                     target_sources_names.contains(fname.as_str()),
+                    filtered_target_sources_names.contains(fname.as_str()),
                 );
             }
             add_move_lang_diagnostics(&mut env, diags);
@@ -242,6 +256,7 @@ pub fn run_model_builder_with_options_and_compilation_flags<
             fsrc,
             is_target,
             target_sources_names.contains(fname.as_str()),
+            filtered_target_sources_names.contains(fname.as_str()),
         );
     }
 
@@ -257,6 +272,7 @@ pub fn run_model_builder_with_options_and_compilation_flags<
                 fsrc,
                 is_target,
                 target_sources_names.contains(fname.as_str()),
+                filtered_target_sources_names.contains(fname.as_str()),
             );
         }
     }

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

@@ -560,6 +560,8 @@ pub struct GlobalEnv {
     pub(crate) file_id_is_target: BTreeSet<FileId>,
     /// A set indicating whether a file id is a test/docgen/warning/prover target.
     pub(crate) file_id_is_primary_target: BTreeSet<FileId>,
+    /// A set indicating whether a file id is a filtered out as a prover target.
+    pub(crate) file_id_is_filtered_out_in_verification: BTreeSet<FileId>,
     /// A special constant location representing an unknown location.
     /// This uses a pseudo entry in `source_files` to be safely represented.
     pub(crate) unknown_loc: Loc,
@@ -651,6 +653,7 @@ impl GlobalEnv {
             file_idx_to_id,
             file_id_is_target: BTreeSet::new(),
             file_id_is_primary_target: BTreeSet::new(),
+            file_id_is_filtered_out_in_verification: BTreeSet::new(),
             diags: RefCell::new(vec![]),
             symbol_pool: SymbolPool::new(),
             next_free_node_id: Default::default(),
@@ -815,6 +818,7 @@ impl GlobalEnv {
         source: &str,
         is_target: bool,
         is_primary_target: bool,
+        is_filtered_out: bool,
     ) -> FileId {
         // Check for address alias conflicts.
         self.stdlib_address =
@@ -833,6 +837,14 @@ impl GlobalEnv {
             if is_primary_target && !self.file_id_is_primary_target.contains(file_id) {
                 self.file_id_is_primary_target.insert(*file_id);
             }
+            if is_filtered_out
+                && !self
+                    .file_id_is_filtered_out_in_verification
+                    .contains(file_id)
+            {
+                self.file_id_is_filtered_out_in_verification
+                    .insert(*file_id);
+            }
             *file_id
         } else {
             // Record new source file and properties
@@ -849,6 +861,9 @@ impl GlobalEnv {
             if is_primary_target {
                 self.file_id_is_primary_target.insert(file_id);
             }
+            if is_filtered_out {
+                self.file_id_is_filtered_out_in_verification.insert(file_id);
+            }
             file_id
         }
     }
@@ -2928,6 +2943,13 @@ impl<'env> ModuleEnv<'env> {
         self.env.file_id_is_primary_target.contains(&file_id)
     }
 
+    pub fn is_filtered_out_in_verification(&self) -> bool {
+        let file_id = self.data.loc.file_id;
+        self.env
+            .file_id_is_filtered_out_in_verification
+            .contains(&file_id)
+    }
+
     /// Returns the path to source file of this module.
     pub fn get_source_path(&self) -> &OsStr {
         let file_id = self.data.loc.file_id;
@@ -3028,7 +3050,7 @@ impl<'env> ModuleEnv<'env> {
             && !other.is_script_module()
             // TODO(#13745): fix this when we have a way to check if
             // two non-primary targets are in the same package
-            && (!self.is_primary_target() || other.is_primary_target())
+            && (!self.is_primary_target() || other.is_primary_target() || other.is_filtered_out_in_verification())
             && self.self_address() == other.self_address()
     }
 

third_party/move/move-prover/src/lib.rs

@@ -65,6 +65,7 @@ pub fn create_move_prover_v2_model<W: WriteColor>(
         experiment_cache: Default::default(),
         sources: options.move_sources,
         sources_deps: vec![],
+        sources_deps_for_verification: vec![],
         warn_deprecated: false,
         warn_of_deprecation_use_in_aptos_libs: false,
         warn_unused: false,

third_party/move/testing-infra/transactional-test-runner/src/framework.rs

@@ -936,6 +936,7 @@ fn compile_source_unit(
                         move_target_package,
                         deps_target_package,
                         lib_paths.to_vec(),
+                        vec![],
                         model_options,
                         flags,
                         known_attributes,

third_party/move/tools/move-decompiler/src/lib.rs

@@ -209,6 +209,7 @@ impl Decompiler {
             "",
             true,
             true,
+            true,
         );
         let loc = Loc::new(file_id, Span::new(0, 0));
         SourceMap::new(self.env.to_ir_loc(&loc), None)

third_party/move/tools/move-package/src/compilation/compiled_package.rs

@@ -772,6 +772,7 @@ impl CompiledPackage {
                     vec![sources_package_paths],
                     vec![],
                     deps_package_paths.into_iter().map(|(p, _)| p).collect_vec(),
+                    vec![],
                     ModelBuilderOptions::default(),
                     flags,
                     &known_attributes,

third_party/move/tools/move-package/src/compilation/model_builder.rs

@@ -82,10 +82,12 @@ impl ModelBuilder {
         } else {
             (vec![target], deps)
         };
-        let (all_targets, all_deps) = match &self.model_config.target_filter {
+        let (all_targets, all_deps, false_targets_in_root) = match &self.model_config.target_filter
+        {
             Some(filter) => {
                 let mut new_targets = vec![];
                 let mut new_deps = all_deps.into_iter().map(|(p, _)| p).collect_vec();
+                let mut false_targets_in_root = vec![];
                 for PackagePaths {
                     name,
                     paths,
@@ -103,17 +105,23 @@ impl ModelBuilder {
                     }
                     if !false_targets.is_empty() {
                         new_deps.push(PackagePaths {
+                            name,
+                            paths: false_targets.clone(),
+                            named_address_map: named_address_map.clone(),
+                        });
+                        false_targets_in_root.push(PackagePaths {
                             name,
                             paths: false_targets,
                             named_address_map,
                         })
                     }
                 }
-                (new_targets, new_deps)
+                (new_targets, new_deps, false_targets_in_root)
             },
             None => (
                 all_targets,
                 all_deps.into_iter().map(|(p, _)| p).collect_vec(),
+                vec![],
             ),
         };
 
@@ -137,7 +145,8 @@ impl ModelBuilder {
                 known_attributes,
             ),
             CompilerVersion::V2_0 | CompilerVersion::V2_1 => {
-                let mut options = make_options_for_v2_compiler(all_targets, all_deps);
+                let mut options =
+                    make_options_for_v2_compiler(all_targets, all_deps, false_targets_in_root);
                 options.language_version = self
                     .resolution_graph
                     .build_options
@@ -154,14 +163,22 @@ impl ModelBuilder {
     }
 }
 
-fn make_options_for_v2_compiler(targets: Vec<PackagePaths>, deps: Vec<PackagePaths>) -> Options {
+fn make_options_for_v2_compiler(
+    targets: Vec<PackagePaths>,
+    deps: Vec<PackagePaths>,
+    false_targets_in_root: Vec<PackagePaths>,
+) -> Options {
     let mut options = Options {
         sources: targets
             .iter()
             .flat_map(|p| p.paths.iter().map(|s| s.to_string()).collect_vec())
             .collect(),
         ..Options::default()
     };
+    options.sources_deps_for_verification = false_targets_in_root
+        .iter()
+        .flat_map(|p| p.paths.iter().map(|s| s.to_string()).collect_vec())
+        .collect();
     options.dependencies = deps
         .iter()
         .flat_map(|p| p.paths.iter().map(|s| s.to_string()).collect_vec())