test: compare gen_proofs_by_nested_macros that they should have distinct hash

NOTE: the assert_ne! assertion fails

thread 'test_compare' panicked at tests/compare.rs:53:9:
assertion `left != right` failed: Hash values of "fn" should not equal: SerFunction {
    hash: "1628665993055122224710783236985879540321",
    def_id: "DefId { id: 0, name: \"verify::proof1\" }",
    attrs: [
        "#[kanitool::proof]",
    ],
    func: SourceCode {
        name: "verify::proof1",
        mangled_name: "_ZN27gen_proofs_by_nested_macros6verify6proof117h4d153120b87a21d4E",
        kind: "Item",
        file: "tests/compare/gen_proofs_by_nested_macros.rs",
        src: "fn",
        before_expansion: Some(
            "inner!($name, $block)",
        ),
    },
    callees_len: 6,
    callees: [],
} vs SerFunction {
    hash: "1628665993055122224710783236985879540321",
    def_id: "DefId { id: 0, name: \"verify::proof1\" }",
    attrs: [
        "#[kanitool::proof]",
    ],
    func: SourceCode {
        name: "verify::proof1",
        mangled_name: "_ZN27gen_proofs_by_nested_macros6verify6proof117h4d153120b87a21d4E",
        kind: "Item",
        file: "tests/compare/gen_proofs_by_nested_macros.rs",
        src: "fn",
        before_expansion: Some(
            "inner!($name, $block)",
        ),
    },
    callees_len: 6,
    callees: [],
}
  left: "1628665993055122224710783236985879540321"
 right: "1628665993055122224710783236985879540321"

Author: zjp-CN

tests/compare.rs

