tests: add tests for deterministic playback of the remaining primitive types (rust-lang#1488)

* feat: add bool test

* feat: add nonzerou8 test

* feat: add array test

* feat: add result test

* feat: add option test

* feat: add custom test

* refactor: rename non_zero_u8 to non_zero

* chore: add newlines to all test files

* docs: make test case notes docstrings

Author: sanjit-bhat

tests/ui/exe-trace/array/expected

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

tests/ui/exe-trace/array/main.rs

@@ -0,0 +1,11 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// kani-flags: --harness harness --enable-unstable --gen-exe-trace
+
+#[kani::proof]
+#[kani::unwind(10)]
+pub fn harness() {
+    let arr_1: [u8; 2] = kani::any();
+    assert!(!(arr_1[0] == 101 && arr_1[1] == 102));
+}

tests/ui/exe-trace/bool/expected

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

tests/ui/exe-trace/bool/main.rs

@@ -0,0 +1,11 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// kani-flags: --harness harness --enable-unstable --gen-exe-trace
+
+/// Note: We can't test a false value yet because any::<bool>() could be any non-zero number.
+#[kani::proof]
+pub fn harness() {
+    let bool_1: bool = kani::any();
+    assert!(bool_1 != true);
+}

tests/ui/exe-trace/custom/expected

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

tests/ui/exe-trace/custom/main.rs

@@ -0,0 +1,21 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// kani-flags: --harness harness --enable-unstable --gen-exe-trace
+
+struct MyStruct {
+    field1: u8,
+    field2: u16,
+}
+
+impl kani::Arbitrary for MyStruct {
+    fn any() -> Self {
+        MyStruct { field1: kani::any(), field2: kani::any() }
+    }
+}
+
+#[kani::proof]
+pub fn harness() {
+    let my_struct: MyStruct = kani::any();
+    assert!(!(my_struct.field1 == 101 && my_struct.field2 == 102));
+}

tests/ui/exe-trace/f32/expected

@@ -24,4 +24,4 @@ fn kani_exe_trace_harness
     ];
     kani::exe_trace_run(det_vals, harness);
 }
-```
+```

tests/ui/exe-trace/f32/main.rs

@@ -3,6 +3,7 @@
 
 // kani-flags: --harness harness --enable-unstable --gen-exe-trace
 
+/// Note: Don't include NaN because there are multiple possible NaN values.
 #[kani::proof]
 pub fn harness() {
     let f32_1: f32 = kani::any();
@@ -23,5 +24,4 @@ pub fn harness() {
             && f32_7 == f32::MAX
             && f32_8 == f32::INFINITY)
     );
-    // Note: Don't include NaN because there are multiple possible NaN values.
 }

tests/ui/exe-trace/f64/expected

@@ -24,4 +24,4 @@ fn kani_exe_trace_harness
     ];
     kani::exe_trace_run(det_vals, harness);
 }
-```
+```

tests/ui/exe-trace/f64/main.rs

@@ -3,6 +3,7 @@
 
 // kani-flags: --harness harness --enable-unstable --gen-exe-trace
 
+/// Note: Don't include NaN because there are multiple possible NaN values.
 #[kani::proof]
 pub fn harness() {
     let f64_1: f64 = kani::any();
@@ -23,5 +24,4 @@ pub fn harness() {
             && f64_7 == f64::MAX
             && f64_8 == f64::INFINITY)
     );
-    // Note: Don't include NaN because there are multiple possible NaN values.
 }

tests/ui/exe-trace/i128/expected

@@ -18,4 +18,4 @@ fn kani_exe_trace_harness
     ];
     kani::exe_trace_run(det_vals, harness);
 }
-```
+```

tests/ui/exe-trace/i16/expected

@@ -18,4 +18,4 @@ fn kani_exe_trace_harness
     ];
     kani::exe_trace_run(det_vals, harness);
 }
-```
+```

tests/ui/exe-trace/i32/expected

