feat: 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

@@ -106,3 +106,58 @@ impl Kind {
         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/lib.rs

@@ -74,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.

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);
+}