diff --git a/.github/workflows/mirai_on_mirai.yml b/.github/workflows/mirai_on_mirai.yml index 8cf42ca4..ce9074fe 100644 --- a/.github/workflows/mirai_on_mirai.yml +++ b/.github/workflows/mirai_on_mirai.yml @@ -50,7 +50,7 @@ jobs: extra-args: --clean-buildtrees-after-build - name: Install MIRAI run: | - cargo install --force --path ./checker --no-default-features --features="z3, use-vcpkg-z3" + cargo install --force --path ./checker --no-default-features --features=vcpkg - name: Run MIRAI on MIRAI run: | cargo mirai --no-default-features \ No newline at end of file diff --git a/.github/workflows/rust.yml b/.github/workflows/rust.yml index 2bf16bc7..9ff2819f 100644 --- a/.github/workflows/rust.yml +++ b/.github/workflows/rust.yml @@ -39,7 +39,7 @@ jobs: - name: Execute tests run: | - cargo test --all --no-default-features --features="z3, use-vcpkg-z3" -- --test-threads=1 + cargo test --all --no-default-features --features=vcpkg -- --test-threads=1 env: CARGO_INCREMENTAL: 0 RUSTFLAGS: "-Zprofile -Ccodegen-units=1 -Copt-level=0 -Clink-dead-code -Coverflow-checks=off -Zpanic_abort_tests" diff --git a/Cargo.lock b/Cargo.lock index b1b5d4a5..1d7d51d1 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -1206,7 +1206,7 @@ dependencies = [ [[package]] name = "z3-sys" version = "0.8.1" -source = "git+https://github.com/prove-rs/z3.rs.git#1335297b447a281ba90497481865e31b48c40508" +source = "git+https://github.com/prove-rs/z3.rs.git#8eea45394f314eb0c26697e095d68cc00d8bcb90" dependencies = [ "bindgen", "cmake", diff --git a/binaries/summary_store.tar b/binaries/summary_store.tar index 33538f78..708acb14 100644 Binary files a/binaries/summary_store.tar and b/binaries/summary_store.tar differ diff --git a/checker/Cargo.toml b/checker/Cargo.toml index 431995fa..4050cc23 100644 --- a/checker/Cargo.toml +++ b/checker/Cargo.toml @@ -64,8 +64,8 @@ walkdir = "*" contracts = { version = "0.6.0", features = ["mirai_assertions"] } [features] -default = ["z3", "static-link-z3"] -use-vcpkg-z3 = ["z3-sys/vcpkg"] -static-link-z3 = ["z3-sys/static-link-z3"] +default = ["static-link"] +vcpkg = ["z3-sys/vcpkg", "z3"] +static-link = ["z3-sys/static-link-z3", "z3"] z3 = [] diff --git a/install_mirai.sh b/install_mirai.sh index 6256575a..1c447269 100755 --- a/install_mirai.sh +++ b/install_mirai.sh @@ -12,5 +12,11 @@ set -e #install mirai into cargo cargo uninstall -q mirai || true touch checker/src/lib.rs -cargo install --locked --path ./checker + +# Check if dynamic link to vcpkg installed Z3 is wanted rather than static linking +if [ "$1" == "vcpkg" ]; then + cargo install --locked --path ./checker --no-default-features --features=vcpkg +else + cargo install --locked --path ./checker +fi diff --git a/validate.sh b/validate.sh index 4c68287a..b6a55052 100755 --- a/validate.sh +++ b/validate.sh @@ -6,6 +6,12 @@ # Exit immediately if a command exits with a non-zero status. set -e + +# Check if dynamic link to vcpkg installed Z3 is wanted rather than static linking +if [ "$1" == "vcpkg" ]; then + FLAGS='--no-default-features --features=vcpkg' +fi + # start clean cargo clean cargo update @@ -30,12 +36,12 @@ cd ../../.. # Run cargo test, starting clean so that the new summary store is used. cargo clean -cargo build --tests -time cargo test +cargo build --tests $FLAGS +time cargo test $FLAGS # Install MIRAI into cargo so that we can use optimized binaries to analyze debug binaries built with special flags cargo uninstall mirai || true -cargo install --path ./checker +cargo install --path ./checker $FLAGS # Run mirai on itself, using the optimized build in cargo as the bootstrap. cargo clean -p mirai diff --git a/vcpkg b/vcpkg index 830f86fb..3265c187 160000 --- a/vcpkg +++ b/vcpkg @@ -1 +1 @@ -Subproject commit 830f86fb309ad7167468a433a890b7415fbb90a5 +Subproject commit 3265c187c74914aa5569b75355badebfdbab7987