Executable trace feature (#1409)

* feat: prototype E2E mechanism for gen det vals and running exec trace

This was formed by squashing the following commits:

feat: exec-trace POC that gets kani::any assignments

feat: init work making exec_trace a Kani command line flag

feat: make trace parsing more precise

feat: allow for multiple extracted values

feat: Move parsing code into the driver

refactor: move functions outside KaniSession

test: add basic UI test for det val

feat: change any_raw to make it easier to parse trace

feat: update any_raw to use byte array

feat: update parser to take in byte array

chore: run rustfmt

test: add constant generic bound to func abstraction tests

test: fix remaining test issues to pass regression

feat: update any_raw_inner to return bytes

chore: remove spurious results file

feat: update any_raw_inner to read from det_vals file

feat: add exec_trace flag to kani-compiler

refactor(kani-compiler): rename vars to increase readability

feat(kani-compiler): specify different Kani lib paths

feat: prototype E2E mechanism for gen det vals & running exec trace

fix: add generic const trait bounds to any_vec

feat: add print out to get debug command

chore: remove det vals from tmp file list for demo

* feat: towards printing unit test case

* feat: add source modification feature

* refactor: lots of it

* feat: call cbmc only once

* add back exe trace and fix unit test line numbers

* refactor: create exe trace main

* chore: revert kani-compiler changes

* fix: update parser for new cbmc trace format

* refactor: change contains to starts_with for perf

* chore: revert check-output change

* feat: put Kani lib exe trace code behind a feature

* tests: fix one-assert test

* feat: add more code under exe_trace feat

* fix: reverse det vals list since we're popping off vals

* feat: add exe_trace impls for other kani lib funcs

* fix: assertion failed may not always be failure

* fix: strict string equality actually works

* feat: add fields to get the end of a func

* feat: insert exe trace after harness

* refactor: rename everything to exe_trace instead of exec_trace

* refactor: move funcs out of kani session and remove pub visibility

* refactor: move some code into parser module

* refactor: remove generic const any_raw_inner since it will only be called on ints after Celina's PR

* fix: remove 1 TODO and make 1 func priv

* fix: add newline to cargo toml

* feat: switch to using Vec<Vec<u8>>

* feat: add comment in exe trace with interp det val

* refactor: extend iterator

* feat: don't insert same exe trace twice

* feat: add kani lib func to init det vals

* tests: forgot to add generic const stuff back into tests

* tests: forgot about one-assert going back to normal

* feat: add exe trace functionality for kani standalone

* tests: add kani overall test

* tests: forgot to add the exe trace test dir

* chore: add safety msg back in

* some more tests work

* fix: clippy and license checks

* tests: exe-trace test covers more primitives

* docs: add func comments

* small changes

* docs: add comments

* refactor: use named params in format strings

* fix: update generic const invariants in kani lib after arbitrary change

* fix: change parser to accomodate kani lib arbitrary changes

* docs: add test case comment

* docs: make arg comment a bit nicer

* refactor: generalize rustfmt func in a nice way

* feat: add any_raw_inner to more reliably get CBMC output. Also clarify test case semantics

* feat: better formatting of printed test case

* test: split tests into different directories per primitive

* test: add f32, f64 tests

* test: add comment about f32/f64 NaN values

* docs: add better explanations for generic_const_exprs feature

* refactor: rename parser funcs

* feat: convert DET_VALS to static mut

* feat: add lock around det vals for thread safety, update playback api to exe_trace_run

* address some of Celina's PR comments

* one way of implementing file reads using String vectors

* refactor: different way of implementing src code modification, all as big strings

* feat: hide exe traces under quiet flag

* refactor: generate output filename once

* feat: add more arg exclusions

* refactor: call exe_trace_main inside run_cbmc

* ui: add more info to concrete-mode assertion conversions

* refactor: as much as possible, move Kani lib exe trace code to separate module

* refactor: add kani::any_raw_internal exe_trace impl to sep mod also

* refactor: replace whitespace with constant

* refactor: add ExeTrace and DetVal structs

* refactor, docs: rename bunch of funcs and add CBMC output format

* refactor: remove as_slice

* refactor: split up big if let in parser

* fix: small typo that printed out test name instead of actual test

* ui: make exe trace exists in src code comment more specific

* feat: add anyhow error handling to CBMC trace parser

* feat: add anyhow error handling to rest of kani driver exe_trace file

* fix: clippy to_string display lints

* feat: remove extra string allocation for new src file

* ui: don't abreviate exe trace

* docs: add todo for new parser

* ui: add error handling for multiple diff asserts and checks

* ui: add warning for adding unit tests for multiple failing harnesses

* refactor: move have_parsed_assert_fail into parser glob var

* refactor: make DET_VALS a thread_local static refcell

* fix: had incorrect type info in the refcell changes

* fix: changed exe_trace::any_raw_internal to pub crate

* feat: add error handling around using any_raw funcs and switch to if cfg bang feature

* ui: add assert around --output-format old

* fix: make exe_trace mod private

* refactor: change over to if cfg exe_trace instead of cfg exe_trace macro

* refactor: require harness arg -> make have_parsed_assert_fail local to a single harness

* fix: in CBMC output parser, write CBMC output to file if using exe_trace flag. This is for old exe_trace parser compatibility

* lints: add carrots around URLs to fix clippy warning

* refactor: move buf writer inside parser, but there's still an ownership issue

* fix: the cbmc output parser ownership issue

* fix: address PR comments around cbmc output parser changes

Co-authored-by: Celina G. Val <celinval@amazon.com>

Author: sanjit-bhat

cprover_bindings/src/goto_program/location.rs

@@ -13,7 +13,14 @@ pub enum Location {
     BuiltinFunction { function_name: InternedString, line: Option<u64> },
     /// Location in user code.
     /// `function` is `None` for global, `Some(function_name)` for function local.
-    Loc { file: InternedString, function: Option<InternedString>, line: u64, col: Option<u64> },
+    Loc {
+        file: InternedString,
+        function: Option<InternedString>,
+        start_line: u64,
+        start_col: Option<u64>,
+        end_line: u64,
+        end_col: Option<u64>,
+    },
     /// Location for Statements that use Property Class and Description - Assert, Assume, Cover etc.
     Property {
         file: InternedString,
@@ -50,9 +57,16 @@ impl Location {
         }
     }
 
-    pub fn line(&self) -> Option<u64> {
+    pub fn start_line(&self) -> Option<u64> {
         match self {
-            Location::Loc { line, .. } => Some(*line),
+            Location::Loc { start_line, .. } => Some(*start_line),
+            _ => None,
+        }
+    }
+
+    pub fn end_line(&self) -> Option<u64> {
+        match self {
+            Location::Loc { end_line, .. } => Some(*end_line),
             _ => None,
         }
     }
@@ -68,7 +82,7 @@ impl Location {
             Location::BuiltinFunction { function_name, line: None } => {
                 format!("<{}>", function_name)
             }
-            Location::Loc { file, line, .. } => format!("{}:{}", file, line),
+            Location::Loc { file, start_line: line, .. } => format!("{}:{}", file, line),
             Location::Property { file, line, .. } => {
                 format!("<{:?}>:{}", file, line)
             }
@@ -82,18 +96,29 @@ impl Location {
     pub fn new<T, U: Into<InternedString>, V: Into<InternedString>>(
         file: U,
         function: Option<V>,
-        line: T,
-        col: Option<T>,
+        start_line: T,
+        start_col: Option<T>,
+        end_line: T,
+        end_col: Option<T>,
     ) -> Location
     where
         T: TryInto<u64>,
         T::Error: Debug,
     {
-        let file = file.into();
-        let line = line.try_into().unwrap();
-        let col = col.map(|x| x.try_into().unwrap());
-        let function = function.intern();
-        Location::Loc { file, function, line, col }
+        let file_into = file.into();
+        let start_line_into = start_line.try_into().unwrap();
+        let start_col_into = start_col.map(|x| x.try_into().unwrap());
+        let end_line_into = end_line.try_into().unwrap();
+        let end_col_into = end_col.map(|x| x.try_into().unwrap());
+        let function_into = function.intern();
+        Location::Loc {
+            file: file_into,
+            function: function_into,
+            start_line: start_line_into,
+            start_col: start_col_into,
+            end_line: end_line_into,
+            end_col: end_col_into,
+        }
     }
 
     /// Create a Property type Location
@@ -134,14 +159,16 @@ impl Location {
                 comment.into(),
                 property_name.into(),
             ),
-            Location::Loc { file, function, line, col } => Location::property_location(
-                file.into(),
-                function.intern(),
-                line,
-                col,
-                comment.into(),
-                property_name.into(),
-            ),
+            Location::Loc { file, function, start_line, start_col, end_line: _, end_col: _ } => {
+                Location::property_location(
+                    file.into(),
+                    function.intern(),
+                    start_line,
+                    start_col,
+                    comment.into(),
+                    property_name.into(),
+                )
+            }
             Location::Property { .. } => location,
             Location::PropertyUnknownLocation { .. } => location,
             // This converts None type Locations to PropertyUnknownLocation type which inserts Property Class and Description

cprover_bindings/src/irep/to_irep.rs

@@ -351,12 +351,14 @@ impl ToIrep for Location {
                 (IrepId::Function, Irep::just_string_id(function_name.to_string())),
             ])
             .with_named_sub_option(IrepId::Line, line.map(Irep::just_int_id)),
-            Location::Loc { file, function, line, col } => Irep::just_named_sub(linear_map![
-                (IrepId::File, Irep::just_string_id(file.to_string())),
-                (IrepId::Line, Irep::just_int_id(*line)),
-            ])
-            .with_named_sub_option(IrepId::Column, col.map(Irep::just_int_id))
-            .with_named_sub_option(IrepId::Function, function.map(Irep::just_string_id)),
+            Location::Loc { file, function, start_line, start_col, end_line: _, end_col: _ } => {
+                Irep::just_named_sub(linear_map![
+                    (IrepId::File, Irep::just_string_id(file.to_string())),
+                    (IrepId::Line, Irep::just_int_id(*start_line)),
+                ])
+                .with_named_sub_option(IrepId::Column, start_col.map(Irep::just_int_id))
+                .with_named_sub_option(IrepId::Function, function.map(Irep::just_string_id))
+            }
             Location::Property { file, function, line, col, property_class, comment } => {
                 Irep::just_named_sub(linear_map![
                     (IrepId::File, Irep::just_string_id(file.to_string())),

kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs

@@ -316,7 +316,8 @@ impl<'tcx> GotocCtx<'tcx> {
             pretty_name,
             mangled_name,
             original_file: loc.filename().unwrap(),
-            original_line: loc.line().unwrap().to_string(),
+            original_start_line: loc.start_line().unwrap().to_string(),
+            original_end_line: loc.end_line().unwrap().to_string(),
             unwind_value: None,
         }
     }

kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs

@@ -12,8 +12,11 @@ impl<'tcx> GotocCtx<'tcx> {
     pub fn codegen_span(&self, sp: &Span) -> Location {
         let smap = self.tcx.sess.source_map();
         let lo = smap.lookup_char_pos(sp.lo());
-        let line = lo.line;
-        let col = 1 + lo.col_display;
+        let start_line = lo.line;
+        let start_col = 1 + lo.col_display;
+        let hi = smap.lookup_char_pos(sp.hi());
+        let end_line = hi.line;
+        let end_col = 1 + hi.col_display;
         let filename0 = lo.file.name.prefer_local().to_string_lossy().to_string();
         let filename1 = match std::fs::canonicalize(filename0.clone()) {
             Ok(pathbuf) => pathbuf.to_str().unwrap().to_string(),
@@ -22,8 +25,10 @@ impl<'tcx> GotocCtx<'tcx> {
         Location::new(
             filename1,
             self.current_fn.as_ref().map(|x| x.readable_name().to_string()),
-            line,
-            Some(col),
+            start_line,
+            Some(start_col),
+            end_line,
+            Some(end_col),
         )
     }
 

kani-driver/src/args.rs

@@ -43,6 +43,18 @@ pub struct KaniArgs {
     /// Generate visualizer report to <target-dir>/report/html/index.html
     #[structopt(long)]
     pub visualize: bool,
+    /// Generate executable trace test case and print it to stdout.
+    /// This option does not work with `--output-format old`.
+    #[structopt(
+        long,
+        requires("enable-unstable"),
+        requires("harness"),
+        conflicts_with_all(&["visualize", "dry-run"]),
+    )]
+    pub gen_exe_trace: bool,
+    /// Additionally add executable trace test case to the source code
+    #[structopt(long, requires("gen-exe-trace"))]
+    pub add_exe_trace_to_src: bool,
     /// Keep temporary files generated throughout Kani process
     #[structopt(long, hidden_short_help(true))]
     pub keep_temps: bool,

kani-driver/src/call_cbmc.rs

@@ -22,10 +22,9 @@ impl KaniSession {
     /// Verify a goto binary that's been prepared with goto-instrument
     pub fn run_cbmc(&self, file: &Path, harness: &HarnessMetadata) -> Result<VerificationStatus> {
         let output_filename = crate::util::append_path(file, "cbmc_output");
-
         {
             let mut temps = self.temporaries.borrow_mut();
-            temps.push(output_filename);
+            temps.push(output_filename.clone());
         }
 
         let args: Vec<OsString> = self.cbmc_flags(file, harness)?;
@@ -52,10 +51,13 @@ impl KaniSession {
             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 output_filename_opt: Option<&Path> =
+                    if self.args.gen_exe_trace { Some(&output_filename) } else { None };
                 let processed_result = process_cbmc_output(
                     cbmc_process,
                     self.args.extra_pointer_checks,
                     &self.args.output_format,
+                    output_filename_opt,
                 );
                 Ok(processed_result)
             } else {
@@ -68,6 +70,10 @@ impl KaniSession {
             println!("Verification Time: {}s", elapsed);
         }
 
+        if let Ok(VerificationStatus::Failure) = verification_result {
+            self.gen_and_add_exe_trace(&output_filename, harness);
+        }
+
         verification_result
     }
 
@@ -115,6 +121,10 @@ impl KaniSession {
             args.push("--slice-formula".into());
         }
 
+        if self.args.gen_exe_trace {
+            args.push("--trace".into());
+        }
+
         args.extend(self.args.cbmc_args.iter().cloned());
 
         args.push(file.to_owned().into_os_string());

kani-driver/src/cbmc_output_parser.rs

@@ -29,8 +29,9 @@ use serde::Deserialize;
 use std::{
     collections::HashMap,
     env,
-    io::{BufRead, BufReader},
-    path::PathBuf,
+    fs::File,
+    io::{BufRead, BufReader, BufWriter, Write},
+    path::{Path, PathBuf},
     process::{Child, ChildStdout},
 };
 
@@ -351,11 +352,26 @@ enum Action {
 struct Parser<'a, 'b> {
     pub input_so_far: String,
     pub buffer: &'a mut BufReader<&'b mut ChildStdout>,
+    /// Buffered writer over the CBMC output file.
+    /// This is needed for old parsers (e.g., like the one in the executable trace code) that require the actual CBMC output file.
+    /// TODO: This can be removed once we overhaul the executable trace parser.
+    /// See this tracking issue: <https://github.com/model-checking/kani/issues/1477>.
+    cbmc_out_buf_writer: Option<BufWriter<File>>,
 }
 
 impl<'a, 'b> Parser<'a, 'b> {
-    pub fn new(buffer: &'a mut BufReader<&'b mut ChildStdout>) -> Self {
-        Parser { input_so_far: String::new(), buffer }
+    pub fn new(
+        buffer: &'a mut BufReader<&'b mut ChildStdout>,
+        output_filename_opt: Option<&Path>,
+    ) -> Self {
+        let cbmc_out_buf_writer = output_filename_opt.map(|output_filename| {
+            let cbmc_out_file = File::create(output_filename).expect(&format!(
+                "In CBMC output parser, couldn't create CBMC output file `{}`",
+                output_filename.display()
+            ));
+            BufWriter::new(cbmc_out_file)
+        });
+        Parser { input_so_far: String::new(), buffer, cbmc_out_buf_writer }
     }
 
     /// Triggers an action based on the input:
@@ -423,6 +439,7 @@ impl<'a, 'b> Parser<'a, 'b> {
     /// 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<ParserItem> {
+        self.add_line_to_buf_writer(&input);
         self.add_to_input(input.clone());
         let action_required = self.triggers_action(input);
         if let Some(action) = action_required {
@@ -431,6 +448,26 @@ impl<'a, 'b> Parser<'a, 'b> {
         }
         None
     }
+
+    /// Adds a single line to the CBMC output buffered writer.
+    pub fn add_line_to_buf_writer(&mut self, line: &str) {
+        if let Some(buf_writer) = self.cbmc_out_buf_writer.as_mut() {
+            write!(buf_writer, "{}", line).expect(&format!(
+                "In CBMC output parser, couldn't write `{}` to CBMC output buffered writer",
+                line
+            ));
+        }
+    }
+
+    /// Flushes the CBMC output buffered writer.
+    /// This should be called after the parser has processed the entire CBMC output.
+    pub fn flush_buf_writer(&mut self) {
+        if let Some(buf_writer) = self.cbmc_out_buf_writer.as_mut() {
+            buf_writer.flush().expect(
+                "In CBMC output parser, couldn't flush buffered writer to CBMC output file",
+            );
+        }
+    }
 }
 
 /// The iterator implementation for `Parser` reads the buffer line by line,
@@ -443,6 +480,7 @@ impl<'a, 'b> Iterator for Parser<'a, 'b> {
             match self.buffer.read_line(&mut input) {
                 Ok(len) => {
                     if len == 0 {
+                        self.flush_buf_writer();
                         return None;
                     }
                     let item = self.process_line(input);
@@ -510,10 +548,11 @@ pub fn process_cbmc_output(
     mut process: Child,
     extra_ptr_checks: bool,
     output_format: &OutputFormat,
+    output_filename_opt: Option<&Path>,
 ) -> VerificationStatus {
     let stdout = process.stdout.as_mut().unwrap();
     let mut stdout_reader = BufReader::new(stdout);
-    let parser = Parser::new(&mut stdout_reader);
+    let parser = Parser::new(&mut stdout_reader, output_filename_opt);
     let mut result = false;
 
     for item in parser {
@@ -532,6 +571,7 @@ pub fn process_cbmc_output(
         // TODO: Record processed items and dump them into a JSON file
         // <https://github.com/model-checking/kani/issues/942>
     }
+
     if result { VerificationStatus::Success } else { VerificationStatus::Failure }
 }