From f45287559619d6fad25b5789c16b7386c51c5ffe Mon Sep 17 00:00:00 2001 From: Ranadeep Biswas Date: Mon, 23 Aug 2021 14:07:00 +0200 Subject: [PATCH] From traits for crate Error (#68) * impl From for Error * catch error message from TLC (#52) --- modelator/src/cache/mod.rs | 6 +- modelator/src/cli/mod.rs | 8 +-- modelator/src/error.rs | 12 ++-- modelator/src/jar.rs | 10 ++-- modelator/src/lib.rs | 12 ++-- modelator/src/module/apalache/mod.rs | 6 +- modelator/src/module/tla/json/mod.rs | 2 +- modelator/src/module/tla/mod.rs | 8 +-- modelator/src/module/tlc/mod.rs | 4 +- modelator/src/module/tlc/output.rs | 90 +++++++++++++++++++++++++--- modelator/src/util.rs | 14 ++--- 11 files changed, 122 insertions(+), 50 deletions(-) diff --git a/modelator/src/cache/mod.rs b/modelator/src/cache/mod.rs index 05a317d3..b3e355ee 100644 --- a/modelator/src/cache/mod.rs +++ b/modelator/src/cache/mod.rs @@ -17,7 +17,7 @@ impl Cache { pub(crate) fn new(options: &Options) -> Result { // create cache dir (if it doesn't exist) let cache_dir = options.dir.join("cache"); - std::fs::create_dir_all(&cache_dir).map_err(Error::io)?; + std::fs::create_dir_all(&cache_dir)?; // read files the cache directory let cached_keys = crate::util::read_dir(&cache_dir)?; @@ -33,7 +33,7 @@ impl Cache { let value = if self.cached_keys.contains(key) { // if this key is cached, read it from disk let path = self.key_path(key); - let value = std::fs::read_to_string(path).map_err(Error::io)?; + let value = std::fs::read_to_string(path)?; Some(value) } else { None @@ -51,7 +51,7 @@ impl Cache { // write the value associated with this key to disk let path = self.key_path(&key); - std::fs::write(path, value).map_err(Error::io)?; + std::fs::write(path, value)?; // mark the key as cached self.cached_keys.insert(key); diff --git a/modelator/src/cli/mod.rs b/modelator/src/cli/mod.rs index 5c8622ee..edb3dad5 100644 --- a/modelator/src/cli/mod.rs +++ b/modelator/src/cli/mod.rs @@ -127,9 +127,7 @@ impl TlaMethods { if !tla_trace_file.is_file() { return Err(Error::FileNotFound(tla_trace_file.to_path_buf())); } - let tla_trace = std::fs::read_to_string(&tla_trace_file) - .map_err(Error::io)? - .parse()?; + let tla_trace = std::fs::read_to_string(&tla_trace_file)?.parse()?; let json_trace = crate::module::Tla::tla_trace_to_json_trace(tla_trace)?; tracing::debug!("Tla::tla_trace_to_json_trace output {}", json_trace); @@ -210,7 +208,7 @@ fn generated_tests(tests: Vec<(TlaFile, TlaConfigFile)>) -> Result Result { let path = Path::new("trace.tla").to_path_buf(); - std::fs::write(&path, format!("{}", tla_trace)).map_err(Error::io)?; + std::fs::write(&path, format!("{}", tla_trace))?; Ok(json!({ "tla_trace_file": crate::util::absolute_path(&path), })) @@ -218,7 +216,7 @@ fn save_tla_trace(tla_trace: TlaTrace) -> Result { fn save_json_trace(json_trace: JsonTrace) -> Result { let path = Path::new("trace.json").to_path_buf(); - std::fs::write(&path, format!("{}", json_trace)).map_err(Error::io)?; + std::fs::write(&path, format!("{}", json_trace))?; Ok(json!({ "json_trace_file": crate::util::absolute_path(&path), })) diff --git a/modelator/src/error.rs b/modelator/src/error.rs index fcdc3b62..46515d3d 100644 --- a/modelator/src/error.rs +++ b/modelator/src/error.rs @@ -63,16 +63,20 @@ pub enum Error { JsonParseError(String), } -impl Error { - pub(crate) fn io(err: std::io::Error) -> Error { +impl From for Error { + fn from(err: std::io::Error) -> Self { Error::IO(err.to_string()) } +} - pub(crate) fn ureq(err: ureq::Error) -> Error { +impl From for Error { + fn from(err: ureq::Error) -> Self { Error::Ureq(err.to_string()) } +} - pub(crate) fn nom(err: nom::Err>) -> Error { +impl From>> for Error { + fn from(err: nom::Err>) -> Self { Error::Nom(err.to_string()) } } diff --git a/modelator/src/jar.rs b/modelator/src/jar.rs index 2fa1679f..bb8c1da9 100644 --- a/modelator/src/jar.rs +++ b/modelator/src/jar.rs @@ -57,13 +57,13 @@ impl Jar { let path = self.path(&modelator_dir); // download the jar - let response = ureq::get(&self.link()).call().map_err(Error::ureq)?; + let response = ureq::get(&self.link()).call()?; let mut reader = response.into_reader(); // write jar bytes to the file - let file = std::fs::File::create(path).map_err(Error::io)?; + let file = std::fs::File::create(path)?; let mut file_writer = std::io::BufWriter::new(file); - std::io::copy(&mut reader, &mut file_writer).map_err(Error::io)?; + std::io::copy(&mut reader, &mut file_writer)?; Ok(()) } @@ -99,8 +99,8 @@ pub(crate) fn download_jars>(modelator_dir: P) -> Result<(), Erro eprintln!("[modelator] Checksum of downloaded jars does not match the expected. Will try again!"); // delete modelator dir and create it again - std::fs::remove_dir_all(&modelator_dir).map_err(Error::io)?; - std::fs::create_dir(&modelator_dir).map_err(Error::io)?; + std::fs::remove_dir_all(&modelator_dir)?; + std::fs::create_dir(&modelator_dir)?; // try to download jars again return download_jars(modelator_dir); diff --git a/modelator/src/lib.rs b/modelator/src/lib.rs index 2680746a..5bb495eb 100644 --- a/modelator/src/lib.rs +++ b/modelator/src/lib.rs @@ -91,13 +91,13 @@ pub fn traces>( setup(options)?; // create a temporary directory, and copy TLA+ files there - let dir = tempdir().map_err(Error::io)?; + let dir = tempdir()?; let tla_tests_file = util::copy_files_into("tla", tla_tests_file, dir.path())?; let tla_config_file = util::copy_files_into("cfg", tla_config_file, dir.path())?; // save the current, and change to the temporary directory - let current_dir = env::current_dir().map_err(Error::io)?; - env::set_current_dir(dir.path()).map_err(Error::io)?; + let current_dir = env::current_dir()?; + env::set_current_dir(dir.path())?; // generate tla tests use std::convert::TryFrom; @@ -119,9 +119,9 @@ pub fn traces>( .collect::, _>>()?; // cleanup everything by removing the temporary directory - dir.close().map_err(Error::io)?; + dir.close()?; // restore the current directory - env::set_current_dir(current_dir).map_err(Error::io)?; + env::set_current_dir(current_dir)?; // convert each tla trace to json traces @@ -380,7 +380,7 @@ pub(crate) fn setup(options: &Options) -> Result<(), Error> { // create modelator dir (if it doens't already exist) if !options.dir.as_path().is_dir() { - std::fs::create_dir_all(&options.dir).map_err(Error::io)?; + std::fs::create_dir_all(&options.dir)?; } // download missing jars diff --git a/modelator/src/module/apalache/mod.rs b/modelator/src/module/apalache/mod.rs index d9ccf8e7..fe054822 100644 --- a/modelator/src/module/apalache/mod.rs +++ b/modelator/src/module/apalache/mod.rs @@ -65,7 +65,7 @@ impl Apalache { // convert apalache counterexample to a trace let counterexample_path = Path::new("counterexample.tla"); if counterexample_path.is_file() { - let counterexample = std::fs::read_to_string(counterexample_path).map_err(Error::io)?; + let counterexample = std::fs::read_to_string(counterexample_path)?; tracing::debug!("Apalache counterexample:\n{}", counterexample); let trace = counterexample::parse(counterexample)?; @@ -128,7 +128,7 @@ impl Apalache { fn run_apalache(mut cmd: Command, options: &Options) -> Result { // start apalache // TODO: add timeout - let output = cmd.output().map_err(Error::io)?; + let output = cmd.output()?; // get apalache stdout and stderr let stdout = crate::util::cmd_output_to_string(&output.stdout); @@ -141,7 +141,7 @@ fn run_apalache(mut cmd: Command, options: &Options) -> Result { // apalache writes all its output to the stdout // save apalache log - std::fs::write(&options.model_checker_options.log, &stdout).map_err(Error::io)?; + std::fs::write(&options.model_checker_options.log, &stdout)?; // check if a failure has occurred if stdout.contains("EXITCODE: ERROR") { diff --git a/modelator/src/module/tla/json/mod.rs b/modelator/src/module/tla/json/mod.rs index adbc361b..26e0879b 100644 --- a/modelator/src/module/tla/json/mod.rs +++ b/modelator/src/module/tla/json/mod.rs @@ -13,5 +13,5 @@ pub(crate) fn state_to_json(state: &str) -> Result { ); value }) - .map_err(Error::nom) + .map_err(Into::into) } diff --git a/modelator/src/module/tla/mod.rs b/modelator/src/module/tla/mod.rs index e5de1e63..c99a62d7 100644 --- a/modelator/src/module/tla/mod.rs +++ b/modelator/src/module/tla/mod.rs @@ -100,7 +100,7 @@ impl Tla { } fn extract_test_names(tla_test_file: &TlaFile) -> Result, Error> { - let content = std::fs::read_to_string(tla_test_file.path()).map_err(Error::io)?; + let content = std::fs::read_to_string(tla_test_file.path())?; let test_names = content .lines() .filter_map(|line| { @@ -150,11 +150,11 @@ fn generate_test( // write test module to test module file let test_module_file = tla_tests_dir.join(format!("{}.tla", test_module_name)); - std::fs::write(&test_module_file, test_module).map_err(Error::io)?; + std::fs::write(&test_module_file, test_module)?; // write test config to test config file let test_config_file = tla_tests_dir.join(format!("{}.cfg", test_module_name)); - std::fs::write(&test_config_file, test_config).map_err(Error::io)?; + std::fs::write(&test_config_file, test_config)?; // create tla file and tla config file use std::convert::TryFrom; @@ -184,7 +184,7 @@ EXTENDS {} } fn generate_test_config(tla_config_file: &TlaConfigFile, invariant: &str) -> Result { - let tla_config = std::fs::read_to_string(tla_config_file.path()).map_err(Error::io)?; + let tla_config = std::fs::read_to_string(tla_config_file.path())?; Ok(format!( r#" {} diff --git a/modelator/src/module/tlc/mod.rs b/modelator/src/module/tlc/mod.rs index 79d26b39..7182aa60 100644 --- a/modelator/src/module/tlc/mod.rs +++ b/modelator/src/module/tlc/mod.rs @@ -55,7 +55,7 @@ impl Tlc { // start tlc // TODO: add timeout - let output = cmd.output().map_err(Error::io)?; + let output = cmd.output()?; // get tlc stdout and stderr let stdout = crate::util::cmd_output_to_string(&output.stdout); @@ -69,7 +69,7 @@ impl Tlc { // occurred // save tlc log - std::fs::write(&options.model_checker_options.log, &stdout).map_err(Error::io)?; + std::fs::write(&options.model_checker_options.log, &stdout)?; tracing::debug!( "TLC log written to {}", crate::util::absolute_path(&options.model_checker_options.log) diff --git a/modelator/src/module/tlc/output.rs b/modelator/src/module/tlc/output.rs index e7d37aec..482c94d9 100644 --- a/modelator/src/module/tlc/output.rs +++ b/modelator/src/module/tlc/output.rs @@ -1,23 +1,95 @@ use crate::artifact::tla_trace::{TlaState, TlaTrace}; use crate::{Error, ModelCheckerOptions}; +use std::collections::HashMap; + pub(crate) fn parse(output: String, options: &ModelCheckerOptions) -> Result, Error> { - let mut traces = Vec::new(); - let mut lines = output.lines(); + let mut parsed_output: HashMap>> = HashMap::new(); + + let mut curr_message_id = None; + let mut curr_message = String::new(); + + output.lines().for_each(|line| { + if line.starts_with("@!@!@STARTMSG ") { + // without annotattion + let (code, class) = curr_message_id.take().unwrap_or((0, 0)); + parsed_output + .entry(class) + .or_default() + .entry(code) + .or_default() + .push(curr_message.drain(..).collect()); - while let Some(line) = lines.next() { - // check if found the beginning of the next trace - if line.starts_with("@!@!@ENDMSG 2121 @!@!@") { - if let Some(trace) = parse_trace(&mut lines, options)? { - traces.push(trace); + let (code, class) = line.splitn(3, ' ').nth(1).unwrap().split_once(':').unwrap(); + curr_message_id.insert((code.parse().unwrap(), class.parse().unwrap())); + } else if line.starts_with("@!@!@ENDMSG ") { + let (code, class) = curr_message_id.take().unwrap_or((0, 0)); + parsed_output + .entry(class) + .or_default() + .entry(code) + .or_default() + .push(curr_message.drain(..).collect()); + + let c_code = line.splitn(3, ' ').nth(1).unwrap(); + assert_eq!(code, c_code.parse::().unwrap()); + } else { + curr_message.push_str(line); + curr_message.push('\n'); + } + }); + + if let Some(lines) = parsed_output.get(&4).and_then(|x| x.get(&2217)) { + let mut traces = Vec::new(); + let mut trace = None; + for line in lines { + if line.starts_with("1: ") { + // start of new trace + if let Some(t) = trace.take() { + traces.push(t) + } + trace = Some(TlaTrace::new()); + } + if let Some(t) = trace.as_mut() { + t.add(line.split_once('\n').unwrap().1.into()); } } + // last trace + if let Some(t) = trace.take() { + traces.push(t) + } + Ok(traces) + } else if let Some(errors) = parsed_output.get(&1) { + // Message Codes ref + // https://github.com/tlaplus/tlaplus/blob/master/tlatools/org.lamport.tlatools/src/tlc2/output/EC.java + // Message Classes ref + // https://github.com/tlaplus/tlaplus/blob/master/tlatools/org.lamport.tlatools/src/tlc2/output/MP.java + // NONE = 0; ERROR = 1; TLCBUG = 2; WARNING = 3; STATE = 4; + + let message = errors + .iter() + .map(|(code, message)| { + format!( + "[{}:{}]: {}", + options.log.to_string_lossy(), + code, + &message + .iter() + .map(|x| x.trim().replace("\n", " ")) + .collect::>() + .join(" ") + ) + }) + .collect::>() + .join("\n"); + Err(Error::TLCFailure(message)) + } else { + Ok(vec![]) } - Ok(traces) } fn parse_trace<'a>( - lines: &mut std::str::Lines<'a>, + lines: &mut impl Iterator, options: &ModelCheckerOptions, ) -> Result, Error> { let mut state_index = 0; diff --git a/modelator/src/util.rs b/modelator/src/util.rs index e20a4b2e..a3567316 100644 --- a/modelator/src/util.rs +++ b/modelator/src/util.rs @@ -33,11 +33,10 @@ pub(crate) fn absolute_path>(path: P) -> String { pub(crate) fn read_dir>(path: P) -> Result, Error> { let mut file_names = HashSet::new(); - let files = std::fs::read_dir(path).map_err(Error::io)?; + let files = std::fs::read_dir(path)?; for file in files { // for each file in the modelator directory, check if it is a jar - let file_name = file - .map_err(Error::io)? + let file_name = file? .file_name() .into_string() .map_err(Error::InvalidUnicode)?; @@ -64,13 +63,13 @@ pub(crate) mod digest { } fn digest_file(path: String, digest: &mut sha2::Sha256) -> Result<(), Error> { - let file = std::fs::File::open(path).map_err(Error::io)?; + let file = std::fs::File::open(path)?; let mut reader = std::io::BufReader::new(file); let mut buffer = [0; 1024]; loop { use std::io::Read; - let count = reader.read(&mut buffer).map_err(Error::io)?; + let count = reader.read(&mut buffer)?; if count == 0 { break; } @@ -98,7 +97,7 @@ pub(crate) fn copy_files_into, Q: AsRef>( for file in files { if let Some(file_name) = file.file_name() { let dest = dir.join(file_name); - copy(file, dest).map_err(Error::io)?; + copy(file, dest)?; } } // it is OK to unwrap, as the file has been checked before @@ -127,8 +126,7 @@ fn list_files>(ext: &str, file: P) -> Result, Error> } }); // Collect all files with the same extension in this directory - let files = std::fs::read_dir(dir) - .map_err(Error::io)? + let files = std::fs::read_dir(dir)? .flatten() .filter(|dir_entry| { dir_entry