diff options
Diffstat (limited to 'test/ir')
| -rwxr-xr-x | test/ir/ir2C.py | 2 | ||||
| -rw-r--r-- | test/ir/translators/z3_ir.py | 32 |
2 files changed, 17 insertions, 17 deletions
diff --git a/test/ir/ir2C.py b/test/ir/ir2C.py index c84473c3..20ade999 100755 --- a/test/ir/ir2C.py +++ b/test/ir/ir2C.py @@ -38,7 +38,7 @@ class TestIrIr2C(unittest.TestCase): self.translationTest( ExprOp('-', *args[:2]), r'(((0x0&0xffffffff) - (0x1&0xffffffff))&0xffffffff)') self.translationTest( - ExprOp('bsr', *args[:1]), r'x86_bsr(0x0, 0x20)') + ExprOp('cntleadzeros', *args[:1]), r'cntleadzeros(0x0, 0x20)') self.translationTest( ExprOp('cpuid', *args[:2]), r'cpuid(0x0, 0x1)') self.translationTest( diff --git a/test/ir/translators/z3_ir.py b/test/ir/translators/z3_ir.py index 83744786..6ae2dcd0 100644 --- a/test/ir/translators/z3_ir.py +++ b/test/ir/translators/z3_ir.py @@ -150,22 +150,22 @@ ez3 = Translator.to_language('z3').from_expr(e8) assert not equiv(ez3, z3_e7) # -------------------------------------------------------------------------- -# bsr, bsf - -# bsf(0x1138) == 3 -bsf1 = Translator.to_language('z3').from_expr(ExprOp("bsf", ExprInt(0x1138, 32))) -bsf2 = z3.BitVecVal(3, 32) -assert(equiv(bsf1, bsf2)) - -# bsr(0x11300) == 0x10 -bsr1 = Translator.to_language('z3').from_expr(ExprOp("bsr", ExprInt(0x11300, 32))) -bsr2 = z3.BitVecVal(0x10, 32) -assert(equiv(bsr1, bsr2)) - -# bsf(0x80000) == bsr(0x80000) -bsf3 = Translator.to_language('z3').from_expr(ExprOp("bsf", ExprInt(0x80000, 32))) -bsr3 = Translator.to_language('z3').from_expr(ExprOp("bsr", ExprInt(0x80000, 32))) -assert(equiv(bsf3, bsr3)) +# cntleadzeros, cnttrailzeros + +# cnttrailzeros(0x1138) == 3 +cnttrailzeros1 = Translator.to_language('z3').from_expr(ExprOp("cnttrailzeros", ExprInt(0x1138, 32))) +cnttrailzeros2 = z3.BitVecVal(3, 32) +assert(equiv(cnttrailzeros1, cnttrailzeros2)) + +# cntleadzeros(0x11300) == 0xf +cntleadzeros1 = Translator.to_language('z3').from_expr(ExprOp("cntleadzeros", ExprInt(0x11300, 32))) +cntleadzeros2 = z3.BitVecVal(0xf, 32) +assert(equiv(cntleadzeros1, cntleadzeros2)) + +# cnttrailzeros(0x8000) + 1 == cntleadzeros(0x8000) +cnttrailzeros3 = Translator.to_language('z3').from_expr(ExprOp("cnttrailzeros", ExprInt(0x8000, 32)) + ExprInt(1, 32)) +cntleadzeros3 = Translator.to_language('z3').from_expr(ExprOp("cntleadzeros", ExprInt(0x8000, 32))) +assert(equiv(cnttrailzeros3, cntleadzeros3)) print "TranslatorZ3 tests are OK." |