New expression: count_leading_zeros_exprt #5879
Conversation
tautschnig
requested review from
allredj,
chrisr-diffblue,
hannes-steffenhagen-diffblue,
kroening,
martin-cs,
peterschrammel,
romainbrenguier and
smowton
as code owners
tautschnig
force-pushed
the
clz-expression
branch
from
a9c9588 to
9364cde
Compare
| { | ||
| clz.zero_permitted(true); | ||
| const source_locationt source_location = clz.source_location(); | ||
|
|
There was a problem hiding this comment.
I would go stronger than the nondet: The wording in the gcc docs is that __builtin_clz is undefined when the argument is zero. Assuming they use the meaning of "undefined" as in the ISO C standard, then this is worth an assertion, to be generated in goto_check.
There was a problem hiding this comment.
Hmm, true, then I could perhaps demote the ID_zero_permitted to ID_C_zero_permitted?
There was a problem hiding this comment.
I don't think you need it at all. We don't have anything equivalent for any of the other expressions that are only partially defined.
There was a problem hiding this comment.
But we need to distinguish whether we're handling MSVC's __lzcnt or __builtin_clz. The former is defined for all values, the latter isn't defined for 0.
There was a problem hiding this comment.
Ah, right. Then I'd make it ID_zero_permitted; a comment would be too weak, given that the semantics do differ.
There was a problem hiding this comment.
Except they only sort-of do: it seems that in practice it's almost always ok, it's just that GCC doesn't provide a guarantee: https://stackoverflow.com/questions/19527897/how-undefined-are-builtin-ctz0-or-builtin-clz0. How about the solution that I just pushed?
Codecov Report
@@ Coverage Diff @@
## develop #5879 +/- ##
===========================================
+ Coverage 73.37% 73.55% +0.18%
===========================================
Files 1428 1429 +1
Lines 155121 155219 +98
===========================================
+ Hits 113813 114167 +354
+ Misses 41308 41052 -256
Continue to review full report at Codecov.
|
tautschnig
force-pushed
the
clz-expression
branch
from
9364cde to
530b484
Compare
tautschnig
force-pushed
the
clz-expression
branch
3 times, most recently
from
3566ce6 to
66d3773
Compare
tautschnig
force-pushed
the
clz-expression
branch
2 times, most recently
from
ab6246a to
30ba008
Compare
tautschnig
force-pushed
the
clz-expression
branch
from
30ba008 to
5b1ebeb
Compare
Replaces the hard-coded string by a dstringt to avoid typos, and also changes it to a comment: the annotation (communicating from the front-end to goto_checkt) does not change the semantics of the expression that has been annotated.
Expression lowering may be useful well outside the solvers/ context. Making it a method of the class being lowered also serves as a way of describing the semantics of the expression. This is mainly a refactoring, no changes in behaviour are intended.
Rather than ad-hoc handling __builtin_clz and __lzcnt (and their variants) in the C front-end, make counting-leading-zeros available across the code base.
tautschnig
force-pushed
the
clz-expression
branch
from
5b1ebeb to
7409997
Compare
Rather than ad-hoc handling __builtin_clz and __lzcnt (and their
variants) in the C front-end, make counting-leading-zeros available
across the code base.