SMT-LIB2: shifts with wider shift distances#8834
Conversation
kroening
requested review from
TGWDB,
martin-cs and
peterschrammel
as code owners
Codecov Report❌ Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## develop #8834 +/- ##
========================================
Coverage 80.00% 80.01%
========================================
Files 1700 1700
Lines 188252 188312 +60
Branches 73 73
========================================
+ Hits 150613 150675 +62
+ Misses 37639 37637 -2 ☔ View full report in Codecov by Sentry. 🚀 New features to boost your workflow:
|
kroening
force-pushed
the
smt2-shift
branch
2 times, most recently
from
7fed5fd to
365bd7b
Compare
| out << "((_ zero_extend " << width_op - width_distance << ") "; | ||
| convert_expr(shift_expr.distance()); | ||
| out << ")"; // zero_extend | ||
| out << ')'; // zero_extend |
There was a problem hiding this comment.
Doesn't this require the use of sign_extend if distance_type.id() == ID_signedbv? (And possibly also for distance_type.id() == ID_c_enum if the underlying type is signed.)
There was a problem hiding this comment.
We never had shifts with negative distance, and I don't see a need to introduce them. I'll add a comment to the expression class and the implementation that these have no meaning.
There was a problem hiding this comment.
But then lines 1836.. check for exactly that. (I was also thinking that we should not have such types here, but then we should DATA_INVARIANT'ing this here and really not have those cases in the decision of the if statement).
There was a problem hiding this comment.
We have never banned the use of signed types as arguments for the shift distance. We just don't give meaning for negative values.
There was a problem hiding this comment.
Fair enough - can we please have a comment to say that we always interpret the distance as an unsigned bitvector, irrespective of the type it actually has?
This fixes the case of converting shifts where the shift distance is wider than the shift operand to SMT-LIB2. SMT-LIB2 requires that the width of the shift operand and the shift distance is the same. To not lose leading bits of the shift distance, use the wider one of the two as the width of the shift, and truncate the result when needed.
4 participants
This fixes the case of converting shifts where the shift distance is wider than the shift operand to SMT-LIB2.
SMT-LIB2 requires that the width of the shift operand and the shift distance is the same. To not lose leading bits of the shift distance, use the wider one of the two as the width of the shift, and truncate the result when needed.