From 1e76998eb78fd2b3240e1131c5480f02c2335620 Mon Sep 17 00:00:00 2001 From: Mark Mossberg Date: Thu, 11 May 2017 13:25:43 -0400 Subject: [PATCH] Add infrastructure for core models (#244) * Rename libc.py to models.py * Clean old unused libc.py code * Make models top level importable * Add State level model invocation function So user is not required to pass in state at to a platform level func * Explicitly mark what is in the public API Protects against accidentally making something a public API just because it has a docstring * clean * Move models.py to top level * Rm models * Fix docstring typo * Add default param name, move comment * Update docstring --- docs/api.rst | 4 +- manticore/__init__.py | 2 +- manticore/core/cpu/abstractcpu.py | 2 +- manticore/core/state.py | 11 ++ manticore/manticore.py | 2 +- manticore/models.py | 0 manticore/platforms/libc.py | 170 ------------------------------ 7 files changed, 16 insertions(+), 175 deletions(-) create mode 100644 manticore/models.py delete mode 100644 manticore/platforms/libc.py diff --git a/docs/api.rst b/docs/api.rst index 45cd312..e406876 100644 --- a/docs/api.rst +++ b/docs/api.rst @@ -13,13 +13,13 @@ Manticore --------- .. autoclass:: manticore.Manticore - :members: + :members: add_hook, hook, run, terminate, verbosity State ----- .. autoclass:: manticore.core.state.State - :members: + :members: abandon, constrain, new_symbolic_buffer, new_symbolic_value, solve_n, solve_one, symbolicate_buffer, invoke_model Cpu --- diff --git a/manticore/__init__.py b/manticore/__init__.py index aa195c2..b372319 100644 --- a/manticore/__init__.py +++ b/manticore/__init__.py @@ -1,2 +1,2 @@ from .manticore import Manticore -from .utils.helpers import issymbolic \ No newline at end of file +from .utils.helpers import issymbolic diff --git a/manticore/core/cpu/abstractcpu.py b/manticore/core/cpu/abstractcpu.py index 883eb71..de250ed 100644 --- a/manticore/core/cpu/abstractcpu.py +++ b/manticore/core/cpu/abstractcpu.py @@ -385,7 +385,7 @@ class Cpu(object): :param str register: register name (as listed in `self.all_registers`) :return: register value - :rtype int or long or Expression + :rtype: int or long or Expression ''' return self._regfile.read(register) diff --git a/manticore/core/state.py b/manticore/core/state.py index 07ff3be..3026a3d 100644 --- a/manticore/core/state.py +++ b/manticore/core/state.py @@ -234,3 +234,14 @@ class State(object): self.branches[key] += 1 except KeyError: self.branches[key] = 1 + + def invoke_model(self, model): + ''' + Invoke a `model`. A `model` is a callable whose first argument is a + :class:`~manticore.core.state.State`, and whose following arguments correspond to + the C function being modeled. + + :param callable model: Model to invoke + ''' + # TODO(mark): this can't support varargs core models! + self.platform.invoke_model(model, prefix_args=(self,)) diff --git a/manticore/manticore.py b/manticore/manticore.py index b35af6b..4ea1f1e 100644 --- a/manticore/manticore.py +++ b/manticore/manticore.py @@ -304,7 +304,7 @@ class Manticore(object): ''' Add a callback to be invoked on executing a program counter. Pass `None` for pc to invoke callback on every instruction. `callback` should be a callable - that takes one :class:`~manticore.core.executor.State` argument. + that takes one :class:`~manticore.core.state.State` argument. :param pc: Address of instruction to hook :type pc: int or None diff --git a/manticore/models.py b/manticore/models.py new file mode 100644 index 0000000..e69de29 diff --git a/manticore/platforms/libc.py b/manticore/platforms/libc.py deleted file mode 100644 index 90c4c20..0000000 --- a/manticore/platforms/libc.py +++ /dev/null @@ -1,170 +0,0 @@ -import sys, os, struct -import StringIO -import logging -import random -from ..core.smtlib import solver, Expression, Operators -#, Interruption, Syscall, ConcretizeRegister, ConcretizeMemory, ConcretizeArgument, IgnoreAPI -from ..core.cpu.abstractcpu import Interruption, Syscall, \ - ConcretizeRegister, ConcretizeArgument, IgnoreAPI, \ - ConcretizeMemory -from ..core.memory import MemoryException -from ..core.executor import ForkState -from ..utils.helpers import issymbolic - -logger = logging.getLogger("MODEL") - -def _memset_range(cpu, dst, value, rng): - - minval, maxval, symb_size = rng - - if minval == maxval: - # no range, just write N elements - for i in xrange(0, maxval): - cpu.write_int(dst+i, value, 8) - else: - # up to minval doesn't depend on range - for i in xrange(0, minval): - cpu.write_int(dst+i, value, 8) - - # write range dependent values - for i in xrange(minval, maxval): - cur_v = cpu.read_int(dst+i, 8) - cpu.write_int(dst+i, Operators.ITEBV(8, symb_size >= i, value, cur_v), 8) - - return dst - -def _memmove_range(cpu, dst, src, rng): - - minval, maxval, symb_size = rng - - # read source bytes - src_bytes = [cpu.read_int(src+i, 8) for i in xrange(0, maxval)] - - if minval == maxval: - # no range, just write N elements - for (i,b) in enumerate(src_bytes): - cpu.write_int(dst+i, b, 8) - else: - # up to minval doesn't depend on range - for i in xrange(0, minval): - cpu.write_int(dst+i, src_bytes[i], 8) - - # write range dependent values - for i in xrange(minval, maxval): - cur_v = cpu.read_int(dst+i, 8) - cpu.write_int(dst+i, Operators.ITEBV(8, symb_size >= i, src_bytes[i], cur_v), 8) - - return dst - -class strings(object): - - @staticmethod - def memcpy(state, dst, src, size): - return strings.memmove(state, dst, src, size) - - @staticmethod - def memmove(state, dst, src, size): - """void *memmove(void *dest, const void *src, size_t n);""" - - cpu = state.cpu - - if issymbolic(size): - single_sol = solver.get_all_values(state.constraints, size, maxcnt=2, silent=True) - if len(single_sol) == 1: - size = single_sol[0] - logger.info("memmoving single solution size: {:d}".format(size)) - return _memmove_range(cpu, dst, src, (size, size, None) ) - else: - conc_min, conc_max = solver.minmax(state.constraints, size) - logger.info("memmoving sizes: {:d} - {:d}".format(conc_min, conc_max)) - return _memmove_range(cpu, dst, src, (conc_min, conc_max, size) ) - else: - # concrete case - logger.info("memmoving concrete size: {:d}".format(size)) - return _memmove_range(cpu, dst, src, (size, size, None) ) - - - @staticmethod - def memset(state, dst, char, size): - cpu = state.cpu - - if issymbolic(size): - single_sol = solver.get_all_values(state.constraints, size, maxcnt=2, silent=True) - if len(single_sol) == 1: - size = single_sol[0] - logger.info("memsetting single solution size: {:d}".format(size)) - return _memset_range(cpu, dst, char, (size, size, None) ) - else: - conc_min, conc_max = solver.minmax(state.constraints, size) - logger.info("memsetting in a range: {:d} - {:d}".format(conc_min, conc_max)) - return _memset_range(cpu, dst, char, (conc_min, conc_max, size) ) - else: - # concrete case - logger.info("memsetting concrete size: {:d}".format(size)) - return _memset_range(cpu, dst, char, (size, size, None) ) - - @staticmethod - def strlen(state, src): - cpu = state.cpu - count = 0 - while True: - value = cpu.read_int(src+count, 8) - if issymbolic(value): - if solver.can_be_true(state.constraints, value==0): - raise ForkState(value==0) - elif value == 0: - break - count += 1 - return count - - @staticmethod - def strcpy(state, dst, src): - - cpu = state.cpu - s = [] - i = 0 - while True: - value = cpu.read_int(src, 8) - if not cpu.mem.isWritable(dst+i): - raise MemoryException("No access writing", dst+i) - if issymbolic(value): - if solver.can_be_true(state.constraints, value==0): - raise ConcretizeMemory(src+i) - else: - break - elif value == 0: - break - s.append(value) - - for i in xrange(len(s)): - cpu.write_int(dst+i, s[i], 8) - -class heap(object): - - @staticmethod - def malloc(cpu, size): - if issymbolic(size): - logger.info("malloc(Symbolic Size); concretizing size") - raise ConcretizeArgument(0) - else: - raise IgnoreAPI("malloc({:08x})".format(size)) - - @staticmethod - def realloc(cpu, ptr, size): - if issymbolic(size): - logger.info("realloc({}, Symbolic Size); concretizing size".format(str(ptr))) - raise ConcretizeArgument(1) - else: - raise IgnoreAPI("realloc({}, {:08x})".format(str(ptr), size)) - - @staticmethod - def calloc(cpu, count, size): - if issymbolic(size): - logger.info("calloc({}, Symbolic Size); concretizing size".format(str(count))) - raise ConcretizeArgument(1) - - if issymbolic(count): - logger.info("calloc(Symbolic count, {}); concretizing count".format(str(size))) - raise ConcretizeArgument(0) - - raise IgnoreAPI("calloc({:08x}, {:08x})".format(count, size))