Skip to content

Commit

Permalink
verus-driver: Improve error handling
Browse files Browse the repository at this point in the history
Using 'rustc_session::EarlyDiagCtxt'.
  • Loading branch information
nspin committed Jun 4, 2024
1 parent c9670ef commit c1d8b98
Show file tree
Hide file tree
Showing 3 changed files with 58 additions and 32 deletions.
7 changes: 4 additions & 3 deletions source/verus-driver/src/dep_tracker.rs
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,9 @@ impl DepTracker {
let val = match env::var(var) {
Ok(s) => Some(s),
Err(VarError::NotPresent) => None,
Err(VarError::NotUnicode(_)) => panic!(), // TODO
Err(VarError::NotUnicode(invalid)) => panic!(
"the value of environment variable {var:?} is not value unicode: {invalid:?}"
),
};
self.env.insert(var.to_owned(), val.clone());
val
Expand Down Expand Up @@ -55,8 +57,7 @@ impl<T: AsRef<DepTracker> + Clone + Send + 'static> ConfigCallback for DepTracke
}
for path in dep_tracker.as_ref().files.iter() {
psess.file_depinfo.get_mut().insert(Symbol::intern(
path.to_str()
.unwrap_or_else(|| panic!("{} is not valid unicode", path.display())),
path.to_str().unwrap_or_else(|| panic!("path {path:?} is not valid unicode")),
));
}
}));
Expand Down
56 changes: 39 additions & 17 deletions source/verus-driver/src/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -58,9 +58,11 @@ pub fn main() {
if orig_args.get(1).map(String::as_str) == Some(verifier::LIFETIME_DRIVER_ARG) {
orig_args.remove(1);
let mut buffer = String::new();
std::io::stdin().read_to_string(&mut buffer).expect("failed to read stdin");
std::io::stdin().read_to_string(&mut buffer).unwrap_or_else(|err| {
early_dcx.early_error(format!("failed to read stdin: {err:?}"))
});
verifier::lifetime_rustc_driver(&orig_args, buffer);
exit(0);
return Ok(());
}

// Make "verus-driver --rustc" work like a subcommand that passes further args to "rustc"
Expand Down Expand Up @@ -179,29 +181,28 @@ pub fn main() {
let orig_rustc_args = all_args;

// HACK: clap expects exe in first arg
verus_driver_inner_args.insert(0, "dummy".to_owned());
verus_driver_inner_args.insert(0, "verus-driver-inner".to_owned());

let parsed_verus_driver_inner_args = VerusDriverInnerArgs::try_parse_from(
&verus_driver_inner_args,
)
.unwrap_or_else(|err| {
panic!(
let parsed_verus_driver_inner_args =
VerusDriverInnerArgs::try_parse_from(&verus_driver_inner_args).unwrap_or_else(|err| {
early_dcx.early_error(format!(
"failed to parse verus driver inner args from {verus_driver_inner_args:?}: {err}"
)
});
))
});

if parsed_verus_driver_inner_args.help {
display_help();
exit(0);
return Ok(());
}

if parsed_verus_driver_inner_args.version {
let version_info = rustc_tools_util::get_version_info!();
println!("{version_info}");
exit(0);
return Ok(());
}

let orig_rustc_opts = probe_config(&orig_rustc_args, |config| config.opts.clone()).unwrap();
let orig_rustc_opts = probe_config(&orig_rustc_args, |config| config.opts.clone())
.unwrap_or_else(|_| early_dcx.early_error("failed to parse rustc args"));

let mut rustc_args = orig_rustc_args;

Expand Down Expand Up @@ -246,9 +247,24 @@ pub fn main() {
{
let mut add_extern = |key: &str, pattern: String| {
let path = {
let report_missing_or_corrupt = || {
early_dcx
.early_error("verus sysroot appears to be either missing or corrupt");
};
let mut paths = glob::glob(pattern.as_str()).unwrap();
let path = paths.next().unwrap().unwrap();
assert!(paths.next().is_none());
let path = paths
.next()
.unwrap_or_else(|| {
report_missing_or_corrupt();
unreachable!()
})
.unwrap_or_else(|err| {
early_dcx
.early_error(format!("failed to traverse verus sysroot: {err:?}"))
});
if paths.next().is_some() {
report_missing_or_corrupt();
}
path
};
rustc_args.push(format!("--extern={key}={}", path.display()));
Expand Down Expand Up @@ -282,7 +298,7 @@ pub fn main() {
}
}
if !found {
panic!("could not find .vir file for '{key}'");
early_dcx.early_error(format!("could not find .vir file for '{key}'"));
}
}
}
Expand Down Expand Up @@ -327,7 +343,13 @@ pub fn main() {
.run()
};

verifier::run(verus_inner_args.into_iter(), &rustc_args, mk_file_loader, compiler_runner)
verifier::run(
&early_dcx,
verus_inner_args.into_iter(),
&rustc_args,
mk_file_loader,
compiler_runner,
)
}))
}

Expand Down
27 changes: 15 additions & 12 deletions source/verus-driver/src/verifier.rs
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
use std::time::Instant;

use rustc_driver::Callbacks;
use rustc_session::EarlyDiagCtxt;
use rustc_span::source_map::FileLoader;
use rustc_span::ErrorGuaranteed;

Expand Down Expand Up @@ -31,6 +32,7 @@ where
}

pub(crate) fn run<'a, T, U, V>(
early_dcx: &EarlyDiagCtxt,
verus_inner_args: impl Iterator<Item = String>,
rustc_args: &[String],
mk_file_loader: U,
Expand All @@ -41,22 +43,23 @@ where
U: Fn() -> T,
V: CompilerRunner,
{
let program_name_for_config = "TODO";
// HACK
let program_name_for_config = "verus-inner";

let (parsed_verus_inner_args, unparsed) = rust_verify::config::parse_args_with_imports(
&program_name_for_config.to_owned(),
verus_inner_args,
None,
);

assert!(
unparsed.len() == 1 && unparsed[0] == program_name_for_config,
"leftovers after parsing --verus-arg=<..> args: {:?}",
unparsed
);
if unparsed.len() != 1 || unparsed[0] != program_name_for_config {
early_dcx
.early_error(format!("leftovers after parsing --verus-arg=<..> args: {:?}", unparsed));
}

// TODO
assert!(!parsed_verus_inner_args.version);
if parsed_verus_inner_args.version {
early_dcx.early_error("--verus-inner-arg=--version is not supported");
}

let is_core = parsed_verus_inner_args.vstd == rust_verify::config::Vstd::IsCore;

Expand All @@ -80,18 +83,18 @@ where
let VerifierCallbacksEraseMacro { verifier, .. } = verifier_callbacks;

if !verifier.args.output_json && !verifier.encountered_vir_error {
eprint!(
let mut s = format!(
"verification results:: {} verified, {} errors",
verifier.count_verified, verifier.count_errors,
);
if !is_verifying_entire_crate(&verifier) {
eprint!(" (partial verification with `--verify-*`)");
s.push_str(" (partial verification with `--verify-*`)");
}
eprintln!();
early_dcx.early_note(s);
}

if status.is_err() || verifier.encountered_vir_error {
panic!("verification failed");
early_dcx.early_error("verification failed");
}

if !verifier.args.compile && verifier.args.no_lifetime {
Expand Down

0 comments on commit c1d8b98

Please sign in to comment.