from triton import *
import sys

GREEN = "\033[92m"
RED   = "\033[91m"
ENDC  = "\033[0m"

# Output
#
# $ ./triton ./examples/semanticsTesting.py ./samples/ir_test_suite/ir
# [...]
# [OK] 0x400645: idiv rcx
# [OK] 0x400648: mov rax, 0x1
# [OK] 0x40064f: mov rcx, 0x2
# [OK] 0x400656: mov rdx, 0x3
# [OK] 0x40065d: mov rsi, 0x4
# [OK] 0x400664: imul sil
# [KO] 0x400667: imul cx (2 error)
#      Register       : cf
#      Symbolic Value : 0000000000000001
#      Concrete Value : 0000000000000000
#      Expression     : (ite (= ((_ extract 15 0) #348) ((_ extract 15 0) (_ bv2 64))) (_ bv0 1) (_ bv1 1))
#      Register       : of
#      Symbolic Value : 0000000000000001
#      Concrete Value : 0000000000000000
#      Expression     : (ite (= ((_ extract 15 0) #348) ((_ extract 15 0) (_ bv2 64))) (_ bv0 1) (_ bv1 1))


def sbefore(instruction):
    concretizeAllMem()
    concretizeAllReg()
    return


def cafter(instruction):

    if instruction.getAddress() < 0x600000: # To bypass external lib

        bad  = list()
        regs = getRegs()

        for reg, data in regs.items():

            cvalue = data['concreteValue']
            seid   = data['symbolicExpr']

            if seid == IDREF.MISC.UNSET:
                continue

            expr   = getFullExpression(getSymExpr(seid).getAst())
            svalue = evaluateAST(expr)

            if cvalue != svalue:
                bad.append({
                    'reg': getRegName(reg),
                    'svalue': svalue,
                    'cvalue': cvalue,
                    'expr': getSymExpr(seid).getAst()
                })

        if not bad:
            print "[%sOK%s] %#x: %s" %(GREEN, ENDC, instruction.getAddress(), instruction.getDisassembly())
        else:
            print "[%sKO%s] %#x: %s (%s%d error%s)" %(RED, ENDC, instruction.getAddress(), instruction.getDisassembly(), RED, len(bad), ENDC)
            for w in bad:
                print "     Register       : %s" %(w['reg'])
                print "     Symbolic Value : %016x" %(w['svalue'])
                print "     Concrete Value : %016x" %(w['cvalue'])
                print "     Expression     : %s" %(w['expr'])
    return


if __name__ == '__main__':

    # Start the symbolic analysis from the 'check' function
    startAnalysisFromSymbol('main')

    addCallback(cafter, IDREF.CALLBACK.AFTER)
    addCallback(sbefore, IDREF.CALLBACK.BEFORE_SYMPROC)

    # Run the instrumentation - Never returns
    runProgram()


@@ -931,82 +931,8 @@
 ):%0A%0A
-    if instruction.getAddress() %3C 0x600000: # To bypass external lib%0A%0A    
     
@@ -949,20 +949,16 @@
 t()%0A    
- 
-   
 regs = g
@@ -967,20 +967,16 @@
 Regs()%0A%0A
-    
     for 
@@ -1011,20 +1011,16 @@
         
-   
- 
 cvalue =
@@ -1042,20 +1042,16 @@
 Value'%5D%0A
-    
         
@@ -1089,20 +1089,16 @@
         
- 
-   
 if seid 
@@ -1130,20 +1130,16 @@
         
-  
-  
 continue
@@ -1140,20 +1140,16 @@
 ntinue%0A%0A
-    
         
@@ -1210,20 +1210,16 @@
         
-    
 svalue =
@@ -1246,20 +1246,16 @@
         
- 
-   
 if cvalu
@@ -1279,20 +1279,16 @@
         
-    
 bad.appe
@@ -1292,20 +1292,16 @@
 ppend(%7B%0A
-    
         
@@ -1348,20 +1348,16 @@
         
-    
 'svalue'
@@ -1362,28 +1362,24 @@
 e': svalue,%0A
-    
             
@@ -1416,20 +1416,16 @@
         
-  
-  
 'expr': 
@@ -1466,20 +1466,12 @@
     
-    %7D)%0A%0A    
+%7D)%0A%0A
     
@@ -1478,28 +1478,24 @@
 if not bad:%0A
-    
         prin
@@ -1582,28 +1582,24 @@
 assembly())%0A
-    
     else:%0A  
@@ -1600,28 +1600,24 @@
 se:%0A        
-   
- 
 print %22%5B%25sKO
@@ -1742,20 +1742,16 @@
         
-    
 for w in
@@ -1752,28 +1752,24 @@
 r w in bad:%0A
-    
             
@@ -1817,36 +1817,32 @@
 '%5D)%0A            
-  
-  
 print %22     Symb
@@ -1868,36 +1868,32 @@
  %25(w%5B'svalue'%5D)%0A
-    
             prin
@@ -1931,36 +1931,32 @@
  %25(w%5B'cvalue'%5D)%0A
-    
             prin

Apply testing on all code