Update to nightly-2024-12-03

.github/workflows/mirai_on_mirai.yml

@@ -53,4 +53,5 @@ jobs:
           cargo install --force --path ./checker --no-default-features --features=vcpkg
       - name: Run MIRAI on MIRAI
         run: |
-          cargo mirai --no-default-features
+          cargo mirai --no-default-features --features=vcpkg
+        if: matrix.os != 'windows-latest'

.github/workflows/rust.yml

@@ -42,22 +42,22 @@ jobs:
           cargo test --all -- --test-threads=1
         env:
           CARGO_INCREMENTAL: 0
-          RUSTFLAGS: "-Zprofile -Ccodegen-units=1 -Copt-level=0 -Clink-dead-code -Coverflow-checks=off -Zpanic_abort_tests"
+          RUSTFLAGS: "-Ccodegen-units=1 -Copt-level=0 -Clink-dead-code -Coverflow-checks=off -Zpanic_abort_tests"
 
-#      - name: Setup grcov
-#        run: |
-#          cargo install grcov
-#
-#      - name: Run grcov
-#        run: |
-#          zip -0 cov.zip $(find . -name "mirai*.gc*" -print)
-#          grcov cov.zip -s . -t lcov --llvm --ignore-not-existing --ignore "/*" -o lcov.info
-#
-#      - name: Upload coverage data to codecov.io
-#        uses: codecov/codecov-action@v3
-#        with:
-#          token: ${{ secrets.CODECOV_TOKEN }}
-#          files: "lcov.info"
+  #      - name: Setup grcov
+  #        run: |
+  #          cargo install grcov
+  #
+  #      - name: Run grcov
+  #        run: |
+  #          zip -0 cov.zip $(find . -name "mirai*.gc*" -print)
+  #          grcov cov.zip -s . -t lcov --llvm --ignore-not-existing --ignore "/*" -o lcov.info
+  #
+  #      - name: Upload coverage data to codecov.io
+  #        uses: codecov/codecov-action@v3
+  #        with:
+  #          token: ${{ secrets.CODECOV_TOKEN }}
+  #          files: "lcov.info"
 
   mirai_on_mirai_ubuntu:
     runs-on: ubuntu-latest

annotations/src/lib.rs

@@ -5,6 +5,8 @@
 
 // A set of macros and functions to use for annotating source files that are being checked with MIRAI
 
+#![allow(unexpected_cfgs)]
+
 /// Provides a way to specify a value that should be treated abstractly by the verifier.
 /// The concrete argument provides type information to the verifier and a meaning for
 /// the expression when compiled by the rust compiler.

checker/Cargo.toml

@@ -38,18 +38,19 @@ log = "*"
 log-derive = "*"
 mirai-annotations = { path = "../annotations" }
 petgraph = "*"
+proc-macro2 = "*"
 rand = "*"
 rayon = "*"
 regex = "*"
 rpds = { version = "*", features = ["serde"] }
 rustc_tools_util = "*"
-serde = { version = "=1.0.203", features = ["derive", "alloc", "rc"] }
+serde = { version = "*", features = ["derive", "alloc", "rc"] }
 serde_json = "*"
 shellwords = "*"
 sled = "*"
 tar = "*"
 tempfile = "*"
-z3-sys = { version = "*", git = "https://github.com/prove-rs/z3.rs.git", optional = true }
+z3-sys = { version = "*", git = "https://github.com/prove-rs/z3.rs.git", rev = "cb10013a2a0a017048b1d218bc734afa390f34ff", optional = true }
 
 [dev-dependencies]
 walkdir = "*"

checker/src/abstract_value.rs

