Skip to content

Commit 28fdbc2

Browse files
committed
feat: add item name and kind fields in SourceCode
But compares test fails: thread 'test_compare' panicked at tests/compare.rs:33:13: assertion failed: `(left == right)`: Hash values of "pub fn f()" are not equal: contract1 ≠ contract2 Diff < left / right > : <151423480243889445466514579282516350541 >117543856677718202152688069605492406669
1 parent 03c62f8 commit 28fdbc2

File tree

9 files changed

+2595
-1561
lines changed

9 files changed

+2595
-1561
lines changed

src/functions/cache.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -75,7 +75,7 @@ impl Cache {
7575
let body = inst.body()?;
7676
let rustc = self.rustc.as_ref()?;
7777
let prefix = self.path_prefixes.prefixes();
78-
let src = source_code_with(body.span, rustc.tcx, &rustc.src_map, prefix);
78+
let src = source_code_with(inst, body.span, rustc.tcx, &rustc.src_map, prefix);
7979
Some(CacheFunction { body, src })
8080
})
8181
.as_ref()

src/functions/utils.rs

Lines changed: 15 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,13 +3,22 @@ use rustc_smir::rustc_internal::internal;
33
use rustc_span::{Span, source_map::SourceMap};
44
use rustc_stable_hash::{StableHasher, hashers::SipHasher128};
55
use serde::Serialize;
6+
use stable_mir::mir::mono::Instance;
67
use std::hash::Hasher;
78

