Add strcmp model (#251)

* add models

* wip strcmp tests

* t

* Add some tests

* Better asserts

* More pythonic

* Add effectivene null test

* Handle symbolic pointer arguments

manticore/models.py

@@ -0,0 +1,86 @@
+from .core.cpu.abstractcpu import ConcretizeArgument
+from .utils.helpers import issymbolic
+from .core.smtlib.solver import solver
+from .core.smtlib.operators import ITEBV, ZEXTEND
+
+
+def _find_zero(cpu, constrs, ptr):
+    """
+    Helper for finding the closest NULL or, effectively NULL byte from a starting address.
+
+    :param Cpu cpu:
+    :param ConstraintSet constrs: Constraints for current `State`
+    :param int ptr: Address to start searching for a zero from
+    :return: Offset from `ptr` to first byte that is 0 or an `Expression` that must be zero
+    """
+
+    offset = 0
+    while True:
+        byt = cpu.read_int(ptr + offset, 8)
+
+        if issymbolic(byt):
+            if not solver.can_be_true(constrs, byt != 0):
+                break
+        else:
+            if byt == 0:
+                break
+
+        offset += 1
+
+    return offset
+
+
+def strcmp(state, s1, s2):
+    """
+    strcmp symbolic model.
+
+    Algorithm: Walks from end of string (minimum offset to NULL in either string)
+    to beginning building tree of ITEs each time either of the
+    bytes at current offset is symbolic.
+
+    Points of Interest:
+    - We've been building up a symbolic tree but then encounter two
+      concrete bytes that differ. We can throw away the entire symbolic
+      tree!
+    - If we've been encountering concrete bytes that match
+      at the end of the string as we walk forward, and then we encounter
+      a pair where one is symbolic, we can forget about that 0 `ret` we've
+      been tracking and just replace it with the symbolic subtraction of
+      the two
+
+    :param State state: Current program state
+    :param int s1: Address of string 1
+    :param int s2: Address of string 2
+    :return: Symbolic strcmp result
+    :rtype: Expression or int
+    """
+
+    cpu = state.cpu
+
+    if issymbolic(s1):
+        raise ConcretizeArgument(1)
+    if issymbolic(s2):
+        raise ConcretizeArgument(2)
+
+    s1_zero_idx = _find_zero(cpu, state.constraints, s1)
+    s2_zero_idx = _find_zero(cpu, state.constraints, s2)
+    min_zero_idx = min(s1_zero_idx, s2_zero_idx)
+
+    ret = None
+
+    for offset in xrange(min_zero_idx, -1, -1):
+        s1char = ZEXTEND(cpu.read_int(s1 + offset, 8), cpu.address_bit_size)
+        s2char = ZEXTEND(cpu.read_int(s2 + offset, 8), cpu.address_bit_size)
+
+        if issymbolic(s1char) or issymbolic(s2char):
+            if ret is None or (not issymbolic(ret) and ret == 0):
+                ret = s1char - s2char
+            else:
+                ret = ITEBV(cpu.address_bit_size, s1char != s2char, s1char - s2char, ret)
+        else:
+            if s1char != s2char:
+                ret = s1char - s2char
+            elif ret is None:
+                ret = 0
+
+    return ret

tests/test_models.py

@@ -0,0 +1,101 @@
+import unittest
+
+from manticore.core.smtlib import ConstraintSet, solver
+from manticore.core.state import State
+from manticore.platforms import linux
+
+from manticore.models import strcmp
+
+
+class StrcmpTest(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
+
+    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.assertFalse(solver.can_be_true(self.state.constraints, 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.assertFalse(solver.can_be_true(self.state.constraints, 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.assertFalse(solver.can_be_true(self.state.constraints, ret <= 0))
+        self._clear_constraints()
+
+        self.state.constrain(s2[0] == ord('z'))
+        ret = strcmp(self.state, *strs)
+        self.assertFalse(solver.can_be_true(self.state.constraints, 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.assertFalse(solver.can_be_true(self.state.constraints, ret > 0))
+
+        self.state.constrain(s2[2] == ord('\0'))
+        ret = strcmp(self.state, *strs)
+        self.assertFalse(solver.can_be_true(self.state.constraints, ret != 0))

tests/test_state.py

@@ -1,6 +1,6 @@
 import unittest
 
-from manticore.core.executor import State
+from manticore.core.state import State
 from manticore.core.smtlib import BitVecVariable
 from manticore.core.smtlib import ConstraintSet
 from manticore.platforms import linux