Merge pull request #97 from os-checker/diff

feat: add `merge` and `diff` subcommand for verify_rust_std CLI

Author: zjp-CN

src/bin/verify_rust_std/diff.rs

@@ -0,0 +1,31 @@
+use crate::{Result, read_json};
+use clap::Parser;
+use distributed_verification::diff::{MergeHashKaniList, diff};
+
+pub fn run(args: &[String]) -> Result<()> {
+    SubCmdDiff::parse_from(args).run()
+}
+
+/// `verify_rust_std diff` subcommand that emits a diff merge.json.
+#[derive(Parser, Debug)]
+struct SubCmdDiff {
+    /// Path to a previous merge.json that is generated by `verify_rust_std merge`.
+    #[arg(long)]
+    old: String,
+
+    /// Path to a recent merge.json that is generated by `verify_rust_std merge`.
+    #[arg(long)]
+    new: String,
+}
+
+impl SubCmdDiff {
+    fn run(self) -> Result<()> {
+        let old: Vec<MergeHashKaniList> = read_json(&self.old)?;
+        let new: Vec<MergeHashKaniList> = read_json(&self.new)?;
+
+        let difference = diff(&old, &new);
+        serde_json::to_writer_pretty(std::io::stdout(), &difference)?;
+
+        Ok(())
+    }
+}

src/bin/verify_rust_std/main.rs

@@ -1,6 +1,7 @@
 //! `VERIFY_RUST_STD_LIBRARY=path/to/verify-rust-std/library` and
 //! `KANI_DIR=path/to/kani` should be set beforehand.
 
+use distributed_verification::logger;
 use eyre::{Context, Result};
 use std::process::{Command, Stdio};
 
@@ -12,6 +13,9 @@ extern crate eyre;
 mod env;
 use env::ENV;
 
+mod diff;
+mod merge;
+
 fn main() -> Result<()> {
     let mut args = std::env::args().collect::<Vec<_>>();
 
@@ -38,6 +42,12 @@ fn main() -> Result<()> {
             // build non-core crates
             run("rustc", rustc_args, &[])
         }
+    } else if args.get(1).map(|arg| arg == "merge").unwrap_or(false) {
+        logger::init();
+        merge::run(&args[1..])
+    } else if args.get(1).map(|arg| arg == "diff").unwrap_or(false) {
+        logger::init();
+        diff::run(&args[1..])
     } else {
         run(
             "cargo",
@@ -80,3 +90,9 @@ fn build_core(args: Vec<String>) -> Result<()> {
     new_args.extend(args);
     run(&ENV.DISTRIBUTED_VERIFICATION, &new_args, &[])
 }
+
+fn read_json<T: serde::de::DeserializeOwned>(path: &str) -> Result<T> {
+    let _span = error_span!("read_json", path).entered();
+    let file = std::fs::File::open(path)?;
+    Ok(serde_json::from_reader(file)?)
+}

src/bin/verify_rust_std/merge.rs

@@ -0,0 +1,71 @@
+use crate::Result;
+use clap::Parser;
+use distributed_verification::{
+    SerFunction,
+    diff::{KaniListJson, MergeHashKaniList},
+};
+use std::collections::HashMap;
+
+pub fn run(args: &[String]) -> Result<()> {
+    SubCmdMerge::parse_from(args).run()
+}
+
+/// `verify_rust_std merge` subcommand
+#[derive(Parser, Debug)]
+struct SubCmdMerge {
+    /// Path to hash json file which is generated by distributed-verification.
+    #[arg(long)]
+    hash_json: String,
+
+    /// Strip file path prefix in hash json.
+    #[arg(long, default_value_t)]
+    strip_hash_json_prefix: String,
+
+    /// Path to kani-list.json which is generated by kani.
+    #[arg(long)]
+    kani_list: String,
+
+    /// Strip file path prefix in kani-list.
+    #[arg(long, default_value_t)]
+    strip_kani_list_prefix: String,
+}
+
+impl SubCmdMerge {
+    fn run(self) -> Result<()> {
+        debug!(?self);
+
+        let mut hash_json: Vec<SerFunction> = crate::read_json(&self.hash_json)?;
+
+        let mut kani_list: KaniListJson = crate::read_json(&self.kani_list)?;
+        // normalize paths like core/src/../../portable-simd/crates/core_simd/src/masks.rs
+        kani_list.normalize_file_path();
+
+        if !self.strip_kani_list_prefix.is_empty() {
+            kani_list.strip_path_prefix_raw(&self.strip_kani_list_prefix);
+        }
+
+        let mut hash_map = HashMap::with_capacity(hash_json.len());
+        for func in &mut hash_json {
+            let file = func.file.strip_prefix(&self.strip_hash_json_prefix).unwrap_or(&func.file);
+            let fn_name = &*func.name;
+            let value = &*func.hash;
+            hash_map.insert((file, fn_name), value);
+        }
+
+        let cap = kani_list.totals.standard_harnesses + kani_list.totals.contract_harnesses;
+        let mut v_merge = Vec::with_capacity(cap);
+        for file_func in kani_list.file_func_name() {
+            let (file, func) = file_func;
+            v_merge.push(MergeHashKaniList {
+                file: file.into(),
+                func: func.into(),
+                hash: hash_map.get(&file_func).map(|s| (*s).into()),
+            });
+        }
+        v_merge.sort_unstable();
+
+        serde_json::to_writer_pretty(std::io::stdout(), &v_merge)?;
+
+        Ok(())
+    }
+}

src/diff.rs

@@ -2,6 +2,7 @@ use crate::{BoxStr, ProofKind, SerFunction};
 use indexmap::{IndexMap, IndexSet};
 use serde::{Deserialize, Serialize};
 use std::{
+    collections::HashSet,
     hash::Hash,
     path::{Component, MAIN_SEPARATOR, Path, PathBuf},
 };
@@ -104,6 +105,10 @@ impl KaniListHarnesses {
             }
         }
     }
