From a8ece9f5c56334c37caafb9eddcd38081d6b4464 Mon Sep 17 00:00:00 2001 From: Florent Monjalet Date: Mon, 23 Mar 2015 23:16:29 +0100 Subject: TranslatorZ3: Handling 'parity' and '-' unary operators, and raising errors properly for other unhandled operators. --- test/ir/translators/z3_ir.py | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) (limited to 'test/ir/translators/z3_ir.py') diff --git a/test/ir/translators/z3_ir.py b/test/ir/translators/z3_ir.py index 997a3da9..99d77c5a 100644 --- a/test/ir/translators/z3_ir.py +++ b/test/ir/translators/z3_ir.py @@ -119,5 +119,21 @@ ez3 = Translator.to_language('z3').from_expr(e5) z3_e5 = z3.Extract(31, 0, z3.Concat(z3_four, z3_e)) * z3_five assert equiv(ez3, z3_e5) +# -------------------------------------------------------------------------- +# Parity +for miasm_int, res in [(five, 1), (four, 0)]: + e6 = ExprOp('parity', miasm_int) + ez3 = Translator.to_language('z3').from_expr(e6) + z3_e6 = z3.BitVecVal(res, 1) + assert equiv(ez3, z3_e6) + +# -------------------------------------------------------------------------- +# '-' +for miasm_int, res in [(five, -5), (four, -4)]: + e6 = ExprOp('-', miasm_int) + ez3 = Translator.to_language('z3').from_expr(e6) + z3_e6 = z3.BitVecVal(res, 32) + assert equiv(ez3, z3_e6) + print "TranslatorZ3 tests are OK." -- cgit 1.4.1 From 001472b1cd3c89ebf60a86d29ae7d843d5e453db Mon Sep 17 00:00:00 2001 From: Florent Monjalet Date: Tue, 24 Mar 2015 00:16:03 +0100 Subject: TranslatorZ3: Fixed parity semantic --- miasm2/ir/translators/z3_ir.py | 5 ++++- test/ir/translators/z3_ir.py | 4 +++- 2 files changed, 7 insertions(+), 2 deletions(-) (limited to 'test/ir/translators/z3_ir.py') diff --git a/miasm2/ir/translators/z3_ir.py b/miasm2/ir/translators/z3_ir.py index 04ed9332..564670a6 100644 --- a/miasm2/ir/translators/z3_ir.py +++ b/miasm2/ir/translators/z3_ir.py @@ -167,7 +167,10 @@ class TranslatorZ3(Translator): else: raise NotImplementedError("Unsupported OP yet: %s" % expr.op) elif expr.op == 'parity': - res = z3.Extract(0, 0, res) + arg = z3.Extract(7, 0, res) + res = z3.BitVecVal(1, 1) + for i in xrange(8): + res = res ^ z3.Extract(i, i, arg) elif expr.op == '-': res = -res else: diff --git a/test/ir/translators/z3_ir.py b/test/ir/translators/z3_ir.py index 99d77c5a..5f8f3e45 100644 --- a/test/ir/translators/z3_ir.py +++ b/test/ir/translators/z3_ir.py @@ -121,7 +121,9 @@ assert equiv(ez3, z3_e5) # -------------------------------------------------------------------------- # Parity -for miasm_int, res in [(five, 1), (four, 0)]: +seven = ExprInt32(7) +one0seven = ExprInt32(0x107) +for miasm_int, res in [(five, 1), (four, 0), (seven, 0), (one0seven, 0)]: e6 = ExprOp('parity', miasm_int) ez3 = Translator.to_language('z3').from_expr(e6) z3_e6 = z3.BitVecVal(res, 1) -- cgit 1.4.1 From c8590c5985292d02e2989fac530ea2d3a30535f1 Mon Sep 17 00:00:00 2001 From: Florent Monjalet Date: Tue, 24 Mar 2015 00:24:37 +0100 Subject: TranslatorZ3: Fixed from_ExprId when expr.name is an asmlabel TODO: replace the asmlabel str by its offset? --- miasm2/ir/translators/z3_ir.py | 2 +- test/ir/translators/z3_ir.py | 6 ++++++ 2 files changed, 7 insertions(+), 1 deletion(-) (limited to 'test/ir/translators/z3_ir.py') diff --git a/miasm2/ir/translators/z3_ir.py b/miasm2/ir/translators/z3_ir.py index 564670a6..db038fe1 100644 --- a/miasm2/ir/translators/z3_ir.py +++ b/miasm2/ir/translators/z3_ir.py @@ -117,7 +117,7 @@ class TranslatorZ3(Translator): @classmethod def from_ExprId(cls, expr): - return z3.BitVec(expr.name, expr.size) + return z3.BitVec(str(expr), expr.size) @classmethod def from_ExprMem(cls, expr): diff --git a/test/ir/translators/z3_ir.py b/test/ir/translators/z3_ir.py index 5f8f3e45..fa656ed0 100644 --- a/test/ir/translators/z3_ir.py +++ b/test/ir/translators/z3_ir.py @@ -1,5 +1,6 @@ import z3 +from miasm2.core.asmbloc import asm_label from miasm2.expression.expression import * from miasm2.ir.translators.translator import Translator from miasm2.ir.translators.z3_ir import TranslatorZ3, Z3Mem @@ -137,5 +138,10 @@ for miasm_int, res in [(five, -5), (four, -4)]: z3_e6 = z3.BitVecVal(res, 32) assert equiv(ez3, z3_e6) +# -------------------------------------------------------------------------- +# Should just not throw anything +e7 = ExprId(asm_label("label_histoire", 0xdeadbeef), 32) +ez3 = Translator.to_language('z3').from_expr(e7) + print "TranslatorZ3 tests are OK." -- cgit 1.4.1 From a326cba3e548313a947594370bc97b879a27c63b Mon Sep 17 00:00:00 2001 From: Florent Monjalet Date: Tue, 24 Mar 2015 00:36:58 +0100 Subject: TranslatorZ3: Better handling of asm_labels (translating to BitVecVal when possible) --- miasm2/ir/translators/z3_ir.py | 6 +++++- test/ir/translators/z3_ir.py | 8 +++++++- 2 files changed, 12 insertions(+), 2 deletions(-) (limited to 'test/ir/translators/z3_ir.py') diff --git a/miasm2/ir/translators/z3_ir.py b/miasm2/ir/translators/z3_ir.py index db038fe1..6f0b1aef 100644 --- a/miasm2/ir/translators/z3_ir.py +++ b/miasm2/ir/translators/z3_ir.py @@ -3,6 +3,7 @@ import operator import z3 +from miasm2.core.asmbloc import asm_label from miasm2.ir.translators.translator import Translator log = logging.getLogger("translator_z3") @@ -117,7 +118,10 @@ class TranslatorZ3(Translator): @classmethod def from_ExprId(cls, expr): - return z3.BitVec(str(expr), expr.size) + if isinstance(expr.name, asm_label) and expr.name.offset is not None: + return z3.BitVecVal(expr.name.offset, expr.size) + else: + return z3.BitVec(str(expr), expr.size) @classmethod def from_ExprMem(cls, expr): diff --git a/test/ir/translators/z3_ir.py b/test/ir/translators/z3_ir.py index fa656ed0..6e483d61 100644 --- a/test/ir/translators/z3_ir.py +++ b/test/ir/translators/z3_ir.py @@ -139,9 +139,15 @@ for miasm_int, res in [(five, -5), (four, -4)]: assert equiv(ez3, z3_e6) # -------------------------------------------------------------------------- -# Should just not throw anything e7 = ExprId(asm_label("label_histoire", 0xdeadbeef), 32) ez3 = Translator.to_language('z3').from_expr(e7) +z3_e7 = z3.BitVecVal(0xdeadbeef, 32) +assert equiv(ez3, z3_e7) + +# Should just not throw anything to pass +e8 = ExprId(asm_label("label_jambe"), 32) +ez3 = Translator.to_language('z3').from_expr(e8) +assert not equiv(ez3, z3_e7) print "TranslatorZ3 tests are OK." -- cgit 1.4.1