From bcad629eecabff0499d189f65003dad82078eb1c Mon Sep 17 00:00:00 2001 From: Jay Bosamiya Date: Mon, 1 Apr 2024 18:08:58 -0400 Subject: [PATCH 1/5] Make `parse_and_format` non-public --- src/lib.rs | 2 +- tests/rustfmt-matching.rs | 11 +++++++++-- tests/verus-consistency.rs | 11 ++++++++++- 3 files changed, 20 insertions(+), 4 deletions(-) diff --git a/src/lib.rs b/src/lib.rs index 41d046a..ad6c2d7 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -1514,7 +1514,7 @@ impl miette::Diagnostic for ParseAndFormatError { } } -pub fn parse_and_format(s: &str) -> miette::Result { +fn parse_and_format(s: &str) -> miette::Result { let ctx = Context { inline_comment_lines: find_inline_comment_lines(s), }; diff --git a/tests/rustfmt-matching.rs b/tests/rustfmt-matching.rs index f9a9d0b..2143b8c 100644 --- a/tests/rustfmt-matching.rs +++ b/tests/rustfmt-matching.rs @@ -1,11 +1,18 @@ -use verusfmt::{parse_and_format, rustfmt, VERUS_PREFIX, VERUS_SUFFIX}; +use verusfmt::{rustfmt, VERUS_PREFIX, VERUS_SUFFIX}; /// Tests to check that when formatting standard Rust syntax, /// we match rustfmt fn compare(file: &str) { let verus_file = format!("{}{}{}", VERUS_PREFIX, file, VERUS_SUFFIX); - let verus_fmt = parse_and_format(&verus_file).unwrap(); + let verus_fmt = verusfmt::run( + &verus_file, + verusfmt::RunOptions { + file_name: None, + run_rustfmt: false, + }, + ) + .unwrap(); let start = VERUS_PREFIX.len(); let end = verus_fmt.len() - VERUS_SUFFIX.len(); let verus_inner = &verus_fmt[start..end]; diff --git a/tests/verus-consistency.rs b/tests/verus-consistency.rs index 9838555..133230d 100644 --- a/tests/verus-consistency.rs +++ b/tests/verus-consistency.rs @@ -1,11 +1,20 @@ use insta::assert_snapshot; -use verusfmt::parse_and_format; /// Tests of Verus-specific formatting // We use insta tests (http://insta.rs) to manage the correct answers. // See README.md for details on how to run and update these tests. +fn parse_and_format(s: &str) -> miette::Result { + verusfmt::run( + s, + verusfmt::RunOptions { + file_name: None, + run_rustfmt: true, + }, + ) +} + #[test] fn verus_functions() { let file = r#" From 2d58919f0b13801c0e6e45e007a0b44bec4615b9 Mon Sep 17 00:00:00 2001 From: Jay Bosamiya Date: Mon, 1 Apr 2024 18:49:40 -0400 Subject: [PATCH 2/5] Support passing an explicit `rustfmt.toml` --- Cargo.lock | 114 ++++++++++++++++++++++++++++++------- Cargo.toml | 1 + src/lib.rs | 9 ++- src/main.rs | 2 + src/rustfmt.rs | 57 +++++++++++++++++-- tests/rustfmt-matching.rs | 1 + tests/verus-consistency.rs | 1 + 7 files changed, 157 insertions(+), 28 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 1481b81..2e06fe3 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -107,9 +107,9 @@ dependencies = [ [[package]] name = "bitflags" -version = "2.3.3" +version = "2.5.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "630be753d4e58660abd17930c71b647fe46c27ea6b63cc59e1e3851406972e42" +checksum = "cf4b9d6a944f767f8e5e0db018570623c85f3d925ac718db4e06d0187adb21c1" [[package]] name = "block-buffer" @@ -234,24 +234,19 @@ checksum = "a357d28ed41a50f9c765dbfe56cbc04a64e53e5fc58ba79fbc34c10ef3df831f" [[package]] name = "errno" -version = "0.3.1" +version = "0.3.8" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4bcfec3a70f97c962c307b2d2c56e358cf1d00b558d74262b5f929ee8cc7e73a" +checksum = "a258e46cdc063eb8519c00b9fc845fc47bcfca4130e2f08e88665ceda8474245" dependencies = [ - "errno-dragonfly", "libc", - "windows-sys 0.48.0", + "windows-sys 0.52.0", ] [[package]] -name = "errno-dragonfly" -version = "0.1.2" +name = "fastrand" +version = "2.0.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "aa68f1b12764fab894d2755d2518754e71b4fd80ecfb822714a1206c2aab39bf" -dependencies = [ - "cc", - "libc", -] +checksum = "658bd65b1cf4c852a3cc96f18a8ce7b5640f6b703f905c7d74532294c2a63984" [[package]] name = "fs-err" @@ -340,9 +335,9 @@ checksum = "e2abad23fbc42b3700f2f279844dc832adb2b2eb069b2df918f455c4e18cc646" [[package]] name = "libc" -version = "0.2.147" +version = "0.2.153" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b4668fb0ea861c1df094127ac5f1da3409a82116a4ba74fca2e58ef927159bb3" +checksum = "9c198f91728a82281a64e1f4f9eeb25d82cb32a5de251c6bd1b5154d63a8e7bd" [[package]] name = "linked-hash-map" @@ -352,9 +347,9 @@ checksum = "0717cef1bc8b636c6e1c1bbdefc09e6322da8a9321966e8928ef80d20f7f770f" [[package]] name = "linux-raw-sys" -version = "0.4.3" +version = "0.4.13" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "09fc20d2ca12cb9f044c93e3bd6d32d523e6e2ec3db4f7b2939cd99026ecd3f0" +checksum = "01cda141df6706de531b6c46c3a33ecca755538219bd484262fa09410c13539c" [[package]] name = "log" @@ -562,15 +557,15 @@ checksum = "d626bb9dae77e28219937af045c257c28bfd3f69333c512553507f5f9798cb76" [[package]] name = "rustix" -version = "0.38.4" +version = "0.38.32" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0a962918ea88d644592894bc6dc55acc6c0956488adcebbfb6e273506b7fd6e5" +checksum = "65e04861e65f21776e67888bfbea442b3642beaa0138fdb1dd7a84a52dffdb89" dependencies = [ "bitflags", "errno", "libc", "linux-raw-sys", - "windows-sys 0.48.0", + "windows-sys 0.52.0", ] [[package]] @@ -656,6 +651,18 @@ dependencies = [ "unicode-ident", ] +[[package]] +name = "tempfile" +version = "3.10.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "85b77fafb263dd9d05cbeac119526425676db3784113aa9295c88498cbf8bff1" +dependencies = [ + "cfg-if", + "fastrand", + "rustix", + "windows-sys 0.52.0", +] + [[package]] name = "terminal_size" version = "0.1.17" @@ -840,6 +847,7 @@ dependencies = [ "pretty", "regex", "similar", + "tempfile", "thiserror", "tracing", "tracing-subscriber", @@ -885,6 +893,15 @@ dependencies = [ "windows-targets 0.48.1", ] +[[package]] +name = "windows-sys" +version = "0.52.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "282be5f36a8ce781fad8c8ae18fa3f9beff57ec1b52cb3de0789201425d9a33d" +dependencies = [ + "windows-targets 0.52.4", +] + [[package]] name = "windows-targets" version = "0.42.2" @@ -915,6 +932,21 @@ dependencies = [ "windows_x86_64_msvc 0.48.0", ] +[[package]] +name = "windows-targets" +version = "0.52.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7dd37b7e5ab9018759f893a1952c9420d060016fc19a472b4bb20d1bdd694d1b" +dependencies = [ + "windows_aarch64_gnullvm 0.52.4", + "windows_aarch64_msvc 0.52.4", + "windows_i686_gnu 0.52.4", + "windows_i686_msvc 0.52.4", + "windows_x86_64_gnu 0.52.4", + "windows_x86_64_gnullvm 0.52.4", + "windows_x86_64_msvc 0.52.4", +] + [[package]] name = "windows_aarch64_gnullvm" version = "0.42.2" @@ -927,6 +959,12 @@ version = "0.48.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "91ae572e1b79dba883e0d315474df7305d12f569b400fcf90581b06062f7e1bc" +[[package]] +name = "windows_aarch64_gnullvm" +version = "0.52.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "bcf46cf4c365c6f2d1cc93ce535f2c8b244591df96ceee75d8e83deb70a9cac9" + [[package]] name = "windows_aarch64_msvc" version = "0.42.2" @@ -939,6 +977,12 @@ version = "0.48.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "b2ef27e0d7bdfcfc7b868b317c1d32c641a6fe4629c171b8928c7b08d98d7cf3" +[[package]] +name = "windows_aarch64_msvc" +version = "0.52.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "da9f259dd3bcf6990b55bffd094c4f7235817ba4ceebde8e6d11cd0c5633b675" + [[package]] name = "windows_i686_gnu" version = "0.42.2" @@ -951,6 +995,12 @@ version = "0.48.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "622a1962a7db830d6fd0a69683c80a18fda201879f0f447f065a3b7467daa241" +[[package]] +name = "windows_i686_gnu" +version = "0.52.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b474d8268f99e0995f25b9f095bc7434632601028cf86590aea5c8a5cb7801d3" + [[package]] name = "windows_i686_msvc" version = "0.42.2" @@ -963,6 +1013,12 @@ version = "0.48.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "4542c6e364ce21bf45d69fdd2a8e455fa38d316158cfd43b3ac1c5b1b19f8e00" +[[package]] +name = "windows_i686_msvc" +version = "0.52.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1515e9a29e5bed743cb4415a9ecf5dfca648ce85ee42e15873c3cd8610ff8e02" + [[package]] name = "windows_x86_64_gnu" version = "0.42.2" @@ -975,6 +1031,12 @@ version = "0.48.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "ca2b8a661f7628cbd23440e50b05d705db3686f894fc9580820623656af974b1" +[[package]] +name = "windows_x86_64_gnu" +version = "0.52.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5eee091590e89cc02ad514ffe3ead9eb6b660aedca2183455434b93546371a03" + [[package]] name = "windows_x86_64_gnullvm" version = "0.42.2" @@ -987,6 +1049,12 @@ version = "0.48.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "7896dbc1f41e08872e9d5e8f8baa8fdd2677f29468c4e156210174edc7f7b953" +[[package]] +name = "windows_x86_64_gnullvm" +version = "0.52.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "77ca79f2451b49fa9e2af39f0747fe999fcda4f5e241b2898624dca97a1f2177" + [[package]] name = "windows_x86_64_msvc" version = "0.42.2" @@ -999,6 +1067,12 @@ version = "0.48.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "1a515f5799fe4961cb532f983ce2b23082366b898e52ffbce459c86f67c8378a" +[[package]] +name = "windows_x86_64_msvc" +version = "0.52.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "32b752e52a2da0ddfbdbcc6fceadfeede4c939ed16d13e648833a61dfb611ed8" + [[package]] name = "yaml-rust" version = "0.4.5" diff --git a/Cargo.toml b/Cargo.toml index d4181a2..859e0a1 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -29,6 +29,7 @@ pest_derive = "2.0" pretty = "0.12.1" regex = "1.9.6" similar = "2.2.1" +tempfile = "3.10.1" thiserror = "1.0.52" tracing = "0.1.37" tracing-subscriber = { version = "0.3.17" } diff --git a/src/lib.rs b/src/lib.rs index ad6c2d7..6504376 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -3,7 +3,7 @@ mod rustfmt; -pub use crate::rustfmt::rustfmt; +pub use crate::rustfmt::{rustfmt, RustFmtConfig}; use itertools::Itertools; use pest::{iterators::Pair, iterators::Pairs, Parser}; @@ -1596,6 +1596,8 @@ pub struct RunOptions { pub file_name: Option, /// Whether to run rustfmt on non-verus parts of code. pub run_rustfmt: bool, + /// Whether to perform extra configuration for the rustfmt run. Ignored if `run_rustfmt` is false. + pub rustfmt_config: RustFmtConfig, } impl Default for RunOptions { @@ -1603,6 +1605,7 @@ impl Default for RunOptions { Self { file_name: None, run_rustfmt: true, + rustfmt_config: Default::default(), } } } @@ -1622,7 +1625,9 @@ pub fn run(s: &str, opts: RunOptions) -> miette::Result { let formatted_output = if !opts.run_rustfmt { verus_fmted } else { - rustfmt(&verus_fmted).ok_or(miette::miette!("rustfmt failed"))? + opts.rustfmt_config + .run(&verus_fmted) + .ok_or(miette::miette!("rustfmt failed"))? }; Ok(formatted_output) diff --git a/src/main.rs b/src/main.rs index 330555b..d5921fe 100644 --- a/src/main.rs +++ b/src/main.rs @@ -44,6 +44,7 @@ fn format_file(file: &PathBuf, args: &Args) -> miette::Result<()> { verusfmt::RunOptions { file_name: Some(file.to_string_lossy().into()), run_rustfmt: !args.verus_only, + rustfmt_config: Default::default(), }, )?; @@ -76,6 +77,7 @@ fn format_file(file: &PathBuf, args: &Args) -> miette::Result<()> { verusfmt::RunOptions { file_name: Some(file.to_string_lossy().into()), run_rustfmt: !args.verus_only, + rustfmt_config: Default::default(), }, )?; if formatted_output == reformatted { diff --git a/src/rustfmt.rs b/src/rustfmt.rs index f4bc118..ee1f71f 100644 --- a/src/rustfmt.rs +++ b/src/rustfmt.rs @@ -15,8 +15,35 @@ fn is_multiline_comment(pair: &Pair) -> bool { matches!(&pair.as_span().as_str()[..2], "/*") } -/// Run rustfmt, only on code outside the `verus!` macro +/// Run rustfmt, only on code outside the `verus!` macro. +/// +/// Convenience wrapper around [`RustFmtConfig`]. Equivalent to `RustFmtConfig::default().run(s)`. pub fn rustfmt(s: &str) -> Option { + RustFmtConfig::default().run(s) +} + +/// Options to pass to [`rustfmt_with_config`] +pub struct RustFmtConfig { + /// If set, explicitly provides the specified `rustfmt.toml` configuration to rustfmt; + /// otherwise, uses the default behavior (i.e., picking up `rustfmt.toml` if it exists from + /// working directory or ancestors) + pub rustfmt_toml: Option, +} + +impl Default for RustFmtConfig { + fn default() -> Self { + Self { rustfmt_toml: None } + } +} + +impl RustFmtConfig { + pub fn run(&self, s: &str) -> Option { + rustfmt_with_config(s, self) + } +} + +/// Run rustfmt, only on code outside the `verus!` macro. +fn rustfmt_with_config(s: &str, config: &RustFmtConfig) -> Option { let parsed_file = MinimalVerusParser::parse(Rule::file, s) .expect("Minimal parsing should never fail. If it did, please report this as an error.") .next() @@ -51,7 +78,7 @@ pub fn rustfmt(s: &str) -> Option { } } - let formatted = run_rustfmt(&collapsed_input)?; + let formatted = run_rustfmt(&collapsed_input, config)?; let parsed_file = MinimalVerusParser::parse(Rule::file, &formatted) .expect("Minimal parsing should never fail. If it did, please report this as an error.") @@ -116,10 +143,27 @@ pub fn rustfmt(s: &str) -> Option { Some(final_output) } -fn run_rustfmt(s: &str) -> Option { - let mut proc = Command::new("rustfmt") - .arg("--emit=stdout") - .arg("--edition=2021") +fn run_rustfmt(s: &str, config: &RustFmtConfig) -> Option { + let mut rustfmt = Command::new("rustfmt"); + + // Set up standard arguments we always pass + rustfmt.arg("--emit=stdout").arg("--edition=2021"); + + // If we need to, explicitly set up the rustfmt.toml file + let tempdir = config.rustfmt_toml.as_ref().map(|toml| { + let tempdir = tempfile::Builder::new() + .prefix("verusfmt") + .tempdir() + .unwrap(); + std::fs::File::create_new(tempdir.path().join("rustfmt.toml")) + .unwrap() + .write_all(toml.as_bytes()) + .unwrap(); + rustfmt.arg("--config-path").arg(tempdir.path()); + tempdir + }); + + let mut proc = rustfmt .stdin(Stdio::piped()) .stdout(Stdio::piped()) .stderr(Stdio::piped()) @@ -133,6 +177,7 @@ fn run_rustfmt(s: &str) -> Option { .unwrap(); let output = proc.wait_with_output().ok()?; + drop(tempdir); if output.status.success() { Some(String::from_utf8(output.stdout).unwrap()) } else { diff --git a/tests/rustfmt-matching.rs b/tests/rustfmt-matching.rs index 2143b8c..c9375c5 100644 --- a/tests/rustfmt-matching.rs +++ b/tests/rustfmt-matching.rs @@ -10,6 +10,7 @@ fn compare(file: &str) { verusfmt::RunOptions { file_name: None, run_rustfmt: false, + rustfmt_config: Default::default(), }, ) .unwrap(); diff --git a/tests/verus-consistency.rs b/tests/verus-consistency.rs index 133230d..d7fbdea 100644 --- a/tests/verus-consistency.rs +++ b/tests/verus-consistency.rs @@ -11,6 +11,7 @@ fn parse_and_format(s: &str) -> miette::Result { verusfmt::RunOptions { file_name: None, run_rustfmt: true, + rustfmt_config: Default::default(), }, ) } From 2d12da92ba8a7ea7ad3f122d91ef5dbc4ef1c843 Mon Sep 17 00:00:00 2001 From: Jay Bosamiya Date: Mon, 1 Apr 2024 19:12:09 -0400 Subject: [PATCH 3/5] Improve rustfmt.toml detection Previously, it would pick up from the cwd or ancestors, which can be surprising (and also goes against what rustfmt itself does); with this commit, we explicitly do the same sort of search that rustfmt does, and pick up the correct rustfmt.toml, thereby making our execution independent of where we ran from --- src/main.rs | 25 +++++++++++++++++++++++-- src/rustfmt.rs | 3 ++- 2 files changed, 25 insertions(+), 3 deletions(-) diff --git a/src/main.rs b/src/main.rs index d5921fe..211023b 100644 --- a/src/main.rs +++ b/src/main.rs @@ -4,6 +4,7 @@ use clap::{Parser as ClapParser, ValueEnum}; use fs_err as fs; use miette::{miette, IntoDiagnostic}; use tracing::{error, info}; // debug, trace +use verusfmt::RustFmtConfig; /// A collection of options that should not be relied upon existing long-term, added primarily for /// verusfmt developers to use. @@ -39,12 +40,32 @@ struct Args { fn format_file(file: &PathBuf, args: &Args) -> miette::Result<()> { let unparsed_file = fs::read_to_string(file).into_diagnostic()?; + let rustfmt_config = { + // Repeatedly check for ancestors of `file` until we find either `rustfmt.toml` or + // `.rustfmt.toml`; if we do, that becomes `rustfmt_toml` + let rustfmt_toml = file + .canonicalize() + .unwrap() + .ancestors() + .flat_map(|dir| { + // Why in this particular order? That's the order in which rustfmt checks: + // https://github.com/rust-lang/rustfmt/blob/202fa22cee5badff77129a7bea5c90228d354ac9/src/config/mod.rs#L368-L369 + [".rustfmt.toml", "rustfmt.toml"] + .into_iter() + .map(|n| dir.join(n)) + }) + .filter_map(|p| p.exists().then(|| fs::read_to_string(p).unwrap())) + .next(); + + RustFmtConfig { rustfmt_toml } + }; + let formatted_output = verusfmt::run( &unparsed_file, verusfmt::RunOptions { file_name: Some(file.to_string_lossy().into()), run_rustfmt: !args.verus_only, - rustfmt_config: Default::default(), + rustfmt_config: rustfmt_config.clone(), }, )?; @@ -77,7 +98,7 @@ fn format_file(file: &PathBuf, args: &Args) -> miette::Result<()> { verusfmt::RunOptions { file_name: Some(file.to_string_lossy().into()), run_rustfmt: !args.verus_only, - rustfmt_config: Default::default(), + rustfmt_config, }, )?; if formatted_output == reformatted { diff --git a/src/rustfmt.rs b/src/rustfmt.rs index ee1f71f..5544c09 100644 --- a/src/rustfmt.rs +++ b/src/rustfmt.rs @@ -23,10 +23,11 @@ pub fn rustfmt(s: &str) -> Option { } /// Options to pass to [`rustfmt_with_config`] +#[derive(Clone)] pub struct RustFmtConfig { /// If set, explicitly provides the specified `rustfmt.toml` configuration to rustfmt; /// otherwise, uses the default behavior (i.e., picking up `rustfmt.toml` if it exists from - /// working directory or ancestors) + /// the file's directory or ancestors) pub rustfmt_toml: Option, } From 3e1922d01b72396348e3b2f5891465784c19fbe7 Mon Sep 17 00:00:00 2001 From: Jay Bosamiya Date: Mon, 1 Apr 2024 19:15:20 -0400 Subject: [PATCH 4/5] Use Verus's rustfmt.toml for the verus snapshot --- examples/verus-snapshot/get_latest.sh | 2 +- examples/verus-snapshot/source/rustfmt.toml | 7 +++++ .../source/vstd/source/vstd/atomic.rs | 8 +----- .../source/vstd/source/vstd/atomic_ghost.rs | 26 +++---------------- .../source/vstd/source/vstd/std_specs/num.rs | 16 ++---------- tests/snapshot-examples.rs | 19 ++++++++++++-- 6 files changed, 32 insertions(+), 46 deletions(-) create mode 100644 examples/verus-snapshot/source/rustfmt.toml diff --git a/examples/verus-snapshot/get_latest.sh b/examples/verus-snapshot/get_latest.sh index 37773d8..59d6f91 100755 --- a/examples/verus-snapshot/get_latest.sh +++ b/examples/verus-snapshot/get_latest.sh @@ -12,7 +12,7 @@ wget --quiet -O verus.zip https://github.com/verus-lang/verus/archive/refs/heads echo "[INFO] Unzipping Verus" unzip -q verus.zip -MOVE_PATHS="source/rust_verify/example/syntax.rs source/vstd" +MOVE_PATHS="source/rustfmt.toml source/rust_verify/example/syntax.rs source/vstd" echo "[INFO] Moving files" for path in $MOVE_PATHS; do diff --git a/examples/verus-snapshot/source/rustfmt.toml b/examples/verus-snapshot/source/rustfmt.toml new file mode 100644 index 0000000..9daac34 --- /dev/null +++ b/examples/verus-snapshot/source/rustfmt.toml @@ -0,0 +1,7 @@ +# Copied from Rust compiler's rustfmt.toml settings + +# Run rustfmt with this config (it should be picked up automatically). +# unstable_features=true # provided by vargo +# version=Two # provided by vargo +use_small_heuristics = "Max" +merge_derives = false diff --git a/examples/verus-snapshot/source/vstd/source/vstd/atomic.rs b/examples/verus-snapshot/source/vstd/source/vstd/atomic.rs index 561c6df..906cff9 100644 --- a/examples/verus-snapshot/source/vstd/source/vstd/atomic.rs +++ b/examples/verus-snapshot/source/vstd/source/vstd/atomic.rs @@ -471,13 +471,7 @@ macro_rules! atomic_bool_methods { }; } -make_bool_atomic!( - PAtomicBool, - PermissionBool, - PermissionDataBool, - AtomicBool, - bool -); +make_bool_atomic!(PAtomicBool, PermissionBool, PermissionDataBool, AtomicBool, bool); make_unsigned_integer_atomic!( PAtomicU8, diff --git a/examples/verus-snapshot/source/vstd/source/vstd/atomic_ghost.rs b/examples/verus-snapshot/source/vstd/source/vstd/atomic_ghost.rs index 1da04c3..4dee0b0 100644 --- a/examples/verus-snapshot/source/vstd/source/vstd/atomic_ghost.rs +++ b/examples/verus-snapshot/source/vstd/source/vstd/atomic_ghost.rs @@ -114,33 +114,15 @@ declare_atomic_type!(AtomicU64, PAtomicU64, PermissionU64, u64, AtomicPredU64); declare_atomic_type!(AtomicU32, PAtomicU32, PermissionU32, u32, AtomicPredU32); declare_atomic_type!(AtomicU16, PAtomicU16, PermissionU16, u16, AtomicPredU16); declare_atomic_type!(AtomicU8, PAtomicU8, PermissionU8, u8, AtomicPredU8); -declare_atomic_type!( - AtomicUsize, - PAtomicUsize, - PermissionUsize, - usize, - AtomicPredUsize -); +declare_atomic_type!(AtomicUsize, PAtomicUsize, PermissionUsize, usize, AtomicPredUsize); declare_atomic_type!(AtomicI64, PAtomicI64, PermissionI64, i64, AtomicPredI64); declare_atomic_type!(AtomicI32, PAtomicI32, PermissionI32, i32, AtomicPredI32); declare_atomic_type!(AtomicI16, PAtomicI16, PermissionI16, i16, AtomicPredI16); declare_atomic_type!(AtomicI8, PAtomicI8, PermissionI8, i8, AtomicPredI8); -declare_atomic_type!( - AtomicIsize, - PAtomicIsize, - PermissionIsize, - isize, - AtomicPredIsize -); - -declare_atomic_type!( - AtomicBool, - PAtomicBool, - PermissionBool, - bool, - AtomicPredBool -); +declare_atomic_type!(AtomicIsize, PAtomicIsize, PermissionIsize, isize, AtomicPredIsize); + +declare_atomic_type!(AtomicBool, PAtomicBool, PermissionBool, bool, AtomicPredBool); /// Performs a given atomic operation on a given atomic /// while providing access to its ghost state. diff --git a/examples/verus-snapshot/source/vstd/source/vstd/std_specs/num.rs b/examples/verus-snapshot/source/vstd/source/vstd/std_specs/num.rs index 0fee85b..63edbb6 100644 --- a/examples/verus-snapshot/source/vstd/source/vstd/std_specs/num.rs +++ b/examples/verus-snapshot/source/vstd/source/vstd/std_specs/num.rs @@ -165,20 +165,8 @@ num_specs!(u8, i8, u8_specs, i8_specs, 0x100); num_specs!(u16, i16, u16_specs, i16_specs, 0x1_0000); num_specs!(u32, i32, u32_specs, i32_specs, 0x1_0000_0000); num_specs!(u64, i64, u64_specs, i64_specs, 0x1_0000_0000_0000_0000); -num_specs!( - u128, - i128, - u128_specs, - i128_specs, - 0x1_0000_0000_0000_0000_0000_0000_0000_0000 -); -num_specs!( - usize, - isize, - usize_specs, - isize_specs, - (usize::MAX - usize::MIN + 1) -); +num_specs!(u128, i128, u128_specs, i128_specs, 0x1_0000_0000_0000_0000_0000_0000_0000_0000); +num_specs!(usize, isize, usize_specs, isize_specs, (usize::MAX - usize::MIN + 1)); verus! { diff --git a/tests/snapshot-examples.rs b/tests/snapshot-examples.rs index c988421..8c2ec49 100644 --- a/tests/snapshot-examples.rs +++ b/tests/snapshot-examples.rs @@ -5,7 +5,11 @@ //! modified by any change. fn check_snapshot(original: &str) { - let formatted = verusfmt::run(original, Default::default()).unwrap(); + check_snapshot_with_config(original, Default::default()) +} + +fn check_snapshot_with_config(original: &str, config: verusfmt::RunOptions) { + let formatted = verusfmt::run(original, config).unwrap(); if original != formatted { let diff = similar::udiff::unified_diff( similar::Algorithm::Patience, @@ -52,9 +56,20 @@ fn pagetable_rs_unchanged() { #[test] fn verus_snapshot_unchanged() { + let rustfmt_toml = + std::fs::read_to_string("./examples/verus-snapshot/source/rustfmt.toml").unwrap(); for path in glob::glob("./examples/verus-snapshot/**/*.rs").unwrap() { let path = path.unwrap(); println!("Checking snapshot for {:?}", path); - check_snapshot(&std::fs::read_to_string(path).unwrap()); + check_snapshot_with_config( + &std::fs::read_to_string(path).unwrap(), + verusfmt::RunOptions { + file_name: None, + run_rustfmt: true, + rustfmt_config: verusfmt::RustFmtConfig { + rustfmt_toml: Some(rustfmt_toml.clone()), + }, + }, + ); } } From 086146ee21779555f2129718177b0423f1480c9f Mon Sep 17 00:00:00 2001 From: Jay Bosamiya Date: Mon, 1 Apr 2024 19:22:00 -0400 Subject: [PATCH 5/5] Update CHANGELOG --- CHANGELOG.md | 3 +++ 1 file changed, 3 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index c448e62..a121bcd 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,5 +1,8 @@ # Unreleased +* Improve handling of `rustfmt.toml` for non-`verus!` code + - Rather than picking up `rustfmt.toml` based on working directory, it is now picked up based on the file being formatted. This now matches the search that `rustfmt` itself does. + # v0.2.10 * Add support for `broadcast proof`, `broadcast group`, and `broadcast use` (see [verus#1022](https://github.com/verus-lang/verus/pull/1022))