Feat: Support kani harnesses from crates beyond libcore

.github/gen_core.json.sh

@@ -5,17 +5,24 @@ set -o pipefail
 export WORKSPACE="${WORKSPACE:-$(pwd)}"
 
 export DV_LOG=off
-export OUTPUT_DIR=$WORKSPACE/assets
 export KANI_DIR=$WORKSPACE/kani/target/kani
 export VERIFY_RUST_STD_LIBRARY=$WORKSPACE/verify-rust-std/library
 
+export OUTPUT_DIR=$WORKSPACE/assets/json
+mkdir "$OUTPUT_DIR" -p
+
 # test/verify-rust-std needs this, so remember to
 # * update runid after verify-rust-std submodule syncs
 # * update snapshots after runid changes
 rm tmp -rf
 gh run download -D tmp -R model-checking/verify-rust-std 17086909032
 
-ls -alh $VERIFY_RUST_STD_LIBRARY
+ls -alh "$VERIFY_RUST_STD_LIBRARY"
+
+# Store data across all crates.
+export DB_FILE=$WORKSPACE/tmp/core.sqlite3
+# Remove old data: we don't need data history.
+rm "$DB_FILE" -f
 
 cargo b --bin distributed-verification
 export DISTRIBUTED_VERIFICATION=$WORKSPACE/target/debug/distributed-verification
@@ -29,6 +36,8 @@ $VERIFY_RUST_STD
 
 popd
 pushd verify-rust-std
-ls -a library/core/db.sqlite3
-mv library/core/db.sqlite3 ../assets/core.sqlite3
 git checkout .
+
+popd
+mv "$DB_FILE" assets/core.sqlite3
+ls -a assets/core.sqlite3

.github/workflows/test.yml

@@ -28,7 +28,7 @@ jobs:
         run: ./.github/gen_core.json.sh
 
       - name: View core.json
-        working-directory: assets
+        working-directory: assets/json
         run: |
           ls -alh core.json
           head -n 100 core.json
@@ -38,7 +38,7 @@ jobs:
         with:
           name: artifact-libcore
           path: |
-            assets/core.json
+            assets/json
             assets/core.sqlite3
           compression-level: 9
           if-no-files-found: error

.gitignore

@@ -7,7 +7,7 @@ kani-list.json
 # kani
 
 rustflags.json
-core.json
+assets/json
 /artifact*
 
 *.sqlite3

assets/db.sql

@@ -12,9 +12,11 @@
 --   macro_backtrace_len INTEGER,
 --   macro_backtrace TEXT,
 --   callees_len INTEGER,
---   callees TEXT
+--   callees TEXT,
+--   crate TEXT
 -- ) STRICT;
 SELECT
+  crate,
   file,
   name,
   hash,
@@ -28,6 +30,19 @@ WHERE
 LIMIT
   10;
 
+SELECT
+  crate,
+  count() AS `Functions`,
+  COUNT(
+    CASE
+      WHEN proof_kind IS NOT NULL THEN 1
+    END
+  ) AS `Proofs`
+FROM
+  db
+GROUP BY
+  crate;
+
 SELECT
   count() AS `Total Proofs`
 FROM

src/bin/distributed-verification/cli/mod.rs

@@ -5,10 +5,7 @@ use distributed_verification::{
     kani_path,
 };
 use eyre::Context;
