Refactor for clarity

verus-lang · Jun 4, 2024 · cb818f0 · cb818f0
1 parent 2bcb3bb
commit cb818f0
Show file tree

Hide file tree

Showing 2 changed files with 25 additions and 24 deletions.
diff --git a/source/cargo-verus/src/main.rs b/source/cargo-verus/src/main.rs
@@ -54,6 +54,17 @@ fn show_version() {
     println!("{version_info}");
 }
 
+fn process(args: &[String]) -> Result<(), i32> {
+    let cmd = VerusCmd::new(args);
+
+    let mut cmd = cmd.into_std_cmd();
+
+    let exit_status =
+        cmd.spawn().expect("could not run cargo").wait().expect("failed to wait for cargo?");
+
+    if exit_status.success() { Ok(()) } else { Err(exit_status.code().unwrap_or(-1)) }
+}
+
 struct VerusCmd {
     cargo_subcommand: CargoSubcommand,
     cargo_args: Vec<String>,
@@ -130,20 +141,20 @@ impl VerusCmd {
     }
 
     fn into_std_cmd(self) -> Command {
-        let common_verus_driver_args =
-            pack_verus_driver_args_for_env(self.common_verus_driver_args.iter());
-
         let mut cmd = Command::new(env::var("CARGO").unwrap_or("cargo".into()));
 
-        cmd.env("RUSTC_WRAPPER", checked_verus_driver_path())
-            .arg(self.cargo_subcommand.to_arg().to_owned())
-            .args(&self.cargo_args);
+        cmd.arg(self.cargo_subcommand.to_arg().to_owned()).args(&self.cargo_args);
+
+        cmd.env("RUSTC_WRAPPER", checked_verus_driver_path());
 
         cmd.env("__VERUS_DRIVER_VIA_CARGO__", "1");
 
         // See https://github.com/rust-lang/cargo/blob/94aa7fb1321545bbe922a87cb11f5f4559e3be63/src/cargo/core/compiler/fingerprint/mod.rs#L71
         cmd.env("__CARGO_DEFAULT_LIB_METADATA", "verus");
 
+        let common_verus_driver_args =
+            pack_verus_driver_args_for_env(self.common_verus_driver_args.iter());
+
         if !common_verus_driver_args.is_empty() {
             cmd.env("__VERUS_DRIVER_ARGS__", common_verus_driver_args);
         }
@@ -211,17 +222,6 @@ impl VerusCmd {
     }
 }
 
-fn process(args: &[String]) -> Result<(), i32> {
-    let cmd = VerusCmd::new(args);
-
-    let mut cmd = cmd.into_std_cmd();
-
-    let exit_status =
-        cmd.spawn().expect("could not run cargo").wait().expect("failed to wait for cargo?");
-
-    if exit_status.success() { Ok(()) } else { Err(exit_status.code().unwrap_or(-1)) }
-}
-
 fn filter_args(
     mut orig_args: impl Iterator<Item = impl AsRef<str>>,
     standalone_flags: &[impl AsRef<str>],

diff --git a/source/verus-driver/src/main.rs b/source/verus-driver/src/main.rs
@@ -13,6 +13,7 @@ use std::io::Read;
 use std::mem;
 use std::path::{Path, PathBuf};
 use std::process::exit;
+use std::sync::atomic::AtomicBool;
 use std::sync::Arc;
 
 use rustc_driver::{Callbacks, RunCompiler};
@@ -48,7 +49,7 @@ pub fn main() {
             handler.note(format!("Verus version: {version_info}"));
         })
     } else {
-        std::sync::Arc::new(std::sync::atomic::AtomicBool::new(false))
+        Arc::new(AtomicBool::new(false))
     };
 
     exit(rustc_driver::catch_with_exit_code(move || {
@@ -218,6 +219,12 @@ pub fn main() {
             }
         }
 
+        let mut import_deps_if_present = parsed_verus_driver_inner_args
+            .import_dep_if_present
+            .iter()
+            .cloned()
+            .collect::<BTreeSet<_>>();
+
         let mut externs = BTreeMap::<String, Vec<PathBuf>>::new();
 
         for (key, entry) in orig_rustc_opts.externs.iter() {
@@ -233,12 +240,6 @@ pub fn main() {
             }
         }
 
-        let mut import_deps_if_present = parsed_verus_driver_inner_args
-            .import_dep_if_present
-            .iter()
-            .cloned()
-            .collect::<BTreeSet<_>>();
-
         if let Some(verus_sysroot) = parsed_verus_driver_inner_args
             .verus_sysroot
             .or_else(|| dep_tracker.get_env("VERUS_SYSROOT"))