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

Feat: add Kind field to SerFunction; check json with output of kani list

Author: zjp-CN

src/functions/mod.rs

@@ -11,7 +11,9 @@ mod cache;
 pub use cache::{clear_rustc_ctx, set_rustc_ctx};
 
 mod kani;
+
 mod utils;
+pub use utils::vec_convertion;
 
 mod serialization;
 pub use serialization::SerFunction;

src/functions/serialization.rs

@@ -4,7 +4,7 @@ use serde::Serialize;
 use stable_mir::{CrateDef, mir::mono::Instance};
 use std::{cmp::Ordering, hash::Hasher};
 
-/// A Rust funtion with its file source, attributes, and raw function content.
+/// A kani proof with its file source, attributes, and raw function content.
 #[derive(Debug, Serialize)]
 pub struct SerFunction {
     hash: String,
@@ -13,6 +13,8 @@ pub struct SerFunction {
     /// Attributes are attached the function, but it seems that attributes
     /// and function must be separated to query.
     attrs: Vec<String>,
+    /// Proof kind
+    kind: Kind,
     /// Raw function string, including name, signature, and body.
     func: SourceCode,
     /// Count of callees.
@@ -26,6 +28,7 @@ impl SerFunction {
         let inst = fun.instance;
         let def_id = format_def_id(&inst);
         let attrs: Vec<_> = fun.attrs.iter().map(|a| a.as_str().to_owned()).collect();
+        let kind = Kind::new(&attrs);
         // Though this is from body span, fn name and signature are included.
         let func = cache::get_source_code(&inst).unwrap_or_default();
         let callees: Vec<_> = fun.callees.iter().map(Callee::new).collect();
@@ -40,7 +43,7 @@ impl SerFunction {
         callees.iter().for_each(|callee| callee.func.with_hasher(&mut hasher));
         let Hash128(hash) = hasher.finish();
 
-        SerFunction { hash, def_id, attrs, func, callees_len, callees }
+        SerFunction { hash, def_id, attrs, kind, func, callees_len, callees }
     }
 
     /// Compare by file and func string.
@@ -78,3 +81,83 @@ impl Callee {
         Callee { def_id, func }
     }
 }
+
+/// kani proof kind
+#[derive(Debug, Serialize)]
+pub enum Kind {
+    /// `#[kani::proof]` (actually `kanitool::proof`)
+    Standard,
+    /// `#[kani::proof_for_contract]` (actually `kanitool::proof_for_contract`)
+    Contract,
+}
+
+impl Kind {
+    /// ## Panic
+    ///
+    /// The given attributes must contain one of the proof kind macro.
+    fn new(attrs: &[String]) -> Self {
+        for attr in attrs {
+            if attr.contains("kanitool::proof_for_contract") {
+                return Kind::Contract;
+            } else if attr.contains("kanitool::proof") {
+                return Kind::Standard;
+            }
+        }
+        panic!("{attrs:?} doesn't contain a proof kind.")
+    }
+}
+
+/// Convertion from lib's SerFunction into the counterpart in main.rs
+mod conversion {
+    use super::*;
+    use crate::functions::utils::{MacroBacktrace, vec_convertion};
+    use distributed_verification as lib;
+
+    impl From<SerFunction> for lib::SerFunction {
+        fn from(value: SerFunction) -> Self {
+            let SerFunction { hash, def_id, attrs, kind, func, callees_len, callees } = value;
+            let func = func.into();
+            let kind = kind.into();
+            let callees = vec_convertion(callees);
+            Self { hash, def_id, attrs, kind, func, callees_len, callees }
+        }
+    }
+
+    impl From<Kind> for lib::Kind {
+        fn from(value: Kind) -> Self {
+            match value {
+                Kind::Standard => Self::Standard,
+                Kind::Contract => Self::Contract,
+            }
+        }
+    }
+
+    impl From<Callee> for lib::Callee {
+        fn from(Callee { def_id, func }: Callee) -> Self {
+            let func = func.into();
+            Self { def_id, func }
+        }
+    }
+
+    impl From<SourceCode> for lib::SourceCode {
+        fn from(value: SourceCode) -> Self {
+            let SourceCode {
+                name,
+                mangled_name,
+                kind,
+                file,
+                src,
+                macro_backtrace_len,
+                macro_backtrace,
+            } = value;
+            let macro_backtrace = vec_convertion(macro_backtrace);
+            Self { name, mangled_name, kind, file, src, macro_backtrace_len, macro_backtrace }
+        }
+    }
+
+    impl From<MacroBacktrace> for lib::MacroBacktrace {
+        fn from(MacroBacktrace { callsite, defsite }: MacroBacktrace) -> Self {
+            Self { callsite, defsite }
+        }
+    }
+}

src/functions/utils.rs

@@ -61,8 +61,8 @@ impl SourceCode {
 
 #[derive(Clone, Debug, Serialize, PartialEq, Eq, PartialOrd, Ord, Default)]
 pub struct MacroBacktrace {
-    callsite: String,
-    defsite: String,
+    pub callsite: String,
+    pub defsite: String,
 }
 
 fn span_to_source(span: Span, src_map: &SourceMap) -> String {
@@ -123,3 +123,7 @@ pub fn source_code_with(
     let kind = format!("{:?}", inst.kind);
     SourceCode { name, mangled_name, kind, file, src, macro_backtrace_len, macro_backtrace }
 }
+
+pub fn vec_convertion<U, T: From<U>>(vec: Vec<U>) -> Vec<T> {
+    vec.into_iter().map(T::from).collect()
+}

src/kani_list.rs

@@ -0,0 +1,100 @@
+use indexmap::{IndexMap, IndexSet};
+use serde::{Deserialize, Serialize};
+use std::{collections::HashMap, process::Command};
+
+use crate::{Kind, SerFunction};
+
+/// 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,
+}
+
+/// Get kani list and check if it complies with Vec<SerFunction>.
+pub fn check(file: &str, v_ser_fun: &[SerFunction]) {
+    let list = get_kani_list(file);
+    check_proofs(&list, v_ser_fun);
+}
+
+pub 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()
+}
+
+pub fn check_proofs(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, f.kind)))
+        .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 val = map.get(&key).unwrap();
+            dbg!(val);
+        }
+    }
+
+    // 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);
+        }
+    }
+
+    // double check
+    for (&(path, proof), &(_, kind)) in &map {
+        let harnesses = match kind {
+            Kind::Standard => &list.standard_harnesses[path],
+            Kind::Contract => &list.contract_harnesses[path],
+        };
+        _ = harnesses.get(proof).unwrap();
+    }
+}

