[SMT] Add bitvector type, attribute, and constant operation #6804
Conversation
maerhart
force-pushed
the
maerhart-smt-bitvector-constants
branch
3 times, most recently
from
bd9d336
to
c89bf61
Compare
There was a problem hiding this comment.
Nice!
I'm just wondering if keeping the same syntax as SMT-LIB makse sense or not.
My reasonning would be that keeping it the same as MLIR/CIRCT would make more sense, but that's a matter of preferences I think, and I would be okay for both.
I'm just not quite sure what we would gain from the SMT-LIB way!
| ```mlir | ||
| #smt.bv<"#b0101"> : !smt.bv<4> | ||
| #smt.bv<"#x5c"> : !smt.bv<8> | ||
| ``` |
There was a problem hiding this comment.
Is there a reason we want this compared to #smt.bv<15> : !smt.bv<8> ?
I feel that this removes the "complexity" of choosing between #x and #b, and this follows better what MLIR integer attributes, and hw.constant is doing?
There was a problem hiding this comment.
I think I just went for this syntax for the more SMT-like feel, but using regular decimal numbers is also a good approach. It's probably just a matter of taste. The only disadvantages of using regular decimals I see are
- bit-vector width cannot be inferred from the constant, i.e., we need the explicit type annotation:
smt.bv.constant #smt.bv<5> : !smt.bv<8>vssmt.bv.constant "#x05"which basically means we always need thequantifiedversion of the attribute in any operation assembly formats, on the other hand it saves typing a lot of zeros for big bit-vectors just storing small numbers - need to do some APInt
zextandtruncwith sanity checks, i.e., we just replace the complexity with some other complexity - I don't really understand why MLIR doesn't allow integer constants of the format
0b1010which is the most basic way of representing bit-vectors
There was a problem hiding this comment.
I might disagree with the first point, because while #x05 is easy to read and to understand, I cannot tell you from a glance what's the bitwidth of #b010101010101101100011101010, so having an explicit bitwidth makes a lot of sense to me!
What is the difference with zext and trunc? My understanding is that this would be the same? At least, I do not recommend changing the storage of #smt.bv.
And I would agree for the third point, though the problem is knowing when to use that format, and when to use the decimal format.
There was a problem hiding this comment.
When parsing an APInt, the bitwidth does not necessarily match the one required for the given bitvector type and has to be adjusted in the attribute parser with sext and trunc and before truncating it should be checked if the truncated bits are significant/meaningful. The storage of #smt.bv is the autogenerated one with just a single APInt since that stores both the value and the bitwidth.
maerhart
force-pushed
the
maerhart-smt-bitvector-constants
branch
2 times, most recently
from
52b0d1c
to
7d80fd8
Compare
| %c5_bv32 = smt.bv.constant #smt.bv<5> : !smt.bv<32> {smt.some_attr} | ||
| // CHECK: %c92_bv8 = smt.bv.constant #smt.bv<92> : !smt.bv<8> {smt.some_attr} | ||
| %c92_bv8 = smt.bv.constant #smt.bv<0x5c> : !smt.bv<8> {smt.some_attr} | ||
| // CHECK: %c-1_bv8 = smt.bv.constant #smt.bv<-1> : !smt.bv<8> |
There was a problem hiding this comment.
I'm also wondering, should we print this as -1, or should we print this as 255?
I do not have a good answer, but that's probably a question we should ask ourselves.
There was a problem hiding this comment.
I just went with the same as the HW dialect does. In the end it's a signless bitvector, whether we interpret it here as a signed or unsigned value is probably equally good or bad.
maerhart
force-pushed
the
maerhart-smt-bitvector-constants
branch
from
7d80fd8
to
228bfdf
Compare
To clearly separate semantics, define a bit-vector type and attribute instead of reusing the built-in integer attribute. The built-in integer is usually encoded using two SMT bit-vectors to model poison and the regular bit values.
Stacked PR, only review top commit.