Skip to content

Commit 0e127b0

Browse files
zjp-CNzjp-CN
committed
lib: move get_kani_list and check functions to kani_list module
1 parent c065104 commit 0e127b0

File tree

3 files changed

+105
-94
lines changed

3 files changed

+105
-94
lines changed

‎src/kani_list.rs‎

Lines changed: 100 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,100 @@
1+
use indexmap::{IndexMap, IndexSet};
2+
use serde::{Deserialize, Serialize};
3+
use std::{collections::HashMap, process::Command};
4+
5+
use crate::{Kind, SerFunction};
6+
7+
/// Output of `kani list` command.
8+
#[derive(Debug, Serialize, Deserialize, Clone)]
9+
#[serde(rename_all = "kebab-case")]
10+
pub struct KaniList {
11+
pub kani_version: String,
12+
pub file_version: String,
13+
pub standard_harnesses: IndexMap<String, IndexSet<String>>,
14+
pub contract_harnesses: IndexMap<String, IndexSet<String>>,
15+
pub contracts: IndexSet<ContractedFunction>,
16+
pub totals: Total,
17+
}
18+
19+
#[derive(Debug, Serialize, Deserialize, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
20+
pub struct ContractedFunction {
21+
pub function: String,
22+
pub file: String,
23+
pub harnesses: Vec<String>,
24+
}
25+
26+
#[derive(Debug, Serialize, Deserialize, Clone)]
27+
#[serde(rename_all = "kebab-case")]
28+
pub struct Total {
29+
pub standard_harnesses: usize,
30+
pub contract_harnesses: usize,
31+
pub functions_under_contract: usize,
32+
}
33+
34+
/// Get kani list and check if it complies with Vec<SerFunction>.
35+
pub fn check(file: &str, v_ser_fun: &[SerFunction]) {
36+
let list = get_kani_list(file);
37+
check_proofs(&list, v_ser_fun);
38+
}
39+
40+
pub fn get_kani_list(file: &str) -> KaniList {
41+
// kani list -Zlist -Zfunction-contracts --format=json file.rs
42+
let args = ["list", "-Zlist", "-Zfunction-contracts", "--format=json", file];
43+
let output = Command::new("kani").args(args).output().unwrap();
44+
assert!(
45+
output.status.success(),
46+
"Failed to run `kani list -Zlist -Zfunction-contracts --format=json {file}`:\n{}",
47+
std::str::from_utf8(&output.stderr).unwrap()
48+
);
49+
50+
// read kani-list.json
51+
let file_json = std::fs::File::open("kani-list.json").unwrap();
52+
serde_json::from_reader(file_json).unwrap()
53+
}
54+
55+
pub fn check_proofs(list: &KaniList, v_ser_fun: &[SerFunction]) {
56+
// sanity check
57+
let totals = &list.totals;
58+
assert_eq!(v_ser_fun.len(), totals.standard_harnesses + totals.contract_harnesses);
59+
assert_eq!(
60+
list.standard_harnesses.values().map(|s| s.len()).sum::<usize>(),
61+
totals.standard_harnesses
62+
);
63+
assert_eq!(
64+
list.contract_harnesses.values().map(|s| s.len()).sum::<usize>(),
65+
totals.contract_harnesses
66+
);
67+
68+
let map: HashMap<_, _> = v_ser_fun
69+
.iter()
70+
.enumerate()
71+
.map(|(idx, f)| ((&*f.func.file, &*f.func.name), (idx, f.kind)))
72+
.collect();
73+
74+
// check all standard proofs are in distributed-verification json
75+
for (path, proofs) in &list.standard_harnesses {
76+
for proof in proofs {
77+
let key = (path.as_str(), proof.as_str());
78+
let val = map.get(&key).unwrap();
79+
dbg!(val);
80+
}
81+
}
82+
83+
// check all contract proofs are in distributed-verification json
84+
for (path, proofs) in &list.contract_harnesses {
85+
for proof in proofs {
86+
let key = (path.as_str(), proof.as_str());
87+
let idx = map.get(&key).unwrap();
88+
dbg!(idx);
89+
}
90+
}
91+
92+
// double check
93+
for (&(path, proof), &(_, kind)) in &map {
94+
let harnesses = match kind {
95+
Kind::Standard => &list.standard_harnesses[path],
96+
Kind::Contract => &list.contract_harnesses[path],
97+
};
98+
_ = harnesses.get(proof).unwrap();
99+
}
100+
}

‎src/lib.rs‎

Lines changed: 2 additions & 28 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
1-
use indexmap::{IndexMap, IndexSet};
21
use serde::{Deserialize, Serialize};
32

