Skip to content

Commit 0908356

Browse files
zjp-CNzjp-CN
authored
Merge pull request #38 from os-checker/test-macro-expansion
test: support generating contract proofs by macro
2 parents 9a6ca71 + f418d73 commit 0908356

File tree

10 files changed

+6462
-13
lines changed

10 files changed

+6462
-13
lines changed

‎Cargo.lock‎

Lines changed: 1 addition & 0 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

‎Cargo.toml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ edition = "2024"
66
[dependencies]
77
clap = { version = "4.5.35", features = ["derive"] }
88
serde = { version = "1", features = ["derive"] }
9-
serde_json = "1"
9+
serde_json = { version = "1", features = ["preserve_order"] }
1010
indexmap = "2.9.0"
1111

1212
# error handling

‎src/lib.rs‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
use serde::{Deserialize, Serialize};
22

33
/// A Rust funtion with its file source, attributes, and raw function content.
4-
#[derive(Debug, Serialize, Deserialize)]
4+
#[derive(Debug, Serialize, Deserialize, Clone)]
55
pub struct SerFunction {
66
pub hash: String,
77
/// DefId in stable_mir.
@@ -15,13 +15,13 @@ pub struct SerFunction {
1515
pub callees: Vec<Callee>,
1616
}
1717

18-
#[derive(Debug, Serialize, Deserialize)]
18+
#[derive(Debug, Serialize, Deserialize, Clone)]
1919
pub struct Callee {
2020
pub def_id: String,
2121
pub func: SourceCode,
2222
}
2323

24-
#[derive(Debug, Serialize, Deserialize)]
24+
#[derive(Debug, Serialize, Deserialize, Clone)]
2525
pub struct SourceCode {
2626
// A file path where src lies.
2727
// The path is stripped with pwd or sysroot prefix.

‎tests/proofs.rs‎

Lines changed: 40 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -40,14 +40,38 @@ fn assert_unique_hash(proofs: &[PathBuf], v_json: &[Vec<SerFunction>]) {
4040
}
4141
}
4242

43+
fn extract_macros_items(json: &[SerFunction]) -> Vec<SerFunction> {
44+
// all proofs are generated by macros, so just filter out
45+
// callees that are not directly locally defined (i.e.
46+
// filter out kani items).
47+
json.iter()
48+
.map(|j| {
49+
let callees = j
50+
.callees
51+
.iter()
52+
.filter(|callee| callee.def_id.contains("\"verify::"))
53+
.cloned()
54+
.collect();
55+
SerFunction {
56+
hash: j.hash.clone(),
57+
def_id: j.def_id.clone(),
58+
attrs: j.attrs.clone(),
59+
func: j.func.clone(),
60+
callees,
61+
}
62+
})
63+
.collect()
64+
}
65+
4366
#[test]
4467
fn test_proofs() -> Result<()> {
4568
let proofs = get_proofs("tests/proofs")?;
4669

4770
expect![[r#"
4871
[
4972
"tests/proofs/ad_hoc.rs",
50-
"tests/proofs/gen_by_macros.rs",
73+
"tests/proofs/gen_contracts_by_macros.rs",
74+
"tests/proofs/gen_proofs_by_macros.rs",
5175
"tests/proofs/proofs_for_contract.rs",
5276
"tests/proofs/standard_proofs.rs",
5377
"tests/proofs/standard_proofs_with_contracts.rs",
@@ -56,19 +80,32 @@ fn test_proofs() -> Result<()> {
5680
.assert_debug_eq(&proofs);
5781

5882
let mut v_json = Vec::<Vec<SerFunction>>::with_capacity(proofs.len());
59-
for path in &proofs {
83+
let mut v_macro = vec![];
84+
for (idx, path) in proofs.iter().enumerate() {
6085
let file_stem = path.file_stem().and_then(|f| f.to_str()).unwrap();
6186
let text = cmd(&[&format!("tests/proofs/{file_stem}.rs")]);
6287
expect_file![format!("./snapshots/{file_stem}.json")].assert_eq(&text);
6388
v_json.push(serde_json::from_str(&text).unwrap());
89+
// collect macro generated proofs
90+
if file_stem.ends_with("by_macros") {
91+
v_macro.push((idx, file_stem));
92+
}
6493
}
6594

6695
assert_unique_hash(&proofs, &v_json);
96+
97+
// take snapshots on macro generated local items
98+
for (idx, file_stem) in v_macro {
99+
let json = extract_macros_items(&v_json[idx]);
100+
let text = serde_json::to_string_pretty(&json).unwrap();
101+
expect_file![format!("./snapshots/by_macros/{file_stem}.json")].assert_eq(&text);
102+
}
103+
67104
Ok(())
68105
}
69106

70107
#[test]
71-
fn test_compare() -> Result<()> {
108+
fn test_compare_unique_hash() -> Result<()> {
72109
let proofs = get_proofs("tests/compare")?;
73110

74111
expect![[r#"

‎tests/proofs/gen_contracts_by_macros.rs‎

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
macro_rules! gen {
2+
($proof:ident: $contract_name:ident($arg:ident), $e:expr) => {
3+
#[kani::requires($e)]
4+
fn $contract_name($arg: u8) -> u8 { $arg }
5+
6+
#[kani::proof_for_contract($contract_name)]
7+
fn $proof() {
8+
$contract_name(kani::any::<u8>());
9+
}
10+
}
11+
}
12+
13+
#[cfg(kani)]
14+
mod verify {
15+
gen! { proof1: contract1(arg), arg > 0}
16+
gen! { proof2: contract2(arg), arg != 0}
17+
gen! { proof3: contract3(arg), arg < 10}
18+
}

‎tests/proofs/gen_by_macros.rs‎ renamed to ‎tests/proofs/gen_proofs_by_macros.rs‎

File renamed without changes.

‎tests/snapshots/by_macros/gen_contracts_by_macros.json‎

Lines changed: 188 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,188 @@
1+
[
2+
{
3+
"hash": "173901617224167753396123006979376078418",
4+
"def_id": "DefId { id: 13, name: \"verify::proof1\" }",
5+
"attrs": [
6+
"#[kanitool::proof_for_contract = \"contract1\"]"
7+
],
8+
"func": {
9+
"file": "tests/proofs/gen_contracts_by_macros.rs",
10+
"src": "fn $proof() {\n $contract_name(kani::any::<u8>());\n }",
11+
"before_expansion": "gen! { proof1: contract1(arg), arg > 0}"
12+
},
13+
"callees": [
14+
{
15+
"def_id": "DefId { id: 1, name: \"verify::contract1::kani_register_contract\" }",
16+
"func": {
17+
"file": "tests/proofs/gen_contracts_by_macros.rs",
18+
"src": "#[kani::requires($e)]",
19+
"before_expansion": "#[kani::requires($e)]"
20+
}
21+
},
22+
{
23+
"def_id": "DefId { id: 1, name: \"verify::contract1::kani_register_contract\" }",
24+
"func": {
25+
"file": "tests/proofs/gen_contracts_by_macros.rs",
26+
"src": "#[kani::requires($e)]",
27+
"before_expansion": "#[kani::requires($e)]"
28+
}
29+
},
30+
{
31+
"def_id": "DefId { id: 2, name: \"verify::contract1::kani_contract_mode\" }",
32+
"func": {
33+
"file": "tests/proofs/gen_contracts_by_macros.rs",
34+
"src": "#[kani::requires($e)]",
35+
"before_expansion": "#[kani::requires($e)]"
36+
}
37+
},
38+
{
39+
"def_id": "DefId { id: 1, name: \"verify::contract1::kani_register_contract\" }",
40+
"func": {
41+
"file": "tests/proofs/gen_contracts_by_macros.rs",
42+
"src": "#[kani::requires($e)]",
43+
"before_expansion": "#[kani::requires($e)]"
44+
}
45+
},
46+
{
47+
"def_id": "DefId { id: 1, name: \"verify::contract1::kani_register_contract\" }",
48+
"func": {
49+
"file": "tests/proofs/gen_contracts_by_macros.rs",
50+
"src": "#[kani::requires($e)]",
51+
"before_expansion": "#[kani::requires($e)]"
52+
}
53+
},
54+
{
55+
"def_id": "DefId { id: 0, name: \"verify::contract1\" }",
56+
"func": {
57+
"file": "tests/proofs/gen_contracts_by_macros.rs",
58+
"src": "fn",
59+
"before_expansion": "gen! { proof1: contract1(arg), arg > 0}"
60+
}
61+
}
62+
]
63+
},
64+
{
65+
"hash": "123976172475411212985328458414396205982",
66+
"def_id": "DefId { id: 27, name: \"verify::proof2\" }",
67+
"attrs": [
68+
"#[kanitool::proof_for_contract = \"contract2\"]"
69+
],
70+
"func": {
71+
"file": "tests/proofs/gen_contracts_by_macros.rs",
72+
"src": "fn $proof() {\n $contract_name(kani::any::<u8>());\n }",
73+
"before_expansion": "gen! { proof2: contract2(arg), arg != 0}"
74+
},
75+
"callees": [
76+
{
77+
"def_id": "DefId { id: 15, name: \"verify::contract2::kani_register_contract\" }",
78+
"func": {
79+
"file": "tests/proofs/gen_contracts_by_macros.rs",
80+
"src": "#[kani::requires($e)]",
81+
"before_expansion": "#[kani::requires($e)]"
82+
}
83+
},
84+
{
85+
"def_id": "DefId { id: 15, name: \"verify::contract2::kani_register_contract\" }",
86+
"func": {
87+
"file": "tests/proofs/gen_contracts_by_macros.rs",
88+
"src": "#[kani::requires($e)]",
89+
"before_expansion": "#[kani::requires($e)]"
90+
}
91+
},
92+
{
93+
"def_id": "DefId { id: 15, name: \"verify::contract2::kani_register_contract\" }",
94+
"func": {
95+
"file": "tests/proofs/gen_contracts_by_macros.rs",
96+
"src": "#[kani::requires($e)]",
97+
"before_expansion": "#[kani::requires($e)]"
98+
}
99+
},
100+
{
101+
"def_id": "DefId { id: 15, name: \"verify::contract2::kani_register_contract\" }",
102+
"func": {
103+
"file": "tests/proofs/gen_contracts_by_macros.rs",
104+
"src": "#[kani::requires($e)]",
105+
"before_expansion": "#[kani::requires($e)]"
106+
}
107+
},
108+
{
109+
"def_id": "DefId { id: 16, name: \"verify::contract2::kani_contract_mode\" }",
110+
"func": {
111+
"file": "tests/proofs/gen_contracts_by_macros.rs",
112+
"src": "#[kani::requires($e)]",
113+
"before_expansion": "#[kani::requires($e)]"
114+
}
115+
},
116+
{
117+
"def_id": "DefId { id: 14, name: \"verify::contract2\" }",
118+
"func": {
119+
"file": "tests/proofs/gen_contracts_by_macros.rs",
120+
"src": "fn",
121+
"before_expansion": "gen! { proof2: contract2(arg), arg != 0}"
122+
}
123+
}
124+
]
125+
},
126+
{
127+
"hash": "65100024384283587041305320168463434750",
128+
"def_id": "DefId { id: 41, name: \"verify::proof3\" }",
129+
"attrs": [
130+
"#[kanitool::proof_for_contract = \"contract3\"]"
131+
],
132+
"func": {
133+
"file": "tests/proofs/gen_contracts_by_macros.rs",
134+
"src": "fn $proof() {\n $contract_name(kani::any::<u8>());\n }",
135+
"before_expansion": "gen! { proof3: contract3(arg), arg < 10}"
136+
},
137+
"callees": [
138+
{
139+
"def_id": "DefId { id: 29, name: \"verify::contract3::kani_register_contract\" }",
140+
"func": {
141+
"file": "tests/proofs/gen_contracts_by_macros.rs",
142+
"src": "#[kani::requires($e)]",
143+
"before_expansion": "#[kani::requires($e)]"
144+
}
145+
},
146+
{
147+
"def_id": "DefId { id: 30, name: \"verify::contract3::kani_contract_mode\" }",
148+
"func": {
149+
"file": "tests/proofs/gen_contracts_by_macros.rs",
150+
"src": "#[kani::requires($e)]",
151+
"before_expansion": "#[kani::requires($e)]"
152+
}
153+
},
154+
{
155+
"def_id": "DefId { id: 29, name: \"verify::contract3::kani_register_contract\" }",
156+
"func": {
157+
"file": "tests/proofs/gen_contracts_by_macros.rs",
158+
"src": "#[kani::requires($e)]",
159+
"before_expansion": "#[kani::requires($e)]"
160+
}
161+
},
162+
{
163+
"def_id": "DefId { id: 29, name: \"verify::contract3::kani_register_contract\" }",
164+
"func": {
165+
"file": "tests/proofs/gen_contracts_by_macros.rs",
166+
"src": "#[kani::requires($e)]",
167+
"before_expansion": "#[kani::requires($e)]"
168+
}
169+
},
170+
{
171+
"def_id": "DefId { id: 29, name: \"verify::contract3::kani_register_contract\" }",
172+
"func": {
173+
"file": "tests/proofs/gen_contracts_by_macros.rs",
174+
"src": "#[kani::requires($e)]",
175+
"before_expansion": "#[kani::requires($e)]"
176+
}
177+
},
178+
{
179+
"def_id": "DefId { id: 28, name: \"verify::contract3\" }",
180+
"func": {
181+
"file": "tests/proofs/gen_contracts_by_macros.rs",
182+
"src": "fn",
183+
"before_expansion": "gen! { proof3: contract3(arg), arg < 10}"
184+
}
185+
}
186+
]
187+
}
188+
]

‎tests/snapshots/by_macros/gen_proofs_by_macros.json‎

Lines changed: 41 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,41 @@
1+
[
2+
{
3+
"hash": "46016022776817712457248418356562080180",
4+
"def_id": "DefId { id: 0, name: \"verify::proof1\" }",
5+
"attrs": [
6+
"#[kanitool::proof]"
7+
],
8+
"func": {
9+
"file": "tests/proofs/gen_proofs_by_macros.rs",
10+
"src": "fn $name() $block",
11+
"before_expansion": "gen! { proof1, { assert_eq!(kani::any::<u8>(), 0) }}"
12+
},
13+
"callees": []
14+
},
15+
{
16+
"hash": "790930765940395853317344064822859799449",
17+
"def_id": "DefId { id: 1, name: \"verify::proof2\" }",
18+
"attrs": [
19+
"#[kanitool::proof]"
20+
],
21+
"func": {
22+
"file": "tests/proofs/gen_proofs_by_macros.rs",
23+
"src": "fn $name() $block",
24+
"before_expansion": "gen! { proof2, { assert_eq!(kani::any::<u8>(), 0) }}"
25+
},
26+
"callees": []
27+
},
28+
{
29+
"hash": "1212665539524790206110637770712875499847",
30+
"def_id": "DefId { id: 2, name: \"verify::proof3\" }",
31+
"attrs": [
32+
"#[kanitool::proof]"
33+
],
34+
"func": {
35+
"file": "tests/proofs/gen_proofs_by_macros.rs",
36+
"src": "fn $name() $block",
37+
"before_expansion": "gen! { proof3, { assert_eq!(kani::any::<u8>(), 1) }}"
38+
},
39+
"callees": []
40+
}
41+
]

0 commit comments

Comments
 (0)