Lots of fixs, features and improvements

[Bindings]      New ast attribute into the SymExpression class (Based on #94)
[Bindings]      New class SmtAstAbstractNode (Based on #94)
[Bindings]      New getFullExpression(node) function (Based on #94)
[Bindings]      New smt2lib string function (Based on #94)
[Bindings]      Remove the display syntax function
[Bindings]      Remove the expression attribute from the SymExpression class (Based on #94)
[Bindings]      Remove the getBacktrackedSymExpr function (Based on #94 and #95)
[Bindings]      Remove the saveTrace feature
[Bindings]      Remove the simplify syntax function
[Bindings]      Update the Sx and Zx functions takes the sizeExt as first argument
[Bindings]      Update the create{Reg,Sym,Expr}ToSymVar() functions take a varSize as bits granularity (#125)
[Bindings]      Update the extract function takes now only one convention
[Core]          Replace the string manipulation to an AST for all SMT expressions (#94)
[Semantics]     Modification of the PF expression (#124)
[SymEngine]     Mofification of the SymbolicExpression class (Based on #94)
[SymEngine]     Reduce the time of the SMT reconstruction (#95)
[SymExpression] Remove the dst attribute (Based on #94)
[SymExpression] Remove the source attribute (Based on #94)

Author: JonathanSalwan

.build_number

@@ -1 +1 @@
-628
+633

examples/callback_after.py

@@ -152,7 +152,7 @@ def my_callback_after(instruction):
     print '%#x: %s' %(instruction.address, instruction.assembly)
 
     for se in instruction.symbolicExpressions:
-        print '\t -> %s %s' %(se.expression, (('; ' + se.comment) if se.comment is not None else ''))
+        print '\t -> #%d = %s %s' %(se.id, se.ast, (('; ' + se.comment) if se.comment is not None else ''))
 
     print
 

examples/callback_before.py

@@ -22,7 +22,7 @@
 # TID (0) 0x400597 mov ecx, eax
 # TID (0) 0x400599 mov rdx, qword ptr [rip+0x200aa0]
 # TID (0) 0x4005a0 mov eax, dword ptr [rbp-0x4]
-# TID (0) 0x4005a3 cdqe 
+# TID (0) 0x4005a3 cdqe
 # TID (0) 0x4005a5 add rax, rdx
 # TID (0) 0x4005a8 movzx eax, byte ptr [rax]
 # TID (0) 0x4005ab movsx eax, al

examples/callback_signals.py

@@ -58,7 +58,7 @@ def signals(threadId, sig):
     for reg, data in regs.items():
         value = data['concreteValue']
         seid  = data['symbolicExpr']
-        print '%s:\t%#016x\t%s' %(getRegName(reg), value, (getSymExpr(seid).expression if seid != IDREF.MISC.UNSET else 'UNSET'))
+        print '%s:\t%#016x\t%s' %(getRegName(reg), value, (getSymExpr(seid).ast if seid != IDREF.MISC.UNSET else 'UNSET'))
     return
 
 

examples/crackme_hash_collision.py

@@ -51,45 +51,29 @@ def cafter(instruction):
     # RAX points on the user password
     if instruction.address == 0x400572:
         rsiId = getRegSymbolicID(IDREF.REG.RSI)
-        convertExprToSymVar(rsiId, 8)
+        convertExprToSymVar(rsiId, 64)
 
     # mov eax,DWORD PTR [rbp-0x4]
     # RAX must be equal to 0xad6d to win
     if instruction.address == 0x4005c5:
         print '[+] Please wait, computing in progress...'
         raxId = getRegSymbolicID(IDREF.REG.RAX)
-        raxExpr = getBacktrackedSymExpr(raxId)
-        expr = str()
+        raxExpr = getFullExpression(getSymExpr(raxId).ast)
 
         # We want printable characters
-        # (assert (bvsgt SymVar_0 96)
-        # (assert (bvslt SymVar_0 123)
-        expr += smt2lib.smtAssert(smt2lib.bvugt('SymVar_0', smt2lib.bv(96, 64)))
-        expr += smt2lib.smtAssert(smt2lib.bvult('SymVar_0', smt2lib.bv(123, 64)))
-
-        # (assert (bvsgt SymVar_1 96)
-        # (assert (bvslt SymVar_1 123)
-        expr += smt2lib.smtAssert(smt2lib.bvugt('SymVar_1', smt2lib.bv(96, 64)))
-        expr += smt2lib.smtAssert(smt2lib.bvult('SymVar_1', smt2lib.bv(123, 64)))
-
-        # (assert (bvsgt SymVar_2 96)
-        # (assert (bvslt SymVar_2 123)
-        expr += smt2lib.smtAssert(smt2lib.bvugt('SymVar_2', smt2lib.bv(96, 64)))
-        expr += smt2lib.smtAssert(smt2lib.bvult('SymVar_2', smt2lib.bv(123, 64)))
-
-        # (assert (bvsgt SymVar_3 96)
-        # (assert (bvslt SymVar_3 123)
-        expr += smt2lib.smtAssert(smt2lib.bvugt('SymVar_3', smt2lib.bv(96, 64)))
-        expr += smt2lib.smtAssert(smt2lib.bvult('SymVar_3', smt2lib.bv(123, 64)))
-
-        # (assert (bvsgt SymVar_4 96)
-        # (assert (bvslt SymVar_4 123)
-        expr += smt2lib.smtAssert(smt2lib.bvugt('SymVar_4', smt2lib.bv(96, 64)))
-        expr += smt2lib.smtAssert(smt2lib.bvult('SymVar_4', smt2lib.bv(123, 64)))
-
-        # We want the collision
-        # (assert (= rax 0xad6d)
-        expr += smt2lib.smtAssert(smt2lib.equal(raxExpr, smt2lib.bv(0xad6d, 64)))
+        expr = smt2lib.compound([
+                 smt2lib.smtAssert(smt2lib.bvugt(smt2lib.string('SymVar_0'), smt2lib.bv(96,  64))),
+                 smt2lib.smtAssert(smt2lib.bvult(smt2lib.string('SymVar_0'), smt2lib.bv(123, 64))),
+                 smt2lib.smtAssert(smt2lib.bvugt(smt2lib.string('SymVar_1'), smt2lib.bv(96,  64))),
+                 smt2lib.smtAssert(smt2lib.bvult(smt2lib.string('SymVar_1'), smt2lib.bv(123, 64))),
+                 smt2lib.smtAssert(smt2lib.bvugt(smt2lib.string('SymVar_2'), smt2lib.bv(96,  64))),
+                 smt2lib.smtAssert(smt2lib.bvult(smt2lib.string('SymVar_2'), smt2lib.bv(123, 64))),
+                 smt2lib.smtAssert(smt2lib.bvugt(smt2lib.string('SymVar_3'), smt2lib.bv(96,  64))),
+                 smt2lib.smtAssert(smt2lib.bvult(smt2lib.string('SymVar_3'), smt2lib.bv(123, 64))),
+                 smt2lib.smtAssert(smt2lib.bvugt(smt2lib.string('SymVar_4'), smt2lib.bv(96,  64))),
+                 smt2lib.smtAssert(smt2lib.bvult(smt2lib.string('SymVar_4'), smt2lib.bv(123, 64))),
+                 smt2lib.smtAssert(smt2lib.equal(raxExpr, smt2lib.bv(0xad6d, 64)))  # collision: (assert (= rax 0xad6d)
+               ])
 
         # Get max 20 different models
         models = getModels(expr, 20)

examples/get_model.py

@@ -45,12 +45,12 @@ def cafter(instruction):
 
     # 0x40058b: movzx eax, byte ptr [rax]
     if instruction.address == 0x40058b:
-        convertRegToSymVar(IDREF.REG.RAX, 4)
+        convertRegToSymVar(IDREF.REG.RAX, 32)
 
     # 0x4005ae: cmp ecx, eax
     if instruction.address == 0x4005ae:
         zfId    = getRegSymbolicID(IDREF.FLAG.ZF)
-        zfExpr  = getBacktrackedSymExpr(zfId)
+        zfExpr  = getFullExpression(getSymExpr(zfId).ast)
         expr    = smt2lib.smtAssert(smt2lib.equal(zfExpr, smt2lib.bvtrue())) # (assert (= zf True))
         models  = getModel(expr)
         global password

examples/inject_model_with_snapshot.py

@@ -19,9 +19,9 @@ def cafter(instruction):
     print '%#x: %s' %(instruction.address, instruction.assembly)
     for se in instruction.symbolicExpressions:
         if se.isTainted == True:
-            print '\t -> %s%s%s' %(GREEN, se.expression, ENDC)
+            print '\t -> %s%s%s' %(GREEN, se.ast, ENDC)
         else:
-            print '\t -> %s' %(se.expression)
+            print '\t -> %s' %(se.ast)
     print