Skip to content

Commit 2446466

Browse files
zjp-CNzjp-CN
committed
test: add kani_list to snapshot all proofs
1 parent 03388f3 commit 2446466

11 files changed

+252
-19
lines changed

‎.gitignore‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,7 @@
11
/target
22

3+
# kani list
4+
kani-list.json
5+
36
# ignore kani folder for grep or files findings
47
# kani

‎tests/kani_list.rs‎

Lines changed: 37 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,37 @@
1+
use distributed_verification::KaniList;
2+
use std::process::Command;
3+
4+
mod utils;
5+
use utils::*;
6+
7+
#[test]
8+
fn validate_kani_list_json() -> Result<()> {
9+
let proofs = get_proofs("tests/proofs")?;
10+
11+
for path in &proofs {
12+
let kani_list = get_kani_list(path.to_str().unwrap());
13+
let file_stem = file_stem(path);
14+
let list_path = format!("kani_list/{file_stem}.txt");
15+
dbg!(&list_path);
16+
expect_file![list_path].assert_debug_eq(&kani_list);
17+
}
18+
19+
Ok(())
20+
}
21+
22+
fn get_kani_list(file: &str) -> KaniList {
23+
// kani list -Zlist --format=json file.rs
24+
let output = Command::new("kani")
25+
.args(["list", "-Zlist", "-Zfunction-contracts", "--format=json", file])
26+
.output()
27+
.unwrap();
28+
assert!(
29+
output.status.success(),
30+
"Failed to run `kani list -Zlist --format=json {file}`:\n{}",
31+
std::str::from_utf8(&output.stderr).unwrap()
32+
);
33+
34+
// read kani-list.json
35+
let file_json = std::fs::File::open("kani-list.json").unwrap();
36+
serde_json::from_reader(file_json).unwrap()
37+
}

‎tests/kani_list/ad_hoc.txt‎

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
KaniList {
2+
kani_version: "0.60.0",
3+
file_version: "0.1",
4+
standard_harnesses: {
5+
"tests/proofs/ad_hoc.rs": {
6+
"adhoc::callee_defined_in_proof",
7+
"adhoc::closure_in_proof",
8+
"adhoc::proof_in_fn_item::proof",
9+
},
10+
},
11+
contract_harnesses: {},
12+
contracts: {},
13+
totals: Total {
14+
standard_harnesses: 3,
15+
contract_harnesses: 0,
16+
functions_under_contract: 0,
17+
},
18+
}

‎tests/kani_list/gen_contracts_by_macros.txt‎

Lines changed: 40 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,40 @@
1+
KaniList {
2+
kani_version: "0.60.0",
3+
file_version: "0.1",
4+
standard_harnesses: {},
5+
contract_harnesses: {
6+
"tests/proofs/gen_contracts_by_macros.rs": {
7+
"verify::proof1",
8+
"verify::proof2",
9+
"verify::proof3",
10+
},
11+
},
12+
contracts: {
13+
ContractedFunction {
14+
function: "verify::contract1",
15+
file: "tests/proofs/gen_contracts_by_macros.rs",
16+
harnesses: [
17+
"verify::proof1",
18+
],
19+
},
20+
ContractedFunction {
21+
function: "verify::contract2",
22+
file: "tests/proofs/gen_contracts_by_macros.rs",
23+
harnesses: [
24+
"verify::proof2",
25+
],
26+
},
27+
ContractedFunction {
28+
function: "verify::contract3",
29+
file: "tests/proofs/gen_contracts_by_macros.rs",
30+
harnesses: [
31+
"verify::proof3",
32+
],
33+
},
34+
},
35+
totals: Total {
36+
standard_harnesses: 0,
37+
contract_harnesses: 3,
38+
functions_under_contract: 3,
39+
},
40+
}

‎tests/kani_list/gen_proofs_by_macros.txt‎

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
KaniList {
2+
kani_version: "0.60.0",
3+
file_version: "0.1",
4+
standard_harnesses: {
5+
"tests/proofs/gen_proofs_by_macros.rs": {
6+
"verify::proof1",
7+
"verify::proof2",
8+
"verify::proof3",
9+
},
10+
},
11+
contract_harnesses: {},
12+
contracts: {},
13+
totals: Total {
14+
standard_harnesses: 3,
15+
contract_harnesses: 0,
16+
functions_under_contract: 0,
17+
},
18+
}

‎tests/kani_list/gen_proofs_by_nested_macros.txt‎

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
KaniList {
2+
kani_version: "0.60.0",
3+
file_version: "0.1",
4+
standard_harnesses: {
5+
"tests/proofs/gen_proofs_by_nested_macros.rs": {
6+
"verify::proof1",
7+
"verify::proof2",
8+
"verify::proof3",
9+
},
10+
},
11+
contract_harnesses: {},
12+
contracts: {},
13+
totals: Total {
14+
standard_harnesses: 3,
15+
contract_harnesses: 0,
16+
functions_under_contract: 0,
17+
},
18+
}

‎tests/kani_list/proofs_for_contract.txt‎

