feat: add callees_len field in SerFunction

zjp-CN · zjp-CN · commit 03c62f899143 · 2025-04-17T14:32:08.000+08:00
diff --git a/src/functions/serialization.rs b/src/functions/serialization.rs
@@ -15,6 +15,8 @@ pub struct SerFunction {
     attrs: Vec<String>,
     /// Raw function string, including name, signature, and body.
     func: SourceCode,
+    /// Count of callees.
+    callees_len: usize,
     /// Recursive function calls inside the proof.
     callees: Vec<Callee>,
 }
@@ -27,17 +29,18 @@ impl SerFunction {
         // Though this is from body span, fn name and signature are included.
         let func = cache::get_source_code(&inst).unwrap_or_default();
         let callees: Vec<_> = fun.callees.iter().map(Callee::new).collect();
+        let callees_len = callees.len();
 
         // Hash
         let mut hasher = StableHasher::<SipHasher128>::new();
         func.with_hasher(&mut hasher);
         hasher.write_length_prefix(attrs.len());
         attrs.iter().for_each(|attr| hasher.write_str(attr));
-        hasher.write_length_prefix(callees.len());
+        hasher.write_length_prefix(callees_len);
         callees.iter().for_each(|callee| callee.func.with_hasher(&mut hasher));
         let Hash128(hash) = hasher.finish();
 
-        SerFunction { hash, def_id, attrs, func, callees }
+        SerFunction { hash, def_id, attrs, func, callees_len, callees }
     }
 
     /// Compare by file and func string.
diff --git a/src/lib.rs b/src/lib.rs
@@ -11,6 +11,8 @@ pub struct SerFunction {
     pub attrs: Vec<String>,
     /// Raw function string, including name, signature, and body.
     pub func: SourceCode,
+    /// Count of callees.
+    pub callees_len: usize,
     /// Recursive function calls inside the body.
     pub callees: Vec<Callee>,
 }
diff --git a/tests/proofs.rs b/tests/proofs.rs
@@ -46,7 +46,7 @@ fn extract_macros_items(json: &[SerFunction]) -> Vec<SerFunction> {
     // filter out kani items).
     json.iter()
         .map(|j| {
-            let callees = j
+            let callees: Vec<_> = j
                 .callees
                 .iter()
                 .filter(|callee| callee.def_id.contains("\"verify::"))
@@ -57,6 +57,7 @@ fn extract_macros_items(json: &[SerFunction]) -> Vec<SerFunction> {
                 def_id: j.def_id.clone(),
                 attrs: j.attrs.clone(),
                 func: j.func.clone(),
+                callees_len: callees.len(),
                 callees,
             }
         })
diff --git a/tests/snapshots/ad_hoc.json b/tests/snapshots/ad_hoc.json
@@ -10,6 +10,7 @@
       "src": "fn callee_defined_in_proof() {\n        fn f() -> u8 {\n            1\n        }\n        assert!(f() == 1);\n    }",
       "before_expansion": null
     },