-use std::fmt;
-
-/// Compare simplify-json and kani-list.json
-pub mod diff;
+use std::{fmt, path::PathBuf};
 
 /// Parse cli arguments.
 pub fn parse() -> Result<Run> {
@@ -21,7 +18,7 @@ pub fn parse() -> Result<Run> {
 struct Args {
     /// Possible one of these values:
     /// * `--json false`: skip serializing to json
-    /// * `--json path/to/file.json`: serlialize into a file
+    /// * `--json folder`: serlialize into a file under this folder with name being `{crate_name}.json`
     /// * `--json` or `--json stdout`: print to stdout
     ///
     /// NOTE: the default value is stdout, so if no other output is specified,
@@ -121,18 +118,20 @@ pub enum Output {
     False,
     /// Write to stdout.
     Stdout,
-    /// Write to a local file.
-    Path(String),
+    /// Write to a local file under this folder.
+    Dir(PathBuf),
 }
 
 impl Output {
-    pub fn emit<T: serde::Serialize>(self, val: &T) -> Result<()> {
+    pub fn emit<T: serde::Serialize>(self, val: &T, crate_name: &str) -> Result<()> {
         let _span = error_span!("emit", ?self).entered();
 
         let writer: Box<dyn std::io::Write> = match self {
             Output::False => return Ok(()),
             Output::Stdout => Box::new(std::io::stdout()),
-            Output::Path(path) => {
+            Output::Dir(mut path) => {
+                path.push(crate_name);
+                path.set_extension("json");
                 let file = std::fs::File::create(path)?;
                 Box::new(file)
             }
@@ -152,7 +151,11 @@ impl From<String> for Output {
         match &*s.to_ascii_lowercase() {
             "false" => Self::False,
             "" | "stdout" => Self::Stdout,
-            _ => Self::Path(s),
+            _ => {
+                let dir = PathBuf::from(s);
+                assert!(dir.exists(), "The folder doesn't exist: {}", dir.display());
+                Self::Dir(dir)
+            }
         }
     }
 }
@@ -162,7 +165,7 @@ impl fmt::Display for Output {
         f.write_str(match self {
             Output::False => "false",
             Output::Stdout => "stdout",
-            Output::Path(path) => path,
+            Output::Dir(path) => path.to_str().unwrap(),
         })
     }
 }

src/bin/distributed-verification/functions/cache/db.rs

@@ -2,7 +2,7 @@ use super::Functions;
 use crate::Result;
 use distributed_verification::db::{
     DbFunction,
-    sql::{SQL_CREATE, SQL_DROP, SQL_INSERT, SQL_VACUUM, db_file},
+    sql::{SQL_CREATE, SQL_INSERT, db_file},
 };
 use eyre::{Context, ContextCompat};
 use rusqlite::{Connection, named_params};
@@ -20,21 +20,19 @@ impl Db {
         let _span = error_span!("Db::new", db_file).entered();
         let db = Connection::open(db_file).context("Failed to open or create db file.")?;
 
-        db.execute(SQL_DROP, []).context("Failed to drop db.")?;
-        db.execute(SQL_VACUUM, []).context("Failed to VACUUM.")?;
         db.execute(SQL_CREATE, []).context("Failed to execute SQL_CREATE.")?;
 
         Ok(Db { db })
     }
 
     /// This function should be called after recursive hashes are computed for all functions.
-    pub fn store(&mut self, map: &Functions) -> Result<()> {
+    pub fn store(&mut self, map: &Functions, crate_name: &str) -> Result<()> {
         info!(db = ?self.db.path(), "data ready to be stored to sqlite db");
         let tx = self.db.transaction()?;
         let mut stmt = tx.prepare(SQL_INSERT)?;
 
         let mut count = 0usize;
-        for func in cache_to_db_func(map) {
+        for func in cache_to_db_func(map, crate_name) {
             let func = match func {
                 Ok(func) => func,
                 Err(err) => {
@@ -56,6 +54,7 @@ impl Db {
                 ":macro_backtrace": to_string_pretty(&func.macro_backtrace).unwrap(),
                 ":callees_len": func.callees_len,
                 ":callees": to_string_pretty(&func.callees).unwrap(),
+                ":crate": &func.krate,
             };
 
             if let Err(err) = stmt.insert(params) {
@@ -84,7 +83,7 @@ impl Db {
     }
 }
 
-fn cache_to_db_func(map: &Functions) -> impl Iterator<Item = Result<DbFunction>> {
+fn cache_to_db_func(map: &Functions, crate_name: &str) -> impl Iterator<Item = Result<DbFunction>> {
     map.iter().map(|(inst, func)| {
         let _span = error_span!("cache_to_db_func", ?inst, ?func).entered();
         // skip func that has no body
@@ -114,11 +113,12 @@ fn cache_to_db_func(map: &Functions) -> impl Iterator<Item = Result<DbFunction>>
             inst_kind: src.inst_kind,
             proof_kind: f.proof_kind,
             attrs: src.attrs.clone(),
-            src: src.src.clone(),
+            src: src.src.as_str().into(),
             macro_backtrace_len: src.macro_backtrace_len,
             macro_backtrace: src.macro_backtrace.clone(),
             callees_len: callees.len(),
             callees,
+            krate: crate_name.into(),
         })
     })
 }

src/bin/distributed-verification/functions/cache/mod.rs

@@ -149,15 +149,15 @@ impl Cache {
             // stable sort through file, fn name, (direct) hash
             set.sort_unstable_by(|a, b| {
                 let fields = |inst: &Instance| {
-                    let func = self.get(inst).inner.as_ref().unwrap();
-                    (&*func.file, &*func.name, &*func.hash)
+                    let func = self.get(inst).inner.as_ref()?;
+                    Some((&*func.file, &*func.name, &*func.hash))
                 };
                 fields(a).cmp(&fields(b))
             });
 
             let mut hasher = StreamHasher::new();
             for inst in &*set {
-                let hash = &*self.get(inst).inner.as_ref().unwrap().hash;
+                let hash = self.get(inst).inner.as_ref().map(|val| &*val.hash);
                 hasher.append(hash);
             }
             let recursive_hash = hasher.finish();
@@ -170,7 +170,8 @@ impl Cache {
     /// Store functions info to db
     fn store_to_db(&self) {
         let mut db = db::Db::new().unwrap();
-        db.store(&self.functions).unwrap();
+        let crate_name = &rustc_public::local_crate().name;
+        db.store(&self.functions, crate_name).unwrap();
     }
 }
 
@@ -232,9 +233,9 @@ impl Function {
                     ord => ord,
                 }
             }
-            (None, None) | (None, Some(_)) | (Some(_), None) => {
-                unreachable!("{self:?} and {other:?} must be a valid function")
-            }
+            (None, None) => Ordering::Equal,
+            (None, Some(_)) => Ordering::Less,
+            (Some(_), None) => Ordering::Greater,
         }
     }
 }

src/bin/distributed-verification/functions/mod.rs

@@ -15,10 +15,12 @@ pub use kani::TOOL;
 
 mod utils;
 
-pub fn analyze(tcx: TyCtxt) -> Vec<SerFunction> {
+pub fn analyze(tcx: TyCtxt) -> (String, Vec<SerFunction>) {
+    let crate_name = rustc_public::local_crate().name;
+    // FIXME: retrieve functions using local_crate
     let local_items = all_local_items();
     let cap = local_items.len();
-    dbg!(cap);
+    dbg!(&crate_name, cap);
 
     let mut entries = Vec::with_capacity(cap);
 
@@ -46,7 +48,7 @@ pub fn analyze(tcx: TyCtxt) -> Vec<SerFunction> {
 
     cache::store_to_db();
 
-    v_func.into_iter().map(|f| f.0).collect()
+    (crate_name, v_func.into_iter().map(|f| f.0).collect())
 }
 
 /// A Rust funtion with its file source, attributes, and raw function content.

src/bin/distributed-verification/main.rs

@@ -17,6 +17,7 @@ use distributed_verification::kani_list::check_proofs;
 use eyre::Result;
 use functions::{clear_rustc_ctx, set_rustc_ctx};
 use rustc_middle::ty::TyCtxt;
+use rustc_public::CompilerError;
 
 mod cli;
 mod functions;
@@ -63,14 +64,18 @@ fn main() -> Result<()> {
     });
 
     match res {
-        Ok(res_inner) | Err(rustc_public::CompilerError::Interrupted(res_inner)) => res_inner,
-        Err(err) => Err(eyre!("Unexpected error {err:?}")),
+        Ok(err) | Err(CompilerError::Interrupted(err)) => err,
+        Err(CompilerError::Failed) => bail!("Compilation failed!"),
+        Err(CompilerError::Skipped) => {
+            eprintln!("Compilation skipped.");
+            Ok(())
+        }
     }
 }
 
 fn analyze_proofs(tcx: TyCtxt, run: cli::Run) -> Result<()> {
     set_rustc_ctx(tcx);
-    let output = functions::analyze(tcx);
+    let (crate_name, output) = functions::analyze(tcx);
     clear_rustc_ctx();
 
     let mut res_check_kani_list = Ok(());
@@ -79,7 +84,7 @@ fn analyze_proofs(tcx: TyCtxt, run: cli::Run) -> Result<()> {
         res_check_kani_list = check_proofs(&kani_list, &proofs);
     }
 
-    let res_json = run.json.emit(&output);
+    let res_json = run.json.emit(&output, &crate_name);
 
     match (res_check_kani_list, res_json) {
         (Ok(_), Ok(_)) => Ok(()),

src/bin/distributed-verification/stat/mod.rs

@@ -22,6 +22,7 @@ fn new_local_crate(tcx: TyCtxt) -> LocalCrateFnDefs {
 
     // for krate in stable_mir::find_crates("core") {
     let krate = local_crate();
+    this.crate_name = krate.name.clone();
     let fn_defs = krate.fn_defs();
     this.fn_defs.total = fn_defs.len();
 
@@ -76,7 +77,7 @@ fn new_local_crate(tcx: TyCtxt) -> LocalCrateFnDefs {
 
 pub fn analyze(out: Output, tcx: TyCtxt) -> crate::Result<()> {
     let stat = new_stat(tcx);
-    out.emit(&stat)
+    out.emit(&stat, &stat.local.crate_name)
 }
 
 // From verify-rust-std CI:

src/bin/verify_rust_std/env.rs

@@ -33,14 +33,10 @@ impl EnvVar {
         info!("{path:?} is written.");
         Ok(())
     }
-
-    pub fn core_json(&self) -> PathBuf {
-        self.OUTPUT_DIR.join("core.json")
-    }
 }
 
 fn var_to_path(env: &str) -> PathBuf {
-    let s = var(env).unwrap();
+    let s = var(env).unwrap_or_else(|err| panic!("Failed to read env var {env:?}:\n{err:?}"));
     let path = Path::new(&s);
     assert!(path.exists(), "{env}={s:?} doesn't point to a valid path.");
     path.canonicalize().unwrap()