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

Using z3 with symbolic boolean array crashes CBMC #2002

Closed
zhassan-aws opened this issue Dec 15, 2022 · 3 comments · Fixed by #2301
Closed

Using z3 with symbolic boolean array crashes CBMC #2002

zhassan-aws opened this issue Dec 15, 2022 · 3 comments · Fixed by #2301
Labels
[C] Bug This is a bug. Something isn't working. [F] Crash Kani crashed T-CBMC Issue related to an existing CBMC issue

Comments

@zhassan-aws
Copy link
Contributor

I tried this code:

#[kani::proof]
fn main() {
    let _arr: [bool; 1] = kani::any();
}

using the following command line invocation:

kani test1.rs  --enable-unstable --cbmc-args --z3

with Kani version: 438e582

I expected to see this happen: Verification successful

Instead, this happened: CBMC crashed:

Runtime Symex: 0.114774s
size of program expression: 4174 steps
slicing removed 2993 assignments
Generated 298 VCC(s), 48 remaining after simplification
Runtime Postprocess Equation: 0.0009437s
--- begin invariant violation report ---
Invariant check failed
File: ../src/solvers/smt2/smt2_conv.cpp:5643 function: convert_type
Condition: Check return value
Reason: to_union_type(ns.follow(type)).components().empty() || width != 0
Backtrace:
cbmc(+0xa98040) [0x55e09d4f4040]
cbmc(+0xa985e9) [0x55e09d4f45e9]
cbmc(+0x225a74) [0x55e09cc81a74]
cbmc(+0x8b6066) [0x55e09d312066]
cbmc(+0x8908b7) [0x55e09d2ec8b7]
cbmc(+0x890782) [0x55e09d2ec782]
cbmc(+0x8b03e7) [0x55e09d30c3e7]
cbmc(+0x8b0cad) [0x55e09d30ccad]
cbmc(+0x8b02a6) [0x55e09d30c2a6]
cbmc(+0x8b0cad) [0x55e09d30ccad]
cbmc(+0x8b0b6f) [0x55e09d30cb6f]
cbmc(+0x8b0d57) [0x55e09d30cd57]
cbmc(+0x8b0c24) [0x55e09d30cc24]
cbmc(+0x8b0fdf) [0x55e09d30cfdf]
cbmc(+0x8ad5a8) [0x55e09d3095a8]
cbmc(+0x8ad5e3) [0x55e09d3095e3]
cbmc(+0x8ad5e3) [0x55e09d3095e3]
cbmc(+0x8affd8) [0x55e09d30bfd8]
cbmc(+0x8b1cda) [0x55e09d30dcda]
cbmc(+0x5508f1) [0x55e09cfac8f1]
cbmc(+0x5590a6) [0x55e09cfb50a6]
cbmc(+0x559c52) [0x55e09cfb5c52]
cbmc(+0x348d84) [0x55e09cda4d84]
cbmc(+0x349205) [0x55e09cda5205]
cbmc(+0x35ac95) [0x55e09cdb6c95]
cbmc(+0x201189) [0x55e09cc5d189]
cbmc(+0x1fd6ae) [0x55e09cc596ae]
cbmc(+0x1f4e9f) [0x55e09cc50e9f]
cbmc(+0x1e0ec9) [0x55e09cc3cec9]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0xf3) [0x7f9e98c530b3]
cbmc(+0x1f681e) [0x55e09cc5281e]

Diagnostics: 
<< EXTRA DIAGNOSTICS >>
failed to get width of union
<< END EXTRA DIAGNOSTICS >>

--- end invariant violation report ---
Passing problem to SMT2 QF_AUFBV using Z3
@zhassan-aws zhassan-aws added [C] Bug This is a bug. Something isn't working. [F] Crash Kani crashed T-CBMC Issue related to an existing CBMC issue labels Dec 15, 2022
@rahulku
Copy link
Contributor

rahulku commented Dec 15, 2022

cbmc issue?

@zhassan-aws
Copy link
Contributor Author

I'm trying to reproduce it on a C program (similar to what I did for diffblue/cbmc#7308), to make debugging easier. So far, I haven't been successful.

@zhassan-aws
Copy link
Contributor Author

Created diffblue/cbmc#7442 with the goto binary for the time being.

@zhassan-aws zhassan-aws changed the title Using z3 with symbolic boolear array crashes CBMC Using z3 with symbolic boolean array crashes CBMC Dec 22, 2022
tautschnig added a commit to tautschnig/kani that referenced this issue Mar 17, 2023
- Re-enable tests that had to be disabled with the toolchain upgrade in
  model-checking#2149. Fixes model-checking#2286, fixes model-checking#2191.
- Do not generate non-NULL pointer constants. Together with the CBMC
  version update this avoids the need for an unwinding annotation in the
  mir-linker test. Fixes model-checking#1978.
- CBMC 5.79.0 ships simplifier improvements that enable constant
  propagation to avoid slow-down with the Display trait. Fixes model-checking#1996.
- CBMC 5.79.0 ships SMT back-end fixes. Fixes model-checking#2002.

Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>
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] Crash Kani crashed T-CBMC Issue related to an existing CBMC issue
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants