From 963d9d5bdb4362fdfdf63eff58ba519b0d17db5a Mon Sep 17 00:00:00 2001 From: Nick Spinale Date: Tue, 4 Jun 2024 07:33:45 +0000 Subject: [PATCH] verus-driver: Improve error handling Using 'rustc_session::EarlyDiagCtxt'. --- source/verus-driver/src/dep_tracker.rs | 7 ++-- source/verus-driver/src/main.rs | 56 ++++++++++++++++++-------- source/verus-driver/src/verifier.rs | 27 +++++++------ 3 files changed, 58 insertions(+), 32 deletions(-) diff --git a/source/verus-driver/src/dep_tracker.rs b/source/verus-driver/src/dep_tracker.rs index 83f5e51d31..dc7dbaefe1 100644 --- a/source/verus-driver/src/dep_tracker.rs +++ b/source/verus-driver/src/dep_tracker.rs @@ -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 @@ -55,8 +57,7 @@ impl + 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")), )); } })); diff --git a/source/verus-driver/src/main.rs b/source/verus-driver/src/main.rs index 01373f33b8..bc5d3c7329 100644 --- a/source/verus-driver/src/main.rs +++ b/source/verus-driver/src/main.rs @@ -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" @@ -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; @@ -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())); @@ -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}'")); } } } @@ -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, + ) })) } diff --git a/source/verus-driver/src/verifier.rs b/source/verus-driver/src/verifier.rs index c04859d61e..e34dd19e5b 100644 --- a/source/verus-driver/src/verifier.rs +++ b/source/verus-driver/src/verifier.rs @@ -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; @@ -31,6 +32,7 @@ where } pub(crate) fn run<'a, T, U, V>( + early_dcx: &EarlyDiagCtxt, verus_inner_args: impl Iterator, rustc_args: &[String], mk_file_loader: U, @@ -41,7 +43,8 @@ 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(), @@ -49,14 +52,14 @@ where 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; @@ -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 {