merge z3 interface and fast backward analysis

amoco/__init__.py

@@ -1,2 +1,4 @@
+# -*- coding: utf-8 -*-
+
 from .config import conf
 from .main import *

amoco/arch/arm/cpu_armv7.py

@@ -1,5 +1,7 @@
+# -*- coding: utf-8 -*-
+
 # This code is part of Amoco
-# Copyright (C) 2006-2014 Axel Tillequin ([email protected]) 
+# Copyright (C) 2006-2014 Axel Tillequin ([email protected])
 # published under GPLv2 license
 
 from amoco.arch.arm.v7.asm import *

amoco/arch/arm/cpu_armv8.py

@@ -1,5 +1,7 @@
+# -*- coding: utf-8 -*-
+
 # This code is part of Amoco
-# Copyright (C) 2006-2014 Axel Tillequin ([email protected]) 
+# Copyright (C) 2006-2014 Axel Tillequin ([email protected])
 # published under GPLv2 license
 
 from amoco.arch.arm.v8.asm64 import *

amoco/arch/arm/v7/asm.py

@@ -1,5 +1,7 @@
+# -*- coding: utf-8 -*-
+
 # This code is part of Amoco
-# Copyright (C) 2006-2011 Axel Tillequin ([email protected]) 
+# Copyright (C) 2006-2011 Axel Tillequin ([email protected])
 # published under GPLv2 license
 
 from .env import *
@@ -32,7 +34,7 @@ def __check_state(i,fmap):
         if address._is_cst:
             raise InstructionError(i)
         else:
-            logger.warning('impossible to check isetstate (ARM/Thumb) until pc is cst')
+            logger.verbose('impossible to check isetstate (ARM/Thumb) until pc is cst')
 
 def __pre(i,fmap):
     fmap[pc] = fmap(pc+i.length)
@@ -49,6 +51,7 @@ def __pre(i,fmap):
     return cond,dest,op1
 
 def __setflags(fmap,cond,cout,result,overflow=None):
+    if cout is None: cout = fmap(C)
     fmap[C] = tst(cond,cout,fmap(C))
     fmap[Z] = tst(cond,(result==0),fmap(Z))
     fmap[N] = tst(cond,(result<0),fmap(N))
@@ -164,13 +167,13 @@ def i_BIC(i,fmap):
         __setflags(fmap,cond,cout,result)
 
 def i_CMN(i,fmap):
-    cond,dest,op1,op2 = __pre(i,fmap)
-    result,cout,overflow = AddWithCarry(fmap(op1),fmap(op2))
+    cond,dest,op1 = __pre(i,fmap)
+    result,cout,overflow = AddWithCarry(fmap(dest),fmap(op1))
     __setflags(fmap,cond,cout,result,overflow)
 
 def i_CMP(i,fmap):
-    cond,dest,op1,op2 = __pre(i,fmap)
-    result,cout,overflow = SubWithBorrow(fmap(op1),fmap(op2))
+    cond,dest,op1 = __pre(i,fmap)
+    result,cout,overflow = SubWithBorrow(fmap(dest),fmap(op1))
     __setflags(fmap,cond,cout,result,overflow)
 
 def i_EOR(i,fmap):
@@ -270,15 +273,15 @@ def i_SUB(i,fmap):
         __setflags(fmap,cond,cout,result,overflow)
 
 def i_TEQ(i,fmap):
-    cond,dest,op1,op2 = __pre(i,fmap)
-    result = fmap(op1 ^ op2)
-    cout = fmap(op2.bit(31))
+    cond,dest,op1 = __pre(i,fmap)
+    result = fmap(dest ^ op1)
+    cout = fmap(op1.bit(31))
     __setflags(fmap,cond,cout,result)
 
 def i_TST(i,fmap):
-    cond,dest,op1,op2 = __pre(i,fmap)
-    result = fmap(op1 & op2)
-    cout = fmap(op2.bit(31))
+    cond,dest,op1 = __pre(i,fmap)
+    result = fmap(dest & op1)
+    cout = fmap(op1.bit(31))
     __setflags(fmap,cond,cout,result)
 
 # shifts (4.4.2)
@@ -864,6 +867,7 @@ def i_PLI(i,fmap):
 def i_SETEND(i,fmap):
     fmap[pc] = fmap(pc+i.length)
     internals['endianstate'] = 1 if i.set_bigend else 0
+    exp.setendian(-1 if i.set_bigend else +1)
 
 # event hint
 def i_SEV(i,fmap):

amoco/arch/arm/v7/env.py

