distributed_verification/
diff.rs1use crate::{BoxStr, ProofKind, SerFunction};
2use indexmap::{IndexMap, IndexSet};
3use serde::{Deserialize, Serialize};
4use std::{
5 hash::Hash,
6 path::{Component, MAIN_SEPARATOR, Path, PathBuf},
7};
8
9#[derive(Debug, Clone, Serialize, Deserialize, Eq, PartialEq)]
12#[serde(transparent)]
13pub struct KaniListHarnesses {
14 pub inner: IndexMap<BoxStr, IndexSet<BoxStr>>,
15}
16
17impl KaniListHarnesses {
18 pub fn normalize_file_path(&mut self) {
19 pub fn normalize_path(path: &Path) -> String {
20 let mut components = path.components().peekable();
21 let mut ret = if let Some(c @ Component::Prefix(..)) = components.peek().cloned() {
22 components.next();
23 PathBuf::from(c.as_os_str())
24 } else {
25 PathBuf::new()
26 };
27
28 for component in components {
29 match component {
30 Component::Prefix(..) => unreachable!(),
31 Component::RootDir => {
32 ret.push(component.as_os_str());
33 }
34 Component::CurDir => {}
35 Component::ParentDir => {
36 ret.pop();
37 }
38 Component::Normal(c) => {
39 ret.push(c);
40 }
41 }
42 }
43 ret.display().to_string()
44 }
45
46 let mut inner = IndexMap::with_capacity(self.inner.len());
47 for (path, value) in self.inner.iter_mut() {
48 let key = normalize_path(&PathBuf::from(&**path)).into();
49 inner.insert(key, std::mem::take(value));
50 }
51 self.inner = inner;
52 }
53
54 pub fn strip_path_prefix(&mut self, prefix: &str) {
55 let mut map = IndexMap::with_capacity(self.inner.len());
56 for (key, val) in self.inner.iter_mut() {
57 let val = std::mem::take(val);
58 match key.strip_prefix(prefix) {
59 Some(stripped) => _ = map.insert(stripped.into(), val),
60 None => {
61 warn!("The key `{key}`\nis not stripped with prefix `{prefix}`.");
66 _ = map.insert(key.clone(), val);
67 }
68 }
69 }
70 map.sort_unstable_keys();
71 self.inner = map;
72 }
73
74 pub fn strip_path_closure_name(&mut self, v_text: &[&str]) {
75 for set in self.inner.values_mut() {
76 let mut stripped = IndexSet::with_capacity(set.len());
77 for name in set.iter() {
78 let mut new_name = String::new();
79 for text in v_text {
80 new_name = name.replace(text, "");
81 }
82 stripped.insert(new_name.into());
83 }
84 *set = stripped;
85 }
86 }
87
88 fn files(&self) -> Vec<&str> {
89 self.inner.keys().map(|s| &**s).collect()
90 }
91
92 fn names<'harness>(
95 &'harness self,
96 v: &mut Vec<&'harness str>,
97 mut filter: impl FnMut(&str, &str) -> bool,
98 ) {
99 for (file, harnesses) in &self.inner {
100 for name in harnesses {
101 if filter(file, name) {
102 v.push(&**name);
103 }
104 }
105 }
106 }
107}
108
109#[derive(Debug, Clone, Serialize, Deserialize, Eq, PartialEq, PartialOrd, Ord, Hash)]
110pub struct ContractedFunction {
111 pub function: BoxStr,
113 pub file: BoxStr,
115 pub harnesses: Box<[BoxStr]>,
117}
118
119#[derive(Debug, Clone, Serialize, Deserialize, Eq, PartialEq, PartialOrd, Ord)]
120#[serde(rename_all = "kebab-case")]
121pub struct Totals {
122 standard_harnesses: usize,
123 contract_harnesses: usize,
124 functions_under_contract: usize,
125}
126
127#[derive(Debug, Clone, Serialize, Deserialize, Eq, PartialEq)]
131#[serde(rename_all = "kebab-case")]
132pub struct KaniListJson {
133 pub kani_version: BoxStr,
134 pub file_version: BoxStr,
135 pub standard_harnesses: KaniListHarnesses,
136 pub contract_harnesses: KaniListHarnesses,
137 pub contracts: IndexSet<ContractedFunction>,
138 pub totals: Totals,
139}
140
141impl KaniListJson {
142 pub fn normalize_file_path(&mut self) {
144 self.standard_harnesses.normalize_file_path();
145 self.contract_harnesses.normalize_file_path();
146 }
147
148 pub fn strip_path_prefix<P: AsRef<Path>>(&mut self, path: P) {
150 let path = path.as_ref();
151 let path = path
152 .canonicalize()
153 .unwrap_or_else(|err| panic!("Unable to canonicalize {path:?}:\n{err}"));
154 let prefix = &format!("{}{MAIN_SEPARATOR}", path.to_str().unwrap());
155
156 self.standard_harnesses.strip_path_prefix(prefix);
157 self.contract_harnesses.strip_path_prefix(prefix);
158 }
159
160 pub fn strip_path_prefix_raw(&mut self, prefix: &str) {
162 self.standard_harnesses.strip_path_prefix(prefix);
163 self.contract_harnesses.strip_path_prefix(prefix);
164 }
165
166 pub fn strip_path_closure_name(&mut self, text: &[&str]) {
167 self.standard_harnesses.strip_path_closure_name(text);
168 self.contract_harnesses.strip_path_closure_name(text);
169 }
170
171 pub fn files(&self) -> serde_json::Value {
172 serde_json::json!({
173 "standard_harnesses": self.standard_harnesses.files(),
174 "contract_harnesses": self.contract_harnesses.files()
175 })
176 }
177
178 pub fn harness_names(&self, mut filter: impl FnMut(&str, &str) -> bool) -> IndexSet<&str> {
179 let totals = &self.totals;
180 let len = totals.standard_harnesses + totals.contract_harnesses;
181 let mut v = Vec::with_capacity(len);
182
183 self.standard_harnesses.names(&mut v, &mut filter);
184 self.contract_harnesses.names(&mut v, &mut filter);
185
186 let duplicates = count_gt1(&v);
187 assert!(duplicates.is_empty(), "Function name duplicates: {duplicates:#?}");
188 vec_to_set(&v)
189 }
190}
191
192fn count_gt1<T: Copy + Hash + Eq>(v: &[T]) -> Vec<(T, u32)> {
193 let mut map = IndexMap::with_capacity(v.len());
194 for key in v {
195 map.entry(*key).and_modify(|n| *n += 1).or_insert(1u32);
196 }
197 map.into_iter().filter(|(_, n)| *n != 1).collect()
198}
199
200fn vec_to_set<T: Copy + Hash + Eq + Ord>(v: &[T]) -> IndexSet<T> {
201 let mut set: IndexSet<_> = v.iter().copied().collect();
202 set.sort_unstable();
203 set
204}
205
206pub struct MergedHarnesses<'a> {
209 pub functions: &'a [SerFunction],
210 pub standard: Box<[&'a SerFunction]>,
211 pub contract: Box<[&'a SerFunction]>,
212}
213
214impl MergedHarnesses<'_> {
215 pub fn new(functions: &[SerFunction]) -> MergedHarnesses<'_> {
216 let cap = functions.len();
217 let mut standard = Vec::with_capacity(cap);
218 let mut contract = Vec::with_capacity(cap);
219 for func in functions {
220 match func.proof_kind {
221 Some(ProofKind::Standard) => standard.push(func),
222 Some(ProofKind::Contract) => contract.push(func),
223 None => (),
224 }
225 }
226 MergedHarnesses {
227 functions,
228 standard: standard.into_boxed_slice(),
229 contract: contract.into_boxed_slice(),
230 }
231 }
232
233 pub fn function_names(&self, mut filter: impl FnMut(&SerFunction) -> bool) -> IndexSet<&str> {
234 let v: Vec<_> = self.functions.iter().filter(|f| filter(f)).map(|f| &*f.name).collect();
235 vec_to_set(&v)
237 }
238}