520a9be47d
* Wip refactoring * Executor and exceptions refactor wip wip * Fixing all_insts auto tests * Visited and generate testcase now at manticore api level * Aggregating state statistics into executor statistics * Wip refactoring * Executor and exceptions refactor wip wip * Fixing all_insts auto tests * Visited and generate testcase now at manticore api level * Aggregating state statistics into executor statistics * forwarding events wip * state setstate fix and setup_stack merge fix * will_terminate_state fix and tests skipped * Update all ConcretizeRegister and ConcretizeMemory * Wip refactoring * Executor and exceptions refactor wip wip * Fixing all_insts auto tests * Visited and generate testcase now at manticore api level * Aggregating state statistics into executor statistics * Wip refactoring * Executor and exceptions refactor wip wip * Fixing all_insts auto tests * Visited and generate testcase now at manticore api level * Aggregating state statistics into executor statistics * forwarding events wip * state setstate fix and setup_stack merge fix * will_terminate_state fix and tests skipped * Update all ConcretizeRegister and ConcretizeMemory * Exceptions are crazy crazy crazy * fix last merge * Merge merge until it pass * Instructions count default to 0 * will/did execute/emulate * Delayed keybpoard interrupt now shutdowns nicely * fix auto test generator x86 * Undo bad merge * utterly hopeless * basic working * Fix merge bugs and github comments * Remove unnecesary comment - github comments * trace_item not used there * model-platform and system.py fixed * backup/restore to store/load -- cpu.instruction property * Slightly better did/will naming and dynamic signal forwarding * platform.constraints and cpu.instruction as properties * Fix forward signals getattr * set las decoded pc at decode_instruction() / reenable instruction_cache * Signals name convention: did/will/on * Forward normal signals * Maintain last decoded pc in abstractcpu * Changed context manager so it just wont raise interrupt * Decree now forwards signals and sets constraints * linux.SymbolicFile does not need to maintain constraints * remove debbug print * Assimilating some PR commets * size_total == size * better merge of manticore.py * typo * Forwarding only specified objects in signal arguments * Fix few broken tests * revert + merge * remove some unused stuff from manticore() * manticore context <-> executor context * manticore context <-> executor context2 * context context context * forgotten return * Fix basix.arm * arm bitwise fix * fix context * Comment 1 * Comment 2 * Comment 3 * Comment 4 * Comment 5 * Comment 6 * Fix (still needs refactor but it works) profiling * Fix (still needs refactor but it works) profiling * The forgotten bit * Update tests to reflect current output * Verbosity fix * Fix verbosity test
151 lines
4.6 KiB
Python
151 lines
4.6 KiB
Python
import unittest
|
|
|
|
from manticore.platforms import linux
|
|
from manticore.utils.event import Signal
|
|
from manticore.core.state import State
|
|
from manticore.core.smtlib import BitVecVariable, ConstraintSet
|
|
|
|
class FakeMemory(object):
|
|
def __init__(self):
|
|
self._constraints = None
|
|
|
|
@property
|
|
def constraints(self):
|
|
return self._constraints
|
|
|
|
@constraints.setter
|
|
def constraints(self, constraints):
|
|
self._constraints = constraints
|
|
|
|
class FakeCpu(object):
|
|
def __init__(self):
|
|
self.will_decode_instruction = Signal()
|
|
self.will_execute_instruction = Signal()
|
|
self.did_execute_instruction = Signal()
|
|
self.will_emulate_instruction = Signal()
|
|
self.did_emulate_instruction = Signal()
|
|
|
|
self.will_read_register = Signal()
|
|
self.will_write_register = Signal()
|
|
self.will_read_memory = Signal()
|
|
self.will_write_memory = Signal()
|
|
|
|
self._memory = FakeMemory()
|
|
|
|
@property
|
|
def memory(self):
|
|
return self._memory
|
|
|
|
class FakePlatform(object):
|
|
def __init__(self):
|
|
self._constraints = None
|
|
self.procs = [FakeCpu()]
|
|
|
|
@property
|
|
def current(self):
|
|
return self.procs[0]
|
|
|
|
@property
|
|
def constraints(self):
|
|
return self._constraints
|
|
|
|
@constraints.setter
|
|
def constraints(self, constraints):
|
|
self._constraints = constraints
|
|
for proc in self.procs:
|
|
proc.memory.constraints = constraints
|
|
|
|
|
|
|
|
class StateTest(unittest.TestCase):
|
|
_multiprocess_can_split_ = True
|
|
def setUp(self):
|
|
l = linux.Linux('/bin/ls')
|
|
self.state = State(ConstraintSet(), l)
|
|
|
|
def test_solve_one(self):
|
|
val = 42
|
|
expr = BitVecVariable(32, 'tmp')
|
|
self.state.constrain(expr == val)
|
|
solved = self.state.solve_one(expr)
|
|
self.assertEqual(solved, val)
|
|
|
|
def test_solve_n(self):
|
|
expr = BitVecVariable(32, 'tmp')
|
|
self.state.constrain(expr > 4)
|
|
self.state.constrain(expr < 7)
|
|
solved = self.state.solve_n(expr, 2)
|
|
self.assertEqual(solved, [5,6])
|
|
|
|
def test_solve_n2(self):
|
|
expr = BitVecVariable(32, 'tmp')
|
|
self.state.constrain(expr > 4)
|
|
self.state.constrain(expr < 100)
|
|
solved = self.state.solve_n(expr, 5)
|
|
self.assertEqual(len(solved), 5)
|
|
|
|
def test_policy_one(self):
|
|
expr = BitVecVariable(32, 'tmp')
|
|
self.state.constrain(expr > 0)
|
|
self.state.constrain(expr < 100)
|
|
solved = self.state.concretize(expr, 'ONE')
|
|
self.assertEqual(len(solved), 1)
|
|
self.assertIn(solved[0], xrange(100))
|
|
|
|
def test_state(self):
|
|
constraints = ConstraintSet()
|
|
initial_state = State(constraints, FakePlatform())
|
|
|
|
arr = initial_state.symbolicate_buffer('+'*100, label='SYMBA')
|
|
initial_state.constrain(arr[0] > 0x41)
|
|
self.assertTrue(len(initial_state.constraints.declarations) == 1 )
|
|
with initial_state as new_state:
|
|
|
|
self.assertTrue(len(initial_state.constraints.declarations) == 1 )
|
|
self.assertTrue(len(new_state.constraints.declarations) == 1 )
|
|
arrb = new_state.symbolicate_buffer('+'*100, label='SYMBB')
|
|
|
|
self.assertTrue(len(initial_state.constraints.declarations) == 1 )
|
|
self.assertTrue(len(new_state.constraints.declarations) == 1 )
|
|
|
|
new_state.constrain(arrb[0] > 0x42)
|
|
|
|
|
|
self.assertTrue(len(new_state.constraints.declarations) == 2 )
|
|
|
|
|
|
self.assertTrue(len(initial_state.constraints.declarations) == 1 )
|
|
|
|
def test_new_symbolic_buffer(self):
|
|
length = 64
|
|
expr = self.state.new_symbolic_buffer(length)
|
|
self.assertEqual(len(expr), length)
|
|
|
|
def test_new_symbolic_value(self):
|
|
length = 64
|
|
expr = self.state.new_symbolic_value(length)
|
|
self.assertEqual(expr.size, length)
|
|
|
|
def test_new_bad_symbolic_value(self):
|
|
length = 62
|
|
with self.assertRaises(Exception):
|
|
expr = self.state.new_symbolic_value(length)
|
|
|
|
@unittest.skip('Record branches not a part of state anymore')
|
|
def test_record_branches(self):
|
|
branch = 0x80488bb
|
|
target = 0x8048997
|
|
fallthrough = 0x80488c1
|
|
self.state.last_pc = (0, branch)
|
|
|
|
self.state.record_branches([target, fallthrough])
|
|
|
|
self.assertEqual(self.state.branches[(branch, target)], 1)
|
|
self.assertEqual(self.state.branches[(branch, fallthrough)], 1)
|
|
|
|
self.state.record_branches([target, fallthrough])
|
|
|
|
self.assertEqual(self.state.branches[(branch, target)], 2)
|
|
self.assertEqual(self.state.branches[(branch, fallthrough)], 2)
|
|
|