Match expressions with | and variables causing spurious failure.

[B-Lorentz]

I tried this code:

#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum AbstractInt {
    Bottom = 0,
    Zero = 1,
    Top = 2,
}

impl AbstractInt {
    pub fn merge(self, other: Self) -> Self {
        use AbstractInt::*;
        match (self, other) {
            (Bottom, x) => x,
            (x, Bottom) => x,
            (Zero, Zero) => Zero,
            (Top, _) | (_, Top) => Top,
        }
    }
}

#[cfg(kani)]
mod test {
    use super::*;
    impl kani::Arbitrary for AbstractInt {
        fn any() -> Self {
            use AbstractInt::*;
            match kani::any::<u8>() {
                0 => Bottom,
                1 => Zero,
                _ => Top,
            }
        }
    }
    #[kani::proof]
    fn merge_with_bottom() {
        let x: AbstractInt = kani::any();
        assert!(x.merge(AbstractInt::Bottom) == x);
        assert!(AbstractInt::Bottom.merge(x) == x)
    }
}

and the equivalent implementaion of merge, using a | in the pattern:

impl AbstractInt {
    pub fn merge(self, other: Self) -> Self {
        use AbstractInt::*;
        match (self, other) {
            (Bottom, x) |(x, Bottom) => x,
            (Zero, Zero) => Zero,
            (Top, _) | (_, Top) => Top,
        }
    }
}

using the following command line invocation:

kani src/repro.rs

with Kani version: Kani Rust Verifier 0.53.0 (standalone)

I expected to see this happen: I expected the proof to verify with both implementations of merge.

Instead, this happened: The proof verifies with the implementation where (Bottom, x) and (x, Bottom) are on separate lines, but fails when they are on the same line separated by a |:

Kani Rust Verifier 0.53.0 (standalone)
Checking harness test::merge_with_bottom...
CBMC 5.95.1 (cbmc-5.95.1)
CBMC version 5.95.1 (cbmc-5.95.1) 64-bit x86_64 linux
Reading GOTO program from file /home/lorinc/github.com/B-Lorentz/kan/src/repro__RNvNtCsiCi0JD7ZDuS_5repro4test17merge_with_bottom.out
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 16 object bits, 48 offset bits (user-specified)
Starting Bounded Model Checking
Runtime Symex: 0.0190811s
size of program expression: 825 steps
slicing removed 508 assignments
Generated 28 VCC(s), 6 remaining after simplification
Runtime Postprocess Equation: 0.000188282s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 0.000896564s
Running propositional reduction
Post-processing
Runtime Post-process: 6.136e-06s
Solving with CaDiCaL 1.7.2
390 variables, 437 clauses
SAT checker: instance is SATISFIABLE
Runtime Solver: 6.5924e-05s
Runtime decision procedure: 0.00102995s
Running propositional reduction
Solving with CaDiCaL 1.7.2
390 variables, 438 clauses
SAT checker: instance is SATISFIABLE
Runtime Solver: 2.3305e-05s
Runtime decision procedure: 4.6675e-05s
Running propositional reduction
Solving with CaDiCaL 1.7.2
390 variables, 439 clauses
SAT checker: instance is UNSATISFIABLE
Runtime Solver: 2.043e-05s
Runtime decision procedure: 3.7687e-05s

RESULTS:
Check 1: test::merge_with_bottom.assertion.1
         - Status: FAILURE
         - Description: "assertion failed: x.merge(AbstractInt::Bottom) == x"
         - Location: src/repro.rs:35:9 in function test::merge_with_bottom

Check 2: test::merge_with_bottom.assertion.2
         - Status: SUCCESS
         - Description: "assertion failed: AbstractInt::Bottom.merge(x) == x"
         - Location: src/repro.rs:36:9 in function test::merge_with_bottom

Check 3: AbstractInt::merge.unreachable.1
         - Status: SUCCESS
         - Description: "unreachable code"
         - Location: src/repro.rs:11:15 in function AbstractInt::merge

Check 4: <AbstractInt as std::cmp::PartialEq>::eq.pointer_dereference.1
         - Status: SUCCESS
         - Description: "dereference failure: pointer NULL"
         - Location: src/repro.rs:1:30 in function <AbstractInt as std::cmp::PartialEq>::eq

Check 5: <AbstractInt as std::cmp::PartialEq>::eq.pointer_dereference.2
         - Status: SUCCESS
         - Description: "dereference failure: pointer invalid"
         - Location: src/repro.rs:1:30 in function <AbstractInt as std::cmp::PartialEq>::eq

