Merge pull request #49 from os-checker/kani-list

zjp-CN · web-flow · commit 949f4a54d0f6 · 2025-04-21T20:44:41.000+08:00
Feat: define KaniList for parsing the output of `kani list`
diff --git a/.gitignore b/.gitignore
@@ -1,4 +1,7 @@
 /target
 
+# kani list
+kani-list.json
+
 # ignore kani folder for grep or files findings
 # kani
diff --git a/Cargo.lock b/Cargo.lock
diff --git a/Cargo.toml b/Cargo.toml
@@ -7,7 +7,7 @@ edition = "2024"
 clap = { version = "4.5.35", features = ["derive"] }
 serde = { version = "1", features = ["derive"] }
 serde_json = { version = "1", features = ["preserve_order"] }
-indexmap = "2.9.0"
+indexmap = { version = "2.9.0", features = ["serde"] }
 
 # error handling
 eyre = "0.6"
diff --git a/src/lib.rs b/src/lib.rs
@@ -1,3 +1,4 @@
+use indexmap::{IndexMap, IndexSet};
 use serde::{Deserialize, Serialize};
 
 /// A Rust funtion with its file source, attributes, and raw function content.
@@ -83,3 +84,30 @@ pub fn kani_path() -> String {
     assert!(std::fs::exists(&path).unwrap());
     path
 }