@@ -11,7 +11,7 @@ fn get(text: &str, start: &str) -> SerFunction {
 
 const COMPARE: &str = "tests/compare";
 
-fn compare(tmp: &str, v_file: &[&str], f: &str) {
+fn compare(tmp: &str, v_file: &[&str], f: &str, assert: impl Fn(&SerFunction, &SerFunction, &str)) {
     let len = v_file.len();
     assert!(len > 1);
     let tmp = format!("{COMPARE}/{tmp}.rs");
@@ -30,20 +30,49 @@ fn compare(tmp: &str, v_file: &[&str], f: &str) {
     // the hash value must be the same.
     for i in 0..len - 1 {
         for j in 1..len {
-            assert_eq!(
-                v_func[i].hash, v_func[j].hash,
-                "Hash values of {f:?} are not equal: {} ≠ {}",
-                v_file[i], v_file[j]
-            );
-            // if v_func[i].hash == v_func[j].hash {
-            //     println!("Hash values of {f:?} are not equal: {} ≠ {}", v_file[i], v_file[j]);
-            // }
+            assert(&v_func[i], &v_func[j], f);
         }
     }
 }
 
 #[test]
 fn test_compare() {
-    compare("proof", &["proof1", "proof2"], "pub fn f()");
-    compare("contract", &["contract1", "contract2"], "pub fn f()");
+    fn eq(fn1: &SerFunction, fn2: &SerFunction, f: &str) {
+        assert_eq!(
+            fn1.hash,
+            fn2.hash,
+            "Hash values of {f:?} are not equal: {f1:#?} ≠ {f2:#?}",
+            f1 = simplify_ser_function(fn1),
+            f2 = simplify_ser_function(fn2),
+        );
+    }
+    compare("proof", &["proof1", "proof2"], "pub fn f()", eq);
+    compare("contract", &["contract1", "contract2"], "pub fn f()", eq);
+
+    fn not_eq(fn1: &SerFunction, fn2: &SerFunction, f: &str) {
+        assert_ne!(
+            fn1.hash,
+            fn2.hash,
+            "Hash values of {f:?} should not equal: {f1:#?} vs {f2:#?}",
+            f1 = simplify_ser_function(fn1),
+            f2 = simplify_ser_function(fn2),
+        );
+    }
+    compare(
+        "gen_proofs_by_nested_macros",
+        &["gen_proofs_by_nested_macros1", "gen_proofs_by_nested_macros2"],
+        "fn",
+        not_eq,
+    );
+}
+
+fn simplify_ser_function(fn1: &SerFunction) -> SerFunction {
+    SerFunction {
+        hash: fn1.hash.clone(),
+        def_id: fn1.def_id.clone(),
+        attrs: fn1.attrs.clone(),
+        func: fn1.func.clone(),
+        callees_len: fn1.callees_len,
+        ..Default::default()
+    }
 }

tests/compare/gen_proofs_by_nested_macros1.rs

@@ -0,0 +1,17 @@
+macro_rules! outer {
+    ($name:ident, $block:block) => {
+        inner!($name, $block);
+    };
+}
+
+macro_rules! inner {
+    ($name:ident, $block:block) => {
+        #[kani::proof]
+        fn $name() $block
+    }
+}
+
+#[cfg(kani)]
+mod verify {
+    outer! { proof1, { assert_eq!(kani::any::<u8>(), 0) }}
+}

tests/compare/gen_proofs_by_nested_macros2.rs

@@ -0,0 +1,17 @@
+macro_rules! outer {
+    ($name:ident, $block:block) => {
+        inner!($name, $block);
+    };
+}
+
+macro_rules! inner {
+    ($name:ident, $block:block) => {
+        #[kani::proof]
+        fn $name() $block
+    }
+}
+
+#[cfg(kani)]
+mod verify {
+    outer! { proof1, { assert_eq!(kani::any::<u8>(), 1) }}
+}

tests/snapshots/gen_proofs_by_nested_macros1.json

@@ -0,0 +1,86 @@
+[
+  {
+    "hash": "1628665993055122224710783236985879540321",
+    "def_id": "DefId { id: 0, name: \"verify::proof1\" }",
+    "attrs": [
+      "#[kanitool::proof]"
+    ],
+    "func": {
+      "name": "verify::proof1",
+      "mangled_name": "_ZN27gen_proofs_by_nested_macros6verify6proof117h4d153120b87a21d4E",
+      "kind": "Item",
+      "file": "tests/compare/gen_proofs_by_nested_macros.rs",
+      "src": "fn",
+      "before_expansion": "inner!($name, $block)"
+    },
+    "callees_len": 6,
+    "callees": [
+      {
+        "def_id": "DefId { id: 4, name: \"<u8 as kani::Arbitrary>::any\" }",
+        "func": {
+          "name": "<u8 as kani::Arbitrary>::any",
+          "mangled_name": "_ZN38_$LT$u8$u20$as$u20$kani..Arbitrary$GT$3any17hfd29445e7b2cdd95E",
+          "kind": "Item",
+          "file": "kani/library/kani_core/src/arbitrary.rs",
+          "src": "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                    }",
+          "before_expansion": "trivial_arbitrary!(u8)"
+        }
+      },
+      {
+        "def_id": "DefId { id: 1, name: \"kani::any\" }",
+        "func": {
+          "name": "kani::any::<u8>",
+          "mangled_name": "_ZN4kani3any17h800d752a2e66bb13E",
+          "kind": "Item",
+          "file": "kani/library/kani_core/src/lib.rs",
+          "src": "pub fn any<T: Arbitrary>() -> T {\n            T::any()\n        }",
+          "before_expansion": "kani_core::kani_intrinsics!(std)"
+        }
+      },
+      {
+        "def_id": "DefId { id: 6, name: \"kani::any_raw\" }",
+        "func": {
+          "name": "kani::any_raw::<u8>",
+          "mangled_name": "_ZN4kani7any_raw17hef764f0401a0f588E",
+          "kind": "Item",
+          "file": "kani/library/kani_core/src/lib.rs",
+          "src": "fn any_raw<T: Copy>() -> T {\n            kani_intrinsic()\n        }",
+          "before_expansion": "kani_core::kani_intrinsics!(std)"
+        }
+      },
+      {
+        "def_id": "DefId { id: 5, name: \"kani::any_raw_internal\" }",
+        "func": {
+          "name": "kani::any_raw_internal::<u8>",
+          "mangled_name": "_ZN4kani16any_raw_internal17h86fbfff4755b5586E",
+          "kind": "Item",
+          "file": "kani/library/kani_core/src/lib.rs",
+          "src": "unsafe fn any_raw_internal<T: Copy>() -> T {\n            any_raw::<T>()\n        }",
+          "before_expansion": "kani_core::kani_intrinsics!(std)"
+        }
+      },
+      {
+        "def_id": "DefId { id: 2, name: \"kani::assert\" }",
+        "func": {
+          "name": "kani::assert",
+          "mangled_name": "_ZN4kani6assert17hcc89e8c2e0f13823E",
+          "kind": "Item",
+          "file": "kani/library/kani_core/src/lib.rs",
+          "src": "pub const fn assert(cond: bool, msg: &'static str) {\n            let _ = cond;\n            let _ = msg;\n        }",
+          "before_expansion": "kani_core::kani_intrinsics!(std)"
+        }
+      },
+      {
+        "def_id": "DefId { id: 7, name: \"kani::kani_intrinsic\" }",
+        "func": {
+          "name": "kani::kani_intrinsic::<u8>",
+          "mangled_name": "_ZN4kani14kani_intrinsic17h4c94b2d1e6f52b91E",
+          "kind": "Item",
+          "file": "kani/library/kani_core/src/lib.rs",
+          "src": "fn kani_intrinsic<T>() -> T {\n            #[allow(clippy::empty_loop)]\n            loop {}\n        }",
+          "before_expansion": "kani_core::kani_intrinsics!(std)"
+        }
+      }
+    ]
+  }
+]

tests/snapshots/gen_proofs_by_nested_macros2.json

@@ -0,0 +1,86 @@
+[
+  {
+    "hash": "1628665993055122224710783236985879540321",
+    "def_id": "DefId { id: 0, name: \"verify::proof1\" }",
+    "attrs": [
+      "#[kanitool::proof]"
+    ],
+    "func": {
+      "name": "verify::proof1",
+      "mangled_name": "_ZN27gen_proofs_by_nested_macros6verify6proof117h4d153120b87a21d4E",
+      "kind": "Item",
+      "file": "tests/compare/gen_proofs_by_nested_macros.rs",
+      "src": "fn",
+      "before_expansion": "inner!($name, $block)"
+    },
+    "callees_len": 6,
+    "callees": [
+      {
+        "def_id": "DefId { id: 4, name: \"<u8 as kani::Arbitrary>::any\" }",
+        "func": {
+          "name": "<u8 as kani::Arbitrary>::any",
+          "mangled_name": "_ZN38_$LT$u8$u20$as$u20$kani..Arbitrary$GT$3any17hfd29445e7b2cdd95E",
+          "kind": "Item",
+          "file": "kani/library/kani_core/src/arbitrary.rs",
+          "src": "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                    }",
+          "before_expansion": "trivial_arbitrary!(u8)"
+        }
+      },
+      {
+        "def_id": "DefId { id: 1, name: \"kani::any\" }",
+        "func": {
+          "name": "kani::any::<u8>",
+          "mangled_name": "_ZN4kani3any17h800d752a2e66bb13E",
+          "kind": "Item",
+          "file": "kani/library/kani_core/src/lib.rs",
+          "src": "pub fn any<T: Arbitrary>() -> T {\n            T::any()\n        }",
+          "before_expansion": "kani_core::kani_intrinsics!(std)"
+        }
+      },
+      {
+        "def_id": "DefId { id: 6, name: \"kani::any_raw\" }",
+        "func": {
+          "name": "kani::any_raw::<u8>",
+          "mangled_name": "_ZN4kani7any_raw17hef764f0401a0f588E",
+          "kind": "Item",
+          "file": "kani/library/kani_core/src/lib.rs",
+          "src": "fn any_raw<T: Copy>() -> T {\n            kani_intrinsic()\n        }",
+          "before_expansion": "kani_core::kani_intrinsics!(std)"
+        }
+      },
+      {
+        "def_id": "DefId { id: 5, name: \"kani::any_raw_internal\" }",
+        "func": {
+          "name": "kani::any_raw_internal::<u8>",
+          "mangled_name": "_ZN4kani16any_raw_internal17h86fbfff4755b5586E",
+          "kind": "Item",
+          "file": "kani/library/kani_core/src/lib.rs",
+          "src": "unsafe fn any_raw_internal<T: Copy>() -> T {\n            any_raw::<T>()\n        }",
+          "before_expansion": "kani_core::kani_intrinsics!(std)"
+        }
+      },
+      {
+        "def_id": "DefId { id: 2, name: \"kani::assert\" }",
+        "func": {
+          "name": "kani::assert",
+          "mangled_name": "_ZN4kani6assert17hcc89e8c2e0f13823E",
+          "kind": "Item",
+          "file": "kani/library/kani_core/src/lib.rs",
+          "src": "pub const fn assert(cond: bool, msg: &'static str) {\n            let _ = cond;\n            let _ = msg;\n        }",
+          "before_expansion": "kani_core::kani_intrinsics!(std)"
+        }
+      },
+      {
+        "def_id": "DefId { id: 7, name: \"kani::kani_intrinsic\" }",
+        "func": {
+          "name": "kani::kani_intrinsic::<u8>",
+          "mangled_name": "_ZN4kani14kani_intrinsic17h4c94b2d1e6f52b91E",
+          "kind": "Item",
+          "file": "kani/library/kani_core/src/lib.rs",
+          "src": "fn kani_intrinsic<T>() -> T {\n            #[allow(clippy::empty_loop)]\n            loop {}\n        }",
+          "before_expansion": "kani_core::kani_intrinsics!(std)"
+        }
+      }
+    ]
+  }
+]