Merge pull request #19 from os-checker/tests-diff

Fix: ensures hash is unchanged when unrelated contracts and proofs are added

Author: zjp-CN

Cargo.lock

@@ -21,6 +21,7 @@ tracing-error = "0.2"
 [dev-dependencies]
 assert_cmd = "2.0.16"
 expect-test = "1.5.1"
+pretty_assertions = "1.4.1"
 
 [lints.rust]
 unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] }

Cargo.toml

@@ -0,0 +1,20 @@
+# Distributed and resource-efficient verification for verify-rust-std
+
+Context: [Distributed and resource-efficient verification][distributed], GSoC Rust 2025
+
+[distributed]: https://github.com/rust-lang/google-summer-of-code/tree/45141d74c28d91e114cf621d2d56aea6c3f82547?tab=readme-ov-file#distributed-and-resource-efficient-verification
+
+## Steps
+
+The list in very incomplete at the moment.
+
+- [ ] Analyze kani's proofs and contracts
+    - [x] Rust Compiler Driver
+    - [x] Reuse reachability code from kani
+    - [x] Traverse calls starting from proofs and contracts
+- [ ] Generate proofs that need to rerun
+    - [ ] Compute difference
+    - [ ] Emit JSON
+- [ ] CI setup
+    - [ ] Run kani
+    - [ ] Run ESBMC ??

README.md

@@ -9,6 +9,7 @@ use stable_mir::{
     mir::mono::{Instance, MonoItem},
     ty::{FnDef, RigidTy, Ty, TyKind},
 };
+use std::cmp::Ordering;
 
 mod kani;
 mod serialization;
@@ -81,6 +82,7 @@ impl Function {
 
         let mut callees = IndexSet::new();
         callgraph.recursive_callees(item, &mut callees);
+        callees.sort_by(|a, b| cmp_callees(a, b, tcx, src_map));
 
         let func = source_code_with(body.span, tcx, src_map);
         info!(" - {:?} ({span:?}): {func}", inst_def.name());
@@ -119,3 +121,20 @@ fn source_code_with(
     let span = internal(tcx, stable_mir_span);
     source_code(span, src_map)
 }
+
+fn source_code_of_body(inst: &Instance, tcx: TyCtxt, src_map: &SourceMap) -> Option<String> {
+    inst.body().map(|body| source_code_with(body.span, tcx, src_map))
+}
+
+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();
+    match filename_a.cmp(&filename_b) {
+        Ordering::Equal => (),
+        ord => return ord,
+    }
+
+    let body_a = source_code_of_body(a, tcx, src_map);
+    let body_b = source_code_of_body(b, tcx, src_map);
+    body_a.cmp(&body_b)
+}

src/functions/mod.rs

@@ -76,10 +76,7 @@ impl Callee {
         let inst_def = &inst.def;
         let def_id = format_def_id(&inst_def.def_id());
         let file = inst_def.span().get_filename();
-        let func = inst
-            .body()
-            .map(|body| super::source_code_with(body.span, tcx, src_map))
-            .unwrap_or_default();
+        let func = super::source_code_of_body(inst, tcx, src_map).unwrap_or_default();
         Callee { def_id, file, func }
     }
 }

src/functions/serialization.rs

@@ -0,0 +1,36 @@
+use serde::{Deserialize, Serialize};
+
+/// A Rust funtion with its file source, attributes, and raw function content.
+#[derive(Debug, Serialize, Deserialize)]
+pub struct SerFunction {
+    pub hash: String,
+    /// DefId in stable_mir.
+    pub def_id: String,
+    /// Every funtion must be declared in a specific file, even for those
+    /// generated by macros.
+    pub file: String,
+    /// Attributes are attached the function, but it seems that attributes
+    /// and function must be separated to query.
+    pub attrs: Vec<String>,
+    /// Raw function string, including name, signature, and body.
+    pub func: String,
+    /// Recursive fnction calls inside the body.
+    pub callees: Vec<Callee>,
+}
+
+#[derive(Debug, Serialize, Deserialize)]
+pub struct Callee {
+    pub def_id: String,
+    pub file: String,
+    pub func: String,
+}
+
+impl SerFunction {
+    /// Even though callees are in insertion order, to make them easy to check,
+    /// sort by file and function.
+    pub fn callee_sorted_by_file_func(&self) -> Vec<[&str; 2]> {
+        let mut callees: Vec<_> = self.callees.iter().collect();
+        callees.sort_by(|a, b| (&a.file, &a.func).cmp(&(&b.file, &b.func)));
+        callees.into_iter().map(|c| [&*c.file, &*c.func]).collect()
+    }
+}

src/lib.rs

@@ -0,0 +1,10 @@
+#[cfg(kani)]
+mod verify {
+    #[kani::requires(a > 0)]
+    pub fn contract(a: u8) {}
+
+    #[kani::proof]
+    pub fn f() {
+        contract(0);
+    }
+}

tests/compare/contract1.rs

@@ -0,0 +1,13 @@
+#[cfg(kani)]
+mod verify {
+    #[kani::requires(a > 0)]
+    pub fn contract(a: u8) {}
+
+    #[kani::proof]
+    pub fn f() {
+        contract(0);
+    }
+
+    #[kani::requires(a > 0)]
+    pub fn g(a: u8) {}
+}

tests/compare/contract2.rs

@@ -0,0 +1,8 @@
+#[cfg(kani)]
+mod verify {
+    #[kani::proof]
+    pub fn f() {
+        let a = 1;
+        assert_eq!(a + 1, 2);
+    }
+}

tests/compare/proof1.rs

@@ -0,0 +1,14 @@
+#[cfg(kani)]
+mod verify {
+    #[kani::proof]
+    pub fn f() {
+        let a = 1;
+        assert_eq!(a + 1, 2);
+    }
+
+    #[kani::proof]
+    pub fn g() {
+        let a = 1;
+        assert_eq!(a + 1, 2);
+    }
+}