feat: enable deterministic playback for variables optimized out due to --slice-formula (#1512)

* initial slice-formula stuff

* mark u8_2 as unused

* fix: change parser to accept goto_symex_return lhs

* docs: update comment

* docs: allow unused test case vars to be anything

* ui: improve leftover det vals error msg

Author: sanjit-bhat

kani-driver/src/call_cbmc.rs

@@ -117,7 +117,7 @@ impl KaniSession {
             args.push("--validate-ssa-equation".into());
         }
 
-        if !self.args.visualize && !self.args.no_slice_formula {
+        if !self.args.visualize && !self.args.gen_exe_trace && !self.args.no_slice_formula {
             args.push("--slice-formula".into());
         }
 

kani-driver/src/exe_trace.rs

@@ -250,7 +250,7 @@ struct ExeTrace {
 ///     ...,
 ///     { "description": "assertion failed: x", "status": "FAILURE", "trace": [
 ///         ...,
-///         { "assignmentType": "variable", "lhs": "var_0",
+///         { "assignmentType": "variable", "lhs": "goto_symex$$return_value...",
 ///           "sourceLocation": { "function": "kani::any_raw_internal::<u8, 1_usize>" },
 ///           "stepType": "assignment", "value": { "binary": "00000001", "data": "101", "width": 8 } }
 ///         ..., ] }
@@ -371,7 +371,7 @@ mod parser {
             trace_entry["value"]["width"].as_u64(),
         ) {
             if step_type == "assignment"
-                && lhs == "var_0"
+                && lhs.starts_with("goto_symex$$return_value")
                 && func.starts_with("kani::any_raw_internal")
             {
                 let declared_width = width_u64 as usize;

library/kani/src/exe_trace.rs

@@ -24,6 +24,20 @@ pub fn exe_trace_run<F: Fn()>(mut local_det_vals: Vec<Vec<u8>>, proof_harness: F
     });
     // Since F is a type argument, there should be a direct, static call to proof_harness().
     proof_harness();
+    // This code will not run if a user assertion fails on deterministic playback.
+    // But if you comment out the failing assertion during playback,
+    // this can be used to know if too many det vals were loaded into the deterministic test case.
+    DET_VALS.with(|glob_det_vals| {
+        let ref_glob_det_vals = &*glob_det_vals.borrow();
+        assert!(
+            ref_glob_det_vals.is_empty(),
+            "At the end of deterministic playback, there were still these deterministic values left over `{:?}`. \
+            This either happened because: \
+            1) Your code/harness changed after you generated this deterministic test. \
+            2) There's a bug in Kani. Please report the issue here: <https://github.com/model-checking/kani/issues/new?assignees=&labels=bug&template=bug_report.md>",
+            ref_glob_det_vals
+        );
+    });
 }
 
 /// Executable trace implementation of kani::any_raw_internal.

tests/ui/exe-trace/slice-formula/expected

@@ -0,0 +1,20 @@
+VERIFICATION:- FAILED
+
+Executable trace
+```
+#[test]
+fn kani_exe_trace_harness
+    let det_vals: Vec<Vec<u8>> = vec![
+        //
+        vec![
+        // 101
+        vec![101, 0],
+        //
+        vec![
+        // 102ul
+        vec![102, 0, 0, 0, 0, 0, 0, 0]
+    ];
+    kani::exe_trace_run(det_vals, harness);
+}
+```
+

tests/ui/exe-trace/slice-formula/main.rs

@@ -0,0 +1,16 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// kani-flags: --harness harness --enable-unstable --gen-exe-trace
+
+//! We explicitly don't check what concrete values are returned for `_u8_1` and `_u8_3` as they could be anything.
+//! In practice, though, they will likely be 0.
+
+#[kani::proof]
+pub fn harness() {
+    let _u8_1: u8 = kani::any();
+    let u8_2: u16 = kani::any();
+    let _u8_3: u32 = kani::any();
+    let u8_4: u64 = kani::any();
+    assert!(!(u8_2 == 101 && u8_4 == 102));
+}