diff options
| -rw-r--r-- | miasm2/analysis/expression_range.py | 65 | ||||
| -rw-r--r-- | miasm2/analysis/modularintervals.py | 499 | ||||
| -rw-r--r-- | miasm2/core/interval.py | 8 | ||||
| -rw-r--r-- | miasm2/expression/simplifications_common.py | 2 | ||||
| -rw-r--r-- | test/analysis/modularintervals.py | 149 | ||||
| -rw-r--r-- | test/analysis/range.py | 96 | ||||
| -rwxr-xr-x | test/core/interval.py | 4 | ||||
| -rwxr-xr-x | test/test_all.py | 4 |
8 files changed, 826 insertions, 1 deletions
diff --git a/miasm2/analysis/expression_range.py b/miasm2/analysis/expression_range.py new file mode 100644 index 00000000..ca63588c --- /dev/null +++ b/miasm2/analysis/expression_range.py @@ -0,0 +1,65 @@ +"""Naive range analysis for expression""" + +from miasm2.analysis.modularintervals import ModularIntervals + +_op_range_handler = { + "+": lambda x, y: x + y, + "&": lambda x, y: x & y, + "|": lambda x, y: x | y, + "^": lambda x, y: x ^ y, + ">>": lambda x, y: x >> y, + "a>>": lambda x, y: x.arithmetic_shift_right(y), + "<<": lambda x, y: x << y, + ">>": lambda x, y: x >> y, + ">>>": lambda x, y: x.rotation_right(y), + "<<<": lambda x, y: x.rotation_left(y), +} + +def expr_range(expr): + """Return a ModularIntervals containing the range of possible values of + @expr""" + max_bound = (1 << expr.size) - 1 + if expr.is_int(): + return ModularIntervals(expr.size, [(int(expr), int(expr))]) + elif expr.is_id() or expr.is_mem(): + return ModularIntervals(expr.size, [(0, max_bound)]) + elif expr.is_slice(): + interval_mask = ((1 << expr.start) - 1) ^ ((1 << expr.stop) - 1) + arg = expr_range(expr.arg) + # Mask for possible range, and shift range + return ((arg & interval_mask) >> expr.start).size_update(expr.size) + elif expr.is_compose(): + sub_ranges = [expr_range(arg) for arg in expr.args] + args_idx = [info[0] for info in expr.iter_args()] + + # No shift for the first one + ret = sub_ranges[0].size_update(expr.size) + + # Doing it progressively (2 by 2) + for shift, sub_range in zip(args_idx[1:], sub_ranges[1:]): + ret |= sub_range.size_update(expr.size) << shift + return ret + elif expr.is_op(): + # A few operation are handled with care + # Otherwise, overapproximate (ie. full range interval) + if expr.op in _op_range_handler: + sub_ranges = [expr_range(arg) for arg in expr.args] + return reduce(_op_range_handler[expr.op], + (sub_range for sub_range in sub_ranges[1:]), + sub_ranges[0]) + elif expr.op == "-": + assert len(expr.args) == 1 + return - expr_range(expr.args[0]) + elif expr.op == "%": + assert len(expr.args) == 2 + op, mod = [expr_range(arg) for arg in expr.args] + if mod.intervals.length == 1: + # Modulo intervals is not supported + return op % mod.intervals.hull()[0] + + # Operand not handled, return the full domain + return ModularIntervals(expr.size, [(0, max_bound)]) + elif expr.is_cond(): + return expr_range(expr.src1).union(expr_range(expr.src2)) + else: + raise TypeError("Unsupported type: %s" % expr.__class__) diff --git a/miasm2/analysis/modularintervals.py b/miasm2/analysis/modularintervals.py new file mode 100644 index 00000000..0752f57b --- /dev/null +++ b/miasm2/analysis/modularintervals.py @@ -0,0 +1,499 @@ +"""Intervals with a maximum size, supporting modular arithmetic""" +from itertools import product + +from miasm2.core.interval import interval + +class ModularIntervals(object): + """Intervals with a maximum size, supporting modular arithmetic""" + + def __init__(self, size, intervals=None): + """Instanciate a ModularIntervals of size @size + @size: maximum size of elements + @intervals: (optional) interval instance, or any type supported by + interval initialisation; element of the current instance + """ + # Create or cast @intervals argument + if intervals is None: + intervals = interval() + if not isinstance(intervals, interval): + intervals = interval(intervals) + self.intervals = intervals + self.size = size + + # Sanity check + start, end = intervals.hull() + assert end <= self.mask + assert start >= 0 + + # Helpers + + @staticmethod + def size2mask(size): + """Return the bit mask of size @size""" + return (1 << size) - 1 + + def _range2interval(func): + """Convert a function taking 2 ranges to a function taking a ModularIntervals + and applying to the current instance""" + def ret_func(self, target): + ret = interval() + for left_i, right_i in product(self.intervals, target.intervals): + ret += func(self, left_i[0], left_i[1], right_i[0], + right_i[1]) + return self.__class__(self.size, ret) + return ret_func + + def _range2integer(func): + """Convert a function taking 1 range and optional arguments to a function + applying to the current instance""" + def ret_func(self, *args): + ret = interval() + for x_min, x_max in self.intervals: + ret += func(self, x_min, x_max, *args) + return self.__class__(self.size, ret) + return ret_func + + def _promote(func): + """Check and promote the second argument from integer to + ModularIntervals with one value""" + def ret_func(self, target): + if isinstance(target, (int, long)): + target = ModularIntervals(self.size, interval([(target, target)])) + if not isinstance(target, ModularIntervals): + raise TypeError("Unsupported operation with %s" % target.__class__) + if target.size != self.size: + raise TypeError("Size are not the same: %s vs %s" % (self.size, + target.size)) + return func(self, target) + return ret_func + + def _unsigned2signed(self, value): + """Return the signed value of @value, based on self.size""" + if (value & (1 << (self.size - 1))): + return -(self.mask ^ value) - 1 + else: + return value + + def _signed2unsigned(self, value): + """Return the unsigned value of @value, based on self.size""" + return value & self.mask + + # Operation internals + # + # Naming convention: + # _range_{op}: takes 2 interval bounds and apply op + # _range_{op}_uniq: takes 1 interval bounds and apply op + # _interval_{op}: apply op on an ModularIntervals + # _integer_{op}: apply op on itself with possible arguments + + def _range_add(self, x_min, x_max, y_min, y_max): + """Bounds interval for x + y, with + - x, y of size 'self.size' + - @x_min <= x <= @x_max + - @y_min <= y <= @y_max + - operations are considered unsigned + From Hacker's Delight: Chapter 4 + """ + max_bound = self.mask + if (x_min + y_min <= max_bound and + x_max + y_max >= max_bound + 1): + # HD returns 0, max_bound; but this is because it cannot handle multiple + # interval. + # x_max + y_max can only overflow once, so returns + # [result_min, overflow] U [0, overflow_rest] + return interval([(x_min + y_min, max_bound), + (0, (x_max + y_max) & max_bound)]) + else: + return interval([((x_min + y_min) & max_bound, + (x_max + y_max) & max_bound)]) + + _interval_add = _range2interval(_range_add) + + def _range_minus_uniq(self, x_min, x_max): + """Bounds interval for -x, with + - x of size self.size + - @x_min <= x <= @x_max + - operations are considered unsigned + From Hacker's Delight: Chapter 4 + """ + max_bound = self.mask + if (x_min == 0 and x_max != 0): + # HD returns 0, max_bound; see _range_add + return interval([(0, 0), ((- x_max) & max_bound, max_bound)]) + else: + return interval([((- x_max) & max_bound, (- x_min) & max_bound)]) + + _interval_minus = _range2integer(_range_minus_uniq) + + def _range_or_min(self, x_min, x_max, y_min, y_max): + """Interval min for x | y, with + - x, y of size self.size + - @x_min <= x <= @x_max + - @y_min <= y <= @y_max + - operations are considered unsigned + From Hacker's Delight: Chapter 4 + """ + max_bit = 1 << (self.size - 1) + while max_bit: + if ~x_min & y_min & max_bit: + temp = (x_min | max_bit) & - max_bit + if temp <= x_max: + x_min = temp + break + elif x_min & ~y_min & max_bit: + temp = (y_min | max_bit) & - max_bit + if temp <= y_max: + y_min = temp + break + max_bit >>= 1 + return x_min | y_min + + def _range_or_max(self, x_min, x_max, y_min, y_max): + """Interval max for x | y, with + - x, y of size self.size + - @x_min <= x <= @x_max + - @y_min <= y <= @y_max + - operations are considered unsigned + From Hacker's Delight: Chapter 4 + """ + max_bit = 1 << (self.size - 1) + while max_bit: + if x_max & y_max & max_bit: + temp = (x_max - max_bit) | (max_bit - 1) + if temp >= x_min: + x_max = temp + break + temp = (y_max - max_bit) | (max_bit - 1) + if temp >= y_min: + y_max = temp + break + max_bit >>= 1 + return x_max | y_max + + def _range_or(self, x_min, x_max, y_min, y_max): + """Interval bounds for x | y, with + - x, y of size self.size + - @x_min <= x <= @x_max + - @y_min <= y <= @y_max + - operations are considered unsigned + From Hacker's Delight: Chapter 4 + """ + return interval([(self._range_or_min(x_min, x_max, y_min, y_max), + self._range_or_max(x_min, x_max, y_min, y_max))]) + + _interval_or = _range2interval(_range_or) + + def _range_and_min(self, x_min, x_max, y_min, y_max): + """Interval min for x & y, with + - x, y of size self.size + - @x_min <= x <= @x_max + - @y_min <= y <= @y_max + - operations are considered unsigned + From Hacker's Delight: Chapter 4 + """ + max_bit = (1 << (self.size - 1)) + while max_bit: + if ~x_min & ~y_min & max_bit: + temp = (x_min | max_bit) & - max_bit + if temp <= x_max: + x_min = temp + break + temp = (y_min | max_bit) & - max_bit + if temp <= y_max: + y_min = temp + break + max_bit >>= 1 + return x_min & y_min + + def _range_and_max(self, x_min, x_max, y_min, y_max): + """Interval max for x & y, with + - x, y of size self.size + - @x_min <= x <= @x_max + - @y_min <= y <= @y_max + - operations are considered unsigned + From Hacker's Delight: Chapter 4 + """ + max_bit = (1 << (self.size - 1)) + while max_bit: + if x_max & ~y_max & max_bit: + temp = (x_max & ~max_bit) | (max_bit - 1) + if temp >= x_min: + x_max = temp + break + elif ~x_max & y_max & max_bit: + temp = (y_max & ~max_bit) | (max_bit - 1) + if temp >= y_min: + y_max = temp + break + max_bit >>= 1 + return x_max & y_max + + def _range_and(self, x_min, x_max, y_min, y_max): + """Interval bounds for x & y, with + - x, y of size @size + - @x_min <= x <= @x_max + - @y_min <= y <= @y_max + - operations are considered unsigned + From Hacker's Delight: Chapter 4 + """ + return interval([(self._range_and_min(x_min, x_max, y_min, y_max), + self._range_and_max(x_min, x_max, y_min, y_max))]) + + _interval_and = _range2interval(_range_and) + + def _range_xor(self, x_min, x_max, y_min, y_max): + """Interval bounds for x ^ y, with + - x, y of size self.size + - @x_min <= x <= @x_max + - @y_min <= y <= @y_max + - operations are considered unsigned + From Hacker's Delight: Chapter 4 + """ + not_size = lambda x: x ^ self.mask + min_xor = self._range_and_min(x_min, x_max, not_size(y_max), not_size(y_min)) | self._range_and_min(not_size(x_max), not_size(x_min), y_min, y_max) + max_xor = self._range_or_max(0, + self._range_and_max(x_min, x_max, not_size(y_max), not_size(y_min)), + 0, + self._range_and_max(not_size(x_max), not_size(x_min), y_min, y_max)) + return interval([(min_xor, max_xor)]) + + _interval_xor = _range2interval(_range_xor) + + def _range_mod_uniq(self, x_min, x_max, mod): + """Interval bounds for x % @mod, with + - x, @mod of size self.size + - @x_min <= x <= @x_max + - operations are considered unsigned + """ + if (x_max - x_min) >= mod: + return interval([(0, mod - 1)]) + x_max = x_max % mod + x_min = x_min % mod + if x_max < x_min: + return interval([(0, x_max), (x_min, mod - 1)]) + else: + return interval([(x_min, x_max)]) + + _integer_modulo = _range2integer(_range_mod_uniq) + + def _range_shift_uniq(self, x_min, x_max, shift, op): + """Bounds interval for x @op @shift with + - x of size self.size + - @x_min <= x <= @x_max + - operations are considered unsigned + - shift <= self.size + """ + assert shift <= self.size + # Shift operations are monotonic, and overflow results in 0 + max_bound = self.mask + + if op == "<<": + obtain_max = x_max << shift + if obtain_max > max_bound: + # Overflow at least on max, best-effort + # result '0' often happen, include it + return interval([(0, 0), ((1 << shift) - 1, max_bound)]) + else: + return interval([(x_min << shift, obtain_max)]) + elif op == ">>": + return interval([((x_min >> shift) & max_bound, + (x_max >> shift) & max_bound)]) + elif op == "a>>": + # The Miasm2 version (Expr or ModInt) could have been used, but + # introduce unnecessary dependencies for this module + # Python >> is the arithmetic one + ashr = lambda x, y: self._signed2unsigned(self._unsigned2signed(x) >> y) + end_min, end_max = ashr(x_min, shift), ashr(x_max, shift) + end_min, end_max = min(end_min, end_max), max(end_min, end_max) + return interval([(end_min, end_max)]) + else: + raise ValueError("%s is not a shifter" % op) + + def _interval_shift(self, operation, shifter): + """Apply the shifting operation @operation with a shifting + ModularIntervals @shifter on the current instance""" + # Work on a copy of shifter intervals + shifter = interval(shifter.intervals) + if (shifter.hull()[1] >= self.size): + shifter += interval([(self.size, self.size)]) + shifter &= interval([(0, self.size)]) + ret = interval() + for shift_range in shifter: + for shift in xrange(shift_range[0], shift_range[1] + 1): + for x_min, x_max in self.intervals: + ret += self._range_shift_uniq(x_min, x_max, shift, operation) + return self.__class__(self.size, ret) + + def _range_rotate_uniq(self, x_min, x_max, shift, op): + """Bounds interval for x @op @shift with + - x of size self.size + - @x_min <= x <= @x_max + - operations are considered unsigned + - shift <= self.size + """ + assert shift <= self.size + # Divide in sub-operations: a op b: a left b | a right (size - b) + if op == ">>>": + left, right = ">>", "<<" + elif op == "<<<": + left, right = "<<", ">>" + else: + raise ValueError("Not a rotator: %s" % op) + + left_intervals = self._range_shift_uniq(x_min, x_max, shift, left) + right_intervals = self._range_shift_uniq(x_min, x_max, + self.size - shift, right) + + result = self.__class__(self.size, left_intervals) | self.__class__(self.size, right_intervals) + return result.intervals + + def _interval_rotate(self, operation, shifter): + """Apply the rotate operation @operation with a shifting + ModularIntervals @shifter on the current instance""" + # Consider only rotation without repetition, and enumerate + # -> apply a '% size' on shifter + shifter %= self.size + ret = interval() + for shift_range in shifter: + for shift in xrange(shift_range[0], shift_range[1] + 1): + for x_min, x_max in self.intervals: + ret += self._range_rotate_uniq(x_min, x_max, shift, + operation) + + return self.__class__(self.size, ret) + + # Operation wrappers + + @_promote + def __add__(self, to_add): + """Add @to_add to the current intervals + @to_add: ModularInstances or integer + """ + return self._interval_add(to_add) + + @_promote + def __or__(self, to_or): + """Bitwise OR @to_or to the current intervals + @to_or: ModularInstances or integer + """ + return self._interval_or(to_or) + + @_promote + def __and__(self, to_and): + """Bitwise AND @to_and to the current intervals + @to_and: ModularInstances or integer + """ + return self._interval_and(to_and) + + @_promote + def __xor__(self, to_xor): + """Bitwise XOR @to_xor to the current intervals + @to_or: ModularInstances or integer + """ + return self._interval_xor(to_xor) + + @_promote + def __rshift__(self, to_shift): + """Logical shift right the current intervals of @to_shift + @to_shift: ModularInstances or integer + """ + return self._interval_shift('>>', to_shift) + + @_promote + def __lshift__(self, to_shift): + """Logical shift left the current intervals of @to_shift + @to_shift: ModularInstances or integer + """ + return self._interval_shift('<<', to_shift) + + @_promote + def arithmetic_shift_right(self, to_shift): + """Arithmetic shift right the current intervals of @to_shift + @to_shift: ModularInstances or integer + """ + return self._interval_shift('a>>', to_shift) + + def __neg__(self): + """Negate the current intervals""" + return self._interval_minus() + + def __mod__(self, modulo): + """Apply % @modulo on the current intervals + @modulo: integer + """ + + if not isinstance(modulo, (int, long)): + raise TypeError("Modulo with %s is not supported" % modulo.__class__) + return self._integer_modulo(modulo) + + @_promote + def rotation_right(self, to_rotate): + """Right rotate the current intervals of @to_rotate + @to_rotate: ModularInstances or integer + """ + return self._interval_rotate('>>>', to_rotate) + + @_promote + def rotation_left(self, to_rotate): + """Left rotate the current intervals of @to_rotate + @to_rotate: ModularInstances or integer + """ + return self._interval_rotate('<<<', to_rotate) + + # Instance operations + + @property + def mask(self): + """Return the mask corresponding to the instance size""" + return ModularIntervals.size2mask(self.size) + + def __iter__(self): + return iter(self.intervals) + + def __contains__(self, other): + if isinstance(other, ModularIntervals): + other = other.intervals + return other in self.intervals + + def __str__(self): + return "%s (Size: %s)" % (self.intervals, self.size) + + def size_update(self, new_size): + """Update the instance size to @new_size + The size of elements must be <= @new_size""" + + # Increasing size is always safe + if new_size < self.size: + # Check that current values are indeed included in the new range + assert self.intervals.hull()[1] <= ModularIntervals.size2mask(new_size) + + self.size = new_size + + # For easy chainning + return self + + # Mimic Python's set operations + + @_promote + def union(self, to_union): + """Union set operation with @to_union + @to_union: ModularIntervals instance""" + return ModularIntervals(self.size, self.intervals + to_union.intervals) + + @_promote + def update(self, to_union): + """Union set operation in-place with @to_union + @to_union: ModularIntervals instance""" + self.intervals += to_union.intervals + + @_promote + def intersection(self, to_intersect): + """Intersection set operation with @to_intersect + @to_intersect: ModularIntervals instance""" + return ModularIntervals(self.size, self.intervals & to_intersect.intervals) + + @_promote + def intersection_update(self, to_intersect): + """Intersection set operation in-place with @to_intersect + @to_intersect: ModularIntervals instance""" + self.intervals &= to_intersect.intervals diff --git a/miasm2/core/interval.py b/miasm2/core/interval.py index 66445674..019764d4 100644 --- a/miasm2/core/interval.py +++ b/miasm2/core/interval.py @@ -244,3 +244,11 @@ class interval(object): if dry_run is False: img.show() + + @property + def length(self): + """ + Return the cumulated length of intervals + """ + # Do not use __len__ because we may return a value > 32 bits + return sum((stop - start + 1) for start, stop in self.intervals) diff --git a/miasm2/expression/simplifications_common.py b/miasm2/expression/simplifications_common.py index 4bd35390..503a0e77 100644 --- a/miasm2/expression/simplifications_common.py +++ b/miasm2/expression/simplifications_common.py @@ -44,7 +44,7 @@ def simp_cst_propagation(e_s, e): o = i1.arg << i2.arg elif op == 'a>>': x1 = mod_size2int[i1.arg.size](i1.arg) - x2 = mod_size2int[i2.arg.size](i2.arg) + x2 = mod_size2uint[i2.arg.size](i2.arg) o = mod_size2uint[i1.arg.size](x1 >> x2) elif op == '>>>': o = (i1.arg >> (i2.arg % i2.size) | 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 |