Skip to content

Commit cfe98b5

Browse files
zjp-CNzjp-CN
authored
Merge pull request #44 from os-checker/fix-compare
Fix: have Instance as Cache set key
2 parents df0c91c + d0a8e7f commit cfe98b5

File tree

10 files changed

+16858
-6824
lines changed

10 files changed

+16858
-6824
lines changed

‎src/functions/cache.rs‎

Lines changed: 7 additions & 29 deletions
Original file line numberDiff line numberDiff line change
@@ -6,10 +6,7 @@ use super::utils::{SourceCode, source_code_with};
66
use rustc_data_structures::fx::FxHashMap;
77
use rustc_middle::ty::TyCtxt;
88
use rustc_span::source_map::{SourceMap, get_source_map};
9-
use stable_mir::{
10-
CrateDef, DefId,
11-
mir::{Body, mono::Instance},
12-
};
9+
use stable_mir::mir::{Body, mono::Instance};
1310
use std::{cell::RefCell, cmp::Ordering, sync::Arc};
1411

1512
thread_local! {
@@ -45,39 +42,20 @@ pub fn get_source_code(inst: &Instance) -> Option<SourceCode> {
4542
get_cache_func(inst, |cf| cf.src.clone())
4643
}
4744

48-
/// NOTE: this function doesn't auto insert SourceCode if Instance isn't handled.
49-
pub fn share_same_source_code(a: &Instance, b: &Instance) -> bool {
50-
get_cache(|cache| {
51-
let defid_a = a.def.def_id();
52-
let defid_b = b.def.def_id();
53-
let src_a = cache.set.get(&defid_a);
54-
let src_b = cache.set.get(&defid_b);
55-
match (src_a, src_b) {
56-
(Some(cache_a), Some(cache_b)) => match (cache_a, cache_b) {
57-
(Some(func_a), Some(func_b)) => func_a.src == func_b.src,
58-
(None, None) => defid_a == defid_b,
59-
(None, Some(_)) => false,
60-
(Some(_), None) => false,
61-
},
62-
(None, None) => defid_a == defid_b,
63-
(None, Some(_)) => false,
64-
(Some(_), None) => false,
65-
}
66-
})
67-
}
68-
6945
pub fn cmp_callees(a: &Instance, b: &Instance) -> Ordering {
7046
get_cache(|cache| {
7147
cache.get_or_insert(a);
7248
cache.get_or_insert(b);
73-
let func_a = cache.set.get(&a.def.def_id()).unwrap().as_ref().map(|f| &f.src);
74-
let func_b = cache.set.get(&b.def.def_id()).unwrap().as_ref().map(|f| &f.src);
49+
let func_a = cache.set.get(a).unwrap().as_ref().map(|f| &f.src);
50+
let func_b = cache.set.get(b).unwrap().as_ref().map(|f| &f.src);
7551
func_a.cmp(&func_b)
7652
})
7753
}
7854

7955
struct Cache {
80-
set: FxHashMap<DefId, Option<CacheFunction>>,
56+
/// The reason to have Instance as the key is
57+
/// https://github.com/os-checker/distributed-verification/issues/42
58+
set: FxHashMap<Instance, Option<CacheFunction>>,
8159
rustc: Option<RustcCxt>,
8260
path_prefixes: PathPrefixes,
8361
}
@@ -91,7 +69,7 @@ impl Cache {
9169

9270
fn get_or_insert(&mut self, inst: &Instance) -> Option<&CacheFunction> {
9371
self.set
94-
.entry(inst.def.def_id())
72+
.entry(*inst)
9573
.or_insert_with(|| {
9674
let body = inst.body()?;
9775
let rustc = self.rustc.as_ref()?;

‎src/functions/mod.rs‎

Lines changed: 1 addition & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -53,7 +53,7 @@ pub struct Function {
5353

5454
/// Recursive fnction calls inside the body.
5555
/// The elements are sorted by file path and fn source code to keep hash value stable.
56-
callees: Vec<Instance>,
56+
callees: IndexSet<Instance>,
5757
}
5858

5959
impl Function {
@@ -75,11 +75,7 @@ impl Function {
7575

7676
let mut callees = IndexSet::new();
7777
callgraph.recursive_callees(item, &mut callees);
78-
79-
// Multiple instances may share the same defid (or rather SourceCode), so deduplicate them.
80-
let mut callees: Vec<_> = callees.into_iter().collect();
8178
callees.sort_by(cache::cmp_callees);
82-
callees.dedup_by(|a, b| cache::share_same_source_code(a, b));
8379

8480
let this = Function { instance, attrs, callees };
8581
filter(&this).then_some(this)

‎tests/compare.rs‎

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
use std::fs::{copy, remove_file};
22

33
mod utils;
4-
use utils::*;
4+
use utils::{assert_eq, *};
55

66
fn get(text: &str, start: &str) -> SerFunction {
77
let json = &text[text.find("[\n").unwrap()..];
@@ -30,14 +30,14 @@ fn compare(tmp: &str, v_file: &[&str], f: &str) {
3030
// the hash value must be the same.
3131
for i in 0..len - 1 {
3232
for j in 1..len {
33-
// assert_eq!(
34-
// v_func[i].hash, v_func[j].hash,
35-
// "Hash values of {f:?} are not equal: {} ≠ {}",
36-
// v_file[i], v_file[j]
37-
// );
38-
if v_func[i].hash == v_func[j].hash {
39-
println!("Hash values of {f:?} are not equal: {} ≠ {}", v_file[i], v_file[j]);
40-
}
33+
assert_eq!(
34+
v_func[i].hash, v_func[j].hash,
35+
"Hash values of {f:?} are not equal: {} ≠ {}",
36+
v_file[i], v_file[j]
37+
);
38+
// if v_func[i].hash == v_func[j].hash {
39+
// println!("Hash values of {f:?} are not equal: {} ≠ {}", v_file[i], v_file[j]);
40+
// }
4141
}
4242
}
4343
}

‎tests/snapshots/by_macros/gen_contracts_by_macros.json‎

Lines changed: 96 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
[
22
{
3-
"hash": "845442505770887177010392654257959311323",
3+
"hash": "50317602858703944474094180767144751790",
44
"def_id": "DefId { id: 13, name: \"verify::proof1\" }",
55
"attrs": [
66
"#[kanitool::proof_for_contract = \"contract1\"]"
@@ -12,7 +12,7 @@
1212
"src": "fn $proof() {\n $contract_name(kani::any::<u8>());\n }",
1313
"before_expansion": "gen! { proof1: contract1(arg), arg > 0}"
1414
},
15-
"callees_len": 3,
15+
"callees_len": 6,
1616
"callees": [
1717
{
1818
"def_id": "DefId { id: 0, name: \"verify::contract1\" }",
@@ -34,6 +34,36 @@
3434
"before_expansion": "#[kani::requires($e)]"
3535
}
3636
},
37+
{
38+
"def_id": "DefId { id: 1, name: \"verify::contract1::kani_register_contract\" }",
39+
"func": {
40+
"name": "verify::contract1::kani_register_contract::<u8, {closure@tests/proofs/gen_contracts_by_macros.rs:3:9: 3:30}>",
41+
"kind": "Item",
42+
"file": "tests/proofs/gen_contracts_by_macros.rs",
43+
"src": "#[kani::requires($e)]",
44+
"before_expansion": "#[kani::requires($e)]"
45+
}
46+
},
47+
{
48+
"def_id": "DefId { id: 1, name: \"verify::contract1::kani_register_contract\" }",
49+
"func": {
50+
"name": "verify::contract1::kani_register_contract::<u8, {closure@tests/proofs/gen_contracts_by_macros.rs:3:9: 3:30}>",
51+
"kind": "Item",
52+
"file": "tests/proofs/gen_contracts_by_macros.rs",
53+
"src": "#[kani::requires($e)]",
54+
"before_expansion": "#[kani::requires($e)]"
55+
}
56+
},
57+
{
58+
"def_id": "DefId { id: 1, name: \"verify::contract1::kani_register_contract\" }",
59+
"func": {
60+
"name": "verify::contract1::kani_register_contract::<u8, {closure@tests/proofs/gen_contracts_by_macros.rs:3:9: 3:30}>",
61+
"kind": "Item",
62+
"file": "tests/proofs/gen_contracts_by_macros.rs",
63+
"src": "#[kani::requires($e)]",
64+
"before_expansion": "#[kani::requires($e)]"
65+
}
66+
},
3767
{
3868
"def_id": "DefId { id: 1, name: \"verify::contract1::kani_register_contract\" }",
3969
"func": {
@@ -47,7 +77,7 @@
4777
]
4878
},
4979
{
50-
"hash": "626547758136143336212812375568748807677",
80+
"hash": "123668483634893862457299768406549499156",
5181
"def_id": "DefId { id: 27, name: \"verify::proof2\" }",
5282
"attrs": [
5383
"#[kanitool::proof_for_contract = \"contract2\"]"
@@ -59,7 +89,7 @@
5989
"src": "fn $proof() {\n $contract_name(kani::any::<u8>());\n }",
6090
"before_expansion": "gen! { proof2: contract2(arg), arg != 0}"
6191
},
62-
"callees_len": 3,
92+
"callees_len": 6,
6393
"callees": [
6494
{
6595
"def_id": "DefId { id: 14, name: \"verify::contract2\" }",
@@ -81,6 +111,36 @@
81111
"before_expansion": "#[kani::requires($e)]"
82112
}
83113
},
114+
{
115+
"def_id": "DefId { id: 15, name: \"verify::contract2::kani_register_contract\" }",
116+
"func": {
117+
"name": "verify::contract2::kani_register_contract::<u8, {closure@tests/proofs/gen_contracts_by_macros.rs:3:9: 3:30}>",
118+
"kind": "Item",
119+
"file": "tests/proofs/gen_contracts_by_macros.rs",
120+
"src": "#[kani::requires($e)]",
121+
"before_expansion": "#[kani::requires($e)]"
122+
}
123+
},
124+
{
125+
"def_id": "DefId { id: 15, name: \"verify::contract2::kani_register_contract\" }",
126+
"func": {
127+
"name": "verify::contract2::kani_register_contract::<u8, {closure@tests/proofs/gen_contracts_by_macros.rs:3:9: 3:30}>",
128+
"kind": "Item",
129+
"file": "tests/proofs/gen_contracts_by_macros.rs",
130+
"src": "#[kani::requires($e)]",
131+
"before_expansion": "#[kani::requires($e)]"
132+
}
133+
},
134+
{
135+
"def_id": "DefId { id: 15, name: \"verify::contract2::kani_register_contract\" }",
136+
"func": {
137+
"name": "verify::contract2::kani_register_contract::<u8, {closure@tests/proofs/gen_contracts_by_macros.rs:3:9: 3:30}>",
138+
"kind": "Item",
139+
"file": "tests/proofs/gen_contracts_by_macros.rs",
140+
"src": "#[kani::requires($e)]",
141+
"before_expansion": "#[kani::requires($e)]"
142+
}
143+
},
84144
{
85145
"def_id": "DefId { id: 15, name: \"verify::contract2::kani_register_contract\" }",
86146
"func": {
@@ -94,7 +154,7 @@
94154
]
95155
},
96156
{
97-
"hash": "1808781832361317200114116752328221501869",
157+
"hash": "55432547161220750194751943225746429104",
98158
"def_id": "DefId { id: 41, name: \"verify::proof3\" }",
99159
"attrs": [
100160
"#[kanitool::proof_for_contract = \"contract3\"]"
@@ -106,7 +166,7 @@
106166
"src": "fn $proof() {\n $contract_name(kani::any::<u8>());\n }",
107167
"before_expansion": "gen! { proof3: contract3(arg), arg < 10}"
108168
},
109-
"callees_len": 3,
169+
"callees_len": 6,
110170
"callees": [
111171
{
112172
"def_id": "DefId { id: 28, name: \"verify::contract3\" }",
@@ -128,6 +188,36 @@
128188
"before_expansion": "#[kani::requires($e)]"
129189
}
130190
},
191+
{
192+
"def_id": "DefId { id: 29, name: \"verify::contract3::kani_register_contract\" }",
193+
"func": {
194+
"name": "verify::contract3::kani_register_contract::<u8, {closure@tests/proofs/gen_contracts_by_macros.rs:3:9: 3:30}>",
195+
"kind": "Item",
196+
"file": "tests/proofs/gen_contracts_by_macros.rs",
197+
"src": "#[kani::requires($e)]",
198+
"before_expansion": "#[kani::requires($e)]"
199+
}
200+
},
201+
{
202+
"def_id": "DefId { id: 29, name: \"verify::contract3::kani_register_contract\" }",
203+
"func": {
204+
"name": "verify::contract3::kani_register_contract::<u8, {closure@tests/proofs/gen_contracts_by_macros.rs:3:9: 3:30}>",
205+
"kind": "Item",
206+
"file": "tests/proofs/gen_contracts_by_macros.rs",
207+
"src": "#[kani::requires($e)]",
208+
"before_expansion": "#[kani::requires($e)]"
209+
}
210+
},
211+
{
212+
"def_id": "DefId { id: 29, name: \"verify::contract3::kani_register_contract\" }",
213+
"func": {
214+
"name": "verify::contract3::kani_register_contract::<u8, {closure@tests/proofs/gen_contracts_by_macros.rs:3:9: 3:30}>",
215+
"kind": "Item",
216+
"file": "tests/proofs/gen_contracts_by_macros.rs",
217+
"src": "#[kani::requires($e)]",
218+
"before_expansion": "#[kani::requires($e)]"
219+
}
220+
},
131221
{
132222
"def_id": "DefId { id: 29, name: \"verify::contract3::kani_register_contract\" }",
133223
"func": {

0 commit comments

Comments
 (0)