simplify extractbits_exprt representation
#8246
Conversation
kroening
force-pushed
the
extractbits-width
branch
3 times, most recently
from
2f964a7 to
71827f4
Compare
The current representation of extractbits_exprt stores both the upper and lower indices of the range that is to be extracted, and their difference plus one in form of the width of the type of the expression. This removes the upper index, as it can be deduced from the lower index and the width of the result. The key benefit is reducing burden on the user of the class, who a) doesn't have to remember which index comes first, and b) doesn't have to do the calculation of the upper index.
kroening
force-pushed
the
extractbits-width
branch
from
71827f4 to
97cb8a3
Compare
Codecov ReportAttention: Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## develop #8246 +/- ##
========================================
Coverage 79.64% 79.64%
========================================
Files 1684 1684
Lines 195661 195622 -39
========================================
- Hits 155837 155809 -28
+ Misses 39824 39813 -11 ☔ View full report in Codecov by Sentry. |
kroening
requested review from
peterschrammel,
thomasspriggs,
TGWDB,
esteffin,
martin-cs,
tautschnig and
remi-delmas-3000
as code owners
tautschnig
added
the
Version 6
|
Labelling "Version 6" as we need to get this merged before the release (or otherwise alongside a goto-program-version-bump) for it would result in incompatibility with previously compiled goto binaries. |
I don't think we have a way to get this expression into a goto program. |
| dest += convert_with_precedence(upper, precedence); | ||
| } | ||
| else | ||
| dest += "?"; |
There was a problem hiding this comment.
Will this result in syntactically invalid C being generated? If so, is that a problem and would it be better to throw some kind of error or have an invariant?
There was a problem hiding this comment.
The expr2X functions are designed to generate some string when given an unknown expression -- this should be added to the documentation.
| DATA_INVARIANT( | ||
| lower_as_int <= upper_as_int, | ||
| "upper bound must be greater or equal to lower bound"); | ||
|
|
There was a problem hiding this comment.
Removing invariants because that case is simply not possible seems like a good thing.
The current representation of
extractbits_exprtstores both the upper and lower indices of the range that is to be extracted, and their difference plus one in form of the width of the type of the expression.This removes the upper index, as it can be deduced from the lower index and the width of the result. The key benefit is reducing burden on the user of the class, who a) doesn't have to remember which index comes first, and b) doesn't have to do the calculation of the upper index.