Skip to content

Commit 4269a85

Browse files
committed
verify_rust_std: add diff subcommand to emit a diff merge.json
1 parent be74ad4 commit 4269a85

File tree

4 files changed

+55
-27
lines changed

4 files changed

+55
-27
lines changed

src/bin/verify_rust_std/diff.rs

Lines changed: 31 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,31 @@
1+
use crate::{Result, read_json};
2+
use clap::Parser;
3+
use distributed_verification::diff::{MergeHashKaniList, diff};
4+
5+
pub fn run(args: &[String]) -> Result<()> {
6+
SubCmdDiff::parse_from(args).run()
7+
}
8+
9+
/// `verify_rust_std diff` subcommand that emits a diff merge.json.
10+
#[derive(Parser, Debug)]
11+
struct SubCmdDiff {
12+
/// Path to a previous merge.json that is generated by `verify_rust_std merge`.
13+
#[arg(long)]
14+
old: String,
15+
16+
/// Path to a recent merge.json that is generated by `verify_rust_std merge`.
17+
#[arg(long)]
18+
new: String,
19+
}
20+
21+
impl SubCmdDiff {
22+
fn run(self) -> Result<()> {
23+
let old: Vec<MergeHashKaniList> = read_json(&self.old)?;
24+
let new: Vec<MergeHashKaniList> = read_json(&self.new)?;
25+
26+
let difference = diff(&old, &new);
27+
serde_json::to_writer_pretty(std::io::stdout(), &difference)?;
28+
29+
Ok(())
30+
}
31+
}

src/bin/verify_rust_std/main.rs

Lines changed: 12 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11
//! `VERIFY_RUST_STD_LIBRARY=path/to/verify-rust-std/library` and
22
//! `KANI_DIR=path/to/kani` should be set beforehand.
33
4+
use distributed_verification::logger;
45
use eyre::{Context, Result};
56
use std::process::{Command, Stdio};
67

@@ -12,6 +13,7 @@ extern crate eyre;
1213
mod env;
1314
use env::ENV;
1415

16+
mod diff;
1517
mod merge;
1618

1719
fn main() -> Result<()> {
@@ -41,8 +43,11 @@ fn main() -> Result<()> {
4143
run("rustc", rustc_args, &[])
4244
}
4345
} else if args.get(1).map(|arg| arg == "merge").unwrap_or(false) {
44-
distributed_verification::logger::init();
46+
logger::init();
4547
merge::run(&args[1..])
48+
} else if args.get(1).map(|arg| arg == "diff").unwrap_or(false) {
49+
logger::init();
50+
diff::run(&args[1..])
4651
} else {
4752
run(
4853
"cargo",
@@ -85,3 +90,9 @@ fn build_core(args: Vec<String>) -> Result<()> {
8590
new_args.extend(args);
8691
run(&ENV.DISTRIBUTED_VERIFICATION, &new_args, &[])
8792
}
93+
94+
fn read_json<T: serde::de::DeserializeOwned>(path: &str) -> Result<T> {
95+
let _span = error_span!("read_json", path).entered();
96+
let file = std::fs::File::open(path)?;
97+
Ok(serde_json::from_reader(file)?)
98+
}

src/bin/verify_rust_std/merge.rs

Lines changed: 6 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ use distributed_verification::{
44
SerFunction,
55
diff::{KaniListJson, MergeHashKaniList},
66
};
7-
use std::{collections::HashMap, fs::File};
7+
use std::collections::HashMap;
88

99
pub fn run(args: &[String]) -> Result<()> {
1010
SubCmdMerge::parse_from(args).run()
@@ -34,7 +34,11 @@ impl SubCmdMerge {
3434
fn run(self) -> Result<()> {
3535
debug!(?self);
3636

37-
let (mut hash_json, mut kani_list) = read_json(&self.hash_json, &self.kani_list)?;
37+
let mut hash_json: Vec<SerFunction> = crate::read_json(&self.hash_json)?;
38+
39+
let mut kani_list: KaniListJson = crate::read_json(&self.kani_list)?;
40+
// normalize paths like core/src/../../portable-simd/crates/core_simd/src/masks.rs
41+
kani_list.normalize_file_path();
3842

3943
if !self.strip_kani_list_prefix.is_empty() {
4044
kani_list.strip_path_prefix_raw(&self.strip_kani_list_prefix);
@@ -65,24 +69,3 @@ impl SubCmdMerge {
6569
Ok(())
6670
}
6771
}
68-
69-
fn read_json(
70-
hash_json_path: &str,
71-
kani_list_path: &str,
72-
) -> Result<(Vec<SerFunction>, KaniListJson)> {
73-
let hash_json: Vec<SerFunction> = {
74-
let _span = error_span!("hash_json_path", hash_json_path).entered();
75-
let file = File::open(hash_json_path)?;
76-
serde_json::from_reader(file)?
77-
};
78-
79-
let mut kani_list: KaniListJson = {
80-
let _span = error_span!("kani_list_path", kani_list_path).entered();
81-
let file = File::open(kani_list_path)?;
82-
serde_json::from_reader(file)?
83-
};
84-
// normalize paths like core/src/../../portable-simd/crates/core_simd/src/masks.rs
85-
kani_list.normalize_file_path();
86-
87-
Ok((hash_json, kani_list))
88-
}

src/diff.rs

Lines changed: 6 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -256,9 +256,12 @@ pub struct MergeHashKaniList {
256256
pub hash: Option<Box<str>>,
257257
}
258258

259-
/// Compare two `MergeHashKaniList`, and returns the ones from new that don't have hash values or
260-
/// whoes hash values changed.
259+
/// Compare two `MergeHashKaniList`, and returns the ones from new that don't match the old,
260+
/// usually the ones don't have hash values or whoes hash values changed.
261+
///
262+
/// If new is sorted, especially directly from the stdout of verify_rust_std merge subcommand,
263+
/// the result is sorted.
261264
pub fn diff(old: &[MergeHashKaniList], new: &[MergeHashKaniList]) -> Vec<MergeHashKaniList> {
262265
let set: HashSet<_> = old.iter().collect();
263-
new.iter().filter(|item| !set.contains(item)).cloned().collect()
266+
new.iter().filter(|item| item.hash.is_none() || !set.contains(item)).cloned().collect()
264267
}

0 commit comments

Comments
 (0)