feat: make kani::any::<bool>() non-det bit pattern more intuitive (r…

…ust-lang#1539)

* feat: update any bool func

* tests: added more paths to exe-trace tests that use bool

library/kani/src/arbitrary.rs

@@ -49,7 +49,8 @@ impl Arbitrary for bool {
     #[inline(always)]
     fn any() -> Self {
         let byte = u8::any();
-        byte == 0
+        crate::assume(byte < 2);
+        byte == 1
     }
 }
 

tests/ui/exe-trace/bool/expected

@@ -6,7 +6,9 @@ Executable trace
 fn kani_exe_trace_harness
     let det_vals: Vec<Vec<u8>> = vec![
         // 0
-        vec![0
+        vec![0],
+        // 1
+        vec![1]
     ];
     kani::exe_trace_run(det_vals, harness);
 }

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

@@ -3,9 +3,9 @@
 
 // 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);
+    let bool_2: bool = kani::any();
+    assert!(!(!bool_1 && bool_2));
 }

tests/ui/exe-trace/option/expected

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

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

@@ -3,12 +3,9 @@
 
 // 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));
+    let option_2: Option<u8> = kani::any();
+    assert!(!(option_1 == Some(101) && option_2 == None));
 }

tests/ui/exe-trace/result/expected

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

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

@@ -3,12 +3,9 @@
 
 // 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));
+    let result_2: Result<u8, u8> = kani::any();
+    assert!(!(result_1 == Ok(101) && result_2 == Err(102)));
 }