diff options
Diffstat (limited to 'test')
| -rw-r--r-- | test/arch/arm/sem.py | 4 | ||||
| -rw-r--r-- | test/arch/msp430/sem.py | 2 | ||||
| -rw-r--r-- | test/arch/x86/sem.py | 2 | ||||
| -rw-r--r-- | test/expression/expression.py | 8 | ||||
| -rw-r--r-- | test/expression/expression_helper.py | 5 | ||||
| -rw-r--r-- | test/expression/simplifications.py | 178 | ||||
| -rw-r--r-- | test/ir/symbexec.py | 30 | ||||
| -rw-r--r-- | test/ir/translators/z3_ir.py | 2 |
8 files changed, 112 insertions, 119 deletions
diff --git a/test/arch/arm/sem.py b/test/arch/arm/sem.py index feef7372..8fc609fb 100644 --- a/test/arch/arm/sem.py +++ b/test/arch/arm/sem.py @@ -29,7 +29,7 @@ def compute(asm, inputstate={}, debug=False): instr = mn.dis(code, "l") instr.offset = inputstate.get(PC, 0) interm.add_instr(instr) - symexec.emul_ir_blocs(interm, instr.offset) + symexec.emul_ir_blocks(instr.offset) if debug: for k, v in symexec.symbols.items(): if regs_init.get(k, None) != v: @@ -285,7 +285,7 @@ class TestARMSemantic(unittest.TestCase): self.assertEqual(compute('AND R4, R4, R5 LSR 2 ', {R4: 0xFFFFFFFF, R5: 0x80000041, }), {R4: 0x20000010, R5: 0x80000041, }) self.assertEqual(compute('AND R4, R4, R5 ASR 3 ', {R4: 0xF00000FF, R5: 0x80000081, }), {R4: 0xF0000010, R5: 0x80000081, }) self.assertEqual(compute('AND R4, R4, R5 ROR 4 ', {R4: 0xFFFFFFFF, R5: 0x000000FF, }), {R4: 0xF000000F, R5: 0x000000FF, }) - self.assertEqual(compute('AND R4, R4, R5 RRX ', {R4: 0xFFFFFFFF, R5: 0x00000101, }), {R4: ExprCompose([(ExprInt(0x80, 31),0,31), (cf_init,31,32)]), R5: 0x00000101, }) + self.assertEqual(compute('AND R4, R4, R5 RRX ', {R4: 0xFFFFFFFF, R5: 0x00000101, }), {R4: ExprCompose(ExprInt(0x80, 31), cf_init), R5: 0x00000101, }) # §A8.8.15: AND{S}{<c>}{<q>} {<Rd>,} <Rn>, <Rm>, <type> <Rs> self.assertEqual(compute('AND R4, R6, R4 LSL R5', {R4: 0x00000001, R5: 0x00000004, R6: -1, }), {R4: 0x00000010, R5: 0x00000004, R6: 0xFFFFFFFF, }) diff --git a/test/arch/msp430/sem.py b/test/arch/msp430/sem.py index 2488d633..515b4c53 100644 --- a/test/arch/msp430/sem.py +++ b/test/arch/msp430/sem.py @@ -27,7 +27,7 @@ def compute(asm, inputstate={}, debug=False): instr = mn.dis(code, mode) instr.offset = inputstate.get(PC, 0) interm.add_instr(instr) - symexec.emul_ir_blocs(interm, instr.offset) + symexec.emul_ir_blocks(instr.offset) if debug: for k, v in symexec.symbols.items(): if regs_init.get(k, None) != v: diff --git a/test/arch/x86/sem.py b/test/arch/x86/sem.py index 617b929b..7cf81828 100644 --- a/test/arch/x86/sem.py +++ b/test/arch/x86/sem.py @@ -26,7 +26,7 @@ def symb_exec(interm, inputstate, debug): sympool = dict(regs_init) sympool.update(inputstate) symexec = symbexec(interm, sympool) - symexec.emul_ir_blocs(interm, 0) + symexec.emul_ir_blocks(0) if debug: for k, v in symexec.symbols.items(): if regs_init.get(k, None) != v: diff --git a/test/expression/expression.py b/test/expression/expression.py index 90236744..847ba7eb 100644 --- a/test/expression/expression.py +++ b/test/expression/expression.py @@ -30,10 +30,10 @@ for expr in [ A + cst1, A + ExprCond(cond1, cst1, cst2), ExprCond(cond1, cst1, cst2) + ExprCond(cond2, cst3, cst4), - ExprCompose([(A, 0, 32), (cst1, 32, 64)]), - ExprCompose([(ExprCond(cond1, cst1, cst2), 0, 32), (A, 32, 64)]), - ExprCompose([(ExprCond(cond1, cst1, cst2), 0, 32), - (ExprCond(cond2, cst3, cst4), 32, 64)]), + ExprCompose(A, cst1), + ExprCompose(ExprCond(cond1, cst1, cst2), A), + ExprCompose(ExprCond(cond1, cst1, cst2), + ExprCond(cond2, cst3, cst4)), ExprCond(ExprCond(cond1, cst1, cst2), cst3, cst4), ]: print "*" * 80 diff --git a/test/expression/expression_helper.py b/test/expression/expression_helper.py index 514a9a51..a3a8fba4 100644 --- a/test/expression/expression_helper.py +++ b/test/expression/expression_helper.py @@ -16,11 +16,10 @@ class TestExpressionExpressionHelper(unittest.TestCase): ebx = m2_expr.ExprId("EBX") ax = eax[0:16] expr = eax + ebx - expr = m2_expr.ExprCompose([(ax, 0, 16), (expr[16:32], 16, 32)]) + expr = m2_expr.ExprCompose(ax, expr[16:32]) expr2 = m2_expr.ExprMem((eax + ebx) ^ (eax), size=16) expr2 = expr2 | ax | expr2 | cst - exprf = expr - expr + m2_expr.ExprCompose([(expr2, 0, 16), - (cst, 16, 32)]) + exprf = expr - expr + m2_expr.ExprCompose(expr2, cst) # Identify variables vi = Variables_Identifier(exprf) diff --git a/test/expression/simplifications.py b/test/expression/simplifications.py index 99cc7c35..bf658a30 100644 --- a/test/expression/simplifications.py +++ b/test/expression/simplifications.py @@ -24,11 +24,9 @@ i2 = ExprInt(uint32(0x2)) icustom = ExprInt(uint32(0x12345678)) cc = ExprCond(a, b, c) -o = ExprCompose([(a[:8], 8, 16), - (a[8:16], 0, 8)]) +o = ExprCompose(a[8:16], a[:8]) -o2 = ExprCompose([(a[8:16], 0, 8), - (a[:8], 8, 16)]) +o2 = ExprCompose(a[8:16], a[:8]) l = [a[:8], b[:8], c[:8], m[:8], s, i1[:8], i2[:8], o[:8]] l2 = l[::-1] @@ -93,11 +91,11 @@ to_test = [(ExprInt32(1) - ExprInt32(1), ExprInt32(0)), (a[8:16][:8], a[8:16]), (a[8:32][:8], a[8:16]), (a[:16][8:16], a[8:16]), - (ExprCompose([(a, 0, 32)]), a), - (ExprCompose([(a[:16], 0, 16)]), a[:16]), - (ExprCompose([(a[:16], 0, 16), (a[:16], 16, 32)]), - ExprCompose([(a[:16], 0, 16), (a[:16], 16, 32)]),), - (ExprCompose([(a[:16], 0, 16), (a[16:32], 16, 32)]), a), + (ExprCompose(a), a), + (ExprCompose(a[:16]), a[:16]), + (ExprCompose(a[:16], a[:16]), + ExprCompose(a[:16], a[:16]),), + (ExprCompose(a[:16], a[16:32]), a), (ExprMem(a)[:32], ExprMem(a)), (ExprMem(a)[:16], ExprMem(a, size=16)), @@ -106,14 +104,12 @@ to_test = [(ExprInt32(1) - ExprInt32(1), ExprInt32(0)), (ExprCond(ExprInt32(0), b, a), a), (ExprInt32(0x80000000)[31:32], ExprInt1(1)), - (ExprCompose([ - (ExprInt16(0x1337)[ - :8], 0, 8), (ExprInt16(0x1337)[8:16], 8, 16)]), + (ExprCompose(ExprInt16(0x1337)[:8], ExprInt16(0x1337)[8:16]), ExprInt16(0x1337)), - (ExprCompose([(ExprInt32(0x1337beef)[8:16], 8, 16), - (ExprInt32(0x1337beef)[:8], 0, 8), - (ExprInt32(0x1337beef)[16:32], 16, 32)]), + (ExprCompose(ExprInt32(0x1337beef)[:8], + ExprInt32(0x1337beef)[8:16], + ExprInt32(0x1337beef)[16:32]), ExprInt32(0x1337BEEF)), (ExprCond(a, ExprCond(a, @@ -122,9 +118,9 @@ to_test = [(ExprInt32(1) - ExprInt32(1), ExprInt32(0)), d), ExprCond(a, b, d)), ((a & b & ExprInt32(0x12))[31:32], ExprInt1(0)), - (ExprCompose([ - (ExprCond(a, ExprInt16(0x10), ExprInt16(0x20)), 0, 16), - (ExprInt16(0x1337), 16, 32)]), + (ExprCompose( + ExprCond(a, ExprInt16(0x10), ExprInt16(0x20)), + ExprInt16(0x1337)), ExprCond(a, ExprInt32(0x13370010), ExprInt32(0x13370020))), (ExprCond(ExprCond(a, ExprInt1(0), ExprInt1(1)), b, c), ExprCond(a, c, b)), @@ -167,103 +163,99 @@ to_test = [(ExprInt32(1) - ExprInt32(1), ExprInt32(0)), (ExprOp('-', ExprInt8(1), ExprInt8(0)), ExprInt8(1)), - (ExprCompose([(a, 0, 32), (ExprInt32(0), 32, 64)]) << ExprInt64(0x20), - ExprCompose([(ExprInt32(0), 0, 32), (a, 32, 64)])), - (ExprCompose([(a, 0, 32), (ExprInt32(0), 32, 64)]) << ExprInt64(0x10), - ExprCompose([(ExprInt16(0), 0, 16), (a, 16, 48), (ExprInt16(0), 48, 64)])), - (ExprCompose([(a, 0, 32), (ExprInt32(0), 32, 64)]) << ExprInt64(0x30), - ExprCompose([(ExprInt(0, 48), 0, 48), (a[:0x10], 48, 64)])), - (ExprCompose([(a, 0, 32), (ExprInt32(0), 32, 64)]) << ExprInt64(0x11), - ExprCompose([(ExprInt(0, 0x11), 0, 0x11), (a, 0x11, 0x31), (ExprInt(0, 0xF), 0x31, 0x40)])), - (ExprCompose([(a, 0, 32), (ExprInt32(0), 32, 64)]) << ExprInt64(0x40), + (ExprCompose(a, ExprInt32(0)) << ExprInt64(0x20), + ExprCompose(ExprInt32(0), a)), + (ExprCompose(a, ExprInt32(0)) << ExprInt64(0x10), + ExprCompose(ExprInt16(0), a, ExprInt16(0))), + (ExprCompose(a, ExprInt32(0)) << ExprInt64(0x30), + ExprCompose(ExprInt(0, 48), a[:0x10])), + (ExprCompose(a, ExprInt32(0)) << ExprInt64(0x11), + ExprCompose(ExprInt(0, 0x11), a, ExprInt(0, 0xF))), + (ExprCompose(a, ExprInt32(0)) << ExprInt64(0x40), ExprInt64(0)), - (ExprCompose([(a, 0, 32), (ExprInt32(0), 32, 64)]) << ExprInt64(0x50), + (ExprCompose(a, ExprInt32(0)) << ExprInt64(0x50), ExprInt64(0)), - (ExprCompose([(ExprInt32(0), 0, 32), (a, 32, 64)]) >> ExprInt64(0x20), - ExprCompose([(a, 0, 32), (ExprInt32(0), 32, 64)])), - (ExprCompose([(ExprInt32(0), 0, 32), (a, 32, 64)]) >> ExprInt64(0x10), - ExprCompose([(ExprInt16(0), 0, 16), (a, 16, 48), (ExprInt16(0), 48, 64)])), - (ExprCompose([(ExprInt32(0), 0, 32), (a, 32, 64)]) >> ExprInt64(0x30), - ExprCompose([(a[0x10:], 0, 16), (ExprInt(0, 48), 16, 64)])), - (ExprCompose([(ExprInt32(0), 0, 32), (a, 32, 64)]) >> ExprInt64(0x11), - ExprCompose([(ExprInt(0, 0xf), 0, 0xf), (a, 0xf, 0x2f), (ExprInt(0, 0x11), 0x2f, 0x40)])), - (ExprCompose([(ExprInt32(0), 0, 32), (a, 32, 64)]) >> ExprInt64(0x40), + (ExprCompose(ExprInt32(0), a) >> ExprInt64(0x20), + ExprCompose(a, ExprInt32(0))), + (ExprCompose(ExprInt32(0), a) >> ExprInt64(0x10), + ExprCompose(ExprInt16(0), a, ExprInt16(0))), + (ExprCompose(ExprInt32(0), a) >> ExprInt64(0x30), + ExprCompose(a[0x10:], ExprInt(0, 48))), + (ExprCompose(ExprInt32(0), a) >> ExprInt64(0x11), + ExprCompose(ExprInt(0, 0xf), a, ExprInt(0, 0x11))), + (ExprCompose(ExprInt32(0), a) >> ExprInt64(0x40), ExprInt64(0)), - (ExprCompose([(ExprInt32(0), 0, 32), (a, 32, 64)]) >> ExprInt64(0x50), + (ExprCompose(ExprInt32(0), a) >> ExprInt64(0x50), ExprInt64(0)), - (ExprCompose([(a, 0, 32), (b, 32, 64)]) << ExprInt64(0x20), - ExprCompose([(ExprInt32(0), 0, 32), (a, 32, 64)])), - (ExprCompose([(a, 0, 32), (b, 32, 64)]) << ExprInt64(0x10), - ExprCompose([(ExprInt16(0), 0, 16), (a, 16, 48), (b[:16], 48, 64)])), + (ExprCompose(a, b) << ExprInt64(0x20), + ExprCompose(ExprInt32(0), a)), + (ExprCompose(a, b) << ExprInt64(0x10), + ExprCompose(ExprInt16(0), a, b[:16])), - (ExprCompose([(a, 0, 32), (b, 32, 64)]) | ExprCompose([(c, 0, 32), (d, 32, 64)]), - ExprCompose([(a|c, 0, 32), (b|d, 32, 64)])), - (ExprCompose([(a, 0, 32), (ExprInt32(0), 32, 64)]) | ExprCompose([(ExprInt32(0), 0, 32), (d, 32, 64)]), - ExprCompose([(a, 0, 32), (d, 32, 64)])), - (ExprCompose([(f[:32], 0, 32), (ExprInt32(0), 32, 64)]) | ExprCompose([(ExprInt32(0), 0, 32), (f[32:], 32, 64)]), + (ExprCompose(a, b) | ExprCompose(c, d), + ExprCompose(a|c, b|d)), + (ExprCompose(a, ExprInt32(0)) | ExprCompose(ExprInt32(0), d), + ExprCompose(a, d)), + (ExprCompose(f[:32], ExprInt32(0)) | ExprCompose(ExprInt32(0), f[32:]), f), - ((ExprCompose([(a, 0, 32), (ExprInt32(0), 32, 64)]) * ExprInt64(0x123))[32:64], - (ExprCompose([(a, 0, 32), (ExprInt32(0), 32, 64)]) * ExprInt64(0x123))[32:64]), + ((ExprCompose(a, ExprInt32(0)) * ExprInt64(0x123))[32:64], + (ExprCompose(a, ExprInt32(0)) * ExprInt64(0x123))[32:64]), (ExprInt32(0x12), ExprInt32(0x12L)), - (ExprCompose(((a, 0, 32), (b, 32, 64), (c, 64, 96)))[:16], + (ExprCompose(a, b, c)[:16], a[:16]), - (ExprCompose(((a, 0, 32), (b, 32, 64), (c, 64, 96)))[16:32], + (ExprCompose(a, b, c)[16:32], a[16:]), - (ExprCompose(((a, 0, 32), (b, 32, 64), (c, 64, 96)))[32:48], + (ExprCompose(a, b, c)[32:48], b[:16]), - (ExprCompose(((a, 0, 32), (b, 32, 64), (c, 64, 96)))[48:64], + (ExprCompose(a, b, c)[48:64], b[16:]), - (ExprCompose(((a, 0, 32), (b, 32, 64), (c, 64, 96)))[64:80], + (ExprCompose(a, b, c)[64:80], c[:16]), - (ExprCompose(((a, 0, 32), (b, 32, 64), (c, 64, 96)))[80:], + (ExprCompose(a, b, c)[80:], c[16:]), - (ExprCompose(((a, 0, 32), (b, 32, 64), (c, 64, 96)))[80:82], + (ExprCompose(a, b, c)[80:82], c[16:18]), - (ExprCompose(((a, 0, 32), (b, 32, 64), (c, 64, 96)))[16:48], - ExprCompose(((a[16:], 0, 16), (b[:16], 16, 32)))), - (ExprCompose(((a, 0, 32), (b, 32, 64), (c, 64, 96)))[48:80], - ExprCompose(((b[16:], 0, 16), (c[:16], 16, 32)))), - - (ExprCompose(((a[0:8], 0, 8), - (b[8:16], 8, 16), - (ExprInt(uint48(0x0L)), 16, 64)))[12:32], - ExprCompose(((b[12:16], 0, 4), (ExprInt(uint16(0)), 4, 20))) + (ExprCompose(a, b, c)[16:48], + ExprCompose(a[16:], b[:16])), + (ExprCompose(a, b, c)[48:80], + ExprCompose(b[16:], c[:16])), + + (ExprCompose(a[0:8], b[8:16], ExprInt(uint48(0x0L)))[12:32], + ExprCompose(b[12:16], ExprInt(uint16(0))) ), - (ExprCompose(((ExprCompose(((a[:8], 0, 8), - (ExprInt(uint56(0x0L)), 8, 64)))[8:32] - & - ExprInt(uint24(0x1L)), 0, 24), - (ExprInt(uint40(0x0L)), 24, 64))), + (ExprCompose(ExprCompose(a[:8], ExprInt(uint56(0x0L)))[8:32] + & + ExprInt(uint24(0x1L)), + ExprInt(uint40(0x0L))), ExprInt64(0)), - (ExprCompose(((ExprCompose(((a[:8], 0, 8), - (ExprInt(uint56(0x0L)), 8, 64)))[:8] - & - ExprInt(uint8(0x1L)), 0, 8), - (ExprInt(uint56(0x0L)), 8, 64))), - ExprCompose(((a[:8]&ExprInt8(1), 0, 8), (ExprInt(uint56(0)), 8, 64)))), - - (ExprCompose(((ExprCompose(((a[:8], 0, 8), - (ExprInt(uint56(0x0L)), 8, 64)))[:32] - & - ExprInt(uint32(0x1L)), 0, 32), - (ExprInt(uint32(0x0L)), 32, 64))), - ExprCompose(((ExprCompose(((ExprSlice(a, 0, 8), 0, 8), - (ExprInt(uint24(0x0L)), 8, 32))) - & - ExprInt(uint32(0x1L)), 0, 32), - (ExprInt(uint32(0x0L)), 32, 64))) + (ExprCompose(ExprCompose(a[:8], ExprInt(uint56(0x0L)))[:8] + & + ExprInt(uint8(0x1L)), + (ExprInt(uint56(0x0L)))), + ExprCompose(a[:8]&ExprInt8(1), ExprInt(uint56(0)))), + + (ExprCompose(ExprCompose(a[:8], + ExprInt(uint56(0x0L)))[:32] + & + ExprInt(uint32(0x1L)), + ExprInt(uint32(0x0L))), + ExprCompose(ExprCompose(ExprSlice(a, 0, 8), + ExprInt(uint24(0x0L))) + & + ExprInt(uint32(0x1L)), + ExprInt(uint32(0x0L))) ), - (ExprCompose([(a[:16], 0, 16), (b[:16], 16, 32)])[8:32], - ExprCompose([(a[8:16], 0, 8), (b[:16], 8, 24)])), + (ExprCompose(a[:16], b[:16])[8:32], + ExprCompose(a[8:16], b[:16])), ((a >> ExprInt32(16))[:16], a[16:32]), ((a >> ExprInt32(16))[8:16], @@ -410,10 +402,10 @@ match_tests = [ (MatchExpr(ExprCond(x, y, z), ExprCond(a, b, c), [a, b, c]), {a: x, b: y, c: z}), - (MatchExpr(ExprCompose([(x[:8], 0, 8), (y[:8], 8, 16)]), a, [a]), - {a: ExprCompose([(x[:8], 0, 8), (y[:8], 8, 16)])}), - (MatchExpr(ExprCompose([(x[:8], 0, 8), (y[:8], 8, 16)]), - ExprCompose([(a[:8], 0, 8), (b[:8], 8, 16)]), [a, b]), + (MatchExpr(ExprCompose(x[:8], y[:8]), a, [a]), + {a: ExprCompose(x[:8], y[:8])}), + (MatchExpr(ExprCompose(x[:8], y[:8]), + ExprCompose(a[:8], b[:8]), [a, b]), {a: x, b: y}), (MatchExpr(e1, e2, [b]), {b: ExprInt32(0x10)}), (MatchExpr(e3, diff --git a/test/ir/symbexec.py b/test/ir/symbexec.py index 9165fccb..6df0bbc3 100644 --- a/test/ir/symbexec.py +++ b/test/ir/symbexec.py @@ -21,7 +21,7 @@ class TestSymbExec(unittest.TestCase): addr40 = ExprInt32(40) addr50 = ExprInt32(50) mem0 = ExprMem(addr0) - mem1 = ExprMem(addr1) + mem1 = ExprMem(addr1, 8) mem8 = ExprMem(addr8) mem9 = ExprMem(addr9) mem20 = ExprMem(addr20) @@ -34,22 +34,24 @@ class TestSymbExec(unittest.TestCase): id_a = ExprId('a') id_eax = ExprId('eax_init') - e = symbexec( - ir_x86_32(), {mem0: id_x, mem1: id_y, mem9: id_x, mem40w: id_x, mem50v: id_y, id_a: addr0, id_eax: addr0}) + e = symbexec(ir_x86_32(), + {mem0: id_x, mem1: id_y, mem9: id_x, + mem40w: id_x[:16], mem50v: id_y, + id_a: addr0, id_eax: addr0}) self.assertEqual(e.find_mem_by_addr(addr0), mem0) self.assertEqual(e.find_mem_by_addr(addrX), None) - self.assertEqual(e.eval_ExprMem(ExprMem(addr1 - addr1)), id_x) - self.assertEqual(e.eval_ExprMem(ExprMem(addr1, 8)), id_y) - self.assertEqual(e.eval_ExprMem(ExprMem(addr1 + addr1)), ExprCompose( - [(id_x[16:32], 0, 16), (ExprMem(ExprInt32(4), 16), 16, 32)])) - self.assertEqual(e.eval_ExprMem(mem8), ExprCompose( - [(id_x[0:24], 0, 24), (ExprMem(ExprInt32(11), 8), 24, 32)])) - self.assertEqual(e.eval_ExprMem(mem40v), id_x[:8]) - self.assertEqual(e.eval_ExprMem(mem50w), ExprCompose( - [(id_y, 0, 8), (ExprMem(ExprInt32(51), 8), 8, 16)])) - self.assertEqual(e.eval_ExprMem(mem20), mem20) + self.assertEqual(e.eval_expr(ExprMem(addr1 - addr1)), id_x) + self.assertEqual(e.eval_expr(ExprMem(addr1, 8)), id_y) + self.assertEqual(e.eval_expr(ExprMem(addr1 + addr1)), ExprCompose( + id_x[16:32], ExprMem(ExprInt32(4), 16))) + self.assertEqual(e.eval_expr(mem8), ExprCompose( + id_x[0:24], ExprMem(ExprInt32(11), 8))) + self.assertEqual(e.eval_expr(mem40v), id_x[:8]) + self.assertEqual(e.eval_expr(mem50w), ExprCompose( + id_y, ExprMem(ExprInt32(51), 8))) + self.assertEqual(e.eval_expr(mem20), mem20) e.func_read = lambda x: x - self.assertEqual(e.eval_ExprMem(mem20), mem20) + self.assertEqual(e.eval_expr(mem20), mem20) self.assertEqual(set(e.modified()), set(e.symbols)) self.assertRaises( KeyError, e.symbols.__getitem__, ExprMem(ExprInt32(100))) diff --git a/test/ir/translators/z3_ir.py b/test/ir/translators/z3_ir.py index e080c7f5..5fcfe25e 100644 --- a/test/ir/translators/z3_ir.py +++ b/test/ir/translators/z3_ir.py @@ -114,7 +114,7 @@ check_interp(model[memb.get_mem_array(32)], [(0xdeadbeef, 0), (0xdeadbeef + 3, 2)]) # -------------------------------------------------------------------------- -e5 = ExprSlice(ExprCompose(((e, 0, 32), (four, 32, 64))), 0, 32) * five +e5 = ExprSlice(ExprCompose(e, four), 0, 32) * five ez3 = Translator.to_language('z3').from_expr(e5) z3_e5 = z3.Extract(31, 0, z3.Concat(z3_four, z3_e)) * z3_five |