diff --git a/Cargo.lock b/Cargo.lock index 59a06f18b1cb..726476f4aadb 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -156,6 +156,20 @@ dependencies = [ "walkdir", ] +[[package]] +name = "console" +version = "0.15.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "89eab4d20ce20cea182308bca13088fecea9c05f6776cf287205d41a0ed3c847" +dependencies = [ + "encode_unicode", + "libc", + "once_cell", + "terminal_size", + "unicode-width", + "winapi", +] + [[package]] name = "cprover_bindings" version = "0.7.0" @@ -185,6 +199,12 @@ version = "1.7.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "3f107b87b6afc2a64fd13cac55fe06d6c8859f12d4b14cbcdd2c67d0976781be" +[[package]] +name = "encode_unicode" +version = "0.3.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a357d28ed41a50f9c765dbfe56cbc04a64e53e5fc58ba79fbc34c10ef3df831f" + [[package]] name = "getopts" version = "0.2.21" @@ -318,8 +338,12 @@ dependencies = [ "anyhow", "cargo_metadata", "clap", + "console", "glob", "kani_metadata", + "once_cell", + "pathdiff", + "regex", "serde", "serde_json", "structopt", @@ -549,6 +573,12 @@ dependencies = [ "windows-sys", ] +[[package]] +name = "pathdiff" +version = "0.2.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8835116a5c179084a830efb3adc117ab007512b535bc1a21c991d3b32a6b44dd" + [[package]] name = "pin-project-lite" version = "0.2.9" @@ -831,6 +861,16 @@ dependencies = [ "unicode-ident", ] +[[package]] +name = "terminal_size" +version = "0.1.17" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "633c1a546cee861a1a6d0dc69ebeca693bf4296661ba7852b9d21d159e0506df" +dependencies = [ + "libc", + "winapi", +] + [[package]] name = "textwrap" version = "0.11.0" diff --git a/kani-driver/Cargo.toml b/kani-driver/Cargo.toml index e6e5e836ab7f..3bbc7085cc9b 100644 --- a/kani-driver/Cargo.toml +++ b/kani-driver/Cargo.toml @@ -15,12 +15,16 @@ publish = false kani_metadata = { path = "../kani_metadata" } cargo_metadata = "0.15.0" anyhow = "1" +console = "0.15.1" +once_cell = "1.13.0" serde = { version = "1", features = ["derive"] } serde_json = "1" structopt = "0.3" clap = "2.34" glob = "0.3" toml = "0.5" +regex = "1.6" +pathdiff = "0.2.1" # A good set of suggested dependencies can be found in rustup: # https://github.com/rust-lang/rustup/blob/master/Cargo.toml diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs index 9285436be15b..ee4be38fbe11 100644 --- a/kani-driver/src/call_cbmc.rs +++ b/kani-driver/src/call_cbmc.rs @@ -9,6 +9,7 @@ use std::process::Command; use std::time::Instant; use crate::args::KaniArgs; +use crate::cbmc_output_parser::process_cbmc_output; use crate::session::KaniSession; #[derive(PartialEq, Eq)] @@ -24,7 +25,7 @@ impl KaniSession { { let mut temps = self.temporaries.borrow_mut(); - temps.push(output_filename.clone()); + temps.push(output_filename); } let args: Vec = self.cbmc_flags(file, harness)?; @@ -33,32 +34,41 @@ impl KaniSession { let mut cmd = Command::new("cbmc"); cmd.args(args); - if self.args.output_format == crate::args::OutputFormat::Old { + let now = Instant::now(); + + let verification_result = if self.args.output_format == crate::args::OutputFormat::Old { if self.run_terminal(cmd).is_err() { - return Ok(VerificationStatus::Failure); + Ok(VerificationStatus::Failure) + } else { + Ok(VerificationStatus::Success) } } else { - // extra argument + // Add extra argument to receive the output in JSON format. + // Done here because `--visualize` uses the XML format instead. cmd.arg("--json-ui"); - let now = Instant::now(); - let _cbmc_result = self.run_redirect(cmd, &output_filename)?; - let elapsed = now.elapsed().as_secs_f32(); - let format_result = self.format_cbmc_output(&output_filename); - - if format_result.is_err() { - // Because of things like --assertion-reach-checks and other future features, - // we now decide if we fail or not based solely on the output of the formatter. - return Ok(VerificationStatus::Failure); - // todo: this is imperfect, since we don't know why failure happened. - // the best possible fix is port to rust instead of using python, or getting more - // feedback than just exit status (or using a particular magic exit code?) + // Spawn the CBMC process and process its output below + let cbmc_process_opt = self.run_piped(cmd)?; + if let Some(cbmc_process) = cbmc_process_opt { + // The introduction of reachability checks forces us to decide + // the verification result based on the postprocessing of CBMC results. + let processed_result = process_cbmc_output( + cbmc_process, + self.args.extra_pointer_checks, + &self.args.output_format, + ); + Ok(processed_result) + } else { + Ok(VerificationStatus::Failure) } - // TODO: We should print this even the verification fails but not if it crashes. + }; + // TODO: We should print this even the verification fails but not if it crashes. + if !self.args.dry_run { + let elapsed = now.elapsed().as_secs_f32(); println!("Verification Time: {}s", elapsed); } - Ok(VerificationStatus::Success) + verification_result } /// used by call_cbmc_viewer, invokes different variants of CBMC. diff --git a/kani-driver/src/call_display_results.rs b/kani-driver/src/call_display_results.rs deleted file mode 100644 index cd544a4f8ba5..000000000000 --- a/kani-driver/src/call_display_results.rs +++ /dev/null @@ -1,31 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT - -use anyhow::Result; -use std::ffi::OsString; -use std::path::Path; -use std::process::Command; - -use crate::session::KaniSession; - -impl KaniSession { - /// Display the results of a CBMC run in a user-friendly manner. - pub fn format_cbmc_output(&self, file: &Path) -> Result<()> { - let mut args: Vec = vec![ - self.cbmc_json_parser_py.clone().into(), - file.into(), - self.args.output_format.to_string().to_lowercase().into(), - ]; - - if self.args.extra_pointer_checks { - args.push("--extra-ptr-check".into()); - } - - let mut cmd = Command::new("python3"); - cmd.args(args); - - self.run_terminal(cmd)?; - - Ok(()) - } -} diff --git a/kani-driver/src/cbmc_output_parser.rs b/kani-driver/src/cbmc_output_parser.rs new file mode 100644 index 000000000000..cc647a0786a1 --- /dev/null +++ b/kani-driver/src/cbmc_output_parser.rs @@ -0,0 +1,990 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Module for parsing CBMC's JSON output. In general, this output follows +//! the structure: +//! ``` +//! [ +//! Program, +//! Message, +//! ..., +//! Message, +//! Result, +//! Message, +//! ProverStatus +//! ] +//! ``` +//! The parser included in this file reads from buffered input line by line, and +//! determines if an item can be processed after reading certain lines. +//! +//! The rest of code in this file is related to result postprocessing. + +use crate::{args::OutputFormat, call_cbmc::VerificationStatus}; +use anyhow::Result; +use console::style; +use once_cell::sync::Lazy; +use pathdiff::diff_paths; +use regex::Regex; +use serde::Deserialize; +use std::{ + collections::HashMap, + env, + io::{BufRead, BufReader}, + path::PathBuf, + process::{Child, ChildStdout}, +}; + +type CbmcAltDescriptions = HashMap<&'static str, Vec<(&'static str, Option<&'static str>)>>; + +/// Hash map that relates property classes with descriptions, used by +/// `get_readable_description` to provide user friendly descriptions. +/// See the comment in `get_readable_description` for more information on +/// how this data structure is used. +static CBMC_ALT_DESCRIPTIONS: Lazy = Lazy::new(|| { + let mut map = HashMap::new(); + map.insert("error_label", vec![]); + map.insert("division-by-zero", vec![("division by zero", None)]); + map.insert("enum-range-check", vec![("enum range check", None)]); + map.insert( + "undefined-shift", + vec![ + ("shift distance is negative", None), + ("shift distance too large", None), + ("shift operand is negative", None), + ("shift of non-integer type", None), + ], + ); + map.insert( + "overflow", + vec![ + ("result of signed mod is not representable", None), + ("arithmetic overflow on signed type conversion", None), + ("arithmetic overflow on signed division", None), + ("arithmetic overflow on signed unary minus", None), + ("arithmetic overflow on signed shl", None), + ("arithmetic overflow on unsigned unary minus", None), + ("arithmetic overflow on signed +", Some("arithmetic overflow on signed addition")), + ("arithmetic overflow on signed -", Some("arithmetic overflow on signed subtraction")), + ( + "arithmetic overflow on signed *", + Some("arithmetic overflow on signed multiplication"), + ), + ("arithmetic overflow on unsigned +", Some("arithmetic overflow on unsigned addition")), + ( + "arithmetic overflow on unsigned -", + Some("arithmetic overflow on unsigned subtraction"), + ), + ( + "arithmetic overflow on unsigned *", + Some("arithmetic overflow on unsigned multiplication"), + ), + ("arithmetic overflow on floating-point typecast", None), + ("arithmetic overflow on floating-point division", None), + ("arithmetic overflow on floating-point addition", None), + ("arithmetic overflow on floating-point subtraction", None), + ("arithmetic overflow on floating-point multiplication", None), + ("arithmetic overflow on unsigned to signed type conversion", None), + ("arithmetic overflow on float to signed integer type conversion", None), + ("arithmetic overflow on signed to unsigned type conversion", None), + ("arithmetic overflow on unsigned to unsigned type conversion", None), + ("arithmetic overflow on float to unsigned integer type conversion", None), + ], + ); + map.insert( + "NaN", + vec![ + ("NaN on +", Some("NaN on addition")), + ("NaN on -", Some("NaN on subtraction")), + ("NaN on /", Some("NaN on division")), + ("NaN on *", Some("NaN on multiplication")), + ], + ); + map.insert("pointer", vec![("same object violation", None)]); + map.insert( + "pointer_arithmetic", + vec![ + ("pointer relation: deallocated dynamic object", None), + ("pointer relation: dead object", None), + ("pointer relation: pointer NULL", None), + ("pointer relation: pointer invalid", None), + ("pointer relation: pointer outside dynamic object bounds", None), + ("pointer relation: pointer outside object bounds", None), + ("pointer relation: invalid integer address", None), + ("pointer arithmetic: deallocated dynamic object", None), + ("pointer arithmetic: dead object", None), + ("pointer arithmetic: pointer NULL", None), + ("pointer arithmetic: pointer invalid", None), + ("pointer arithmetic: pointer outside dynamic object bounds", None), + ("pointer arithmetic: pointer outside object bounds", None), + ("pointer arithmetic: invalid integer address", None), + ], + ); + map.insert( + "pointer_dereference", + vec![ + ( + "dereferenced function pointer must be", + Some("dereference failure: invalid function pointer"), + ), + ("dereference failure: pointer NULL", None), + ("dereference failure: pointer invalid", None), + ("dereference failure: deallocated dynamic object", None), + ("dereference failure: dead object", None), + ("dereference failure: pointer outside dynamic object bounds", None), + ("dereference failure: pointer outside object bounds", None), + ("dereference failure: invalid integer address", None), + ], + ); + // These are very hard to understand without more context. + map.insert( + "pointer_primitives", + vec![ + ("pointer invalid", None), + ("deallocated dynamic object", Some("pointer to deallocated dynamic object")), + ("dead object", Some("pointer to dead object")), + ("pointer outside dynamic object bounds", None), + ("pointer outside object bounds", None), + ("invalid integer address", None), + ], + ); + map.insert( + "array_bounds", + vec![ + ("lower bound", Some("index out of bounds")), + // This one is redundant: + // ("dynamic object upper bound", Some("access out of bounds")), + ( + "upper bound", + Some("index out of bounds: the length is less than or equal to the given index"), + ), + ], + ); + map.insert( + "bit_count", + vec![ + ("count trailing zeros is undefined for value zero", None), + ("count leading zeros is undefined for value zero", None), + ], + ); + map.insert("memory-leak", vec![("dynamically allocated memory never freed", None)]); + // These pre-conditions should not print temporary variables since they are embedded in the libc implementation. + // They are added via `__CPROVER_precondition`. + // map.insert("precondition_instance": vec![]); + map +}); + +const UNSUPPORTED_CONSTRUCT_DESC: &str = "is not currently supported by Kani"; +const UNWINDING_ASSERT_DESC: &str = "unwinding assertion loop"; +const ASSERTION_FALSE: &str = "assertion false"; +const DEFAULT_ASSERTION: &str = "assertion"; +const REACH_CHECK_DESC: &str = "[KANI_REACHABILITY_CHECK]"; + +/// Enum that represents a parser item. +/// See the parser for more information on how they are processed. +#[derive(Debug, Deserialize)] +#[serde(untagged)] +enum ParserItem { + Program { + program: String, + }, + #[serde(rename_all = "camelCase")] + Message { + message_text: String, + message_type: String, + }, + Result { + result: Vec, + }, + #[serde(rename_all = "camelCase")] + ProverStatus { + _c_prover_status: String, + }, +} + +impl ParserItem { + /// Determines if an item must be skipped or not. + fn must_be_skipped(&self) -> bool { + matches!(&self, ParserItem::Message { message_text, .. } if message_text.starts_with("Building error trace") || message_text.starts_with("VERIFICATION")) + } +} + +/// Struct that represents a property. +/// +/// Note: `reach` is not part of the parsed data, but it's useful to annotate +/// its reachability status. +#[derive(Clone, Debug, Deserialize)] +pub struct Property { + pub description: String, + pub property: String, + #[serde(rename = "sourceLocation")] + pub source_location: SourceLocation, + pub status: CheckStatus, + pub reach: Option, + pub trace: Option>, +} + +/// Struct that represents a source location. +/// +/// Source locations may be completely empty, which is why +/// all members are optional. +#[derive(Clone, Debug, Deserialize)] +pub struct SourceLocation { + pub column: Option, + pub file: Option, + pub function: Option, + pub line: Option, +} + +impl SourceLocation { + /// Determines if fundamental parts of a source location are missing. + fn is_missing(&self) -> bool { + self.file.is_none() && self.function.is_none() + } +} + +/// `Display` implement for `SourceLocation`. +/// +/// This is used to format source locations for individual checks. But source +/// locations may be printed in a different way in other places (e.g., in the +/// "Failed Checks" summary at the end). +/// +/// Source locations formatted this way will look like: +/// `:: in function ` +/// if all attributes were specified. Otherwise, we: +/// * Omit `in function ` if the function isn't specified. +/// * Use `Unknown file` instead of `::` if the file isn't +/// specified. +/// * Lines and columns are only formatted if they were specified and preceding +/// attribute was formatted. +/// +/// TODO: We could `write!` to `f` directly +/// +impl std::fmt::Display for SourceLocation { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + use std::fmt::Write; + let mut fmt_str = String::new(); + if let Some(file) = self.file.clone() { + let file_path = filepath(file); + write!(&mut fmt_str, "{file_path}")?; + if let Some(line) = self.line.clone() { + write!(&mut fmt_str, ":{line}")?; + if let Some(column) = self.column.clone() { + write!(&mut fmt_str, ":{column}")?; + } + } + } else { + write!(&mut fmt_str, "Unknown file")?; + } + if let Some(function) = self.function.clone() { + write!(&mut fmt_str, " in function {function}")?; + } + + write! {f, "{}", fmt_str} + } +} + +/// Returns a path relative to the current working directory. +fn filepath(file: String) -> String { + let file_path = PathBuf::from(file.clone()); + let cur_dir = env::current_dir().unwrap(); + + let diff_path_opt = diff_paths(file_path, cur_dir); + if let Some(diff_path) = diff_path_opt { + diff_path.into_os_string().into_string().unwrap() + } else { + file + } +} +/// Struct that represents traces. +/// +/// In general, traces may include more information than this, but this is not +/// documented anywhere. So we ignore the rest for now. +#[derive(Clone, Debug, Deserialize)] +#[serde(rename_all = "camelCase")] +pub struct TraceItem { + pub thread: u32, + pub step_type: String, + pub hidden: bool, + pub source_location: Option, +} + +#[derive(Copy, Clone, Debug, Deserialize, PartialEq, Eq)] +#[serde(rename_all = "UPPERCASE")] +pub enum CheckStatus { + Failure, + Success, + Undetermined, + Unreachable, +} + +impl std::fmt::Display for CheckStatus { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + let check_str = match self { + CheckStatus::Success => style("SUCCESS").green(), + CheckStatus::Failure => style("FAILURE").red(), + CheckStatus::Unreachable => style("UNREACHABLE").yellow(), + CheckStatus::Undetermined => style("UNDETERMINED").yellow(), + }; + write! {f, "{}", check_str} + } +} + +#[derive(PartialEq)] +enum Action { + ClearInput, + ProcessItem, +} + +/// A parser for CBMC output, whose state is determined by: +/// 1. The input accumulator, required to process items on the fly. +/// 2. The buffer, which is accessed to retrieve more lines. +/// +/// CBMC's JSON output is defined as a JSON array which contains: +/// 1. One program at the beginning (i.e., a message with CBMC's version). +/// 2. Messages, which can appears anywhere, and are either status messages or error messages. +/// 3. Verification results, another JSON array with all individual checks. +/// 4. Prover status, at the end. Because the verification results depends on +/// our postprocessing, this is not used. +/// +/// The parser reads the output line by line. A line may trigger one action, and +/// the action may return a parsed item. +struct Parser<'a, 'b> { + pub input_so_far: String, + pub buffer: &'a mut BufReader<&'b mut ChildStdout>, +} + +impl<'a, 'b> Parser<'a, 'b> { + pub fn new(buffer: &'a mut BufReader<&'b mut ChildStdout>) -> Self { + Parser { input_so_far: String::new(), buffer } + } + + /// Triggers an action based on the input: + /// * Square brackets ('[' and ']') will trigger the `ClearInput` action + /// because we assume parsing is done on a JSON array. + /// * Curly closing bracket ('}') preceded by two spaces will trigger the + /// `ProcessItem` action. The spaces are important in this case because + /// assume we're in a JSON array. Matching on this specific string guarantees + /// that we'll always get an item when we attempt to process an item. + /// + /// This has be updated if the output format changes at some point. + fn triggers_action(&self, input: String) -> Option { + if input.starts_with('[') || input.starts_with(']') { + // We don't expect any other characters (except '\n') to appear + // after '[' or ']'. The assert below ensures we won't ignore them. + assert!(input.len() == 2); + return Some(Action::ClearInput); + } + if input.starts_with(" }") { + return Some(Action::ProcessItem); + } + None + } + + /// Clears the input accumulated so far. + fn clear_input(&mut self) { + self.input_so_far.clear(); + } + + /// Performs an action. In both cases, the input is cleared. + fn do_action(&mut self, action: Action) -> Option { + match action { + Action::ClearInput => { + self.clear_input(); + None + } + Action::ProcessItem => { + let item = self.parse_item(); + self.clear_input(); + Some(item) + } + } + } + + // Adds a string to the input accumulated so far + fn add_to_input(&mut self, input: String) { + self.input_so_far.push_str(&input); + } + + // Returns a `ParserItem` from the input we have accumulated so far. Since + // all items except the last one are delimited (with a comma), we first try + // to parse the item without the delimiter (i.e., the last character). If + // that fails, then we parse the item using the whole input. + fn parse_item(&self) -> ParserItem { + let string_without_delimiter = &self.input_so_far[0..self.input_so_far.len() - 2]; + let result_item: Result = serde_json::from_str(string_without_delimiter); + if let Ok(item) = result_item { + return item; + } + let complete_string = &self.input_so_far[0..self.input_so_far.len()]; + let result_item: Result = serde_json::from_str(complete_string); + result_item.unwrap() + } + + /// Processes a line to determine if an action must be triggered. + /// The action may result in a `ParserItem`, which is then returned. + pub fn process_line(&mut self, input: String) -> Option { + self.add_to_input(input.clone()); + let action_required = self.triggers_action(input); + if let Some(action) = action_required { + let possible_item = self.do_action(action); + return possible_item; + } + None + } +} + +/// The iterator implementation for `Parser` reads the buffer line by line, +/// and determines if it must return an item based on processing each line. +impl<'a, 'b> Iterator for Parser<'a, 'b> { + type Item = ParserItem; + fn next(&mut self) -> Option { + loop { + let mut input = String::new(); + match self.buffer.read_line(&mut input) { + Ok(len) => { + if len == 0 { + return None; + } + let item = self.process_line(input); + if item.is_some() { + return item; + } else { + continue; + } + } + Err(error) => { + panic!("Error: Got error {} while parsing the output.", error); + } + } + } + } +} + +/// Processes a `ParserItem`. In general, all items are returned as they are, +/// except for: +/// * Error messages, which may be edited. +/// * Verification results, which must be postprocessed. +fn process_item( + item: ParserItem, + extra_ptr_checks: bool, + verification_result: &mut bool, +) -> ParserItem { + match item { + ParserItem::Result { result } => { + let (postprocessed_result, overall_status) = + postprocess_result(result, extra_ptr_checks); + *verification_result = overall_status; + ParserItem::Result { result: postprocessed_result } + } + ParserItem::Message { ref message_type, .. } if message_type == "ERROR" => { + postprocess_error_message(item) + } + item => item, + } +} + +/// Edits an error message. +/// +/// At present, we only know one case where CBMC emits an error message, related +/// to `--object-bits` being too low. The message is edited to show Kani +/// options. +fn postprocess_error_message(message: ParserItem) -> ParserItem { + if let ParserItem::Message { ref message_text, message_type: _ } = message && message_text.contains("use the `--object-bits n` option") { + ParserItem::Message { + message_text: message_text.replace("--object-bits ", "--enable-unstable --cbmc-args --object-bits "), + message_type: String::from("ERROR") } + } else { + message + } +} + +/// The main function to process CBMC's output. +/// +/// First, we create a reader on CBMC's `stdout`, which is required for the +/// parser. Then, we iterate over all the items coming from the parser. In +/// general, items are first processed (this may or may not transform the item), +/// then formatted (according to the output format) and printed. The +/// verification status (i.e., the returned value) depends on processing the +/// verification results. +pub fn process_cbmc_output( + mut process: Child, + extra_ptr_checks: bool, + output_format: &OutputFormat, +) -> VerificationStatus { + let stdout = process.stdout.as_mut().unwrap(); + let mut stdout_reader = BufReader::new(stdout); + let parser = Parser::new(&mut stdout_reader); + let mut result = false; + + for item in parser { + // Some items (e.g., messages) are skipped. + // We could also process them and decide to skip later. + if item.must_be_skipped() { + continue; + } + let processed_item = process_item(item, extra_ptr_checks, &mut result); + // Both formatting and printing could be handled by objects which + // implement a trait `Printer`. + let formatted_item = format_item(&processed_item, output_format); + if let Some(fmt_item) = formatted_item { + println!("{}", fmt_item); + } + // TODO: Record processed items and dump them into a JSON file + // + } + if result { VerificationStatus::Success } else { VerificationStatus::Failure } +} + +/// Returns an optional formatted item based on the output format +fn format_item(item: &ParserItem, output_format: &OutputFormat) -> Option { + match output_format { + OutputFormat::Old => todo!(), + OutputFormat::Regular => format_item_regular(item), + OutputFormat::Terse => format_item_terse(item), + } +} + +/// Formats an item using the regular output format +fn format_item_regular(item: &ParserItem) -> Option { + match item { + ParserItem::Program { program } => Some(program.to_string()), + ParserItem::Message { message_text, .. } => Some(message_text.to_string()), + ParserItem::Result { result } => Some(format_result(result, true)), + _ => None, + } +} + +/// Formats an item using the terse output format +fn format_item_terse(item: &ParserItem) -> Option { + match item { + ParserItem::Result { result } => Some(format_result(result, false)), + _ => None, + } +} + +/// Formats a result item (i.e., the complete set of verification checks). +/// This could be split into two functions for clarity, but at the moment +/// it uses the flag `show_checks` which depends on the output format. +/// +/// TODO: We could `write!` to `result_str` instead +/// +fn format_result(properties: &Vec, show_checks: bool) -> String { + let mut result_str = String::new(); + let mut number_tests_failed = 0; + let mut number_tests_unreachable = 0; + let mut number_tests_undetermined = 0; + let mut failed_tests: Vec<&Property> = vec![]; + + let mut index = 1; + + if show_checks { + result_str.push_str("\nRESULTS:\n"); + } + + for prop in properties { + let name = &prop.property; + let status = &prop.status; + let description = &prop.description; + let location = &prop.source_location; + + match status { + CheckStatus::Failure => { + number_tests_failed += 1; + failed_tests.push(prop); + } + CheckStatus::Undetermined => { + number_tests_undetermined += 1; + } + CheckStatus::Unreachable => { + number_tests_unreachable += 1; + } + _ => (), + } + + if show_checks { + let check_id = format!("Check {}: {}\n", index, name); + let status_msg = format!("\t - Status: {}\n", status); + let description_msg = format!("\t - Description: \"{}\"\n", description); + + result_str.push_str(&check_id); + result_str.push_str(&status_msg); + result_str.push_str(&description_msg); + + if !location.is_missing() { + let location_msg = format!("\t - Location: {}\n", location); + result_str.push_str(&location_msg); + } + result_str.push('\n'); + } + + index += 1; + } + + if show_checks { + result_str.push_str("\nSUMMARY:"); + } else { + result_str.push_str("\nVERIFICATION RESULT:"); + } + + let summary = format!("\n ** {} of {} failed", number_tests_failed, properties.len()); + result_str.push_str(&summary); + + let mut other_status = Vec::::new(); + if number_tests_undetermined > 0 { + let undetermined_str = format!("{} undetermined", number_tests_undetermined); + other_status.push(undetermined_str); + } + if number_tests_unreachable > 0 { + let unreachable_str = format!("{} unreachable", number_tests_unreachable); + other_status.push(unreachable_str); + } + if !other_status.is_empty() { + result_str.push_str(" ("); + result_str.push_str(&other_status.join(",")); + result_str.push(')'); + } + result_str.push('\n'); + + for prop in failed_tests { + let failure_message = build_failure_message(prop.description.clone(), &prop.trace.clone()); + result_str.push_str(&failure_message); + } + + let verification_result = + if number_tests_failed == 0 { style("SUCCESSFUL").green() } else { style("FAILED").red() }; + let overall_result = format!("\nVERIFICATION:- {}\n", verification_result); + result_str.push_str(&overall_result); + + // Ideally, we should generate two `ParserItem::Message` and push them + // into the parser iterator so they are the next messages to be processed. + // However, we haven't figured out the best way to do this for now. + // + if has_check_failure(properties, UNSUPPORTED_CONSTRUCT_DESC) { + result_str.push_str( + "** WARNING: A Rust construct that is not currently supported \ + by Kani was found to be reachable. Check the results for \ + more details.", + ); + } + if has_check_failure(properties, UNWINDING_ASSERT_DESC) { + result_str.push_str("[Kani] info: Verification output shows one or more unwinding failures.\n\ + [Kani] tip: Consider increasing the unwinding value or disabling `--unwinding-assertions`.\n"); + } + + result_str +} + +/// Attempts to build a message for a failed property with as much detailed +/// information on the source location as possible. +fn build_failure_message(description: String, trace: &Option>) -> String { + let backup_failure_message = format!("Failed Checks: {}\n", description); + if trace.is_none() { + return backup_failure_message; + } + let failure_trace = trace.clone().unwrap(); + + let failure_source_wrap = failure_trace[failure_trace.len() - 1].source_location.clone(); + if failure_source_wrap.is_none() { + return backup_failure_message; + } + let failure_source = failure_source_wrap.unwrap(); + + if failure_source.file.is_some() + && failure_source.function.is_some() + && failure_source.line.is_some() + { + let failure_file = failure_source.file.unwrap(); + let failure_function = failure_source.function.unwrap(); + let failure_line = failure_source.line.unwrap(); + return format!( + "Failed Checks: {}\n File: \"{}\", line {}, in {}\n", + description, failure_file, failure_line, failure_function + ); + } + backup_failure_message +} + +/// Postprocess verification results to check for certain cases (e.g. a reachable unsupported construct or a failed +/// unwinding assertion), and update the results of impacted checks accordingly. +/// +/// This postprocessing follows the same steps: +/// 1. Change all "SUCCESS" results to "UNDETERMINED" if the reachability check +/// for a Rust construct that is not currently supported by Kani failed, since +/// the missing exploration of execution paths through the unsupported construct +/// may hide failures +/// 2. Change a check's result from "SUCCESS" to "UNREACHABLE" if its +/// reachability check's result was "SUCCESS" +/// 3. Change results from "SUCCESS" to "UNDETERMINED" if an unwinding +/// assertion failed, since the insufficient unwinding may cause some execution +/// paths to be left unexplored. +/// +/// Additionally, print a message at the end of the output that indicates if any +/// of the special cases above was hit. +pub fn postprocess_result( + properties: Vec, + extra_ptr_checks: bool, +) -> (Vec, bool) { + // First, determine if there are reachable unsupported constructs or unwinding assertions + let has_reachable_unsupported_constructs = + has_check_failure(&properties, UNSUPPORTED_CONSTRUCT_DESC); + let has_failed_unwinding_asserts = has_check_failure(&properties, UNWINDING_ASSERT_DESC); + // Then, determine if there are reachable undefined functions, and change + // their description to highlight this fact + let (properties_with_undefined, has_reachable_undefined_functions) = + modify_undefined_function_checks(properties); + // Split all properties into two groups: Regular properties and reachability checks + let (properties_without_reachs, reach_checks) = filter_reach_checks(properties_with_undefined); + // Filter out successful sanity checks introduced during compilation + let properties_without_sanity_checks = filter_sanity_checks(properties_without_reachs); + // Annotate properties with the results from reachability checks + let properties_annotated = + annotate_properties_with_reach_results(properties_without_sanity_checks, reach_checks); + // Remove reachability check IDs from regular property descriptions + let properties_without_ids = remove_check_ids_from_description(properties_annotated); + + // Filter out extra pointer checks if needed + let properties_filtered = if !extra_ptr_checks { + filter_ptr_checks(properties_without_ids) + } else { + properties_without_ids + }; + let has_fundamental_failures = has_reachable_unsupported_constructs + || has_failed_unwinding_asserts + || has_reachable_undefined_functions; + // Update the status of properties according to reachability checks, among other things + let properties_updated = + update_properties_with_reach_status(properties_filtered, has_fundamental_failures); + + let overall_result = determine_verification_result(&properties_updated); + (properties_updated, overall_result) +} + +/// Determines if there is property with status `FAILURE` and the given description +fn has_check_failure(properties: &Vec, description: &str) -> bool { + for prop in properties { + if prop.status == CheckStatus::Failure && prop.description.contains(description) { + return true; + } + } + false +} + +/// Replaces the description of all properties from functions with a missing +/// definition. +/// TODO: This hasn't been working as expected, see +/// +fn modify_undefined_function_checks(mut properties: Vec) -> (Vec, bool) { + let mut has_unknown_location_checks = false; + for mut prop in &mut properties { + if prop.description.contains(ASSERTION_FALSE) + && extract_property_class(prop).unwrap() == DEFAULT_ASSERTION + && prop.source_location.file.is_none() + { + prop.description = "Function with missing definition is unreachable".to_string(); + if prop.status == CheckStatus::Failure { + has_unknown_location_checks = true; + } + }; + } + (properties, has_unknown_location_checks) +} + +/// Returns a user friendly property description. +/// +/// `CBMC_ALT_DESCRIPTIONS` is a hash map where: +/// * The key is a property class. +/// * The value is a vector of pairs. In each of these pairs, the first member +/// is a description used to match (with method `contains`) on the original +/// property. If a match is found, we inspect the second member: +/// * If it's `None`, we replace the original property with the description +/// used to match. +/// * If it's `Some(string)`, we replace the original property with `string`. +/// +/// For CBMC checks, this will ensure that check failures do not include any +/// temporary variable in their descriptions. +fn get_readable_description(property: &Property) -> String { + let original = property.description.clone(); + let class_id = extract_property_class(property).unwrap(); + + let description_alternatives = CBMC_ALT_DESCRIPTIONS.get(class_id); + if let Some(alt_descriptions) = description_alternatives { + for (desc_to_match, opt_desc_to_replace) in alt_descriptions { + if original.contains(desc_to_match) { + if let Some(desc_to_replace) = opt_desc_to_replace { + return desc_to_replace.to_string(); + } else { + return desc_to_match.to_string(); + } + } + } + } + original +} + +/// Performs a last pass to update all properties as follows: +/// 1. Descriptions are replaced with more readable ones. +/// 2. If there were failures that made the verification result unreliable +/// (e.g., a reachable unsupported construct), changes all `SUCCESS` results +/// to `UNDETERMINED`. +/// 3. If there weren't such failures, it updates all results with a `SUCCESS` +/// reachability check to `UNREACHABLE`. +fn update_properties_with_reach_status( + mut properties: Vec, + has_fundamental_failures: bool, +) -> Vec { + for prop in properties.iter_mut() { + prop.description = get_readable_description(prop); + if has_fundamental_failures { + if prop.status == CheckStatus::Success { + prop.status = CheckStatus::Undetermined; + } + } else if prop.reach.is_some() && prop.reach.unwrap() == CheckStatus::Success { + let description = &prop.description; + assert!( + prop.status == CheckStatus::Success, + "** ERROR: Expecting the unreachable property \"{}\" to have a status of \"SUCCESS\"", + description + ); + prop.status = CheckStatus::Unreachable + } + } + properties +} + +/// Some Kani-generated asserts have a unique ID in their description of the form: +/// ``` +/// [KANI_CHECK_ID__] +/// ``` +/// e.g.: +/// ``` +/// [KANI_CHECK_ID_foo.6875c808::foo_0] assertion failed: x % 2 == 0 +/// ``` +/// This function removes those IDs from the property's description so that +/// they're not shown to the user. The removal of the IDs should only be done +/// after all ID-based post-processing is done. +fn remove_check_ids_from_description(mut properties: Vec) -> Vec { + let check_id_pat = Regex::new(r"\[KANI_CHECK_ID_([^\]]*)\] ").unwrap(); + for prop in properties.iter_mut() { + prop.description = check_id_pat.replace(&prop.description, "").to_string(); + } + properties +} + +/// Extracts the property class from the property string. +/// +/// Property strings have the format `([.].)` +fn extract_property_class(property: &Property) -> Option<&str> { + let property_class: Vec<&str> = property.property.rsplitn(3, '.').collect(); + if property_class.len() > 1 { Some(property_class[1]) } else { None } +} + +/// Given a description, this splits properties into two groups: +/// 1. Properties that don't contain the description +/// 2. Properties that contain the description +fn filter_properties(properties: Vec, message: &str) -> (Vec, Vec) { + let mut filtered_properties = Vec::::new(); + let mut removed_properties = Vec::::new(); + for prop in properties { + if prop.description.contains(message) { + removed_properties.push(prop); + } else { + filtered_properties.push(prop); + } + } + (filtered_properties, removed_properties) +} + +/// Filters reachability checks with `filter_properties` +fn filter_reach_checks(properties: Vec) -> (Vec, Vec) { + filter_properties(properties, REACH_CHECK_DESC) +} + +/// Filters out Kani-generated sanity checks with a `SUCCESS` status +fn filter_sanity_checks(properties: Vec) -> Vec { + properties + .into_iter() + .filter(|prop| { + !(extract_property_class(prop).unwrap() == "sanity_check" + && prop.status == CheckStatus::Success) + }) + .collect() +} + +/// Filters out properties related to extra pointer checks +/// +/// Our support for primitives and overflow pointer checks is unstable and +/// can result in lots of spurious failures. By default, we filter them out. +fn filter_ptr_checks(properties: Vec) -> Vec { + properties + .into_iter() + .filter(|prop| { + !extract_property_class(prop).unwrap().contains("pointer_arithmetic") + && !extract_property_class(prop).unwrap().contains("pointer_primitives") + }) + .collect() +} + +/// When assertion reachability checks are turned on, Kani prefixes each +/// assert's description with an ID of the following form: +/// ``` +/// [KANI_CHECK_ID__] +/// ``` +/// e.g.: +/// ``` +/// [KANI_CHECK_ID_foo.6875c808::foo_0] assertion failed: x % 2 == 0 +/// ``` +/// In addition, the description of each reachability check that it generates +/// includes the ID of the assert for which we want to check its reachability. +/// The description of a reachability check uses the following template: +/// ``` +/// [KANI_REACHABILITY_CHECK] +/// ``` +/// e.g.: +/// ``` +/// [KANI_REACHABILITY_CHECK] KANI_CHECK_ID_foo.6875c808::foo_0 +/// ``` +/// This function first collects all data from reachability checks. Then, +/// it updates the reachability status for all properties accordingly. +fn annotate_properties_with_reach_results( + mut properties: Vec, + reach_checks: Vec, +) -> Vec { + let mut reach_map: HashMap = HashMap::new(); + let reach_desc_pat = Regex::new("KANI_CHECK_ID_.*_([0-9])*").unwrap(); + // Collect data (ID, status) from reachability checks + for reach_check in reach_checks { + let description = reach_check.description; + // Capture the ID in the reachability check + let check_id = + reach_desc_pat.captures(description.as_str()).unwrap().get(0).unwrap().as_str(); + let check_id_str = format!("[{}]", check_id); + // Get the status and insert into `reach_map` + let status = reach_check.status; + let res_ins = reach_map.insert(check_id_str, status); + assert!(res_ins.is_none()); + } + + for prop in properties.iter_mut() { + let description = &prop.description; + let check_marker_pat = Regex::new(r"\[KANI_CHECK_ID_([^\]]*)\]").unwrap(); + if check_marker_pat.is_match(description) { + // Capture the ID in the property + let prop_match_id = + check_marker_pat.captures(description.as_str()).unwrap().get(0).unwrap().as_str(); + // Get the status associated to the ID we captured + let reach_status_opt = reach_map.get(&prop_match_id.to_string()); + // Update the reachability status of the property + if let Some(reach_status) = reach_status_opt { + prop.reach = Some(*reach_status); + } + } + } + properties +} + +/// Gets the overall verification result (i.e., failure if any properties show failure) +fn determine_verification_result(properties: &[Property]) -> bool { + let number_failed_properties = + properties.iter().filter(|prop| prop.status == CheckStatus::Failure).count(); + number_failed_properties == 0 +} diff --git a/kani-driver/src/main.rs b/kani-driver/src/main.rs index a264d98ca588..a1dda17c8f22 100644 --- a/kani-driver/src/main.rs +++ b/kani-driver/src/main.rs @@ -16,11 +16,11 @@ mod args_toml; mod call_cargo; mod call_cbmc; mod call_cbmc_viewer; -mod call_display_results; mod call_goto_cc; mod call_goto_instrument; mod call_single_file; mod call_symtab; +mod cbmc_output_parser; mod metadata; mod session; mod util; diff --git a/kani-driver/src/session.rs b/kani-driver/src/session.rs index 0cb83279a71d..2387a612ac60 100644 --- a/kani-driver/src/session.rs +++ b/kani-driver/src/session.rs @@ -7,7 +7,7 @@ use anyhow::{bail, Context, Result}; use std::cell::RefCell; use std::io::Write; use std::path::{Path, PathBuf}; -use std::process::{Command, ExitStatus}; +use std::process::{Child, Command, ExitStatus, Stdio}; /// Contains information about the execution environment and arguments that affect operations pub struct KaniSession { @@ -20,8 +20,6 @@ pub struct KaniSession { pub kani_lib_c: PathBuf, /// The location we found the Kani C stub .c files pub kani_c_stubs: PathBuf, - /// The location we found 'cbmc_json_parser.py' - pub cbmc_json_parser_py: PathBuf, /// The location we found our pre-built libraries pub kani_rlib: Option, @@ -49,7 +47,6 @@ impl KaniSession { kani_compiler: install.kani_compiler()?, kani_lib_c: install.kani_lib_c()?, kani_c_stubs: install.kani_c_stubs()?, - cbmc_json_parser_py: install.cbmc_json_parser_py()?, kani_rlib: install.kani_rlib()?, temporaries: RefCell::new(vec![]), }) @@ -140,6 +137,26 @@ impl KaniSession { cmd.status().context(format!("Failed to invoke {}", cmd.get_program().to_string_lossy())) } + + /// Run a job and pipe its output to this process. + /// Returns an error if the process could not be spawned + pub fn run_piped(&self, mut cmd: Command) -> Result> { + if self.args.verbose || self.args.dry_run { + println!("{}", render_command(&cmd).to_string_lossy()); + if self.args.dry_run { + return Ok(None); + } + } + // Run the process as a child process + let process = cmd.stdout(Stdio::piped()).spawn(); + + // Render the command if the process could not be spawned + if process.is_err() { + bail!("Could not spawn process `{}`", render_command(&cmd).to_string_lossy()); + } + // Return the child process handle + Ok(Some(process.unwrap())) + } } /// Return the path for the folder where the current executable is located. @@ -192,10 +209,6 @@ impl InstallType { self.base_path_with("library/kani/stubs/C") } - pub fn cbmc_json_parser_py(&self) -> Result { - self.base_path_with("scripts/cbmc_json_parser.py") - } - pub fn kani_rlib(&self) -> Result> { match self { Self::DevRepo(_repo) => { diff --git a/scripts/cbmc_json_parser.py b/scripts/cbmc_json_parser.py deleted file mode 100755 index 5bf0ff25e069..000000000000 --- a/scripts/cbmc_json_parser.py +++ /dev/null @@ -1,841 +0,0 @@ -#!/usr/bin/env python3 -# Copyright Kani Contributors -# SPDX-License-Identifier: Apache-2.0 OR MIT - - -"""CBMC JSON Parser - -This script allows kani to print to the console the final output displayed to the user -after CBMC gives the response JSON object. - -This script accepts JSON files. - -This script requires that `colorama` be installed within the Python -environment you are running this script in. - -This file can also be imported as a module and contains the following -functions: - - * transform_cbmc_output - returns the formatted string output after parsing - * main - the main function of the script -""" - -import json -import os -import re -import sys - -from colorama import Fore, Style -from enum import Enum -from os import path - -# Enum to store the style of output that is given by the argument flags -output_style_switcher = { - 'default': 'regular', - 'regular': 'regular', - 'terse': 'terse', - 'old': 'old' -} - -class GlobalMessages(str, Enum): - """ - Enum class to store all the global messages - """ - CONST_TRACE_MESSAGE = 'Building error trace', - PROGRAM = 'program' - RESULT = 'result' - MESSAGE_TEXT = 'messageText' - MESSAGE_TYPE = 'messageType' - SUCCESS = 'SUCCESS' - FAILED = 'FAILED' - REACH_CHECK_DESC = "[KANI_REACHABILITY_CHECK]" - REACH_CHECK_KEY = "reachCheckResult" - CHECK_ID = "KANI_CHECK_ID" - ASSERTION_FALSE = "assertion false" - DEFAULT_ASSERTION = "assertion" - CHECK_ID_RE = CHECK_ID + r"_.*_([0-9])*" - UNSUPPORTED_CONSTRUCT_DESC = "is not currently supported by Kani" - UNWINDING_ASSERT_DESC = "unwinding assertion loop" - - -def usage_error(msg): - """ Prints an error message followed by the expected usage. Then exit process. """ - print(f"Error: {msg} Usage:") - print("cbmc_json_parser.py [--extra-ptr-check]") - sys.exit(1) - - -def main(argv): - """ - Script main function. - Usage: - > cbmc_json_parser.py [--extra-ptr-check] - """ - # We expect [3, 4] arguments. - if len(argv) < 3: - usage_error("Missing required arguments.") - - max_args = 4 - if len(argv) > max_args: - usage_error(f"Expected up to {max_args} arguments but found {len(argv)}.") - - output_style = output_style_switcher.get(argv[2], None) - if not output_style: - usage_error(f"Invalid output format '{argv[2]}'.") - - extra_ptr_check = False - if len(argv) == 4: - if argv[3] == "--extra-ptr-check": - extra_ptr_check = True - else: - usage_error(f"Unexpected argument '{argv[3]}'.") - - # parse the input json file - with open(argv[1]) as f: - sample_json_file_parsing = f.read() - - # the main function should take a json file as input - return_code = transform_cbmc_output(sample_json_file_parsing, - output_style, extra_ptr_check) - sys.exit(return_code) - - -class SourceLocation: - def __init__(self, source_location={}): - """ Convert a source location dictionary from CBMC json into an object. - The SOURCE_LOCATION_OBJECT has the following structure: - { - 'column': '', - 'file': '', - 'function': '', - 'line': '' - }}, - - Some fields might be missing. - """ - self.filename = source_location.get("file", None) - self.function = source_location.get("function", None) - self.column = source_location.get("column", None) - self.line = source_location.get("line", None) - - def filepath(self): - """ Return a more user friendly path. - - - If the path is inside the current directory, return a relative path. - - If not but the path is in the ${HOME} directory, return relative to ${HOME} - - Otherwise, return the path as is. - """ - if not self.filename: - return None - - # Reference to C files use relative paths, while rust uses absolute. - # Normalize both to be absolute first. - full_path = path.abspath(self.filename) - cwd = os.getcwd() - if path.commonpath([full_path, cwd]) == cwd: - return path.relpath(full_path) - - home_path = path.expanduser("~") - if path.commonpath([full_path, home_path]) == home_path: - return "~/{}".format(path.relpath(full_path, home_path)) - - return self.filename - - def __str__(self): - if self.filename: - s = f"{self.filepath()}" - if self.line: - s += f":{self.line}" - if self.column: - s += f":{self.column}" - else: - s = "Unknown File" - if self.function: - s += f" in function {self.function}" - return s - - def __bool__(self): - return bool(self.function) or bool(self.filename) - - -def transform_cbmc_output(cbmc_response_string, output_style, extra_ptr_check): - """ - Take Unstructured CBMC Response object, parse the blob and gives structured - and formatted output depending on User Provided Output Style - - Parameters - - cbmc_response_string : str - A response blob that is given to the function from CBMC - output_style : int - An index to tell the script which style of output is requested by the User. - - Returns - - None - Prints the final output string to the user - """ - - # Output Message is the final output that is printed to the user - output_message = "" - - # Check if the output given by CBMC is in Json format or not - is_json_bool, cbmc_json_array = parse_json(cbmc_response_string) - if is_json_bool: - - # Extract property information from the restructured JSON file - properties, solver_information = extract_solver_information(cbmc_json_array) - - # Check if there were any errors - errors = extract_errors(solver_information) - if errors: - print('\n'.join(errors)) - return 1 - - properties, messages = postprocess_results(properties, extra_ptr_check) - - # Using Case Switching to Toggle between various output styles - # For now, the two options provided are default and terse - if output_style == output_style_switcher["regular"]: - - # Extract Solver Information from the json file and construct message - output_message += construct_solver_information_message(solver_information) - - # Extract property messages from the json file - property_message, num_failed = construct_property_message(properties) - # Combine both messages to give as final output - output_message += property_message - - elif output_style == output_style_switcher["terse"]: - - # Construct only summarized result and display output - output_message, num_failed = construct_terse_property_message(properties) - - # Print using an Interface function - print(output_message) - print(messages) - - else: - # When CBMC crashes or does not produce json output, print the response - # string to allow us to debug - print(cbmc_response_string) - raise Exception("CBMC Crashed - Unable to present Result") - - return num_failed > 0 - -# Check if the blob is in json format for parsing -def parse_json(cbmc_output_string): - try: - cbmc_json_array = json.loads(cbmc_output_string) - except ValueError: - return False, None - return True, cbmc_json_array - -def extract_solver_information(cbmc_response_json_array): - """ - Takes the CBMC Response, now in JSON Array format and extracts solver and property information - and splits them into two seperate lists. - - Parameters - - cbmc_response_json_array : JSON Array - A response JSON Array that contains the Result Object from CBMC and - Solver Information - - Input Example - - [{'program': 'CBMC 5.44.0 (cbmc-5.44.0)'}, - {'messageText': 'CBMC version 5.44.0 (cbmc-5.44.0) 64-bit x86_64 linux', 'messageType': 'STATUS-MESSAGE'}, - {'messageText': 'Reading GOTO program from file', 'messageType': 'STATUS-MESSAGE'}, - ... - {'result': [{'description': 'assertion failed: 2 == 4', 'property': 'main.assertion.1', 'status': 'FAILURE', ' - trace': [{'function': {'displayName': '__CPROVER_initialize', 'identifier': '__CPROVER_initialize', - 'sourceLocation': {'file': '', 'line': '40', 'workingDirectory': '/home/ubuntu'}}, - ...'thread': 0}]} - - Returns - - properties : List - Contains the list of properties that is obtained from the "result" object from CBMC. - - solver_information : List - Contains the list of message texts which collectively contain information about the solver. - - """ - - # Solver information is all the fields in the json object which are not related to the results - solver_information = [] - properties = None - - # Parse each object and extract out the "result" object to be returned seperately - for response_object in cbmc_response_json_array: - """Example response object - - 1) {'program': 'CBMC 5.44.0 (cbmc-5.44.0)'}, - 2) {'result': [{'description': 'assertion failed: 2 == 4',..} - """ - if GlobalMessages.RESULT in response_object.keys(): - properties = response_object["result"] - else: - solver_information.append(response_object) - - return properties, solver_information - -def modify_undefined_function_checks(properties): - """ - 1. Searches for any check which has unknown file location or missing defition and replaces description - 2. If a function with missing definition is reachable, then we turn all SUCCESS status to UNDETERMINED. - If there are no reachable functions with missing definitions, then the verification is not affected, so we retain all of the SUCCESS status. - """ - has_unknown_location_checks = False - for property in properties: - # Specifically trying to capture assertions that CBMC generates for functions with missing definitions - if GlobalMessages.ASSERTION_FALSE in property["description"] and extract_property_class( - property) == GlobalMessages.DEFAULT_ASSERTION and not hasattr(property["sourceLocation"], "file"): - property["description"] = "Function with missing definition is unreachable" - if property["status"] == "FAILURE": - has_unknown_location_checks = True - return has_unknown_location_checks - -def extract_errors(solver_information): - """ - Extract errors from the CBMC output, which are messages that have the - message type 'ERROR' - """ - errors = [] - for message in solver_information: - if GlobalMessages.MESSAGE_TYPE in message and message[GlobalMessages.MESSAGE_TYPE] == 'ERROR': - error_message = message[GlobalMessages.MESSAGE_TEXT] - # Replace "--object bits n" with "--enable-unstable --cbmc-args - # --object bits n" in the message - if 'use the `--object-bits n` option' in error_message: - error_message = error_message.replace("--object-bits ", "--enable-unstable --cbmc-args --object-bits ") - errors.append(error_message) - return errors - -def postprocess_results(properties, extra_ptr_check): - """ - Check for certain cases, e.g. a reachable unsupported construct or a failed - unwinding assertion, and update the results of impacted checks accordingly. - 1. Change all "SUCCESS" results to "UNDETERMINED" if the reachability check - for a Rust construct that is not currently supported by Kani failed, since - the missing exploration of execution paths through the unsupported construct - may hide failures - 2. Change a check's result from "SUCCESS" to "UNREACHABLE" if its - reachability check's result was "SUCCESS" - 3. TODO: Change results from "SUCCESS" to "UNDETERMINED" if an unwinding - assertion failed, since the insufficient unwinding may cause some execution - paths to be left unexplored (https://github.com/model-checking/kani/issues/746) - - Additionally, print a message at the end of the output that indicates if any - of the special cases above was hit. - """ - - has_reachable_unsupported_constructs = has_check_failure(properties, GlobalMessages.UNSUPPORTED_CONSTRUCT_DESC) - has_failed_unwinding_asserts = has_check_failure(properties, GlobalMessages.UNWINDING_ASSERT_DESC) - has_reachable_undefined_functions = modify_undefined_function_checks(properties) - properties, reach_checks = filter_reach_checks(properties) - properties = filter_sanity_checks(properties) - annotate_properties_with_reach_results(properties, reach_checks) - remove_check_ids_from_description(properties) - - if not extra_ptr_check: - properties = filter_ptr_checks(properties) - - for property in properties: - property["description"] = get_readable_description(property) - if has_reachable_unsupported_constructs or has_failed_unwinding_asserts or has_reachable_undefined_functions: - # Change SUCCESS to UNDETERMINED for all properties - if property["status"] == "SUCCESS": - property["status"] = "UNDETERMINED" - elif GlobalMessages.REACH_CHECK_KEY in property and property[GlobalMessages.REACH_CHECK_KEY] == "SUCCESS": - # Change SUCCESS to UNREACHABLE - description = property["description"] - assert property[ - "status"] == "SUCCESS", f"** ERROR: Expecting the unreachable property \"{description}\" to have a status of \"SUCCESS\"" - property["status"] = "UNREACHABLE" - - messages = "" - if has_reachable_unsupported_constructs: - messages += "** WARNING: A Rust construct that is not currently supported " \ - "by Kani was found to be reachable. Check the results for " \ - "more details." - if has_failed_unwinding_asserts: - messages += "[Kani] info: Verification output shows one or more unwinding failures.\n" \ - "[Kani] tip: Consider increasing the unwinding value or disabling `--unwinding-assertions`.\n" - - return properties, messages - - -def has_check_failure(properties, message): - """ - Search in properties for a failed property with the given message - """ - for property in properties: - if message in property["description"] and property["status"] == "FAILURE": - return True - return False - -def filter_reach_checks(properties): - return filter_properties(properties, GlobalMessages.REACH_CHECK_DESC) - -def filter_sanity_checks(properties): - """ - Specific filter for sanity_check checks that removed checks with SUCCESS status - """ - filtered_properties = [] - property_class = "sanity_check" - for property in properties: - if property_class in extract_property_class(property) and property["status"] == "SUCCESS": - pass - else: - filtered_properties.append(property) - - return filtered_properties - -def filter_properties(properties, message): - """ - Move properties that have "message" in their description out of "properties" - into "removed_properties" - """ - filtered_properties = [] - removed_properties = [] - for property in properties: - if message in property["description"]: - removed_properties.append(property) - else: - filtered_properties.append(property) - return filtered_properties, removed_properties - -class CProverCheck: - """ Represents a CProverCheck and provides methods to replace the check. - - Objects of this class are used to represent specific types of CBMC's - check messages. It allow us to identify and to replace them by a more - user friendly message. - - That includes rewriting them and removing information that don't - make sense in the ust context. E.g.: - - Original CBMC message: "dead object in OBJECT_SIZE(&temp_0)" - Not in the original code -> ^^^^^^^^^^^^^^^^^^^^ - - New message: "pointer to dead object" - """ - - def __init__(self, msg, new_msg=None): - self.original = msg - self.kani_msg = new_msg if new_msg else msg - - def matches(self, msg): - return self.original in msg - - def replace(self, msg): - return self.kani_msg - - -CBMC_DESCRIPTIONS = { - "error_label": [], - "division-by-zero": [CProverCheck("division by zero")], - "enum-range-check": [CProverCheck("enum range check")], - "undefined-shift": [CProverCheck("shift distance is negative"), - CProverCheck("shift distance too large"), - CProverCheck("shift operand is negative"), - CProverCheck("shift of non-integer type")], - "overflow": [ - CProverCheck("result of signed mod is not representable"), - CProverCheck("arithmetic overflow on signed type conversion"), - CProverCheck("arithmetic overflow on signed division"), - CProverCheck("arithmetic overflow on signed unary minus"), - CProverCheck("arithmetic overflow on signed shl"), - CProverCheck("arithmetic overflow on unsigned unary minus"), - CProverCheck("arithmetic overflow on signed +", "arithmetic overflow on signed addition"), - CProverCheck("arithmetic overflow on signed -", "arithmetic overflow on signed subtraction"), - CProverCheck("arithmetic overflow on signed *", "arithmetic overflow on signed multiplication"), - CProverCheck("arithmetic overflow on unsigned +", "arithmetic overflow on unsigned addition"), - CProverCheck("arithmetic overflow on unsigned -", "arithmetic overflow on unsigned subtraction"), - CProverCheck("arithmetic overflow on unsigned *", "arithmetic overflow on unsigned multiplication"), - CProverCheck("arithmetic overflow on floating-point typecast"), - CProverCheck("arithmetic overflow on floating-point division"), - CProverCheck("arithmetic overflow on floating-point addition"), - CProverCheck("arithmetic overflow on floating-point subtraction"), - CProverCheck("arithmetic overflow on floating-point multiplication"), - CProverCheck("arithmetic overflow on unsigned to signed type conversion"), - CProverCheck("arithmetic overflow on float to signed integer type conversion"), - CProverCheck("arithmetic overflow on signed to unsigned type conversion"), - CProverCheck("arithmetic overflow on unsigned to unsigned type conversion"), - CProverCheck("arithmetic overflow on float to unsigned integer type conversion")], - "NaN": [ - CProverCheck("NaN on +", "NaN on addition"), - CProverCheck("NaN on -", "NaN on subtraction"), - CProverCheck("NaN on /", "NaN on division"), - CProverCheck("NaN on *", "NaN on multiplication")], - "pointer": [ - CProverCheck("same object violation")], - "pointer_arithmetic": [ - CProverCheck("pointer relation: deallocated dynamic object"), - CProverCheck("pointer relation: dead object"), - CProverCheck("pointer relation: pointer NULL"), - CProverCheck("pointer relation: pointer invalid"), - CProverCheck("pointer relation: pointer outside dynamic object bounds"), - CProverCheck("pointer relation: pointer outside object bounds"), - CProverCheck("pointer relation: invalid integer address"), - CProverCheck("pointer arithmetic: deallocated dynamic object"), - CProverCheck("pointer arithmetic: dead object"), - CProverCheck("pointer arithmetic: pointer NULL"), - CProverCheck("pointer arithmetic: pointer invalid"), - CProverCheck("pointer arithmetic: pointer outside dynamic object bounds"), - CProverCheck("pointer arithmetic: pointer outside object bounds"), - CProverCheck("pointer arithmetic: invalid integer address")], - "pointer_dereference": [ - CProverCheck("dereferenced function pointer must be", "dereference failure: invalid function pointer"), - CProverCheck("dereference failure: pointer NULL"), - CProverCheck("dereference failure: pointer invalid"), - CProverCheck("dereference failure: deallocated dynamic object"), - CProverCheck("dereference failure: dead object"), - CProverCheck("dereference failure: pointer outside dynamic object bounds"), - CProverCheck("dereference failure: pointer outside object bounds"), - CProverCheck("dereference failure: invalid integer address")], - "pointer_primitives": [ - # These are very hard to understand without more context. - CProverCheck("pointer invalid"), - CProverCheck("deallocated dynamic object", "pointer to deallocated dynamic object"), - CProverCheck("dead object", "pointer to dead object"), - CProverCheck("pointer outside dynamic object bounds"), - CProverCheck("pointer outside object bounds"), - CProverCheck("invalid integer address") - ], - "array_bounds": [ - CProverCheck("lower bound", "index out of bounds"), # Irrelevant check. Only usize allowed as index. - # This one is redundant: - # CProverCheck("dynamic object upper bound", "access out of bounds"), - CProverCheck("upper bound", "index out of bounds: the length is less than or equal to the given index"), ], - "bit_count": [ - CProverCheck("count trailing zeros is undefined for value zero"), - CProverCheck("count leading zeros is undefined for value zero")], - "memory-leak": [ - CProverCheck("dynamically allocated memory never freed")], - # These pre-conditions should not print temporary variables since they are embedded in the libc implementation. - # They are added via __CPROVER_precondition. - # "precondition_instance": [], -} - - -def extract_property_class(prop): - """ - This function extracts the property class from the property string. - Property strings have the format of -([.].) - """ - prop_class = prop["property"].rsplit(".", 3) - # Do nothing if prop_class is diff than cbmc's convention - class_id = prop_class[-2] if len(prop_class) > 1 else None - return class_id - - -def filter_ptr_checks(props): - """This function will filter out extra pointer checks. - - Our support to primitives and overflow pointer checks is unstable and - can result in lots of spurious failures. By default, we filter them out. - """ - def not_extra_check(prop): - return extract_property_class(prop) not in ["pointer_arithmetic", "pointer_primitives"] - - return list(filter(not_extra_check, props)) - - -def get_readable_description(prop): - """This function will return a user friendly property description. - - For CBMC checks, it will ensure that the failure does not include any - temporary variable. - """ - original = prop["description"] - class_id = extract_property_class(prop) - if class_id in CBMC_DESCRIPTIONS: - # Contains a list for potential message translation [String]. - prop_type = [check.replace(original) for check in CBMC_DESCRIPTIONS[class_id] if check.matches(original)] - if len(prop_type) != 1: - if "KANI_FAIL_ON_UNEXPECTED_DESCRIPTION" in os.environ: - print(f"Unexpected description: {original}\n" - f" - class_id: {class_id}\n" - f" - matches: {prop_type}\n") - exit(1) - else: - return original - else: - return prop_type[0] - return original - -def annotate_properties_with_reach_results(properties, reach_checks): - """ - When assertion reachability checks are turned on, kani prefixes each - assert's description with an "ID" of the following form: - [KANI_CHECK_ID__] - e.g.: - [KANI_CHECK_ID_foo.6875c808::foo_0] assertion failed: x % 2 == 0 - In addition, the description of each reachability check that it generates - includes the ID of the assert that we want to check its reachability. The - description of a reachability check uses the following template: - [KANI_REACHABILITY_CHECK] - e.g.: - [KANI_REACHABILITY_CHECK] KANI_CHECK_ID_foo.6875c808::foo_0 - This function iterates over the reachability checks, and for each: - 1. It finds the corresponding assert through matching the ID - 2. It annotates the assert's data with the result of the reachability check - under the GlobalMessages.REACH_CHECK_KEY key - """ - for reach_check in reach_checks: - description = reach_check["description"] - # Extract the ID of the assert from the description - match_obj = re.search(GlobalMessages.CHECK_ID_RE, description) - if not match_obj: - raise Exception("Error: failed to extract check ID for reachability check \"" + description + "\"") - check_id = match_obj.group(0) - prop = get_matching_property(properties, check_id) - # Attach the result of the reachability check to this property - prop[GlobalMessages.REACH_CHECK_KEY] = reach_check["status"] - - -def get_matching_property(properties, check_id): - """ - Find the property with the given ID - """ - for property in properties: - description = property["description"] - match_obj = re.search("\\[" + GlobalMessages.CHECK_ID_RE + "\\]", description) - # Currently, not all properties have a check ID - if match_obj: - prop_check_id = match_obj.group(0) - if prop_check_id == "[" + check_id + "]": - return property - raise Exception("Error: failed to find a property with ID \"" + check_id + "\"") - - -def remove_check_ids_from_description(properties): - """ - Some asserts generated by Kani have a unique ID in their description that is - of the form: - - [KANI_CHECK_ID__] - - e.g.: - - [KANI_CHECK_ID_foo.6875c808::foo_0] assertion failed: x % 2 == 0 - - This function removes those IDs from the property's description so that - they're not shown to the user. The removal of the IDs should only be done - after all ID-based post-processing is done. - """ - check_id_pattern = re.compile(r"\[" + GlobalMessages.CHECK_ID_RE + r"\] ") - for property in properties: - property["description"] = re.sub(check_id_pattern, "", property["description"]) - - -def construct_solver_information_message(solver_information): - """ - From the extracted information, construct a message and append to the final Output - - Sample Output - - CBMC 5.36.0 (cbmc-5.36.0) - CBMC version 5.36.0 (cbmc-5.36.0) 64-bit x86_64 linux - Reading GOTO program from file - ... - """ - - solver_information_message = "" - for message_object in solver_information: - # 'Program' and 'messageText' fields give us the information about the solver - try: - # Objects with the key "program" give information about CBMC's version - # Example - {'program': 'CBMC 5.44.0 (cbmc-5.44.0)'} - if GlobalMessages.PROGRAM in message_object.keys(): - solver_information_message += message_object['program'] - - # Check message texts - objects with the key 'messageText' - # Example - {'messageText': 'CBMC version 5.44.0 (cbmc-5.44.0) 64-bit x86_64 linux', 'messageType': 'STATUS-MESSAGE'}, - # {'messageText': 'Reading GOTO program from file', 'messageType': 'STATUS-MESSAGE'} - elif GlobalMessages.MESSAGE_TEXT in message_object.keys(): - # Remove certain messageTexts which do not contain important information, like "Building error trace" - if message_object['messageText'] != GlobalMessages.CONST_TRACE_MESSAGE: - solver_information_message += message_object['messageText'] - else: - solver_information_message += '\n' - break - else: - pass - except KeyError as e: - print("Key Error, Missing Properties in reading Solver Information from JSON") - solver_information_message += '\n' - return solver_information_message - -def construct_terse_property_message(properties): - """ - Get property tests and results from the Json file written and construct - a terse final output displaying only final results and summary of tests - - input - - list - properties is a list of small json objects containing each test , description and result - Ex - - {'description': 'assertion false', 'property': 'fmaf.assertion.1', 'status': 'SUCCESS'} - {'description': 'assertion failed: 2 == 4', 'property': 'main.assertion.1', 'status': 'FAILURE', 'trace': [{'function': {'displayName' .. - - output - - str - Final string output which is a summary of the property tests - Ex - SUMMARY: - ** 1 of 54 failed - Failed Checks: assertion failed: 2 == 4 - File: "/home/ubuntu/test.rs", line 3, in main - VERIFICATION:- FAILED - """ - number_tests_failed = 0 - output_message = "" - failed_tests = [] - verification_status = GlobalMessages.FAILED - - # Parse each property instance in properties - for property_instance in properties: - status = property_instance["status"] - if status == "FAILURE": - number_tests_failed += 1 - failed_tests.append(property_instance) - else: - pass - - # Ex - OUTPUT: ** 1 of 54 failed - output_message += f"VERIFICATION RESULT: \n ** {number_tests_failed} of {len(properties)} failed\n" - - # The Verification is successful and the program is verified - if number_tests_failed == 0: - verification_status = colored_text(Fore.GREEN, "SUCCESSFUL") - else: - # Go through traces to extract relevant information to be displayed in the summary - # only in the case of failure - verification_status = colored_text(Fore.RED, "FAILED") - for failed_test in failed_tests: - try: - failure_message = failed_test["description"] - failure_source = failed_test["trace"][-1]['sourceLocation'] - failure_message_path = failure_source['file'] - failure_function_name = failure_source['function'] - failure_line_number = failure_source['line'] - output_message += f"Failed Checks: {failure_message}\n File: \"{failure_message_path}\", line {failure_line_number}, in {failure_function_name}\n" - except KeyError: - failure_source = "None" - output_message += f"Failed Checks: {failure_message}\n" - - # TODO: Get final status from the cprover status - output_message += f"\nVERIFICATION:- {verification_status}\n" - - return output_message, number_tests_failed - -def construct_property_message(properties): - """ - Get property tests and results from the Json file written and construct - a verbose final output displaying each property test results and summary of tests - - input - - list - properties is a list of small json objects containing each test , description and result - Ex - - {'description': 'assertion false', 'property': 'fmaf.assertion.1', 'status': 'SUCCESS'} - {'description': 'assertion failed: 2 == 4', 'property': 'main.assertion.1', 'status': 'FAILURE', 'trace': [{'function': {'displayName' .. - - output - - str - Final string output which is a detailed output displaying all the tests and the results - Ex - SUMMARY: - Property 53: sinf.assertion.1 - - Status: SUCCESS - - Description: "assertion false" - - Location: file/path.rs:10:8 in function harness - Property 54: calloc.assertion.1 - - Status: SUCCESS - - Description: "assertion false" - - Note: Location is missing on CBMC checks. In those cases, we omit the Location line. - """ - - number_tests_failed = 0 - number_tests_unreachable = 0 - number_tests_undetermined = 0 - output_message = "" - failed_tests = [] - verification_status = GlobalMessages.FAILED - - output_message = "RESULTS:\n" - - # for property_instance in properties: - for index, property_instance in enumerate(properties): - try: - name = property_instance["property"] - status = property_instance["status"] - description = property_instance["description"] - location = SourceLocation(property_instance.get("sourceLocation", {})) - except KeyError as e: - print("Key not present in json property", e) - - if status == "SUCCESS": - message = colored_text(Fore.GREEN, f"{status}") - elif status == "UNDETERMINED": - message = colored_text(Fore.YELLOW, f"{status}") - number_tests_undetermined += 1 - elif status == "UNREACHABLE": - message = colored_text(Fore.YELLOW, f"{status}") - number_tests_unreachable += 1 - else: - number_tests_failed += 1 - failed_tests.append(property_instance) - message = colored_text(Fore.RED, f"{status}") - - """ Ex - Property 54: calloc.assertion.1 - - Status: SUCCESS - - Description: "assertion false" """ - output_message += f"Check {index+1}: {name}\n" \ - f"\t - Status: {message}\n" \ - f"\t - Description: \"{description}\"\n" - if location: - output_message += f"\t - Location: {location}\n" - - output_message += "\n" - - output_message += f"\nSUMMARY: \n ** {number_tests_failed} of {len(properties)} failed" - other_status = [] - if number_tests_undetermined > 0: - other_status.append(f"{number_tests_undetermined} undetermined") - if number_tests_unreachable > 0: - other_status.append(f"{number_tests_unreachable} unreachable") - if other_status: - output_message += " (" - output_message += ",".join(other_status) - output_message += ")" - output_message += "\n" - - # The Verification is successful and the program is verified - if number_tests_failed == 0: - verification_status = colored_text(Fore.GREEN, "SUCCESSFUL") - else: - verification_status = colored_text(Fore.RED, "FAILED") - for failed_test in failed_tests: - # Go through traces to extract relevant information to be displayed in the summary - # only in the case of failure - try: - failure_message = failed_test["description"] - failure_source = failed_test["trace"][-1]['sourceLocation'] - failure_message_path = failure_source['file'] - failure_function_name = failure_source['function'] - failure_line_number = failure_source['line'] - output_message += f"Failed Checks: {failure_message}\n File: \"{failure_message_path}\", line {failure_line_number}, in {failure_function_name}\n" - except KeyError: - failure_source = "None" - output_message += f"Failed Checks: {failure_message}\n" - - # TODO: Change this to cProver status - # TODO: Extract information from CBMC about iterations - output_message += f"\nVERIFICATION:- {verification_status}\n" - - return output_message, number_tests_failed - -def colored_text(color, text): - """ - Only use colored text if running in a terminal to avoid dumping escape - characters - """ - if sys.stdout.isatty(): - return color + text + Style.RESET_ALL - else: - return text - - -if __name__ == "__main__": - main(sys.argv) diff --git a/scripts/kani-regression.sh b/scripts/kani-regression.sh index 90c0e84858d1..ad3a1dec8594 100755 --- a/scripts/kani-regression.sh +++ b/scripts/kani-regression.sh @@ -25,9 +25,6 @@ check-cbmc-viewer-version.py --major 3 --minor 5 # Formatting check ${SCRIPT_DIR}/kani-fmt.sh --check -# Parser tests -PYTHONPATH=${SCRIPT_DIR} python3 -m unittest ${SCRIPT_DIR}/test_cbmc_json_parser.py - # Build all packages in the workspace cargo build --workspace diff --git a/scripts/setup/macos/install_deps.sh b/scripts/setup/macos/install_deps.sh index 0484b83e1db8..697d23293752 100755 --- a/scripts/setup/macos/install_deps.sh +++ b/scripts/setup/macos/install_deps.sh @@ -15,7 +15,6 @@ brew install universal-ctags wget # Add Python package dependencies PYTHON_DEPS=( autopep8 - colorama # Used for introducing colors into terminal output ) python3 -m pip install "${PYTHON_DEPS[@]}" diff --git a/scripts/setup/ubuntu/install_deps.sh b/scripts/setup/ubuntu/install_deps.sh index 7a6269aecdfa..c3f37cbbcc7a 100755 --- a/scripts/setup/ubuntu/install_deps.sh +++ b/scripts/setup/ubuntu/install_deps.sh @@ -49,7 +49,6 @@ sudo DEBIAN_FRONTEND=noninteractive apt-get install --no-install-recommends --ye # Add Python package dependencies PYTHON_DEPS=( autopep8 - colorama # Used for introducing colors into terminal output ) python3 -m pip install "${PYTHON_DEPS[@]}" diff --git a/scripts/test_cbmc_json_parser.py b/scripts/test_cbmc_json_parser.py deleted file mode 100644 index 74820e2d4472..000000000000 --- a/scripts/test_cbmc_json_parser.py +++ /dev/null @@ -1,133 +0,0 @@ -#!/usr/bin/env python3 -# Copyright Kani Contributors -# SPDX-License-Identifier: Apache-2.0 OR MIT -import unittest -import os -import tempfile -import cbmc_json_parser -from cbmc_json_parser import SourceLocation - - -def source_json(filename=None, function=None, line=None, column=None): - result = dict() - if filename: - result["file"] = filename - if function: - result["function"] = function - if column: - result["column"] = column - if line: - result["line"] = line - return result - - -class IncorrectUsageTest(unittest.TestCase): - """ Test to ensure we correctly handle invalid arguments. """ - - def parse_with_error(self, args): - """ Util function that runs main with given arguments and checks that sys.exit(1) was called """ - with self.assertRaises(SystemExit) as err: - cbmc_json_parser.main(args) - - exception = err.exception - self.assertEqual(exception.code, 1) - - def test_missing_arguments(self): - self.parse_with_error("cbmc_json_parser.py".split()) - self.parse_with_error("cbmc_json_parser.py input.json".split()) - - def test_invalid_format(self): - self.parse_with_error("cbmc_json_parser.py input.json dummy_format".split()) - - def test_invalid_flag(self): - self.parse_with_error("cbmc_json_parser.py input.json terse --invalid-flag".split()) - - def test_too_many_args(self): - self.parse_with_error("cbmc_json_parser.py input.json terse --extra-ptr-check --extra".split()) - - -class SourceLocationTest(unittest.TestCase): - """ Unit tests for SourceLocation """ - - def test_source_location_valid_path(self): - """Path returned by filepath() works for valid paths - - Note: Check is loose because I couldn't find a reliable way to control a real path location. - """ - path = tempfile.gettempdir() - json = source_json(path) - src_loc = SourceLocation(json) - possible_output = {path, os.path.relpath(path), os.path.relpath(path, os.path.expanduser("~"))} - self.assertIn(src_loc.filepath(), possible_output) - - def test_source_location_invalid_path(self): - """Path returned by filepath() returns the input path if it doesn't exist""" - path = "/rust/made/up/path/lib.rs" - json = source_json(path) - src_loc = SourceLocation(json) - self.assertEqual(src_loc.filepath(), path) - - def test_source_location_relative_path(self): - """Path returned by filepath() is relative if the input is also relative""" - relpath = "dummy/target.rs" - json = source_json(relpath) - src_loc = SourceLocation(json) - self.assertEqual(src_loc.filepath(), relpath) - - def test_source_location_absolute_cwd_path(self): - """Path returned by filepath() is relative to current directory - - Note that the file may not exist that this should still hold. - """ - relpath = "dummy/target.rs" - path = os.path.join(os.getcwd(), relpath) - self.assertNotEqual(relpath, path) - - json = source_json(path) - src_loc = SourceLocation(json) - self.assertEqual(src_loc.filepath(), relpath) - - def test_source_location_absolute_user_path(self): - """Path returned by filepath() is relative to current directory - - Note that the file may not exist that this should still hold. - """ - relpath = "~/dummy/target.rs" - path = os.path.expanduser(relpath) - self.assertNotEqual(relpath, path) - - json = source_json(path) - src_loc = SourceLocation(json) - self.assertEqual(src_loc.filepath(), relpath) - - def test_source_location_relative_user_path(self): - """Path returned by filepath() is relative to current directory - - Note that the file may not exist that this should still hold. - """ - relpath = "~/dummy/target.rs" - json = source_json(relpath) - src_loc = SourceLocation(json) - self.assertEqual(src_loc.filepath(), relpath) - - def test_source_location_with_no_path(self): - """Function filepath() is None if no file is given in the input""" - json = source_json(function="main") - src_loc = SourceLocation(json) - self.assertIsNone(src_loc.filepath()) - - def test_source_location_output_format(self): - """Check that output includes all the information provided""" - path = "/rust/made/up/path/lib.rs" - function = "harness" - line = 10 - column = 8 - json = source_json(path, function, line, column) - src_loc = str(SourceLocation(json)) - self.assertIn(path, src_loc) - self.assertIn(f"{path}:{line}:{column}", src_loc) - self.assertIn(function, src_loc) - - -if __name__ == '__main__': - unittest.main() diff --git a/src/setup.rs b/src/setup.rs index 06bbd0b19acd..e369b0ef12e2 100644 --- a/src/setup.rs +++ b/src/setup.rs @@ -112,7 +112,7 @@ fn setup_python_deps(kani_dir: &Path, os: &os_info::Info) -> Result<()> { let pyroot = kani_dir.join("pyroot"); // TODO: this is a repetition of versions from kani/kani-dependencies - let pkg_versions = &["cbmc-viewer==3.6", "colorama==0.4.3"]; + let pkg_versions = &["cbmc-viewer==3.6"]; if os.os_type() == os_info::Type::Ubuntu // Check both versions: https://github.com/stanislav-tkach/os_info/issues/318 diff --git a/tests/cargo-ui/dry-run/expected b/tests/cargo-ui/dry-run/expected index a14e5bbdb3ab..bee6bf6d3366 100644 --- a/tests/cargo-ui/dry-run/expected +++ b/tests/cargo-ui/dry-run/expected @@ -10,4 +10,3 @@ goto-instrument --generate-function-body-options assert-false-assume-false --gen goto-instrument --ensure-one-backedge-per-target Checking harness harness... cbmc --bounds-check --pointer-check --div-by-zero-check --float-overflow-check --nan-check --undefined-shift-check --unwinding-assertions --object-bits 16 --slice-formula -debug/deps/cbmc-for-harness.out.cbmc_output diff --git a/tools/make-kani-release/license-notes.txt b/tools/make-kani-release/license-notes.txt index c2d676e94aa1..a38a7977cf4e 100644 --- a/tools/make-kani-release/license-notes.txt +++ b/tools/make-kani-release/license-notes.txt @@ -22,9 +22,6 @@ License: Apache-2.0 ## Notable Python dependencies -colorama: https://github.com/tartley/colorama -License: BSD-3-Clause - voluptuous: https://github.com/alecthomas/voluptuous License: BSD-3-Clause diff --git a/tools/make-kani-release/src/main.rs b/tools/make-kani-release/src/main.rs index aa5da20d1637..e0e420d4a8ff 100644 --- a/tools/make-kani-release/src/main.rs +++ b/tools/make-kani-release/src/main.rs @@ -81,8 +81,6 @@ fn bundle_kani(dir: &Path) -> Result<()> { let scripts = dir.join("scripts"); std::fs::create_dir(&scripts)?; - cp(Path::new("./scripts/cbmc_json_parser.py"), &scripts)?; - // 3. Kani libraries let library = dir.join("library"); std::fs::create_dir(&library)?;