Check 6: <AbstractInt as std::cmp::PartialEq>::eq.pointer_dereference.3
         - Status: SUCCESS
         - Description: "dereference failure: deallocated dynamic object"
         - Location: src/repro.rs:1:30 in function <AbstractInt as std::cmp::PartialEq>::eq

Check 7: <AbstractInt as std::cmp::PartialEq>::eq.pointer_dereference.4
         - Status: SUCCESS
         - Description: "dereference failure: dead object"
         - Location: src/repro.rs:1:30 in function <AbstractInt as std::cmp::PartialEq>::eq

Check 8: <AbstractInt as std::cmp::PartialEq>::eq.pointer_dereference.5
         - Status: SUCCESS
         - Description: "dereference failure: pointer outside object bounds"
         - Location: src/repro.rs:1:30 in function <AbstractInt as std::cmp::PartialEq>::eq

Check 9: <AbstractInt as std::cmp::PartialEq>::eq.pointer_dereference.6
         - Status: SUCCESS
         - Description: "dereference failure: invalid integer address"
         - Location: src/repro.rs:1:30 in function <AbstractInt as std::cmp::PartialEq>::eq

Check 10: <AbstractInt as std::cmp::PartialEq>::eq.pointer_dereference.7
         - Status: SUCCESS
         - Description: "dereference failure: pointer NULL"
         - Location: src/repro.rs:1:30 in function <AbstractInt as std::cmp::PartialEq>::eq

Check 11: <AbstractInt as std::cmp::PartialEq>::eq.pointer_dereference.8
         - Status: SUCCESS
         - Description: "dereference failure: pointer invalid"
         - Location: src/repro.rs:1:30 in function <AbstractInt as std::cmp::PartialEq>::eq

Check 12: <AbstractInt as std::cmp::PartialEq>::eq.pointer_dereference.9
         - Status: SUCCESS
         - Description: "dereference failure: deallocated dynamic object"
         - Location: src/repro.rs:1:30 in function <AbstractInt as std::cmp::PartialEq>::eq

Check 13: <AbstractInt as std::cmp::PartialEq>::eq.pointer_dereference.10
         - Status: SUCCESS
         - Description: "dereference failure: dead object"
         - Location: src/repro.rs:1:30 in function <AbstractInt as std::cmp::PartialEq>::eq

Check 14: <AbstractInt as std::cmp::PartialEq>::eq.pointer_dereference.11
         - Status: SUCCESS
         - Description: "dereference failure: pointer outside object bounds"
         - Location: src/repro.rs:1:30 in function <AbstractInt as std::cmp::PartialEq>::eq

Check 15: <AbstractInt as std::cmp::PartialEq>::eq.pointer_dereference.12
         - Status: SUCCESS
         - Description: "dereference failure: invalid integer address"
         - Location: src/repro.rs:1:30 in function <AbstractInt as std::cmp::PartialEq>::eq


SUMMARY:
 ** 1 of 15 failed
Failed Checks: assertion failed: x.merge(AbstractInt::Bottom) == x
 File: "src/repro.rs", line 35, in test::merge_with_bottom

VERIFICATION:- FAILED
Verification Time: 0.047771145s

Summary:
Verification failed for - test::merge_with_bottom
Complete - 0 successfully verified harnesses, 1 failures, 1 total.

[adpaco-aws]

Hi @B-Lorentz , thanks for reporting this issue!

I have been able to reproduce it using Kani v0.53.0. Luckily, it looks like it's fixed in the next version, which is going to be released very soon. If you don't want to wait for the release, please compile from source to avoid this issue.

[tautschnig]

We still need to figure out why this is now fixed, i.e., which change made the difference.

[celinval]

I did some debugging here, and it looks like the problem was related to handling of StorageLive and StorageDead which was changed by @tautschnig in #2995.

To confirm that, I checkout the parent commit of e4078b4 which contains the spurious failure. Then applied the changes to kani-compiler and cprover-bindings not related to the CBMC upgrade.

# All of this requires old CBMC 5.95.1
git co e4078b4bdb2~
cargo build-dev
kani match_pattern.rs # This fails

git diff HEAD..e4078b4bdb2 -- kani-compiler/ cprover_bindings/src/env.rs cprover_bindings/src/lib.rs > /tmp/kani.patch
patch -p1 < /tmp/kani.patch
cargo build-dev
kani match_pattern.rs # This succeeds

[celinval]

Let me add the test case first.

[B-Lorentz]

Thank you all.
I'm happy that my report was useful