+
+/// Output of `kani list` command.
+#[derive(Debug, Serialize, Deserialize, Clone)]
+#[serde(rename_all = "kebab-case")]
+pub struct KaniList {
+    pub kani_version: String,
+    pub file_version: String,
+    pub standard_harnesses: IndexMap<String, IndexSet<String>>,
+    pub contract_harnesses: IndexMap<String, IndexSet<String>>,
+    pub contracts: IndexSet<ContractedFunction>,
+    pub totals: Total,
+}
+
+#[derive(Debug, Serialize, Deserialize, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
+pub struct ContractedFunction {
+    pub function: String,
+    pub file: String,
+    pub harnesses: Vec<String>,
+}
+
+#[derive(Debug, Serialize, Deserialize, Clone)]
+#[serde(rename_all = "kebab-case")]
+pub struct Total {
+    pub standard_harnesses: usize,
+    pub contract_harnesses: usize,
+    pub functions_under_contract: usize,
+}
diff --git a/tests/kani_list.rs b/tests/kani_list.rs
@@ -0,0 +1,35 @@
+use distributed_verification::KaniList;
+use std::process::Command;
+
+mod utils;
+use utils::*;
+
+#[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);
+        expect_file![list_path].assert_debug_eq(&kani_list);
+    }
+
+    Ok(())
+}
+
+fn get_kani_list(file: &str) -> KaniList {
+    // kani list -Zlist -Zfunction-contracts --format=json file.rs
+    let args = ["list", "-Zlist", "-Zfunction-contracts", "--format=json", file];
+    let output = Command::new("kani").args(args).output().unwrap();
+    assert!(
+        output.status.success(),
+        "Failed to run `kani list -Zlist -Zfunction-contracts --format=json {file}`:\n{}",
+        std::str::from_utf8(&output.stderr).unwrap()
+    );
+
+    // read kani-list.json
+    let file_json = std::fs::File::open("kani-list.json").unwrap();
+    serde_json::from_reader(file_json).unwrap()
+}
diff --git a/tests/kani_list/ad_hoc.txt b/tests/kani_list/ad_hoc.txt
@@ -0,0 +1,18 @@
+KaniList {
+    kani_version: "0.60.0",
+    file_version: "0.1",
+    standard_harnesses: {
+        "tests/proofs/ad_hoc.rs": {
+            "adhoc::callee_defined_in_proof",
+            "adhoc::closure_in_proof",
+            "adhoc::proof_in_fn_item::proof",
+        },
+    },
+    contract_harnesses: {},
+    contracts: {},
+    totals: Total {
+        standard_harnesses: 3,
+        contract_harnesses: 0,
+        functions_under_contract: 0,
+    },
+}
diff --git a/tests/kani_list/gen_contracts_by_macros.txt b/tests/kani_list/gen_contracts_by_macros.txt
@@ -0,0 +1,40 @@
+KaniList {
+    kani_version: "0.60.0",
+    file_version: "0.1",
+    standard_harnesses: {},
+    contract_harnesses: {
+        "tests/proofs/gen_contracts_by_macros.rs": {
+            "verify::proof1",
+            "verify::proof2",
+            "verify::proof3",
+        },
+    },
+    contracts: {
+        ContractedFunction {
+            function: "verify::contract1",
+            file: "tests/proofs/gen_contracts_by_macros.rs",
+            harnesses: [
+                "verify::proof1",
+            ],
+        },
+        ContractedFunction {
+            function: "verify::contract2",
+            file: "tests/proofs/gen_contracts_by_macros.rs",
+            harnesses: [
+                "verify::proof2",
+            ],
+        },
+        ContractedFunction {
+            function: "verify::contract3",
+            file: "tests/proofs/gen_contracts_by_macros.rs",
+            harnesses: [
+                "verify::proof3",
+            ],
+        },
+    },
+    totals: Total {
+        standard_harnesses: 0,
+        contract_harnesses: 3,
+        functions_under_contract: 3,
+    },
+}
diff --git a/tests/kani_list/gen_proofs_by_macros.txt b/tests/kani_list/gen_proofs_by_macros.txt
@@ -0,0 +1,18 @@
+KaniList {
+    kani_version: "0.60.0",
+    file_version: "0.1",
+    standard_harnesses: {
+        "tests/proofs/gen_proofs_by_macros.rs": {
+            "verify::proof1",
+            "verify::proof2",
+            "verify::proof3",
+        },
+    },
+    contract_harnesses: {},
+    contracts: {},
+    totals: Total {
+        standard_harnesses: 3,
+        contract_harnesses: 0,
+        functions_under_contract: 0,
+    },
+}
diff --git a/tests/kani_list/gen_proofs_by_nested_macros.txt b/tests/kani_list/gen_proofs_by_nested_macros.txt
@@ -0,0 +1,18 @@
+KaniList {
+    kani_version: "0.60.0",
+    file_version: "0.1",
+    standard_harnesses: {
+        "tests/proofs/gen_proofs_by_nested_macros.rs": {
+            "verify::proof1",
+            "verify::proof2",
+            "verify::proof3",
+        },
+    },
+    contract_harnesses: {},
+    contracts: {},
+    totals: Total {
+        standard_harnesses: 3,
+        contract_harnesses: 0,
+        functions_under_contract: 0,
+    },
+}
diff --git a/tests/kani_list/proofs_for_contract.txt b/tests/kani_list/proofs_for_contract.txt
@@ -0,0 +1,42 @@
+KaniList {
+    kani_version: "0.60.0",
+    file_version: "0.1",
+    standard_harnesses: {},
+    contract_harnesses: {
+        "tests/proofs/proofs_for_contract.rs": {
+            "verify::single_contract",
+            "verify::single_contract_requires",
+            "verify::single_with_contract_ensures",
+            "verify::two_contracts_requires_and_ensures",
+        },
+    },
+    contracts: {
+        ContractedFunction {
+            function: "verify::contract",
+            file: "tests/proofs/proofs_for_contract.rs",
+            harnesses: [
+                "verify::single_contract",
+            ],
+        },
+        ContractedFunction {
+            function: "verify::contract_ensures",
+            file: "tests/proofs/proofs_for_contract.rs",
+            harnesses: [
+                "verify::single_with_contract_ensures",
+            ],
+        },
+        ContractedFunction {
+            function: "verify::contract_requires",
+            file: "tests/proofs/proofs_for_contract.rs",
+            harnesses: [
+                "verify::single_contract_requires",
+                "verify::two_contracts_requires_and_ensures",
+            ],
+        },
+    },
+    totals: Total {
+        standard_harnesses: 0,
+        contract_harnesses: 4,
+        functions_under_contract: 3,
+    },
+}
diff --git a/tests/kani_list/standard_proofs.txt b/tests/kani_list/standard_proofs.txt
@@ -0,0 +1,18 @@
+KaniList {
+    kani_version: "0.60.0",
+    file_version: "0.1",
+    standard_harnesses: {
+        "tests/proofs/standard_proofs.rs": {
+            "verify::recursive_callees",
+            "verify::standard_proof",
+            "verify::standard_proof_empty",
+        },
+    },
+    contract_harnesses: {},
+    contracts: {},
+    totals: Total {
+        standard_harnesses: 3,
+        contract_harnesses: 0,
+        functions_under_contract: 0,
+    },
+}
diff --git a/tests/kani_list/standard_proofs_with_contracts.txt b/tests/kani_list/standard_proofs_with_contracts.txt
@@ -0,0 +1,35 @@
+KaniList {
+    kani_version: "0.60.0",
+    file_version: "0.1",
+    standard_harnesses: {
+        "tests/proofs/standard_proofs_with_contracts.rs": {
+            "verify::single_contract",
+            "verify::single_contract_requires",
+            "verify::single_with_contract_ensures",
+            "verify::two_contracts_requires_and_ensures",
+        },
+    },
+    contract_harnesses: {},
+    contracts: {
+        ContractedFunction {
+            function: "verify::contract",
+            file: "tests/proofs/standard_proofs_with_contracts.rs",
+            harnesses: [],
+        },
+        ContractedFunction {
+            function: "verify::contract_ensures",
+            file: "tests/proofs/standard_proofs_with_contracts.rs",
+            harnesses: [],
+        },
+        ContractedFunction {
+            function: "verify::contract_requires",
+            file: "tests/proofs/standard_proofs_with_contracts.rs",
+            harnesses: [],
+        },
+    },
+    totals: Total {
+        standard_harnesses: 4,
+        contract_harnesses: 0,
+        functions_under_contract: 3,
+    },
+}
diff --git a/tests/proofs.rs b/tests/proofs.rs
@@ -4,21 +4,6 @@ use std::path::{Path, PathBuf};
 mod utils;
 use utils::{assert_eq, *};
 
