6616b9e05c
* Port most of the less invasive/controversial changes from dev-evm-dynamicarguments * Port section of fixes from ethereum.py * Port tests unrelated to concretizing dyn args * Add remaining changes from evm.py * clean, fmt, code climate * rm unnecessary setup * disable?? * fmt * remove all the returns * lol cc * Rm unused code * port to .format * don't use map (for py2/3 compat) * simplify slicing * Rm dyn arg code, since it doesn't really even work and will be included when dev-evm-dynamicarguments is totally resolved * add address/get_uint test * Revert "Rm dyn arg code, since it doesn't really even work" 69188da4caf1ff74288b6398e8140f627dc495c4
187 lines
5.7 KiB
Python
187 lines
5.7 KiB
Python
import unittest
|
|
|
|
from manticore.core.smtlib import ConstraintSet, solver
|
|
from manticore.core.state import State
|
|
from manticore.platforms import linux
|
|
|
|
from manticore.models import variadic, isvariadic, strcmp, strlen
|
|
|
|
class ModelMiscTest(unittest.TestCase):
|
|
def test_variadic_dec(self):
|
|
@variadic
|
|
def f():
|
|
pass
|
|
self.assertTrue(isvariadic(f))
|
|
|
|
def test_no_variadic_dec(self):
|
|
def f():
|
|
pass
|
|
self.assertFalse(isvariadic(f))
|
|
|
|
|
|
class ModelTest(unittest.TestCase):
|
|
l = linux.SLinux('/bin/ls')
|
|
state = State(ConstraintSet(), l)
|
|
stack_top = state.cpu.RSP
|
|
|
|
def _clear_constraints(self):
|
|
self.state._constraints = ConstraintSet()
|
|
|
|
def tearDown(self):
|
|
self._clear_constraints()
|
|
self.state.cpu.RSP = self.stack_top
|
|
|
|
def _push_string(self, s):
|
|
cpu = self.state.cpu
|
|
cpu.RSP -= len(s)
|
|
cpu.write_bytes(cpu.RSP, s)
|
|
return cpu.RSP
|
|
|
|
|
|
class StrcmpTest(ModelTest):
|
|
_multiprocess_can_split_ = True
|
|
def _push2(self, s1, s2):
|
|
s1ptr = self._push_string(s1)
|
|
s2ptr = self._push_string(s2)
|
|
return s1ptr, s2ptr
|
|
|
|
def test_concrete_eq(self):
|
|
s = 'abc\0'
|
|
strs = self._push2(s, s)
|
|
ret = strcmp(self.state, *strs)
|
|
self.assertEqual(ret, 0)
|
|
|
|
def test_concrete_lt(self):
|
|
def _concrete_lt(s1, s2):
|
|
strs = self._push2(s1, s2)
|
|
ret = strcmp(self.state, *strs)
|
|
self.assertTrue(ret < 0)
|
|
_concrete_lt('a\0', 'b\0')
|
|
_concrete_lt('a\0', 'ab\0')
|
|
|
|
|
|
def test_concrete_gt(self):
|
|
def _concrete_gt(s1, s2):
|
|
strs = self._push2(s1, s2)
|
|
ret = strcmp(self.state, *strs)
|
|
self.assertTrue(ret > 0)
|
|
_concrete_gt('c\0', 'b\0')
|
|
_concrete_gt('bc\0', 'b\0')
|
|
|
|
def test_symbolic_actually_concrete(self):
|
|
s1 = 'ab\0'
|
|
s2 = self.state.symbolicate_buffer('d+\0')
|
|
strs = self._push2(s1, s2)
|
|
|
|
ret = strcmp(self.state, *strs)
|
|
self.assertTrue(self.state.must_be_true(ret < 0))
|
|
|
|
def test_effective_null(self):
|
|
s1 = self.state.symbolicate_buffer('a+')
|
|
s2 = self.state.symbolicate_buffer('++')
|
|
|
|
strs = self._push2(s1, s2)
|
|
self.state.constrain(s1[1] == 0)
|
|
self.state.constrain(s2[0] == ord('z'))
|
|
|
|
ret = strcmp(self.state, *strs)
|
|
self.assertTrue(self.state.must_be_true(ret < 0))
|
|
|
|
def test_symbolic_concrete(self):
|
|
s1 = 'hi\0'
|
|
s2 = self.state.symbolicate_buffer('+++\0')
|
|
strs = self._push2(s1, s2)
|
|
|
|
ret = strcmp(self.state, *strs)
|
|
self.assertTrue(solver.can_be_true(self.state.constraints, ret != 0))
|
|
self.assertTrue(solver.can_be_true(self.state.constraints, ret == 0))
|
|
|
|
self.state.constrain(s2[0] == ord('a'))
|
|
ret = strcmp(self.state, *strs)
|
|
self.assertTrue(self.state.must_be_true(ret > 0))
|
|
self._clear_constraints()
|
|
|
|
self.state.constrain(s2[0] == ord('z'))
|
|
ret = strcmp(self.state, *strs)
|
|
self.assertTrue(self.state.must_be_true(ret < 0))
|
|
self._clear_constraints()
|
|
|
|
self.state.constrain(s2[0] == ord('h'))
|
|
self.state.constrain(s2[1] == ord('i'))
|
|
ret = strcmp(self.state, *strs)
|
|
self.assertTrue(self.state.must_be_true(ret <= 0))
|
|
|
|
self.state.constrain(s2[2] == ord('\0'))
|
|
ret = strcmp(self.state, *strs)
|
|
self.assertTrue(self.state.must_be_true(ret == 0))
|
|
|
|
|
|
class StrlenTest(ModelTest):
|
|
def test_concrete(self):
|
|
s = self._push_string('abc\0')
|
|
ret = strlen(self.state, s)
|
|
self.assertEqual(ret, 3)
|
|
|
|
def test_concrete_empty(self):
|
|
s = self._push_string('\0')
|
|
ret = strlen(self.state, s)
|
|
self.assertEqual(ret, 0)
|
|
|
|
def test_symbolic_effective_null(self):
|
|
sy = self.state.symbolicate_buffer('ab+')
|
|
self.state.constrain(sy[2] == 0)
|
|
s = self._push_string(sy)
|
|
ret = strlen(self.state, s)
|
|
self.assertEqual(ret, 2)
|
|
|
|
def test_symbolic(self):
|
|
sy = self.state.symbolicate_buffer('+++\0')
|
|
s = self._push_string(sy)
|
|
|
|
ret = strlen(self.state, s)
|
|
self.assertItemsEqual(range(4), solver.get_all_values(self.state.constraints, ret))
|
|
|
|
self.state.constrain(sy[0] == 0)
|
|
ret = strlen(self.state, s)
|
|
self.assertTrue(self.state.must_be_true(ret == 0))
|
|
self._clear_constraints()
|
|
|
|
self.state.constrain(sy[0] != 0)
|
|
self.state.constrain(sy[1] == 0)
|
|
ret = strlen(self.state, s)
|
|
self.assertTrue(self.state.must_be_true(ret == 1))
|
|
self._clear_constraints()
|
|
|
|
self.state.constrain(sy[0] != 0)
|
|
self.state.constrain(sy[1] != 0)
|
|
self.state.constrain(sy[2] == 0)
|
|
ret = strlen(self.state, s)
|
|
self.assertTrue(self.state.must_be_true(ret == 2))
|
|
self._clear_constraints()
|
|
|
|
self.state.constrain(sy[0] != 0)
|
|
self.state.constrain(sy[1] != 0)
|
|
self.state.constrain(sy[2] != 0)
|
|
ret = strlen(self.state, s)
|
|
self.assertTrue(self.state.must_be_true(ret == 3))
|
|
|
|
def test_symbolic_mixed(self):
|
|
sy = self.state.symbolicate_buffer('a+b+\0')
|
|
s = self._push_string(sy)
|
|
|
|
self.state.constrain(sy[1] == 0)
|
|
ret = strlen(self.state, s)
|
|
self.assertTrue(self.state.must_be_true(ret == 1))
|
|
self._clear_constraints()
|
|
|
|
self.state.constrain(sy[1] != 0)
|
|
self.state.constrain(sy[3] == 0)
|
|
ret = strlen(self.state, s)
|
|
self.assertTrue(self.state.must_be_true(ret == 3))
|
|
self._clear_constraints()
|
|
|
|
self.state.constrain(sy[1] != 0)
|
|
self.state.constrain(sy[3] != 0)
|
|
ret = strlen(self.state, s)
|
|
self.assertTrue(self.state.must_be_true(ret == 4))
|