[move-model] re-use the address map produced by move compiler (move-l…

…anguage#429)

* [move-model] re-use the address map produced by move compiler

When constructing address aliases for the move model, use the
`NamedAddressMap` produced by the compiler instead of a handwritten one.
This allows move-model (and hence move-prover) to work even when source
and deps paths are supplied in directory format (instead of via the
package system).

* fixup! [move-model] re-use the address map produced by move compiler

language/move-compiler/src/shared/mod.rs

@@ -331,7 +331,7 @@ impl Flags {
         Self {
             test: false,
             verify: true,
-            shadow: false,
+            shadow: true, // allows overlapping between sources and deps
             flavor: "".to_string(),
             bytecode_version: None,
             keep_testing_functions: false,

language/move-model/src/lib.rs

@@ -5,7 +5,7 @@
 #![forbid(unsafe_code)]
 
 use std::{
-    collections::{BTreeMap, BTreeSet, HashMap},
+    collections::{BTreeMap, BTreeSet},
     rc::Rc,
 };
 
@@ -46,7 +46,6 @@ use crate::{
     model::{FunId, FunctionData, GlobalEnv, Loc, ModuleData, ModuleId, StructId},
     options::ModelBuilderOptions,
     simplifier::{SpecRewriter, SpecRewriterPipeline},
-    symbol::{Symbol, SymbolPool},
 };
 
 pub mod ast;
@@ -111,10 +110,6 @@ pub fn run_model_builder_with_options_and_compilation_flags<
     let mut env = GlobalEnv::new();
     env.set_extension(options);
 
-    // Compute this now because the compiler consumes move sources and deps. We need it later
-    // to attach an alias definition to a module.
-    let address_aliases = create_file_to_address_aliases(env.symbol_pool(), &move_sources, &deps);
-
     // Step 1: parse the program to get comments and a separation of targets and dependencies.
     let (files, comments_and_compiler_res) = Compiler::from_package_paths(move_sources, deps)
         .set_flags(flags)
@@ -138,25 +133,44 @@ pub fn run_model_builder_with_options_and_compilation_flags<
         Ok(res) => res,
     };
     let (compiler, parsed_prog) = compiler.into_ast();
+
     // Add source files for targets and dependencies
     let dep_files: BTreeSet<_> = parsed_prog
         .lib_definitions
         .iter()
         .map(|p| p.def.file_hash())
         .collect();
+
+    for member in parsed_prog
+        .source_definitions
+        .iter()
+        .chain(parsed_prog.lib_definitions.iter())
+    {
+        let fhash = member.def.file_hash();
+        let (fname, fsrc) = files.get(&fhash).unwrap();
+        let is_dep = dep_files.contains(&fhash);
+        let aliases = parsed_prog
+            .named_address_maps
+            .get(member.named_address_map)
+            .iter()
+            .map(|(symbol, addr)| (env.symbol_pool().make(symbol.as_str()), *addr))
+            .collect();
+        env.add_source(fhash, Rc::new(aliases), fname.as_str(), fsrc, is_dep);
+    }
+
+    // If a move file does not contain any definition, it will not appear in `parsed_prog`. Add them explicitly.
     for fhash in files.keys().sorted() {
-        let (fname, fsrc) = files.get(fhash).unwrap();
-        let aliases = address_aliases
-            .get(fname)
-            .cloned()
-            .unwrap_or_else(|| Rc::new(BTreeMap::new()));
-        env.add_source(
-            *fhash,
-            aliases,
-            fname.as_str(),
-            fsrc,
-            dep_files.contains(fhash),
-        );
+        if env.get_file_id(*fhash).is_none() {
+            let (fname, fsrc) = files.get(fhash).unwrap();
+            let is_dep = dep_files.contains(fhash);
+            env.add_source(
+                *fhash,
+                Rc::new(BTreeMap::new()),
+                fname.as_str(),
+                fsrc,
+                is_dep,
+            );
+        }
     }
 
     // Add any documentation comments found by the Move compiler to the env.
@@ -192,6 +206,7 @@ pub fn run_model_builder_with_options_and_compilation_flags<
         }
         Ok(compiler) => compiler.into_ast(),
     };
+
     // Extract the module/script closure
     let mut visited_modules = BTreeSet::new();
     for (_, mident, mdef) in &expansion_ast.modules {
@@ -224,6 +239,7 @@ pub fn run_model_builder_with_options_and_compilation_flags<
         });
         E::Program { modules, scripts }
     };
+
     // Run the compiler fully to the compiled units
     let units = match compiler
         .at_expansion(expansion_ast.clone())
@@ -244,6 +260,7 @@ pub fn run_model_builder_with_options_and_compilation_flags<
             units
         }
     };
+
     // Check for bytecode verifier errors (there should not be any)
     let diags = compiled_unit::verify_units(&units);
     if !diags.is_empty() {
@@ -257,29 +274,6 @@ pub fn run_model_builder_with_options_and_compilation_flags<
     Ok(env)
 }
 
-fn create_file_to_address_aliases<
-    Paths: Into<MoveSymbol> + Clone,
-    NamedAddress: Into<MoveSymbol> + Clone,
->(
-    pool: &SymbolPool,
-    move_sources: &[PackagePaths<Paths, NamedAddress>],
-    deps: &[PackagePaths<Paths, NamedAddress>],
-) -> HashMap<MoveSymbol, Rc<BTreeMap<Symbol, NumericalAddress>>> {
-    let mut res = HashMap::<MoveSymbol, _>::new();
-    for pkg in move_sources.iter().chain(deps.iter()) {
-        let aliases = Rc::new(
-            pkg.named_address_map
-                .iter()
-                .map(|(k, v)| (pool.make(k.clone().into().as_ref()), *v))
-                .collect::<BTreeMap<_, _>>(),
-        );
-        for path in &pkg.paths {
-            res.insert(path.clone().into(), aliases.clone());
-        }
-    }
-    res
-}
-
 fn collect_related_modules_recursive<'a>(
     mident: &'a ModuleIdent_,
     modules: &'a UniqueMap<ModuleIdent, ModuleDefinition>,