Conversation
agle
left a comment
agle
left a comment
There was a problem hiding this comment.
Good work, its probably a good idea to also check in your documentation pdf under /docs as well
lib/analysis/known_bits.ml
Outdated
| if Bitvec.is_nonzero bm then Top | ||
| else tnum (Bitvec.ashr av bv) (Bitvec.shl am bv)) | ||
|
|
||
| let mul = |
There was a problem hiding this comment.
Worth commenting which version of mul you implemented and why
There was a problem hiding this comment.
the algorithm was tweaked to be written in ocaml so it has recursive calls and cases that follows final version of mul as given in the paper but it takes inspiration from other implementations as well
i have explained it more in the comments but lmk if i should change anything there
lib/analysis/known_bits.ml
Outdated
| let bitLSHR = | ||
| bind2 (fun (av, am) (bv, bm) -> | ||
| if Bitvec.is_nonzero bm then Top | ||
| else tnum (Bitvec.lshr av bv) (Bitvec.shl am bv)) |
There was a problem hiding this comment.
Shouldn't the mask be logically shifted right here? (and same for ashr)
I suspect that the property test didn't catch this because it occurs in an edge case for when bm is zero
There was a problem hiding this comment.
omg you are so right sorry gng mb
3 participants
This domain of tnums (tristate numbers) is used to reason about the bitwise uncertainty in program values.