Spurious failure with rust toolchain-2022-12-11

[zhassan-aws]

This is a tracking issue for the failure in an s2n-quic harness (packet::number::tests::round_trip) with the rust toolchain update in #2045.

[zhassan-aws]

This branch contains a minimized example that reproduces the spurious failure: https://github.com/zhassan-aws/s2n-quic/tree/kani-iss2051

The breaking change was introduced in the nightly-2022-11-24 toolchain. Here are the steps to reproduce (these were done using c135fa9):

1. Clone the branch: git clone -b kani-iss2051 https://github.com/zhassan-aws/s2n-quic
2. Apply this patch to kani:

$ git diff
diff --git a/kani-compiler/src/kani_middle/coercion.rs b/kani-compiler/src/kani_middle/coercion.rs
index a92c2f366ae..799ba3b4766 100644
--- a/kani-compiler/src/kani_middle/coercion.rs
+++ b/kani-compiler/src/kani_middle/coercion.rs
@@ -215,7 +215,7 @@ fn custom_coerce_unsize_info<'tcx>(
 
     let trait_ref = ty::Binder::dummy(TraitRef {
         def_id,
-        substs: tcx.mk_substs_trait(source_ty, &[target_ty.into()]),
+        substs: tcx.mk_substs_trait(source_ty, [target_ty.into()]),
     });
 
     match tcx.codegen_select_candidate((ParamEnv::reveal_all(), trait_ref)) {
diff --git a/rust-toolchain.toml b/rust-toolchain.toml
index 0fb3d8fbb64..f342c79ab3a 100644
--- a/rust-toolchain.toml
+++ b/rust-toolchain.toml
@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2022-11-20"
+channel = "nightly-2022-11-24"
 components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]

3. Rebuild kani
4. cd s2n-quic/quic/s2n-quic-core in the cloned branch in step 1
5. Run cargo kani --harness kani_round_trip

This will fail with:

SUMMARY:
 ** 1 of 514 failed (7 unreachable)
Failed Checks: assertion failed: x == y
 File: "/home/ubuntu/git/iss2051/s2n-quic/quic/s2n-quic-core/src/packet/number/mod.rs", line 289, in packet::number::dpn

With the previous nightly rust toolchain (nightly-2022-11-23), verification succeeds:

SUMMARY:
 ** 0 of 514 failed (7 unreachable)

VERIFICATION:- SUCCESSFUL

[zhassan-aws]

The concrete playback test passes:

#[test]
fn kani_concrete_playback_kani_round_trip_5132525969304926950() {
    let concrete_vals: Vec<Vec<u8>> = vec![
        // 4u
        vec![4, 0, 0, 0]
    ];
    kani::concrete_playback_run(concrete_vals, kani_round_trip);
}

Also, if I replace kani::any() in the harness with the value from the concrete playback test (or the one from visualize with is 16) and rerun Kani, verification succeeds, so the failure is definitely bogus.

[tedinski]

I looked at the rust commit log between those two nightly versions with git log ff8c8dfbe..70f8737b2 and saw this one that might be a cause:

• optimize field ordering by grouping m*2^n-sized fields with equivalently aligned ones rust-lang/rust#102750

We might be seeing different type layouts before and after, and this might be exposing a buggy assumption in the kani-compiler.

[tedinski]

Also, if I replace kani::any() in the harness with the value from the concrete playback test (or the one from visualize with is 16) and rerun Kani, verification succeeds

I think the important part here is "rerun Kani". I initially misread this because it was next to concrete playback stuff, but I just validated this.

The failing trace says x = 0, but replacing x = kani::any() with x = 0 causes the proof to succeed. I'm not sure that's possible without a CBMC bug?

[zhassan-aws]

I'm also suspecting a CBMC bug, in particular due to those lines in the --visualize report:

