diff options
| author | Fabrice Desclaux <fabrice.desclaux@cea.fr> | 2020-03-18 12:40:46 +0100 |
|---|---|---|
| committer | Fabrice Desclaux <fabrice.desclaux@cea.fr> | 2020-03-18 13:47:17 +0100 |
| commit | 173ec1d4d8f1a3df3c1ad8f55a0ac278fa2fc170 (patch) | |
| tree | 07537dd7a601593cf1e64462af6877f743956c90 | |
| parent | 8f83721c1f2c491e7ac2b62f82cd0c3ae57e5b27 (diff) | |
| download | miasm-173ec1d4d8f1a3df3c1ad8f55a0ac278fa2fc170.tar.gz miasm-173ec1d4d8f1a3df3c1ad8f55a0ac278fa2fc170.zip | |
Updt z3 version; update z3 api
| -rw-r--r-- | optional_requirements.txt | 2 | ||||
| -rw-r--r-- | test/ir/translators/smt2.py | 4 | ||||
| -rw-r--r-- | test/ir/translators/z3_ir.py | 17 |
3 files changed, 11 insertions, 12 deletions
diff --git a/optional_requirements.txt b/optional_requirements.txt index 88d09170..71ebdbe8 100644 --- a/optional_requirements.txt +++ b/optional_requirements.txt @@ -1,3 +1,3 @@ pycparser -z3-solver==4.5.1.0 +z3-solver==4.8.7.0 llvmlite==0.26.0 diff --git a/test/ir/translators/smt2.py b/test/ir/translators/smt2.py index 81f63b45..bf418f44 100644 --- a/test/ir/translators/smt2.py +++ b/test/ir/translators/smt2.py @@ -43,8 +43,8 @@ e_z3 = t_z3.from_expr(e) smt2 = t_smt2.to_smt2([t_smt2.from_expr(e)]) # parse smt2 string with z3 -smt2_z3 = parse_smt2_string(smt2) - +result = parse_smt2_string(smt2) +smt2_z3 = result[0] # initialise SMT solver s = Solver() diff --git a/test/ir/translators/z3_ir.py b/test/ir/translators/z3_ir.py index b28269fb..b96e43bb 100644 --- a/test/ir/translators/z3_ir.py +++ b/test/ir/translators/z3_ir.py @@ -24,13 +24,12 @@ def check_interp(interp, constraints, bits=32, valbits=8): constraints = dict((addr, z3.BitVecVal(val, valbits)) for addr, val in constraints) - l = interp.as_list() - for entry in l: - if not isinstance(entry, list) or len(entry) < 2: - continue - addr, value = entry[0], entry[1] - if addr.as_long() in constraints: - assert equiv(value, constraints[addr.as_long()]) + entry = interp.children() + assert len(entry) == 3 + _, addr, value = entry + addr = addr.as_long() + assert addr in constraints + assert equiv(value, constraints[addr]) # equiv short test # -------------------------------------------------------------------------- @@ -100,7 +99,7 @@ solver.add(ez3 == 10) solver.check() model = solver.model() check_interp(model[mem.get_mem_array(32)], - [(0xdeadbeef, 2), (0xdeadbeef + 3, 0)]) + [(0xdeadbeef, 2)]) # -------------------------------------------------------------------------- ez3 = translator2.from_expr(e4) @@ -116,7 +115,7 @@ solver.add(ez3 == 10) solver.check() model = solver.model() check_interp(model[memb.get_mem_array(32)], - [(0xdeadbeef, 0), (0xdeadbeef + 3, 2)]) + [(0xdeadbeef+3, 2)]) # -------------------------------------------------------------------------- e5 = ExprSlice(ExprCompose(e, four), 0, 32) * five |