Something went wrong. Try again.
forked from verus-lang/verus
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171#![feature(rustc_private)]
use yansi::Paint;
extern crate rustc_driver;
// For diagnostics when something goes wrong, try "cargo build -vv"
// the build script’s current directory is the source directory of the build script’s package
// path to vstd.rs relative to our directory (source/vstd)const VSTD_RS_PATH: &str = "vstd/vstd.rs";// name of generated veruslib.vir in targetconst VSTD_VIR: &str = "vstd.vir";
fn log_command(cmd: &std::process::Command) { eprintln!("{}", format!("vstd_build running: {:?}", cmd).magenta());}
fn main() { if std::env::var("VERUS_IN_VARGO").is_err() { panic!("not running in vargo, read the README for instructions"); }
let mut args = std::env::args(); args.next().expect("executable name"); let verus_target_path = std::path::PathBuf::from(args.next().expect("missing verus target path"));
let mut release = false; let mut no_verify = false; let mut no_std = false; let mut no_alloc = false; let mut verbose = false; let mut trace = false; let mut log_all = false; let mut no_lifetime = false; let mut no_trait_conflicts = false; let mut expand_errors = false; let mut no_solver_version_check = false; for arg in args { if arg == "--release" { release = true; } else if arg == "--no-verify" { no_verify = true; } else if arg == "--verbose" { verbose = true; } else if arg == "--no-std" { no_std = true; } else if arg == "--no-alloc" { no_alloc = true; } else if arg == "--trace" { trace = true; } else if arg == "--log-all" { log_all = true; } else if arg == "--no-lifetime" { no_lifetime = true; } else if arg == "--no-trait-conflicts" { no_trait_conflicts = true; } else if arg == "--expand-errors" { expand_errors = true; } else if arg == "--no-solver-version-check" { no_solver_version_check = true; } else { panic!("unexpected argument: {:}", arg) } }
if !no_std && no_alloc { panic!("--no-alloc must be specified along with --no-std"); }
#[cfg(target_os = "macos")] let (pre, dl) = ("lib", "dylib");
#[cfg(target_os = "linux")] let (pre, dl) = ("lib", "so");
#[cfg(target_os = "windows")] let (pre, dl) = ("", "dll");
let lib_builtin_path = verus_target_path.join("libverus_builtin.rlib"); assert!(lib_builtin_path.exists()); let lib_builtin_path = lib_builtin_path.to_str().unwrap(); let lib_builtin_macros_path = verus_target_path.join(format!("{}verus_builtin_macros.{}", pre, dl)); assert!(lib_builtin_macros_path.exists()); let lib_builtin_macros_path = lib_builtin_macros_path.to_str().unwrap(); let lib_state_machines_macros_path = verus_target_path.join(format!("{}verus_state_machines_macros.{}", pre, dl)); assert!(lib_state_machines_macros_path.exists()); let lib_state_machines_macros_path = lib_state_machines_macros_path.to_str().unwrap();
if !std::env::var("VERUS_Z3_PATH").is_ok() { std::env::set_var("VERUS_Z3_PATH", if cfg!(windows) { ".\\z3.exe" } else { "./z3" }); }
let mut child_args: Vec<String> = vec![ "--internal-test-mode".to_string(), "--extern".to_string(), format!("verus_builtin={lib_builtin_path}"), "--extern".to_string(), format!("verus_builtin_macros={lib_builtin_macros_path}"), "--extern".to_string(), format!("verus_state_machines_macros={lib_state_machines_macros_path}"), "--crate-type=lib".to_string(), "--export".to_string(), verus_target_path.join(VSTD_VIR).to_str().unwrap().to_string(), "--out-dir".to_string(), verus_target_path.to_str().expect("invalid path").to_string(), "--multiple-errors".to_string(), "2".to_string(), "--is-vstd".to_string(), "--compile".to_string(), ]; if no_verify { child_args.push("--no-verify".to_string()); child_args.push("--no-lifetime".to_string()); child_args.push("--no-trait-conflicts".to_string()); } if trace { child_args.push("--trace".to_string()); } if log_all { child_args.push("--log-all".to_string()); } if no_lifetime { child_args.push("--no-lifetime".to_string()); } if no_trait_conflicts { child_args.push("--no-trait-conflicts".to_string()); } if expand_errors { child_args.push("--expand-errors".to_string()); } if no_solver_version_check { child_args.push("-V".to_string()); child_args.push("no-solver-version-check".to_string()); } if release { child_args.push("-C".to_string()); child_args.push("opt-level=3".to_string()); } if !no_std { child_args.push("--cfg".to_string()); child_args.push("feature=\"std\"".to_string()); } if !no_alloc { child_args.push("--cfg".to_string()); child_args.push("feature=\"alloc\"".to_string()); } child_args.push(VSTD_RS_PATH.to_string());
let cmd = verus_target_path.join("rust_verify"); let mut child = std::process::Command::new(cmd); child.env("RUST_MIN_STACK", (10 * 1024 * 1024).to_string()); child.env("VSTD_KIND", "IsVstd"); child.args(&child_args[..]);
if verbose { log_command(&child); }
let mut child = child.spawn().expect("could not execute lifetime rustc process"); let result = child.wait().expect("vstd verus wait failed"); if !result.success() { let code = result.code(); panic!("vstd build failed with exit code {:?}", code); }}