Lines changed: 42 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,42 @@
1+
KaniList {
2+
kani_version: "0.60.0",
3+
file_version: "0.1",
4+
standard_harnesses: {},
5+
contract_harnesses: {
6+
"tests/proofs/proofs_for_contract.rs": {
7+
"verify::single_contract",
8+
"verify::single_contract_requires",
9+
"verify::single_with_contract_ensures",
10+
"verify::two_contracts_requires_and_ensures",
11+
},
12+
},
13+
contracts: {
14+
ContractedFunction {
15+
function: "verify::contract",
16+
file: "tests/proofs/proofs_for_contract.rs",
17+
harnesses: [
18+
"verify::single_contract",
19+
],
20+
},
21+
ContractedFunction {
22+
function: "verify::contract_ensures",
23+
file: "tests/proofs/proofs_for_contract.rs",
24+
harnesses: [
25+
"verify::single_with_contract_ensures",
26+
],
27+
},
28+
ContractedFunction {
29+
function: "verify::contract_requires",
30+
file: "tests/proofs/proofs_for_contract.rs",
31+
harnesses: [
32+
"verify::single_contract_requires",
33+
"verify::two_contracts_requires_and_ensures",
34+
],
35+
},
36+
},
37+
totals: Total {
38+
standard_harnesses: 0,
39+
contract_harnesses: 4,
40+
functions_under_contract: 3,
41+
},
42+
}

‎tests/kani_list/standard_proofs.txt‎

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
KaniList {
2+
kani_version: "0.60.0",
3+
file_version: "0.1",
4+
standard_harnesses: {
5+
"tests/proofs/standard_proofs.rs": {
6+
"verify::recursive_callees",
7+
"verify::standard_proof",
8+
"verify::standard_proof_empty",
9+
},
10+
},
11+
contract_harnesses: {},
12+
contracts: {},
13+
totals: Total {
14+
standard_harnesses: 3,
15+
contract_harnesses: 0,
16+
functions_under_contract: 0,
17+
},
18+
}

‎tests/kani_list/standard_proofs_with_contracts.txt‎

Lines changed: 35 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,35 @@
1+
KaniList {
2+
kani_version: "0.60.0",
3+
file_version: "0.1",
4+
standard_harnesses: {
5+
"tests/proofs/standard_proofs_with_contracts.rs": {
6+
"verify::single_contract",
7+
"verify::single_contract_requires",
8+
"verify::single_with_contract_ensures",
9+
"verify::two_contracts_requires_and_ensures",
10+
},
11+
},
12+
contract_harnesses: {},
13+
contracts: {
14+
ContractedFunction {
15+
function: "verify::contract",
16+
file: "tests/proofs/standard_proofs_with_contracts.rs",
17+
harnesses: [],
18+
},
19+
ContractedFunction {
20+
function: "verify::contract_ensures",
21+
file: "tests/proofs/standard_proofs_with_contracts.rs",
22+
harnesses: [],
23+
},
24+
ContractedFunction {
25+
function: "verify::contract_requires",
26+
file: "tests/proofs/standard_proofs_with_contracts.rs",
27+
harnesses: [],
28+
},
29+
},
30+
totals: Total {
31+
standard_harnesses: 4,
32+
contract_harnesses: 0,
33+
functions_under_contract: 3,
34+
},
35+
}

‎tests/proofs.rs‎

Lines changed: 1 addition & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -4,21 +4,6 @@ use std::path::{Path, PathBuf};
44
mod utils;
55
use utils::{assert_eq, *};
66

7-
fn get_proofs(dir: &str) -> Result<Vec<PathBuf>> {
8-
let mut proofs = vec![];
9-
for entry in std::fs::read_dir(dir)? {
10-
let entry = entry?;
11-
let path = entry.path();
12-
if path.is_file()
13-
&& path.extension().and_then(|ext| Some(ext.to_str()? == "rs")).unwrap_or(false)
14-
{
15-
proofs.push(path);
16-
}
17-
}
18-
proofs.sort();
19-
Ok(proofs)
20-
}
21-
227
fn assert_unique_hash(proofs: &[PathBuf], v_json: &[Vec<SerFunction>]) {
238
let mut map = IndexMap::<&str, Vec<(&Path, &str)>>::new();
249
for (v, proof) in v_json.iter().zip(proofs) {
@@ -84,7 +69,7 @@ fn test_proofs() -> Result<()> {
8469
let mut v_json = Vec::<Vec<SerFunction>>::with_capacity(proofs.len());
8570
let mut v_macro = vec![];
8671
for (idx, path) in proofs.iter().enumerate() {
87-
let file_stem = path.file_stem().and_then(|f| f.to_str()).unwrap();
72+
let file_stem = file_stem(path);
8873
let text = cmd(&[&format!("tests/proofs/{file_stem}.rs")]);
8974
expect_file![format!("./snapshots/{file_stem}.json")].assert_eq(&text);
9075
v_json.push(serde_json::from_str(&text).unwrap());

0 commit comments

Comments
 (0)