Make simplification with TOP more aggressive (#1244)

.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

.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

.gitmodules

@@ -0,0 +1,3 @@
+[submodule "vcpkg"]
+	path = vcpkg
+	url = git@github.com:microsoft/vcpkg.git

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 = []
 

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.

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
     }
 

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 {

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>>,

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() {