diff options
| -rw-r--r-- | test/analysis/range.py | 96 | ||||
| -rwxr-xr-x | test/test_all.py | 3 |
2 files changed, 99 insertions, 0 deletions
diff --git a/test/analysis/range.py b/test/analysis/range.py new file mode 100644 index 00000000..4cc27f2c --- /dev/null +++ b/test/analysis/range.py @@ -0,0 +1,96 @@ +from miasm2.expression.expression import * +from miasm2.analysis.expression_range import expr_range +from miasm2.ir.translators import Translator +import z3 + +trans = Translator.to_language("z3") +a = ExprId("a", 8) +b = ExprId("b", 32) + +for expr in [ + a, + b, + b[4:6], + a + ExprInt8(4), + ExprInt8(5) + ExprInt8(4), + a.zeroExtend(32) + ExprInt32(0x100), + (a.zeroExtend(32) * ExprInt32(3)) + ExprInt32(0x100), + (a.zeroExtend(32) + ExprInt32(0x80)) * ExprInt32(3), + ExprCond(b, a.zeroExtend(32) + ExprInt32(0x100), + a.zeroExtend(32) + ExprInt32(0x500)), + ExprCond(b[1:2], a.zeroExtend(32), a.zeroExtend(32) + ExprInt32(0x1000)) + \ + ExprCond(b[0:1], a.zeroExtend(32) + ExprInt32(0x5000), a.zeroExtend(32) + ExprInt32(0x10000)), + - a, + - ExprInt8(4), + b[:8].zeroExtend(16) - ExprInt16(4), + a[4:6].zeroExtend(32) + ExprInt32(-1), + a >> ExprInt8(4), + a << ExprInt8(4), + ExprOp("a>>", a, ExprInt8(4)), + ExprInt8(4) >> a, + ExprInt8(4) << a, + ExprOp("a>>", ExprInt8(4), a), + a >> a, + a << a, + ExprOp("a>>", a, a), + ExprInt8(4) >> ExprCond(b[0:1], ExprInt8(1), ExprInt8(10)), + ExprInt8(4) << ExprCond(b[0:1], ExprInt8(1), ExprInt8(10)), + ExprOp("a>>", ExprInt8(4), ExprCond(b[0:1], ExprInt8(1), ExprInt8(10))), + a | ExprInt8(4), + a[3:5] | a[6:8], + ExprInt8(0) | a, + ExprInt8(0xF) | ExprInt8(0xC), + ExprCond(a[0:1], ExprInt8(5), ExprInt8(18)) | a[5:7].zeroExtend(8), + a & ExprInt8(4), + a[3:5] & a[6:8], + ExprInt8(8) & a, + ExprInt8(0xF) & ExprInt8(0xC), + ExprCond(a[0:1], ExprInt8(5), ExprInt8(18)) & (a[4:7].zeroExtend(8) << ExprInt8(2)), + a ^ ExprInt8(4), + a[3:5] ^ a[6:8], + ExprInt8(0xF) ^ a, + ExprInt8(0xF) ^ ExprInt8(0xC), + ExprCond(a[0:1], ExprInt8(5), ExprInt8(18)) ^ (a[4:7].zeroExtend(8) << ExprInt8(2)), + a % ExprInt8(8), + ExprInt8(33) % ExprInt8(8), + a % a, + a[:2].zeroExtend(8) + ExprInt8(0xF) % ExprCond(a[0:1], ExprInt8(5), ExprInt8(18)), + ExprOp("<<<", ExprInt8(4), ExprInt8(1)), + ExprOp("<<<", ExprInt8(4), ExprInt8(14)), + ExprOp("<<<", ExprInt8(4), a), + ExprOp("<<<", a, ExprInt8(4)), + ExprOp("<<<", a, a), + ExprOp("<<<", a[1:2].zeroExtend(8) + ExprInt8(1), ExprCond(a[0:1], ExprInt8(5), ExprInt8(18))), + ExprOp(">>>", ExprInt8(4), ExprInt8(1)), + ExprOp(">>>", ExprInt8(4), ExprInt8(14)), + ExprOp(">>>", ExprInt8(4), a), + ExprOp(">>>", a, ExprInt8(4)), + ExprOp(">>>", a, a), + ExprOp(">>>", a[1:2].zeroExtend(8) + ExprInt8(1), ExprCond(a[0:1], ExprInt8(5), ExprInt8(18))), + + # Fuzzed by ExprRandom, with previous bug + ExprSlice(ExprSlice(ExprOp('<<<', ExprInt(0x7FBE84D6, 51), ExprId('WYBZj', 51)), 6, 48), 3, 35), + ExprOp('>>>', ExprOp('-', ExprOp('&', ExprInt(0x347384F7, 32), ExprId('oIkka', 32), ExprId('jSfOB', 32), ExprId('dUXBp', 32), ExprInt(0x7169DEAA, 32))), ExprId('kMVuR', 32)), + ExprOp('|', ExprInt(0x94A3AB47, 32), ExprCompose(ExprId('dTSkf', 21), ExprOp('>>', ExprInt(0x24, 8), ExprId('HTHES', 8)), ExprId('WHNIZ', 1), ExprMem(ExprInt(0x100, 9), 1), ExprId('kPQck', 1))), + ExprOp('<<<', ExprOp('<<<', ExprCompose(ExprId('OOfuB', 6), ExprInt(0x24, 11), ExprInt(0xE8C, 12), ExprId('jbUWR', 1), ExprInt(0x2, 2)), ExprId('mLlTH', 32)), ExprInt(0xE600B6B2, 32)), + +]: + computed_range = expr_range(expr) + print expr, computed_range + + # Trivia checks + assert all(x[1] < (1 << expr.size) for x in computed_range) + + # Check against z3 + s = z3.Solver() + cond = [] + + ## Constraint expr to be in computed intervals + z3_expr = trans.from_expr(expr) + for mini, maxi in computed_range: + cond.append(z3.And(z3.ULE(mini, z3_expr), + z3.ULE(z3_expr, maxi))) + + ## Ask for a solution outside intervals (should not exists) + s.add(z3.Not(z3.Or(*cond))) + assert s.check() == z3.unsat diff --git a/test/test_all.py b/test/test_all.py index 41a62e25..706b3c16 100755 --- a/test/test_all.py +++ b/test/test_all.py @@ -240,6 +240,7 @@ for script in ["modint.py", "expression_helper.py", ]: testset += RegressionTest([script], base_dir="expression") + ## IR for script in ["symbexec.py", ]: @@ -272,6 +273,8 @@ testset += RegressionTest(["depgraph.py"], base_dir="analysis", (14, 1), (15, 1)) ]) testset += RegressionTest(["modularintervals.py"], base_dir="analysis") +testset += RegressionTest(["range.py"], base_dir="analysis", + tags=[TAGS["z3"]]) ## Degraph |