+
+    fn file_func_name(&self) -> impl Iterator<Item = (&str, &str)> {
+        self.inner.iter().flat_map(|(k, v)| v.iter().map(|func| (&**k, &**func)))
+    }
 }
 
 #[derive(Debug, Clone, Serialize, Deserialize, Eq, PartialEq, PartialOrd, Ord, Hash)]
@@ -119,9 +124,9 @@ pub struct ContractedFunction {
 #[derive(Debug, Clone, Serialize, Deserialize, Eq, PartialEq, PartialOrd, Ord)]
 #[serde(rename_all = "kebab-case")]
 pub struct Totals {
-    standard_harnesses: usize,
-    contract_harnesses: usize,
-    functions_under_contract: usize,
+    pub standard_harnesses: usize,
+    pub contract_harnesses: usize,
+    pub functions_under_contract: usize,
 }
 
 /// The datastructure generated from `kani list --json`.
@@ -187,6 +192,10 @@ impl KaniListJson {
         assert!(duplicates.is_empty(), "Function name duplicates: {duplicates:#?}");
         vec_to_set(&v)
     }
+
+    pub fn file_func_name(&self) -> impl Iterator<Item = (&str, &str)> {
+        self.standard_harnesses.file_func_name().chain(self.contract_harnesses.file_func_name())
+    }
 }
 
 fn count_gt1<T: Copy + Hash + Eq>(v: &[T]) -> Vec<(T, u32)> {
@@ -236,3 +245,23 @@ impl MergedHarnesses<'_> {
         vec_to_set(&v)
     }
 }
+
+/// Merge hash json and kani-list.
+#[derive(Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Hash, Serialize, Deserialize)]
+pub struct MergeHashKaniList {
+    pub file: Box<str>,
+    pub func: Box<str>,
+    #[serde(skip_serializing_if = "Option::is_none")]
+    #[serde(default)]
+    pub hash: Option<Box<str>>,
+}
+
+/// Compare two `MergeHashKaniList`, and returns the ones from new that don't match the old,
+/// usually the ones don't have hash values or whoes hash values changed.
+///
+/// If new is sorted, especially directly from the stdout of verify_rust_std merge subcommand,
+/// the result is sorted.
+pub fn diff(old: &[MergeHashKaniList], new: &[MergeHashKaniList]) -> Vec<MergeHashKaniList> {
+    let set: HashSet<_> = old.iter().collect();
+    new.iter().filter(|item| item.hash.is_none() || !set.contains(item)).cloned().collect()
+}