[rust_verify] fix: skip codegen when --compile is not set (#2509)

Author: mkovaxx

source/rust_verify/src/driver.rs

@@ -115,6 +115,7 @@ This would avoid the complex interleaving above and avoid needing to use lifetim
 for all functions (it would only be needed for functions with tracked data in proof code).
 */
 struct CompilerCallbacksEraseMacro {
+    pub do_compile: bool,
     pub override_stability: bool,
 }
 
@@ -136,6 +137,18 @@ impl rustc_driver::Callbacks for CompilerCallbacksEraseMacro {
             });
         }
     }
+
+    fn after_analysis<'tcx>(
+        &mut self,
+        _compiler: &rustc_interface::interface::Compiler,
+        _tcx: TyCtxt<'tcx>,
+    ) -> rustc_driver::Compilation {
+        if self.do_compile {
+            rustc_driver::Compilation::Continue
+        } else {
+            rustc_driver::Compilation::Stop
+        }
+    }
 }
 
 /// Captures the verification and compilation time
@@ -153,9 +166,11 @@ pub struct Stats {
 
 pub(crate) fn run_with_erase_macro_compile(
     mut rustc_args: Vec<String>,
+    do_compile: bool,
     vstd: Vstd,
 ) -> Result<(), ()> {
     let mut callbacks = CompilerCallbacksEraseMacro {
+        do_compile,
         override_stability: matches!(vstd, Vstd::IsCore | Vstd::ImportedViaCore),
     };
     rustc_args.extend(["--cfg", "verus_only", "--cfg", "verus_keep_ghost"].map(|s| s.to_string()));
@@ -320,7 +335,8 @@ pub fn run(
         if !verifier.compile && (verifier.args.no_erasure_check || verifier.args.no_lifetime) {
             Ok(())
         } else {
-            run_with_erase_macro_compile(rustc_args, verifier.args.vstd)
+            let do_compile = verifier.compile || verifier.via_cargo_args.is_some();
+            run_with_erase_macro_compile(rustc_args, do_compile, verifier.args.vstd)
         };
 
     let time2 = Instant::now();

source/rust_verify_test/tests/common/mod.rs

@@ -443,6 +443,50 @@ pub fn run_verus(
     run
 }
 
+pub fn run_verus_raw(args: &[&str], dir: &std::path::Path) -> std::process::Output {
+    if std::env::var("VERUS_IN_VARGO").is_err() {
+        panic!("not running in vargo, read the README for instructions");
+    }
+    let exe = if cfg!(target_os = "windows") { ".exe" } else { "" };
+
+    let current_exe = std::env::current_exe().unwrap();
+    let deps_path = current_exe.parent().unwrap();
+    let target_path = deps_path.parent().unwrap();
+    let profile = target_path.file_name().unwrap().to_str().unwrap();
+    let verus_target_path = target_path
+        .ancestors()
+        .nth(2)
+        .expect("expected path to have at least two parents")
+        .join("target-verus")
+        .join(profile);
+    let bin = verus_target_path.join(format!("rust_verify{exe}"));
+
+    let z3 = std::env::var("VERUS_Z3_PATH")
+        .map(|p| {
+            let p = std::path::PathBuf::from(p);
+            if p.is_relative() { std::path::PathBuf::from("..").join(p) } else { p }
+        })
+        .unwrap_or({
+            if cfg!(target_os = "windows") {
+                std::path::PathBuf::from("..\\z3.exe")
+            } else {
+                std::path::PathBuf::from("../z3")
+            }
+        });
+    let z3 = path::absolute(z3).expect("Failed to find absolute path for Z3 executable");
+
+    std::process::Command::new(bin)
+        .current_dir(dir)
+        .env("VERUS_Z3_PATH", z3)
+        .args(args)
+        .stdout(std::process::Stdio::piped())
+        .stderr(std::process::Stdio::piped())
+        .spawn()
+        .expect("could not execute verus")
+        .wait_with_output()
+        .expect("raw verus wait failed")
+}
+
 pub fn run_cargo_verus(args: &[&str], dir: &std::path::Path) -> std::process::Output {
     run_cargo_verus_with_target(args, dir, &dir.join("target"))
 }

source/rust_verify_test/tests/compile.rs

@@ -0,0 +1,32 @@
+#![feature(rustc_private)]
+#[macro_use]
+mod common;
+use common::*;
+
+use tempfile::TempDir;
+
+#[test]
+fn compile_flag_produces_binary() {
+    let tempdir = TempDir::new().expect("temp dir");
+    let entry_file = tempdir.path().join("test.rs");
+    let code = format!("{}\n{}\nverus! {{ fn main() {{}} }}\n", FEATURE_PRELUDE, USE_PRELUDE);
+    std::fs::write(&entry_file, code).expect("write source file");
+
+    let output = run_verus_raw(&["--compile", entry_file.to_str().unwrap()], tempdir.path());
+    let exe_name = if cfg!(target_os = "windows") { "test.exe" } else { "test" };
+    assert!(output.status.success(), "verus failed:\n{}", String::from_utf8_lossy(&output.stderr));
+    assert!(tempdir.path().join(exe_name).exists());
+}
+
+#[test]
+fn no_compile_flag_does_not_produce_binary() {
+    let tempdir = TempDir::new().expect("temp dir");
+    let entry_file = tempdir.path().join("test.rs");
+    let code = format!("{}\n{}\nverus! {{ fn main() {{}} }}\n", FEATURE_PRELUDE, USE_PRELUDE);
+    std::fs::write(&entry_file, code).expect("write source file");
+
+    let output = run_verus_raw(&[entry_file.to_str().unwrap()], tempdir.path());
+    let exe_name = if cfg!(target_os = "windows") { "test.exe" } else { "test" };
+    assert!(output.status.success(), "verus failed:\n{}", String::from_utf8_lossy(&output.stderr));
+    assert!(!tempdir.path().join(exe_name).exists());
+}