miasm.analysis.depgraph.DependencyResultImplicit Class Reference

Inheritance diagram for miasm.analysis.depgraph.DependencyResultImplicit:

Collaboration diagram for miasm.analysis.depgraph.DependencyResultImplicit:

Public Member Functions
def	emul (self, ir_arch, ctx=None, step=False)
def	is_satisfiable (self)
def	constraints (self)
Public Member Functions inherited from miasm.analysis.depgraph.DependencyResult
def	__init__ (self, ircfg, initial_state, state, inputs)
def	unresolved (self)
def	relevant_nodes (self)
def	relevant_loc_keys (self)
def	has_loop (self)
def	irblock_slice (self, irb, max_line=None)
Public Member Functions inherited from miasm.analysis.depgraph.DependencyState
def	__init__ (self, loc_key, pending, line_nb=None)
def	__repr__ (self)
def	extend (self, loc_key)
def	get_done_state (self)
def	as_graph (self)
def	graph (self)
def	remove_pendings (self, nodes)
def	add_pendings (self, future_pending)
def	link_element (self, element, line_nb)
def	link_dependencies (self, element, line_nb, dependencies, future_pending)

Static Public Attributes
	unsat_expr = ExprAssign(ExprInt(0, 1), ExprInt(1, 1))

Additional Inherited Members
Public Attributes inherited from miasm.analysis.depgraph.DependencyResult
	initial_state
	history
	pending
	line_nb
	inputs
	links
Public Attributes inherited from miasm.analysis.depgraph.DependencyState
	loc_key
	history
	pending
	line_nb
	links

Detailed Description

Stand for a result of a DependencyGraph with implicit option

Provide path constraints using the z3 solver

Member Function Documentation

constraints()

def miasm.analysis.depgraph.DependencyResultImplicit.constraints

(

self

)

If satisfiable, return a valid solution as a Z3 Model instance

Here is the call graph for this function:

emul()

def miasm.analysis.depgraph.DependencyResultImplicit.emul	(		self,
			ir_arch,
			ctx = None,
			step = False
	)

Symbolic execution of relevant nodes according to the history
Return the values of inputs nodes' elements
@ir_arch: IntermediateRepresentation instance
@ctx: (optional) Initial context as dictionary
@step: (optional) Verbose execution
Warning: The emulation is not sound if the inputs nodes depend on loop
variant.

Reimplemented from miasm.analysis.depgraph.DependencyResult.

Here is the call graph for this function:

is_satisfiable()

def miasm.analysis.depgraph.DependencyResultImplicit.is_satisfiable

(

self

)

Return True iff the solution path admits at least one solution
PRE: 'emul'

Here is the caller graph for this function:

Member Data Documentation

unsat_expr

miasm.analysis.depgraph.DependencyResultImplicit.unsat_expr = ExprAssign(ExprInt(0, 1), ExprInt(1, 1))

static

---

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

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