From e920b73e146b1e888344be83e80ef3546651cb04 Mon Sep 17 00:00:00 2001 From: Mark Mossberg Date: Thu, 16 Mar 2017 14:43:17 -0400 Subject: [PATCH] Move state into own file (#75) * Move State from executor.py * Fix import * relative import --- manticore/core/executor.py | 211 ++----------------------------------- manticore/core/state.py | 204 +++++++++++++++++++++++++++++++++++ manticore/manticore.py | 3 +- 3 files changed, 212 insertions(+), 206 deletions(-) create mode 100644 manticore/core/state.py diff --git a/manticore/core/executor.py b/manticore/core/executor.py index 548ba2c..4808345 100644 --- a/manticore/core/executor.py +++ b/manticore/core/executor.py @@ -49,18 +49,16 @@ from .smtlib import solver, Expression, Operators, SolverException, Array, BitVe from ..utils.event import Signal from ..utils.helpers import issymbolic -#Multiprocessing -from multiprocessing import Manager -from multiprocessing.managers import BaseManager, SyncManager +from multiprocessing.managers import SyncManager - -logger = logging.getLogger("EXECUTOR") - -#initilizer for SyncManager def mgr_init(): signal.signal(signal.SIGINT, signal.SIG_IGN) manager = SyncManager() -manager.start(mgr_init) +manager.start(mgr_init) + +from .state import AbandonState, State + +logger = logging.getLogger("EXECUTOR") class SyscallNotImplemented(Exception): ''' Exception raised when you try to call a not implemented @@ -81,207 +79,10 @@ class Deadlock(Exception): class MaxConsecutiveIntructions(Exception): pass -class AbandonState(Exception): - pass - class ForkState(Exception): def __init__(self, condition): self.condition=condition -class State(object): - #Class global counter - _state_count = manager.Value('i', 0) - _lock = manager.Lock() - @staticmethod - def get_new_id(): - with State._lock: - ret = State._state_count.value - State._state_count.value +=1 - return ret - - def __init__(self, constraints, model): - self.model = model - self.forks = 0 - self.co = self.get_new_id() - self.constraints = constraints - self.model._constraints = constraints - for proc in self.model.procs: - proc._constraints = constraints - proc.memory._constraints = constraints - - self.input_symbols = list() - #Stats I'm not sure we need in general - self.last_pc = (None, None) - self.visited = set() - self.branches = {} - self._child = None - - def __reduce__(self): - return (self.__class__, (self.constraints, self.model), {'visited': self.visited, 'last_pc': self.last_pc, 'forks': self.forks, 'co': self.co, 'input_symbols':self.input_symbols, 'branches': self.branches} ) - - @staticmethod - def state_count(): - return State._state_count.value - - @property - def cpu(self): - return self.model.current - - @property - def mem(self): - return self.model.current.memory - - @property - def name(self): - return 'state_%06d.pkl'%(self.co) - - def __enter__(self): - assert self._child is None - new_state = State(self.constraints.__enter__(), self.model) - new_state.visited = set(self.visited) - new_state.forks = self.forks + 1 - new_state.co = State.get_new_id() - new_state.input_symbols = self.input_symbols - new_state.branches = self.branches - self._child = new_state - return new_state - - def __exit__(self, ty, value, traceback): - self.constraints.__exit__(ty, value, traceback) - self._child = None - - - def execute(self): - trace_item = (self.model._current, self.cpu.PC) - try: - result = self.model.execute() - except: - trace_item = None - raise - assert self.model.constraints is self.constraints - assert self.mem.constraints is self.constraints - self.visited.add(trace_item) - self.last_pc = trace_item - return result - - def add(self, constraint, check=False): - self.constraints.add(constraint) - - def abandon(self): - '''Abandon the currently-active state - - Note: This must be called from the Executor loop, or a user-provided - callback.''' - raise AbandonState - - def new_symbolic_buffer(self, nbytes, **options): - '''Create and return a symbolic buffer of length |nbytes|. The buffer is - not written into State's memory; write it to the state's memory to - introduce it into the program state. - - Args: - nbytes - Length of the new buffer - options - Options to set on the returned expression. Valid options: - name -- The name to assign to the buffer (str) - cstring -- Whether or not to enforce that the buffer is a cstring - (i.e. no \0 bytes, except for the last byte). (bool) - - Returns: - Expression representing the buffer. - ''' - name = options.get('name', 'buffer') - expr = self.constraints.new_array(name=name, index_max=nbytes) - self.input_symbols.append(expr) - - if options.get('cstring', False): - for i in range(nbytes - 1): - self.constraints.add(expr[i] != 0) - - return expr - - - def new_symbolic_value(self, nbits, label='val', taint=frozenset()): - '''Create and return a symbolic value that is |nbits| bits wide. Assign - the value to a register or write it into the address space to introduce - it into the program state. - - Args: - nbits - The bitwidth of the value returned. - label - The label to assign to the value. - taint - A tuple or frozenset of values to use as taint identifiers. - - Returns: - Expression representing the value. - ''' - assert nbits in (1, 4, 8, 16, 32, 64, 128, 256) - expr = self.constraints.new_bitvec(nbits, name=label, taint=taint) - self.input_symbols.append(expr) - return expr - - def symbolicate_buffer(self, data, label = 'INPUT', wildcard='+', string=False): - '''Mark parts of a buffer as symbolic (demarked by the wildcard byte) - - Args: - data -- The string to symbolicate. If no wildcard bytes are provided, - this is the identity function on the first argument. - label -- The label to assign to the value - wildcard -- The byte that is considered a wildcard - string -- Ensure bytes returned can not be \0 - - Returns: - If data does not contain any wildcard bytes, data itself. Otherwise, - a list of values derived from data. Non-wildcard bytes are kept as - is, wildcard bytes are replaced by Expression objects. - ''' - if wildcard in data: - size = len(data) - symb = self.constraints.new_array(name=label, index_max=size) - self.input_symbols.append(symb) - for j in xrange(size): - if data[j] != wildcard: - symb[j] = data[j] - data = [symb[i] for i in range(size)] - - if string: - for b in data: - if issymbolic(b): - self.constraints.add(b != 0) - else: - assert b!=0 - return data - - - def concretize(self, symbolic, policy, maxcount=100): - vals = [] - if policy == 'MINMAX': - vals = solver.minmax(self.constraints, symbolic) - elif policy == 'SAMPLED': - m, M = solver.minmax(self.constraints, symbolic) - vals += [m, M] - if M-m > 3: - if solver.can_be_true(self.constraints, symbolic == (m+M)/2): - vals.append((m+M)/2) - if M-m > 100: - vals += solver.get_all_values(self.constraints, symbolic, maxcnt=maxcount, silent=True) - else: - assert policy == 'ALL' - vals = solver.get_all_values(self.constraints, symbolic, maxcnt=maxcount, silent=False) - - return list(set(vals)) - - @property - def _solver(self): - from .smtlib import solver - return solver - - def solve_one(self, expr): - # type: (Expression) -> int - return self._solver.get_value(self.constraints, expr) - - def solve_n(self, expr, nsolves=1, policy='minmax'): - # type: (Expression, int) -> list - return self._solver.get_all_values(self.constraints, expr, nsolves, silent=True) - def sync(f): """ Synchronization decorator. """ diff --git a/manticore/core/state.py b/manticore/core/state.py new file mode 100644 index 0000000..8223f88 --- /dev/null +++ b/manticore/core/state.py @@ -0,0 +1,204 @@ +from .executor import manager +from .smtlib import solver +from ..utils.helpers import issymbolic + +class AbandonState(Exception): + pass + + +class State(object): + # Class global counter + _state_count = manager.Value('i', 0) + _lock = manager.Lock() + + @staticmethod + def get_new_id(): + with State._lock: + ret = State._state_count.value + State._state_count.value += 1 + return ret + + def __init__(self, constraints, model): + self.model = model + self.forks = 0 + self.co = self.get_new_id() + self.constraints = constraints + self.model._constraints = constraints + for proc in self.model.procs: + proc._constraints = constraints + proc.memory._constraints = constraints + + self.input_symbols = list() + # Stats I'm not sure we need in general + self.last_pc = (None, None) + self.visited = set() + self.branches = {} + self._child = None + + def __reduce__(self): + return (self.__class__, (self.constraints, self.model), + {'visited': self.visited, 'last_pc': self.last_pc, 'forks': self.forks, + 'co': self.co, 'input_symbols': self.input_symbols, + 'branches': self.branches}) + + @staticmethod + def state_count(): + return State._state_count.value + + @property + def cpu(self): + return self.model.current + + @property + def mem(self): + return self.model.current.memory + + @property + def name(self): + return 'state_%06d.pkl' % (self.co) + + def __enter__(self): + assert self._child is None + new_state = State(self.constraints.__enter__(), self.model) + new_state.visited = set(self.visited) + new_state.forks = self.forks + 1 + new_state.co = State.get_new_id() + new_state.input_symbols = self.input_symbols + new_state.branches = self.branches + self._child = new_state + return new_state + + def __exit__(self, ty, value, traceback): + self.constraints.__exit__(ty, value, traceback) + self._child = None + + def execute(self): + trace_item = (self.model._current, self.cpu.PC) + try: + result = self.model.execute() + except: + trace_item = None + raise + assert self.model.constraints is self.constraints + assert self.mem.constraints is self.constraints + self.visited.add(trace_item) + self.last_pc = trace_item + return result + + def add(self, constraint, check=False): + self.constraints.add(constraint) + + def abandon(self): + '''Abandon the currently-active state + + Note: This must be called from the Executor loop, or a user-provided + callback.''' + raise AbandonState + + def new_symbolic_buffer(self, nbytes, **options): + '''Create and return a symbolic buffer of length |nbytes|. The buffer is + not written into State's memory; write it to the state's memory to + introduce it into the program state. + + Args: + nbytes - Length of the new buffer + options - Options to set on the returned expression. Valid options: + name -- The name to assign to the buffer (str) + cstring -- Whether or not to enforce that the buffer is a cstring + (i.e. no \0 bytes, except for the last byte). (bool) + + Returns: + Expression representing the buffer. + ''' + name = options.get('name', 'buffer') + expr = self.constraints.new_array(name=name, index_max=nbytes) + self.input_symbols.append(expr) + + if options.get('cstring', False): + for i in range(nbytes - 1): + self.constraints.add(expr[i] != 0) + + return expr + + def new_symbolic_value(self, nbits, label='val', taint=frozenset()): + '''Create and return a symbolic value that is |nbits| bits wide. Assign + the value to a register or write it into the address space to introduce + it into the program state. + + Args: + nbits - The bitwidth of the value returned. + label - The label to assign to the value. + taint - A tuple or frozenset of values to use as taint identifiers. + + Returns: + Expression representing the value. + ''' + assert nbits in (1, 4, 8, 16, 32, 64, 128, 256) + expr = self.constraints.new_bitvec(nbits, name=label, taint=taint) + self.input_symbols.append(expr) + return expr + + def symbolicate_buffer(self, data, label='INPUT', wildcard='+', string=False): + '''Mark parts of a buffer as symbolic (demarked by the wildcard byte) + + Args: + data -- The string to symbolicate. If no wildcard bytes are provided, + this is the identity function on the first argument. + label -- The label to assign to the value + wildcard -- The byte that is considered a wildcard + string -- Ensure bytes returned can not be \0 + + Returns: + If data does not contain any wildcard bytes, data itself. Otherwise, + a list of values derived from data. Non-wildcard bytes are kept as + is, wildcard bytes are replaced by Expression objects. + ''' + if wildcard in data: + size = len(data) + symb = self.constraints.new_array(name=label, index_max=size) + self.input_symbols.append(symb) + for j in xrange(size): + if data[j] != wildcard: + symb[j] = data[j] + data = [symb[i] for i in range(size)] + + if string: + for b in data: + if issymbolic(b): + self.constraints.add(b != 0) + else: + assert b != 0 + return data + + def concretize(self, symbolic, policy, maxcount=100): + vals = [] + if policy == 'MINMAX': + vals = solver.minmax(self.constraints, symbolic) + elif policy == 'SAMPLED': + m, M = solver.minmax(self.constraints, symbolic) + vals += [m, M] + if M - m > 3: + if solver.can_be_true(self.constraints, symbolic == (m + M) / 2): + vals.append((m + M) / 2) + if M - m > 100: + vals += solver.get_all_values(self.constraints, symbolic, maxcnt=maxcount, + silent=True) + else: + assert policy == 'ALL' + vals = solver.get_all_values(self.constraints, symbolic, maxcnt=maxcount, + silent=False) + + return list(set(vals)) + + @property + def _solver(self): + from .smtlib import solver + return solver + + def solve_one(self, expr): + # type: (Expression) -> int + return self._solver.get_value(self.constraints, expr) + + def solve_n(self, expr, nsolves=1, policy='minmax'): + # type: (Expression, int) -> list + return self._solver.get_all_values(self.constraints, expr, nsolves, silent=True) \ No newline at end of file diff --git a/manticore/manticore.py b/manticore/manticore.py index c3d24a8..a6bb079 100644 --- a/manticore/manticore.py +++ b/manticore/manticore.py @@ -13,7 +13,8 @@ from multiprocessing import Process from elftools.elf.elffile import ELFFile from elftools.elf.sections import SymbolTableSection -from .core.executor import Executor, State, AbandonState +from .core.executor import Executor +from .core.state import State, AbandonState from .core.parser import parse from .core.smtlib import solver, Expression, Operators, SolverException, Array, ConstraintSet from core.smtlib import BitVec, Bool