From 461da57ea3a9b30c20b52d7bcded863d680f3fcd Mon Sep 17 00:00:00 2001 From: feliam Date: Mon, 26 Feb 2018 21:09:34 -0300 Subject: [PATCH] Array value configurable. 8,16,32..256 bits (not prefixed to 8) (#732) * Array value configurable. 8,16,32..256 bits (not prefixed to 8) * Test Array256->256 * Remove old 8 bit assumptions * Add arrayProxy copy constructors and remove old 8 bit assumptions * remove old 8 bit assumptions * remove old 8 bit assumptions * Better ArrayProxy special case handling * Fix tests * Review fixes * review fix * fix gas variable * Review fixes * Fix vm.gas access --- manticore/core/smtlib/constraints.py | 41 ++++++------ manticore/core/smtlib/expression.py | 93 ++++++++++++++++++---------- manticore/core/smtlib/solver.py | 16 +---- manticore/core/smtlib/visitors.py | 5 ++ manticore/core/state.py | 2 +- manticore/platforms/evm.py | 19 +++--- manticore/platforms/linux.py | 6 +- tests/test_smtlibv2.py | 65 +++++++++++++++---- 8 files changed, 158 insertions(+), 89 deletions(-) diff --git a/manticore/core/smtlib/constraints.py b/manticore/core/smtlib/constraints.py index 15361fa..beb62b2 100644 --- a/manticore/core/smtlib/constraints.py +++ b/manticore/core/smtlib/constraints.py @@ -103,20 +103,20 @@ class ConstraintSet(object): elif isinstance(exp, Bool): result += '(declare-fun %s () Bool)' % name elif isinstance(exp, Array): - result += '(declare-fun %s () (Array (_ BitVec %d) (_ BitVec 8)))' % (name, exp.index_bits) + result += '(declare-fun %s () (Array (_ BitVec %d) (_ BitVec %d)))' % (name, exp.index_bits, exp.value_bits) else: raise Exception("Type not supported %r", exp) result += '(assert (= %s %s))\n' % (name, smtlib) - r = translator.pop() - while r is not None: - result += '(assert %s)\n' % r - r = translator.pop() + constraint_str = translator.pop() + while constraint_str is not None: + if constraint_str != 'true': + result += '(assert %s)\n' % constraint_str + constraint_str = translator.pop() logger.debug('Reduced %d constraints!!', N - len(related_constraints)) return result - #return str(self) #//result @property def declarations(self): @@ -163,23 +163,26 @@ class ConstraintSet(object): elif isinstance(exp, Bool): result += '(declare-fun %s () Bool)' % name elif isinstance(exp, Array): - result += '(declare-fun %s () (Array (_ BitVec %d) (_ BitVec 8)))' % (name, exp.index_bits) + result += '(declare-fun %s () (Array (_ BitVec %d) (_ BitVec %d)))' % (name, exp.index_bits, exp.value_bits) else: raise Exception("Type not supported %r", exp) result += '(assert (= %s %s))\n' % (name, smtlib) - r = translator.pop() - while r is not None: - result += '(assert %s)\n' % r - r = translator.pop() + constraint_str = translator.pop() + while constraint_str is not None: + if constraint_str != 'true': + result += '(assert %s)\n' % constraint_str + constraint_str = translator.pop() return result buf = '' for d in self.declarations: buf += d.declaration + '\n' - for a in self.constraints: - buf += '(assert %s)\n' % translate_to_smtlib(a, use_bindings=True) + for constraint in self.constraints: + constraint_str = translate_to_smtlib(constraint, use_bindings=True) + if constraint_str != 'true': + buf += '(assert %s)\n' % constraint_str return buf def _get_new_name(self, name='VAR'): @@ -206,16 +209,16 @@ class ConstraintSet(object): name = self._get_new_name(name) return BitVecVariable(size, name, taint=taint) - def new_array(self, index_bits=32, name='A', index_max=None, taint=frozenset()): - ''' Declares a free symbolic array of 8 bits long bitvectors in the constraint store. - :param index_bit_size: size in bits for the array indexes one of [32, 64] + def new_array(self, index_bits=32, name='A', index_max=None, value_bits=8, taint=frozenset()): + ''' Declares a free symbolic array of value_bits long bitvectors in the constraint store. + :param index_bits: size in bits for the array indexes one of [32, 64] + :param value_bits: size in bits for the array values :param name: try to assign name to internal variable representation, if not uniq a numeric nonce will be appended :param index_max: upper limit for indexes on ths array (#FIXME) - :return: a fresh BitVecVariable + :return: a fresh ArrayProxy ''' - assert index_bits in (8, 16, 32, 64, 128, 256) name = self._get_new_name(name) - return ArrayProxy(ArrayVariable(index_bits, index_max, name, taint=taint)) + return ArrayProxy(ArrayVariable(index_bits, index_max, value_bits, name, taint=taint)) diff --git a/manticore/core/smtlib/expression.py b/manticore/core/smtlib/expression.py index 35aa845..c09d85c 100644 --- a/manticore/core/smtlib/expression.py +++ b/manticore/core/smtlib/expression.py @@ -181,7 +181,6 @@ class BoolITE(BoolOperation): class BitVec(Expression): ''' This adds a bitsize to the Expression class ''' def __init__(self, size, *operands, **kwargs): - #assert size in (1, 8, 16, 32, 64, 128, 256) super(BitVec, self).__init__(*operands, **kwargs) self.size = size @@ -535,12 +534,14 @@ class UnsignedGreaterOrEqual(BoolOperation): ############################################################################### # Array BV32 -> BV8 or BV64 -> BV8 class Array(Expression): - def __init__(self, index_bits, index_max, *operands, **kwargs): + def __init__(self, index_bits, index_max, value_bits, *operands, **kwargs): assert index_bits in (32, 64, 256) + assert value_bits in (8, 16, 32, 64, 256) assert index_max is None or isinstance(index_max, (int, long)) assert index_max is None or index_max >= 0 and index_max < 2 ** index_bits self._index_bits = index_bits self._index_max = index_max + self._value_bits = value_bits super(Array, self).__init__(*operands, **kwargs) def cast_index(self, index): @@ -554,14 +555,23 @@ class Array(Expression): if isinstance(value, str) and len(value) == 1: value = ord(value) if isinstance(value, (int, long)): - return BitVecConstant(8, value) - assert isinstance(value, BitVec) and value.size == 8 + return BitVecConstant(self.value_bits, value) + assert isinstance(value, BitVec) and value.size == self.value_bits return value + def __len__(self): + if self.index_max is None: + raise Exception("Array max index not set") + return self.index_max + @property def index_bits(self): return self._index_bits + @property + def value_bits(self): + return self._value_bits + @property def index_max(self): return self._index_max @@ -572,30 +582,35 @@ class Array(Expression): def store(self, index, value): return ArrayStore(self, self.cast_index(index), self.cast_value(value)) - -class ArrayVariable(Array, Variable): - def __init__(self, index_bits, index_max, name, *operands, **kwargs): - super(ArrayVariable, self).__init__(index_bits, index_max, name, **kwargs) - - @property - def declaration(self): - return '(declare-fun %s () (Array (_ BitVec %d) (_ BitVec 8)))' % (self.name, self.index_bits) - def __getitem__(self, index): return ArraySelect(self, self.cast_index(index)) + @property + def underlying_variable(self): + array = self + while not isinstance(array, ArrayVariable): + array = array.array + return array + +class ArrayVariable(Array, Variable): + def __init__(self, index_bits, index_max, value_bits, name, *operands, **kwargs): + super(ArrayVariable, self).__init__(index_bits, index_max, value_bits, name, **kwargs) + + @property + def declaration(self): + return '(declare-fun %s () (Array (_ BitVec %d) (_ BitVec %d)))' % (self.name, self.index_bits, self.value_bits) class ArrayOperation(Array, Operation): def __init__(self, array, *operands, **kwargs): assert isinstance(array, Array) - super(ArrayOperation, self).__init__(array.index_bits, array.index_max, array, *operands, **kwargs) + super(ArrayOperation, self).__init__(array.index_bits, array.index_max, array.value_bits, array, *operands, **kwargs) class ArrayStore(ArrayOperation): def __init__(self, array, index, value, *args, **kwargs): assert isinstance(array, Array) assert isinstance(index, BitVec) and index.size == array.index_bits - assert isinstance(value, BitVec) and value.size == 8 + assert isinstance(value, BitVec) and value.size == array.value_bits super(ArrayStore, self).__init__(array, index, value, *args, **kwargs) @property @@ -616,14 +631,30 @@ class ArrayStore(ArrayOperation): class ArrayProxy(Array): def __init__(self, array): - assert isinstance(array, ArrayVariable) - super(ArrayProxy, self).__init__(array.index_bits, array.index_max) - self._array = array - self.name = array.name + assert isinstance(array, Array) + if isinstance (array, ArrayProxy): + #copy constructor + super(ArrayProxy, self).__init__(array.index_bits, array.index_max, array.value_bits) + self._array = array._array + self._name = array._name + elif isinstance(array, ArrayVariable): + #fresh array proxy + super(ArrayProxy, self).__init__(array.index_bits, array.index_max, array.value_bits) + self._array = array + self._name = array.name + else: + #arrayproxy for an prepopulated array + super(ArrayProxy, self).__init__(array.index_bits, array.index_max, array.value_bits) + self._name = array.underlying_variable.name + + @property + def array(self): + return self._array - def __len__(self): - return len(self._array) + @property + def name(self): + return self._name @property def operands(self): @@ -636,6 +667,10 @@ class ArrayProxy(Array): @property def index_max(self): return self._array.index_max + + @property + def value_bits(self): + return self._array.value_bits @property def taint(self): @@ -673,7 +708,7 @@ class ArrayProxy(Array): if isinstance(index, slice): start, stop = self._fix_index(index) size = self._get_size(index) - new_array = ArrayVariable(self.index_bits, size, name='%s_b%d_e%d'%(self.name, start, stop), taint=self.taint) + new_array = ArrayVariable(self.index_bits, size, self.value_bits, name='%s_b%d_e%d'%(self.name, start, stop), taint=self.taint) new_array = ArrayProxy(new_array) for i in xrange(size): if self.index_max is not None and not isinstance(i+start, Expression) and i+start >= self.index_max: @@ -688,7 +723,6 @@ class ArrayProxy(Array): return self._array.select(index) def __setitem__(self, index, value): - if isinstance(index, slice): start, stop = self._fix_index(index) size = self._get_size(index) @@ -698,10 +732,6 @@ class ArrayProxy(Array): else: self.store(index, value) - def __len__(self): - if self._array.index_max is None: - raise Exception() - return self._array.index_max def __getstate__(self): state = {} @@ -711,16 +741,17 @@ class ArrayProxy(Array): def __setstate__(self, state): self._array = state['_array'] - self.name = state['name'] - self._index_bits = self._array.index_bits - self._index_max = self._array.index_max + self._name = state['name'] + def __copy__(self): + return ArrayProxy(self) + class ArraySelect(BitVec, Operation): def __init__(self, array, index, *args, **kwargs): assert isinstance(array, Array) assert isinstance(index, BitVec) and index.size == array.index_bits - super(ArraySelect, self).__init__(8, array, index, *args, **kwargs) + super(ArraySelect, self).__init__(array.value_bits, array, index, *args, **kwargs) @property def array(self): diff --git a/manticore/core/smtlib/solver.py b/manticore/core/smtlib/solver.py index 03fc668..99884ee 100644 --- a/manticore/core/smtlib/solver.py +++ b/manticore/core/smtlib/solver.py @@ -452,20 +452,6 @@ class Z3Solver(Solver): The current set of assertions must be sat. :param val: an expression or symbol ''' if not issymbolic(expression): - if expression is None: - return - if isinstance(expression, str): - if len(expression) == 1: - expression = ord(expression) - else: - expression = map(ord, expression) - if isinstance(expression, (list, tuple)): - if len(expression) == 0: - return expression - arr = constraints.new_array(index_max=len(expression)) - for i in range(len(expression)): - arr[i] = expression[i] - return self.get_value(constraints, arr) return expression assert isinstance(expression, (Bool, BitVec, Array)) with constraints as temp_cs: @@ -477,7 +463,7 @@ class Z3Solver(Solver): var = [] result = '' for i in xrange(expression.index_max): - subvar = temp_cs.new_bitvec(8) + subvar = temp_cs.new_bitvec(expression.value_bits) var.append(subvar) temp_cs.add(subvar==expression[i]) diff --git a/manticore/core/smtlib/visitors.py b/manticore/core/smtlib/visitors.py index ad0bb3f..aa95e0e 100644 --- a/manticore/core/smtlib/visitors.py +++ b/manticore/core/smtlib/visitors.py @@ -69,6 +69,11 @@ class Visitor(object): :param use_fixed_point: if True, it runs _methods until a fixed point is found :type use_fixed_point: Bool ''' + + #Special case. Need to get the unsleeved version of the array + if isinstance(node, ArrayProxy): + node = node.array + cache = self._cache visited = set() diff --git a/manticore/core/state.py b/manticore/core/state.py index c5e99dd..1e879d0 100644 --- a/manticore/core/state.py +++ b/manticore/core/state.py @@ -202,7 +202,7 @@ class State(Eventful): ''' label = options.get('label', 'buffer') taint = options.get('taint', frozenset()) - expr = self._constraints.new_array(name=label, index_max=nbytes, taint=taint) + expr = self._constraints.new_array(name=label, index_max=nbytes, value_bits=8, taint=taint) self._input_symbols.append(expr) if options.get('cstring', False): diff --git a/manticore/platforms/evm.py b/manticore/platforms/evm.py index 8376274..c8c9906 100644 --- a/manticore/platforms/evm.py +++ b/manticore/platforms/evm.py @@ -1074,6 +1074,7 @@ class EVM(Eventful): :param bytecode: the byte array that is the machine code to be executed. :param header: the block header of the present block. :param depth: the depth of the present message-call or contract-creation (i.e. the number of CALLs or CREATEs being executed at present). + :param gas: gas budget for this transaction. ''' super(EVM, self).__init__(**kwargs) @@ -1090,7 +1091,6 @@ class EVM(Eventful): self.bytecode = code self.suicides = set() self.logs = [] - self.gas=gas #FIXME parse decode and mark invalid instructions #self.invalid = set() @@ -1104,7 +1104,7 @@ class EVM(Eventful): #Machine state self.pc = 0 self.stack = [] - self.gas = gas + self._gas = gas self.global_storage = global_storage self.allocated = 0 @@ -1117,10 +1117,12 @@ class EVM(Eventful): self._constraints = constraints self.memory.constraints = constraints + @property + def gas(self): + return self._gas def __getstate__(self): state = super(EVM, self).__getstate__() - state['gas'] = self.gas state['memory'] = self.memory state['global_storage'] = self.global_storage state['constraints'] = self.constraints @@ -1136,7 +1138,7 @@ class EVM(Eventful): state['header'] = self.header state['pc'] = self.pc state['stack'] = self.stack - state['gas'] = self.gas + state['gas'] = self._gas state['allocated'] = self.allocated state['suicides'] = self.suicides state['logs'] = self.logs @@ -1144,7 +1146,7 @@ class EVM(Eventful): return state def __setstate__(self, state): - self.gas = state['gas'] + self._gas = state['gas'] self.memory = state['memory'] self.logs = state['logs'] self.global_storage = state['global_storage'] @@ -1161,7 +1163,6 @@ class EVM(Eventful): self.header = state['header'] self.pc = state['pc'] self.stack = state['stack'] - self.gas = state['gas'] self.allocated = state['allocated'] self.suicides = state['suicides'] super(EVM, self).__setstate__(state) @@ -1260,9 +1261,9 @@ class EVM(Eventful): def _consume(self, fee): assert fee>=0 - if self.gas < fee: + if self._gas < fee: raise NotEnoughGas() - self.gas -= fee + self._gas -= fee #Execute an instruction from current pc def execute(self): @@ -1730,7 +1731,7 @@ class EVM(Eventful): def GAS(self): '''Get the amount of available gas, including the corresponding reduction the amount of available gas''' #fixme calculate gas consumption - return self.gas + return self._gas def JUMPDEST(self): '''Mark a valid destination for jumps''' diff --git a/manticore/platforms/linux.py b/manticore/platforms/linux.py index 2e12718..52f4065 100644 --- a/manticore/platforms/linux.py +++ b/manticore/platforms/linux.py @@ -2584,9 +2584,13 @@ class SLinux(Linux): def generate_workspace_files(self): def solve_to_fd(data, fd): + def make_chr(c): + if isinstance(c, int): + return chr(c) + return c try: for c in data: - fd.write(chr(solver.get_value(self.constraints, c))) + fd.write(make_chr(solver.get_value(self.constraints, c))) except SolverException: fd.write('{SolverException}') diff --git a/tests/test_smtlibv2.py b/tests/test_smtlibv2.py index a7b6410..610d643 100644 --- a/tests/test_smtlibv2.py +++ b/tests/test_smtlibv2.py @@ -77,35 +77,74 @@ class ExpressionTest(unittest.TestCase): key = cs.new_bitvec(32) #assert that the array is 'A' at key position - cs.add(array[key] == 'A') + cs.add(array[key] == ord('A')) #lets restrict key to be greater than 1000 cs.add(key.ugt(1000)) with cs as temp_cs: #1001 position of array can be 'A' - temp_cs.add(array[1001] == 'A') + temp_cs.add(array[1001] == ord('A')) self.assertTrue(self.solver.check(temp_cs)) with cs as temp_cs: #1001 position of array can also be 'B' - temp_cs.add(array[1001] == 'B') + temp_cs.add(array[1001] == ord('B')) self.assertTrue(self.solver.check(temp_cs)) with cs as temp_cs: #but if it is 'B' ... - temp_cs.add(array[1001] == 'B') + temp_cs.add(array[1001] == ord('B')) #then key can not be 1001 temp_cs.add(key == 1001) self.assertFalse(self.solver.check(temp_cs)) with cs as temp_cs: #If 1001 position is 'B' ... - temp_cs.add(array[1001] == 'B') + temp_cs.add(array[1001] == ord('B')) #then key can be 1000 for ex.. temp_cs.add(key == 1002) self.assertTrue(self.solver.check(temp_cs)) + + def testBasicArray256(self): + cs = ConstraintSet() + #make array of 32->8 bits + array = cs.new_array(32, value_bits=256) + #make free 32bit bitvector + key = cs.new_bitvec(32) + + #assert that the array is 1234567890.. at key position + cs.add(array[key] == 11111111111111111111111111111111111111111111) + #lets restrict key to be greater than 1000 + cs.add(key.ugt(1000)) + + with cs as temp_cs: + #1001 position of array can be 'A' + temp_cs.add(array[1001] == 11111111111111111111111111111111111111111111) + self.assertTrue(self.solver.check(temp_cs)) + + with cs as temp_cs: + #1001 position of array can also be 'B' + temp_cs.add(array[1001] == 22222222222222222222222222222222222222222222) + self.assertTrue(self.solver.check(temp_cs)) + + + with cs as temp_cs: + #but if it is 'B' ... + temp_cs.add(array[1001] == 22222222222222222222222222222222222222222222) + #then key can not be 1001 + temp_cs.add(key == 1001) + self.assertFalse(self.solver.check(temp_cs)) + + with cs as temp_cs: + #If 1001 position is 'B' ... + temp_cs.add(array[1001] == 22222222222222222222222222222222222222222222) + #then key can be 1000 for ex.. + temp_cs.add(key == 1002) + self.assertTrue(self.solver.check(temp_cs)) + + def testBasicArrayStore(self): name = "bitarray" cs = ConstraintSet() @@ -115,29 +154,29 @@ class ExpressionTest(unittest.TestCase): key = cs.new_bitvec(32) #assert that the array is 'A' at key position - array = array.store(key, 'A') + array = array.store(key, ord('A')) #lets restrict key to be greater than 1000 cs.add(key.ugt(1000)) #1001 position of array can be 'A' - self.assertTrue(self.solver.can_be_true(cs, array.select(1001) == 'A')) + self.assertTrue(self.solver.can_be_true(cs, array.select(1001) == ord('A'))) #1001 position of array can be 'B' - self.assertTrue(self.solver.can_be_true(cs, array.select(1001) == 'B')) + self.assertTrue(self.solver.can_be_true(cs, array.select(1001) == ord('B'))) #name is correctly proxied self.assertEqual(array.name, name + "_1") with cs as temp_cs: #but if it is 'B' ... - temp_cs.add(array.select(1001) == 'B') + temp_cs.add(array.select(1001) == ord('B')) #then key can not be 1001 temp_cs.add(key == 1001) self.assertFalse(self.solver.check(temp_cs)) with cs as temp_cs: #If 1001 position is 'B' ... - temp_cs.add(array.select(1001) == 'B') + temp_cs.add(array.select(1001) == ord('B')) #then key can be 1000 for ex.. temp_cs.add(key != 1002) self.assertTrue(self.solver.check(temp_cs)) @@ -152,7 +191,7 @@ class ExpressionTest(unittest.TestCase): key = cs.new_bitvec(32) #assert that the array is 'A' at key position - array = array.store(key, 'A') + array = array.store(key, ord('A')) #lets restrict key to be greater than 1000 cs.add(key.ugt(1000)) cs = pickle.loads(pickle.dumps(cs)) @@ -214,8 +253,8 @@ class ExpressionTest(unittest.TestCase): a = cs.new_bitvec(32, name='VAR') self.assertEqual(get_depth(a), 1) cond = Operators.AND(a < 200, a > 100) - arr[0]='a' - arr[1]='b' + arr[0]=ord('a') + arr[1]=ord('b')