miasm.analysis.dse.DSEPathConstraint Class Reference

Inheritance diagram for miasm.analysis.dse.DSEPathConstraint:

Collaboration diagram for miasm.analysis.dse.DSEPathConstraint:

Public Member Functions
def	__init__ (self, machine, loc_db, produce_solution=PRODUCE_SOLUTION_CODE_COV, known_solutions=None, **kwargs)
def	take_snapshot (self, *args, **kwargs)
def	restore_snapshot (self, snapshot, keep_known_solutions=True, **kwargs)
def	produce_solution (self, destination)
def	handle_solution (self, model, destination)
def	handle_correct_destination (self, destination, path_constraints)
def	handle (self, cur_addr)
Public Member Functions inherited from miasm.analysis.dse.DSEEngine
def	__init__ (self, machine, loc_db)
def	prepare (self)
def	attach (self, emulator)
def	add_handler (self, addr, callback)
def	add_lib_handler (self, libimp, namespace)
def	add_instrumentation (self, addr, callback)
def	callback (self, _)
def	take_snapshot (self)
def	restore_snapshot (self, snapshot, memory=True)
def	update_state (self, assignblk)
def	update_state_from_concrete (self, cpu=True, mem=False)
def	eval_expr (self, expr)
def	symbolize_memory (self, memory_range)

Public Attributes
	cur_solver
	new_solutions
	z3_trans
Public Attributes inherited from miasm.analysis.dse.DSEEngine
	machine
	loc_db
	handler
	instrumentation
	addr_to_cacheblocks
	ir_arch
	ircfg
	jitter
	symb
	Prepare symbexec engines. More...
	symb_concrete
	mdis

Static Public Attributes
int	MAX_MEMORY_INJECT = 0x10000
int	PRODUCE_NO_SOLUTION = 0
int	PRODUCE_SOLUTION_CODE_COV = 1
int	PRODUCE_SOLUTION_BRANCH_COV = 2
int	PRODUCE_SOLUTION_PATH_COV = 3
Static Public Attributes inherited from miasm.analysis.dse.DSEEngine
	SYMB_ENGINE = ESETrackModif

Additional Inherited Members
Static Public Member Functions inherited from miasm.analysis.dse.DSEEngine
def	memory_to_expr (addr)

Detailed Description

Dynamic Symbolic Execution Engine keeping the path constraint

Possible new "solutions" are produced along the path, by inversing concrete
path constraint. Thus, a "solution" is a potential initial context leading
to a new path.

In order to produce a new solution, one can extend this class, and override
'handle_solution' to produce a solution which fit its needs. It could avoid
computing new solution by overriding 'produce_solution'.

If one is only interested in constraints associated to its path, the option
"produce_solution" should be set to False, to speed up emulation.
The constraints are accumulated in the .z3_cur z3.Solver object.

Constructor & Destructor Documentation

__init__()

def miasm.analysis.dse.DSEPathConstraint.__init__	(		self,
			machine,
			loc_db,
			produce_solution = PRODUCE_SOLUTION_CODE_COV,
			known_solutions = None,
		**	kwargs
	)

Init a DSEPathConstraint
@machine: Machine of the targeted architecture instance
@produce_solution: (optional) if set, new solutions will be computed

Member Function Documentation

handle()

def miasm.analysis.dse.DSEPathConstraint.handle	(		self,
			cur_addr
	)

Handle destination
@cur_addr: Expr of the next address in concrete execution
/!\ cur_addr may be a loc_key

In this method, self.symb is in the "just before branching" state

Reimplemented from miasm.analysis.dse.DSEEngine.

Here is the call graph for this function:

handle_correct_destination()

def miasm.analysis.dse.DSEPathConstraint.handle_correct_destination	(		self,
			destination,
			path_constraints
	)

[DEV] Called by handle() to update internal structures giving the
correct destination (the concrete execution one).

Here is the call graph for this function:

Here is the caller graph for this function:

handle_solution()

def miasm.analysis.dse.DSEPathConstraint.handle_solution	(		self,
			model,
			destination
	)

Called when a new solution for destination @destination is founded
@model: z3 model instance
@destination: Expr instance for an addr which is not on the DSE path

Here is the call graph for this function:

Here is the caller graph for this function:

produce_solution()

def miasm.analysis.dse.DSEPathConstraint.produce_solution	(		self,
			destination
	)

Called to determine if a solution for @destination should be test for
satisfiability and computed
@destination: Expr instance of the target @destination

Here is the call graph for this function:

Here is the caller graph for this function:

restore_snapshot()

def miasm.analysis.dse.DSEPathConstraint.restore_snapshot	(		self,
			snapshot,
			keep_known_solutions = True,
		**	kwargs
	)

Restore a DSEPathConstraint snapshot
@keep_known_solutions: if set, do not forget solutions already found.
-> They will not appear in 'new_solutions'

Here is the call graph for this function:

take_snapshot()

def miasm.analysis.dse.DSEPathConstraint.take_snapshot	(		self,
		*	args,
		**	kwargs
	)

Member Data Documentation

cur_solver

miasm.analysis.dse.DSEPathConstraint.cur_solver

MAX_MEMORY_INJECT

int miasm.analysis.dse.DSEPathConstraint.MAX_MEMORY_INJECT = 0x10000

static

new_solutions

miasm.analysis.dse.DSEPathConstraint.new_solutions

PRODUCE_NO_SOLUTION

int miasm.analysis.dse.DSEPathConstraint.PRODUCE_NO_SOLUTION = 0

static

PRODUCE_SOLUTION_BRANCH_COV

int miasm.analysis.dse.DSEPathConstraint.PRODUCE_SOLUTION_BRANCH_COV = 2

static

PRODUCE_SOLUTION_CODE_COV

int miasm.analysis.dse.DSEPathConstraint.PRODUCE_SOLUTION_CODE_COV = 1

static

PRODUCE_SOLUTION_PATH_COV

int miasm.analysis.dse.DSEPathConstraint.PRODUCE_SOLUTION_PATH_COV = 3

static

z3_trans

miasm.analysis.dse.DSEPathConstraint.z3_trans

---

The documentation for this class was generated from the following file:

• /home/serpilliere/projet/test_doc_miasm/miasm/miasm/analysis/dse.py