Merge tests ui and creusot-contracts

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
 

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
 

creusot/tests/ui.rs

@@ -43,24 +43,21 @@ 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()
         .manifest_path("../creusot-rustc/Cargo.toml")
         .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,