@@ -762,6 +762,8 @@ pub trait AbstractValueTrait: Sized {
     #[must_use]
     fn cast(&self, target_type: ExpressionType) -> Self;
     #[must_use]
+    fn compare(&self, other: Self) -> Self;
+    #[must_use]
     fn conditional_expression(&self, consequent: Self, alternate: Self) -> Self;
     #[must_use]
     fn dereference(&self, target_type: ExpressionType) -> Self;
@@ -1797,6 +1799,17 @@ impl AbstractValueTrait for Rc<AbstractValue> {
             // [0 & y] -> 0
             return self.clone();
         }
+        if matches!(other.expression, Expression::Reference(..)) {
+            if let Expression::CompileTimeConstant(ConstantDomain::U128(1))
+            | Expression::CompileTimeConstant(ConstantDomain::U128(3))
+            | Expression::CompileTimeConstant(ConstantDomain::U128(7)) = self.expression
+            {
+                // [1 & (&y)] -> 0
+                // [3 & (&y)] -> 0
+                // [7 & (&y)] -> 0
+                return Rc::new(ConstantDomain::U128(0).into());
+            }
+        }
         // [x & x] -> x
         if self.eq(&other) {
             return other;
@@ -1987,6 +2000,18 @@ impl AbstractValueTrait for Rc<AbstractValue> {
         }
     }
 
+    /// Returns an element that is "self.cmp(other)".
+    #[logfn_inputs(TRACE)]
+    #[must_use]
+    fn compare(&self, other: Self) -> Self {
+        let zero = Rc::new(ConstantDomain::I128(0).into());
+        let one = Rc::new(ConstantDomain::I128(1).into());
+        let minus_one = Rc::new(ConstantDomain::I128(-1).into());
+        let eq = self.equals(other.clone());
+        let lt = self.less_than(other.clone());
+        eq.conditional_expression(zero, lt.conditional_expression(minus_one, one))
+    }
+
     /// Returns an element that is "if self { consequent } else { alternate }".
     #[logfn_inputs(TRACE)]
     fn conditional_expression(
@@ -3253,7 +3278,19 @@ impl AbstractValueTrait for Rc<AbstractValue> {
     fn intrinsic_bit_vector_unary(&self, bit_length: u8, name: KnownNames) -> Self {
         match &self.expression {
             Expression::CompileTimeConstant(v1) => {
-                let result = v1.intrinsic_bit_vector_unary(bit_length, name);
+                let result = match name {
+                    KnownNames::StdIntrinsicsBitreverse | KnownNames::StdIntrinsicsBswap => {
+                        v1.intrinsic_bit_vector_unary(bit_length, name)
+                    }
+                    KnownNames::StdIntrinsicsCtlz
+                    | KnownNames::StdIntrinsicsCtlzNonzero
+                    | KnownNames::StdIntrinsicsCtpop
+                    | KnownNames::StdIntrinsicsCttz
+                    | KnownNames::StdIntrinsicsCttzNonzero => {
+                        v1.intrinsic_bit_counting_unary(bit_length, name)
+                    }
+                    _ => assume_unreachable!("invalid name for intrinsic {:?}", name),
+                };
                 if result != ConstantDomain::Bottom {
                     return Rc::new(result.into());
                 }
@@ -5589,19 +5626,20 @@ impl AbstractValueTrait for Rc<AbstractValue> {
                 .widen(&alternate.get_as_interval()),
             Expression::Div { left, right } => left.get_as_interval().div(&right.get_as_interval()),
             Expression::IntrinsicBitVectorUnary {
-                name, bit_length, ..
-            } => match name {
-                KnownNames::StdIntrinsicsCtlz
-                | KnownNames::StdIntrinsicsCtlzNonzero
-                | KnownNames::StdIntrinsicsCtpop
-                | KnownNames::StdIntrinsicsCttz
-                | KnownNames::StdIntrinsicsCttzNonzero => {
-                    let min_value: IntervalDomain = IntervalDomain::from(0u128);
-                    let max_value = IntervalDomain::from(*bit_length as u128);
-                    min_value.widen(&max_value)
-                }
-                _ => interval_domain::BOTTOM,
-            },
+                name:
+                    KnownNames::StdIntrinsicsCtlz
+                    | KnownNames::StdIntrinsicsCtlzNonzero
+                    | KnownNames::StdIntrinsicsCtpop
+                    | KnownNames::StdIntrinsicsCttz
+                    | KnownNames::StdIntrinsicsCttzNonzero,
+                bit_length,
+                ..
+            } => {
+                let min_value: IntervalDomain = IntervalDomain::from(0u128);
+                let max_value = IntervalDomain::from(*bit_length as u128);
+                min_value.widen(&max_value)
+            }
+            Expression::IntrinsicBitVectorUnary { .. } => interval_domain::BOTTOM,
             Expression::Join { left, right, .. } => {
                 left.get_as_interval().widen(&right.get_as_interval())
             }
@@ -6596,7 +6634,9 @@ impl AbstractValueTrait for Rc<AbstractValue> {
                 length,
             } => {
                 let refined_length = length.refine_with(path_condition, depth + 1);
-                AbstractValue::make_memcmp(left.clone(), right.clone(), refined_length)
+                let refined_left = left.refine_with(path_condition, depth + 1);
+                let refined_right = right.refine_with(path_condition, depth + 1);
+                AbstractValue::make_memcmp(refined_left, refined_right, refined_length)
             }
             Expression::Mul { left, right } => left
                 .refine_with(path_condition, depth + 1)