steakhal accepted this revision.
steakhal added a comment.
This revision is now accepted and ready to land.
I like the change.
I also proved the equivalence, just for fun really :D
from z3 import *
def proof_equality(F, G):
s = Solver()
s.add(Not(F == G))
r = s.check()
if r == unsat:
print("proved")
else:
print("counterexample")
print(s.model())
Kind = BitVec('Kind', 32)
BaseMask = BitVecVal(0b11, 32)
BaseBits = BitVecVal(2, 32)
Before = (Kind & ~BaseMask) >> BaseBits
After = Kind >> BaseBits
proof_equality(Before, After)
# prints: proved
Repository:
rG LLVM Github Monorepo
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D85026/new/
https://reviews.llvm.org/D85026
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