-fn get_proofs(dir: &str) -> Result<Vec<PathBuf>> {
-    let mut proofs = vec![];
-    for entry in std::fs::read_dir(dir)? {
-        let entry = entry?;
-        let path = entry.path();
-        if path.is_file()
-            && path.extension().and_then(|ext| Some(ext.to_str()? == "rs")).unwrap_or(false)
-        {
-            proofs.push(path);
-        }
-    }
-    proofs.sort();
-    Ok(proofs)
-}
-
 fn assert_unique_hash(proofs: &[PathBuf], v_json: &[Vec<SerFunction>]) {
     let mut map = IndexMap::<&str, Vec<(&Path, &str)>>::new();
     for (v, proof) in v_json.iter().zip(proofs) {
@@ -84,7 +69,7 @@ fn test_proofs() -> Result<()> {
     let mut v_json = Vec::<Vec<SerFunction>>::with_capacity(proofs.len());
     let mut v_macro = vec![];
     for (idx, path) in proofs.iter().enumerate() {
-        let file_stem = path.file_stem().and_then(|f| f.to_str()).unwrap();
+        let file_stem = file_stem(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());
diff --git a/tests/utils.rs b/tests/utils.rs
@@ -1,11 +1,10 @@
+#![allow(dead_code, unused_imports)]
 use assert_cmd::Command;
+use std::path::{Path, PathBuf};
 
 pub use distributed_verification::SerFunction;
-#[allow(unused_imports)] // seems a bug in clippy: RA only recognizes the usage in compare.rs
 pub use expect_test::{expect, expect_file};
-#[allow(unused_imports)] // seems a bug in clippy
 pub use eyre::Result;
-#[allow(unused_imports)] // seems a bug in clippy
 pub use pretty_assertions::assert_eq;
 
 pub fn cmd(args: &[&str]) -> String {
@@ -20,3 +19,23 @@ pub fn cmd(args: &[&str]) -> String {
 
     String::from_utf8(output.stdout).unwrap()
 }
+
+/// Get rs files under a dir.
+pub fn get_proofs(dir: &str) -> Result<Vec<PathBuf>> {
+    let mut proofs = vec![];
+    for entry in std::fs::read_dir(dir)? {
+        let entry = entry?;
+        let path = entry.path();
+        if path.is_file()
+            && path.extension().and_then(|ext| Some(ext.to_str()? == "rs")).unwrap_or(false)
+        {
+            proofs.push(path);
+        }
+    }
+    proofs.sort();
+    Ok(proofs)
+}
+
+pub fn file_stem(path: &Path) -> &str {
+    path.file_stem().and_then(|f| f.to_str()).unwrap()
+}
