when a verusroot is present, with source files, remap spans so that t…

…hey are available in binary releases

source/rust_verify/example/basic_failure.rs

@@ -16,5 +16,9 @@ verus! {
     {
         *r = 0;
     }
+
+    proof fn external_span(s: Seq<nat>) {
+        assert(s[0] == 0);
+    }
 
 }

source/rust_verify/src/driver.rs

@@ -1,4 +1,5 @@
 use crate::config::Vstd;
+use crate::externs::VerusExterns;
 use crate::verifier::{Verifier, VerifierCallbacksEraseMacro};
 use rustc_errors::ErrorGuaranteed;
 use std::time::{Duration, Instant};
@@ -196,70 +197,6 @@ pub fn find_verusroot() -> Option<VerusRoot> {
         })
 }
 
-#[cfg(target_os = "macos")]
-mod lib_exe_names {
-    pub const LIB_PRE: &str = "lib";
-    pub const LIB_DL: &str = "dylib";
-}
-
-#[cfg(target_os = "linux")]
-mod lib_exe_names {
-    pub const LIB_PRE: &str = "lib";
-    pub const LIB_DL: &str = "so";
-}
-
-#[cfg(target_os = "windows")]
-mod lib_exe_names {
-    pub const LIB_PRE: &str = "";
-    pub const LIB_DL: &str = "dll";
-}
-
-use lib_exe_names::{LIB_DL, LIB_PRE};
-
-#[derive(Debug)]
-pub struct VerusExterns<'a> {
-    path: &'a std::path::PathBuf,
-    has_vstd: bool,
-    has_builtin: bool,
-}
-
-impl<'a> VerusExterns<'a> {
-    pub fn to_args(&self) -> impl Iterator<Item = String> {
-        let mut args = vec![
-            format!("--extern"),
-            format!(
-                "builtin_macros={}",
-                self.path.join(format!("{LIB_PRE}builtin_macros.{LIB_DL}")).to_str().unwrap()
-            ),
-            format!("--extern"),
-            format!(
-                "state_machines_macros={}",
-                self.path
-                    .join(format!("{LIB_PRE}state_machines_macros.{LIB_DL}"))
-                    .to_str()
-                    .unwrap()
-            ),
-            format!("-L"),
-            format!("dependency={}", self.path.to_str().unwrap()),
-        ];
-        if self.has_builtin {
-            args.push(format!("--extern"));
-            args.push(format!(
-                "builtin={}",
-                self.path.join(format!("libbuiltin.rlib")).to_str().unwrap()
-            ));
-        }
-        if self.has_vstd {
-            args.push(format!("--extern"));
-            args.push(format!(
-                "vstd={}",
-                self.path.join(format!("libvstd.rlib")).to_str().unwrap()
-            ));
-        }
-        args.into_iter()
-    }
-}
-
 pub fn run<F>(
     verifier: Verifier,
     mut rustc_args: Vec<String>,
@@ -278,19 +215,25 @@ where
         rustc_args.push(format!("--edition"));
         rustc_args.push(format!("2021"));
     }
-    if !build_test_mode {
+    // TODO simplify
+    let verus_externs = if !build_test_mode {
         if let Some(VerusRoot { path: verusroot, in_vargo }) = verus_root {
             let externs = VerusExterns {
-                path: &verusroot,
+                verus_root: verusroot.clone(),
                 has_vstd: verifier.args.vstd == Vstd::Imported,
                 has_builtin: verifier.args.vstd != Vstd::IsCore,
             };
             rustc_args.extend(externs.to_args());
             if in_vargo && !std::env::var("VERUS_Z3_PATH").is_ok() {
                 panic!("we are in vargo, but VERUS_Z3_PATH is not set; this is a bug");
             }
+            if !in_vargo { Some(externs) } else { None }
+        } else {
+            None
         }
-    }
+    } else {
+        None
+    };
 
     let time0 = Instant::now();
     let mut rustc_args_verify = rustc_args.clone();
@@ -308,6 +251,7 @@ where
         lifetime_end_time: None,
         rustc_args: rustc_args.clone(),
         file_loader: Some(Box::new(file_loader.clone())),
