Merge pull request #987 from verus-lang/remove-custom-vstd-build-driver

Remove custom vstd build driver

source/rust_verify/src/config.rs

@@ -47,7 +47,6 @@ pub struct LogArgs {
 
 #[derive(Debug)]
 pub struct ArgsX {
-    pub pervasive_path: Option<String>,
     pub export: Option<String>,
     pub import: Vec<(String, String)>,
     pub verify_root: bool,
@@ -87,7 +86,6 @@ pub struct ArgsX {
 impl ArgsX {
     pub fn new() -> Self {
         Self {
-            pervasive_path: Default::default(),
             export: Default::default(),
             import: Default::default(),
             verify_root: Default::default(),
@@ -442,7 +440,6 @@ pub fn parse_args_with_imports(
     let extended = parse_opts_or_pairs(matches.opt_strs(OPT_EXTENDED_MULTI));
 
     let args = ArgsX {
-        pervasive_path: None,
         verify_root: matches.opt_present(OPT_VERIFY_ROOT),
         export: matches.opt_str(OPT_EXPORT),
         import: import,

source/rust_verify/src/context.rs

@@ -27,11 +27,11 @@ pub struct ContextX<'tcx> {
     pub(crate) krate: &'tcx Crate<'tcx>,
     pub(crate) erasure_info: ErasureInfoRef,
     pub(crate) spans: crate::spans::SpanContext,
-    pub(crate) vstd_crate_name: Option<Ident>,
     pub(crate) verus_items: Arc<VerusItems>,
     pub(crate) diagnostics: std::rc::Rc<std::cell::RefCell<Vec<vir::ast::VirErrAs>>>,
     pub(crate) no_vstd: bool,
     pub(crate) arch_word_bits: Option<vir::ast::ArchWordBits>,
+    pub(crate) vstd_crate_name: Ident,
 }
 
 #[derive(Clone)]

source/rust_verify/src/driver.rs

@@ -18,7 +18,6 @@ fn run_compiler<'a, 'b>(
     erase_ghost: bool,
     verifier: &'b mut (dyn rustc_driver::Callbacks + Send),
     file_loader: Box<dyn 'static + rustc_span::source_map::FileLoader + Send + Sync>,
-    _build_test_mode: bool, // TODO is this needed?
 ) -> Result<(), ErrorGuaranteed> {
     crate::config::enable_default_features_and_verus_attr(
         &mut rustc_args,
@@ -121,7 +120,6 @@ pub(crate) fn run_with_erase_macro_compile(
     mut rustc_args: Vec<String>,
     file_loader: Box<dyn 'static + rustc_span::source_map::FileLoader + Send + Sync>,
     compile: bool,
-    build_test_mode: bool,
 ) -> Result<(), ErrorGuaranteed> {
     let mut callbacks = CompilerCallbacksEraseMacro { do_compile: compile };
     rustc_args.extend(["--cfg", "verus_keep_ghost"].map(|s| s.to_string()));
@@ -141,7 +139,7 @@ pub(crate) fn run_with_erase_macro_compile(
     for a in allow {
         rustc_args.extend(["-A", a].map(|s| s.to_string()));
     }
-    run_compiler(rustc_args, true, true, &mut callbacks, file_loader, build_test_mode)
+    run_compiler(rustc_args, true, true, &mut callbacks, file_loader)
 }
 
 pub struct VerusRoot {
@@ -184,6 +182,7 @@ pub fn find_verusroot() -> Option<VerusRoot> {
                         }
                         Some(VerusRoot { path, in_vargo: false })
                     } else {
+                        // TODO suppress warning when building verus itself
                         eprintln!("warning: did not find a valid verusroot; continuing, but the builtin and vstd crates are likely missing");
                         None
                     }
@@ -258,20 +257,22 @@ pub fn run<F>(
     build_test_mode: bool,
 ) -> (Verifier, Stats, Result<(), ()>)
 where
-    F: 'static + rustc_span::source_map::FileLoader + Send + Sync + Clone,
+    F: 'static
+        + rustc_span::source_map::FileLoader
+        + crate::file_loader::FileLoaderClone
+        + Send
+        + Sync,
 {
+    rustc_args.push(format!("--edition"));
+    rustc_args.push(format!("2018"));
     if !build_test_mode {
         if let Some(VerusRoot { path: verusroot, in_vargo }) = verus_root {
-            rustc_args.push(format!("--edition"));
-            rustc_args.push(format!("2018"));
             let externs = VerusExterns { path: &verusroot, has_vstd: !verifier.args.no_vstd };
             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");
             }
         }
-    } else if verifier.args.no_vstd {
-        panic!("cannot use --no-vstd in test mode");
     }
 
     let time0 = Instant::now();
@@ -287,15 +288,13 @@ where
         lifetime_end_time: None,
         rustc_args: rustc_args.clone(),
         file_loader: Some(Box::new(file_loader.clone())),
-        build_test_mode,
     };
     let status = run_compiler(
         rustc_args_verify.clone(),
         true,
         false,
         &mut verifier_callbacks,
         Box::new(file_loader.clone()),
-        build_test_mode,
     );
     let VerifierCallbacksEraseMacro {
         verifier,
@@ -344,12 +343,7 @@ where
     let compile_status = if !verifier.args.compile && verifier.args.no_lifetime {
         Ok(())
     } else {
-        run_with_erase_macro_compile(
-            rustc_args,
-            Box::new(file_loader),
-            verifier.args.compile,
-            build_test_mode,
-        )
+        run_with_erase_macro_compile(rustc_args, Box::new(file_loader), verifier.args.compile)
     };
 
     let time2 = Instant::now();

source/rust_verify/src/file_loader.rs

@@ -1,40 +1,11 @@
-/// A rustc file loader that remaps "pervasive" to a user-provided path
-#[derive(Clone)]
-pub struct PervasiveFileLoader {
-    pervasive_path: Option<String>,
-}
-
-impl PervasiveFileLoader {
-    pub fn new(pervasive_path: Option<String>) -> Self {
-        Self { pervasive_path }
-    }
+pub use rustc_span::source_map::RealFileLoader;
 
-    fn remap_pervasive_path(&self, path: &std::path::Path) -> std::path::PathBuf {
-        if let Some(pervasive_path) = &self.pervasive_path {
-            if path.parent().and_then(|x| x.file_name()) == Some(std::ffi::OsStr::new("pervasive"))
-            {
-                if let Some(file_name) = path.file_name() {
-                    return std::path::Path::new(pervasive_path).join(file_name).into();
-                }
-            }
-        }
-        path.into()
-    }
+pub trait FileLoaderClone {
+    fn clone(&self) -> Self;
 }
 
-impl rustc_span::source_map::FileLoader for PervasiveFileLoader {
-    fn file_exists(&self, path: &std::path::Path) -> bool {
-        let path = self.remap_pervasive_path(path);
-        rustc_span::source_map::RealFileLoader.file_exists(&path)
-    }
-
-    fn read_file(&self, path: &std::path::Path) -> Result<String, std::io::Error> {
-        let path = self.remap_pervasive_path(path);
-        rustc_span::source_map::RealFileLoader.read_file(&path)
-    }
-
-    fn read_binary_file(&self, path: &std::path::Path) -> Result<Vec<u8>, std::io::Error> {
-        let path = self.remap_pervasive_path(path);
-        rustc_span::source_map::RealFileLoader.read_binary_file(&path)
+impl FileLoaderClone for RealFileLoader {
+    fn clone(&self) -> Self {
+        rustc_span::source_map::RealFileLoader
     }
 }

source/rust_verify/src/main.rs

@@ -37,51 +37,6 @@ pub fn main() {
                 rust_verify::lifetime::lifetime_rustc_driver(&internal_args[..], buffer);
                 return;
             }
-            "--internal-build-vstd-driver" => {
-                let pervasive_path = internal_args.next().unwrap();
-                let vstd_vir = internal_args.next().unwrap();
-                let target_path = std::path::PathBuf::from(internal_args.next().unwrap());
-                let verify = match internal_args.next().unwrap().as_str() {
-                    "verify" => true,
-                    "no-verify" => false,
-                    _ => panic!("invalid verify argument"),
-                };
-                let trace = match internal_args.next().unwrap().as_str() {
-                    "trace" => true,
-                    "no-trace" => false,
-                    _ => panic!("invalid trace argument"),
-                };
-                let log_all = match internal_args.next().unwrap().as_str() {
-                    "log-all" => true,
-                    "no-log-all" => false,
-                    _ => panic!("invalid trace argument"),
-                };
-
-                let mut internal_args: Vec<_> = internal_args.collect();
-                internal_args.insert(0, internal_program);
-
-                use rust_verify::config::{Args, ArgsX};
-                use rust_verify::file_loader::PervasiveFileLoader;
-                use rust_verify::verifier::Verifier;
-
-                let mut our_args: ArgsX = ArgsX::new();
-                our_args.pervasive_path = Some(pervasive_path.to_string());
-                our_args.no_verify = !verify;
-                our_args.no_lifetime = !verify;
-                our_args.multiple_errors = 2;
-                our_args.export = Some(target_path.join(vstd_vir).to_str().unwrap().to_string());
-                our_args.compile = true;
-                our_args.trace = trace;
-                our_args.log_all = log_all;
-                let our_args = Args::from(our_args);
-
-                let file_loader = PervasiveFileLoader::new(Some(pervasive_path.to_string()));
-                let verifier = Verifier::new(our_args);
-                let (_verifier, _stats, status) =
-                    rust_verify::driver::run(verifier, internal_args, None, file_loader, true);
-                status.expect("failed to build vstd library");
-                return;
-            }
             "--internal-test-mode" => true,
             _ => false,
         }
@@ -139,11 +94,9 @@ pub fn main() {
         }
     }
 
-    let pervasive_path = our_args.pervasive_path.clone();
-
     std::env::set_var("RUSTC_BOOTSTRAP", "1");
 
-    let file_loader = rust_verify::file_loader::PervasiveFileLoader::new(pervasive_path);
+    let file_loader = rust_verify::file_loader::RealFileLoader;
     let verifier = rust_verify::verifier::Verifier::new(our_args);
 
     let (verifier, stats, status) =

source/rust_verify/src/rust_to_vir_func.rs

@@ -751,7 +751,7 @@ pub(crate) fn check_item_fn<'tcx>(
     // calling it. But we translate things to point to it internally, so we need to
     // mark it non-private in order to avoid errors down the line.
     let mut visibility = visibility;
-    if path == vir::def::exec_nonstatic_call_path(&ctxt.vstd_crate_name) {
+    if path == vir::def::exec_nonstatic_call_path(&Some(ctxt.vstd_crate_name.clone())) {
         visibility.restricted_to = None;
     }
 

source/rust_verify/src/verifier.rs

@@ -32,7 +32,7 @@ use std::time::{Duration, Instant};
 use vir::context::GlobalCtx;
 
 use crate::buckets::{Bucket, BucketId};
-use vir::ast::{Fun, Ident, Krate, VirErr};
+use vir::ast::{Fun, Krate, VirErr};
 use vir::ast_util::{fun_as_friendly_rust_name, is_visible_to};
 use vir::def::{
     path_to_string, CommandContext, CommandsWithContext, CommandsWithContextX, SnapPos,
@@ -272,7 +272,6 @@ pub struct Verifier {
     created_solver_log_dir: Arc<std::sync::Mutex<Option<std::path::PathBuf>>>,
     vir_crate: Option<Krate>,
     crate_names: Option<Vec<String>>,
-    vstd_crate_name: Option<Ident>,
     air_no_span: Option<vir::messages::Span>,
     current_crate_modules: Option<Vec<vir::ast::Module>>,
     buckets: HashMap<BucketId, Bucket>,
@@ -378,7 +377,6 @@ impl Verifier {
             created_solver_log_dir: Arc::new(std::sync::Mutex::new(None)),
             vir_crate: None,
             crate_names: None,
-            vstd_crate_name: None,
             air_no_span: None,
             current_crate_modules: None,
             buckets: HashMap::new(),
@@ -409,7 +407,6 @@ impl Verifier {
             created_solver_log_dir: self.created_solver_log_dir.clone(),
             vir_crate: self.vir_crate.clone(),
             crate_names: self.crate_names.clone(),
-            vstd_crate_name: self.vstd_crate_name.clone(),
             air_no_span: self.air_no_span.clone(),
             current_crate_modules: self.current_crate_modules.clone(),
             buckets: self.buckets.clone(),
@@ -1638,12 +1635,7 @@ impl Verifier {
         }
 
         let (pruned_krate, mono_abstract_datatypes, lambda_types, bound_traits, fndef_types) =
-            vir::prune::prune_krate_for_module(
-                &krate,
-                bucket_id.module(),
-                bucket_id.function(),
-                &self.vstd_crate_name,
-            );
+            vir::prune::prune_krate_for_module(&krate, bucket_id.module(), bucket_id.function());
         let mut ctx = vir::context::Ctx::new(
             &pruned_krate,
             global_ctx,
@@ -1702,7 +1694,6 @@ impl Verifier {
             air_no_span.clone(),
             self.args.rlimit,
             Arc::new(std::sync::Mutex::new(None)),
-            self.vstd_crate_name.clone(),
         )?;
         vir::recursive_types::check_traits(&krate, &global_ctx)?;
         let krate = vir::ast_simplify::simplify_krate(&mut global_ctx, &krate)?;
@@ -2299,22 +2290,18 @@ impl Verifier {
         };
         let erasure_info = std::rc::Rc::new(std::cell::RefCell::new(erasure_info));
         let import_len = self.args.import.len();
-        let vstd_crate_name = if import_len > 0 || self.args.export.is_some() {
-            Some(Arc::new(vir::def::VERUSLIB.to_string()))
-        } else {
-            None
-        };
+        let vstd_crate_name = Arc::new(vir::def::VERUSLIB.to_string());
         let mut ctxt = Arc::new(ContextX {
             cmd_line_args: self.args.clone(),
             tcx,
             krate: hir.krate(),
             erasure_info,
             spans: spans.clone(),
-            vstd_crate_name: vstd_crate_name.clone(),
             verus_items,
             diagnostics: std::rc::Rc::new(std::cell::RefCell::new(Vec::new())),
             no_vstd: self.args.no_vstd,
             arch_word_bits: None,
+            vstd_crate_name,
         });
         let multi_crate = self.args.export.is_some() || import_len > 0;
         crate::rust_to_vir_base::MULTI_CRATE
@@ -2390,7 +2377,6 @@ impl Verifier {
 
         self.vir_crate = Some(vir_crate.clone());
         self.crate_names = Some(crate_names);
-        self.vstd_crate_name = vstd_crate_name;
 
         let erasure_info = ctxt.erasure_info.borrow();
         let hir_vir_ids = erasure_info.hir_vir_ids.clone();
@@ -2459,7 +2445,6 @@ 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) build_test_mode: bool,
 }
 
 pub(crate) static BODY_HIR_ID_TO_REVEAL_PATH_RES: std::sync::RwLock<
@@ -2593,7 +2578,6 @@ impl rustc_driver::Callbacks for VerifierCallbacksEraseMacro {
                                 self.rustc_args.clone(),
                                 file_loader,
                                 false,
-                                self.build_test_mode,
                             );
                             if compile_status.is_err() {
                                 return;

source/rust_verify_test/tests/common/mod.rs

@@ -279,8 +279,6 @@ pub fn run_verus(
 
     verus_args.extend(
         vec![
-            "--edition".to_string(),
-            "2018".to_string(),
             "--crate-name".to_string(),
             "test_crate".to_string(),
             "--crate-type".to_string(),

source/vir/src/ast_simplify.rs

@@ -1147,7 +1147,6 @@ pub fn simplify_krate(ctx: &mut GlobalCtx, krate: &Krate) -> Result<Krate, VirEr
         ctx.no_span.clone(),
         ctx.rlimit,
         ctx.interpreter_log.clone(),
-        ctx.vstd_crate_name.clone(),
     )?;
     Ok(krate)
 }

source/vir/src/ast_util.rs

@@ -287,12 +287,12 @@ pub fn set_path_as_rust_name(path: &Path, friendly: &Path) {
     }
 }
 
-pub fn get_path_as_rust_names_for_krate(krate: &Option<Ident>) -> Vec<(Path, String)> {
+pub fn get_path_as_rust_names_for_krate(krate: &Ident) -> Vec<(Path, String)> {
     let mut v: Vec<(Path, String)> = Vec::new();
     if let Ok(guard) = PATH_AS_RUST_NAME_MAP.lock() {
         if let Some(map) = &*guard {
             for (path, name) in map {
-                if &path.krate == krate {
+                if &path.krate == &Some(krate.clone()) {
                     v.push((path.clone(), name.clone()));
                 }
             }