DeforaNetworks/manticore
3
0
Fork 0
Code Releases Activity

Document state, cpu, issymbolic (#101)

Browse Source 
* Add unstable warning

* verbosity docs

* Add State and Cpu to docs

* Add State docs

* Add cpu docs

* Add select cpu docs

* Add issymbolic helper doc

* Rm double docstring

* Update write_bytes docstring

* Update Cpu docstr

* Document cpu reg interfaces

* Fix rebase mistakes
This commit is contained in:
Mark Mossberg 2017-03-27 15:03:42 -04:00 committed by GitHub
parent 6b1c69cb28
commit 1047fa42e3
5 changed files with 122 additions and 78 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

23
docs/api.rst
View File

@ -1,10 +1,29 @@
API
===
.. module:: manticore
This API is under active development, and should be considered unstable.
Helpers
-------
.. autofunction:: manticore.issymbolic
Manticore
---------
.. autoclass:: Manticore
.. autoclass:: manticore.Manticore
:members:
State
-----
.. autoclass:: manticore.core.state.State
:members:
Cpu
---
.. autoclass:: manticore.core.cpu.abstractcpu.Cpu
:members: read_int, read_bytes, write_int, write_bytes, write_register, read_register, all_registers

86
manticore/core/cpu/abstractcpu.py
View File

@ -128,19 +128,21 @@ class RegisterFile(object):
############################################################################
# Abstract cpu encapsulating common cpu methods used by models and executor.
class Cpu(object):
def __init__(self, regfile, memory):
'''
This is an abstract representation os a Cpu. Functionality common to all
subyacent architectures (and expected from users of a Cpu) should be here.
'''
Base class for all Cpu architectures. Functionality common to all
architectures (and expected from users of a Cpu) should be here.
The following attributes need to be defined in any derived class
assert hasattr(self, 'arch')
assert hasattr(self, 'mode')
assert hasattr(self, 'max_instr_width')
assert hasattr(self, 'address_bit_size')
assert hasattr(self, 'pc_alias')
assert hasattr(self, 'stack_alias')
'''
The following attributes need to be defined in any derived class
- arch
- mode
- max_instr_width
- address_bit_size
- pc_alias
- stack_alias
'''
def __init__(self, regfile, memory):
assert isinstance(regfile, RegisterFile)
super(Cpu, self).__init__()
self._regfile = regfile
@ -179,26 +181,28 @@ class Cpu(object):
@property
def all_registers(self):
''' Returns the list of all register names for this CPU.
@rtype: tuple
@return: the list of register names for this CPU.
'''Returns all register names for this CPU. Any register returned can be accessed
via a `cpu.REG` convenience interface (e.g. `cpu.EAX`) for both reading and
writing.
:return: valid register names
:rtype: tuple[str]
'''
return self._regfile.all_registers
#this operates on names
def write_register(self, register, value):
''' A convenient method to write a register by name (this accepts alias)
@param register a register name as listed in all_registers
@param value a value
@return It will return the written value possibly croped
'''Dynamic interface for writing cpu registers
:param str register: register name (as listed in `self.all_registers`)
:param value: register value
'''
return self._regfile.write(register, value)
def read_register(self, register):
''' A convenient method to read a register by name (this accepts alias)
@param register a register name as listed in all_registers
@param value a value
@return It will return the written value possibly croped
'''Dynamic interface for reading cpu registers
:param str register: register name (as listed in `self.all_registers`)
:return: register value
'''
return self._regfile.read(register)
@ -225,11 +229,12 @@ class Cpu(object):
def write_int(self, where, expr, size=None):
'''
Writes an integer value of C{size} bits to memory at address C{where}.
Writes int to memory
@param where: the address in memory where to store the value.
@param expr: the value to store in memory.
@param size: the amount of bytes to write.
:param int where: address to write to
:param expr: value to write
:type expr: int or BitVec
:param size: bit size of `expr`
'''
if size is None:
size = self.address_bit_size
@ -238,12 +243,12 @@ class Cpu(object):
def read_int(self, where, size=None):
'''
Reads anm integuer value of C{size} bits from memory at address C{where}.
Reads int from memory
@rtype: int or L{BitVec}
@param where: the address to read from.
@param size: the number of bits to read.
@return: the value read.
:param int where: address to read from
:param size: number of bits to read
:return: the value read
:rtype: int or BitVec
'''
if size is None:
size = self.address_bit_size
@ -256,20 +261,23 @@ class Cpu(object):
def write_bytes(self, where, data):
'''
Writes C{data} in the address C{where}.
Write a concrete or symbolic (or mixed) buffer to memory
@param where: address to write the data C{data}.
@param data: the data to write in the address C{where}.
:param int where: address to write to
:param data: data to write
:type data: str
'''
for i in xrange(len(data)):
self.write_int( where+i, Operators.ORD(data[i]), 8)
def read_bytes(self, where, size):
'''
Writes C{data} in the address C{where}.
Reads from memory
@param where: address to read the data C{data} from.
@param size: number of bytes.
:param int where: address to read data from
:param int size: number of bytes
:return: data
:rtype: list[int or Expression]
'''
result = []
for i in xrange(size):

71
manticore/core/state.py
View File

@ -9,6 +9,14 @@ class AbandonState(Exception):
class State(object):
'''
Representation of a unique program state/path.
:param ConstraintSet constraints: Initial constraints on state
:param model: Initial constraints on state
:type model: Decree or Linux or Windows
'''
# Class global counter
_state_count = manager.Value('i', 0)
_lock = manager.Lock()
@ -91,26 +99,23 @@ class State(object):
self.constraints.add(constraint)
def abandon(self):
'''Abandon the currently-active state
'''Abandon the currently-active state.
Note: This must be called from the Executor loop, or a user-provided
callback.'''
Note: This must be called from the Executor loop, or a :func:`~manticore.Manticore.hook`.
'''
raise AbandonState
def new_symbolic_buffer(self, nbytes, **options):
'''Create and return a symbolic buffer of length |nbytes|. The buffer is
'''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
:param int nbytes: Length of the new buffer
:param str name: (keyword arg only) The name to assign to the buffer
:param bool cstring: (keyword arg only) 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.
:return: :class:`~manticore.core.smtlib.expression.Expression` representing the buffer.
'''
name = options.get('name', 'buffer')
expr = self.constraints.new_array(name=name, index_max=nbytes)
@ -123,17 +128,15 @@ class State(object):
return expr
def new_symbolic_value(self, nbits, label='val', taint=frozenset()):
'''Create and return a symbolic value that is |nbits| bits wide. Assign
'''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.
:param int nbits: The bitwidth of the value returned
:param str label: The label to assign to the value
:param taint: Taint identifier of this value
:type taint: tuple or frozenset
:return: :class:`~manticore.core.smtlib.expression.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)
@ -143,15 +146,13 @@ class State(object):
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,
:param str 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
:param str label: The label to assign to the value
:param str wildcard: The byte that is considered a wildcard
:param bool string: Ensure bytes returned can not be \0
Returns:
If data does not contain any wildcard bytes, data itself. Otherwise,
:return: 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.
'''
@ -198,11 +199,25 @@ class State(object):
return solver
def solve_one(self, expr):
# type: (Expression) -> int
'''
Concretize a symbolic :class:`~manticore.core.smtlib.expression.Expression` into
one solution.
:param manticore.core.smtlib.Expression expr: Symbolic value to concretize
:return: Concrete value
:rtype: int
'''
return self._solver.get_value(self.constraints, expr)
def solve_n(self, expr, nsolves=1, policy='minmax'):
# type: (Expression, int) -> list
'''
Concretize a symbolic :class:`~manticore.core.smtlib.expression.Expression` into
`nsolves` solutions.
:param manticore.core.smtlib.Expression expr: Symbolic value to concretize
:return: Concrete value
:rtype: list[int]
'''
return self._solver.get_all_values(self.constraints, expr, nsolves, silent=True)
def record_branches(self, targets):

7
manticore/manticore.py
View File

@ -295,11 +295,8 @@ class Manticore(object):
@property
def verbosity(self):
'''
Convenience property for controlling the logging verbosity to a number of presets
:getter: Get current verbosity level
:setter: Set current verbosity level [0-5]
:type: int
Convenience interface for setting logging verbosity to one of several predefined
logging presets. Valid values: 0-5
'''
return self._verbosity

7
manticore/utils/helpers.py
View File

@ -3,7 +3,12 @@ from ..core.smtlib import Expression
def issymbolic(value):
'''
Helper to determine whether a value read is symbolic.
Helper to determine whether an object is symbolic (e.g checking
if data read from memory is symbolic)
:param object value: object to check
:return: whether `value` is symbolic
:rtype: bool
'''
return isinstance(value, Expression)