3+
pub mod kani_list;
4+
45
/// A kani proof with its file source, attributes, and raw function content.
56
#[derive(Debug, Default, Serialize, Deserialize, Clone)]
67
pub struct SerFunction {
@@ -96,30 +97,3 @@ pub fn kani_path() -> String {
9697
assert!(std::fs::exists(&path).unwrap());
9798
path
9899
}
99-
100-
/// Output of `kani list` command.
101-
#[derive(Debug, Serialize, Deserialize, Clone)]
102-
#[serde(rename_all = "kebab-case")]
103-
pub struct KaniList {
104-
pub kani_version: String,
105-
pub file_version: String,
106-
pub standard_harnesses: IndexMap<String, IndexSet<String>>,
107-
pub contract_harnesses: IndexMap<String, IndexSet<String>>,
108-
pub contracts: IndexSet<ContractedFunction>,
109-
pub totals: Total,
110-
}
111-
112-
#[derive(Debug, Serialize, Deserialize, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
113-
pub struct ContractedFunction {
114-
pub function: String,
115-
pub file: String,
116-
pub harnesses: Vec<String>,
117-
}
118-
119-
#[derive(Debug, Serialize, Deserialize, Clone)]
120-
#[serde(rename_all = "kebab-case")]
121-
pub struct Total {
122-
pub standard_harnesses: usize,
123-
pub contract_harnesses: usize,
124-
pub functions_under_contract: usize,
125-
}

‎tests/kani_list.rs‎

Lines changed: 3 additions & 66 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,7 @@
1-
use distributed_verification::{KaniList, Kind};
2-
use std::{collections::HashMap, process::Command};
1+
use distributed_verification::kani_list::{check_proofs, get_kani_list};
32

43
mod utils;
5-
use utils::{assert_eq, *};
4+
use utils::*;
65

76
#[test]
87
fn validate_kani_list_json() -> Result<()> {
@@ -21,70 +20,8 @@ fn validate_kani_list_json() -> Result<()> {
2120
// run `distributed_verification`
2221
let text = cmd(&[path]);
2322
let v_ser_function: Vec<SerFunction> = serde_json::from_str(&text).unwrap();
24-
merge(&kani_list, &v_ser_function);
23+
check_proofs(&kani_list, &v_ser_function);
2524
}
2625

2726
Ok(())
2827
}
29-
30-
fn get_kani_list(file: &str) -> KaniList {
31-
// kani list -Zlist -Zfunction-contracts --format=json file.rs
32-
let args = ["list", "-Zlist", "-Zfunction-contracts", "--format=json", file];
33-
let output = Command::new("kani").args(args).output().unwrap();
34-
assert!(
35-
output.status.success(),
36-
"Failed to run `kani list -Zlist -Zfunction-contracts --format=json {file}`:\n{}",
37-
std::str::from_utf8(&output.stderr).unwrap()
38-
);
39-
40-
// read kani-list.json
41-
let file_json = std::fs::File::open("kani-list.json").unwrap();
42-
serde_json::from_reader(file_json).unwrap()
43-
}
44-
45-
fn merge(list: &KaniList, v_ser_fun: &[SerFunction]) {
46-
// sanity check
47-
let totals = &list.totals;
48-
assert_eq!(v_ser_fun.len(), totals.standard_harnesses + totals.contract_harnesses);
49-
assert_eq!(
50-
list.standard_harnesses.values().map(|s| s.len()).sum::<usize>(),
51-
totals.standard_harnesses
52-
);
53-
assert_eq!(
54-
list.contract_harnesses.values().map(|s| s.len()).sum::<usize>(),
55-
totals.contract_harnesses
56-
);
57-
58-
let map: HashMap<_, _> = v_ser_fun
59-
.iter()
60-
.enumerate()
61-
.map(|(idx, f)| ((&*f.func.file, &*f.func.name), (idx, f.kind)))
62-
.collect();
63-
64-
// check all standard proofs are in distributed-verification json
65-
for (path, proofs) in &list.standard_harnesses {
66-
for proof in proofs {
67-
let key = (path.as_str(), proof.as_str());
68-
let val = map.get(&key).unwrap();
69-
dbg!(val);
70-
}
71-
}
72-
73-
// check all contract proofs are in distributed-verification json
74-
for (path, proofs) in &list.contract_harnesses {
75-
for proof in proofs {
76-
let key = (path.as_str(), proof.as_str());
77-
let idx = map.get(&key).unwrap();
78-
dbg!(idx);
79-
}
80-
}
81-
82-
// double check
83-
for (&(path, proof), &(_, kind)) in &map {
84-
let harnesses = match kind {
85-
Kind::Standard => &list.standard_harnesses[path],
86-
Kind::Contract => &list.contract_harnesses[path],
87-
};
88-
_ = harnesses.get(proof).unwrap();
89-
}
90-
}

0 commit comments

Comments
 (0)