From 200b8ebf6627ff6e33d3d28e2141c199788923a7 Mon Sep 17 00:00:00 2001 From: ahuoguo <52595524+ahuoguo@users.noreply.github.com> Date: Wed, 26 Jul 2023 14:36:10 -0400 Subject: [PATCH] Generate error report zip file when verus do not have stdout (#693) * still generate zip file when, verus do not have stdout (json parse will fail when stdout is empty) * refactoring such that every error in creating/parsing json, error report will emit warning and keep going * parse z3 version output * use serde_json::from_value to avoid stringifying and then re-parsing json values --------- Co-authored-by: Andrea Lattuada --- source/Cargo.lock | 1 + source/error_report/Cargo.toml | 1 + source/error_report/src/main.rs | 139 ++++++++++++++++++++++++-------- 3 files changed, 107 insertions(+), 34 deletions(-) diff --git a/source/Cargo.lock b/source/Cargo.lock index 6648ee521f..3f04e664e7 100644 --- a/source/Cargo.lock +++ b/source/Cargo.lock @@ -406,6 +406,7 @@ name = "error_report" version = "0.1.0" dependencies = [ "chrono", + "regex", "serde_json", "toml", "yansi", diff --git a/source/error_report/Cargo.toml b/source/error_report/Cargo.toml index 5c23f60f8c..cd4839d1fb 100644 --- a/source/error_report/Cargo.toml +++ b/source/error_report/Cargo.toml @@ -9,6 +9,7 @@ zip = "0.6.6" chrono = "0.4.26" yansi = "0.5" serde_json = "1.0" +regex = "1" # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html diff --git a/source/error_report/src/main.rs b/source/error_report/src/main.rs index 40f350c076..74466b7606 100644 --- a/source/error_report/src/main.rs +++ b/source/error_report/src/main.rs @@ -1,4 +1,5 @@ use chrono::{prelude::*, DateTime}; +use regex::Regex; use std::time::{Duration, Instant}; use std::{ env, @@ -80,10 +81,18 @@ fn run() -> Result<(), String> { .to_string(), ); - let z3_version_output = - Command::new(z3_path.clone()).arg("--version").output().map_err(|x| { - format!("failed to execute z3 with error message {}, path is at {:?}", x, z3_path) - })?; + let z3_version_output = match Command::new(z3_path.clone()).arg("--version").output() { + Ok(output) => Some(output), + Err(err) => { + eprintln!( + "{}: failed to execute z3 with error message {}, path is at {:?}", + yansi::Paint::yellow("warning"), + err, + z3_path + ); + None + } + }; // mandating --time and --output-json flag, we remove both flags here to prevent passing duplicates to verus if our_args.contains(&"--time".to_string()) || our_args.contains(&"--output-json".to_string()) { @@ -155,31 +164,86 @@ fn run() -> Result<(), String> { fn toml_setup_and_write( args: Vec, - z3_version_output: std::process::Output, + z3_version_output: Option, verus_output: std::process::Output, verus_duration: Duration, ) -> Result<(), String> { - let z3_version = - str::from_utf8(&z3_version_output.stdout).map_err(|x| format!("{}", x))?.to_string(); + let z3_version: Option = if let Some(z3_version_output) = z3_version_output { + let mut z3_version = Map::new(); + let stdout_str = str::from_utf8(&z3_version_output.stdout) + .map_err(|x| format!("z3 version output is not valid utf8 ({})", x))? + .to_string(); + let z3_version_re = Regex::new(r"Z3 version (\d+\.\d+\.\d+) - \d+ bit") + .expect("failed to compile z3 version regex"); + if let Some(captures) = z3_version_re.captures(&stdout_str) { + z3_version.insert("version".into(), Value::String(captures[1].into())); + } else { + eprintln!("{}: failed to parse z3 version stdout", yansi::Paint::yellow("warning"),); + } + z3_version.insert("stdout".into(), Value::String(stdout_str)); + Some(Value::Table(z3_version)) + } else { + None + }; let verus_time = verus_duration.as_secs_f64(); - let stdout_json = - serde_json::from_str::(&String::from_utf8_lossy(&verus_output.stdout)) - .map_err(|x| format!("Could not parse stdout as json with error message: {}", x))?; - - let version_info: toml::Value = serde_json::from_str(&stdout_json["verus"].to_string()) - .map_err(|x| { - format!("failed to parse version info to toml file with error message {}", x) - })?; - - let verification_result: toml::map::Map = - serde_json::from_str(&stdout_json["verification-results"].to_string()).map_err(|x| { - format!("failed to parse verification results with error message {}", x) - })?; - - let stdout_toml_text = serde_json::from_str(&stdout_json.to_string()) - .map_err(|x| format!("failed to parse stdout (json) with error message {}", x))?; + let stdout_string = String::from_utf8_lossy(&verus_output.stdout).to_string(); + + let stdout_json: Option = + match serde_json::from_str::(&stdout_string) { + Ok(json) => Some(json), + Err(err) => { + eprintln!( + "{}: failed to parse stdout to json with error message:\n {}", + yansi::Paint::yellow("warning"), + err + ); + None + } + }; + + let version_info: Option = stdout_json.as_ref().and_then(|stdout_json| { + match serde_json::from_value(stdout_json["verus"].clone()) { + Ok(json) => Some(json), + Err(err) => { + eprintln!( + "{}: failed to parse version info to toml with error message:\n {}", + yansi::Paint::yellow("warning"), + err + ); + None + } + } + }); + + let verification_result: Option = stdout_json.as_ref().and_then(|stdout_json| { + match serde_json::from_value(stdout_json["verification-results"].clone()) { + Ok(json) => Some(json), + Err(err) => { + eprintln!( + "{}: failed to parse verification results to toml with error message:\n {}", + yansi::Paint::yellow("warning"), + err + ); + None + } + } + }); + + let stdout_toml = stdout_json.and_then(|stdout_json| { + match serde_json::from_value::(stdout_json) { + Ok(json) => Some(json), + Err(err) => { + eprintln!( + "{}: failed to convert stdout to toml with error message:\n {}", + yansi::Paint::yellow("warning"), + err + ); + None + } + } + }); let stderr = String::from_utf8_lossy(&verus_output.stderr).to_string(); @@ -189,7 +253,7 @@ fn toml_setup_and_write( version_info, verification_result, verus_time, - stdout_toml_text, + stdout_toml, stderr, )) .map_err(|x| format!("Could not encode TOML value with error message: {}", x))?; @@ -204,25 +268,31 @@ fn toml_setup_and_write( // the command-line arguments, versions, rough time info, and verus output. fn create_toml( args: Vec, - z3_version: String, - verus_version: toml::Value, - verification_result: toml::map::Map, + z3_version: Option, + verus_version: Option, + verification_results: Option, verus_time: f64, - stdout: toml::Value, + stdout: Option, stderr: String, ) -> Value { let mut command_line_arguments = Map::new(); command_line_arguments.insert("args".to_string(), Value::String(args.join(" "))); let mut versions = Map::new(); - versions.insert("z3-version".to_string(), Value::String(z3_version)); - versions.insert("verus-version".to_string(), verus_version); + if let Some(z3_version) = z3_version { + versions.insert("z3".to_string(), z3_version); + } + if let Some(verus_version) = verus_version { + versions.insert("verus".to_string(), verus_version); + } let mut time = Map::new(); time.insert("verus-time".to_string(), Value::Float(verus_time)); let mut output = Map::new(); - output.insert("stdout".to_string(), stdout); + if let Some(stdout) = stdout { + output.insert("stdout".to_string(), stdout); + } output.insert("stderr".to_string(), Value::String(stderr)); let mut map = Map::new(); @@ -230,12 +300,14 @@ fn create_toml( "title".to_string(), Value::String("Error report file - details and dependencies".to_string()), ); - map.insert("report-schema-version".into(), Value::String("1".to_string())); + map.insert("report-schema-version".into(), Value::String("1.1".to_string())); map.insert("command-line-arguments".into(), Value::Table(command_line_arguments)); map.insert("verus-time".into(), Value::Table(time)); map.insert("versions".into(), Value::Table(versions)); map.insert("verus-output".into(), Value::Table(output)); - map.insert("verification-results".into(), Value::Table(verification_result)); + if let Some(verification_results) = verification_results { + map.insert("verification-results".into(), verification_results); + } Value::Table(map) } @@ -260,7 +332,6 @@ pub fn zip_setup(dep_file_name: String) -> Result { // parse the .d file and returns a vector of files names required to generate the crate fn get_dependencies(dep_file_path: &std::path::Path) -> Result, String> { - // update to better error message let file = File::open(dep_file_path) .map_err(|x| format!("{}, dependency file name: {:?}", x, dep_file_path))?; let mut reader = BufReader::new(file);