Llvm sem #130
Llvm sem #130
Conversation
| def srem? {w : Nat} (x y : BitVec w) : Option <| BitVec w := | ||
| if y.toInt = 0 | ||
| then none | ||
| else | ||
| let div := (x.toInt / y.toInt) | ||
| if div < Int.ofNat (2^w) | ||
| then some $ BitVec.ofInt w (x.toInt.rem y.toInt) | ||
| else none |
There was a problem hiding this comment.
This should be reviewed carefully, but I lack the mental acuity today to do so. I'm postponing this to tomorrow, I'm afraid :)
| then none | ||
| else | ||
| let div := (x.toInt / y.toInt) | ||
| if div < Int.ofNat (2^w) |
There was a problem hiding this comment.
Do we not need to check overflow on the negative side as well?
| if div < Int.ofNat (2^w) | |
| if div < Int.ofNat (2^w) && div >= - (Int.ofNat (2^w)) |
There was a problem hiding this comment.
@bollu good point! but then it should be < intMin or > intMax, right? (in particular, that's 2^(w-1), no?)
There was a problem hiding this comment.
You're right, in 2s complement, something of width w goes from
| then none | ||
| else | ||
| let div := (x.toInt / y.toInt) | ||
| if div < Int.ofNat (2^w) |
There was a problem hiding this comment.
Do we not need to check the other side of overflow as well?
| if div < Int.ofNat (2^w) | |
| if div < Int.ofNat (2^w) && div >= - (Int.ofNat (2^w)) |
Co-authored-by: Siddharth <[email protected]>
Co-authored-by: Siddharth <[email protected]>
yeah, ideally we should use the mlirnatural entry point and run a bunch of tests to compare with LLVM/MLIR. I'll add an issue for that. |
Check our denotation with the LLVM semantics (and document those).
The only thing I'm not 100% sure is what happens with constants when they exceed the bitwidth (will check that with examples later)