DeforaNetworks/manticore
3
0
Fork 0
Code Releases Activity

Array value configurable. 8,16,32..256 bits (not prefixed to 8) (#732)

Browse Source 
* 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
This commit is contained in:
feliam
2018-02-26 21:09:34 -03:00
committed by GitHub
parent a3ee31e6e6
commit 461da57ea3
8 changed files with 158 additions and 89 deletions
Download Patch File Download Diff File Expand all files Collapse all files
manticore/core/smtlib/constraints.py
+22 -19
View File
@@ -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))
manticore/core/smtlib/expression.py
+62 -31
View File
@@ -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):
manticore/core/smtlib/solver.py
+1 -15
View File
@@ -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])
manticore/core/smtlib/visitors.py
+5
View File
@@ -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()
manticore/core/state.py
+1 -1
View File
@@ -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):
manticore/platforms/evm.py
+10 -9
View File
@@ -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'''
manticore/platforms/linux.py
+5 -1
View File
@@ -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}')
tests/test_smtlibv2.py
+52 -13
View File
@@ -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')