0b850dba40
* Enable simple ARM register concretization for Unicorn * Add canonical_registers property to abstractcpu * cpu to self * Check for regs_access better * Emulate a single instruction * Bypass capstone 3.0.4 arm bug * Dealing with capstone * Temporary disable ASR and remobe BitVec.Bool from test * WIP WIP debug prints WIP WIP * Unicorn fallback working (using unicorn master) * HAck to support unicorn 1.0.0 * WIP * Unicorn hack to handle PC updates * [WIP] do not do anything with this commit; for debugging only * Adding before clean up * emulation more or less works; need to work out more unicorn bugs * clean up emulate() caller code * move hooks to methods; cleanup * Concretize memory when emulating * Re-add Bool() * Update tests to start at offset 4 When an instruction branches to the previous instruction, Unicorn attempts to dereference that memory. We'd like to use unit tests to also make sure Unicorn emulation is in line with our own semantics. If we start all tests at offset 4, we can jump to a previous instruction and not fault when Unicorn dereferences it. * Fix concretization * Clean up test imports; upper-case Cpu * Unicorn tests * Add tests for all the ARM semantics, but make sure they're equivalent on unicorn. * Add a few tests to make sure unicorn correctly concretizes the memory it references * Fix broken import * Add symbolic register tests * Re-introduce the unicorn hack * Add the 'ONE' concretization policy * Rm unused function * Update concretization; add comments * Add ONE policy test * Create a base class for all concretization exceptions * Remove Armv7Cpu._concretize_registers * Check for enabled logging in a more idiomatic way * [wip] intermediate testing commit * Reimplement hooks and execution with unicorn * Add a DMB (mem barrier) instruction; nop * simplify instruction resolution * improve unicorn error handling * explicitly delete emu * Handle ARM helpers inline * map fetched memory * Narrow exception handling * Update DMB docs; make __kuser_dmb match real implementation * Fix typo; add comment; remove extraneous parameter * typos++
127 lines
3.7 KiB
Python
127 lines
3.7 KiB
Python
import unittest
|
|
|
|
from manticore.core.executor import State
|
|
from manticore.core.smtlib import BitVecVariable
|
|
from manticore.core.smtlib import ConstraintSet
|
|
from manticore.models import linux
|
|
|
|
class FakeMemory(object):
|
|
def __init__(self):
|
|
self._constraints = None
|
|
|
|
@property
|
|
def constraints(self):
|
|
return self._constraints
|
|
|
|
class FakeCpu(object):
|
|
def __init__(self):
|
|
self._memory = FakeMemory()
|
|
|
|
@property
|
|
def memory(self):
|
|
return self._memory
|
|
|
|
class FakeModel(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
|
|
|
|
|
|
class StateTest(unittest.TestCase):
|
|
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.add(expr == val)
|
|
solved = self.state.solve_one(expr)
|
|
self.assertEqual(solved, val)
|
|
|
|
def test_solve_n(self):
|
|
expr = BitVecVariable(32, 'tmp')
|
|
self.state.add(expr > 4)
|
|
self.state.add(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.add(expr > 4)
|
|
self.state.add(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.add(expr > 0)
|
|
self.state.add(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, FakeModel())
|
|
|
|
arr = initial_state.symbolicate_buffer('+'*100, label='SYMBA')
|
|
initial_state.add(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.add(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)
|
|
|
|
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)
|
|
|