Type mismatch for `FnDefStruct`

[zhassan-aws]

Running Kani on harnesses in the s2n-quic-transport crate in this branch of s2n-quic results in a CBMC error:

: function call: parameter "_RINvNtCshBEb14mhtvp_4core3cmp6max_byjNvYjNtB2_3Ord3cmpECsPu7NGxNZ36_5tokio::1::var_3::compare" type mismatch:
got struct_tag
  * identifier: tag-_RNvXsR_NtNtCshBEb14mhtvp_4core3cmp5implsjNtB7_3Ord3cmpCs3J42wHhXxpW_18s2n_quic_transport::FnDefStruct
expected struct_tag
  * identifier: tag-_RNvXsR_NtNtCshBEb14mhtvp_4core3cmp5implsjNtB7_3Ord3cmpCsPu7NGxNZ36_5tokio::FnDefStruct

Trying to come up with a minimal reproducer to attach to this issue.

[fzaiser]

I believe I'm hitting the same issue when trying to run the tokio tests in Kani.

[fzaiser]

Strangely, demangling the two names using rustfilt -h, I get tag-<usize as core[cd150e9e29982b29]::cmp::Ord>::cmp::FnDefStruct for both.

[tautschnig]

They might be the same underlying type, but it seems their struct tags (the names of the symbols that have the actual type information in the symbol table) are different.

[zhassan-aws]

The error can be reproduced on the attached tarball with the following steps:

1. tar xvzf foo.tar.gz
2. cd foo
3. cargo kani --harness main

Checking harness main...
CBMC 5.63.0 (cbmc-5.63.0)
CBMC version 5.63.0 (cbmc-5.63.0) 64-bit x86_64 linux
Reading GOTO program from file /home/ubuntu/tmp/foo/target/x86_64-unknown-linux-gnu/debug/deps/cbmc-for-main.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
: function call: parameter "_RINvNtCshBEb14mhtvp_4core3cmp6max_byjNvYjNtB2_3Ord3cmpECs4oZXxRZAdit_5bytes::1::var_3::compare" type mismatch:
got struct_tag
  * identifier: tag-_RNvXsR_NtNtCshBEb14mhtvp_4core3cmp5implsjNtB7_3Ord3cmpCs64sXxVJzpr7_3foo::FnDefStruct
expected struct_tag
  * identifier: tag-_RNvXsR_NtNtCshBEb14mhtvp_4core3cmp5implsjNtB7_3Ord3cmpCs4oZXxRZAdit_5bytes::FnDefStruct
Verification Time: 2.3077645s

with b0aeb2bcd53 foo.tar.gz

[zhassan-aws]

The error can be reproduced with 131c07348f360de2a2ac8157923dc2ddbb77dfb7, but not with the next commit: 632fda645364790ada91b5e9980731638c7fc8b7, so looks like something in that commit fixed the issue. @celinval any idea what may have fixed this error in that commit?

[celinval]

Have you compared the MIR that is generated in each commit? My first guess is that something has changed in the compiler but it could also be some obscure issue with our trait handling. Don't know.

[zhassan-aws]

This can no longer be reproduced since 632fda645364790ada91b5e9980731638c7fc8b7. Closing.

[zhassan-aws]

Reopening: this issue can again be reproduced with af6c93eb745 using the following steps:

1. git clone https://github.com/aws/s2n-quic
2. cd s2n-quic/quic/s2n-quic-core
3. git checkout ae29a32660741b4926d557920fa852a313aa4f86
4. cargo kani --tests --harness eight_byte_sequence_test

This produces:

Unwinding loop _RNvMs3_NtCshwRV6iS787W_4core3fmtNtB5_9Arguments6as_strCscMpydEzG0lq_13s2n_quic_core.0 iteration 1 file /home/ubuntu/.rustup/toolchains/nightly-2022-09-13-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/fmt/mod.rs line 519 column 19 function std::fmt::Arguments::as_str thread 0
: function call: parameter "_RINvMNtCshwRV6iS787W_4core6optionINtB3_6OptionReE11map_or_elseNtNtCsbTLSx9MNYye_5alloc6string6StringNCNvNtB12_3fmt6format0NvYeNtNtB12_6borrow7ToOwned8to_ownedECs3ViRrCGVxbG_9yaml_rust::1::var_3::f" type mismatch:
got struct_tag
  * identifier: tag-_RNvXs2_NtCsbTLSx9MNYye_5alloc3streNtNtB7_6borrow7ToOwned8to_ownedCscMpydEzG0lq_13s2n_quic_core::FnDefStruct
expected struct_tag
  * identifier: tag-_RNvXs2_NtCsbTLSx9MNYye_5alloc3streNtNtB7_6borrow7ToOwned8to_ownedCs3ViRrCGVxbG_9yaml_rust::FnDefStruct

CBMC failed with status 6
VERIFICATION:- FAILED

[tedinski]

• Related? #1257