Merge pull request #22 from os-checker/test-ci

Feat: incorporate kani submodule and make CI work

Author: zjp-CN

.cargo/config.toml

@@ -0,0 +1,2 @@
+[env]
+KANI_DIR = "./kani/target/kani"

.github/workflows/test.yml

@@ -4,11 +4,26 @@ on:
   push:
     branches: 
 
+env:
+  CARGO_TERM_COLOR: always
+
 jobs:
   test:
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v4
+        with:
+          submodules: 'recursive'
+
+      - name: Install kani
+        working-directory: kani
+        run: |
+          ./scripts/setup/ubuntu/install_deps.sh
+          cargo build-dev
+          echo PATH=$(pwd)/scripts:$PATH >> $GITHUB_ENV
+
+      - name: Check kani folder
+        run: kani --version
 
       - name: Run tests
         run: cargo test -- --nocapture

.gitmodules

@@ -0,0 +1,3 @@
+[submodule "kani"]
+	path = kani
+	url = https://github.com/model-checking/kani.git

kani

@@ -0,0 +1 @@
+kani/rust-toolchain.toml

rust-toolchain.toml

@@ -75,7 +75,7 @@ impl Function {
         let attrs = KANI_TOOL_ATTRS.iter().flat_map(|v| inst_def.tool_attrs(v)).collect();
 
         let span = inst_def.span();
-        let file = span.get_filename();
+        let file = file_path(&inst);
 
         let fn_def = ty_to_fndef(inst.ty())?;
         let body = fn_def.body()?;
@@ -127,8 +127,8 @@ fn source_code_of_body(inst: &Instance, tcx: TyCtxt, src_map: &SourceMap) -> Opt
 }
 
 fn cmp_callees(a: &Instance, b: &Instance, tcx: TyCtxt, src_map: &SourceMap) -> Ordering {
-    let filename_a = a.def.span().get_filename();
-    let filename_b = b.def.span().get_filename();
+    let filename_a = file_path(a);
+    let filename_b = file_path(b);
     match filename_a.cmp(&filename_b) {
         Ordering::Equal => (),
         ord => return ord,
@@ -138,3 +138,24 @@ fn cmp_callees(a: &Instance, b: &Instance, tcx: TyCtxt, src_map: &SourceMap) ->
     let body_b = source_code_of_body(b, tcx, src_map);
     body_a.cmp(&body_b)
 }
+
+fn file_path(inst: &Instance) -> String {
+    use std::sync::LazyLock;
+    static PREFIXES: LazyLock<[String; 2]> = LazyLock::new(|| {
+        let mut pwd = std::env::current_dir().unwrap().into_os_string().into_string().unwrap();
+        pwd.push('/');
+
+        let out = std::process::Command::new("rustc").arg("--print=sysroot").output().unwrap();
+        let sysroot = std::str::from_utf8(&out.stdout).unwrap().trim();
+        let sysroot = format!("{sysroot}/lib/rustlib/src/rust/");
+        [pwd, sysroot]
+    });
+
+    let file = inst.def.span().get_filename();
+    for prefix in &*PREFIXES {
+        if let Some(file) = file.strip_prefix(prefix) {
+            return file.to_owned();
+        }
+    }
+    file
+}

rust-toolchain.toml

@@ -75,7 +75,7 @@ impl Callee {
     fn new(inst: &Instance, tcx: TyCtxt, src_map: &SourceMap) -> Self {
         let inst_def = &inst.def;
         let def_id = format_def_id(&inst_def.def_id());
-        let file = inst_def.span().get_filename();
+        let file = super::file_path(inst);
         let func = super::source_code_of_body(inst, tcx, src_map).unwrap_or_default();
         Callee { def_id, file, func }
     }

src/functions/mod.rs

@@ -24,3 +24,23 @@ pub struct Callee {
     pub file: String,
     pub func: String,
 }
+
+/// A local path to kani's artifacts.
+///
+/// Choose the following if found
+/// * `$KANI_DIR`
+/// * or `$KANI_HOME/kani-{version}`
+/// * or `$HOME/.kani/kani-{version}`
+pub fn kani_path() -> String {
+    use std::env::var;
+    let path = if let Ok(path) = var("KANI_DIR") {
+        path
+    } else {
+        let kani = std::process::Command::new("kani").arg("--version").output().unwrap();
+        let kani_folder = std::str::from_utf8(&kani.stdout).unwrap().trim().replace(' ', "-");
+        let home = var("KANI_HOME").or_else(|_| var("HOME")).unwrap();
+        format!("{home}/.kani/{kani_folder}")
+    };
+    assert!(std::fs::exists(&path).unwrap());
+    path
+}

src/functions/serialization.rs

@@ -10,6 +10,7 @@ extern crate rustc_span;
 extern crate rustc_stable_hash;
 extern crate stable_mir;
 
+use distributed_verification::kani_path;
 // 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;
@@ -24,6 +25,8 @@ extern crate tracing;
 fn main() {
     logger::init();
     let cli = cli::parse();
+    let kani_path = kani_path();
+    info!(kani_path);
     let mut args = Vec::from(
         [
             // the first argument to rustc is unimportant
@@ -33,13 +36,13 @@ fn main() {
             "-Zcrate-attr=feature(register_tool)",
             "-Zcrate-attr=register_tool(kanitool)",
             "--sysroot",
-            "/home/zjp/rust/kani/target/kani",
+            &kani_path,
             "-L",
-            "/home/zjp/rust/kani/target/kani/lib",
+            &format!("{kani_path}/lib"),
             "--extern",
             "kani",
             "--extern",
-            "noprelude:std=/home/zjp/rust/kani/target/kani/lib/libstd.rlib",
+            &format!("noprelude:std={kani_path}/lib/libstd.rlib"),
             "-Zunstable-options",
             "-Zalways-encode-mir",
             "-Zmir-enable-passes=-RemoveStorageMarkers",