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

Public Member Functions

def __init__
 
def from_ExprInt
 
def from_ExprId
 
def from_ExprMem
 
def from_ExprSlice
 
def from_ExprCompose
 
def from_ExprCond
 
def from_ExprOp
 
def from_ExprAff
 
def register
 
def to_language
 
def available_languages
 
def from_expr
 

Static Public Attributes

list trivial_ops = ["+", "-", "/", "%", "&", "^", "|", "*", "<<"]
 
list available_translators = []
 

Private Attributes

 _mem
 

Static Private Attributes

string __LANG__ = "z3"
 

Detailed Description

Translate a Miasm expression to an equivalent z3 python binding
expression. Memory is abstracted via z3.Array (see Z3Mem).
The result of from_expr will be a z3 Expr.

If you want to interract with the memory abstraction after the translation,
you can instanciate your own Z3Mem, that will be equivalent to the one
used by TranslatorZ3.

Definition at line 98 of file z3_ir.py.

Constructor & Destructor Documentation

def miasm2.ir.translators.z3_ir.TranslatorZ3.__init__ (   self,
  endianness = "<",
  kwargs 
)
Instance a Z3 translator
@endianness: (optional) memory endianness

Definition at line 113 of file z3_ir.py.

114  def __init__(self, endianness="<", **kwargs):
115  """Instance a Z3 translator
116  @endianness: (optional) memory endianness
117  """
118  super(TranslatorZ3, self).__init__(**kwargs)
119  self._mem = Z3Mem(endianness)

Member Function Documentation

def miasm2.ir.translators.translator.Translator.available_languages (   cls)
inherited

Definition at line 34 of file translator.py.

34 
35  def available_languages(cls):
36  "Return the list of registered languages"
37  return [translator.__LANG__ for translator in cls.available_translators]
def miasm2.ir.translators.translator.Translator.from_expr (   self,
  expr 
)
inherited
Translate an expression according to its type
@expr: expression to translate

Definition at line 92 of file translator.py.

92 
93  def from_expr(self, expr):
94  """Translate an expression according to its type
95  @expr: expression to translate
96  """
97  # Use cache
98  if expr in self._cache:
99  return self._cache[expr]
100 
101  # Handle Expr type
102  handlers = {m2_expr.ExprInt: self.from_ExprInt,
103  m2_expr.ExprId: self.from_ExprId,
104  m2_expr.ExprCompose: self.from_ExprCompose,
105  m2_expr.ExprSlice: self.from_ExprSlice,
106  m2_expr.ExprOp: self.from_ExprOp,
107  m2_expr.ExprMem: self.from_ExprMem,
108  m2_expr.ExprAff: self.from_ExprAff,
109  m2_expr.ExprCond: self.from_ExprCond
110  }
111  for target, handler in handlers.iteritems():
112  if isinstance(expr, target):
113  ## Compute value and update the internal cache
114  ret = handler(expr)
115  self._cache[expr] = ret
116  return ret
117  raise ValueError("Unhandled type for %s" % expr)
118 

+ Here is the call graph for this function:

+ Here is the caller graph for this function:

def miasm2.ir.translators.z3_ir.TranslatorZ3.from_ExprAff (   self,
  expr 
)

Definition at line 196 of file z3_ir.py.

197  def from_ExprAff(self, expr):
198  src = self.from_expr(expr.src)
199  dst = self.from_expr(expr.dst)
200  return (src == dst)
201 
202 
203 # Register the class
204 Translator.register(TranslatorZ3)

+ Here is the call graph for this function:

def miasm2.ir.translators.z3_ir.TranslatorZ3.from_ExprCompose (   self,
  expr 
)

Definition at line 138 of file z3_ir.py.

139  def from_ExprCompose(self, expr):
140  res = None
141  args = sorted(expr.args, key=operator.itemgetter(2)) # sort by start off
142  for subexpr, start, stop in args:
143  sube = self.from_expr(subexpr)
144  e = z3.Extract(stop-start-1, 0, sube)
145  if res:
146  res = z3.Concat(e, res)
147  else:
148  res = e
149  return res

+ Here is the call graph for this function:

def miasm2.ir.translators.z3_ir.TranslatorZ3.from_ExprCond (   self,
  expr 
)

Definition at line 150 of file z3_ir.py.

151  def from_ExprCond(self, expr):
152  cond = self.from_expr(expr.cond)
153  src1 = self.from_expr(expr.src1)
154  src2 = self.from_expr(expr.src2)
155  return z3.If(cond != 0, src1, src2)

+ Here is the call graph for this function:

def miasm2.ir.translators.z3_ir.TranslatorZ3.from_ExprId (   self,
  expr 
)

