From 602cc905f026d9cc3aa4c0591d409ba659d1d83e Mon Sep 17 00:00:00 2001 From: coord_e Date: Mon, 21 Sep 2026 16:41:29 +0900 Subject: [PATCH] Document Cargo usage and add integration tests --- README.md | 39 ++++++++++++++++++++++++++ tests/cargo.rs | 38 +++++++++++++++++++++++++ tests/cargo/fail/Cargo.lock | 7 +++++ tests/cargo/fail/Cargo.toml | 6 ++++ tests/cargo/fail/src/arithmetic.rs | 3 ++ tests/cargo/fail/src/arithmetic/add.rs | 3 ++ tests/cargo/fail/src/main.rs | 5 ++++ tests/cargo/pass/Cargo.lock | 7 +++++ tests/cargo/pass/Cargo.toml | 6 ++++ tests/cargo/pass/src/arithmetic.rs | 3 ++ tests/cargo/pass/src/arithmetic/add.rs | 3 ++ tests/cargo/pass/src/main.rs | 5 ++++ 12 files changed, 125 insertions(+) create mode 100644 tests/cargo.rs create mode 100644 tests/cargo/fail/Cargo.lock create mode 100644 tests/cargo/fail/Cargo.toml create mode 100644 tests/cargo/fail/src/arithmetic.rs create mode 100644 tests/cargo/fail/src/arithmetic/add.rs create mode 100644 tests/cargo/fail/src/main.rs create mode 100644 tests/cargo/pass/Cargo.lock create mode 100644 tests/cargo/pass/Cargo.toml create mode 100644 tests/cargo/pass/src/arithmetic.rs create mode 100644 tests/cargo/pass/src/arithmetic/add.rs create mode 100644 tests/cargo/pass/src/main.rs diff --git a/README.md b/README.md index ab3aaf59..378440b1 100644 --- a/README.md +++ b/README.md @@ -66,6 +66,45 @@ safe Integration test examples are located under `tests/ui/` and can be executed using `cargo test`. You can review these examples to understand what the current Thrust implementation can handle. +### Using Thrust with Cargo + +Thrust can check Cargo projects that have no dependencies. External crates are not supported yet (#255). + +First, build Thrust in its source directory: + +```sh +cargo build --bin thrust-rustc +``` + +Set up a project using the same Rust toolchain as Thrust (currently `nightly-2025-09-08`): + +```sh +cargo +nightly-2025-09-08 new --edition 2021 thrust-example +cd thrust-example +``` + +Add assertions to your code. For example, write the following in `src/main.rs`: + +```rust +fn add(x: i64, y: i64) -> i64 { + x + y +} + +fn main() { + assert!(add(1, 2) == 3); +} +``` + +With Z3 on your `PATH`, set `RUSTC` to the absolute path of the built `thrust-rustc` binary and run: + +```sh +RUSTC=/absolute/path/to/thrust/target/debug/thrust-rustc \ +RUSTFLAGS='-C debug-assertions=false' \ +cargo +nightly-2025-09-08 check +``` + +For the example above, the check succeeds. Changing the assertion to `add(1, 2) == 2` makes it fail with `verification error: Unsat` and a nonzero exit status. + ## Annotation Thrust can verify a wide range of programs without explicit annotations, but you can use `#[thrust_macros::requires(expr)]` and `#[thrust_macros::ensures(expr)]` to annotate the precondition and postcondition of a function, aiding in verification or specifying the intended behavior. Here, `expr` is an ordinary Rust expression that Thrust interprets as a logical formula. It supports the usual integer, boolean, and comparison operators, calls to functions declared with `#[thrust_macros::predicate]`, and the model operations described below. diff --git a/tests/cargo.rs b/tests/cargo.rs new file mode 100644 index 00000000..60e87c44 --- /dev/null +++ b/tests/cargo.rs @@ -0,0 +1,38 @@ +use std::process::{Command, Output}; + +fn cargo_check(fixture: &str) -> Output { + let target_dir = tempfile::tempdir().unwrap(); + let fixture = std::path::Path::new(env!("CARGO_MANIFEST_DIR")) + .join("tests/cargo") + .join(fixture); + Command::new(env!("CARGO")) + .args(["check", "--offline", "--locked", "--manifest-path"]) + .arg(fixture.join("Cargo.toml")) + .env("RUSTC", env!("CARGO_BIN_EXE_thrust-rustc")) + .env("RUSTFLAGS", "-C debug-assertions=false") + .env("CARGO_TARGET_DIR", target_dir.path()) + .env_remove("CARGO_ENCODED_RUSTFLAGS") + .env_remove("RUSTC_WRAPPER") + .env_remove("RUSTC_WORKSPACE_WRAPPER") + .env_remove("THRUST_OUTPUT_DIR") + .output() + .unwrap() +} + +#[test] +fn cargo_check_passes_verification() { + let output = cargo_check("pass"); + assert!( + output.status.success(), + "{}", + String::from_utf8_lossy(&output.stderr) + ); +} + +#[test] +fn cargo_check_reports_verification_failure() { + let output = cargo_check("fail"); + let stderr = String::from_utf8_lossy(&output.stderr); + assert!(!output.status.success(), "{stderr}"); + assert!(stderr.contains("verification error: Unsat"), "{stderr}"); +} diff --git a/tests/cargo/fail/Cargo.lock b/tests/cargo/fail/Cargo.lock new file mode 100644 index 00000000..435d4136 --- /dev/null +++ b/tests/cargo/fail/Cargo.lock @@ -0,0 +1,7 @@ +# This file is automatically @generated by Cargo. +# It is not intended for manual editing. +version = 4 + +[[package]] +name = "thrust-cargo-test" +version = "0.1.0" diff --git a/tests/cargo/fail/Cargo.toml b/tests/cargo/fail/Cargo.toml new file mode 100644 index 00000000..f7eb0cca --- /dev/null +++ b/tests/cargo/fail/Cargo.toml @@ -0,0 +1,6 @@ +[package] +name = "thrust-cargo-test" +version = "0.1.0" +edition = "2021" + +[workspace] diff --git a/tests/cargo/fail/src/arithmetic.rs b/tests/cargo/fail/src/arithmetic.rs new file mode 100644 index 00000000..9ed69308 --- /dev/null +++ b/tests/cargo/fail/src/arithmetic.rs @@ -0,0 +1,3 @@ +mod add; + +pub use add::add; diff --git a/tests/cargo/fail/src/arithmetic/add.rs b/tests/cargo/fail/src/arithmetic/add.rs new file mode 100644 index 00000000..af42cc23 --- /dev/null +++ b/tests/cargo/fail/src/arithmetic/add.rs @@ -0,0 +1,3 @@ +pub fn add(x: i64, y: i64) -> i64 { + x + y +} diff --git a/tests/cargo/fail/src/main.rs b/tests/cargo/fail/src/main.rs new file mode 100644 index 00000000..a0cd6a9e --- /dev/null +++ b/tests/cargo/fail/src/main.rs @@ -0,0 +1,5 @@ +mod arithmetic; + +fn main() { + assert!(arithmetic::add(1, 2) == 2); +} diff --git a/tests/cargo/pass/Cargo.lock b/tests/cargo/pass/Cargo.lock new file mode 100644 index 00000000..435d4136 --- /dev/null +++ b/tests/cargo/pass/Cargo.lock @@ -0,0 +1,7 @@ +# This file is automatically @generated by Cargo. +# It is not intended for manual editing. +version = 4 + +[[package]] +name = "thrust-cargo-test" +version = "0.1.0" diff --git a/tests/cargo/pass/Cargo.toml b/tests/cargo/pass/Cargo.toml new file mode 100644 index 00000000..f7eb0cca --- /dev/null +++ b/tests/cargo/pass/Cargo.toml @@ -0,0 +1,6 @@ +[package] +name = "thrust-cargo-test" +version = "0.1.0" +edition = "2021" + +[workspace] diff --git a/tests/cargo/pass/src/arithmetic.rs b/tests/cargo/pass/src/arithmetic.rs new file mode 100644 index 00000000..9ed69308 --- /dev/null +++ b/tests/cargo/pass/src/arithmetic.rs @@ -0,0 +1,3 @@ +mod add; + +pub use add::add; diff --git a/tests/cargo/pass/src/arithmetic/add.rs b/tests/cargo/pass/src/arithmetic/add.rs new file mode 100644 index 00000000..af42cc23 --- /dev/null +++ b/tests/cargo/pass/src/arithmetic/add.rs @@ -0,0 +1,3 @@ +pub fn add(x: i64, y: i64) -> i64 { + x + y +} diff --git a/tests/cargo/pass/src/main.rs b/tests/cargo/pass/src/main.rs new file mode 100644 index 00000000..d51bbcfd --- /dev/null +++ b/tests/cargo/pass/src/main.rs @@ -0,0 +1,5 @@ +mod arithmetic; + +fn main() { + assert!(arithmetic::add(1, 2) == 3); +}