@@ -1,5 +1,7 @@
+# -*- coding: utf-8 -*-
+
 # This code is part of Amoco
-# Copyright (C) 2006-2011 Axel Tillequin ([email protected]) 
+# Copyright (C) 2006-2011 Axel Tillequin ([email protected])
 # published under GPLv2 license
 
 # import expressions:
@@ -11,22 +13,22 @@
 #registers (application level, see B1.3.2) :
 #-------------------------------------------
 
-r0     = reg('r0',32)     # 
-r1     = reg('r1',32)     # 
-r2     = reg('r2',32)     # 
-r3     = reg('r3',32)     # 
-r4     = reg('r4',32)     # 
-r5     = reg('r5',32)     # 
-r6     = reg('r6',32)     # 
-r7     = reg('r7',32)     # 
-r8     = reg('r8',32)     # 
-r9     = reg('r9',32)     # 
-r10    = reg('r10',32)    # 
-r11    = reg('r11',32)    # 
-r12    = reg('r12',32)    # 
-r13    = reg('r13',32)    # 
-r14    = reg('r14',32)    # 
-r15    = reg('r15',32)    # 
+r0     = reg('r0',32)     #
+r1     = reg('r1',32)     #
+r2     = reg('r2',32)     #
+r3     = reg('r3',32)     #
+r4     = reg('r4',32)     #
+r5     = reg('r5',32)     #
+r6     = reg('r6',32)     #
+r7     = reg('r7',32)     #
+r8     = reg('r8',32)     #
+r9     = reg('r9',32)     #
+r10    = reg('r10',32)    #
+r11    = reg('r11',32)    #
+r12    = reg('r12',32)    #
+r13    = reg('r13',32)    #
+r14    = reg('r14',32)    #
+r15    = reg('r15',32)    #
 
 regs = [r0,r1,r2,r3,r4,r5,r6,r7,r8,r9,r10,r11,r12,r13,r14,r15]
 

amoco/arch/arm/v7/formats.py

@@ -1,3 +1,5 @@
+# -*- coding: utf-8 -*-
+
 from .env import *
 from .utils import *
 from amoco.arch.core import Formatter

amoco/arch/arm/v7/spec_armv7.py

@@ -1,5 +1,7 @@
+# -*- coding: utf-8 -*-
+
 # This code is part of Amoco
-# Copyright (C) 2006-2011 Axel Tillequin ([email protected]) 
+# Copyright (C) 2006-2011 Axel Tillequin ([email protected])
 # published under GPLv2 license
 
 # spec_xxx files are providers for instruction objects.

amoco/arch/arm/v7/spec_thumb.py

@@ -1,7 +1,7 @@
-#!/usr/bin/env python
+# -*- coding: utf-8 -*-
 
 # This code is part of Amoco
-# Copyright (C) 2006-2011 Axel Tillequin ([email protected]) 
+# Copyright (C) 2006-2011 Axel Tillequin ([email protected])
 # published under GPLv2 license
 
 # spec_xxx files are providers for instruction objects.
@@ -117,7 +117,7 @@ def A_default(obj,Rm):
   obj.type = type_data_processing
   obj.cond = env.CONDITION_AL
 
-@ispec("16[ 1010 0 Rd(3) imm8(8) ]", mnemonic="ADR")
+@ispec("16[ 1010 0 Rd(3) imm8(8) ]", mnemonic="ADR", add=True)
 def A_adr(obj,Rd,imm8):
   obj.d = env.regs[Rd]
   obj.imm32 = env.cst(imm8<<2,32)

amoco/arch/arm/v7/spec_thumb2.py

@@ -1,5 +1,7 @@
+# -*- coding: utf-8 -*-
+
 # This code is part of Amoco
-# Copyright (C) 2006-2011 Axel Tillequin ([email protected]) 
+# Copyright (C) 2006-2011 Axel Tillequin ([email protected])
 # published under GPLv2 license
 
 # spec_xxx files are providers for instruction objects.
@@ -147,8 +149,8 @@ def A_bits(obj,Rn,imm3,Rd,imm2,msb):
 
 @ispec("32[ 11 J1 0 J2 #imm10L(10) 0 11110 S #imm10H(10) ]", mnemonic="BLX")
 def A_label(obj,S,imm10H,J1,J2,imm10L):
