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
This commit is contained in:
Mark Mossberg
GitHub
+2
-2
@@ -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
|
||||
---
|
||||
|
||||
@@ -1,2 +1,2 @@
|
||||
from .manticore import Manticore
|
||||
from .utils.helpers import issymbolic
|
||||
from .utils.helpers import issymbolic
|
||||
|
||||
@@ -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)
|
||||
|
||||
|
||||
@@ -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,))
|
||||
|
||||
@@ -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
|
||||
|
||||
@@ -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))
|
||||
Reference in New Issue
Block a user