BitfieldSimplifier: arbitrary precision bit masks #11
Conversation
lib/Expr/BitfieldSimplifier.cpp
Outdated
|
|
||
| case Expr::And: | ||
| rbits.knownOneBits = bits[0].knownOneBits & bits[1].knownOneBits; | ||
| rbits.knownZeroBits = bits[0].knownZeroBits | bits[1].knownZeroBits; | ||
|
|
||
| bits[0].ignoredBits = ignoredBits | bits[1].knownZeroBits; | ||
| bits[1].ignoredBits = ignoredBits | (bits[0].knownZeroBits & ~bits[1].knownZeroBits); | ||
| bits[1].ignoredBits = ignoredBits | bits[0].knownZeroBits; |
There was a problem hiding this comment.
Why is the remaining part of the expression missing?
There was a problem hiding this comment.
If a bit on the left side is 0, doesn't it mean that we can ignore the corresponding bit on the right side? And is also commutative so wouldn't it make sense to have the same expression for ignored bits on the left and on the right?
There was a problem hiding this comment.
Could be, I'll have a better look later. In the meantime, could you move optimizations/bugfixes in a separate commit? The first commit would just have the mechanical conversion to APInt. This would make it much simpler to review.
There was a problem hiding this comment.
In the original zeroMask is only needed because the masks are 64 bits wide even when the expressions are narrower than 64 bits. APInts can be any number of bits wide so that would not be needed anymore. Should I keep 64-bit masks and zeroMask in the mechanical conversion or not?
|
I admit that this BitFieldSimplifier is a bit fuzzy in my mind. There are some expressions that look different from before, it would make sense to add comments to the code to explain the changes. Also a couple of test cases would help. They should be simple to add, following this model: https://github.com/S2E/klee/blob/master/unittests/Expr/ExprTest.cpp |
Still limited to 64-bit masks. Signed-off-by: Matteo Rizzo <matteo.rizzo@epfl.ch>
Use llvm::APInt to support expressions of arbitrary width. Signed-off-by: Matteo Rizzo <matteo.rizzo@epfl.ch>
matrizzo
force-pushed
the
improvement/ap-simplifier
branch
from
c9e2ed2
to
d60fbe1
Compare
Use llvm::APInt instead of uint64_t for bit masks.
Needed for the modified (non-forking) helper for signed multiplication
which uses 128-bit integers.
Signed-off-by: Matteo Rizzo matteo.rizzo@epfl.ch