parent
3e81cba8fb
commit
b612332132
@ -10,8 +10,8 @@ Ideally you should be able to do something like
|
|||||||
for th in binary.threads():
|
for th in binary.threads():
|
||||||
setup(th)
|
setup(th)
|
||||||
|
|
||||||
But there are difference between format that makes it difficult to find a siple and common API.
|
But there are difference between format that makes it difficult to find a simple
|
||||||
interpreters? linkers? linked dlls?
|
and common API. interpreters? linkers? linked DLLs?
|
||||||
|
|
||||||
'''
|
'''
|
||||||
|
|
||||||
|
|||||||
@ -442,7 +442,7 @@ class CONTEXT_amd64(Structure):
|
|||||||
("LastExceptionFromRip", "<Q")]
|
("LastExceptionFromRip", "<Q")]
|
||||||
|
|
||||||
class CONTEXT_arm32(Structure):
|
class CONTEXT_arm32(Structure):
|
||||||
# XXX: this structure is UNCOMPLETE
|
# XXX: this structure is INCOMPLETE
|
||||||
_fields_ = [("ContextFlags", "<I"), \
|
_fields_ = [("ContextFlags", "<I"), \
|
||||||
("R0", "<I"), \
|
("R0", "<I"), \
|
||||||
("R1", "<I"), \
|
("R1", "<I"), \
|
||||||
|
|||||||
@ -15,7 +15,7 @@ logger = logging.getLogger("CPU")
|
|||||||
|
|
||||||
|
|
||||||
SANE_SIZES = {8, 16, 32, 64, 80, 128, 256}
|
SANE_SIZES = {8, 16, 32, 64, 80, 128, 256}
|
||||||
# This encapsulates how to acccess operands (regs/mem/immediates) for differents cpus
|
# This encapsulates how to access operands (regs/mem/immediates) for different CPUs
|
||||||
class Operand(object):
|
class Operand(object):
|
||||||
|
|
||||||
class MemSpec(object):
|
class MemSpec(object):
|
||||||
@ -234,7 +234,7 @@ class Cpu(object):
|
|||||||
'''
|
'''
|
||||||
return self._regfile.read(register)
|
return self._regfile.read(register)
|
||||||
|
|
||||||
# Pythonic acces to registers and aliases
|
# Pythonic access to registers and aliases
|
||||||
def __getattr__(self, name):
|
def __getattr__(self, name):
|
||||||
'''
|
'''
|
||||||
A Pythonic version of read_register
|
A Pythonic version of read_register
|
||||||
@ -334,7 +334,7 @@ class Cpu(object):
|
|||||||
|
|
||||||
def decode_instruction(self, pc):
|
def decode_instruction(self, pc):
|
||||||
'''
|
'''
|
||||||
This will decode an intructcion from memory pointed by @pc
|
This will decode an instruction from memory pointed by @pc
|
||||||
|
|
||||||
:param int pc: address of the instruction
|
:param int pc: address of the instruction
|
||||||
'''
|
'''
|
||||||
@ -389,7 +389,7 @@ class Cpu(object):
|
|||||||
pass
|
pass
|
||||||
|
|
||||||
def execute(self):
|
def execute(self):
|
||||||
''' Decode, and execute one intruction pointed by register PC'''
|
''' Decode, and execute one instruction pointed by register PC'''
|
||||||
if not isinstance(self.PC, (int,long)):
|
if not isinstance(self.PC, (int,long)):
|
||||||
raise SymbolicPCException()
|
raise SymbolicPCException()
|
||||||
|
|
||||||
@ -467,7 +467,7 @@ class Cpu(object):
|
|||||||
|
|
||||||
|
|
||||||
class DecodeException(Exception):
|
class DecodeException(Exception):
|
||||||
''' Raised when trying to decode an unknown or invalid intruction '''
|
''' Raised when trying to decode an unknown or invalid instruction '''
|
||||||
def __init__(self, pc, bytes, extra):
|
def __init__(self, pc, bytes, extra):
|
||||||
super(DecodeException, self).__init__("Error decoding instruction @%08x", pc)
|
super(DecodeException, self).__init__("Error decoding instruction @%08x", pc)
|
||||||
self.pc=pc
|
self.pc=pc
|
||||||
|
|||||||
@ -286,7 +286,7 @@ class Armv7Cpu(Cpu):
|
|||||||
# Register file has the actual CPU flags
|
# Register file has the actual CPU flags
|
||||||
def setFlags(self, **flags):
|
def setFlags(self, **flags):
|
||||||
'''
|
'''
|
||||||
Note: For any unupdated flags, update _last_flags with the most recent
|
Note: For any unmodified flags, update _last_flags with the most recent
|
||||||
committed value. Otherwise, for example, this could happen:
|
committed value. Otherwise, for example, this could happen:
|
||||||
|
|
||||||
overflow=0
|
overflow=0
|
||||||
|
|||||||
@ -558,7 +558,7 @@ class AMD64RegFile(RegisterFile):
|
|||||||
|
|
||||||
register_id, ty, offset, size, reset = self._table[name]
|
register_id, ty, offset, size, reset = self._table[name]
|
||||||
if register_id != name:
|
if register_id != name:
|
||||||
#Fixme add a coulumn to _table with parent_size so we dont need to access the dict twice
|
#FIXME add a column to _table with parent_size so we don't need to access the dict twice
|
||||||
register_size = self._table[register_id].size
|
register_size = self._table[register_id].size
|
||||||
else:
|
else:
|
||||||
register_size = size
|
register_size = size
|
||||||
@ -741,7 +741,7 @@ class X86Cpu(Cpu):
|
|||||||
|
|
||||||
################################################
|
################################################
|
||||||
# This its unused but shouldn't be deleted!!!
|
# This its unused but shouldn't be deleted!!!
|
||||||
# The intruction cache must be invalidated after an executable
|
# The instruction cache must be invalidated after an executable
|
||||||
# page was changed or removed or added
|
# page was changed or removed or added
|
||||||
def invalidate_cache(cpu, address, size):
|
def invalidate_cache(cpu, address, size):
|
||||||
''' remove decoded instruction from instruction cache '''
|
''' remove decoded instruction from instruction cache '''
|
||||||
@ -814,7 +814,7 @@ class X86Cpu(Cpu):
|
|||||||
|
|
||||||
:param cpu: current CPU.
|
:param cpu: current CPU.
|
||||||
'''
|
'''
|
||||||
#FIXME Choose conserative values and consider returning some default when eax not here
|
#FIXME Choose conservative values and consider returning some default when eax not here
|
||||||
conf = { 0x0: (0x0000000d, 0x756e6547, 0x6c65746e, 0x49656e69),
|
conf = { 0x0: (0x0000000d, 0x756e6547, 0x6c65746e, 0x49656e69),
|
||||||
0x1: (0x000306c3, 0x05100800, 0x7ffafbff, 0xbfebfbff),
|
0x1: (0x000306c3, 0x05100800, 0x7ffafbff, 0xbfebfbff),
|
||||||
0x2: (0x76035a01, 0x00f0b5ff, 0x00000000, 0x00c10000),
|
0x2: (0x76035a01, 0x00f0b5ff, 0x00000000, 0x00c10000),
|
||||||
@ -3606,7 +3606,7 @@ class X86Cpu(Cpu):
|
|||||||
dest.write(new_val)
|
dest.write(new_val)
|
||||||
|
|
||||||
cpu.CF = Operators.ITE(tempCount != 0, (left & 1) == 1, cpu.CF)
|
cpu.CF = Operators.ITE(tempCount != 0, (left & 1) == 1, cpu.CF)
|
||||||
#for RCR these are calcualted before rotation starts
|
#for RCR these are calculated before rotation starts
|
||||||
s_MSB = ((new_val >> (OperandSize-1)) & 0x1) == 1
|
s_MSB = ((new_val >> (OperandSize-1)) & 0x1) == 1
|
||||||
s_MSB2 = ((new_val >> (OperandSize-2)) & 0x1) == 1
|
s_MSB2 = ((new_val >> (OperandSize-2)) & 0x1) == 1
|
||||||
cpu.OF = Operators.ITE(tempCount==1,
|
cpu.OF = Operators.ITE(tempCount==1,
|
||||||
@ -3762,7 +3762,7 @@ class X86Cpu(Cpu):
|
|||||||
|
|
||||||
SIGN_MASK = (1<<(OperandSize-1))
|
SIGN_MASK = (1<<(OperandSize-1))
|
||||||
|
|
||||||
# We can't use this one as the 'true' expresion gets eagerly calculated even on count == 0 + cpu.CF = Operators.ITE(count!=0, ((value >> Operators.ZEXTEND(count-1, OperandSize)) & 1) !=0, cpu.CF)
|
# We can't use this one as the 'true' expression gets eagerly calculated even on count == 0 + cpu.CF = Operators.ITE(count!=0, ((value >> Operators.ZEXTEND(count-1, OperandSize)) & 1) !=0, cpu.CF)
|
||||||
# cpu.CF = Operators.ITE(count!=0, ((value >> Operators.ZEXTEND(count-1, OperandSize)) & 1) !=0, cpu.CF)
|
# cpu.CF = Operators.ITE(count!=0, ((value >> Operators.ZEXTEND(count-1, OperandSize)) & 1) !=0, cpu.CF)
|
||||||
|
|
||||||
if issymbolic(count):
|
if issymbolic(count):
|
||||||
@ -4353,7 +4353,7 @@ class X86Cpu(Cpu):
|
|||||||
the ES:RDI, ES:EDI or the ES:DI registers (depending on the address-size
|
the ES:RDI, ES:EDI or the ES:DI registers (depending on the address-size
|
||||||
attribute of the instruction, 32 or 16, respectively)::
|
attribute of the instruction, 32 or 16, respectively)::
|
||||||
|
|
||||||
IF (byte cmparison)
|
IF (byte comparison)
|
||||||
THEN
|
THEN
|
||||||
temp = AL - SRC;
|
temp = AL - SRC;
|
||||||
SetStatusFlags(temp);
|
SetStatusFlags(temp);
|
||||||
@ -4799,7 +4799,7 @@ class X86Cpu(Cpu):
|
|||||||
:param cpu: current CPU.
|
:param cpu: current CPU.
|
||||||
:param op0: destination operand.
|
:param op0: destination operand.
|
||||||
:param op1: source operand.
|
:param op1: source operand.
|
||||||
@todo: check alingment.
|
@todo: check alignment.
|
||||||
'''
|
'''
|
||||||
op0.write(op1.read())
|
op0.write(op1.read())
|
||||||
|
|
||||||
@ -5120,7 +5120,7 @@ class X86Cpu(Cpu):
|
|||||||
Packed subtract.
|
Packed subtract.
|
||||||
|
|
||||||
Performs a SIMD subtract of the packed integers of the source operand (second operand) from the packed
|
Performs a SIMD subtract of the packed integers of the source operand (second operand) from the packed
|
||||||
integers of the destpination operand (first operand), and stores the packed integer results in the
|
integers of the destination operand (first operand), and stores the packed integer results in the
|
||||||
destination operand. The source operand can be an MMX(TM) technology register or a 64-bit memory location,
|
destination operand. The source operand can be an MMX(TM) technology register or a 64-bit memory location,
|
||||||
or it can be an XMM register or a 128-bit memory location. The destination operand can be an MMX or an XMM
|
or it can be an XMM register or a 128-bit memory location. The destination operand can be an MMX or an XMM
|
||||||
register.
|
register.
|
||||||
@ -5341,9 +5341,9 @@ class X86Cpu(Cpu):
|
|||||||
to move data between two XMM registers.
|
to move data between two XMM registers.
|
||||||
|
|
||||||
When the source or destination operand is a memory operand, the operand
|
When the source or destination operand is a memory operand, the operand
|
||||||
must be aligned on a 16-byte boundaryor a general-protection exception
|
must be aligned on a 16-byte boundary or a general-protection exception
|
||||||
(#GP) will be generated. To move integer data to and from unaligned
|
(#GP) will be generated. To move integer data to and from unaligned
|
||||||
memorylocations, use the VMOVDQU instruction.'''
|
memory locations, use the VMOVDQU instruction.'''
|
||||||
#TODO raise exception when unaligned!
|
#TODO raise exception when unaligned!
|
||||||
dest.write(src.read())
|
dest.write(src.read())
|
||||||
|
|
||||||
@ -5516,7 +5516,7 @@ class X86Cpu(Cpu):
|
|||||||
|
|
||||||
if issymbolic(selector):
|
if issymbolic(selector):
|
||||||
# need to check if selector can be any of cpu_segments.keys()
|
# need to check if selector can be any of cpu_segments.keys()
|
||||||
# and if so concretize acordinglyi
|
# and if so concretize accordingly
|
||||||
raise NotImplementedError("Do not yet implement symbolic LSL")
|
raise NotImplementedError("Do not yet implement symbolic LSL")
|
||||||
|
|
||||||
#Checks that the segment selector is not null.
|
#Checks that the segment selector is not null.
|
||||||
|
|||||||
@ -546,11 +546,11 @@ class Executor(object):
|
|||||||
assert remaining > 0
|
assert remaining > 0
|
||||||
vals = random.sample(vals, min(remaining, len(vals)) )
|
vals = random.sample(vals, min(remaining, len(vals)) )
|
||||||
else:
|
else:
|
||||||
#No room really so keep only one (Which will replace the curent state)
|
#No room really so keep only one (Which will replace the current state)
|
||||||
vals = random.sample(vals, 1)
|
vals = random.sample(vals, 1)
|
||||||
logger.debug("Sampled possible values are: %s", ["0x%016x"%x for x in vals])
|
logger.debug("Sampled possible values are: %s", ["0x%016x"%x for x in vals])
|
||||||
|
|
||||||
#Check if we are using too much stoage
|
#Check if we are using too much storage
|
||||||
if self.max_storage != 0:
|
if self.max_storage != 0:
|
||||||
total_used_storage = self.getTotalUsedStorage()
|
total_used_storage = self.getTotalUsedStorage()
|
||||||
if total_used_storage > self.max_storage:
|
if total_used_storage > self.max_storage:
|
||||||
@ -603,7 +603,7 @@ class Executor(object):
|
|||||||
|
|
||||||
def _stopRun(self, count=0):
|
def _stopRun(self, count=0):
|
||||||
#notify siblings we are about to stop this run
|
#notify siblings we are about to stop this run
|
||||||
#log how many intruction were executed
|
#log how many instructions were executed
|
||||||
with self._lock:
|
with self._lock:
|
||||||
self._running.value-=1
|
self._running.value-=1
|
||||||
self._count.value += count
|
self._count.value += count
|
||||||
@ -633,7 +633,7 @@ class Executor(object):
|
|||||||
|
|
||||||
while not self.isShutdown():
|
while not self.isShutdown():
|
||||||
try:
|
try:
|
||||||
#select a suitable state to analize
|
#select a suitable state to analyze
|
||||||
if current_state is None:
|
if current_state is None:
|
||||||
|
|
||||||
#notify siblings we are about to stop this run
|
#notify siblings we are about to stop this run
|
||||||
|
|||||||
@ -5,7 +5,7 @@ import mmap as MMAP
|
|||||||
mmap_function = None
|
mmap_function = None
|
||||||
munmap_function = None
|
munmap_function = None
|
||||||
|
|
||||||
#initialize glogal functions depeding on platform
|
# initialize global functions depending on platform
|
||||||
osname = sys.platform.lower()
|
osname = sys.platform.lower()
|
||||||
if osname == "darwin" or osname.startswith("linux"):
|
if osname == "darwin" or osname.startswith("linux"):
|
||||||
|
|
||||||
|
|||||||
@ -30,7 +30,7 @@ class SymbolicMemoryException(MemoryException):
|
|||||||
|
|
||||||
def __init__(self, cause, address, size, constraint):
|
def __init__(self, cause, address, size, constraint):
|
||||||
super(SymbolicMemoryException, self, ).__init__(cause, address)
|
super(SymbolicMemoryException, self, ).__init__(cause, address)
|
||||||
#the crashing contraint you need to assert
|
#the crashing constraint you need to assert
|
||||||
self.constraint = constraint
|
self.constraint = constraint
|
||||||
self.size = size
|
self.size = size
|
||||||
|
|
||||||
@ -84,7 +84,7 @@ class Map(object):
|
|||||||
perms = property(_get_perms, _set_perms)
|
perms = property(_get_perms, _set_perms)
|
||||||
|
|
||||||
def access_ok(self, access):
|
def access_ok(self, access):
|
||||||
''' Check if there is onough permissions for access '''
|
''' Check if there is enough permissions for access '''
|
||||||
for c in access:
|
for c in access:
|
||||||
if c not in self.perms:
|
if c not in self.perms:
|
||||||
return False
|
return False
|
||||||
@ -719,7 +719,7 @@ class Memory(object):
|
|||||||
self.callback[name] = callback
|
self.callback[name] = callback
|
||||||
|
|
||||||
def perms(self, index):
|
def perms(self, index):
|
||||||
# not happy with ths interface.
|
# not happy with this interface.
|
||||||
if isinstance(index, slice):
|
if isinstance(index, slice):
|
||||||
# get the more restrictive set of perms for the range
|
# get the more restrictive set of perms for the range
|
||||||
raise NotImplementedError('No perms for slices')
|
raise NotImplementedError('No perms for slices')
|
||||||
@ -898,7 +898,7 @@ class SMemory(Memory):
|
|||||||
condition = Operators.OR(address == base, condition )
|
condition = Operators.OR(address == base, condition )
|
||||||
raise ForkState(condition)
|
raise ForkState(condition)
|
||||||
|
|
||||||
#So here we have all potential solutions to addreess
|
#So here we have all potential solutions to address
|
||||||
assert len(solutions) > 0
|
assert len(solutions) > 0
|
||||||
|
|
||||||
|
|
||||||
|
|||||||
@ -189,7 +189,7 @@ class ConstraintSet(object):
|
|||||||
return BoolVariable(name, taint=taint)
|
return BoolVariable(name, taint=taint)
|
||||||
|
|
||||||
def new_bitvec(self, size, name='V', taint=frozenset()):
|
def new_bitvec(self, size, name='V', taint=frozenset()):
|
||||||
''' Declares a free symbolic bitvectore in the constraint store
|
''' Declares a free symbolic bitvector in the constraint store
|
||||||
:param size: size in bits for the bitvector
|
:param size: size in bits for the bitvector
|
||||||
:param name: try to assign name to internal variable representation,
|
:param name: try to assign name to internal variable representation,
|
||||||
if not uniq a numeric nonce will be appended
|
if not uniq a numeric nonce will be appended
|
||||||
|
|||||||
@ -1,17 +1,17 @@
|
|||||||
###############################################################################
|
###############################################################################
|
||||||
# Solver
|
# Solver
|
||||||
# A solver maintains a companion smtlib capable proceess connected via stdio.
|
# A solver maintains a companion smtlib capable process connected via stdio.
|
||||||
# It can be in 4 main states: None, unknown, sat, unsat
|
# It can be in 4 main states: None, unknown, sat, unsat
|
||||||
# None nothing was yet sent to the smtlib proccess. Al the state is only at the python side
|
# None nothing was yet sent to the smtlib process. Al the state is only at the python side
|
||||||
# unknown is an error state. Some query sent early was unsuccessful or timed out. Further
|
# unknown is an error state. Some query sent early was unsuccessful or timed out. Further
|
||||||
# interaction with the smtlib proccess will probably kept beign unknown. An exception is raised.
|
# interaction with the smtlib process will probably kept beign unknown. An exception is raised.
|
||||||
# sat the current set of constraints is sat-isfiable and has at least one solution
|
# sat the current set of constraints is satisfiable and has at least one solution
|
||||||
# unsat the current set of constraints is impossible
|
# unsat the current set of constraints is impossible
|
||||||
#
|
#
|
||||||
# It starts at None.
|
# It starts at None.
|
||||||
# Once you Solver.check() it the status is changed to sat or unsat (or unknown+exception)
|
# Once you Solver.check() it the status is changed to sat or unsat (or unknown+exception)
|
||||||
# You can create new symbols operate on them. The declarations will be sended to the smtlib proceess when needed.
|
# You can create new symbols operate on them. The declarations will be sent to the smtlib process when needed.
|
||||||
# You can add new constraints. A new contraint may change the state from {None, sat} to {sat, unsat, unknown}
|
# You can add new constraints. A new constraint may change the state from {None, sat} to {sat, unsat, unknown}
|
||||||
|
|
||||||
from subprocess import PIPE, Popen, check_output
|
from subprocess import PIPE, Popen, check_output
|
||||||
from abc import ABCMeta, abstractmethod
|
from abc import ABCMeta, abstractmethod
|
||||||
@ -51,10 +51,10 @@ class Solver(object):
|
|||||||
|
|
||||||
@abstractmethod
|
@abstractmethod
|
||||||
def optimize(self, X, operation, M=10000):
|
def optimize(self, X, operation, M=10000):
|
||||||
''' Iterativelly finds the maximun or minimal value for the operation
|
''' Iterativelly finds the maximum or minimal value for the operation
|
||||||
(Normally Operators.UGT or Operators.ULT)
|
(Normally Operators.UGT or Operators.ULT)
|
||||||
:param X: a symbol or expression
|
:param X: a symbol or expression
|
||||||
:param M: maximun number of iterations allowed
|
:param M: maximum number of iterations allowed
|
||||||
'''
|
'''
|
||||||
pass
|
pass
|
||||||
|
|
||||||
@ -74,7 +74,7 @@ class Solver(object):
|
|||||||
|
|
||||||
@abstractmethod
|
@abstractmethod
|
||||||
def get_value(self, constraints, expression):
|
def get_value(self, constraints, expression):
|
||||||
''' Ask the solver for one possible assigment for expression using currrent set
|
''' Ask the solver for one possible assignment for expression using current set
|
||||||
of constraints.
|
of constraints.
|
||||||
The current set of assertions must be sat.
|
The current set of assertions must be sat.
|
||||||
:param val: an expression or symbol '''
|
:param val: an expression or symbol '''
|
||||||
@ -83,7 +83,7 @@ class Solver(object):
|
|||||||
def max(self, constraints, X, M=10000):
|
def max(self, constraints, X, M=10000):
|
||||||
''' Iterativelly finds the maximum value for a symbol.
|
''' Iterativelly finds the maximum value for a symbol.
|
||||||
:param X: a symbol or expression
|
:param X: a symbol or expression
|
||||||
:param M: maximun number of iterations allowed
|
:param M: maximum number of iterations allowed
|
||||||
'''
|
'''
|
||||||
assert isinstance(X, BitVec)
|
assert isinstance(X, BitVec)
|
||||||
return self.optimize(constraints, X, 'maximize')
|
return self.optimize(constraints, X, 'maximize')
|
||||||
@ -91,7 +91,7 @@ class Solver(object):
|
|||||||
def min(self, constraints, X, M=10000):
|
def min(self, constraints, X, M=10000):
|
||||||
''' Iterativelly finds the minimum value for a symbol.
|
''' Iterativelly finds the minimum value for a symbol.
|
||||||
:param X: a symbol or expression
|
:param X: a symbol or expression
|
||||||
:param M: maximun number of iterations allowed
|
:param M: maximum number of iterations allowed
|
||||||
'''
|
'''
|
||||||
assert isinstance(X, BitVec)
|
assert isinstance(X, BitVec)
|
||||||
return self.optimize(constraints, X, 'minimize')
|
return self.optimize(constraints, X, 'minimize')
|
||||||
@ -112,7 +112,7 @@ consider_unknown_as_unsat = True
|
|||||||
Version = collections.namedtuple('Version', 'major minor patch')
|
Version = collections.namedtuple('Version', 'major minor patch')
|
||||||
class Z3Solver(Solver):
|
class Z3Solver(Solver):
|
||||||
def __init__(self):
|
def __init__(self):
|
||||||
''' Build a Z3 solver intance.
|
''' Build a Z3 solver instance.
|
||||||
This is implemented using an external z3 solver (via a subprocess).
|
This is implemented using an external z3 solver (via a subprocess).
|
||||||
'''
|
'''
|
||||||
super(Z3Solver, self).__init__()
|
super(Z3Solver, self).__init__()
|
||||||
@ -162,7 +162,7 @@ class Z3Solver(Solver):
|
|||||||
|
|
||||||
|
|
||||||
def _start_proc(self):
|
def _start_proc(self):
|
||||||
''' Auxiliary method to spawn the external solver pocess'''
|
''' Auxiliary method to spawn the external solver process'''
|
||||||
assert '_proc' not in dir(self) or self._proc is None
|
assert '_proc' not in dir(self) or self._proc is None
|
||||||
try:
|
try:
|
||||||
self._proc = Popen(self._command.split(' '), stdin=PIPE, stdout=PIPE )
|
self._proc = Popen(self._command.split(' '), stdin=PIPE, stdout=PIPE )
|
||||||
@ -280,7 +280,7 @@ class Z3Solver(Solver):
|
|||||||
self._send('(assert %s)'%smtlib)
|
self._send('(assert %s)'%smtlib)
|
||||||
|
|
||||||
def _getvalue(self, expression):
|
def _getvalue(self, expression):
|
||||||
''' Ask the solver for one possible assigment for val using currrent set
|
''' Ask the solver for one possible assignment for val using current set
|
||||||
of constraints.
|
of constraints.
|
||||||
The current set of assertions must be sat.
|
The current set of assertions must be sat.
|
||||||
:param val: an expression or symbol '''
|
:param val: an expression or symbol '''
|
||||||
@ -365,10 +365,10 @@ class Z3Solver(Solver):
|
|||||||
|
|
||||||
#@memoized
|
#@memoized
|
||||||
def optimize(self, constraints, x, goal, M=10000):
|
def optimize(self, constraints, x, goal, M=10000):
|
||||||
''' Iterativelly finds the maximun or minimal value for the operation
|
''' Iterativelly finds the maximum or minimal value for the operation
|
||||||
(Normally Operators.UGT or Operators.ULT)
|
(Normally Operators.UGT or Operators.ULT)
|
||||||
:param X: a symbol or expression
|
:param X: a symbol or expression
|
||||||
:param M: maximun number of iterations allowed
|
:param M: maximum number of iterations allowed
|
||||||
'''
|
'''
|
||||||
assert goal in ('maximize', 'minimize')
|
assert goal in ('maximize', 'minimize')
|
||||||
assert isinstance(x, BitVec)
|
assert isinstance(x, BitVec)
|
||||||
@ -418,7 +418,7 @@ class Z3Solver(Solver):
|
|||||||
|
|
||||||
#@memoized
|
#@memoized
|
||||||
def get_value(self, constraints, expression):
|
def get_value(self, constraints, expression):
|
||||||
''' Ask the solver for one possible assigment for val using currrent set
|
''' Ask the solver for one possible assignment for val using current set
|
||||||
of constraints.
|
of constraints.
|
||||||
The current set of assertions must be sat.
|
The current set of assertions must be sat.
|
||||||
:param val: an expression or symbol '''
|
:param val: an expression or symbol '''
|
||||||
|
|||||||
@ -293,7 +293,7 @@ class Linux(object):
|
|||||||
stdin.peer = self.output
|
stdin.peer = self.output
|
||||||
stdout.peer = self.output
|
stdout.peer = self.output
|
||||||
stderr.peer = self.stderr
|
stderr.peer = self.stderr
|
||||||
#A receive from stdin will get data from inp
|
#A receive from stdin will get data from input
|
||||||
self.input.peer = stdin
|
self.input.peer = stdin
|
||||||
#A receive on stdout or stderr will return no data (rx_bytes: 0)
|
#A receive on stdout or stderr will return no data (rx_bytes: 0)
|
||||||
|
|
||||||
@ -1232,7 +1232,7 @@ class Linux(object):
|
|||||||
:param cpu: current CPU.
|
:param cpu: current CPU.
|
||||||
:param start: the starting address to change the permissions.
|
:param start: the starting address to change the permissions.
|
||||||
:param size: the size of the portion of memory to change the permissions.
|
:param size: the size of the portion of memory to change the permissions.
|
||||||
:param prot: the new acces premission for the memory.
|
:param prot: the new access permission for the memory.
|
||||||
:return: C{0} on success.
|
:return: C{0} on success.
|
||||||
'''
|
'''
|
||||||
perms = perms_from_protflags(prot)
|
perms = perms_from_protflags(prot)
|
||||||
@ -1610,8 +1610,8 @@ class Linux(object):
|
|||||||
self._current = next
|
self._current = next
|
||||||
|
|
||||||
def wait(self, readfds, writefds, timeout):
|
def wait(self, readfds, writefds, timeout):
|
||||||
''' Wait for filedescriptors or timout.
|
''' Wait for file descriptors or timeout.
|
||||||
Adds the current process in the correspondant wainting list and
|
Adds the current process in the correspondent waiting list and
|
||||||
yield the cpu to another running process.
|
yield the cpu to another running process.
|
||||||
'''
|
'''
|
||||||
logger.debug("WAIT:")
|
logger.debug("WAIT:")
|
||||||
@ -1642,8 +1642,8 @@ class Linux(object):
|
|||||||
self.check_timers()
|
self.check_timers()
|
||||||
|
|
||||||
def awake(self, procid):
|
def awake(self, procid):
|
||||||
''' Remove procid from waitlists and restablish it in the running list '''
|
''' Remove procid from waitlists and reestablish it in the running list '''
|
||||||
logger.debug("Remove procid:%d from waitlists and restablish it in the running list", procid)
|
logger.debug("Remove procid:%d from waitlists and reestablish it in the running list", procid)
|
||||||
for wait_list in self.rwait:
|
for wait_list in self.rwait:
|
||||||
if procid in wait_list: wait_list.remove(procid)
|
if procid in wait_list: wait_list.remove(procid)
|
||||||
for wait_list in self.twait:
|
for wait_list in self.twait:
|
||||||
|
|||||||
@ -37,7 +37,7 @@ class SymbolicSyscallArgument(ConcretizeRegister):
|
|||||||
reg_name = ['EBX', 'ECX', 'EDX', 'ESI', 'EDI', 'EBP' ][number]
|
reg_name = ['EBX', 'ECX', 'EDX', 'ESI', 'EDI', 'EBP' ][number]
|
||||||
super(SymbolicSyscallArgument, self).__init__(reg_name, message, policy)
|
super(SymbolicSyscallArgument, self).__init__(reg_name, message, policy)
|
||||||
|
|
||||||
#FIXME Cosider movnig this to executor.state?
|
#FIXME Consider moving this to executor.state?
|
||||||
def toStr(state, value):
|
def toStr(state, value):
|
||||||
if issymbolic(value):
|
if issymbolic(value):
|
||||||
minmax = solver.get_all_values(state.constraints, value, maxcnt=2, silent=True)
|
minmax = solver.get_all_values(state.constraints, value, maxcnt=2, silent=True)
|
||||||
@ -313,7 +313,7 @@ class Windows(object):
|
|||||||
|
|
||||||
def execute(self):
|
def execute(self):
|
||||||
"""
|
"""
|
||||||
Execute one cpu instruction in the current thread (only one suported).
|
Execute one cpu instruction in the current thread (only one supported).
|
||||||
:rtype: bool
|
:rtype: bool
|
||||||
:return: C{True}
|
:return: C{True}
|
||||||
|
|
||||||
|
|||||||
@ -146,7 +146,7 @@ class UnicornEmulator(object):
|
|||||||
if self._cpu.arch == CS_ARCH_ARM:
|
if self._cpu.arch == CS_ARCH_ARM:
|
||||||
return globals()['UC_ARM_REG_' + reg_name]
|
return globals()['UC_ARM_REG_' + reg_name]
|
||||||
elif self._cpu.arch == CS_ARCH_X86:
|
elif self._cpu.arch == CS_ARCH_X86:
|
||||||
# TODO(yan): This needs to handle AF regiseter
|
# TODO(yan): This needs to handle AF register
|
||||||
return globals()['UC_X86_REG_' + reg_name]
|
return globals()['UC_X86_REG_' + reg_name]
|
||||||
else:
|
else:
|
||||||
# TODO(yan): raise a more appropriate exception
|
# TODO(yan): raise a more appropriate exception
|
||||||
|
|||||||
Loading…
x
Reference in New Issue
Block a user