Miasm2
 All Classes Namespaces Files Functions Variables Typedefs Properties Macros
Public Member Functions | Static Private Attributes | List of all members
miasm2.analysis.depgraph.DependencyResultImplicit Class Reference
+ Inheritance diagram for miasm2.analysis.depgraph.DependencyResultImplicit:
+ Collaboration diagram for miasm2.analysis.depgraph.DependencyResultImplicit:

Public Member Functions

def emul
 
def is_satisfiable
 
def constraints
 
def graph
 
def history
 
def unresolved
 
def relevant_nodes
 
def relevant_labels
 
def input
 
def has_loop
 

Static Private Attributes

list __slots__
 
 _solver = None
 

Detailed Description

Stand for a result of a DependencyGraph with implicit option

Provide path constraints using the z3 solver

Definition at line 573 of file depgraph.py.

Member Function Documentation

def miasm2.analysis.depgraph.DependencyResultImplicit.constraints (   self) 
If satisfiable, return a valid solution as a Z3 Model instance

Definition at line 631 of file depgraph.py.

631 
632  def constraints(self):
633  """If satisfiable, return a valid solution as a Z3 Model instance"""
634  if not self.is_satisfiable:
635  raise ValueError("Unsatisfiable")
636  return self._solver.model()
637 

+ Here is the call graph for this function:

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

Definition at line 584 of file depgraph.py.

584 
585  def emul(self, ctx=None, step=False):
586  # Init
587  ctx_init = self._ira.arch.regs.regs_init
588  if ctx is not None:
589  ctx_init.update(ctx)
590  depnodes = self.relevant_nodes
591  solver = z3.Solver()
592  symb_exec = symbexec(self._ira, ctx_init)
593  temp_label = asm_label("Temp")
594  history = self.relevant_labels[::-1]
595  history_size = len(history)
596 
597  for hist_nb, label in enumerate(history):
598  # Build block with relevant lines only
599  affected_lines = set(depnode.line_nb for depnode in depnodes
600  if depnode.label == label)
601  irs = self._ira.blocs[label].irs
602  affects = []
603 
604  for line_nb in sorted(affected_lines):
605  affects.append(irs[line_nb])
606 
607  # Emul the block and get back destination
608  dst = symb_exec.emulbloc(irbloc(temp_label, affects), step=step)
609 
610  # Add constraint
611  if hist_nb + 1 < history_size:
612  next_label = history[hist_nb + 1]
613  expected = symb_exec.eval_expr(m2_expr.ExprId(next_label, 32))
614  constraint = m2_expr.ExprAff(dst, expected)
615  solver.add(Translator.to_language("z3").from_expr(constraint))
616 
617  # Save the solver
618  self._solver = solver
619 
620  # Return only inputs values (others could be wrongs)
621  return {depnode.element: symb_exec.symbols[depnode.element]
622  for depnode in self.input}
miasm2.core.asmbloc.asm_label
Definition: asmbloc.py:37

+ Here is the call graph for this function:

def miasm2.analysis.depgraph.DependencyResult.graph (   self)
inherited 
Returns a DiGraph instance representing the DependencyGraph

Definition at line 483 of file depgraph.py.

483 
484  def graph(self):
485  """Returns a DiGraph instance representing the DependencyGraph"""
486  if self._graph is None:
487  self._graph = self._depdict.as_graph(self._input_depnodes)
488  return self._graph
def miasm2.analysis.depgraph.DependencyResult.has_loop (   self)
inherited 
True if current dictionnary has a loop

Definition at line 532 of file depgraph.py.

532 
533  def has_loop(self):
534  """True if current dictionnary has a loop"""
535  if self._has_loop is None:
536  self._has_loop = (len(self.relevant_labels) !=
537  len(set(self.relevant_labels)))
538  return self._has_loop

+ Here is the call graph for this function:

def miasm2.analysis.depgraph.DependencyResult.history (   self)
inherited 
List of depdict corresponding to the blocks encountered in the
analysis

Definition at line 490 of file depgraph.py.

490 
491  def history(self):
492  """List of depdict corresponding to the blocks encountered in the
493  analysis"""
494  return list(self._depdict.history) + [self._depdict]

+ Here is the caller graph for this function:

def miasm2.analysis.depgraph.DependencyResult.input (   self)
inherited 
Set of DependencyGraph start nodes

Definition at line 527 of file depgraph.py.

527 
528  def input(self):
529  """Set of DependencyGraph start nodes"""
530  return self._input_depnodes

+ Here is the caller graph for this function:

def miasm2.analysis.depgraph.DependencyResultImplicit.is_satisfiable (   self) 
Return True iff the solution path admits at least one solution
PRE: 'emul'

Definition at line 624 of file depgraph.py.

624 
625  def is_satisfiable(self):
626  """Return True iff the solution path admits at least one solution
627  PRE: 'emul'
628  """
629  return self._solver.check().r > 0

+ Here is the caller graph for this function:

def miasm2.analysis.depgraph.DependencyResult.relevant_labels (   self)
inherited 
List of labels containing nodes influencing @self.input_depnodes.
The history order is preserved.

Definition at line 511 of file depgraph.py.

511 
512  def relevant_labels(self):
513  """List of labels containing nodes influencing @self.input_depnodes.
514  The history order is preserved.
515  """
516  # Get used labels
517  used_labels = set(depnode.label for depnode in self.relevant_nodes)
518 
519  # Keep history order
520  output = []
521  for label in [depdict.label for depdict in self.history]:
522  if label in used_labels:
523  output.append(label)
524 
525  return output

+ Here is the call graph for this function:

+ Here is the caller graph for this function:

def miasm2.analysis.depgraph.DependencyResult.relevant_nodes (   self)
inherited 
Set of nodes directly and indirectly influencing
@self.input_depnodes

Definition at line 502 of file depgraph.py.

502 
503  def relevant_nodes(self):
504  """Set of nodes directly and indirectly influencing
505  @self.input_depnodes"""
506  output = set()
507  for depnodes in self._depdict.cache.values():
508  output.update(depnodes)
509  return output

+ Here is the caller graph for this function:

def miasm2.analysis.depgraph.DependencyResult.unresolved (   self)
inherited 
Set of nodes whose dependencies weren't found

Definition at line 496 of file depgraph.py.

496 
497  def unresolved(self):
498  """Set of nodes whose dependencies weren't found"""
499  return set(node.nostep_repr for node in self._depdict.pending
500  if node.element != self._ira.IRDst)

Member Data Documentation

list miasm2.analysis.depgraph.DependencyResultImplicit.__slots__
staticprivate
Initial value:
1 = ["_ira", "_depdict", "_input_depnodes", "_graph",
2  "_has_loop", "_solver"]

Definition at line 578 of file depgraph.py.

miasm2.analysis.depgraph.DependencyResultImplicit._solver = None
staticprivate

Definition at line 582 of file depgraph.py.

The documentation for this class was generated from the following file:
Generated by   doxygen 1.8.8