refactor: rename exe_trace to concrete_playback and det_vals to concrete_vals (rust-lang#1548)

* rename a bunch of stuff

* rename JustPrint to Print

Author: sanjit-bhat

kani-driver/src/args.rs

@@ -43,18 +43,17 @@ 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.
+    /// Generate concrete playback unit test and either 1) just print it to stdout or 2) add it in-place to the source code.
     /// This option does not work with `--output-format old`.
     #[structopt(
         long,
         requires("enable-unstable"),
         requires("harness"),
         conflicts_with_all(&["visualize", "dry-run"]),
+        possible_values = &ConcretePlaybackMode::variants(),
+        case_insensitive = true,
     )]
-    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,
+    pub concrete_playback: Option<ConcretePlaybackMode>,
     /// Keep temporary files generated throughout Kani process
     #[structopt(long, hidden_short_help(true))]
     pub keep_temps: bool,
@@ -206,6 +205,14 @@ impl KaniArgs {
     }
 }
 
+arg_enum! {
+    #[derive(Debug, PartialEq, Eq)]
+    pub enum ConcretePlaybackMode {
+        Print,
+        InPlace,
+    }
+}
+
 arg_enum! {
     #[derive(Debug, PartialEq, Eq)]
     pub enum OutputFormat {

kani-driver/src/call_cbmc.rs

@@ -52,7 +52,7 @@ impl KaniSession {
                 // 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 };
+                    self.args.concrete_playback.as_ref().map(|_| output_filename.as_path());
                 let processed_result = process_cbmc_output(
                     cbmc_process,
                     self.args.extra_pointer_checks,
@@ -71,7 +71,7 @@ impl KaniSession {
         }
 
         if let Ok(VerificationStatus::Failure) = verification_result {
-            self.gen_and_add_exe_trace(&output_filename, harness);
+            self.gen_and_add_concrete_playback(&output_filename, harness);
         }
 
         verification_result
@@ -117,11 +117,14 @@ impl KaniSession {
             args.push("--validate-ssa-equation".into());
         }
 
-        if !self.args.visualize && !self.args.gen_exe_trace && !self.args.no_slice_formula {
+        if !self.args.visualize
+            && self.args.concrete_playback.is_none()
+            && !self.args.no_slice_formula
+        {
             args.push("--slice-formula".into());
         }
 
-        if self.args.gen_exe_trace {
+        if self.args.concrete_playback.is_some() {
             args.push("--trace".into());
         }
 

kani-driver/src/cbmc_output_parser.rs

@@ -354,8 +354,8 @@ 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.
+    /// This is needed for old parsers (e.g., like the one in the concrete playback code) that require the actual CBMC output file.
+    /// TODO: This can be removed once we overhaul the concrete playback parser.
     /// See this tracking issue: <https://github.com/model-checking/kani/issues/1477>.
     cbmc_out_buf_writer: Option<BufWriter<File>>,
 }