search

diffblue / cbmc

C Bounded Model Checker
https://diffblue.github.io/cbmc
Other
850 stars 265 forks source link

SMT2 backend crashes with invariant violation when handling a union with a float member #6348

Closed andreast271 closed 2 years ago

andreast271 commented 3 years ago

CBMC version: cbmc-5.38.0-13-gb4c3a12d2 Operating system: Linux x86_64 Exact command line resulting in the issue: cbmc --z3 myalg.c What behaviour did you expect: Verification failure What happened instead: crash with invariant violation

The test case myalg.c is:

union uf { float f; };

int main() {
  int a;
  union uf u;
  u.f = a;
  __CPROVER_assert(u.f > 0, "");
  return 0;
}

The invariant violation report is:

Invariant check failed
File: smt2/smt2_conv.cpp:941 function: type2id
Condition: false
Reason: Unreachable

The crash report with back traces enabled is attached. smt2crash.txt

The type of code causing the crash is used in math.c in the implementation of nextUp, which is used by sqrt. As a result, code that uses these functions will crash in the SMT2 backend

andreast271 commented 3 years ago

A test case for the bug without unions is:

int main() {
    float f;
    unsigned u = *(unsigned *)&f;
    __CPROVER_assert(u > 0, "");
    return 0;
}

The invariant violation message is the unchanged.

TGWDB commented 3 years ago

Thanks for the update. The issue is with casts of floats into bitvectors for the SMT solver backend. (They are being cast to ID_bv and the conversion is currently expecting explicitly signed or unsigned, but not generic bitvectors.) I'm adding this comment in case someone else is looking into fixing this at the moment (I'll be away for a couple of weeks).