@@ -18,4 +18,4 @@ fn kani_exe_trace_harness
     ];
     kani::exe_trace_run(det_vals, harness);
 }
-```
+```

tests/ui/exe-trace/i64/expected

@@ -18,4 +18,4 @@ fn kani_exe_trace_harness
     ];
     kani::exe_trace_run(det_vals, harness);
 }
-```
+```

tests/ui/exe-trace/i8/expected

@@ -18,4 +18,4 @@ fn kani_exe_trace_harness
     ];
     kani::exe_trace_run(det_vals, harness);
 }
-```
+```

tests/ui/exe-trace/isize/expected

@@ -18,4 +18,4 @@ fn kani_exe_trace_harness
     ];
     kani::exe_trace_run(det_vals, harness);
 }
-```
+```

tests/ui/exe-trace/non_zero/expected

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

tests/ui/exe-trace/non_zero/main.rs

@@ -0,0 +1,20 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// kani-flags: --harness harness --enable-unstable --gen-exe-trace
+
+use std::num::NonZeroU8;
+
+#[kani::proof]
+pub fn harness() {
+    let non_zero_u8_1: NonZeroU8 = kani::any();
+    let non_zero_u8_2: NonZeroU8 = kani::any();
+    let non_zero_u8_3: NonZeroU8 = kani::any();
+    unsafe {
+        assert!(
+            !(non_zero_u8_1 == NonZeroU8::new_unchecked(1)
+                && non_zero_u8_2 == NonZeroU8::new_unchecked(101)
+                && non_zero_u8_3 == NonZeroU8::new_unchecked(255))
+        );
+    }
+}

tests/ui/exe-trace/option/expected

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

tests/ui/exe-trace/option/main.rs

@@ -0,0 +1,14 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// kani-flags: --harness harness --enable-unstable --gen-exe-trace
+
+/// This should generate 2 bools.
+/// The first should be 0 because the Option type is Some.
+/// The second should be 101, the inner value of the Some.
+/// Note: We can't test on a None type yet because the first any::<bool>() could be any non-zero number.
+#[kani::proof]
+pub fn harness() {
+    let option_1: Option<u8> = kani::any();
+    assert!(option_1 != Some(101));
+}

tests/ui/exe-trace/result/expected

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

tests/ui/exe-trace/result/main.rs

@@ -0,0 +1,14 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// kani-flags: --harness harness --enable-unstable --gen-exe-trace
+
+/// This should generate 2 bools.
+/// The first should be 0 because the Result type is Ok.
+/// The second should be 101, the inner value of the Ok.
+/// Note: We can't test an Err type yet because the first any::<bool>() could be any non-zero number.
+#[kani::proof]
+pub fn harness() {
+    let result_1: Result<u8, u8> = kani::any();
+    assert!(result_1 != Ok(101));
+}

tests/ui/exe-trace/u128/expected

@@ -14,4 +14,4 @@ fn kani_exe_trace_harness
     ];
     kani::exe_trace_run(det_vals, harness);
 }
-```
+```

tests/ui/exe-trace/u16/expected

@@ -14,4 +14,4 @@ fn kani_exe_trace_harness
     ];
     kani::exe_trace_run(det_vals, harness);
 }
-```
+```

tests/ui/exe-trace/u32/expected

@@ -14,4 +14,4 @@ fn kani_exe_trace_harness
     ];
     kani::exe_trace_run(det_vals, harness);
 }
-```
+```

tests/ui/exe-trace/u64/expected

@@ -14,4 +14,4 @@ fn kani_exe_trace_harness
     ];
     kani::exe_trace_run(det_vals, harness);
 }
-```
+```

tests/ui/exe-trace/u8/expected

@@ -14,4 +14,4 @@ fn kani_exe_trace_harness
     ];
     kani::exe_trace_run(det_vals, harness);
 }
-```
+```

tests/ui/exe-trace/usize/expected

@@ -14,4 +14,4 @@ fn kani_exe_trace_harness
     ];
     kani::exe_trace_run(det_vals, harness);
 }
-```
+```