diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 04fe7365c..4ff3ec9a5 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -10,19 +10,17 @@ Follow the instructions provided in the [README](./README.md). This will provide The UI tests are used to validate the translation of Creusot. They can be found in `creusot/tests/should_fail` and `creusot/tests/should_suceed`. Ideally, each test includes a comment specifying the property or feature being checked. -To validate the translation one can run `cargo test --test ui`, or to run only a subset of tests run `cargo test --test ui -- "string-pattern"`. +To validate the translation one can run `cargo test --test ui`, or to run only a subset of tests run `cargo test --test ui "pattern"`. ## 2.2. Updating UI tests -If you have made changes to the Creusot translation and the UI tests show a diff you believe to be legitimate, you can tell Creusot to record the new output using `cargo test --test ui -- "pattern" --bless`. +If you have made changes to the Creusot translation and the UI tests show a diff you believe to be legitimate, you can tell Creusot to record the new output using `cargo test --test ui "pattern" -- --bless`. When contributing or updating tests, we ask that you minimize avoidable warnings, in particular, top-level declarations should be marked public, and unused arguments removed or replaced by wildcards. The warnings and errors of each test are recorded in an accompanying `stderr` file if any were present. -## 2.3. Testing `creusot-contracts` - -There is one special test used for the `creusot-contracts` crate, that can be run with `cargo test --test creusot-contracts`. - -The corresponding coma file is located at `creusot/tests/creusot-contracts/creusot-contracts.coma`. It can be updated with the `--bless` flag: `cargo test --test creusot-contracts -- --bless`. +The `ui` test also runs the Creusot translation on `creusot-contracts`. +The result is located at `creusot/tests/creusot-contracts/creusot-contracts.coma`. +To run the translation only on `creusot-contracts`, use a pattern that matches nothing, like `cargo test --test ui qq` # 3. Verifying proofs diff --git a/creusot/Cargo.toml b/creusot/Cargo.toml index d1ce064ef..9b8b9e122 100644 --- a/creusot/Cargo.toml +++ b/creusot/Cargo.toml @@ -40,10 +40,6 @@ libc = "0.2" name = "ui" harness = false -[[test]] -name = "creusot-contracts" -harness = false - [package.metadata.rust-analyzer] rustc_private = true diff --git a/creusot/tests/creusot-contracts.rs b/creusot/tests/creusot-contracts.rs deleted file mode 100644 index cf944d8ff..000000000 --- a/creusot/tests/creusot-contracts.rs +++ /dev/null @@ -1,122 +0,0 @@ -use clap::Parser; -use std::{ - env, - io::{IsTerminal, Write as _}, - path::PathBuf, -}; -use termcolor::{BufferWriter, Color, ColorChoice, ColorSpec, StandardStream, WriteColor as _}; - -mod diff; -use diff::differ; - -#[derive(Debug, Parser)] -struct Args { - /// Force color output - #[clap(long)] - force_color: bool, - /// Overwrite expected output files with actual output - #[clap(long)] - bless: bool, - /// Only run tests which contain this string - filter: Option, -} - -fn main() { - let mut args = Args::parse(); - if env::var("CI").is_ok() { - args.force_color = true; - } - // Build creusot-rustc to make it available to cargo-creusot - let creusot_rustc = escargot::CargoBuild::new() - .bin("creusot-rustc") - .current_release() - .manifest_path("../creusot-rustc/Cargo.toml") - .current_target() - .run() - .unwrap(); - let mut cargo_creusot = escargot::CargoBuild::new() - .bin("cargo-creusot") - .current_release() - .manifest_path("../cargo-creusot/Cargo.toml") - .current_target() - .run() - .unwrap() - .command(); - let mut base_path = PathBuf::from(env!("CARGO_MANIFEST_DIR")); - base_path.pop(); - - std::process::Command::new("touch") - .current_dir(&base_path) - .args(["creusot-contracts/src/lib.rs"]) - .status() - .unwrap(); - cargo_creusot.current_dir(&base_path).args([ - "creusot", - "--creusot-rustc", - creusot_rustc.path().to_str().unwrap(), - "--stdout", - "--export-metadata=false", - "--span-mode=relative", - "--spans-relative-to=creusot/tests/creusot-contracts", - "--", - "--package", - "creusot-contracts", - ]); - - let is_tty = std::io::stdout().is_terminal(); - let mut out = StandardStream::stdout(if args.force_color || is_tty { - ColorChoice::Always - } else { - ColorChoice::Never - }); - - write!(out, "Testing creusot-contracts ... ").unwrap(); - out.flush().unwrap(); - - let output = cargo_creusot.output().unwrap(); - let stdout = PathBuf::from("tests/creusot-contracts/creusot-contracts.coma"); - - let mut failed = false; - if args.bless { - if output.stdout.is_empty() { - panic!( - "creusot-contracts should have an output! stderr is:\n\n{}", - std::str::from_utf8(&output.stderr).unwrap() - ) - } - out.set_color(ColorSpec::new().set_fg(Some(Color::Blue))).unwrap(); - writeln!(&mut out, "blessed").unwrap(); - out.reset().unwrap(); - let (success, _) = differ(output.clone(), &stdout, None, true, is_tty).unwrap(); - - if !success { - out.set_color(ColorSpec::new().set_fg(Some(Color::Red))).unwrap(); - writeln!(&mut out, "failure").unwrap(); - out.reset().unwrap(); - } - - std::fs::write(stdout, &output.stdout).unwrap(); - } else { - let (success, buf) = differ(output.clone(), &stdout, None, true, is_tty).unwrap(); - - if success { - out.set_color(ColorSpec::new().set_fg(Some(Color::Green))).unwrap(); - writeln!(&mut out, "ok").unwrap(); - } else { - out.set_color(ColorSpec::new().set_fg(Some(Color::Red))).unwrap(); - writeln!(&mut out, "failure").unwrap(); - - failed = true; - }; - out.reset().unwrap(); - - let wrt = BufferWriter::stdout(ColorChoice::Always); - wrt.print(&buf).unwrap(); - } - - if failed { - out.set_color(ColorSpec::new().set_fg(Some(Color::Red))).unwrap(); - drop(out); - panic!("output of creusot-contracts failed"); - } -} diff --git a/creusot/tests/ui.rs b/creusot/tests/ui.rs index b31fdc681..978aa1db4 100644 --- a/creusot/tests/ui.rs +++ b/creusot/tests/ui.rs @@ -43,8 +43,13 @@ struct Args { } fn main() { - // Build `creusot-rustc` and `cargo-creusot` + let mut args = Args::parse(); + if env::var("CI").is_ok() { + args.quiet = true; + args.force_color = true; + } + println! {"Building creusot-rustc..."}; let creusot_rustc = escargot::CargoBuild::new() .bin("creusot-rustc") .current_release() @@ -52,15 +57,7 @@ fn main() { .current_target() .run() .unwrap(); - - let cargo_creusot = escargot::CargoBuild::new() - .bin("cargo-creusot") - .current_release() - .manifest_path("../cargo-creusot/Cargo.toml") - .current_target() - .run() - .unwrap() - .command(); + let creusot_rustc = creusot_rustc.path(); let mut base_path = PathBuf::from(env!("CARGO_MANIFEST_DIR")); base_path.pop(); @@ -71,37 +68,114 @@ fn main() { temp_file.push("debug"); temp_file.push("libcreusot_contracts.cmeta"); - let mut metadata_file = cargo_creusot; - metadata_file.current_dir(base_path); - metadata_file.arg("creusot").args(&[ - "--creusot-rustc".as_ref(), - creusot_rustc.path().as_os_str(), - "--metadata-path".as_ref(), - temp_file.as_os_str(), - "--output-file=/dev/null".as_ref(), - ]); - metadata_file.args(&["--", "--package", "creusot-contracts"]).env("CREUSOT_CONTINUE", "true"); - - if !metadata_file.status().expect("could not dump metadata for `creusot_contracts`").success() { - std::process::exit(1); - } - - let mut args = Args::parse(); - if env::var("CI").is_ok() { - args.quiet = true; - args.force_color = true; - } + translate_creusot_contracts(&args, creusot_rustc, &base_path, &temp_file); should_fail("tests/should_fail/**/*.rs", &args, |p| { - run_creusot(creusot_rustc.path(), p, &temp_file.to_string_lossy()) + run_creusot(creusot_rustc, p, &temp_file.to_string_lossy()) }); should_succeed("tests/should_succeed/**/*.rs", &args, |p| { - run_creusot(creusot_rustc.path(), p, &temp_file.to_string_lossy()) + run_creusot(creusot_rustc, p, &temp_file.to_string_lossy()) }); println!("All tests passed!"); } +fn translate_creusot_contracts( + args: &Args, + creusot_rustc: &Path, + base_path: &PathBuf, + temp_file: &PathBuf, +) { + println! {"Building cargo-creusot..."}; + let cargo_creusot = escargot::CargoBuild::new() + .bin("cargo-creusot") + .current_release() + .manifest_path("../cargo-creusot/Cargo.toml") + .current_target() + .run() + .unwrap() + .command(); + + print! {"Translating creusot-contracts... "}; + std::io::stdout().flush().unwrap(); + std::process::Command::new("touch") + .current_dir(&base_path) + .args(["creusot-contracts/src/lib.rs"]) + .status() + .unwrap(); + let mut creusot_contracts = cargo_creusot; + creusot_contracts.current_dir(base_path); + creusot_contracts + .arg("creusot") + .args(&[ + "--creusot-rustc", + creusot_rustc.to_str().unwrap(), + "--metadata-path", + temp_file.to_str().unwrap(), + "--stdout", + "--span-mode=relative", + "--spans-relative-to=creusot/tests/creusot-contracts", + "--", + "--package", + "creusot-contracts", + ]) + .env("CREUSOT_CONTINUE", "true"); + + let output = creusot_contracts.output().expect("could not translate `creusot_contracts`"); + let expect = PathBuf::from("tests/creusot-contracts/creusot-contracts.coma"); + + let is_tty = std::io::stdout().is_terminal(); + let mut out = StandardStream::stdout(if args.force_color || is_tty { + ColorChoice::Always + } else { + ColorChoice::Never + }); + + let mut failed = false; + if args.bless { + if output.stdout.is_empty() { + panic!( + "creusot-contracts should have an output! stderr is:\n\n{}", + std::str::from_utf8(&output.stderr).unwrap() + ) + } + let (success, _) = differ(output.clone(), &expect, None, true, is_tty).unwrap(); + + if success { + out.set_color(ColorSpec::new().set_fg(Some(Color::Green))).unwrap(); + writeln!(&mut out, "unchanged").unwrap(); + out.reset().unwrap(); + } else { + out.set_color(ColorSpec::new().set_fg(Some(Color::Blue))).unwrap(); + writeln!(&mut out, "blessed").unwrap(); + out.reset().unwrap(); + std::fs::write(expect, &output.stdout).unwrap(); + } + } else { + let (success, buf) = differ(output.clone(), &expect, None, true, is_tty).unwrap(); + + if success { + out.set_color(ColorSpec::new().set_fg(Some(Color::Green))).unwrap(); + writeln!(&mut out, "ok").unwrap(); + } else { + out.set_color(ColorSpec::new().set_fg(Some(Color::Red))).unwrap(); + writeln!(&mut out, "failure").unwrap(); + + failed = true; + }; + out.reset().unwrap(); + + let wrt = BufferWriter::stdout(ColorChoice::Always); + wrt.print(&buf).unwrap(); + out.flush().unwrap(); + } + + if !output.status.success() || failed { + eprintln!("Translation of creusot-contracts failed"); + std::process::exit(1); + } +} + fn run_creusot( creusot_rustc: &Path, file: &Path,