Merge pull request #26 from os-checker/test-proofs

Test: add new tests for proofs behaviors

Author: zjp-CN

.gitignore

@@ -1 +1,4 @@
 /target
+
+# ignore kani folder for grep or files findings
+# kani

tests/proofs.rs

@@ -18,6 +18,7 @@ fn test_proofs() -> eyre::Result<()> {
         [
             "tests/proofs/standard_proofs_with_contracts.rs",
             "tests/proofs/standard_proofs.rs",
+            "tests/proofs/ad_hoc.rs",
         ]
     "#]]
     .assert_debug_eq(&proofs);

tests/proofs/ad_hoc.rs

@@ -0,0 +1,23 @@
+#[cfg(kani)]
+mod adhoc {
+    #[kani::proof]
+    fn callee_defined_in_proof() {
+        fn f() -> u8 {
+            1
+        }
+        assert!(f() == 1);
+    }
+
+    #[kani::proof]
+    fn closure_in_proof() {
+        let f = || 1;
+        assert!(f() == 1);
+    }
+
+    fn proof_in_fn_item() {
+        #[kani::proof]
+        fn proof() {
+            assert!(kani::any::<u8>() == 1);
+        }
+    }
+}

tests/proofs/standard_proofs_with_contracts.rs

@@ -4,7 +4,7 @@ mod verify {
     fn contract_requires(a: u8) {}
 
     #[kani::proof]
-    fn standard_proof_with_contract_requires() {
+    fn single_contract_requires() {
         contract_requires(0);
     }
 
@@ -14,7 +14,25 @@ mod verify {
     }
 
     #[kani::proof]
-    fn standard_proof_with_contract_ensures() {
+    fn single_with_contract_ensures() {
         contract_ensures(0);
     }
+
+    #[kani::proof]
+    fn two_contracts_requires_and_ensures() {
+        let val = contract_ensures(0);
+        contract_ensures(val);
+    }
+
+    #[kani::requires(a > 0)]
+    #[kani::ensures(|&ret| ret > 0)]
+    fn contract(a: u8) -> u8 {
+        a
+    }
+
+    #[kani::proof]
+    fn single_contract() {
+        let val = contract(1);
+        assert!(val > 0);
+    }
 }

tests/snapshots/ad_hoc.json

@@ -0,0 +1,85 @@
+[
+  {
+    "hash": "952175153267326104817555187587143859995",
+    "def_id": "DefId { id: 0, name: \"adhoc::callee_defined_in_proof\" }",
+    "file": "tests/proofs/ad_hoc.rs",
+    "attrs": [
+      "#[kanitool::proof]"
+    ],
+    "func": "fn callee_defined_in_proof() {\n        fn f() -> u8 {\n            1\n        }\n        assert!(f() == 1);\n    }",
+    "callees": [
+      {
+        "def_id": "DefId { id: 6, name: \"kani::assert\" }",
+        "file": "kani/library/kani_core/src/lib.rs",
+        "func": "pub const fn assert(cond: bool, msg: &'static str) {\n            let _ = cond;\n            let _ = msg;\n        }"
+      },
+      {
+        "def_id": "DefId { id: 1, name: \"adhoc::callee_defined_in_proof::f\" }",
+        "file": "tests/proofs/ad_hoc.rs",
+        "func": "fn f() -> u8 {\n            1\n        }"
+      }
+    ]
+  },
+  {
+    "hash": "75621983092344117614099719256493026487",
+    "def_id": "DefId { id: 2, name: \"adhoc::closure_in_proof\" }",
+    "file": "tests/proofs/ad_hoc.rs",
+    "attrs": [
+      "#[kanitool::proof]"
+    ],
+    "func": "fn closure_in_proof() {\n        let f = || 1;\n        assert!(f() == 1);\n    }",
+    "callees": [
+      {
+        "def_id": "DefId { id: 6, name: \"kani::assert\" }",
+        "file": "kani/library/kani_core/src/lib.rs",
+        "func": "pub const fn assert(cond: bool, msg: &'static str) {\n            let _ = cond;\n            let _ = msg;\n        }"
+      },
+      {
+        "def_id": "DefId { id: 3, name: \"adhoc::closure_in_proof::{closure#0}\" }",
+        "file": "tests/proofs/ad_hoc.rs",
+        "func": "|| 1"
+      }
+    ]
+  },
+  {
+    "hash": "767440852073129240514318853477184375838",
+    "def_id": "DefId { id: 5, name: \"adhoc::proof_in_fn_item::proof\" }",
+    "file": "tests/proofs/ad_hoc.rs",
+    "attrs": [
+      "#[kanitool::proof]"
+    ],
+    "func": "fn proof() {\n            assert!(kani::any::<u8>() == 1);\n        }",
+    "callees": [
+      {
+        "def_id": "DefId { id: 10, name: \"<u8 as kani::Arbitrary>::any\" }",
+        "file": "kani/library/kani_core/src/arbitrary.rs",
+        "func": "fn any() -> Self {\n                        // This size_of call does not use generic_const_exprs feature. It's inside a macro, and Self isn't generic.\n                        unsafe { crate::kani::any_raw_internal::<Self>() }\n                    }"
+      },
+      {
+        "def_id": "DefId { id: 12, name: \"kani::any_raw\" }",
+        "file": "kani/library/kani_core/src/lib.rs",
+        "func": "fn any_raw<T: Copy>() -> T {\n            kani_intrinsic()\n        }"
+      },
+      {
+        "def_id": "DefId { id: 13, name: \"kani::kani_intrinsic\" }",
+        "file": "kani/library/kani_core/src/lib.rs",
+        "func": "fn kani_intrinsic<T>() -> T {\n            #[allow(clippy::empty_loop)]\n            loop {}\n        }"
+      },
+      {
+        "def_id": "DefId { id: 6, name: \"kani::assert\" }",
+        "file": "kani/library/kani_core/src/lib.rs",
+        "func": "pub const fn assert(cond: bool, msg: &'static str) {\n            let _ = cond;\n            let _ = msg;\n        }"
+      },
+      {
+        "def_id": "DefId { id: 8, name: \"kani::any\" }",
+        "file": "kani/library/kani_core/src/lib.rs",
+        "func": "pub fn any<T: Arbitrary>() -> T {\n            T::any()\n        }"
+      },
+      {
+        "def_id": "DefId { id: 11, name: \"kani::any_raw_internal\" }",
+        "file": "kani/library/kani_core/src/lib.rs",
+        "func": "unsafe fn any_raw_internal<T: Copy>() -> T {\n            any_raw::<T>()\n        }"
+      }
+    ]
+  }
+]