+        verus_externs,
     };
     let status = run_compiler(
         rustc_args_verify.clone(),

source/rust_verify/src/externs.rs

@@ -0,0 +1,96 @@
+#[cfg(target_os = "macos")]
+mod lib_exe_names {
+    pub const LIB_PRE: &str = "lib";
+    pub const LIB_DL: &str = "dylib";
+}
+
+#[cfg(target_os = "linux")]
+mod lib_exe_names {
+    pub const LIB_PRE: &str = "lib";
+    pub const LIB_DL: &str = "so";
+}
+
+#[cfg(target_os = "windows")]
+mod lib_exe_names {
+    pub const LIB_PRE: &str = "";
+    pub const LIB_DL: &str = "dll";
+}
+
+use lib_exe_names::{LIB_DL, LIB_PRE};
+
+#[derive(Debug)]
+pub struct VerusExterns {
+    pub verus_root: std::path::PathBuf,
+    pub has_vstd: bool,
+    pub has_builtin: bool,
+}
+
+pub enum VerusExtern {
+    Macros,
+    Builtin,
+    Vstd,
+}
+
+fn verus_builtin_std() -> Box<[(VerusExtern, &'static str, String)]> {
+    vec![
+        (VerusExtern::Macros, "builtin_macros", format!("{LIB_PRE}builtin_macros.{LIB_DL}")),
+        (
+            VerusExtern::Macros,
+            "state_machines_macros",
+            format!("{LIB_PRE}state_machines_macros.{LIB_DL}"),
+        ),
+        (VerusExtern::Builtin, "builtin", format!("libbuiltin.rlib")),
+        (VerusExtern::Vstd, "vstd", format!("libvstd.rlib")),
+    ]
+    .into_boxed_slice()
+}
+
+impl VerusExterns {
+    pub fn to_args(&self) -> impl Iterator<Item = String> {
+        let mut args = Vec::new();
+        args.push(format!("-L"));
+        args.push(format!("dependency={}", self.verus_root.to_str().unwrap()));
+        for (extern_, name, file) in verus_builtin_std().iter() {
+            match extern_ {
+                VerusExtern::Macros => {}
+                VerusExtern::Builtin => {
+                    if !self.has_builtin {
+                        continue;
+                    }
+                }
+                VerusExtern::Vstd => {
+                    if !self.has_vstd {
+                        continue;
+                    }
+                }
+            }
+            let path = self.verus_root.join(file);
+            let path = path.to_str().unwrap();
+            args.push(format!("--extern"));
+            args.push(format!("{}={}", name, path));
+        }
+        args.into_iter()
+    }
+
+    pub fn to_path_mappings(&self) -> Box<[(String, std::path::PathBuf)]> {
+        let mut args = Vec::new();
+        for (extern_, name, _file) in verus_builtin_std().iter() {
+            match extern_ {
+                VerusExtern::Macros => {}
+                VerusExtern::Builtin => {
+                    if !self.has_builtin {
+                        continue;
+                    }
+                }
+                VerusExtern::Vstd => {
+                    if !self.has_vstd {
+                        continue;
+                    }
+                }
+            }
+            let path = self.verus_root.join(name);
+            args.push((name.to_string(), path));
+        }
+        args.into_boxed_slice()
+    }
+}

source/rust_verify/src/lib.rs

@@ -42,6 +42,7 @@ pub mod def;
 pub mod driver;
 pub mod erase;
 mod expand_errors_driver;
+pub mod externs;
 pub mod file_loader;
 mod fn_call_to_vir;
 mod hir_hide_reveal_rewrite;

source/rust_verify/src/spans.rs

@@ -8,6 +8,8 @@ use std::sync::{Arc, Mutex};
 use vir::ast::{SpannedTyped, Typ};
 use vir::def::Spanned;
 
+use crate::externs::VerusExterns;
+
 pub(crate) fn to_raw_span(span: Span) -> vir::messages::RawSpan {
     Arc::new(span.data())
 }
@@ -72,10 +74,12 @@ impl SpanContextX {
         local_crate: StableCrateId,
         source_map: &SourceMap,
         original_crate_files: HashMap<u64, HashMap<Vec<u8>, FileStartEndPos>>,
+        verus_externs: Option<&VerusExterns>,
     ) -> SpanContext {
         let mut imported_crates = HashMap::new();
         let mut local_files = HashMap::new();
         let mut remaining_crate_files = original_crate_files.clone();
+        let path_mappings = verus_externs.map(|x| x.to_path_mappings());
 
         for source_file in source_map.files().iter() {
             match *source_file.external_src.borrow() {
@@ -100,7 +104,46 @@ impl SpanContextX {
                         original_crate_files.get(&imported_crate).and_then(|x| x.get(&hash))
                     {
                         remaining_crate_files.get_mut(&imported_crate).unwrap().remove(&hash);
-                        let info = ExternSourceInfo::Loaded { start_pos, end_pos };
+                        let info = if let FileName::Real(real_file_name) = &source_file.name {
+                            // Ideally we'd change this into Remapped, but I don't know how to do that
+                            if let (Some(path_mappings), RealFileName::LocalPath(local_file_name)) =
+                                (&path_mappings, real_file_name)
+                            {
+                                let mut found_match = None;
+                                for (name, epath) in path_mappings.iter() {
+                                    // search for source/<name> in local_file_path.components()
+                                    let mut found = 0;
+                                    let mut components = local_file_name.components();
+                                    while let Some(c) = components.next() {
+                                        if found == 0 {
+                                            if c.as_os_str().to_str().unwrap() == "source" {
+                                                found += 1;
+                                            }
+                                        } else if found == 1 {
+                                            if c.as_os_str().to_str().unwrap() == name {
+                                                found += 1;
+                                                break;
+                                            }
+                                        }
+                                    }
+                                    let rest = components.as_path().to_path_buf();
+                                    if found == 2 {
+                                        found_match = Some((name, epath, rest));
+                                        break;
+                                    }
+                                }
+                                if let Some((_, base_path, file)) = found_match {
+                                    let filename = base_path.join(file);
+                                    ExternSourceInfo::Delayed { filename, hash }
+                                } else {
+                                    ExternSourceInfo::Loaded { start_pos, end_pos }
+                                }
+                            } else {
+                                ExternSourceInfo::Loaded { start_pos, end_pos }
+                            }
+                        } else {
+                            ExternSourceInfo::Loaded { start_pos, end_pos }
+                        };
                         let file = ExternSourceFile {
                             original_start_pos: BytePos(original.start_pos),
                             original_end_pos: BytePos(original.end_pos),

source/rust_verify/src/verifier.rs

@@ -2,6 +2,7 @@ use crate::commands::{Op, OpGenerator, OpKind, QueryOp, Style};
 use crate::config::{Args, ShowTriggers};
 use crate::context::{ContextX, ErasureInfo};
 use crate::debugger::Debugger;
+use crate::externs::VerusExterns;
 use crate::spans::{from_raw_span, SpanContext, SpanContextX};
 use crate::user_filter::UserFilter;
 use crate::util::error;
@@ -2762,6 +2763,7 @@ pub(crate) struct VerifierCallbacksEraseMacro {
     pub(crate) rustc_args: Vec<String>,
     pub(crate) file_loader:
         Option<Box<dyn 'static + rustc_span::source_map::FileLoader + Send + Sync>>,
+    pub(crate) verus_externs: Option<VerusExterns>,
 }
 
 pub(crate) static BODY_HIR_ID_TO_REVEAL_PATH_RES: std::sync::RwLock<
@@ -2846,6 +2848,7 @@ impl rustc_driver::Callbacks for VerifierCallbacksEraseMacro {
                 tcx.stable_crate_id(LOCAL_CRATE),
                 compiler.sess.source_map(),
                 imported.metadatas.into_iter().map(|c| (c.crate_id, c.original_files)).collect(),
+                self.verus_externs.as_ref(),
             );
             {
                 let reporter = Reporter::new(&spans, compiler);

tools/vargo/src/main.rs

@@ -1237,6 +1237,57 @@ cd "$( dirname "${{BASH_SOURCE[0]}}" )"
                 }
             }
 
+            fn copy_dir(
+                src: &std::path::Path,
+                dest: &std::path::Path,
+                exclude: &[&std::path::Path],
+            ) -> std::io::Result<()> {
+                assert!(exclude.iter().all(|x| x.is_relative()));
+                copy_dir_internal(src, dest, exclude, 0)
+            }
+
+            fn copy_dir_internal<'a>(
+                src: &std::path::Path,
+                dest: &std::path::Path,
+                exclude: &[&std::path::Path],
+                depth: usize,
+            ) -> std::io::Result<()> {
+                std::fs::create_dir_all(dest)?;
+                for entry in std::fs::read_dir(src)? {
+                    let entry = entry?;
+                    let path = entry.path();
+                    let dest_path = dest.join(path.file_name().unwrap());
+                    if exclude.iter().any(|xcl| {
+                        let xcl = xcl.iter().skip(depth).collect::<std::path::PathBuf>();
+                        path.starts_with(xcl)
+                    }) {
+                        continue;
+                    }
+                    if entry.file_type()?.is_dir() {
+                        copy_dir(&path, &dest_path, exclude)?;
+                    } else {
+                        std::fs::copy(&path, &dest_path)?;
+                    }
+                }
+                Ok(())
+            }
+
+            for src in [
+                format!("builtin"),
+                format!("builtin_macros"),
+                format!("state_machines_macros"),
+                format!("vstd"),
+            ] {
+                let from_d = std::path::Path::new(&src);
+                let to_d = target_verus_dir.join(&src);
+
+                if to_d.exists() {
+                    std::fs::remove_dir_all(&to_d).unwrap();
+                }
+                copy_dir(from_d, &to_d, &[&std::path::Path::new("target")])
+                    .map_err(|_| format!("could not copy source directory {src}"))?;
+            }
+
             let stored_fingerprint = if fingerprint_path.exists() {
                 let s = std::fs::read_to_string(&fingerprint_path)
                     .map_err(|x| format!("cannot read {} ({x:?})", fingerprint_path.display()))?;