SRI-CSL / yices2 / 30149647219

71%

push

github

Fix signed-overflow UB in bv64 interval abstraction (#656)

* Fix signed-overflow UB in bv64 interval abstraction

sum/diff computed x+y / x-y as signed int64 (undefined on overflow),
then detected the overflow by inspecting the result's sign. At -O2/-O3
GCC assumes signed overflow never happens and deletes those sign-based
checks, so overflow went undetected -> unsound BV interval abstraction
-> wrong "unsat". opposite/mul/negate/power had the same class of UB
via -x / -(int64_t)c on INT64_MIN. macOS/clang happened to keep the
checks, so this only showed on Linux release builds.

Do the wraparound arithmetic and negations in the unsigned domain
(well-defined, identical two's-complement result) so the overflow
checks survive optimization.

Add two QF_BV regression tests (from SMT-LIB QF_BV/20210219-Sydr)
that return unsat on the buggy build and sat with the fix.

* Replace stale BV64 arithmetic tests

---------

Co-authored-by: Stephane Graham-Lengrand <stephane.graham-lengrand@sri.com>

5 of 8 new or added lines in 1 file covered. (62.5%)

95541 of 134173 relevant lines covered (71.21%)

1666283.3 hits per line