+    "callees_len": 2,
     "callees": [
       {
         "def_id": "DefId { id: 6, name: \"kani::assert\" }",
@@ -40,6 +41,7 @@
       "src": "fn closure_in_proof() {\n        let f = || 1;\n        assert!(f() == 1);\n    }",
       "before_expansion": null
     },
+    "callees_len": 2,
     "callees": [
       {
         "def_id": "DefId { id: 6, name: \"kani::assert\" }",
@@ -70,6 +72,7 @@
       "src": "fn proof() {\n            assert!(kani::any::<u8>() == 1);\n        }",
       "before_expansion": null
     },
+    "callees_len": 6,
     "callees": [
       {
         "def_id": "DefId { id: 10, name: \"<u8 as kani::Arbitrary>::any\" }",
diff --git a/tests/snapshots/by_macros/gen_contracts_by_macros.json b/tests/snapshots/by_macros/gen_contracts_by_macros.json
@@ -10,6 +10,7 @@
       "src": "fn $proof() {\n            $contract_name(kani::any::<u8>());\n        }",
       "before_expansion": "gen! { proof1: contract1(arg), arg > 0}"
     },
+    "callees_len": 6,
     "callees": [
       {
         "def_id": "DefId { id: 1, name: \"verify::contract1::kani_register_contract\" }",
@@ -72,6 +73,7 @@
       "src": "fn $proof() {\n            $contract_name(kani::any::<u8>());\n        }",
       "before_expansion": "gen! { proof2: contract2(arg), arg != 0}"
     },
+    "callees_len": 6,
     "callees": [
       {
         "def_id": "DefId { id: 15, name: \"verify::contract2::kani_register_contract\" }",
@@ -134,6 +136,7 @@
       "src": "fn $proof() {\n            $contract_name(kani::any::<u8>());\n        }",
       "before_expansion": "gen! { proof3: contract3(arg), arg < 10}"
     },
+    "callees_len": 6,
     "callees": [
       {
         "def_id": "DefId { id: 29, name: \"verify::contract3::kani_register_contract\" }",
diff --git a/tests/snapshots/by_macros/gen_proofs_by_macros.json b/tests/snapshots/by_macros/gen_proofs_by_macros.json
@@ -10,6 +10,7 @@
       "src": "fn $name() $block",
       "before_expansion": "gen! { proof1, { assert_eq!(kani::any::<u8>(), 0) }}"
     },
+    "callees_len": 0,
     "callees": []
   },
   {
@@ -23,6 +24,7 @@
       "src": "fn $name() $block",
       "before_expansion": "gen! { proof2, { assert_eq!(kani::any::<u8>(), 0) }}"
     },
+    "callees_len": 0,
     "callees": []
   },
   {
@@ -36,6 +38,7 @@
       "src": "fn $name() $block",
       "before_expansion": "gen! { proof3, { assert_eq!(kani::any::<u8>(), 1) }}"
     },
+    "callees_len": 0,
     "callees": []
   }
 ]
diff --git a/tests/snapshots/contract1.json b/tests/snapshots/contract1.json
@@ -10,6 +10,7 @@
       "src": "pub fn f() {\n        contract(0);\n    }",
       "before_expansion": null
     },
+    "callees_len": 249,
     "callees": [
       {
         "def_id": "DefId { id: 14, name: \"kani::panic\" }",
diff --git a/tests/snapshots/contract2.json b/tests/snapshots/contract2.json
@@ -10,6 +10,7 @@
       "src": "pub fn f() {\n        contract(0);\n    }",
       "before_expansion": null
     },
+    "callees_len": 249,
     "callees": [
       {
         "def_id": "DefId { id: 27, name: \"kani::panic\" }",
diff --git a/tests/snapshots/gen_contracts_by_macros.json b/tests/snapshots/gen_contracts_by_macros.json
@@ -10,6 +10,7 @@
       "src": "fn $proof() {\n            $contract_name(kani::any::<u8>());\n        }",
       "before_expansion": "gen! { proof1: contract1(arg), arg > 0}"
     },
+    "callees_len": 255,
     "callees": [
       {
         "def_id": "DefId { id: 263, name: \"<u8 as kani::Arbitrary>::any\" }",
@@ -2064,6 +2065,7 @@
       "src": "fn $proof() {\n            $contract_name(kani::any::<u8>());\n        }",
       "before_expansion": "gen! { proof2: contract2(arg), arg != 0}"
     },
+    "callees_len": 255,
     "callees": [
       {
         "def_id": "DefId { id: 263, name: \"<u8 as kani::Arbitrary>::any\" }",
@@ -4118,6 +4120,7 @@
       "src": "fn $proof() {\n            $contract_name(kani::any::<u8>());\n        }",
       "before_expansion": "gen! { proof3: contract3(arg), arg < 10}"
     },
+    "callees_len": 255,
     "callees": [
       {
         "def_id": "DefId { id: 263, name: \"<u8 as kani::Arbitrary>::any\" }",
diff --git a/tests/snapshots/gen_proofs_by_macros.json b/tests/snapshots/gen_proofs_by_macros.json
@@ -10,6 +10,7 @@
       "src": "fn $name() $block",
       "before_expansion": "gen! { proof1, { assert_eq!(kani::any::<u8>(), 0) }}"
     },
+    "callees_len": 6,
     "callees": [
       {
         "def_id": "DefId { id: 6, name: \"<u8 as kani::Arbitrary>::any\" }",
@@ -72,6 +73,7 @@
       "src": "fn $name() $block",
       "before_expansion": "gen! { proof2, { assert_eq!(kani::any::<u8>(), 0) }}"
     },
+    "callees_len": 6,
     "callees": [
       {
         "def_id": "DefId { id: 6, name: \"<u8 as kani::Arbitrary>::any\" }",
@@ -134,6 +136,7 @@
       "src": "fn $name() $block",
       "before_expansion": "gen! { proof3, { assert_eq!(kani::any::<u8>(), 1) }}"
     },
+    "callees_len": 6,
     "callees": [
       {
         "def_id": "DefId { id: 6, name: \"<u8 as kani::Arbitrary>::any\" }",
diff --git a/tests/snapshots/proof1.json b/tests/snapshots/proof1.json
@@ -10,6 +10,7 @@
       "src": "pub fn f() {\n        let a = 1;\n        assert_eq!(a + 1, 2);\n    }",
       "before_expansion": null
     },
+    "callees_len": 1,
     "callees": [
       {
         "def_id": "DefId { id: 1, name: \"kani::assert\" }",
diff --git a/tests/snapshots/proof2.json b/tests/snapshots/proof2.json
@@ -10,6 +10,7 @@
       "src": "pub fn f() {\n        let a = 1;\n        assert_eq!(a + 1, 2);\n    }",
       "before_expansion": null
     },
+    "callees_len": 1,
     "callees": [
       {
         "def_id": "DefId { id: 2, name: \"kani::assert\" }",
@@ -32,6 +33,7 @@
       "src": "pub fn g() {\n        let a = 1;\n        assert_eq!(a + 1, 2);\n    }",
       "before_expansion": null
     },
+    "callees_len": 1,
     "callees": [
       {
         "def_id": "DefId { id: 2, name: \"kani::assert\" }",
diff --git a/tests/snapshots/proofs_for_contract.json b/tests/snapshots/proofs_for_contract.json
@@ -10,6 +10,7 @@
       "src": "fn single_contract() {\n        let val = contract(1);\n        assert!(val > 0);\n    }",
       "before_expansion": null
     },
+    "callees_len": 251,
     "callees": [
       {
         "def_id": "DefId { id: 272, name: \"kani::assert\" }",
@@ -2032,6 +2033,7 @@
       "src": "fn single_contract_requires() {\n        contract_requires(0);\n    }",
       "before_expansion": null
     },
+    "callees_len": 250,
     "callees": [
       {
         "def_id": "DefId { id: 53, name: \"kani::panic\" }",
@@ -4046,6 +4048,7 @@
       "src": "fn single_with_contract_ensures() {\n        contract_ensures(0);\n    }",
       "before_expansion": null
     },
+    "callees_len": 250,
     "callees": [
       {
         "def_id": "DefId { id: 53, name: \"kani::panic\" }",
@@ -6060,6 +6063,7 @@
       "src": "fn two_contracts_requires_and_ensures() {\n        let val = contract_ensures(0);\n        contract_requires(val);\n    }",
       "before_expansion": null
     },
+    "callees_len": 260,
     "callees": [
       {
         "def_id": "DefId { id: 53, name: \"kani::panic\" }",
diff --git a/tests/snapshots/standard_proofs.json b/tests/snapshots/standard_proofs.json
@@ -10,6 +10,7 @@
       "src": "fn recursive_callees() {\n        crate::top_level();\n    }",
       "before_expansion": null
     },
+    "callees_len": 109,
     "callees": [
       {
         "def_id": "DefId { id: 75, name: \"std::char::convert::char_try_from_u32\" }",
@@ -896,6 +897,7 @@
       "src": "fn standard_proof() {\n        let val: u8 = kani::any();\n        assert_eq!(val, 1, \"Not eq to 1.\");\n    }",
       "before_expansion": null
     },
+    "callees_len": 6,
     "callees": [
       {
         "def_id": "DefId { id: 8, name: \"<u8 as kani::Arbitrary>::any\" }",
@@ -958,6 +960,7 @@
       "src": "fn standard_proof_empty() {}",
       "before_expansion": null
     },
+    "callees_len": 0,
     "callees": []
   }
 ]
diff --git a/tests/snapshots/standard_proofs_with_contracts.json b/tests/snapshots/standard_proofs_with_contracts.json
@@ -10,6 +10,7 @@
       "src": "fn single_contract() {\n        let val = contract(1);\n        assert!(val > 0);\n    }",
       "before_expansion": null
     },
+    "callees_len": 250,
     "callees": [
       {
         "def_id": "DefId { id: 271, name: \"kani::assert\" }",
@@ -2024,6 +2025,7 @@
       "src": "fn single_contract_requires() {\n        contract_requires(0);\n    }",
       "before_expansion": null
     },
+    "callees_len": 249,
     "callees": [
       {
         "def_id": "DefId { id: 53, name: \"kani::panic\" }",
@@ -4030,6 +4032,7 @@
       "src": "fn single_with_contract_ensures() {\n        contract_ensures(0);\n    }",
       "before_expansion": null
     },
+    "callees_len": 249,
     "callees": [
       {
         "def_id": "DefId { id: 53, name: \"kani::panic\" }",
@@ -6036,6 +6039,7 @@
       "src": "fn two_contracts_requires_and_ensures() {\n        let val = contract_ensures(0);\n        contract_requires(val);\n    }",
       "before_expansion": null
     },
+    "callees_len": 259,
     "callees": [
       {
         "def_id": "DefId { id: 53, name: \"kani::panic\" }",
diff --git a/tests/standard_proof_simple.rs b/tests/standard_proof_simple.rs
@@ -1,18 +1,10 @@
 #[cfg(kani)]
 mod verify {
+    #[kani::requires(a>0)]
+    fn f(a: u8) {}
 
     #[kani::proof]
     fn recursive_callees() {
-        crate::top_level();
-    }
-}
-
-pub fn top_level() {
-    m::func1();
-}
-
-mod m {
-    pub fn func1() {
-        let _a = "".trim();
+        f(0);
     }
 }

Original file line number	Diff line number	Diff line change
`@@ -11,6 +11,8 @@ pub struct SerFunction {`
`11`	`11`	`pub attrs: Vec<String>,`
`12`	`12`	`/// Raw function string, including name, signature, and body.`
`13`	`13`	`pub func: SourceCode,`
	`14`	`+ /// Count of callees.`
	`15`	`+ pub callees_len: usize,`
`14`	`16`	`/// Recursive function calls inside the body.`
`15`	`17`	`pub callees: Vec<Callee>,`
`16`	`18`	`}`
Original file line number	Diff line number	Diff line change
`@@ -10,6 +10,7 @@`
`10`	`10`	`"src": "fn $name() $block",`
`11`	`11`	`"before_expansion": "gen! { proof1, { assert_eq!(kani::any::<u8>(), 0) }}"`
`12`	`12`	`},`
	`13`	`+ "callees_len": 0,`
`13`	`14`	`"callees": []`
`14`	`15`	`},`
`15`	`16`	`{`
`@@ -23,6 +24,7 @@`
`23`	`24`	`"src": "fn $name() $block",`
`24`	`25`	`"before_expansion": "gen! { proof2, { assert_eq!(kani::any::<u8>(), 0) }}"`
`25`	`26`	`},`
	`27`	`+ "callees_len": 0,`
`26`	`28`	`"callees": []`
`27`	`29`	`},`
`28`	`30`	`{`
`@@ -36,6 +38,7 @@`
`36`	`38`	`"src": "fn $name() $block",`
`37`	`39`	`"before_expansion": "gen! { proof3, { assert_eq!(kani::any::<u8>(), 1) }}"`
`38`	`40`	`},`
	`41`	`+ "callees_len": 0,`
`39`	`42`	`"callees": []`
`40`	`43`	`}`
`41`	`44`	`]`