Step 8342: Function [packet::number::dpn](http://localhost:8000/src/packet/number/mod.rs.html#277), File [src/packet/number/mod.rs](http://localhost:8000/src/packet/number/mod.rs.html), Line [295](http://localhost:8000/src/packet/number/mod.rs.html#295)
let x = packet_bytes;
x.buf.cap = 1ul (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000001)
Step 8343: Function [packet::number::dpn](http://localhost:8000/src/packet/number/mod.rs.html#277), File [src/packet/number/mod.rs](http://localhost:8000/src/packet/number/mod.rs.html), Line [295](http://localhost:8000/src/packet/number/mod.rs.html#295)
let x = packet_bytes;
x.buf.ptr.pointer.pointer = dynamic_object 
Step 8344: Function [packet::number::dpn](http://localhost:8000/src/packet/number/mod.rs.html#277), File [src/packet/number/mod.rs](http://localhost:8000/src/packet/number/mod.rs.html), Line [295](http://localhost:8000/src/packet/number/mod.rs.html#295)
let x = packet_bytes;
x.len = 1ul (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000001)
Step 8345: Function MISSING, File MISSING, Line 0
-> [packet::number::encode](http://localhost:8000/src/packet/number/mod.rs.html#302)
Step 8838: Function MISSING, File MISSING, Line 0
<- [packet::number::encode](http://localhost:8000/src/packet/number/mod.rs.html#302)
Step 8839: Function MISSING, File MISSING, Line 0
y.buf.cap = 1ul (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000001)
Step 8840: Function MISSING, File MISSING, Line 0
y.buf.ptr.pointer.pointer = dynamic_object$1 
Step 8841: Function MISSING, File MISSING, Line 0
y.len = 1ul (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000001)

More specifically, the $1 suffix in dynamic_object is something I haven't seen before, and I'm not sure what it means.

The full report is attached.

report-packet-number-kani_round_trip.tar.gz

[zhassan-aws]

Looks like there's nothing wrong with the $<num> suffix. It seems to just be a counter for dynamic objects. It appears on programs such as this one:

#[kani::proof]
fn main() {
    let v1 = vec![1];
    let v2 = vec![2];
    assert_eq!(v1, v2);
}

v1.buf.ptr.pointer.pointer = (signed int *)&dynamic_object 
v2.buf.ptr.pointer.pointer = (signed int *)&dynamic_object$0 

[zhassan-aws]

goto-instrument --validate-goto-model is pointing out a possible issue:

$ goto-instrument --validate-goto-model s2n_quic_core-8f24532ce3fa20f6.symtab.out 
Reading GOTO program from 's2n_quic_core-8f24532ce3fa20f6.symtab.out'
memcmp type inconsistency
goto program type: code
symbol table type: code (at: file /home/ubuntu/.rustup/toolchains/nightly-2022-11-24-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/cmp.rs line 91 column 13 function <[u8] as core::slice::cmp::SlicePartialEq<u8>>::equal)

This is the line of code it's pointing out:
https://github.com/rust-lang/rust/blob/70f8737b2f5d3bf7d6b784fad00b663b7ff9feda/library/core/src/slice/cmp.rs#L91

[zhassan-aws]

FWIW, the issue pointed out by --validate-goto-model also occurs with the older toolchain.

[zhassan-aws]

Interestingly, the spurious failure does not occur with CBMC 5.70.0 (even with the newer toolchain):

$ cargo kani --harness kani_round_trip
# -- snip -- 

Checking harness packet::number::kani_round_trip...
CBMC 5.70.0 (cbmc-5.70.0)
CBMC version 5.70.0 (cbmc-5.70.0) 64-bit x86_64 linux
Reading GOTO program from file /home/ubuntu/git/iss2051/s2n-quic/target/kani/x86_64-unknown-linux-gnu/debug/deps/s2n_quic_core-8f24532ce3fa20f6.for-packet-number-kani_round_trip.out
Generating GOTO Program
# -- snip --


SUMMARY:
 ** 0 of 514 failed (7 unreachable)

VERIFICATION:- SUCCESSFUL

but it occurs with CBMC 5.71.0 and 5.72.0.

[zhassan-aws]

@tautschnig need your help on this one.

[zhassan-aws]

Tracked by diffblue/cbmc#7462