-  I1, I2 = str(~(J1^S)), str(~(J2^S))
-  v = int(S+I1+I2+imm10H+imm10L+'00',2)
+  I1, I2 = str(~(J1^S)&0x1), str(~(J2^S)&0x1)
+  v = int(str(S)+I1+I2+imm10H+imm10L+'00',2)
   obj.imm32 = env.cst(v,25).signextend(32)
   obj.operands = [obj.imm32]
   obj.type = type_control_flow
@@ -564,7 +566,7 @@ def A_reglist(obj,Rt):
   obj.cond = env.CONDITION_AL
 
 @ispec("32[ 0 #M 0 #register_list(13) 11101 00 100 1 0 1101 ]", mnemonic="PUSH")
-def A_reglist(obj,P,M,register_list):
+def A_reglist(obj,M,register_list):
   obj.registers = [env.regs[i] for i,r in enumerate(register_list[::-1]+'0'+M+'0') if r=='1']
   if len(obj.registers)<2: raise InstructionError(obj)
   obj.operands = [obj.registers]

amoco/arch/arm/v7/utils.py

@@ -1,20 +1,23 @@
+# -*- coding: utf-8 -*-
+
 # This code is part of Amoco
-# Copyright (C) 2006-2011 Axel Tillequin ([email protected]) 
+# Copyright (C) 2006-2011 Axel Tillequin ([email protected])
 # published under GPLv2 license
 
 from amoco.cas.expressions import *
 
 def LSL_C(x,shift):
-    assert shift>0
-    carry_out = x.bit(-shift)
+    assert shift>=0
+    carry_out = x.bit(-shift) if shift>0 else None
     return (x<<shift,carry_out)
 
 def LSL(x,shift):
     assert shift>=0
     return x<<shift
 
 def LSR_C(x,shift):
-    assert shift>0
+    assert shift>=0
+    if shift==0: return (x,None)
     carry_out = x.bit(shift-1) if shift<x.size else 0
     return (x>>shift,carry_out)
 
@@ -23,16 +26,17 @@ def LSR(x,shift):
     return x>>shift
 
 def ASR_C(x,shift):
-    assert shift>0
+    assert shift>=0
     n = x.size
     xx = x.signextend(n+shift)
-    return (xx[shift:shift+n-1],xx.bit(shift-1))
+    carry_out = xx.bit(shift-1) if shift>0 else None
+    return (xx[shift:shift+n],carry_out)
 
 def ASR(x,shift):
     assert shift>=0
     n = x.size
     xx = x.signextend(n+shift)
-    return xx[shift:shift+n-1]
+    return xx[shift:shift+n]
 
 def ROR_C(x,shift):
     assert shift != 0

amoco/arch/arm/v8/asm64.py

@@ -1,5 +1,7 @@
+# -*- coding: utf-8 -*-
+
 # This code is part of Amoco
-# Copyright (C) 2013 Axel Tillequin ([email protected]) 
+# Copyright (C) 2013 Axel Tillequin ([email protected])
 # published under GPLv2 license
 
 from amoco.logger import Log

amoco/arch/arm/v8/env64.py

@@ -1,5 +1,7 @@
+# -*- coding: utf-8 -*-
+
 # This code is part of Amoco
-# Copyright (C) 2013 Axel Tillequin ([email protected]) 
+# Copyright (C) 2013 Axel Tillequin ([email protected])
 # published under GPLv2 license
 
 # import expressions:

amoco/arch/arm/v8/formats.py

@@ -1,3 +1,5 @@
+# -*- coding: utf-8 -*-
+
 from .env64 import *
 from .utils import *
 from amoco.arch.core import Formatter

amoco/arch/arm/v8/spec_armv8.py

@@ -1,5 +1,7 @@
+# -*- coding: utf-8 -*-
+
 # This code is part of Amoco
-# Copyright (C) 2013 Axel Tillequin ([email protected]) 
+# Copyright (C) 2013 Axel Tillequin ([email protected])
 # published under GPLv2 license
 
 # spec_xxx files are providers for instruction objects.
@@ -41,7 +43,7 @@ def ExtendReg(r,etype,shift=0):
     return r[0:l].extend(signed,N)<<shift
 
 def System_Reg(*args):
-    # TODO: decode args into system register name (see §D.8). 
+    # TODO: decode args into system register name (see §D.8).
     return reg('sysreg{%s}'%(' '.join(['{:b}'.format(x) for x in args])),64)
 
 def sp2z(x):

amoco/arch/arm/v8/utils.py

@@ -1,5 +1,7 @@
+# -*- coding: utf-8 -*-
+
 # This code is part of Amoco
-# Copyright (C) 2006-2011 Axel Tillequin ([email protected]) 
+# Copyright (C) 2006-2011 Axel Tillequin ([email protected])
 # published under GPLv2 license
 
 from amoco.cas.expressions import *

