test: mertge kani list and distributed verification list for proofs

Author: zjp-CN

tests/kani_list.rs

@@ -1,19 +1,27 @@
 use distributed_verification::KaniList;
-use std::process::Command;
+use std::{collections::HashMap, process::Command};
 
 mod utils;
-use utils::*;
+use utils::{assert_eq, *};
 
 #[test]
 fn validate_kani_list_json() -> Result<()> {
     let proofs = get_proofs("tests/proofs")?;
 
     for path in &proofs {
-        let kani_list = get_kani_list(path.to_str().unwrap());
         let file_stem = file_stem(path);
         let list_path = format!("kani_list/{file_stem}.txt");
         dbg!(&list_path);
+
+        let path = path.to_str().unwrap();
+        // run `kani list`
+        let kani_list = get_kani_list(path);
         expect_file![list_path].assert_debug_eq(&kani_list);
+
+        // run `distributed_verification`
+        let text = cmd(&[path]);
+        let v_ser_function: Vec<SerFunction> = serde_json::from_str(&text).unwrap();
+        merge(&kani_list, &v_ser_function);
     }
 
     Ok(())
@@ -33,3 +41,53 @@ fn get_kani_list(file: &str) -> KaniList {
     let file_json = std::fs::File::open("kani-list.json").unwrap();
     serde_json::from_reader(file_json).unwrap()
 }
+
+fn merge(list: &KaniList, v_ser_fun: &[SerFunction]) {
+    // sanity check
+    let totals = &list.totals;
+    assert_eq!(v_ser_fun.len(), totals.standard_harnesses + totals.contract_harnesses);
+    assert_eq!(
+        list.standard_harnesses.values().map(|s| s.len()).sum::<usize>(),
+        totals.standard_harnesses
+    );
+    assert_eq!(
+        list.contract_harnesses.values().map(|s| s.len()).sum::<usize>(),
+        totals.contract_harnesses
+    );
+
+    let map: HashMap<_, _> = v_ser_fun
+        .iter()
+        .enumerate()
+        .map(|(idx, f)| ((&*f.func.file, &*f.func.name), idx))
+        .collect();
+
+    // check all standard proofs are in distributed-verification json
+    for (path, proofs) in &list.standard_harnesses {
+        for proof in proofs {
+            let key = (path.as_str(), proof.as_str());
+            let idx = map.get(&key).unwrap();
+            dbg!(idx);
+        }
+    }
+
+    // check all contract proofs are in distributed-verification json
+    for (path, proofs) in &list.contract_harnesses {
+        for proof in proofs {
+            let key = (path.as_str(), proof.as_str());
+            let idx = map.get(&key).unwrap();
+            dbg!(idx);
+        }
+    }
+
+    // douoble check
+    for &(path, proof) in map.keys() {
+        // FIXME: split standard and contract proofs if kind supported
+        match list.standard_harnesses.get(path) {
+            Some(set) => _ = set.get(proof).unwrap(),
+            None => match list.contract_harnesses.get(path) {
+                Some(set) => _ = set.get(proof).unwrap(),
+                None => panic!("{path} {proof} does not exist"),
+            },
+        };
+    }
+}

tests/proofs.rs

@@ -70,6 +70,7 @@ fn test_proofs() -> Result<()> {
     let mut v_macro = vec![];
     for (idx, path) in proofs.iter().enumerate() {
         let file_stem = file_stem(path);
+        // FIXME: no need to construct path
         let text = cmd(&[&format!("tests/proofs/{file_stem}.rs")]);
         expect_file![format!("./snapshots/{file_stem}.json")].assert_eq(&text);
         v_json.push(serde_json::from_str(&text).unwrap());
@@ -110,6 +111,7 @@ fn test_compare_unique_hash() -> Result<()> {
     let mut v_json = Vec::<Vec<SerFunction>>::with_capacity(proofs.len());
     for path in &proofs {
         let file_stem = path.file_stem().and_then(|f| f.to_str()).unwrap();
+        // FIXME: no need to construct path
         let text = cmd(&[&format!("tests/compare/{file_stem}.rs")]);
         // NOTE: don't write text to json file, since compare.rs write it in a different way
         v_json.push(serde_json::from_str(&text).unwrap());