QQ: when bitblasting verification for asm, how do you handle insn w/ (conditionally) undefined result? (e.g., 0 shift, bsr, bsf)
-
Wouldn't want to just forbid such inputs… could ignore the result when undefined, mask out, etc. But can't assume any specific result :|
@pkhuong At old place, we'd typically carry a mask for defined/undefined register bits, memory, and flags. Full story too long for twitter.
-
-
@danluu I'm thinking of verification for superoptimisers… unclear how trustworthy w/o a final desk check. -
@pkhuong@danluu not exactly the same but we put a lot of work into getting UB right in Alive http://www.cs.utah.edu/~regehr/papers/pldi15.pdf …
End of conversation
New conversation -
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.