src/lib.rs

@@ -1,7 +1,8 @@
-use indexmap::{IndexMap, IndexSet};
 use serde::{Deserialize, Serialize};
 
-/// A Rust funtion with its file source, attributes, and raw function content.
+pub mod kani_list;
+
+/// A kani proof with its file source, attributes, and raw function content.
 #[derive(Debug, Default, Serialize, Deserialize, Clone)]
 pub struct SerFunction {
     pub hash: String,
@@ -10,6 +11,8 @@ pub struct SerFunction {
     /// Attributes are attached the function, but it seems that attributes
     /// and function must be separated to query.
     pub attrs: Vec<String>,
+    /// Proof kind
+    pub kind: Kind,
     /// Raw function string, including name, signature, and body.
     pub func: SourceCode,
     /// Count of callees.
@@ -18,6 +21,16 @@ pub struct SerFunction {
     pub callees: Vec<Callee>,
 }
 
+/// kani proof kind
+#[derive(Debug, Default, Serialize, Deserialize, Clone, Copy)]
+pub enum Kind {
+    /// `#[kani::proof]` (actually `kanitool::proof`)
+    #[default]
+    Standard,
+    /// `#[kani::proof_for_contract]` (actually `kanitool::proof_for_contract`)
+    Contract,
+}
+
 #[derive(Debug, Default, Serialize, Deserialize, Clone)]
 pub struct Callee {
     pub def_id: String,
@@ -61,8 +74,8 @@ pub struct SourceCode {
 
 #[derive(Debug, Default, Serialize, Deserialize, Clone)]
 pub struct MacroBacktrace {
-    callsite: String,
-    defsite: String,
+    pub callsite: String,
+    pub defsite: String,
 }
 
 /// A local path to kani's artifacts.
@@ -84,30 +97,3 @@ 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,
-}

src/main.rs

@@ -14,6 +14,7 @@ extern crate stable_mir;
 
 use distributed_verification::kani_path;
 use functions::{clear_rustc_ctx, set_rustc_ctx};
+use rustc_middle::ty::TyCtxt;
 // FIXME: this is a bug for rustc_smir, because rustc_interface is used by
 // run_with_tcx! without being imported inside.
 use rustc_smir::rustc_internal;
@@ -78,10 +79,18 @@ fn main() {
         };
 
         res().unwrap();
+        check_kani_list(output, tcx);
 
         // Stop emitting artifact for the source code being compiled.
         ControlFlow::<(), ()>::Break(())
     });
     // rustc_smir uses `Err(CompilerError::Interrupted)` to represent ControlFlow::Break.
     assert!(res == Err(stable_mir::CompilerError::Interrupted(())), "Unexpected {res:?}");
 }
+
+fn check_kani_list(output: Vec<functions::SerFunction>, tcx: TyCtxt) {
+    let output: Vec<distributed_verification::SerFunction> = functions::vec_convertion(output);
+    let crate_file = tcx.sess.local_crate_source_file().expect("No real crate root file.");
+    let crate_file = crate_file.local_path().unwrap().to_str().unwrap();
+    distributed_verification::kani_list::check(crate_file, &output);
+}

tests/kani_list.rs

@@ -1,5 +1,4 @@
-use distributed_verification::KaniList;
-use std::process::Command;
+use distributed_verification::kani_list::{check_proofs, get_kani_list};
 
 mod utils;
 use utils::*;
@@ -9,27 +8,20 @@ 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();
+        check_proofs(&kani_list, &v_ser_function);
     }
 
     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()
-}