Use bv_typet to fix type consistency in byte-operator lowering #4519
Conversation
tautschnig
requested review from
allredj,
chrisr-diffblue,
kroening,
martin-cs,
peterschrammel,
pkesseli,
romainbrenguier and
smowton
as code owners
| case bvtypet::IS_BV: | ||
| INVARIANT( | ||
| src_width == dest_width, | ||
| "source bitvector with shall equal the destination bitvector width"); |
There was a problem hiding this comment.
Thanks, fixed (two occurrences).
tautschnig
force-pushed
the
float-byte-extract
branch
3 times, most recently
from
9bb3226 to
573c9e4
Compare
src/util/simplify_expr.cpp
Outdated
| expr = from_integer(int_value, expr_type); | ||
| else | ||
| expr = from_integer( | ||
| int_value, ns.follow_tag(to_c_enum_tag_type(expr_type))); |
There was a problem hiding this comment.
I am afraid that the tag type needs to be restored, or otherwise the type of the expression changes.
There was a problem hiding this comment.
Err, thanks for catching that!
src/util/simplify_expr_int.cpp
Outdated
| { | ||
| exprt tmp = expr.op0(); | ||
| tmp.type().id(ID_unsignedbv); | ||
| value = numeric_cast<mp_integer>(tmp); |
There was a problem hiding this comment.
Use bvrep2integer instead?
tautschnig
force-pushed
the
float-byte-extract
branch
from
573c9e4 to
f3eb00f
Compare
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: ff93c2d).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/108049220
Status will be re-evaluated on next push.
Common spurious failures include: the cbmc commit has disappeared in the mean time (e.g. in a force-push); the author is not in the list of contributors (e.g. first-time contributors); compatibility was already broken by an earlier merge.
Previously we fixed the extracted bytes to be unsigned bitvectors, but we should not actually impose (un)signedness as we do not actually interpret the bytes as numeric values. This fixes byte operators over floating-point values, and makes various SMT-solver tests pass as the SMT back-end is more strict about typing and therefore was more frequently affected by this bug. To make all this work it was also necessary to extend and fix the simplifier's handling of bv_typet expressions, and also cover one more case of type casts in the bitvector back-end. The tests Array_operations1/test.desc Float-equality1/test_no_equality.desc memory_allocation1/test.desc union12/test.desc union6/test.desc union7/test.desc continue to fail on Windows and thus cannot yet be enabled.
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: 29eea0f).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/108049870
Status will be re-evaluated on next push.
Common spurious failures include: the cbmc commit has disappeared in the mean time (e.g. in a force-push); the author is not in the list of contributors (e.g. first-time contributors); compatibility was already broken by an earlier merge.
One case was pre-existing, the second was the result of copy&paste.
tautschnig
force-pushed
the
float-byte-extract
branch
from
f3eb00f to
ee07f0a
Compare
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: e8c3fa1).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/108050247
Status will be re-evaluated on next push.
Common spurious failures include: the cbmc commit has disappeared in the mean time (e.g. in a force-push); the author is not in the list of contributors (e.g. first-time contributors); compatibility was already broken by an earlier merge.
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: 9bb3226).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/108050730
Status will be re-evaluated on next push.
Common spurious failures include: the cbmc commit has disappeared in the mean time (e.g. in a force-push); the author is not in the list of contributors (e.g. first-time contributors); compatibility was already broken by an earlier merge.
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: f3eb00f).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/108051519
Status will be re-evaluated on next push.
Common spurious failures include: the cbmc commit has disappeared in the mean time (e.g. in a force-push); the author is not in the list of contributors (e.g. first-time contributors); compatibility was already broken by an earlier merge.
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: 573c9e4).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/108052100
Status will be re-evaluated on next push.
Common spurious failures include: the cbmc commit has disappeared in the mean time (e.g. in a force-push); the author is not in the list of contributors (e.g. first-time contributors); compatibility was already broken by an earlier merge.
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: ee07f0a).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/108053686
3 participants
Previously we fixed the extracted bytes to be unsigned bitvectors, but
we should not actually imposed (un)signedness as we do not actually
interpret the bytes as numeric values. This fixes byte operators over
floating-point values, and makes various SMT-solver tests pass as the
SMT back-end is more strict about typing.
To make all this work it was also necessary to extend and fix the
simplifier's handling of bv_typet expressions, and also cover one more
case of type casts in the bitvector back-end.