From f69b1dc5bd716f24a2e49b8d7f6d56937e25f5fa Mon Sep 17 00:00:00 2001
From: Herman Venter <herman@endor.ai>
Date: Tue, 24 Oct 2023 11:12:52 -0700
Subject: [PATCH] Simplify features (#1245)

[itk] Fix download failure (#34533)

* [itk] Fix download failure

* update version

* remove port-version

* update version

---------

Co-authored-by: vzhli17 <v-zhli17@microsoft.com>
---
 .github/workflows/mirai_on_mirai.yml |   2 +-
 .github/workflows/rust.yml           |   2 +-
 Cargo.lock                           |   2 +-
 binaries/summary_store.tar           | Bin 2991104 -> 2999296 bytes
 checker/Cargo.toml                   |   6 +++---
 install_mirai.sh                     |   8 +++++++-
 validate.sh                          |  12 +++++++++---
 vcpkg                                |   2 +-
 8 files changed, 23 insertions(+), 11 deletions(-)

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 33538f78c06ceb4f3f5a96a6411b11fcc940980d..708acb1424b37cfe6d8c4daa1dbe7e5614356e63 100644
GIT binary patch
delta 1989
zcmd7TO-~a+90u^6+HP&ZQl%78(5WwoFCAyLv$O4iLm?_87%dQ^r)Fu_gh*Rxs{t>N
zc)*K?N&+14V7PfTk+0yz#Bbn7&~H$mE|r3*#2el8muxrPbe}%|nXY~PLe}2ykv^7X
zm6wHrU0%sns-?2SDhp1&78|ee?pmG>7&1YHG=*tdN^wcKu(&Wa%H5B|HVCOR%@_4+
z9!+~_=jfvu`jj@0#x*Sf1}s72{cbHb98S;9PUF0B?85fO(qR9{HqN><tuI$9Fne)v
z!C{N#(krKE7juqAJleNN_~*PHExO+<Yy9vlI`r6Ho^b5EQ@;DJJYF}C;79Wq+>{B8
zF1PZmCO9or=L^oLP^qL)Ns&^_5=yC*OeTY-MW-gm($nJ;lTYrkWxHA}vv!X>n$Aq7
zUr%Q;mhs}j{ele26rI6MQ_qgO2{{9Qf(F|q74JQfT4W`B(1%hcp5NSm{?CN;5<kn%
zEtKXe?j^l#iv|}$bzY0e*3&Ao86w@jH=(5buig@7vNL*n*DB4jOg#MI(!4C2pK}`v
zY~^?2f3G~VvGOG69oboTt1~ylR&FOA8!(P6H3Tq(Ffeq-FExwFgyJa-XzJvbnzvb*
z`|BGVl{NRhH^jG2d;~mj3cS#`rh^|&LjZ!%1>JB4LeK+YI1A^X7b4IHQRs*BFaQ_e
zA`HS1T!PD6#7FC)PapmB_4<!Gj@9qK)<Zgl7+is?a1E}*Fx-F<xCyu5Hr&|@>2ZBi
zXW3k-_}m>nf4kvxw|y&N9mMaLZ66y(s5N~1DaM)+j*K577(y!ia~(f^`#U}U6S#Te
X<F~mJKfGm_jm6WPzdiCHUe|vEju8VK

delta 337
zcmZ9|O-{mK5XNywp@L#TsQ5)ot0G@EX>H4U0PjS?N{kEKxBwD42#MX`&IPwH-ogFr
zpJ>21$#3=K$z*2ul*(}VDwEuEDY{ir61hRx>&5Ywn~c4?ap27*Uy-R*9&B=@;^co`
z`^{teDpcgbPybQuk=TN5>>z_I4D2F@Jod1U0uErJh!PG_Mg<m*P{lD$aEddWqlVQ^
z2lbiQt~NjW?-{K>G;{y(H8LF+9xiZ+D>QJ8CR%8tgD!4T)A5a$nYHl$J|YR#`p{I~
Hd~JLK;fPSs

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