distributed_verification/
diff.rs

1use 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// ************ `kani list --json` ************
10
11#[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                    // Some files refer to registry folder:
62                    // `/home/runner/.cargo/registry/src/innerdex.crates.io-1949cf8
63                    // c6b5b557f/addr2line-0.25.0/src/line.rs`
64                    // So we should keep it as it is.
65                    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    /// filter is a closure where the first argument is filename, and the second is function name.
93    /// If filter returns true, the function name will be appended to v.
94    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    /// The fully qualified name the user gave to the function (i.e. includes the module path).
112    pub function: BoxStr,
113    /// The (currently full-) path to the file this function was declared within.
114    pub file: BoxStr,
115    /// The pretty names of the proof harnesses (`#[kani::proof_for_contract]`) for this function
116    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/// The datastructure generated from `kani list --json`.
128///
129/// ref: https://github.com/model-checking/kani/blob/b64e59de669cd77b625cc8c0b9a94f29117a0ff7/kani-driver/src/list/output.rs#L113
130#[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    /// Call this immediately after deserialization is done, especially before strip_path_prefix.
143    pub fn normalize_file_path(&mut self) {
144        self.standard_harnesses.normalize_file_path();
145        self.contract_harnesses.normalize_file_path();
146    }
147
148    // FIXME: merge this and the raw one.
149    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    /// This function is used in tests.
161    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
206// ************ difference ************
207
208pub 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        // FIXME: it's possible the function name will duplicate, need to figure out why.
236        vec_to_set(&v)
237    }
238}