From aac396b3ba0ce23484125f6218c1fe2adeeadc90 Mon Sep 17 00:00:00 2001
From: Herman Venter <herman@endor.ai>
Date: Mon, 23 Oct 2023 23:35:48 -0700
Subject: [PATCH] Make simplification with TOP more aggressive (#1244)

---
 .github/workflows/mirai_on_mirai.yml |  56 +++++++++++++++++++++++++++
 .github/workflows/rust.yml           |  48 ++++++++---------------
 .gitmodules                          |   3 ++
 Cargo.lock                           |  38 ++++++++++--------
 binaries/summary_store.tar           | Bin 2999296 -> 2991104 bytes
 checker/Cargo.toml                   |   9 +++--
 checker/src/abstract_value.rs        |   6 ++-
 checker/src/body_visitor.rs          |   3 +-
 checker/src/path.rs                  |   7 ++++
 checker/src/type_visitor.rs          |   1 +
 checker/tests/run-pass/transmute.rs  |   2 +-
 vcpkg                                |   1 +
 12 files changed, 120 insertions(+), 54 deletions(-)
 create mode 100644 .github/workflows/mirai_on_mirai.yml
 create mode 100644 .gitmodules
 create mode 160000 vcpkg

diff --git a/.github/workflows/mirai_on_mirai.yml b/.github/workflows/mirai_on_mirai.yml
new file mode 100644
index 00000000..8cf42ca4
--- /dev/null
+++ b/.github/workflows/mirai_on_mirai.yml
@@ -0,0 +1,56 @@
+name: MIRAI on MIRAI
+
+on:
+  push:
+    branches: [ main ]
+  pull_request:
+    branches: [ main ]
+
+jobs:
+  build_with_vcpkg_installed_z3:
+    strategy:
+      matrix:
+        build: [macos, windows] #[linux, macos, windows]
+        include:
+#          - build: linux
+#            os: ubuntu-latest
+#            vcpkg_triplet: x64-linux
+          - build: macos
+            os: macos-latest
+            vcpkg_triplet: x64-osx
+          - build: windows
+            os: windows-latest
+            vcpkg_triplet: x64-windows-static-md
+    runs-on: ${{ matrix.os }}
+    env:
+      VCPKG_ROOT: ${{ github.workspace }}/vcpkg
+    steps:
+      - uses: actions/checkout@v3
+        with:
+          submodules: recursive
+      - name: Install LLVM and Clang # required for bindgen to work, see https://github.com/rust-lang/rust-bindgen/issues/1797
+        uses: KyleMayes/install-llvm-action@v1
+        if: matrix.os == 'windows-latest'
+        with:
+          version: "11.0"
+          directory: ${{ runner.temp }}/llvm
+      - name: Set LIBCLANG_PATH
+        run: echo "LIBCLANG_PATH=$((gcm clang).source -replace "clang.exe")" >> $env:GITHUB_ENV
+        if: matrix.os == 'windows-latest'
+      - run: echo  Installing z3:${{ matrix.vcpkg_triplet }} on ${{ matrix.os }}.
+      - name: vcpkg build z3
+        uses: johnwason/vcpkg-action@v5
+        id: vcpkg
+        with:
+          pkgs: z3
+          triplet: ${{ matrix.vcpkg_triplet }}
+          cache-key: ${{ matrix.os }}
+          revision: master
+          token: ${{ github.token }}
+          extra-args: --clean-buildtrees-after-build
+      - name: Install MIRAI
+        run: |
+          cargo install --force --path ./checker --no-default-features  --features="z3, use-vcpkg-z3"
+      - 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 3eba341f..2bf16bc7 100644
--- a/.github/workflows/rust.yml
+++ b/.github/workflows/rust.yml
@@ -18,13 +18,28 @@ jobs:
 
   tests:
     runs-on: macos-latest
+    env:
+      VCPKG_ROOT: ${{ github.workspace }}/vcpkg
 
     steps:
       - uses: actions/checkout@v3.5.2
+        with:
+          submodules: recursive
+
+      - name: vcpkg build z3
+        uses: johnwason/vcpkg-action@v5
+        id: vcpkg
+        with:
+          pkgs: z3
+          triplet: x64-osx
+          cache-key: macos-latest
+          revision: master
+          token: ${{ github.token }}
+          extra-args: --clean-buildtrees-after-build
 
       - name: Execute tests
         run: |
-          cargo test --all -- --test-threads=1
+          cargo test --all --no-default-features --features="z3, use-vcpkg-z3" -- --test-threads=1
         env:
           CARGO_INCREMENTAL: 0
           RUSTFLAGS: "-Zprofile -Ccodegen-units=1 -Copt-level=0 -Clink-dead-code -Coverflow-checks=off -Zpanic_abort_tests"
@@ -44,20 +59,6 @@ jobs:
           token: ${{ secrets.CODECOV_TOKEN }}
           files: "lcov.info"
 
-  mirai_on_mirai_macos:
-    runs-on: macos-latest
-
-    steps:
-      - uses: actions/checkout@v3.5.2
-
-      - name: Install MIRAI
-        run: |
-          cargo install --force --path ./checker --no-default-features
-
-      - name: Run MIRAI on MIRAI
-        run: |
-          cargo mirai --no-default-features
-
   mirai_on_mirai_ubuntu:
     runs-on: ubuntu-latest
 
@@ -70,19 +71,4 @@ jobs:
 
       - name: Run MIRAI on MIRAI
         run: |
-          cargo mirai --no-default-features
-
-  mirai_on_mirai_windows:
-    runs-on: windows-latest
-
-    steps:
-      - uses: actions/checkout@v3.5.2
-
-      - name: Install MIRAI
-        run: |
-          cargo install --force --path ./checker
-
-      - name: Run MIRAI on MIRAI
-        run: |
-          cargo mirai --no-default-features
-
+          cargo mirai --no-default-features
\ No newline at end of file
diff --git a/.gitmodules b/.gitmodules
new file mode 100644
index 00000000..53e4058e
--- /dev/null
+++ b/.gitmodules
@@ -0,0 +1,3 @@
+[submodule "vcpkg"]
+	path = vcpkg
+	url = git@github.com:microsoft/vcpkg.git
diff --git a/Cargo.lock b/Cargo.lock
index 437233f3..b1b5d4a5 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -421,9 +421,9 @@ checksum = "d2fabcfbdc87f4758337ca535fb41a6d701b65693ce38287d856d1674551ec9b"
 
 [[package]]
 name = "hashbrown"
-version = "0.14.1"
+version = "0.14.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "7dfda62a12f55daeae5015f81b0baea145391cb4520f86c248fc615d72640d12"
+checksum = "f93e7192158dbcda357bdec5fb5788eebf8bbac027f3f33e719d29135ae84156"
 
 [[package]]
 name = "hermit-abi"
@@ -524,9 +524,9 @@ checksum = "da2479e8c062e40bf0066ffa0bc823de0a9368974af99c9f6df941d2c231e03f"
 
 [[package]]
 name = "lock_api"
-version = "0.4.10"
+version = "0.4.11"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "c1cc9717a20b1bb222f333e6a92fd32f7d8a18ddc5a3191a11af45dcbf4dcd16"
+checksum = "3c168f8615b12bc01f9c17e2eb0cc07dcae1940121185446edc3744920e8ef45"
 dependencies = [
  "autocfg",
  "scopeguard",
@@ -758,9 +758,9 @@ dependencies = [
 
 [[package]]
 name = "regex"
-version = "1.10.1"
+version = "1.10.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "aaac441002f822bc9705a681810a4dd2963094b9ca0ddc41cb963a4c189189ea"
+checksum = "380b951a9c5e80ddfd6136919eef32310721aa4aacd4889a8d39124b026ab343"
 dependencies = [
  "aho-corasick",
  "memchr",
@@ -770,9 +770,9 @@ dependencies = [
 
 [[package]]
 name = "regex-automata"
-version = "0.4.2"
+version = "0.4.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "5011c7e263a695dc8ca064cddb722af1be54e517a280b12a5356f98366899e5d"
+checksum = "5f804c7828047e88b2d32e2d7fe5a105da8ee3264f01902f796c8e067dc2483f"
 dependencies = [
  "aho-corasick",
  "memchr",
@@ -809,9 +809,9 @@ checksum = "8ba09476327c4b70ccefb6180f046ef588c26a24cf5d269a9feba316eb4f029f"
 
 [[package]]
 name = "rustix"
-version = "0.38.19"
+version = "0.38.20"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "745ecfa778e66b2b63c88a61cb36e0eea109e803b0b86bf9879fbc77c70e86ed"
+checksum = "67ce50cb2e16c2903e30d1cbccfd8387a74b9d4c938b6a4c5ec6cc7556f7a8a0"
 dependencies = [
  "bitflags 2.4.1",
  "errno",
@@ -1016,18 +1016,18 @@ dependencies = [
 
 [[package]]
 name = "thiserror"
-version = "1.0.49"
+version = "1.0.50"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "1177e8c6d7ede7afde3585fd2513e611227efd6481bd78d2e82ba1ce16557ed4"
+checksum = "f9a7210f5c9a7156bb50aa36aed4c95afb51df0df00713949448cf9e97d382d2"
 dependencies = [
  "thiserror-impl",
 ]
 
 [[package]]
 name = "thiserror-impl"
-version = "1.0.49"
+version = "1.0.50"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "10712f02019e9288794769fba95cd6847df9874d49d871d062172f9dd41bc4cc"
+checksum = "266b2e40bc00e5a6c09c3584011e08b06f123c00362c92b975ba9843aaaa14b8"
 dependencies = [
  "proc-macro2",
  "quote",
@@ -1068,6 +1068,12 @@ version = "0.2.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "711b9620af191e0cdc7468a8d14e709c3dcdb115b36f838e601583af800a370a"
 
+[[package]]
+name = "vcpkg"
+version = "0.2.15"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "accd4ea62f7bb7a82fe23066fb0957d48ef677f6eeb8215f372f52e48bb32426"
+
 [[package]]
 name = "verification_status"
 version = "0.1.0"
@@ -1200,9 +1206,9 @@ dependencies = [
 [[package]]
 name = "z3-sys"
 version = "0.8.1"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "d7cf70fdbc0de3f42b404f49b0d4686a82562254ea29ff0a155eef2f5430f4b0"
+source = "git+https://github.com/prove-rs/z3.rs.git#1335297b447a281ba90497481865e31b48c40508"
 dependencies = [
  "bindgen",
  "cmake",
+ "vcpkg",
 ]
diff --git a/binaries/summary_store.tar b/binaries/summary_store.tar
index f0aa724ecb4f93ad397f1b96b86c27b685e9dedd..33538f78c06ceb4f3f5a96a6411b11fcc940980d 100644
GIT binary patch
delta 342
zcmZ9|%TB^j5XNyw3l;?{rQT_6z2BO&wukcoz7ugLgas_zpox7D6T8u!3*W-<4(^YC
zVj#pxe!DN<WTrPNrT6tFPxfO|Ww$z0S(v1qPM$A?Y8>5-ljv1yEqV6b`-Onkx%wYy
z&jL9OI@JV{zlMSML-7U6Sb>EKs#t}M8rHCmIvUu3gH1Hyq6H6I*v1Zav4?#eppEIy
z0EdP6p>ZbNPs^BZ!#wnVCPOC(5#b2OIKe5-aE=RH;tJQeDV-p$ycFJhJUeyzEUi*K
LKed#P*i?T3o()oy

delta 1994
zcmd7T%T5zf90u^2+D>gj3Q~$F=&2XPOONNAnK?rjEDBK}!6=t_SvAvkOo+6Fwwme&
zq6=K;qLKg$T=57d@(ONz0}~TpK;NK#ofcb6CGO~?zhpY;r1SOrpVRd(pVjrZ`|1Eq
z(&F=M)-JqE7EAepLyOB!rV^d1u<lBR3<*Og+%UP$EY3`mFfJ|2QV4TD65UkQDph<D
zzv5Apdv==KUm%Z3<EULz0w7=&YVY?d(b3+-;^I8cYsVh!Y_1Luj_u&AOHl^W`7E_p
zR+b&QQpmq>a&|85D5^*K8t(nMq(yS>Hyah!`ihJ^u*=hqopB1c{*}k;=Hcvc9>Gju
zDx}=Zv!*kWEiGl82`=N7!MPN1D!D0i5w~Q}w8-qtWMY15dgkG6TDD820&Vxm6N$N*
z#H;zaIZHgddnaoIjW}7rO|wsqx(PW02SJ1FlJXCpa3x&sYbiwP2w>I&d{WhZ)lZYD
z<$S8>UeemuC>Up~^J+x6P_xNKh(!D1(2M-9;+PQ9;2luhyO!20OUKi<w&tbDOv<e+
zu$|eB{k`@i)*kK=9a&m;votruc6v7!9TJBY8v+Q<Ii~K&#ilc=OH*>m#^cA|nfIVG
z_vhyloi(<;H>z(#^{L>26X1o~H4Xf55&{r}F6f3+&;udpg+4e9{Sbx$h`=D6fgv~x
z=U^B{;5=N|R(+%zdQ^J<t6KeD#j*DK+mDTqMj#3o;SyYiD=-RIVGORpb+`dH_d{CD
zx24f!I-h&$j-S8X_|>+4%M$!g{*KxDv1jx&$FH7ZvJv6X03w3mhJk;tBL}d)+w=Ii
bWXHd0Z0*JlCeUrbtgWBM1n#RJV^!@p4x9uY

diff --git a/checker/Cargo.toml b/checker/Cargo.toml
index 270bd1a8..431995fa 100644
--- a/checker/Cargo.toml
+++ b/checker/Cargo.toml
@@ -49,7 +49,7 @@ shellwords = "*"
 sled = "*"
 tar = "0.4.38"
 tempfile = "*"
-z3-sys = { version = "*", features = ["static-link-z3"], optional = true }
+z3-sys = { version = "*", git="https://github.com/prove-rs/z3.rs.git", optional = true }
 
 [dev-dependencies]
 walkdir = "*"
@@ -64,7 +64,8 @@ walkdir = "*"
 contracts = { version = "0.6.0", features = ["mirai_assertions"] }
 
 [features]
-default = ["z3"]
-z3 = ["dep:z3-sys"]
-
+default = ["z3", "static-link-z3"]
+use-vcpkg-z3 = ["z3-sys/vcpkg"]
+static-link-z3 = ["z3-sys/static-link-z3"]
+z3 = []
 
diff --git a/checker/src/abstract_value.rs b/checker/src/abstract_value.rs
index 854ca428..8037a9f5 100644
--- a/checker/src/abstract_value.rs
+++ b/checker/src/abstract_value.rs
@@ -3416,7 +3416,11 @@ impl AbstractValueTrait for Rc<AbstractValue> {
     /// True if all possible concrete values are elements of the set corresponding to this domain.
     #[logfn_inputs(TRACE)]
     fn is_top(&self) -> bool {
-        matches!(&self.expression, Expression::Top)
+        match &self.expression {
+            Expression::Top => true,
+            Expression::Variable { path, .. } => path.is_top(),
+            _ => false,
+        }
     }
 
     /// True if this value is an empty tuple, which is the sole value of the unit type.
diff --git a/checker/src/body_visitor.rs b/checker/src/body_visitor.rs
index 2febdab9..e19facc6 100644
--- a/checker/src/body_visitor.rs
+++ b/checker/src/body_visitor.rs
@@ -835,6 +835,7 @@ impl<'analysis, 'compilation, 'tcx> BodyVisitor<'analysis, 'compilation, 'tcx> {
             return environment;
         }
         trace!("def_id {:?}", self.tcx.def_kind(self.def_id));
+        let saved_type_visitor = self.type_visitor.clone();
         let saved_mir = self.mir;
         let saved_def_id = self.def_id;
         for (ordinal, constant_mir) in self.tcx.promoted_mir(self.def_id).iter().enumerate() {
@@ -917,7 +918,7 @@ impl<'analysis, 'compilation, 'tcx> BodyVisitor<'analysis, 'compilation, 'tcx> {
         }
         self.def_id = saved_def_id;
         self.mir = saved_mir;
-        self.type_visitor_mut().mir = saved_mir;
+        *self.type_visitor_mut() = saved_type_visitor;
         environment
     }
 
diff --git a/checker/src/path.rs b/checker/src/path.rs
index cdbc9510..ab3b6819 100644
--- a/checker/src/path.rs
+++ b/checker/src/path.rs
@@ -506,6 +506,13 @@ impl Path {
         }
     }
 
+    pub fn is_top(&self) -> bool {
+        match &self.value {
+            PathEnum::Computed { value } => value.is_top(),
+            _ => false,
+        }
+    }
+
     // Returns the length of the path.
     #[logfn_inputs(TRACE)]
     pub fn path_length(&self) -> usize {
diff --git a/checker/src/type_visitor.rs b/checker/src/type_visitor.rs
index b6624f43..4a67d9ca 100644
--- a/checker/src/type_visitor.rs
+++ b/checker/src/type_visitor.rs
@@ -73,6 +73,7 @@ impl<'tcx> TypeCache<'tcx> {
     }
 }
 
+#[derive(Clone)]
 pub struct TypeVisitor<'tcx> {
     pub actual_argument_types: Vec<Ty<'tcx>>,
     pub closures_being_specialized: RefCell<HashSet<DefId>>,
diff --git a/checker/tests/run-pass/transmute.rs b/checker/tests/run-pass/transmute.rs
index d0d27ac1..72fb9ebf 100644
--- a/checker/tests/run-pass/transmute.rs
+++ b/checker/tests/run-pass/transmute.rs
@@ -120,7 +120,7 @@ pub unsafe fn t6() {
     let arr_ptr = std::mem::transmute::<&[i32], *const [i32]>(arr_ref);
     let fat_ptr = std::mem::transmute::<*const [i32], FatPtr<i32>>(arr_ptr);
     verify!(fat_ptr.fat == 3);
-    verify!(*fat_ptr.ptr == 1);
+    verify!(*fat_ptr.ptr == 1); //~ possible false verification condition
 }
 
 pub unsafe fn t7() {
diff --git a/vcpkg b/vcpkg
new file mode 160000
index 00000000..830f86fb
--- /dev/null
+++ b/vcpkg
@@ -0,0 +1 @@
+Subproject commit 830f86fb309ad7167468a433a890b7415fbb90a5