Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Spurious failure with rust toolchain-2022-12-11 #2051

Closed
zhassan-aws opened this issue Dec 29, 2022 · 12 comments · Fixed by #2067
Closed

Spurious failure with rust toolchain-2022-12-11 #2051

zhassan-aws opened this issue Dec 29, 2022 · 12 comments · Fixed by #2067
Labels
[C] Bug This is a bug. Something isn't working. [F] Spurious Failure Issues that cause Kani verification to fail despite the code being correct. T-CBMC Issue related to an existing CBMC issue
Milestone

Comments

@zhassan-aws
Copy link
Contributor

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 zhassan-aws added [C] Bug This is a bug. Something isn't working. [F] Spurious Failure Issues that cause Kani verification to fail despite the code being correct. labels Dec 29, 2022
@zhassan-aws
Copy link
Contributor Author

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"]
  1. Rebuild kani
  2. cd s2n-quic/quic/s2n-quic-core in the cloned branch in step 1
  3. 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
Copy link
Contributor Author

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
Copy link
Contributor

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:

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

@tedinski
Copy link
Contributor

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
Copy link
Contributor Author

zhassan-aws commented Dec 30, 2022

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
Copy link
Contributor Author

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
Copy link
Contributor Author

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
Copy link
Contributor Author

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

@zhassan-aws
Copy link
Contributor Author

zhassan-aws commented Dec 30, 2022

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 zhassan-aws added the T-CBMC Issue related to an existing CBMC issue label Dec 30, 2022
@zhassan-aws
Copy link
Contributor Author

@tautschnig need your help on this one.

@zhassan-aws
Copy link
Contributor Author

Tracked by diffblue/cbmc#7462

@tautschnig
Copy link
Member

diffblue/cbmc#7462 is now resolved and will be part of 5.75.0 (due 2023-01-19).

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
[C] Bug This is a bug. Something isn't working. [F] Spurious Failure Issues that cause Kani verification to fail despite the code being correct. T-CBMC Issue related to an existing CBMC issue
Projects
No open projects
Status: Done
Development

Successfully merging a pull request may close this issue.

4 participants