Merge pull request #496 from commial/feature/expr_range

Feature/expr range

4 files changed, 253 insertions, 0 deletions

diff --git a/test/analysis/modularintervals.py b/test/analysis/modularintervals.py
new file mode 100644
index 00000000..36a29aa8
--- /dev/null
+++ b/test/analysis/modularintervals.py
@@ -0,0 +1,149 @@
+from random import shuffle, seed
+
+from miasm2.core.interval import interval
+from miasm2.analysis.modularintervals import ModularIntervals
+from miasm2.expression.expression import *
+from miasm2.expression.simplifications import expr_simp
+
+
+def gen_all_intervals(size):
+    """Return every possible interval for element of @size bit
+    -> 2**(2**size) (number of partition)
+    """
+    nb_elements = 1 << size
+    for bvec in xrange(1 << nb_elements):
+        # Bit vector: if bit i is on, i is in the interval
+        to_ret = interval()
+        for i in xrange(nb_elements):
+            if bvec & i == i:
+                to_ret += [(i, i)]
+        yield to_ret
+
+def interval_elements(interv):
+    """Generator on element of an interval"""
+    for sub_range in interv:
+        for i in xrange(sub_range[0], sub_range[1] + 1):
+            yield i
+
+size = 4
+left, right = list(gen_all_intervals(size)), list(gen_all_intervals(size))
+right_int = range(1 << size)
+mask = (1 << size) - 1
+
+def test(left, right):
+    """Launch tests on left OP right"""
+    global size, mask
+
+    for left_i in left:
+        left_i = ModularIntervals(size, left_i)
+        left_values = list(interval_elements(left_i))
+
+        # Check operations without other arguments
+        ## Check NEG
+        result = - left_i
+        for x in left_values:
+            rez = (- x) & mask
+            assert rez in result
+
+        # Check operations on intervals
+        for right_i in right:
+            right_i = ModularIntervals(size, right_i)
+            right_values = list(interval_elements(right_i))
+
+            # Check operations available only on integer
+            if len(right_values) == 1:
+                # Check mod
+                value = right_values[0]
+                # Avoid division by zero
+                if value != 0:
+                    result = left_i % value
+                    for x in left_values:
+                        rez = (x % value) & mask
+                        assert rez in result
+
+            # Check ADD
+            result = left_i + right_i
+            for x in left_values:
+                for y in right_values:
+                    rez = (x + y) & mask
+                    assert rez in result
+
+            # Check OR
+            result = left_i | right_i
+            for x in left_values:
+                for y in right_values:
+                    rez = (x | y) & mask
+                    assert rez in result
+
+            # Check AND
+            result = left_i & right_i
+            for x in left_values:
+                for y in right_values:
+                    rez = (x & y) & mask
+                    assert rez in result
+
+            # Check XOR
+            result = left_i ^ right_i
+            for x in left_values:
+                for y in right_values:
+                    rez = (x ^ y) & mask
+                    assert rez in result
+
+            # Check >>
+            result = left_i >> right_i
+            for x in left_values:
+                for y in right_values:
+                    rez = (x >> y) & mask
+                    assert rez in result
+
+            # Check <<
+            result = left_i << right_i
+            for x in left_values:
+                for y in right_values:
+                    rez = (x << y) & mask
+                    assert rez in result
+
+            # Check a>>
+            result = left_i.arithmetic_shift_right(right_i)
+            for x in left_values:
+                x = ExprInt(x, size)
+                for y in right_values:
+                    y = ExprInt(y, size)
+                    rez = int(expr_simp(ExprOp('a>>', x, y)))
+                    assert rez in result
+
+            # Check >>>
+            result = left_i.rotation_right(right_i)
+            for x in left_values:
+                x = ExprInt(x, size)
+                for y in right_values:
+                    y = ExprInt(y, size)
+                    rez = int(expr_simp(ExprOp('>>>', x, y)))
+                    assert rez in result
+
+            # Check <<<
+            result = left_i.rotation_left(right_i)
+            for x in left_values:
+                x = ExprInt(x, size)
+                for y in right_values:
+                    y = ExprInt(y, size)
+                    rez = int(expr_simp(ExprOp('<<<', x, y)))
+                    assert rez in result
+
+
+
+# Following tests take around 10 minutes with PyPy, but too long for Python
+# interval_uniq = [interval([(i, i)]) for i in xrange(1 << size)]
+# test(left, interval_uniq)
+# test(interval_uniq, right)
+
+# Uncomment the following line for a full test over intervals, which may take
+# several hours
+# test(left, right)
+
+# Random pick for tests
+seed(0)
+shuffle(left)
+shuffle(right)
+
+test(left[:100], right[:100])
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/core/interval.py b/test/core/interval.py
index ab18e567..97d45a39 100755
--- a/test/core/interval.py
+++ b/test/core/interval.py
@@ -90,6 +90,10 @@ assert(i14 & i15 == i14)
 assert(i15 & i14 == i14)
 assert(i14 & i16 == interval([(3, 5), (7, 8)]))
 
+assert(i5.length == 5)
+assert(i6.length == 7)
+assert((i1 - i1).length == 0)
+
 x1 = [(7, 87), (76, 143), (94, 129), (79, 89), (46, 100)]
 assert(interval(x1) == interval([(7, 143)]))
 x2 = [(11, 16), (35, 74), (18, 114), (91, 188), (3, 75)]
diff --git a/test/test_all.py b/test/test_all.py
index 86d40bcb..0c9a0c08 100755
--- a/test/test_all.py
+++ b/test/test_all.py
@@ -241,6 +241,7 @@ for script in ["modint.py",
                "expression_helper.py",
                ]:
     testset += RegressionTest([script], base_dir="expression")
+
 ## IR
 for script in ["symbexec.py",
                ]:
@@ -272,6 +273,9 @@ testset += RegressionTest(["depgraph.py"], base_dir="analysis",
                                                      (12, 1), (13, 1),
                                                      (14, 1), (15, 1))
                            ])
+testset += RegressionTest(["modularintervals.py"], base_dir="analysis")
+testset += RegressionTest(["range.py"], base_dir="analysis",
+                          tags=[TAGS["z3"]])
 
 
 ## Degraph