Move state into own file (#75)
* Move State from executor.py * Fix import * relative import
This commit is contained in:
Mark Mossberg
GitHub
+6
-205
@@ -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. """
|
||||
|
||||
@@ -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)
|
||||
@@ -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
|
||||
|
||||
Reference in New Issue
Block a user