fix: strip local path of kani in file path

zjp-CN · zjp-CN · commit f98ee314b5bc · 2025-04-14T21:30:48.000+08:00
close #21
diff --git a/src/functions/mod.rs b/src/functions/mod.rs
@@ -75,7 +75,7 @@ impl Function {
         let attrs = KANI_TOOL_ATTRS.iter().flat_map(|v| inst_def.tool_attrs(v)).collect();
 
         let span = inst_def.span();
-        let file = span.get_filename();
+        let file = file_path(&inst);
 
         let fn_def = ty_to_fndef(inst.ty())?;
         let body = fn_def.body()?;
@@ -127,8 +127,8 @@ fn source_code_of_body(inst: &Instance, tcx: TyCtxt, src_map: &SourceMap) -> Opt
 }
 
 fn cmp_callees(a: &Instance, b: &Instance, tcx: TyCtxt, src_map: &SourceMap) -> Ordering {
-    let filename_a = a.def.span().get_filename();
-    let filename_b = b.def.span().get_filename();
+    let filename_a = file_path(a);
+    let filename_b = file_path(b);
     match filename_a.cmp(&filename_b) {
         Ordering::Equal => (),
         ord => return ord,
@@ -138,3 +138,14 @@ fn cmp_callees(a: &Instance, b: &Instance, tcx: TyCtxt, src_map: &SourceMap) ->
     let body_b = source_code_of_body(b, tcx, src_map);
     body_a.cmp(&body_b)
 }
+
+fn file_path(inst: &Instance) -> String {
+    use std::sync::LazyLock;
+    static PWD: LazyLock<String> = LazyLock::new(|| {
+        let mut path = std::env::current_dir().unwrap().into_os_string().into_string().unwrap();
+        path.push('/');
+        path
+    });
+    let file = inst.def.span().get_filename();
+    file.strip_prefix(&*PWD).map(String::from).unwrap_or(file)
+}
diff --git a/src/functions/serialization.rs b/src/functions/serialization.rs
@@ -75,7 +75,7 @@ impl Callee {
     fn new(inst: &Instance, tcx: TyCtxt, src_map: &SourceMap) -> Self {
         let inst_def = &inst.def;
         let def_id = format_def_id(&inst_def.def_id());
-        let file = inst_def.span().get_filename();
+        let file = super::file_path(inst);
         let func = super::source_code_of_body(inst, tcx, src_map).unwrap_or_default();
         Callee { def_id, file, func }
     }
diff --git a/tests/snapshots/contract1.json b/tests/snapshots/contract1.json
@@ -1,6 +1,6 @@
 [
   {
-    "hash": "1333061076946858250810580638840992453503",
+    "hash": "115172008545498701307566340849891514113",
     "def_id": "DefId { id: 13, name: \"verify::f\" }",
     "file": "tests/compare/contract.rs",
     "attrs": [
@@ -1220,7 +1220,7 @@
       },
       {
         "def_id": "DefId { id: 14, name: \"kani::panic\" }",
-        "file": "/home/zjp/rust/distributed-verification/kani/library/kani_core/src/lib.rs",
+        "file": "kani/library/kani_core/src/lib.rs",
         "func": "pub const fn panic(message: &'static str) -> ! {\n            panic!(\"{}\", message)\n        }"
       },
       {
diff --git a/tests/snapshots/contract2.json b/tests/snapshots/contract2.json
@@ -1,6 +1,6 @@
 [
   {
-    "hash": "1333061076946858250810580638840992453503",
+    "hash": "115172008545498701307566340849891514113",
     "def_id": "DefId { id: 13, name: \"verify::f\" }",
     "file": "tests/compare/contract.rs",
     "attrs": [
@@ -1220,7 +1220,7 @@
       },
       {
         "def_id": "DefId { id: 27, name: \"kani::panic\" }",
-        "file": "/home/zjp/rust/distributed-verification/kani/library/kani_core/src/lib.rs",
+        "file": "kani/library/kani_core/src/lib.rs",
         "func": "pub const fn panic(message: &'static str) -> ! {\n            panic!(\"{}\", message)\n        }"
       },
       {
diff --git a/tests/snapshots/proof1.json b/tests/snapshots/proof1.json
@@ -1,6 +1,6 @@
 [
   {
-    "hash": "1080390447388388208111011526646376797302",
+    "hash": "323435775406490987911952280202009855384",
     "def_id": "DefId { id: 0, name: \"verify::f\" }",
     "file": "tests/compare/proof.rs",
     "attrs": [
@@ -10,7 +10,7 @@
     "callees": [
       {
         "def_id": "DefId { id: 1, name: \"kani::assert\" }",
-        "file": "/home/zjp/rust/distributed-verification/kani/library/kani_core/src/lib.rs",
+        "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        }"
       }
     ]
diff --git a/tests/snapshots/proof2.json b/tests/snapshots/proof2.json
@@ -1,6 +1,6 @@
 [
   {
-    "hash": "1080390447388388208111011526646376797302",
+    "hash": "323435775406490987911952280202009855384",
     "def_id": "DefId { id: 0, name: \"verify::f\" }",
     "file": "tests/compare/proof.rs",
     "attrs": [
@@ -10,13 +10,13 @@
     "callees": [
       {
         "def_id": "DefId { id: 2, name: \"kani::assert\" }",
-        "file": "/home/zjp/rust/distributed-verification/kani/library/kani_core/src/lib.rs",
+        "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        }"
       }
     ]
   },
   {
-    "hash": "111100297692849598313316231646472092130",
+    "hash": "93182050081686602881562663240458408606",
     "def_id": "DefId { id: 1, name: \"verify::g\" }",
     "file": "tests/compare/proof.rs",
     "attrs": [
@@ -26,7 +26,7 @@
     "callees": [
       {
         "def_id": "DefId { id: 2, name: \"kani::assert\" }",
-        "file": "/home/zjp/rust/distributed-verification/kani/library/kani_core/src/lib.rs",
+        "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        }"
       }
     ]
diff --git a/tests/snapshots/standard_proofs.json b/tests/snapshots/standard_proofs.json
@@ -10,7 +10,7 @@
     "callees": []
   },
   {
-    "hash": "598200882196848966016444482128164260930",
+    "hash": "1326945528524461068796384134380740941",
     "def_id": "DefId { id: 0, name: \"verify::standard_proof\" }",
     "file": "tests/proofs/standard_proofs.rs",
     "attrs": [
@@ -20,32 +20,32 @@
     "callees": [
       {
         "def_id": "DefId { id: 8, name: \"<u8 as kani::Arbitrary>::any\" }",
-        "file": "/home/zjp/rust/distributed-verification/kani/library/kani_core/src/arbitrary.rs",
+        "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: 10, name: \"kani::any_raw\" }",
-        "file": "/home/zjp/rust/distributed-verification/kani/library/kani_core/src/lib.rs",
+        "file": "kani/library/kani_core/src/lib.rs",
         "func": "fn any_raw<T: Copy>() -> T {\n            kani_intrinsic()\n        }"
       },
       {
         "def_id": "DefId { id: 11, name: \"kani::kani_intrinsic\" }",
-        "file": "/home/zjp/rust/distributed-verification/kani/library/kani_core/src/lib.rs",
+        "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": "/home/zjp/rust/distributed-verification/kani/library/kani_core/src/lib.rs",
+        "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: 5, name: \"kani::any\" }",
-        "file": "/home/zjp/rust/distributed-verification/kani/library/kani_core/src/lib.rs",
+        "file": "kani/library/kani_core/src/lib.rs",
         "func": "pub fn any<T: Arbitrary>() -> T {\n            T::any()\n        }"
       },
       {
         "def_id": "DefId { id: 9, name: \"kani::any_raw_internal\" }",
-        "file": "/home/zjp/rust/distributed-verification/kani/library/kani_core/src/lib.rs",
+        "file": "kani/library/kani_core/src/lib.rs",
         "func": "unsafe fn any_raw_internal<T: Copy>() -> T {\n            any_raw::<T>()\n        }"
       }
     ]
diff --git a/tests/snapshots/standard_proofs_with_contracts.json b/tests/snapshots/standard_proofs_with_contracts.json
@@ -1,6 +1,6 @@
 [
   {
-    "hash": "1025309838735755950413656814657831068918",
+    "hash": "1720175471726112845615145613787907368267",
     "def_id": "DefId { id: 13, name: \"verify::standard_proof_with_contract_requires\" }",
     "file": "tests/proofs/standard_proofs_with_contracts.rs",
     "attrs": [
@@ -1220,7 +1220,7 @@
       },
       {
         "def_id": "DefId { id: 33, name: \"kani::panic\" }",
-        "file": "/home/zjp/rust/distributed-verification/kani/library/kani_core/src/lib.rs",
+        "file": "kani/library/kani_core/src/lib.rs",
         "func": "pub const fn panic(message: &'static str) -> ! {\n            panic!(\"{}\", message)\n        }"
       },
       {
@@ -1256,7 +1256,7 @@
     ]
   },
   {
-    "hash": "1317424779862856706714064197163667502053",
+    "hash": "176046216958037015626605244695592309696",
     "def_id": "DefId { id: 32, name: \"verify::standard_proof_with_contract_ensures\" }",
     "file": "tests/proofs/standard_proofs_with_contracts.rs",
     "attrs": [
@@ -2476,7 +2476,7 @@
       },
       {
         "def_id": "DefId { id: 33, name: \"kani::panic\" }",
-        "file": "/home/zjp/rust/distributed-verification/kani/library/kani_core/src/lib.rs",
+        "file": "kani/library/kani_core/src/lib.rs",
         "func": "pub const fn panic(message: &'static str) -> ! {\n            panic!(\"{}\", message)\n        }"
       },
       {

Original file line number	Diff line number	Diff line change
`@@ -75,7 +75,7 @@ impl Callee {`
`75`	`75`	`fn new(inst: &Instance, tcx: TyCtxt, src_map: &SourceMap) -> Self {`
`76`	`76`	`let inst_def = &inst.def;`
`77`	`77`	`let def_id = format_def_id(&inst_def.def_id());`
`78`		`- let file = inst_def.span().get_filename();`
	`78`	`+ let file = super::file_path(inst);`
`79`	`79`	`let func = super::source_code_of_body(inst, tcx, src_map).unwrap_or_default();`
`80`	`80`	`Callee { def_id, file, func }`
`81`	`81`	`}`
Original file line number	Diff line number	Diff line change
`@@ -1,6 +1,6 @@`
`1`	`1`	`[`
`2`	`2`	`{`
`3`		`- "hash": "1333061076946858250810580638840992453503",`
	`3`	`+ "hash": "115172008545498701307566340849891514113",`
`4`	`4`	`"def_id": "DefId { id: 13, name: \"verify::f\" }",`
`5`	`5`	`"file": "tests/compare/contract.rs",`
`6`	`6`	`"attrs": [`
`@@ -1220,7 +1220,7 @@`
`1220`	`1220`	`},`
`1221`	`1221`	`{`
`1222`	`1222`	`"def_id": "DefId { id: 14, name: \"kani::panic\" }",`
`1223`		`- "file": "/home/zjp/rust/distributed-verification/kani/library/kani_core/src/lib.rs",`
	`1223`	`+ "file": "kani/library/kani_core/src/lib.rs",`
`1224`	`1224`	`"func": "pub const fn panic(message: &'static str) -> ! {\n panic!(\"{}\", message)\n }"`
`1225`	`1225`	`},`
`1226`	`1226`	`{`
Original file line number	Diff line number	Diff line change
`@@ -1,6 +1,6 @@`
`1`	`1`	`[`
`2`	`2`	`{`
`3`		`- "hash": "1080390447388388208111011526646376797302",`
	`3`	`+ "hash": "323435775406490987911952280202009855384",`
`4`	`4`	`"def_id": "DefId { id: 0, name: \"verify::f\" }",`
`5`	`5`	`"file": "tests/compare/proof.rs",`
`6`	`6`	`"attrs": [`
`@@ -10,7 +10,7 @@`
`10`	`10`	`"callees": [`
`11`	`11`	`{`
`12`	`12`	`"def_id": "DefId { id: 1, name: \"kani::assert\" }",`
`13`		`- "file": "/home/zjp/rust/distributed-verification/kani/library/kani_core/src/lib.rs",`
	`13`	`+ "file": "kani/library/kani_core/src/lib.rs",`
`14`	`14`	`"func": "pub const fn assert(cond: bool, msg: &'static str) {\n let _ = cond;\n let _ = msg;\n }"`
`15`	`15`	`}`
`16`	`16`	`]`
Original file line number	Diff line number	Diff line change
`@@ -1,6 +1,6 @@`
`1`	`1`	`[`
`2`	`2`	`{`
`3`		`- "hash": "1025309838735755950413656814657831068918",`
	`3`	`+ "hash": "1720175471726112845615145613787907368267",`
`4`	`4`	`"def_id": "DefId { id: 13, name: \"verify::standard_proof_with_contract_requires\" }",`
`5`	`5`	`"file": "tests/proofs/standard_proofs_with_contracts.rs",`
`6`	`6`	`"attrs": [`
`@@ -1220,7 +1220,7 @@`
`1220`	`1220`	`},`
`1221`	`1221`	`{`
`1222`	`1222`	`"def_id": "DefId { id: 33, name: \"kani::panic\" }",`
`1223`		`- "file": "/home/zjp/rust/distributed-verification/kani/library/kani_core/src/lib.rs",`
	`1223`	`+ "file": "kani/library/kani_core/src/lib.rs",`
`1224`	`1224`	`"func": "pub const fn panic(message: &'static str) -> ! {\n panic!(\"{}\", message)\n }"`
`1225`	`1225`	`},`
`1226`	`1226`	`{`
`@@ -1256,7 +1256,7 @@`
`1256`	`1256`	`]`
`1257`	`1257`	`},`
`1258`	`1258`	`{`
`1259`		`- "hash": "1317424779862856706714064197163667502053",`
	`1259`	`+ "hash": "176046216958037015626605244695592309696",`
`1260`	`1260`	`"def_id": "DefId { id: 32, name: \"verify::standard_proof_with_contract_ensures\" }",`
`1261`	`1261`	`"file": "tests/proofs/standard_proofs_with_contracts.rs",`
`1262`	`1262`	`"attrs": [`
`@@ -2476,7 +2476,7 @@`
`2476`	`2476`	`},`
`2477`	`2477`	`{`
`2478`	`2478`	`"def_id": "DefId { id: 33, name: \"kani::panic\" }",`
`2479`		`- "file": "/home/zjp/rust/distributed-verification/kani/library/kani_core/src/lib.rs",`
	`2479`	`+ "file": "kani/library/kani_core/src/lib.rs",`
`2480`	`2480`	`"func": "pub const fn panic(message: &'static str) -> ! {\n panic!(\"{}\", message)\n }"`
`2481`	`2481`	`},`
`2482`	`2482`	`{`