89
/// Source code and potential source code before expansion.
910
///
1011
/// The field order matters, since this struct implements Ord.
1112
#[derive(Clone, Debug, Serialize, PartialEq, Eq, PartialOrd, Ord, Default)]
1213
pub struct SourceCode {
14+
/// Function name.
15+
pub name: String,
16+
17+
/// String of [`InstanceKind`].
18+
///
19+
/// [`InstanceKind`]: https://doc.rust-lang.org/nightly/nightly-rustc/stable_mir/mir/mono/enum.InstanceKind.html
20+
pub kind: String,
21+
1322
// A file path where src lies.
1423
// The path is stripped with pwd or sysroot prefix.
1524
pub file: String,
@@ -31,6 +40,8 @@ pub struct SourceCode {
3140

3241
impl SourceCode {
3342
pub fn with_hasher(&self, hasher: &mut StableHasher<SipHasher128>) {
43+
hasher.write_str(&self.name);
44+
hasher.write_str(&self.kind);
3445
hasher.write_str(&self.file);
3546
hasher.write_str(&self.src);
3647
match &self.before_expansion {
@@ -55,6 +66,7 @@ fn span_to_source(span: Span, src_map: &SourceMap) -> String {
5566

5667
/// Source code for a stable_mir span.
5768
pub fn source_code_with(
69+
inst: &Instance,
5870
stable_mir_span: stable_mir::ty::Span,
5971
tcx: TyCtxt,
6072
src_map: &SourceMap,
@@ -75,5 +87,7 @@ pub fn source_code_with(
7587
}
7688
}
7789

78-
SourceCode { file, src, before_expansion }
90+
let name = inst.name();
91+
let kind = format!("{:?}", inst.kind);
92+
SourceCode { name, kind, file, src, before_expansion }
7993
}

src/lib.rs

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -25,6 +25,14 @@ pub struct Callee {
2525

2626
#[derive(Debug, Serialize, Deserialize, Clone)]
2727
pub struct SourceCode {
28+
/// Function name.
29+
pub name: String,
30+
31+
/// String of [`InstanceKind`].
32+
///
33+
/// [`InstanceKind`]: https://doc.rust-lang.org/nightly/nightly-rustc/stable_mir/mir/mono/enum.InstanceKind.html
34+
pub kind: String,
35+
2836
// A file path where src lies.
2937
// The path is stripped with pwd or sysroot prefix.
3038
file: String,

tests/compare.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -32,7 +32,7 @@ fn compare(tmp: &str, v_file: &[&str], f: &str) {
3232
for j in 1..len {
3333
assert_eq!(
3434
v_func[i].hash, v_func[j].hash,
35-
"Hash values are not equal: {} ≠ {}",
35+
"Hash values of {f:?} are not equal: {} ≠ {}",
3636
v_file[i], v_file[j]
3737
);
3838
}

tests/snapshots/contract1.json

Lines changed: 1277 additions & 777 deletions
Large diffs are not rendered by default.

tests/snapshots/contract2.json

Lines changed: 1277 additions & 777 deletions
Large diffs are not rendered by default.

tests/snapshots/proof1.json

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,13 @@
11
[
22
{
3-
"hash": "876433099390387370318218200145590989814",
3+
"hash": "177631543608855386312483865423304532457",
44
"def_id": "DefId { id: 0, name: \"verify::f\" }",
55
"attrs": [
66
"#[kanitool::proof]"
77
],
88
"func": {
9+
"name": "verify::f",
10+
"kind": "Item",
911
"file": "tests/compare/proof.rs",
1012
"src": "pub fn f() {\n let a = 1;\n assert_eq!(a + 1, 2);\n }",
1113
"before_expansion": null
@@ -15,6 +17,8 @@
1517
{
1618
"def_id": "DefId { id: 1, name: \"kani::assert\" }",
1719
"func": {
20+
"name": "kani::assert",
21+
"kind": "Item",
1822
"file": "kani/library/kani_core/src/lib.rs",
1923
"src": "pub const fn assert(cond: bool, msg: &'static str) {\n let _ = cond;\n let _ = msg;\n }",
2024
"before_expansion": "kani_core::kani_intrinsics!(std)"

tests/snapshots/proof2.json

Lines changed: 10 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,13 @@
11
[
22
{
3-
"hash": "876433099390387370318218200145590989814",
3+
"hash": "177631543608855386312483865423304532457",
44
"def_id": "DefId { id: 0, name: \"verify::f\" }",
55
"attrs": [
66
"#[kanitool::proof]"
77
],
88
"func": {
9+
"name": "verify::f",
10+
"kind": "Item",
911
"file": "tests/compare/proof.rs",
1012
"src": "pub fn f() {\n let a = 1;\n assert_eq!(a + 1, 2);\n }",
1113
"before_expansion": null
@@ -15,6 +17,8 @@
1517
{
1618
"def_id": "DefId { id: 2, name: \"kani::assert\" }",
1719
"func": {
20+
"name": "kani::assert",
21+
"kind": "Item",
1822
"file": "kani/library/kani_core/src/lib.rs",
1923
"src": "pub const fn assert(cond: bool, msg: &'static str) {\n let _ = cond;\n let _ = msg;\n }",
2024
"before_expansion": "kani_core::kani_intrinsics!(std)"
@@ -23,12 +27,14 @@
2327
]
2428
},
2529
{
26-
"hash": "47211252920145052832965334366253119118",
30+
"hash": "14466344698218474136540205228183942188",
2731
"def_id": "DefId { id: 1, name: \"verify::g\" }",
2832
"attrs": [
2933
"#[kanitool::proof]"
3034
],
3135
"func": {
36+
"name": "verify::g",
37+
"kind": "Item",
3238
"file": "tests/compare/proof.rs",
3339
"src": "pub fn g() {\n let a = 1;\n assert_eq!(a + 1, 2);\n }",
3440
"before_expansion": null
@@ -38,6 +44,8 @@
3844
{
3945
"def_id": "DefId { id: 2, name: \"kani::assert\" }",
4046
"func": {
47+
"name": "kani::assert",
48+
"kind": "Item",
4149
"file": "kani/library/kani_core/src/lib.rs",
4250
"src": "pub const fn assert(cond: bool, msg: &'static str) {\n let _ = cond;\n let _ = msg;\n }",
4351
"before_expansion": "kani_core::kani_intrinsics!(std)"

tests/standard_proof_simple.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ mod verify {
44
fn f(a: u8) {}
55

66
#[kani::proof]
7-
fn recursive_callees() {
7+
fn proof() {
88
f(0);
99
}
1010
}

0 commit comments

Comments
 (0)