Definition at line 123 of file z3_ir.py.

124  def from_ExprId(self, expr):
125  if isinstance(expr.name, asm_label) and expr.name.offset is not None:
126  return z3.BitVecVal(expr.name.offset, expr.size)
127  else:
128  return z3.BitVec(str(expr), expr.size)
def miasm2.ir.translators.z3_ir.TranslatorZ3.from_ExprInt (   self,
  expr 
)

Definition at line 120 of file z3_ir.py.

121  def from_ExprInt(self, expr):
122  return z3.BitVecVal(expr.arg.arg, expr.size)
def miasm2.ir.translators.z3_ir.TranslatorZ3.from_ExprMem (   self,
  expr 
)

Definition at line 129 of file z3_ir.py.

130  def from_ExprMem(self, expr):
131  addr = self.from_expr(expr.arg)
132  return self._mem.get(addr, expr.size)

+ Here is the call graph for this function:

def miasm2.ir.translators.z3_ir.TranslatorZ3.from_ExprOp (   self,
  expr 
)

Definition at line 156 of file z3_ir.py.

157  def from_ExprOp(self, expr):
158  args = map(self.from_expr, expr.args)
159  res = args[0]
160 
161  if len(args) > 1:
162  for arg in args[1:]:
163  if expr.op in self.trivial_ops:
164  res = eval("res %s arg" % expr.op)
165  elif expr.op == ">>":
166  res = z3.LShR(res, arg)
167  elif expr.op == "a>>":
168  res = res >> arg
169  elif expr.op == "a<<":
170  res = res << arg
171  elif expr.op == "<<<":
172  res = z3.RotateLeft(res, arg)
173  elif expr.op == ">>>":
174  res = z3.RotateRight(res, arg)
175  elif expr.op == "idiv":
176  res = res / arg
177  elif expr.op == "udiv":
178  res = z3.UDiv(res, arg)
179  elif expr.op == "imod":
180  res = res % arg
181  elif expr.op == "umod":
182  res = z3.URem(res, arg)
183  else:
184  raise NotImplementedError("Unsupported OP yet: %s" % expr.op)
185  elif expr.op == 'parity':
186  arg = z3.Extract(7, 0, res)
187  res = z3.BitVecVal(1, 1)
188  for i in xrange(8):
189  res = res ^ z3.Extract(i, i, arg)
190  elif expr.op == '-':
191  res = -res
192  else:
193  raise NotImplementedError("Unsupported OP yet: %s" % expr.op)
194 
195  return res

+ Here is the call graph for this function:

def miasm2.ir.translators.z3_ir.TranslatorZ3.from_ExprSlice (   self,
  expr 
)

Definition at line 133 of file z3_ir.py.

134  def from_ExprSlice(self, expr):
135  res = self.from_expr(expr.arg)
136  res = z3.Extract(expr.stop-1, expr.start, res)
137  return res

+ Here is the call graph for this function:

def miasm2.ir.translators.translator.Translator.register (   cls,
  translator 
)
inherited
Register a translator
@translator: Translator sub-class

Definition at line 14 of file translator.py.

14 
15  def register(cls, translator):
16  """Register a translator
17  @translator: Translator sub-class
18  """
19  cls.available_translators.append(translator)
def miasm2.ir.translators.translator.Translator.to_language (   cls,
  target_lang,
  args,
  kwargs 
)
inherited
Return the corresponding translator instance
@target_lang: str (case insensitive) wanted language
Raise a NotImplementedError in case of unmatched language

Definition at line 21 of file translator.py.

21 
22  def to_language(cls, target_lang, *args, **kwargs):
23  """Return the corresponding translator instance
24  @target_lang: str (case insensitive) wanted language
25  Raise a NotImplementedError in case of unmatched language
26  """
27  target_lang = target_lang.lower()
28  for translator in cls.available_translators:
29  if translator.__LANG__.lower() == target_lang:
30  return translator(*args, **kwargs)
31 
32  raise NotImplementedError("Unknown target language: %s" % target_lang)
tuple translator
Definition: ir2C.py:15

Member Data Documentation

string miasm2.ir.translators.z3_ir.TranslatorZ3.__LANG__ = "z3"
staticprivate

Definition at line 109 of file z3_ir.py.

miasm2.ir.translators.z3_ir.TranslatorZ3._mem
private

Definition at line 118 of file z3_ir.py.

list miasm2.ir.translators.translator.Translator.available_translators = []
staticinherited

Definition at line 9 of file translator.py.

list miasm2.ir.translators.z3_ir.TranslatorZ3.trivial_ops = ["+", "-", "/", "%", "&", "^", "|", "*", "<<"]
static

Definition at line 111 of file z3_ir.py.


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