amoco/arch/core.py

@@ -1,7 +1,7 @@
 #!/usr/bin/env python
 
 # This code is part of Amoco
-# Copyright (C) 2006-2014 Axel Tillequin ([email protected]) 
+# Copyright (C) 2006-2014 Axel Tillequin ([email protected])
 # published under GPLv2 license
 
 from crysp.bits import *
@@ -32,7 +32,6 @@
 }
 
 class icore(object):
-    __slots__ = ['bytes', 'type', 'mnemonic', 'operands']
 
     def __init__(self,istr=''):
         self.bytes    = istr
@@ -182,13 +181,13 @@ def __call__(self,bytestring,**kargs):
 # ispec (parametrable) decorator
 # -----------------------------------------
 # @ispec allows to easily define instruction decoders based on architectures specifications.
-# The 'spec' argument is a human-friendly string that describes how the ispec object will 
+# The 'spec' argument is a human-friendly string that describes how the ispec object will
 # (on request) decode a given bytestring and how it will expose various decoded entities to
-# the decorated function in order to define an instruction instance. 
+# the decorated function in order to define an instruction instance.
 # It uses the following syntax :
-# 
+#
 #   'LEN<[ FORMAT ]' : LEN indicates the bit length corresponding to the FORMAT. Here,
-#                      FORMAT is interpreted as a list of directives ordered 
+#                      FORMAT is interpreted as a list of directives ordered
 #                      from MSB (bit index LEN-1) to LSB (bit index 0). This is the default
 #                      direction if the '<' indicator is missing. LEN%8!=0 is unsupported.
 # or
@@ -199,7 +198,7 @@ def __call__(self,bytestring,**kargs):
 # possibly terminated with an optional '+' char to indicate that the spec is a prefix.
 # In this case, the bytestring prefix matching the ispec format is stacked temporarily
 # until the rest of the bytestring matches a non prefix ispec.
-# 
+#
 # The directives composing the FORMAT string are used to associate symbols to bits
 # located at dedicated offsets within the bitstring to be decoded. A directive has the
 # following syntax:
@@ -223,7 +222,7 @@ def __call__(self,bytestring,**kargs):
 #    location: is an optional string matching the following expressions
 #      '( len )'    : indicates that the value is decoded from the next len bits starting
 #                     from the current position of the directive within the FORMAT string.
-#      '(*)'        : indicates a 'variable length directive' for which the value is decoded 
+#      '(*)'        : indicates a 'variable length directive' for which the value is decoded
 #                     from the current position with all remaining bits in the FORMAT.
 #                     If the FORMAT LEN is also variable then all remaining bits from the
 #                     instruction buffer input string are used.
@@ -234,7 +233,7 @@ def __call__(self,bytestring,**kargs):
 #
 # Example:
 #
-# @ispec(32[ .cond(4) 101 1 imm24(24) ]", mnemonic="BL", _flag=True) 
+# @ispec(32[ .cond(4) 101 1 imm24(24) ]", mnemonic="BL", _flag=True)
 # def f(obj,imm24,_flag):
 #     [...]
 #
@@ -246,9 +245,9 @@ def __call__(self,bytestring,**kargs):
 #  => will decode 4 bits at position [28,29,30,31] and provide this value as an integer
 #     in 'obj.cond' instruction instance attribute.
 #  => will decode 24 bits at positions 23..0 and provide this value as an integer as
-#     argument 'imm24' of the decorated function f. 
+#     argument 'imm24' of the decorated function f.
 #  => will set obj.mnemonic to 'BL' and pass argument _flag=True to f.
-#  => will call f(obj,...) 
+#  => will call f(obj,...)
 #  => will return obj
 
 # additional arguments to ispec decorator **must** be provided with symbol=value form and
@@ -257,6 +256,7 @@ def __call__(self,bytestring,**kargs):
 # with value 'BL' when the function is called.
 # -----------------------------------------
 class ispec(object):
+    __slots__ = ['format','iattr','fargs','ast','fix','mask','pfx','size','hook']
 
     def __init__(self,format,**kargs):
         self.format = format

amoco/arch/gas.py

@@ -1,5 +1,7 @@
+# -*- coding: utf-8 -*-
+
 # This code is part of Amoco
-# Copyright (C) 2013 Axel Tillequin ([email protected]) 
+# Copyright (C) 2013 Axel Tillequin ([email protected])
 # published under GPLv2 license
 
 try: