diff options
Diffstat (limited to 'test')
| -rw-r--r-- | test/expression/simplifications.py | 9 | ||||
| -rwxr-xr-x | test/ir/ir2C.py | 2 | ||||
| -rw-r--r-- | test/ir/translators/z3_ir.py | 32 |
3 files changed, 26 insertions, 17 deletions
diff --git a/test/expression/simplifications.py b/test/expression/simplifications.py index 3e2e5177..a4e839cf 100644 --- a/test/expression/simplifications.py +++ b/test/expression/simplifications.py @@ -395,6 +395,15 @@ to_test = [(ExprInt(1, 32) - ExprInt(1, 32), ExprInt(0, 32)), ExprInt(0xc6, 8)), (ExprOp("imod", ExprInt(0x0123, 16), ExprInt(0xfffb, 16))[:8], ExprInt(0x01, 8)), + (ExprOp("cnttrailzeros", ExprInt(0x2, 32)), + ExprInt(0x1, 32)), + (ExprOp("cnttrailzeros", ExprInt(0x0, 32)), + ExprInt(0x20, 32)), + (ExprOp("cntleadzeros", ExprInt(0x2, 32)), + ExprInt(30, 32)), + (ExprOp("cntleadzeros", ExprInt(0x0, 32)), + ExprInt(0x20, 32)), + (ExprCompose(ExprInt(0x0123, 16), ExprMem(a + ExprInt(0x40, a.size), 16), ExprMem(a + ExprInt(0x42, a.size), 16), ExprInt(0x0321, 16)), 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." |