signature:
def CMOVNO ( cpu , dest , src ) :
    """Conditional move - Not overflow .
 Tests the status flags in the EFLAGS register and moves the source operand
 ( second operand ) to the destination operand ( first operand ) if the given
 test condition is true .
 : param cpu : current CPU .
 : param dest : destination operand .
 : param src : source operand ."""

implementation: dest . write ( Operators . ITEBV ( dest . size , cpu . OF == False , src . read ( ) , dest . read ( ) ) )


signature:
def CMOVS ( cpu , dest , src ) :
    """Conditional move - Sign ( negative ) .
 Tests the status flags in the EFLAGS register and moves the source operand
 ( second operand ) to the destination operand ( first operand ) if the given
 test condition is true .
 : param cpu : current CPU .
 : param dest : destination operand .
 : param src : source operand ."""

implementation: dest . write ( Operators . ITEBV ( dest . size , cpu . SF , src . read ( ) , dest . read ( ) ) )


signature:
def CMOVNS ( cpu , dest , src ) :
    """Conditional move - Not sign ( non - negative ) .
 Tests the status flags in the EFLAGS register and moves the source operand
 ( second operand ) to the destination operand ( first operand ) if the given
 test condition is true .
 : param cpu : current CPU .
 : param dest : destination operand .
 : param src : source operand ."""

implementation: dest . write ( Operators . ITEBV ( dest . size , cpu . SF == False , src . read ( ) , dest . read ( ) ) )


signature:
def LAHF ( cpu ) :
    """Loads status flags into AH register .
 Moves the low byte of the EFLAGS register ( which includes status flags
 SF , ZF , AF , PF , and CF ) to the AH register . Reserved bits 1 , 3 , and 5
 of the EFLAGS register are set in the AH register : :
 AH = EFLAGS ( SF : ZF : 0 : AF : 0 : PF : 1 : CF ) ;
 : param cpu : current CPU .
 : param dest : destination operand .
 : param src : source operand ."""

implementation:
used_regs = ( cpu . SF , cpu . ZF , cpu . AF , cpu . PF , cpu . CF )
is_expression = any ( issymbolic ( x ) for x in used_regs )
def make_flag ( val , offset ) :
    if is_expression :
        return Operators . ITEBV ( 8 , val , BitVecConstant ( 8 , 1 << offset ) , BitVecConstant ( 8 , 0 ) )
    else :
        return val << offset
cpu . AH = ( make_flag ( cpu . SF , 7 ) | make_flag ( cpu . ZF , 6 ) | make_flag ( 0 , 5 ) | make_flag ( cpu . AF , 4 ) | make_flag ( 0 , 3 ) | make_flag ( cpu . PF , 2 ) | make_flag ( 1 , 1 ) | make_flag ( cpu . CF , 0 ) )


signature:
def LEA ( cpu , dest , src ) :
    """Loads effective address .
 Computes the effective address of the second operand ( the source operand ) and stores it in the first operand
 ( destination operand ) . The source operand is a memory address ( offset part ) specified with one of the processors
 addressing modes ; the destination operand is a general - purpose register . The address - size and operand - size
 attributes affect the action performed by this instruction . The operand - size
 attribute of the instruction is determined by the chosen register ; the address - size attribute is determined by the
 attribute of the code segment .
 : param cpu : current CPU .
 : param dest : destination operand .
 : param src : source operand ."""

implementation: dest . write ( Operators . EXTRACT ( src . address ( ) , 0 , dest . size ) )


signature:
def MOVBE ( cpu , dest , src ) :
    """Moves data after swapping bytes .
 Performs a byte swap operation on the data copied from the second operand ( source operand ) and store the result
 in the first operand ( destination operand ) . The source operand can be a general - purpose register , or memory location ; the destination register can be a general - purpose register , or a memory location ; however , both operands can
 not be registers , and only one operand can be a memory location . Both operands must be the same size , which can
 be a word , a doubleword or quadword .
 The MOVBE instruction is provided for swapping the bytes on a read from memory or on a write to memory ; thus
 providing support for converting little - endian values to big - endian format and vice versa .
 In 64 - bit mode , the instruction ' s default operation size is 32 bits . Use of the REX . R prefix permits access to additional registers ( R8 - R15 ) . Use of the REX . W prefix promotes operation to 64 bits : :
 TEMP = SRC
 IF ( OperandSize = 16)
 THEN
 DEST [ 7:0 ] = TEMP [ 15:8 ] ;
 DEST [ 15:8 ] = TEMP [ 7:0 ] ;
 ELSE IF ( OperandSize = 32)
 DEST [ 7:0 ] = TEMP [ 31:24 ] ;
 DEST [ 15:8 ] = TEMP [ 23:16 ] ;
 DEST [ 23:16 ] = TEMP [ 15:8 ] ;
 DEST [ 31:23 ] = TEMP [ 7:0 ] ;
 ELSE IF ( OperandSize = 64)
 DEST [ 7:0 ] = TEMP [ 63:56 ] ;
 DEST [ 15:8 ] = TEMP [ 55:48 ] ;
 DEST [ 23:16 ] = TEMP [ 47:40 ] ;
 DEST [ 31:24 ] = TEMP [ 39:32 ] ;
 DEST [ 39:32 ] = TEMP [ 31:24 ] ;
 DEST [ 47:40 ] = TEMP [ 23:16 ] ;
 DEST [ 55:48 ] = TEMP [ 15:8 ] ;
 DEST [ 63:56 ] = TEMP [ 7:0 ] ;
 FI ;
 : param cpu : current CPU .
 : param dest : destination operand .
 : param src : source operand ."""

implementation:
size = dest . size
arg0 = dest . read ( )
temp = 0
for pos in range ( 0 , size , 8 ) :
    temp = ( temp << 8 ) | ( arg0 & 0xff )
    arg0 = arg0 >> 8
dest . write ( arg0 )


signature:
def SAHF ( cpu ) :
    """Stores AH into flags .
 Loads the SF , ZF , AF , PF , and CF flags of the EFLAGS register with values
 from the corresponding bits in the AH register ( bits 7 , 6 , 4 , 2 , and 0,
 respectively ) . Bits 1 , 3 , and 5 of register AH are ignored ; the corresponding
 reserved bits ( 1 , 3 , and 5 ) in the EFLAGS register remain as shown below : :
 EFLAGS ( SF : ZF : 0 : AF : 0 : PF : 1 : CF ) = AH ;
 : param cpu : current CPU .
 : param dest : destination operand .
 : param src : source operand ."""

implementation:
eflags_size = 32
val = cpu . AH & 0xD5 | 0x02
cpu . EFLAGS = Operators . ZEXTEND ( val , eflags_size )


signature:
def SETA ( cpu , dest ) :
    """Sets byte if above .
 Sets the destination operand to 0 or 1 depending on the settings of the status flags ( CF , SF , OF , ZF , and PF , 1 , 0 ) in the
 EFLAGS register . The destination operand points to a byte register or a byte in memory . The condition code suffix
 ( cc , 1 , 0 ) indicates the condition being tested for : :
 IF condition
 THEN
 DEST = 1;
 ELSE
 DEST = 0;
 FI ;
 : param cpu : current CPU .
 : param dest : destination operand ."""

implementation: dest . write ( Operators . ITEBV ( dest . size , Operators . OR ( cpu . CF , cpu . ZF ) == False , 1 , 0 ) )


signature:
def SETB ( cpu , dest ) :
    """Sets byte if below .
 : param cpu : current CPU .
 : param dest : destination operand ."""

implementation: dest . write ( Operators . ITEBV ( dest . size , cpu . CF , 1 , 0 ) )


signature:
def SETBE ( cpu , dest ) :
    """Sets byte if below or equal .
 : param cpu : current CPU .
 : param dest : destination operand ."""

implementation: dest . write ( Operators . ITEBV ( dest . size , Operators . OR ( cpu . CF , cpu . ZF ) , 1 , 0 ) )


signature:
def SETC ( cpu , dest ) :
    """Sets if carry .
 : param cpu : current CPU .
 : param dest : destination operand ."""


signature:
def SETE ( cpu , dest ) :
    """Sets byte if equal .
 : param cpu : current CPU .
 : param dest : destination operand ."""

implementation: dest . write ( Operators . ITEBV ( dest . size , cpu . ZF , 1 , 0 ) )


signature:
def SETGE ( cpu , dest ) :
    """Sets byte if greater or equal .
 : param cpu : current CPU .
 : param dest : destination operand ."""

implementation: dest . write ( Operators . ITEBV ( dest . size , cpu . SF == cpu . OF , 1 , 0 ) )


signature:
def SETNAE ( cpu , dest ) :
    """Sets byte if not above or equal .
 : param cpu : current CPU .
 : param dest : destination operand ."""


signature:
def SETNB ( cpu , dest ) :
    """Sets byte if not below .
 : param cpu : current CPU .
 : param dest : destination operand ."""

implementation: dest . write ( Operators . ITEBV ( dest . size , cpu . CF == False , 1 , 0 ) )


signature:
def SETNBE ( cpu , dest ) :
    """Sets byte if not below or equal .
 : param cpu : current CPU .
 : param dest : destination operand ."""

implementation: dest . write ( Operators . ITEBV ( dest . size , Operators . AND ( cpu . CF == False , cpu . ZF == False ) , 1 , 0 ) )


signature:
def SETNG ( cpu , dest ) :
    """Sets byte if not greater .
 : param cpu : current CPU .
 : param dest : destination operand ."""

implementation: dest . write ( Operators . ITEBV ( dest . size , Operators . OR ( cpu . ZF , cpu . SF != cpu . OF ) , 1 , 0 ) )


signature:
def SETNLE ( cpu , dest ) :
    """Sets byte if not less or equal .
 : param cpu : current CPU .
 : param dest : destination operand ."""

implementation: dest . write ( Operators . ITEBV ( dest . size , Operators . AND ( cpu . ZF == False , cpu . SF == cpu . OF ) , 1 , 0 ) )


signature:
def SETNO ( cpu , dest ) :
    """Sets byte if not overflow .
 : param cpu : current CPU .
 : param dest : destination operand ."""

implementation: dest . write ( Operators . ITEBV ( dest . size , cpu . OF == False , 1 , 0 ) )


signature:
def SETNS ( cpu , dest ) :
    """Sets byte if not sign .
 : param cpu : current CPU .
 : param dest : destination operand ."""

implementation: dest . write ( Operators . ITEBV ( dest . size , cpu . SF == False , 1 , 0 ) )


signature:
def SETNZ ( cpu , dest ) :
    """Sets byte if not zero .
 : param cpu : current CPU .
 : param dest : destination operand ."""

implementation: dest . write ( Operators . ITEBV ( dest . size , cpu . ZF == False , 1 , 0 ) )


signature:
def SETO ( cpu , dest ) :
    """Sets byte if overflow .
 : param cpu : current CPU .
 : param dest : destination operand ."""

implementation: dest . write ( Operators . ITEBV ( dest . size , cpu . OF , 1 , 0 ) )


signature:
def SETP ( cpu , dest ) :
    """Sets byte if parity .
 : param cpu : current CPU .
 : param dest : destination operand ."""

implementation: dest . write ( Operators . ITEBV ( dest . size , cpu . PF , 1 , 0 ) )


signature:
def SETPE ( cpu , dest ) :
    """Sets byte if parity even .
 : param cpu : current CPU .
 : param dest : destination operand ."""


signature:
def SETPO ( cpu , dest ) :
    """Sets byte if parity odd .
 : param cpu : current CPU .
 : param dest : destination operand ."""

implementation: dest . write ( Operators . ITEBV ( dest . size , cpu . PF == False , 1 , 0 ) )


signature:
def SETS ( cpu , dest ) :
    """Sets byte if sign .
 : param cpu : current CPU .
 : param dest : destination operand ."""

implementation: dest . write ( Operators . ITEBV ( dest . size , cpu . SF , 1 , 0 ) )


signature:
def SETZ ( cpu , dest ) :
    """Sets byte if zero .
 : param cpu : current CPU .
 : param dest : destination operand ."""


signature:
def XCHG ( cpu , dest , src ) :
    """Exchanges register / memory with register .
 Exchanges the contents of the destination ( first ) and source ( second )
 operands . The operands can be two general - purpose registers or a register
 and a memory location . If a memory operand is referenced , the processor ' s
 locking protocol is automatically implemented for the duration of the
 exchange operation , regardless of the presence or absence of the LOCK
 prefix or of the value of the IOPL .
 This instruction is useful for implementing semaphores or similar data
 structures for process synchronization .
 The XCHG instruction can also be used instead of the BSWAP instruction
 for 16 - bit operands : :
 TEMP = DEST
 DEST = SRC
 SRC = TEMP
 : param cpu : current CPU .
 : param dest : destination operand .
 : param src : source operand ."""

implementation:
temp = dest . read ( )
dest . write ( src . read ( ) )
src . write ( temp )


signature:
def LEAVE ( cpu ) :
    """High level procedure exit .
 Releases the stack frame set up by an earlier ENTER instruction . The
 LEAVE instruction copies the frame pointer ( in the EBP register ) into
 the stack pointer register ( ESP ) , which releases the stack space allocated
 to the stack frame . The old frame pointer ( the frame pointer for the calling
 procedure that was saved by the ENTER instruction ) is then popped from
 the stack into the EBP register , restoring the calling procedure ' s stack
 frame .
 A RET instruction is commonly executed following a LEAVE instruction
 to return program control to the calling procedure : :
 IF Stackaddress _ bit _ size = 32
 THEN
 ESP = EBP ;
 ELSE ( * Stackaddress _ bit _ size = 16 * )
 SP = BP ;
 FI ;
 IF OperandSize = 32
 THEN
 EBP = Pop ( ) ;
 ELSE ( * OperandSize = 16 * )
 BP = Pop ( ) ;
 FI ;
 : param cpu : current CPU ."""

implementation:
cpu . STACK = cpu . FRAME
cpu . FRAME = cpu . pop ( cpu . address_bit_size )


signature:
def PUSH ( cpu , src ) :
    """Pushes a value onto the stack .
 Decrements the stack pointer and then stores the source operand on the top of the stack .
 : param cpu : current CPU .
 : param src : source operand ."""

implementation:
# http : / / stackoverflow . com / questions / 11291151 / how - push - imm - encodes
size = src . size
v = src . read ( )
if size != 64 and size != cpu . address_bit_size // 2 :
    v = Operators . SEXTEND ( v , size , cpu . address_bit_size )
    size = cpu . address_bit_size
cpu . push ( v , size )


signature:
def POPF ( cpu ) :
    """Pops stack into EFLAGS register .
 : param cpu : current CPU ."""


signature:
def POPFQ ( cpu ) :
    """Pops stack into EFLAGS register .
 : param cpu : current CPU ."""


signature:
def INT ( cpu , op0 ) :
    """Calls to interrupt procedure .
 The INT n instruction generates a call to the interrupt or exception handler specified
 with the destination operand . The INT n instruction is the general mnemonic for executing
 a software - generated call to an interrupt handler . The INTO instruction is a special
 mnemonic for calling overflow exception ( # OF ) , interrupt vector number 4 . The overflow
 interrupt checks the OF flag in the EFLAGS register and calls the overflow interrupt handler
 if the OF flag is set to 1.
 : param cpu : current CPU .
 : param op0 : destination operand ."""

implementation:
if op0 . read ( ) != 0x80 :
    logger . warning ( "Unsupported interrupt" )
raise Interruption ( op0 . read ( ) )


signature:
def CALL ( cpu , op0 ) :
    """Procedure call .
 Saves procedure linking information on the stack and branches to the called procedure specified using the target
 operand . The target operand specifies the address of the first instruction in the called procedure . The operand can
 be an immediate value , a general - purpose register , or a memory location .
 : param cpu : current CPU .
 : param op0 : target operand ."""

implementation:
# TODO FIX 64Bit FIX segment
proc = op0 . read ( )
cpu . push ( cpu . PC , cpu . address_bit_size )
cpu . PC = proc


signature:
def RET ( cpu , * operands ) :
    """Returns from procedure .
 Transfers program control to a return address located on the top of
 the stack . The address is usually placed on the stack by a CALL instruction ,
 and the return is made to the instruction that follows the CALL instruction .
 The optional source operand specifies the number of stack bytes to be
 released after the return address is popped ; the default is none .
 : param cpu : current CPU .
 : param operands : variable operands list ."""

implementation:
# TODO FIX 64Bit FIX segment
N = 0
if len ( operands ) > 0 :
    N = operands [ 0 ] . read ( )
cpu . PC = cpu . pop ( cpu . address_bit_size )
cpu . STACK += N


signature:
def JA ( cpu , target ) :
    """Jumps short if above .
 : param cpu : current CPU .
 : param target : destination operand ."""

implementation: cpu . PC = Operators . ITEBV ( cpu . address_bit_size , Operators . AND ( cpu . CF == False , cpu . ZF == False ) , target . read ( ) , cpu . PC )


signature:
def JB ( cpu , target ) :
    """Jumps short if below .
 : param cpu : current CPU .
 : param target : destination operand ."""

implementation: cpu . PC = Operators . ITEBV ( cpu . address_bit_size , cpu . CF == True , target . read ( ) , cpu . PC )


signature:
def JBE ( cpu , target ) :
    """Jumps short if below or equal .
 : param cpu : current CPU .
 : param target : destination operand ."""

implementation: cpu . PC = Operators . ITEBV ( cpu . address_bit_size , Operators . OR ( cpu . CF , cpu . ZF ) , target . read ( ) , cpu . PC )


signature:
def JC ( cpu , target ) :
    """Jumps short if carry .
 : param cpu : current CPU .
 : param target : destination operand ."""

implementation: cpu . PC = Operators . ITEBV ( cpu . address_bit_size , cpu . CF , target . read ( ) , cpu . PC )


signature:
def JCXZ ( cpu , target ) :
    """Jumps short if CX register is 0.
 : param cpu : current CPU .
 : param target : destination operand ."""

implementation: cpu . PC = Operators . ITEBV ( cpu . address_bit_size , cpu . CX == 0 , target . read ( ) , cpu . PC )


signature:
def JECXZ ( cpu , target ) :
    """Jumps short if ECX register is 0.
 : param cpu : current CPU .
 : param target : destination operand ."""

implementation: cpu . PC = Operators . ITEBV ( cpu . address_bit_size , cpu . ECX == 0 , target . read ( ) , cpu . PC )


signature:
def JRCXZ ( cpu , target ) :
    """Jumps short if RCX register is 0.
 : param cpu : current CPU .
 : param target : destination operand ."""

implementation: cpu . PC = Operators . ITEBV ( cpu . address_bit_size , cpu . RCX == 0 , target . read ( ) , cpu . PC )


signature:
def JG ( cpu , target ) :
    """Jumps short if greater .
 : param cpu : current CPU .
 : param target : destination operand ."""

implementation: cpu . PC = Operators . ITEBV ( cpu . address_bit_size , Operators . AND ( cpu . ZF == False , cpu . SF == cpu . OF ) , target . read ( ) , cpu . PC )


signature:
def JGE ( cpu , target ) :
    """Jumps short if greater or equal .
 : param cpu : current CPU .
 : param target : destination operand ."""

implementation: cpu . PC = Operators . ITEBV ( cpu . address_bit_size , ( cpu . SF == cpu . OF ) , target . read ( ) , cpu . PC )


signature:
def JNB ( cpu , target ) :
    """Jumps short if not below .
 : param cpu : current CPU .
 : param target : destination operand ."""

implementation: cpu . PC = Operators . ITEBV ( cpu . address_bit_size , cpu . CF == False , target . read ( ) , cpu . PC )


signature:
def JNE ( cpu , target ) :
    """Jumps short if not equal .
 : param cpu : current CPU .
 : param target : destination operand ."""

implementation: cpu . PC = Operators . ITEBV ( cpu . address_bit_size , False == cpu . ZF , target . read ( ) , cpu . PC )


signature:
def JNG ( cpu , target ) :
    """Jumps short if not greater .
 : param cpu : current CPU .
 : param target : destination operand ."""

implementation: cpu . PC = Operators . ITEBV ( cpu . address_bit_size , Operators . OR ( cpu . ZF , cpu . SF != cpu . OF ) , target . read ( ) , cpu . PC )


signature:
def JNO ( cpu , target ) :
    """Jumps short if not overflow .
 : param cpu : current CPU .
 : param target : destination operand ."""

implementation: cpu . PC = Operators . ITEBV ( cpu . address_bit_size , False == cpu . OF , target . read ( ) , cpu . PC )


signature:
def JNP ( cpu , target ) :
    """Jumps short if not parity .
 : param cpu : current CPU .
 : param target : destination operand ."""

implementation: cpu . PC = Operators . ITEBV ( cpu . address_bit_size , False == cpu . PF , target . read ( ) , cpu . PC )


signature:
def JNS ( cpu , target ) :
    """Jumps short if not sign .
 : param cpu : current CPU .
 : param target : destination operand ."""

implementation: cpu . PC = Operators . ITEBV ( cpu . address_bit_size , False == cpu . SF , target . read ( ) , cpu . PC )


signature:
def JO ( cpu , target ) :
    """Jumps short if overflow .
 : param cpu : current CPU .
 : param target : destination operand ."""

implementation: cpu . PC = Operators . ITEBV ( cpu . address_bit_size , cpu . OF , target . read ( ) , cpu . PC )


signature:
def JP ( cpu , target ) :
    """Jumps short if parity .
 : param cpu : current CPU .
 : param target : destination operand ."""

implementation: cpu . PC = Operators . ITEBV ( cpu . address_bit_size , cpu . PF , target . read ( ) , cpu . PC )


signature:
def JS ( cpu , target ) :
    """Jumps short if sign .
 : param cpu : current CPU .
 : param target : destination operand ."""

implementation: cpu . PC = Operators . ITEBV ( cpu . address_bit_size , cpu . SF , target . read ( ) , cpu . PC )


signature:
def JZ ( cpu , target ) :
    """Jumps short if zero .
 : param cpu : current CPU .
 : param target : destination operand ."""

implementation: cpu . PC = Operators . ITEBV ( cpu . address_bit_size , cpu . ZF , target . read ( ) , cpu . PC )


signature:
def LJMP ( cpu , cs_selector , target ) :
    """We are just going to ignore the CS selector for now ."""

implementation:
logger . info ( "LJMP: Jumping to: %r:%r" , cs_selector . read ( ) , target . read ( ) )
cpu . CS = cs_selector . read ( )
cpu . PC = target . read ( )


signature:
def LOOP ( cpu , dest ) :
    """Loops according to ECX counter .
 Performs a loop operation using the ECX or CX register as a counter .
 Each time the LOOP instruction is executed , the count register is decremented ,
 then checked for 0 . If the count is 0 , the loop is terminated and program
 execution continues with the instruction following the LOOP instruction .
 If the count is not zero , a near jump is performed to the destination
 ( target ) operand , which is presumably the instruction at the beginning
 of the loop . If the address - size attribute is 32 bits , the ECX register
 is used as the count register ; otherwise the CX register is used : :
 IF address _ bit _ size = 32
 THEN
 Count is ECX ;
 ELSE ( * address _ bit _ size = 16 * )
 Count is CX ;
 FI ;
 Count = Count - 1;
 IF ( Count 0 ) = 1
 THEN
 EIP = EIP + SignExtend ( DEST ) ;
 IF OperandSize = 16
 THEN
 EIP = EIP AND 0000FFFFH ;
 FI ;
 ELSE
 Terminate loop and continue program execution at EIP ;
 FI ;
 : param cpu : current CPU .
 : param dest : destination operand ."""

implementation:
counter_name = { 16 : 'CX' , 32 : 'ECX' , 64 : 'RCX' } [ cpu . address_bit_size ]
counter = cpu . write_register ( counter_name , cpu . read_register ( counter_name ) - 1 )
cpu . PC = Operators . ITEBV ( cpu . address_bit_size , counter == 0 , ( cpu . PC + dest . read ( ) ) & ( ( 1 << dest . size ) - 1 ) , cpu . PC + cpu . instruction . size )


signature:
def LOOPNZ ( cpu , target ) :
    """Loops if ECX counter is nonzero .
 : param cpu : current CPU .
 : param target : destination operand ."""

implementation:
counter_name = { 16 : 'CX' , 32 : 'ECX' , 64 : 'RCX' } [ cpu . address_bit_size ]
counter = cpu . write_register ( counter_name , cpu . read_register ( counter_name ) - 1 )
cpu . PC = Operators . ITEBV ( cpu . address_bit_size , counter != 0 , ( cpu . PC + target . read ( ) ) & ( ( 1 << target . size ) - 1 ) , cpu . PC + cpu . instruction . size )


signature:
def RCL ( cpu , dest , src ) :
    """Rotates through carry left .
 Shifts ( rotates ) the bits of the first operand ( destination operand ) the number of bit positions specified in the
 second operand ( count operand ) and stores the result in the destination operand . The destination operand can be
 a register or a memory location ; the count operand is an unsigned integer that can be an immediate or a value in
 the CL register . In legacy and compatibility mode , the processor restricts the count to a number between 0 and 31
 by masking all the bits in the count operand except the 5 least - significant bits .
 The RCL instruction shifts the CF flag into the least - significant bit and shifts the most - significant bit into the CF flag .
 : param cpu : current CPU .
 : param dest : destination operand .
 : param src : count operand ."""

implementation:
OperandSize = dest . size
count = src . read ( )
countMask = { 8 : 0x1f , 16 : 0x1f , 32 : 0x1f , 64 : 0x3f } [ OperandSize ]
tempCount = Operators . ZEXTEND ( ( count & countMask ) % ( src . size + 1 ) , OperandSize )
value = dest . read ( )
if isinstance ( tempCount , int ) and tempCount == 0 : # this is a no - op
    new_val = value
    dest . write ( new_val )
else :
    carry = Operators . ITEBV ( OperandSize , cpu . CF , 1 , 0 )
    right = value >> ( OperandSize - tempCount )
    new_val = ( value << tempCount ) | ( carry << ( tempCount - 1 ) ) | ( right >> 1 )
    dest . write ( new_val )
    def sf ( v , size ) :
        return ( v & ( 1 << ( size - 1 ) ) ) != 0
    cpu . CF = sf ( value << ( tempCount - 1 ) , OperandSize )
    cpu . OF = Operators . ITE ( tempCount == 1 , sf ( new_val , OperandSize ) != cpu . CF , cpu . OF )


signature:
def RCR ( cpu , dest , src ) :
    """Rotates through carry right ( RCR ) .
 Shifts ( rotates ) the bits of the first operand ( destination operand ) the number of bit positions specified in the
 second operand ( count operand ) and stores the result in the destination operand . The destination operand can be
 a register or a memory location ; the count operand is an unsigned integer that can be an immediate or a value in
 the CL register . In legacy and compatibility mode , the processor restricts the count to a number between 0 and 31
 by masking all the bits in the count operand except the 5 least - significant bits .
 Rotate through carry right ( RCR ) instructions shift all the bits toward less significant bit positions , except
 for the least - significant bit , which is rotated to the most - significant bit location . The RCR instruction shifts the
 CF flag into the most - significant bit and shifts the least - significant bit into the CF flag .
 : param cpu : current CPU .
 : param dest : destination operand .
 : param src : count operand ."""

implementation:
OperandSize = dest . size
count = src . read ( )
countMask = { 8 : 0x1f , 16 : 0x1f , 32 : 0x1f , 64 : 0x3f } [ OperandSize ]
tempCount = Operators . ZEXTEND ( ( count & countMask ) % ( src . size + 1 ) , OperandSize )
value = dest . read ( )
if isinstance ( tempCount , int ) and tempCount == 0 : # this is a no - op
    new_val = value
    dest . write ( new_val )
else :
    carry = Operators . ITEBV ( OperandSize , cpu . CF , 1 , 0 )
    left = value >> ( tempCount - 1 )
    right = value << ( OperandSize - tempCount )
    new_val = ( left >> 1 ) | ( carry << ( OperandSize - tempCount ) ) | ( right << 1 )
    dest . write ( new_val )
    cpu . CF = Operators . ITE ( tempCount != 0 , ( left & 1 ) == 1 , cpu . CF )
    # for RCR these are calculated before rotation starts
    s_MSB = ( ( new_val >> ( OperandSize - 1 ) ) & 0x1 ) == 1
    s_MSB2 = ( ( new_val >> ( OperandSize - 2 ) ) & 0x1 ) == 1
    cpu . OF = Operators . ITE ( tempCount == 1 , s_MSB ^ s_MSB2 , cpu . OF )


signature:
def ROL ( cpu , dest , src ) :
    """Rotates left ( ROL ) .
 Shifts ( rotates ) the bits of the first operand ( destination operand ) the number of bit positions specified in the
 second operand ( count operand ) and stores the result in the destination operand . The destination operand can be
 a register or a memory location ; the count operand is an unsigned integer that can be an immediate or a value in
 the CL register . In legacy and compatibility mode , the processor restricts the count to a number between 0 and 31
 by masking all the bits in the count operand except the 5 least - significant bits .
 The rotate left shift all the bits toward more - significant bit positions , except for the most - significant bit , which
 is rotated to the least - significant bit location .
 : param cpu : current CPU .
 : param dest : destination operand .
 : param src : count operand ."""

implementation:
OperandSize = dest . size
count = src . read ( )
countMask = { 8 : 0x1f , 16 : 0x1f , 32 : 0x1f , 64 : 0x3f } [ OperandSize ]
tempCount = Operators . ZEXTEND ( ( count & countMask ) % ( OperandSize ) , OperandSize )
value = dest . read ( )
newValue = ( value << tempCount ) | ( value >> ( OperandSize - tempCount ) )
dest . write ( newValue )
cpu . CF = Operators . ITE ( tempCount != 0 , ( newValue & 1 ) == 1 , cpu . CF )
s_MSB = ( ( newValue >> ( OperandSize - 1 ) ) & 0x1 ) == 1
cpu . OF = Operators . ITE ( tempCount == 1 , s_MSB ^ cpu . CF , cpu . OF )


signature:
def SAL ( cpu , dest , src ) :
    """The shift arithmetic left .
 Shifts the bits in the first operand ( destination operand ) to the left or right by the number of bits specified in the
 second operand ( count operand ) . Bits shifted beyond the destination operand boundary are first shifted into the CF
 flag , then discarded . At the end of the shift operation , the CF flag contains the last bit shifted out of the destination
 operand .
 : param cpu : current CPU .
 : param dest : destination operand .
 : param src : count operand ."""

implementation:
OperandSize = dest . size
count = src . read ( )
countMask = { 8 : 0x1f , 16 : 0x1f , 32 : 0x1f , 64 : 0x3f } [ OperandSize ]
tempCount = Operators . ZEXTEND ( count & countMask , dest . size )
tempDest = value = dest . read ( )
res = dest . write ( Operators . ITEBV ( dest . size , tempCount == 0 , tempDest , value << tempCount ) )
# Should not modify flags if tempcount = = 0
MASK = ( 1 << OperandSize ) - 1
SIGN_MASK = 1 << ( OperandSize - 1 )
cpu . CF = Operators . OR ( Operators . AND ( tempCount == 0 , cpu . CF ) , Operators . AND ( tempCount != 0 , ( tempDest & ( 1 << ( OperandSize - tempCount ) ) != 0 ) ) )
# OF is only set iff count = = 1 , and set to XOR ( CF , MSB ( res ) )
# OF is only defined for count = = 1 , but in practice ( unit tests from real cpu ) its calculated for count ! = 0
cpu . OF = Operators . ITE ( tempCount != 0 , ( cpu . CF ) ^ ( ( ( res >> ( OperandSize - 1 ) ) & 0x1 ) == 1 ) , cpu . OF )
cpu . SF = Operators . OR ( Operators . AND ( tempCount == 0 , cpu . SF ) , Operators . AND ( tempCount != 0 , ( res & SIGN_MASK ) != 0 ) )
cpu . ZF = Operators . OR ( Operators . AND ( tempCount == 0 , cpu . ZF ) , Operators . AND ( tempCount != 0 , res == 0 ) )
cpu . PF = Operators . OR ( Operators . AND ( tempCount == 0 , cpu . PF ) , Operators . AND ( tempCount != 0 , cpu . _calculate_parity_flag ( res ) ) )


signature:
def SAR ( cpu , dest , src ) :
    """Shift arithmetic right .
 The shift arithmetic right ( SAR ) and shift logical right ( SHR ) instructions shift the bits of the destination operand to
 the right ( toward less significant bit locations ) . For each shift count , the least significant bit of the destination
 operand is shifted into the CF flag , and the most significant bit is either set or cleared depending on the instruction
 type . The SHR instruction clears the most significant bit . the SAR instruction sets or clears the most significant bit
 to correspond to the sign ( most significant bit ) of the original value in the destination operand . In effect , the SAR
 instruction fills the empty bit position ' s shifted value with the sign of the unshifted value
 : param cpu : current CPU .
 : param dest : destination operand .
 : param src : source operand ."""

implementation:
OperandSize = dest . size
countMask = { 8 : 0x1f , 16 : 0x1f , 32 : 0x1f , 64 : 0x3f } [ OperandSize ]
count = src . read ( ) & countMask
value = dest . read ( )
res = Operators . SAR ( OperandSize , value , Operators . ZEXTEND ( count , OperandSize ) )
dest . write ( res )
SIGN_MASK = ( 1 << ( OperandSize - 1 ) )
# We can ' t use this one as the ' true ' expression gets eagerly calculated even on count = = 0 + cpu . CF = Operators . ITE ( count ! = 0 , ( ( value > > Operators . ZEXTEND ( count - 1 , OperandSize ) ) & 1 ) ! = 0 , cpu . CF )
# cpu . CF = Operators . ITE ( count ! = 0 , ( ( value > > Operators . ZEXTEND ( count - 1 , OperandSize ) ) & 1 ) ! = 0 , cpu . CF )
if issymbolic ( count ) : # We can ' t use this one as the EXTRACT op needs the offset arguments to be concrete
# cpu . CF = Operators . ITE ( count ! = 0 , Operands . EXTRACT ( value , count - 1,1 ) ! = 0 , cpu . CF )
    cpu . CF = Operators . ITE ( Operators . AND ( count != 0 , count <= OperandSize ) , ( ( value >> Operators . ZEXTEND ( count - 1 , OperandSize ) ) & 1 ) != 0 , cpu . CF )
else :
    if count != 0 :
        if count > OperandSize :
            count = OperandSize
        cpu . CF = Operators . EXTRACT ( value , count - 1 , 1 ) != 0
# on count = = 0 AF is unaffected , for count > 0 , AF is undefined .
# in either case , do not touch AF
cpu . ZF = Operators . ITE ( count != 0 , res == 0 , cpu . ZF )
cpu . SF = Operators . ITE ( count != 0 , ( res & SIGN_MASK ) != 0 , cpu . SF )
cpu . OF = Operators . ITE ( count == 1 , False , cpu . OF )
cpu . PF = Operators . ITE ( count != 0 , cpu . _calculate_parity_flag ( res ) , cpu . PF )


signature:
def SHR ( cpu , dest , src ) :
    """Shift logical right .
 The shift arithmetic right ( SAR ) and shift logical right ( SHR )
 instructions shift the bits of the destination operand to the right
 ( toward less significant bit locations ) . For each shift count , the
 least significant bit of the destination operand is shifted into the CF
 flag , and the most significant bit is either set or cleared depending
 on the instruction type . The SHR instruction clears the most
 significant bit .
 : param cpu : current CPU .
 : param dest : destination operand .
 : param src : count operand ."""

implementation:
OperandSize = dest . size
count = Operators . ZEXTEND ( src . read ( ) & ( OperandSize - 1 ) , OperandSize )
value = dest . read ( )
res = dest . write ( value >> count )
# UNSIGNED Operators . UDIV2 ! ! TODO Check
MASK = ( 1 << OperandSize ) - 1
SIGN_MASK = 1 << ( OperandSize - 1 )
if issymbolic ( count ) :
    cpu . CF = Operators . ITE ( count != 0 , ( ( value >> Operators . ZEXTEND ( count - 1 , OperandSize ) ) & 1 ) != 0 , cpu . CF )
else :
    if count != 0 :
        cpu . CF = Operators . EXTRACT ( value , count - 1 , 1 ) != 0
cpu . ZF = Operators . ITE ( count != 0 , res == 0 , cpu . ZF )
cpu . SF = Operators . ITE ( count != 0 , ( res & SIGN_MASK ) != 0 , cpu . SF )
# OF is only defined for count = = 1 , but in practice ( unit tests from real cpu ) it ' s calculated for count ! = 0
cpu . OF = Operators . ITE ( count != 0 , ( ( value >> ( OperandSize - 1 ) ) & 0x1 ) == 1 , cpu . OF )
cpu . PF = Operators . ITE ( count != 0 , cpu . _calculate_parity_flag ( res ) , cpu . PF )


signature:
def SHLD ( cpu , dest , src , count ) :
    """Double precision shift right .
 Shifts the first operand ( destination operand ) to the left the number of bits specified by the third operand
 ( count operand ) . The second operand ( source operand ) provides bits to shift in from the right ( starting with
 the least significant bit of the destination operand ) .
 : param cpu : current CPU .
 : param dest : destination operand .
 : param src : source operand .
 : param count : count operand"""

implementation:
OperandSize = dest . size
tempCount = Operators . ZEXTEND ( count . read ( ) , OperandSize ) & ( OperandSize - 1 )
arg0 = dest . read ( )
arg1 = src . read ( )
MASK = ( ( 1 << OperandSize ) - 1 )
t0 = ( arg0 << tempCount )
t1 = arg1 >> ( OperandSize - tempCount )
res = Operators . ITEBV ( OperandSize , tempCount == 0 , arg0 , t0 | t1 )
res = res & MASK
dest . write ( res )
if isinstance ( tempCount , int ) and tempCount == 0 :
    pass
else :
    SIGN_MASK = 1 << ( OperandSize - 1 )
    lastbit = 0 != ( ( arg0 << ( tempCount - 1 ) ) & SIGN_MASK )
    cpu . _set_shiftd_flags ( OperandSize , arg0 , res , lastbit , tempCount )


signature:
def _getMemoryBit ( cpu , bitbase , bitoffset ) :
    """Calculate address and bit offset given a base address and a bit offset
 relative to that address ( in the form of asm operands )"""

implementation:
assert bitbase . type == 'memory'
assert bitbase . size >= bitoffset . size
addr = bitbase . address ( )
offt = Operators . SEXTEND ( bitoffset . read ( ) , bitoffset . size , bitbase . size )
offt_is_neg = offt >= ( 1 << ( bitbase . size - 1 ) )
offt_in_bytes = offt // 8
bitpos = offt % 8
new_addr = addr + Operators . ITEBV ( bitbase . size , offt_is_neg , - offt_in_bytes , offt_in_bytes )
return ( new_addr , bitpos )


signature:
def BSF ( cpu , dest , src ) :
    """Bit scan forward .
 Searches the source operand ( second operand ) for the least significant
 set bit ( 1 bit ) . If a least significant 1 bit is found , its bit index
 is stored in the destination operand ( first operand ) . The source operand
 can be a register or a memory location ; the destination operand is a register .
 The bit index is an unsigned offset from bit 0 of the source operand .
 If the contents source operand are 0 , the contents of the destination
 operand is undefined : :
 IF SRC = 0
 THEN
 ZF = 1;
 DEST is undefined ;
 ELSE
 ZF = 0;
 temp = 0;
 WHILE Bit ( SRC , temp ) = 0
 DO
 temp = temp + 1;
 DEST = temp ;
 OD ;
 FI ;
 : param cpu : current CPU .
 : param dest : destination operand .
 : param src : source operand ."""

implementation:
value = src . read ( )
flag = Operators . EXTRACT ( value , 0 , 1 ) == 1
res = 0
for pos in range ( 1 , src . size ) :
    res = Operators . ITEBV ( dest . size , flag , res , pos )
    flag = Operators . OR ( flag , Operators . EXTRACT ( value , pos , 1 ) == 1 )
cpu . ZF = value == 0
dest . write ( Operators . ITEBV ( dest . size , cpu . ZF , dest . read ( ) , res ) )


signature:
def BSR ( cpu , dest , src ) :
    """Bit scan reverse .
 Searches the source operand ( second operand ) for the most significant
 set bit ( 1 bit ) . If a most significant 1 bit is found , its bit index is
 stored in the destination operand ( first operand ) . The source operand
 can be a register or a memory location ; the destination operand is a register .
 The bit index is an unsigned offset from bit 0 of the source operand .
 If the contents source operand are 0 , the contents of the destination
 operand is undefined : :
 IF SRC = 0
 THEN
 ZF = 1;
 DEST is undefined ;
 ELSE
 ZF = 0;
 temp = OperandSize - 1;
 WHILE Bit ( SRC , temp ) = 0
 DO
 temp = temp - 1;
 DEST = temp ;
 OD ;
 FI ;
 : param cpu : current CPU .
 : param dest : destination operand .
 : param src : source operand ."""

implementation:
value = src . read ( )
flag = Operators . EXTRACT ( value , src . size - 1 , 1 ) == 1
res = 0
for pos in reversed ( range ( 0 , src . size ) ) :
    res = Operators . ITEBV ( dest . size , flag , res , pos )
    flag = Operators . OR ( flag , ( Operators . EXTRACT ( value , pos , 1 ) == 1 ) )
cpu . PF = cpu . _calculate_parity_flag ( res )
cpu . ZF = value == 0
dest . write ( Operators . ITEBV ( dest . size , cpu . ZF , dest . read ( ) , res ) )


signature:
def BT ( cpu , dest , src ) :
    """Bit Test .
 Selects the bit in a bit string ( specified with the first operand , called the bit base ) at the
 bit - position designated by the bit offset ( specified by the second operand ) and stores the value
 of the bit in the CF flag . The bit base operand can be a register or a memory location ; the bit
 offset operand can be a register or an immediate value :
 - If the bit base operand specifies a register , the instruction takes the modulo 16 , 32 , or 64
 of the bit offset operand ( modulo size depends on the mode and register size ; 64 - bit operands
 are available only in 64 - bit mode ) .
 - If the bit base operand specifies a memory location , the operand represents the address of the
 byte in memory that contains the bit base ( bit 0 of the specified byte ) of the bit string . The
 range of the bit position that can be referenced by the offset operand depends on the operand size .
 : param cpu : current CPU .
 : param dest : bit base .
 : param src : bit offset ."""

implementation:
if dest . type == 'register' :
    cpu . CF = ( ( dest . read ( ) >> ( src . read ( ) % dest . size ) ) & 1 ) != 0
elif dest . type == 'memory' :
    addr , pos = cpu . _getMemoryBit ( dest , src )
    base , size , ty = cpu . get_descriptor ( cpu . DS )
    value = cpu . read_int ( addr + base , 8 )
    cpu . CF = Operators . EXTRACT ( value , pos , 1 ) == 1
else :
    raise NotImplementedError ( f"Unknown operand for BT: {dest.type}" )


signature:
def BTC ( cpu , dest , src ) :
    """Bit test and complement .
 Selects the bit in a bit string ( specified with the first operand , called
 the bit base ) at the bit - position designated by the bit offset operand
 ( second operand ) , stores the value of the bit in the CF flag , and complements
 the selected bit in the bit string .
 : param cpu : current CPU .
 : param dest : bit base operand .
 : param src : bit offset operand ."""

implementation:
if dest . type == 'register' :
    value = dest . read ( )
    pos = src . read ( ) % dest . size
    cpu . CF = value & ( 1 << pos ) == 1 << pos
    dest . write ( value ^ ( 1 << pos ) )
elif dest . type == 'memory' :
    addr , pos = cpu . _getMemoryBit ( dest , src )
    base , size , ty = cpu . get_descriptor ( cpu . DS )
    addr += base
    value = cpu . read_int ( addr , 8 )
    cpu . CF = value & ( 1 << pos ) == 1 << pos
    value = value ^ ( 1 << pos )
    cpu . write_int ( addr , value , 8 )
else :
    raise NotImplementedError ( f"Unknown operand for BTC: {dest.type}" )


signature:
def POPCNT ( cpu , dest , src ) :
    """This instruction calculates of number of bits set to 1 in the second
 operand ( source ) and returns the count in the first operand ( a destination
 register ) .
 Count = 0;
 For ( i = 0 ; i < OperandSize ; i + + ) {
 IF ( SRC [ i ] = 1 ) / / i ' th bit
 THEN Count + + ;
 FI ;
 DEST = Count ;
 Flags Affected
 OF , SF , ZF , AF , CF , PF are all cleared .
 ZF is set if SRC = 0 , otherwise ZF is cleared"""

implementation:
count = 0
source = src . read ( )
for i in range ( src . size ) :
    count += Operators . ITEBV ( dest . size , ( source >> i ) & 1 == 1 , 1 , 0 )
dest . write ( count )
# Flags
cpu . OF = False
cpu . SF = False
cpu . AF = False
cpu . CF = False
cpu . PF = False
cpu . ZF = source == 0


signature:
def CMPS ( cpu , dest , src ) :
    """Compares string operands .
 Compares the byte , word , double word or quad specified with the first source
 operand with the byte , word , double or quad word specified with the second
 source operand and sets the status flags in the EFLAGS register according
 to the results . Both the source operands are located in memory : :
 temp = SRC1 - SRC2;
 SetStatusFlags ( temp ) ;
 IF ( byte comparison )
 THEN IF DF = 0
 THEN
 ( E ) SI = ( E ) SI + 1;
 ( E ) DI = ( E ) DI + 1;
 ELSE
 ( E ) SI = ( E ) SI - 1;
 ( E ) DI = ( E ) DI - 1;
 FI ;
 ELSE IF ( word comparison )
 THEN IF DF = 0
 ( E ) SI = ( E ) SI + 2;
 ( E ) DI = ( E ) DI + 2;
 ELSE
 ( E ) SI = ( E ) SI - 2;
 ( E ) DI = ( E ) DI - 2;
 FI ;
 ELSE ( * doubleword comparison * )
 THEN IF DF = 0
 ( E ) SI = ( E ) SI + 4;
 ( E ) DI = ( E ) DI + 4;
 ELSE
 ( E ) SI = ( E ) SI - 4;
 ( E ) DI = ( E ) DI - 4;
 FI ;
 FI ;
 : param cpu : current CPU .
 : param dest : first source operand .
 : param src : second source operand ."""

implementation:
src_reg = { 8 : 'SI' , 32 : 'ESI' , 64 : 'RSI' } [ cpu . address_bit_size ]
dest_reg = { 8 : 'DI' , 32 : 'EDI' , 64 : 'RDI' } [ cpu . address_bit_size ]
base , _ , ty = cpu . get_descriptor ( cpu . DS )
src_addr = cpu . read_register ( src_reg ) + base
dest_addr = cpu . read_register ( dest_reg ) + base
size = dest . size
# Compare
arg1 = cpu . read_int ( dest_addr , size )
arg0 = cpu . read_int ( src_addr , size )
res = ( arg0 - arg1 ) & ( ( 1 << size ) - 1 )
cpu . _calculate_CMP_flags ( size , res , arg0 , arg1 )
# Advance EDI / ESI pointers
increment = Operators . ITEBV ( cpu . address_bit_size , cpu . DF , - size // 8 , size // 8 )
cpu . write_register ( src_reg , cpu . read_register ( src_reg ) + increment )
cpu . write_register ( dest_reg , cpu . read_register ( dest_reg ) + increment )


signature:
def LODS ( cpu , dest , src ) :
    """Loads string .
 Loads a byte , word , or doubleword from the source operand into the AL , AX , or EAX register , respectively . The
 source operand is a memory location , the address of which is read from the DS : ESI or the DS : SI registers
 ( depending on the address - size attribute of the instruction , 32 or 16 , respectively ) . The DS segment may be over -
 ridden with a segment override prefix .
 After the byte , word , or doubleword is transferred from the memory location into the AL , AX , or EAX register , the
 ( E ) SI register is incremented or decremented automatically according to the setting of the DF flag in the EFLAGS
 register . ( If the DF flag is 0 , the ( E ) SI register is incremented ; if the DF flag is 1 , the ESI register is decremented . )
 The ( E ) SI register is incremented or decremented by 1 for byte operations , by 2 for word operations , or by 4 for
 doubleword operations .
 : param cpu : current CPU .
 : param dest : source operand ."""

implementation:
src_reg = { 8 : 'SI' , 32 : 'ESI' , 64 : 'RSI' } [ cpu . address_bit_size ]
base , _ , ty = cpu . get_descriptor ( cpu . DS )
src_addr = cpu . read_register ( src_reg ) + base
size = dest . size
arg0 = cpu . read_int ( src_addr , size )
dest . write ( arg0 )
increment = Operators . ITEBV ( cpu . address_bit_size , cpu . DF , - size // 8 , size // 8 )
cpu . write_register ( src_reg , cpu . read_register ( src_reg ) + increment )


signature:
def MOVS ( cpu , dest , src ) :
    """Moves data from string to string .
 Moves the byte , word , or doubleword specified with the second operand ( source operand ) to the location specified
 with the first operand ( destination operand ) . Both the source and destination operands are located in memory . The
 address of the source operand is read from the DS : ESI or the DS : SI registers ( depending on the address - size
 attribute of the instruction , 32 or 16 , respectively ) . The address of the destination operand is read from the ES : EDI
 or the ES : DI registers ( again depending on the address - size attribute of the instruction ) . The DS segment may be
 overridden with a segment override prefix , but the ES segment cannot be overridden .
 : param cpu : current CPU .
 : param dest : destination operand .
 : param src : source operand ."""

implementation:
base , size , ty = cpu . get_descriptor ( cpu . DS )
src_addr = src . address ( ) + base
dest_addr = dest . address ( ) + base
src_reg = src . mem . base
dest_reg = dest . mem . base
size = dest . size
# Copy the data
dest . write ( src . read ( ) )
# Advance EDI / ESI pointers
increment = Operators . ITEBV ( cpu . address_bit_size , cpu . DF , - size // 8 , size // 8 )
cpu . write_register ( src_reg , cpu . read_register ( src_reg ) + increment )
cpu . write_register ( dest_reg , cpu . read_register ( dest_reg ) + increment )


signature:
def SCAS ( cpu , dest , src ) :
    """Scans String .
 Compares the byte , word , or double word specified with the memory operand
 with the value in the AL , AX , EAX , or RAX register , and sets the status flags
 according to the results . The memory operand address is read from either
 the ES : RDI , ES : EDI or the ES : DI registers ( depending on the address - size
 attribute of the instruction , 32 or 16 , respectively ) : :
 IF ( byte comparison )
 THEN
 temp = AL - SRC ;
 SetStatusFlags ( temp ) ;
 THEN IF DF = 0
 THEN ( E ) DI = ( E ) DI + 1;
 ELSE ( E ) DI = ( E ) DI - 1;
 FI ;
 ELSE IF ( word comparison )
 THEN
 temp = AX - SRC ;
 SetStatusFlags ( temp )
 THEN IF DF = 0
 THEN ( E ) DI = ( E ) DI + 2;
 ELSE ( E ) DI = ( E ) DI - 2;
 FI ;
 ELSE ( * doubleword comparison * )
 temp = EAX - SRC ;
 SetStatusFlags ( temp )
 THEN IF DF = 0
 THEN
 ( E ) DI = ( E ) DI + 4;
 ELSE
 ( E ) DI = ( E ) DI - 4;
 FI ;
 FI ;
 FI ;
 : param cpu : current CPU .
 : param dest : destination operand .
 : param src : source operand ."""

implementation:
dest_reg = dest . reg
mem_reg = src . mem . base
# , src . type , src . read ( )
size = dest . size
arg0 = dest . read ( )
arg1 = src . read ( )
res = arg0 - arg1
cpu . _calculate_CMP_flags ( size , res , arg0 , arg1 )
increment = Operators . ITEBV ( cpu . address_bit_size , cpu . DF , - size // 8 , size // 8 )
cpu . write_register ( mem_reg , cpu . read_register ( mem_reg ) + increment )


signature:
def STOS ( cpu , dest , src ) :
    """Stores String .
 Stores a byte , word , or doubleword from the AL , AX , or EAX register ,
 respectively , into the destination operand . The destination operand is
 a memory location , the address of which is read from either the ES : EDI
 or the ES : DI registers ( depending on the address - size attribute of the
 instruction , 32 or 16 , respectively ) . The ES segment cannot be overridden
 with a segment override prefix .
 : param cpu : current CPU .
 : param dest : destination operand .
 : param src : source operand ."""

implementation:
size = src . size
dest . write ( src . read ( ) )
dest_reg = dest . mem . base
increment = Operators . ITEBV ( { 'RDI' : 64 , 'EDI' : 32 , 'DI' : 16 } [ dest_reg ] , cpu . DF , - size // 8 , size // 8 )
cpu . write_register ( dest_reg , cpu . read_register ( dest_reg ) + increment )


signature:
def ANDN ( cpu , dest , src1 , src2 ) :
    """Performs a bitwise logical AND of inverted second operand ( the first source operand )
 with the third operand ( the second source operand ) . The result is stored in the first
 operand ( destination operand ) .
 DEST < - ( NOT SRC1 ) bitwiseAND SRC2;
 SF < - DEST [ OperandSize - 1 ] ;
 ZF < - ( DEST = 0 ) ;
 Flags Affected
 SF and ZF are updated based on result . OF and CF flags are cleared . AF and PF flags are undefined ."""

implementation:
value = ~ src1 . read ( ) & src2 . read ( )
dest . write ( value )
cpu . ZF = value == 0
cpu . SF = ( value & ( 1 << dest . size ) ) != 0
cpu . OF = False
cpu . CF = False


signature:
def SHLX ( cpu , dest , src , count ) :
    """The shift arithmetic left .
 Shifts the bits in the first operand ( destination operand ) to the left or right by the number of bits specified in the
 second operand ( count operand ) . Bits shifted beyond the destination operand boundary are first shifted into the CF
 flag , then discarded . At the end of the shift operation , the CF flag contains the last bit shifted out of the destination
 operand .
 : param cpu : current CPU .
 : param dest : destination operand .
 : param src : count operand ."""

implementation:
OperandSize = dest . size
count = count . read ( )
countMask = { 8 : 0x1f , 16 : 0x1f , 32 : 0x1f , 64 : 0x3f } [ OperandSize ]
tempCount = Operators . ZEXTEND ( count & countMask , dest . size )
tempDest = value = src . read ( )
res = dest . write ( Operators . ITEBV ( dest . size , tempCount == 0 , tempDest , value << tempCount ) )


signature:
def SARX ( cpu , dest , src , count ) :
    """The shift arithmetic right .
 : param cpu : current CPU .
 : param dest : destination operand .
 : param src : count operand ."""

implementation:
OperandSize = dest . size
count = count . read ( )
countMask = { 8 : 0x1f , 16 : 0x1f , 32 : 0x1f , 64 : 0x3f } [ OperandSize ]
tempCount = count & countMask
tempDest = value = src . read ( )
sign = value & ( 1 << ( OperandSize - 1 ) )
while tempCount != 0 :
    cpu . CF = ( value & 0x1 ) != 0
    # LSB
    value = ( value >> 1 ) | sign
    tempCount = tempCount - 1
res = dest . write ( value )


signature:
def PMINUB ( cpu , dest , src ) :
    """PMINUB : returns minimum of packed unsigned byte integers in the dest operand
 see PMAXUB"""

implementation:
dest_value = dest . read ( )
src_value = src . read ( )
result = 0
for pos in range ( 0 , dest . size , 8 ) :
    itema = ( dest_value >> pos ) & 0xff
    itemb = ( src_value >> pos ) & 0xff
    result |= Operators . ITEBV ( dest . size , itema < itemb , itema , itemb ) << pos
dest . write ( result )


signature:
def PXOR ( cpu , dest , src ) :
    """Logical exclusive OR .
 Performs a bitwise logical exclusive - OR ( XOR ) operation on the quadword
 source ( second ) and destination ( first ) operands and stores the result
 in the destination operand location . The source operand can be an MMX ( TM )
 technology register or a quadword memory location ; the destination operand
 must be an MMX register . Each bit of the result is 1 if the corresponding
 bits of the two operands are different ; each bit is 0 if the corresponding
 bits of the operands are the same : :
 DEST = DEST XOR SRC ;
 : param cpu : current CPU .
 : param dest : destination operand .
 : param src : quadword source operand ."""

implementation: res = dest . write ( dest . read ( ) ^ src . read ( ) )


signature:
def _PUNPCKL ( cpu , dest , src , item_size ) :
    """Generic PUNPCKL"""

implementation:
assert dest . size == src . size
size = dest . size
dest_value = dest . read ( )
src_value = src . read ( )
mask = ( 1 << item_size ) - 1
res = 0
count = 0
for pos in range ( 0 , size // item_size ) :
    if count >= size :
        break
    item0 = Operators . ZEXTEND ( ( dest_value >> ( pos * item_size ) ) & mask , size )
    item1 = Operators . ZEXTEND ( ( src_value >> ( pos * item_size ) ) & mask , size )
    res |= item0 << count
    count += item_size
    res |= item1 << count
    count += item_size
dest . write ( res )


signature:
def PSHUFW ( cpu , op0 , op1 , op3 ) :
    """Packed shuffle words .
 Copies doublewords from source operand ( second operand ) and inserts them in the destination operand
 ( first operand ) at locations selected with the order operand ( third operand ) .
 : param cpu : current CPU .
 : param op0 : destination operand .
 : param op1 : source operand .
 : param op3 : order operand ."""


signature:
def PSHUFD ( cpu , op0 , op1 , op3 ) :
    """Packed shuffle doublewords .
 Copies doublewords from source operand ( second operand ) and inserts them in the destination operand
 ( first operand ) at locations selected with the order operand ( third operand ) .
 : param cpu : current CPU .
 : param op0 : destination operand .
 : param op1 : source operand .
 : param op3 : order operand ."""

implementation:
size = op0 . size
arg0 = op0 . read ( )
arg1 = op1 . read ( )
order = Operators . ZEXTEND ( op3 . read ( ) , size )
arg0 = arg0 & 0xffffffffffffffffffffffffffffffff00000000000000000000000000000000
arg0 |= ( ( arg1 >> ( ( ( order >> 0 ) & 3 ) * 32 ) ) & 0xffffffff )
arg0 |= ( ( arg1 >> ( ( ( order >> 2 ) & 3 ) * 32 ) ) & 0xffffffff ) << 32
arg0 |= ( ( arg1 >> ( ( ( order >> 4 ) & 3 ) * 32 ) ) & 0xffffffff ) << 64
arg0 |= ( ( arg1 >> ( ( ( order >> 6 ) & 3 ) * 32 ) ) & 0xffffffff ) << 96
op0 . write ( arg0 )


signature:
def PMOVMSKB ( cpu , op0 , op1 ) :
    """Moves byte mask to general - purpose register .
 Creates an 8 - bit mask made up of the most significant bit of each byte of the source operand
 ( second operand ) and stores the result in the low byte or word of the destination operand
 ( first operand ) . The source operand is an MMX ( TM ) technology or an XXM register ; the destination
 operand is a general - purpose register .
 : param cpu : current CPU .
 : param op0 : destination operand .
 : param op1 : source operand ."""

implementation:
arg0 = op0 . read ( )
arg1 = op1 . read ( )
res = 0
for i in reversed ( range ( 7 , op1 . size , 8 ) ) :
    res = ( res << 1 ) | ( ( arg1 >> i ) & 1 )
op0 . write ( Operators . EXTRACT ( res , 0 , op0 . size ) )


signature:
def PSRLDQ ( cpu , dest , src ) :
    """Packed shift right logical double quadword .
 Shifts the destination operand ( first operand ) to the right by the number
 of bytes specified in the count operand ( second operand ) . The empty high - order
 bytes are cleared ( set to all 0s ) . If the value specified by the count
 operand is greater than 15 , the destination operand is set to all 0s .
 The destination operand is an XMM register . The count operand is an 8 - bit
 immediate : :
 TEMP = SRC ;
 if ( TEMP > 15 ) TEMP = 16;
 DEST = DEST > > ( temp * 8 ) ;
 : param cpu : current CPU .
 : param dest : destination operand .
 : param src : count operand ."""

implementation:
# TODO ( yan ) : Verify the correctness of truncating SRC like this ( tests
# use ' - 1 ' as the value
temp = Operators . EXTRACT ( src . read ( ) , 0 , 8 )
temp = Operators . ITEBV ( src . size , temp > 15 , 16 , temp )
dest . write ( dest . read ( ) >> ( temp * 8 ) )


signature:
def MOVZX ( cpu , op0 , op1 ) :
    """Moves with zero - extend .
 Copies the contents of the source operand ( register or memory location ) to the destination
 operand ( register ) and zero extends the value to 16 or 32 bits . The size of the converted value
 depends on the operand - size attribute : :
 OP0 = ZeroExtend ( OP1 ) ;
 : param cpu : current CPU .
 : param op0 : destination operand .
 : param op1 : source operand ."""

implementation: op0 . write ( Operators . ZEXTEND ( op1 . read ( ) , op0 . size ) )


signature:
def MOVSX ( cpu , op0 , op1 ) :
    """Moves with sign - extension .
 Copies the contents of the source operand ( register or memory location ) to the destination
 operand ( register ) and sign extends the value to 16 : :
 OP0 = SignExtend ( OP1 ) ;
 : param cpu : current CPU .
 : param op0 : destination operand .
 : param op1 : source operand ."""

implementation: op0 . write ( Operators . SEXTEND ( op1 . read ( ) , op1 . size , op0 . size ) )


signature:
def CQO ( cpu ) :
    """RDX : RAX = sign - extend of RAX ."""

implementation:
res = Operators . SEXTEND ( cpu . RAX , 64 , 128 )
cpu . RAX = Operators . EXTRACT ( res , 0 , 64 )
cpu . RDX = Operators . EXTRACT ( res , 64 , 64 )


signature:
def CDQ ( cpu ) :
    """EDX : EAX = sign - extend of EAX"""

implementation: cpu . EDX = Operators . EXTRACT ( Operators . SEXTEND ( cpu . EAX , 32 , 64 ) , 32 , 32 )


signature:
def CWDE ( cpu ) :
    """Converts word to doubleword .
 DX = sign - extend of AX .
 : param cpu : current CPU ."""

implementation:
bit = Operators . EXTRACT ( cpu . AX , 15 , 1 )
cpu . EAX = Operators . SEXTEND ( cpu . AX , 16 , 32 )
cpu . EDX = Operators . SEXTEND ( bit , 1 , 32 )


signature:
def RDTSC ( cpu ) :
    """Reads time - stamp counter .
 Loads the current value of the processor ' s time - stamp counter into the
 EDX : EAX registers . The time - stamp counter is contained in a 64 - bit
 MSR . The high - order 32 bits of the MSR are loaded into the EDX
 register , and the low - order 32 bits are loaded into the EAX register .
 The processor increments the time - stamp counter MSR every clock cycle
 and resets it to 0 whenever the processor is reset .
 : param cpu : current CPU ."""

implementation:
val = cpu . icount
cpu . RAX = val & 0xffffffff
cpu . RDX = ( val >> 32 ) & 0xffffffff


signature:
def SYSCALL ( cpu ) :
    """Calls to interrupt procedure .
 The INT n instruction generates a call to the interrupt or exception handler specified
 with the destination operand . The INT n instruction is the general mnemonic for executing
 a software - generated call to an interrupt handler . The INTO instruction is a special
 mnemonic for calling overflow exception ( # OF ) , interrupt vector number 4 . The overflow
 interrupt checks the OF flag in the EFLAGS register and calls the overflow interrupt handler
 if the OF flag is set to 1.
 : param cpu : current CPU ."""

implementation:
cpu . RCX = cpu . RIP
cpu . R11 = cpu . RFLAGS
raise Syscall ( )


signature:
def MOVLPD ( cpu , dest , src ) :
    """Moves low packed double - precision floating - point value .
 Moves a double - precision floating - point value from the source operand ( second operand ) and the
 destination operand ( first operand ) . The source and destination operands can be an XMM register
 or a 64 - bit memory location . This instruction allows double - precision floating - point values to be moved
 to and from the low quadword of an XMM register and memory . It cannot be used for register to register
 or memory to memory moves . When the destination operand is an XMM register , the high quadword of the
 register remains unchanged .
 : param cpu : current CPU .
 : param dest : destination operand .
 : param src : source operand ."""

implementation:
value = src . read ( )
if src . size == 64 and dest . size == 128 :
    value = ( dest . read ( ) & 0xffffffffffffffff0000000000000000 ) | Operators . ZEXTEND ( value , 128 )
dest . write ( value )


signature:
def MOVHPD ( cpu , dest , src ) :
    """Moves high packed double - precision floating - point value .
 Moves a double - precision floating - point value from the source operand ( second operand ) and the
 destination operand ( first operand ) . The source and destination operands can be an XMM register
 or a 64 - bit memory location . This instruction allows double - precision floating - point values to be moved
 to and from the high quadword of an XMM register and memory . It cannot be used for register to
 register or memory to memory moves . When the destination operand is an XMM register , the low quadword
 of the register remains unchanged .
 : param cpu : current CPU .
 : param dest : destination operand .
 : param src : source operand ."""

implementation:
if src . size == 128 :
    assert dest . size == 64
    dest . write ( Operators . EXTRACT ( src . read ( ) , 64 , 64 ) )
else :
    assert src . size == 64 and dest . size == 128
    value = Operators . EXTRACT ( dest . read ( ) , 0 , 64 )
    # low part
    dest . write ( Operators . CONCAT ( 128 , src . read ( ) , value ) )


signature:
def PSUBB ( cpu , dest , src ) :
    """Packed subtract .
 Performs a SIMD subtract of the packed integers of the source operand ( second operand ) from the packed
 integers of the destination operand ( first operand ) , and stores the packed integer results in the
 destination operand . The source operand can be an MMX ( TM ) technology register or a 64 - bit memory location ,
 or it can be an XMM register or a 128 - bit memory location . The destination operand can be an MMX or an XMM
 register .
 The PSUBB instruction subtracts packed byte integers . When an individual result is too large or too small
 to be represented in a byte , the result is wrapped around and the low 8 bits are written to the
 destination element .
 : param cpu : current CPU .
 : param dest : destination operand .
 : param src : source operand ."""

implementation:
result = [ ]
value_a = dest . read ( )
value_b = src . read ( )
for i in reversed ( range ( 0 , dest . size , 8 ) ) :
    a = Operators . EXTRACT ( value_a , i , 8 )
    b = Operators . EXTRACT ( value_b , i , 8 )
    result . append ( ( a - b ) & 0xff )
dest . write ( Operators . CONCAT ( 8 * len ( result ) , * result ) )


signature:
def POR ( cpu , dest , src ) :
    """Performs a bitwise logical OR operation on the source operand ( second operand ) and the destination operand
 ( first operand ) and stores the result in the destination operand . The source operand can be an MMX technology
 register or a 64 - bit memory location or it can be an XMM register or a 128 - bit memory location . The destination
 operand can be an MMX technology register or an XMM register . Each bit of the result is set to 1 if either
 or both of the corresponding bits of the first and second operands are 1 ; otherwise , it is set to 0."""

implementation: res = dest . write ( dest . read ( ) | src . read ( ) )


signature:
def XORPS ( cpu , dest , src ) :
    """Performs a bitwise logical OR operation on the source operand ( second operand ) and the destination operand
 ( first operand ) and stores the result in the destination operand . The source operand can be an MMX technology
 register or a 64 - bit memory location or it can be an XMM register or a 128 - bit memory location . The destination
 operand can be an MMX technology register or an XMM register . Each bit of the result is set to 1 if either
 or both of the corresponding bits of the first and second operands are 1 ; otherwise , it is set to 0."""


signature:
def VORPD ( cpu , dest , src , src2 ) :
    """Performs a bitwise logical OR operation on the source operand ( second operand ) and second source operand ( third operand )
 and stores the result in the destination operand ( first operand ) ."""

implementation: res = dest . write ( src . read ( ) | src2 . read ( ) )


signature:
def VORPS ( cpu , dest , src , src2 ) :
    """Performs a bitwise logical OR operation on the source operand ( second operand ) and second source operand ( third operand )
 and stores the result in the destination operand ( first operand ) ."""


signature:
def PTEST ( cpu , dest , src ) :
    """PTEST
 PTEST set the ZF flag if all bits in the result are 0 of the bitwise AND
 of the first source operand ( first operand ) and the second source operand
 ( second operand ) . Also this sets the CF flag if all bits in the result
 are 0 of the bitwise AND of the second source operand ( second operand )
 and the logical NOT of the destination operand ."""

implementation:
cpu . OF = False
cpu . AF = False
cpu . PF = False
cpu . SF = False
cpu . ZF = ( Operators . EXTRACT ( dest . read ( ) , 0 , 128 ) & Operators . EXTRACT ( src . read ( ) , 0 , 128 ) ) == 0
cpu . CF = ( Operators . EXTRACT ( src . read ( ) , 0 , 128 ) & ~ ( Operators . EXTRACT ( dest . read ( ) , 0 , 128 ) ) ) == 0


signature:
def MOVQ ( cpu , dest , src ) :
    """Move quadword .
 Copies a quadword from the source operand ( second operand ) to the destination operand ( first operand ) .
 The source and destination operands can be MMX ( TM ) technology registers , XMM registers , or 64 - bit memory
 locations . This instruction can be used to move a between two MMX registers or between an MMX register
 and a 64 - bit memory location , or to move data between two XMM registers or between an XMM register and
 a 64 - bit memory location . The instruction cannot be used to transfer data between memory locations .
 When the source operand is an XMM register , the low quadword is moved ; when the destination operand is
 an XMM register , the quadword is stored to the low quadword of the register , and the high quadword is
 cleared to all 0s : :
 MOVQ instruction when operating on MMX registers and memory locations :
 DEST = SRC ;
 MOVQ instruction when source and destination operands are XMM registers :
 DEST [ 63-0 ] = SRC [ 63-0 ] ;
 MOVQ instruction when source operand is XMM register and destination operand is memory location :
 DEST = SRC [ 63-0 ] ;
 MOVQ instruction when source operand is memory location and destination operand is XMM register :
 DEST [ 63-0 ] = SRC ;
 DEST [ 127-64 ] = 00000H ;
 : param cpu : current CPU .
 : param dest : destination operand .
 : param src : source operand ."""

implementation:
# mmx to mmx or mmx to mem
if dest . size == src . size and dest . size == 64 :
    dest . write ( src . read ( ) )
# two xmm regs
elif dest . size == src . size and dest . size == 128 :
    src_lo = Operators . EXTRACT ( src . read ( ) , 0 , 64 )
    dest . write ( Operators . ZEXTEND ( src_lo , 128 ) )
# mem to xmm
elif dest . size == 128 and src . size == 64 :
    dest . write ( Operators . ZEXTEND ( src . read ( ) , dest . size ) )
# xmm to mem
elif dest . size == 64 and src . size == 128 :
    dest . write ( Operators . EXTRACT ( src . read ( ) , 0 , dest . size ) )
else :
    msg = 'Invalid size in MOVQ'
    logger . error ( msg )
    raise Exception ( msg )


signature:
def MOVSD ( cpu , dest , src ) :
    """Move Scalar Double - Precision Floating - Point Value
 Moves a scalar double - precision floating - point value from the source
 operand ( second operand ) to the destination operand ( first operand ) .
 The source and destination operands can be XMM registers or 64 - bit memory
 locations . This instruction can be used to move a double - precision
 floating - point value to and from the low quadword of an XMM register and
 a 64 - bit memory location , or to move a double - precision floating - point
 value between the low quadwords of two XMM registers . The instruction
 cannot be used to transfer data between memory locations .
 When the source and destination operands are XMM registers , the high
 quadword of the destination operand remains unchanged . When the source
 operand is a memory location and destination operand is an XMM registers ,
 the high quadword of the destination operand is cleared to all 0s .
 : param cpu : current CPU .
 : param dest : destination operand .
 : param src : source operand ."""

implementation:
assert dest . type != 'memory' or src . type != 'memory'
value = Operators . EXTRACT ( src . read ( ) , 0 , 64 )
if dest . size > src . size :
    value = Operators . ZEXTEND ( value , dest . size )
dest . write ( value )


signature:
def MOVSS ( cpu , dest , src ) :
    """Moves a scalar single - precision floating - point value
 Moves a scalar single - precision floating - point value from the source operand ( second operand )
 to the destination operand ( first operand ) . The source and destination operands can be XMM
 registers or 32 - bit memory locations . This instruction can be used to move a single - precision
 floating - point value to and from the low doubleword of an XMM register and a 32 - bit memory
 location , or to move a single - precision floating - point value between the low doublewords of
 two XMM registers . The instruction cannot be used to transfer data between memory locations .
 When the source and destination operands are XMM registers , the three high - order doublewords of the
 destination operand remain unchanged . When the source operand is a memory location and destination
 operand is an XMM registers , the three high - order doublewords of the destination operand are cleared to all 0s .
 / / MOVSS instruction when source and destination operands are XMM registers :
 if ( IsXMM ( Source ) & & IsXMM ( Destination ) )
 Destination [ 0 . . 31 ] = Source [ 0 . . 31 ] ;
 / / Destination [ 32 . . 127 ] remains unchanged
 / / MOVSS instruction when source operand is XMM register and destination operand is memory location :
 else if ( IsXMM ( Source ) & & IsMemory ( Destination ) )
 Destination = Source [ 0 . . 31 ] ;
 / / MOVSS instruction when source operand is memory location and destination operand is XMM register :
 else {
 Destination [ 0 . . 31 ] = Source ;
 Destination [ 32 . . 127 ] = 0;"""

implementation:
if dest . type == 'register' and src . type == 'register' :
    assert dest . size == 128 and src . size == 128
    dest . write ( dest . read ( ) & ~ 0xffffffff | src . read ( ) & 0xffffffff )
elif dest . type == 'memory' :
    assert src . type == 'register'
    dest . write ( Operators . EXTRACT ( src . read ( ) , 0 , dest . size ) )
else :
    assert src . type == 'memory' and dest . type == 'register'
    assert src . size == 32 and dest . size == 128
    dest . write ( Operators . ZEXTEND ( src . read ( ) , 128 ) )


signature:
def VEXTRACTF128 ( cpu , dest , src , offset ) :
    """Extract Packed Floating - Point Values
 Extracts 128 - bits of packed floating - point values from the source
 operand ( second operand ) at an 128 - bit offset from imm8[0 ] into the
 destination operand ( first operand ) . The destination may be either an
 XMM register or an 128 - bit memory location ."""

implementation:
offset = offset . read ( )
dest . write ( Operators . EXTRACT ( src . read ( ) , offset * 128 , ( offset + 1 ) * 128 ) )


signature:
def PALIGNR ( cpu , dest , src , offset ) :
    """ALIGNR concatenates the destination operand ( the first operand ) and the source
 operand ( the second operand ) into an intermediate composite , shifts the composite
 at byte granularity to the right by a constant immediate , and extracts the right -
 aligned result into the destination ."""

implementation: dest . write ( Operators . EXTRACT ( Operators . CONCAT ( dest . size * 2 , dest . read ( ) , src . read ( ) ) , offset . read ( ) * 8 , dest . size ) )


signature:
def PSLLDQ ( cpu , dest , src ) :
    """Packed Shift Left Logical Double Quadword
 Shifts the destination operand ( first operand ) to the left by the number
 of bytes specified in the count operand ( second operand ) . The empty low - order
 bytes are cleared ( set to all 0s ) . If the value specified by the count
 operand is greater than 15 , the destination operand is set to all 0s .
 The destination operand is an XMM register . The count operand is an 8 - bit
 immediate .
 TEMP = COUNT ;
 if ( TEMP > 15 ) TEMP = 16;
 DEST = DEST < < ( TEMP * 8 ) ;"""

implementation:
count = Operators . ZEXTEND ( src . read ( ) , dest . size * 2 )
byte_count = Operators . ITEBV ( src . size * 2 , count > 15 , 16 , count )
bit_count = byte_count * 8
val = Operators . ZEXTEND ( dest . read ( ) , dest . size * 2 )
val = val << ( Operators . ZEXTEND ( bit_count , dest . size * 2 ) )
dest . write ( Operators . EXTRACT ( val , 0 , dest . size ) )


signature:
def PSRLQ ( cpu , dest , src ) :
    """Shift Packed Data Right Logical
 Shifts the bits in the individual quadword in the destination operand to the right by
 the number of bits specified in the count operand . As the bits in the data elements
 are shifted right , the empty high - order bits are cleared ( set to 0 ) . If the value
 specified by the count operand is greater than 63 , then the destination operand is set
 to all 0s .
 if ( OperandSize = = 64 ) {
 / / PSRLQ instruction with 64 - bit operand :
 if ( Count > 63 ) Destination [ 64 . . 0 ] = 0;
 else Destination = ZeroExtend ( Destination > > Count ) ;
 else {
 / / PSRLQ instruction with 128 - bit operand :
 if ( Count > 15 ) Destination [ 128 . . 0 ] = 0;
 else {
 Destination [ 0 . . 63 ] = ZeroExtend ( Destination [ 0 . . 63 ] > > Count ) ;
 Destination [ 64 . . 127 ] = ZeroExtend ( Destination [ 64 . . 127 ] > > Count ) ;"""

implementation:
count = src . read ( )
count = Operators . ITEBV ( src . size , Operators . UGT ( count , 63 ) , 64 , count )
count = Operators . EXTRACT ( count , 0 , 64 )
if dest . size == 64 :
    dest . write ( dest . read ( ) >> count )
else :
    hi = Operators . EXTRACT ( dest . read ( ) , 64 , 64 ) >> count
    low = Operators . EXTRACT ( dest . read ( ) , 0 , 64 ) >> count
    dest . write ( Operators . CONCAT ( 128 , hi , low ) )


signature:
def VPSHUFB ( cpu , op0 , op1 , op3 ) :
    """Packed shuffle bytes .
 Copies bytes from source operand ( second operand ) and inserts them in the destination operand
 ( first operand ) at locations selected with the order operand ( third operand ) .
 : param cpu : current CPU .
 : param op0 : destination operand .
 : param op1 : source operand .
 : param op3 : order operand ."""

implementation:
size = op0 . size
arg0 = op0 . read ( )
arg1 = op1 . read ( )
arg3 = Operators . ZEXTEND ( op3 . read ( ) , size )
arg0 |= Operators . ITEBV ( size , Operators . EXTRACT ( arg3 , 7 , 1 ) == 1 , 0 , ( arg1 >> ( ( arg3 >> 0 ) & 7 * 8 ) ) & 0xff )
arg0 |= Operators . ITEBV ( size , Operators . EXTRACT ( arg3 , 15 , 1 ) == 1 , 0 , ( ( arg1 >> ( ( arg3 >> 8 ) & 7 * 8 ) ) & 0xff ) << 8 )
arg0 |= Operators . ITEBV ( size , Operators . EXTRACT ( arg3 , 23 , 1 ) == 1 , 0 , ( ( arg1 >> ( ( arg3 >> 16 ) & 7 * 8 ) ) & 0xff ) << 16 )
arg0 |= Operators . ITEBV ( size , Operators . EXTRACT ( arg3 , 31 , 1 ) == 1 , 0 , ( ( arg1 >> ( ( arg3 >> 24 ) & 7 * 8 ) ) & 0xff ) << 24 )
arg0 |= Operators . ITEBV ( size , Operators . EXTRACT ( arg3 , 39 , 1 ) == 1 , 0 , ( ( arg1 >> ( ( arg3 >> 32 ) & 7 * 8 ) ) & 0xff ) << 32 )
arg0 |= Operators . ITEBV ( size , Operators . EXTRACT ( arg3 , 47 , 1 ) == 1 , 0 , ( ( arg1 >> ( ( arg3 >> 40 ) & 7 * 8 ) ) & 0xff ) << 40 )
arg0 |= Operators . ITEBV ( size , Operators . EXTRACT ( arg3 , 55 , 1 ) == 1 , 0 , ( ( arg1 >> ( ( arg3 >> 48 ) & 7 * 8 ) ) & 0xff ) << 48 )
arg0 |= Operators . ITEBV ( size , Operators . EXTRACT ( arg3 , 63 , 1 ) == 1 , 0 , ( ( arg1 >> ( ( arg3 >> 56 ) & 7 * 8 ) ) & 0xff ) << 56 )
arg0 |= Operators . ITEBV ( size , Operators . EXTRACT ( arg3 , 71 , 1 ) == 1 , 0 , ( ( arg1 >> ( ( arg3 >> 64 ) & 7 * 8 ) ) & 0xff ) << 64 )
arg0 |= Operators . ITEBV ( size , Operators . EXTRACT ( arg3 , 79 , 1 ) == 1 , 0 , ( ( arg1 >> ( ( arg3 >> 72 ) & 7 * 8 ) ) & 0xff ) << 72 )
arg0 |= Operators . ITEBV ( size , Operators . EXTRACT ( arg3 , 87 , 1 ) == 1 , 0 , ( ( arg1 >> ( ( arg3 >> 80 ) & 7 * 8 ) ) & 0xff ) << 80 )
arg0 |= Operators . ITEBV ( size , Operators . EXTRACT ( arg3 , 95 , 1 ) == 1 , 0 , ( ( arg1 >> ( ( arg3 >> 88 ) & 7 * 8 ) ) & 0xff ) << 88 )
arg0 |= Operators . ITEBV ( size , Operators . EXTRACT ( arg3 , 103 , 1 ) == 1 , 0 , ( ( arg1 >> ( ( arg3 >> 96 ) & 7 * 8 ) ) & 0xff ) << 96 )
arg0 |= Operators . ITEBV ( size , Operators . EXTRACT ( arg3 , 111 , 1 ) == 1 , 0 , ( ( arg1 >> ( ( arg3 >> 104 ) & 7 * 8 ) ) & 0xff ) << 104 )
arg0 |= Operators . ITEBV ( size , Operators . EXTRACT ( arg3 , 119 , 1 ) == 1 , 0 , ( ( arg1 >> ( ( arg3 >> 112 ) & 7 * 8 ) ) & 0xff ) << 112 )
arg0 |= Operators . ITEBV ( size , Operators . EXTRACT ( arg3 , 127 , 1 ) == 1 , 0 , ( ( arg1 >> ( ( arg3 >> 120 ) & 7 * 8 ) ) & 0xff ) << 120 )
op0 . write ( arg0 )


signature:
def XLATB ( cpu ) :
    """Table look - up translation .
 Locates a byte entry in a table in memory , using the contents of the
 AL register as a table index , then copies the contents of the table entry
 back into the AL register . The index in the AL register is treated as
 an unsigned integer . The XLAT and XLATB instructions get the base address
 of the table in memory from either the DS : EBX or the DS : BX registers .
 In 64 - bit mode , operation is similar to that in legacy or compatibility mode .
 AL is used to specify the table index ( the operand size is fixed at 8 bits ) .
 RBX , however , is used to specify the table ' s base address : :
 IF address _ bit _ size = 16
 THEN
 AL = ( DS : BX + ZeroExtend ( AL ) ) ;
 ELSE IF ( address _ bit _ size = 32)
 AL = ( DS : EBX + ZeroExtend ( AL ) ) ; FI ;
 ELSE ( address _ bit _ size = 64)
 AL = ( RBX + ZeroExtend ( AL ) ) ;
 FI ;
 : param cpu : current CPU .
 : param dest : destination operand ."""

implementation: cpu . AL = cpu . read_int ( cpu . RBX + Operators . ZEXTEND ( cpu . AL , 64 ) , 8 )


implementation: cpu . AL = cpu . read_int ( cpu . EBX + Operators . ZEXTEND ( cpu . AL , 32 ) , 8 )


signature:
def constrain ( self , constraint ) :
    """Constrain state .
 : param manticore . core . smtlib . Bool constraint : Constraint to add"""

implementation:
constraint = self . migrate_expression ( constraint )
self . _constraints . add ( constraint )


signature:
def new_symbolic_buffer ( self , nbytes , ** options ) :
    """Create and return a symbolic buffer of length ` nbytes ` . The buffer is
 not written into State ' s memory ; write it to the state ' s memory to
 introduce it into the program state .
 : param int nbytes : Length of the new buffer
 : param str label : ( keyword arg only ) The label to assign to the buffer
 : param bool cstring : ( keyword arg only ) Whether or not to enforce that the buffer is a cstring
 ( i . e . no NULL bytes , except for the last byte ) . ( bool )
 : param taint : Taint identifier of the new buffer
 : type taint : tuple or frozenset
 : return : : class : ` ~ manticore . core . smtlib . expression . Expression ` representing the buffer ."""

implementation:
label = options . get ( 'label' )
avoid_collisions = False
if label is None :
    label = 'buffer'
    avoid_collisions = True
taint = options . get ( 'taint' , frozenset ( ) )
expr = self . _constraints . new_array ( name = label , index_max = nbytes , value_bits = 8 , taint = taint , avoid_collisions = avoid_collisions )
self . _input_symbols . append ( expr )
if options . get ( 'cstring' , False ) :
    for i in range ( nbytes - 1 ) :
        self . _constraints . add ( expr [ i ] != 0 )
return expr


signature:
def new_symbolic_value ( self , nbits , label = None , taint = frozenset ( ) ) :
    """Create and return a symbolic value that is ` nbits ` bits wide . Assign
 the value to a register or write it into the address space to introduce
 it into the program state .
 : param int nbits : The bitwidth of the value returned
 : param str label : The label to assign to the value
 : param taint : Taint identifier of this value
 : type taint : tuple or frozenset
 : return : : class : ` ~ manticore . core . smtlib . expression . Expression ` representing the value"""

implementation:
assert nbits in ( 1 , 4 , 8 , 16 , 32 , 64 , 128 , 256 )
avoid_collisions = False
if label is None :
    label = 'val'
    avoid_collisions = True
expr = self . _constraints . new_bitvec ( nbits , name = label , taint = taint , avoid_collisions = avoid_collisions )
self . _input_symbols . append ( expr )
return expr


signature:
def concretize ( self , symbolic , policy , maxcount = 7 ) :
    """This finds a set of solutions for symbolic using policy .
 This raises TooManySolutions if more solutions than maxcount"""

implementation:
assert self . constraints == self . platform . constraints
symbolic = self . migrate_expression ( symbolic )
vals = [ ]
if policy == 'MINMAX' :
    vals = self . _solver . minmax ( self . _constraints , symbolic )
elif policy == 'MAX' :
    vals = self . _solver . max ( self . _constraints , symbolic )
elif policy == 'MIN' :
    vals = self . _solver . min ( self . _constraints , symbolic )
elif policy == 'SAMPLED' :
    m , M = self . _solver . minmax ( self . _constraints , symbolic )
    vals += [ m , M ]
    if M - m > 3 :
        if self . _solver . can_be_true ( self . _constraints , symbolic == ( m + M ) // 2 ) :
            vals . append ( ( m + M ) // 2 )
    if M - m > 100 :
        for i in ( 0 , 1 , 2 , 5 , 32 , 64 , 128 , 320 ) :
            if self . _solver . can_be_true ( self . _constraints , symbolic == m + i ) :
                vals . append ( m + i )
            if maxcount <= len ( vals ) :
                break
    if M - m > 1000 and maxcount > len ( vals ) :
        vals += self . _solver . get_all_values ( self . _constraints , symbolic , maxcnt = maxcount - len ( vals ) , silent = True )
elif policy == 'ONE' :
    vals = [ self . _solver . get_value ( self . _constraints , symbolic ) ]
else :
    assert policy == 'ALL'
    vals = solver . get_all_values ( self . _constraints , symbolic , maxcnt = maxcount , silent = True )
return tuple ( set ( vals ) )


signature:
def solve_one ( self , expr , constrain = False ) :
    """Concretize a symbolic : class : ` ~ manticore . core . smtlib . expression . Expression ` into
 one solution .
 : param manticore . core . smtlib . Expression expr : Symbolic value to concretize
 : param bool constrain : If True , constrain expr to concretized value
 : return : Concrete value
 : rtype : int"""

implementation:
expr = self . migrate_expression ( expr )
value = self . _solver . get_value ( self . _constraints , expr )
if constrain :
    self . constrain ( expr == value )
# Include forgiveness here
if isinstance ( value , bytearray ) :
    value = bytes ( value )
return value


signature:
def solve_n ( self , expr , nsolves ) :
    """Concretize a symbolic : class : ` ~ manticore . core . smtlib . expression . Expression ` into
 ` nsolves ` solutions .
 : param manticore . core . smtlib . Expression expr : Symbolic value to concretize
 : return : Concrete value
 : rtype : list [ int ]"""

implementation:
expr = self . migrate_expression ( expr )
return self . _solver . get_all_values ( self . _constraints , expr , nsolves , silent = True )


signature:
def solve_max ( self , expr ) :
    """Solves a symbolic : class : ` ~ manticore . core . smtlib . expression . Expression ` into
 its maximum solution
 : param manticore . core . smtlib . Expression expr : Symbolic value to solve
 : return : Concrete value
 : rtype : list [ int ]"""

implementation:
if isinstance ( expr , int ) :
    return expr
expr = self . migrate_expression ( expr )
return self . _solver . max ( self . _constraints , expr )


signature:
def solve_min ( self , expr ) :
    """Solves a symbolic : class : ` ~ manticore . core . smtlib . expression . Expression ` into
 its minimum solution
 : param manticore . core . smtlib . Expression expr : Symbolic value to solve
 : return : Concrete value
 : rtype : list [ int ]"""

implementation:
if isinstance ( expr , int ) :
    return expr
expr = self . migrate_expression ( expr )
return self . _solver . min ( self . _constraints , expr )


signature:
def solve_minmax ( self , expr ) :
    """Solves a symbolic : class : ` ~ manticore . core . smtlib . expression . Expression ` into
 its minimum and maximun solution . Only defined for bitvects .
 : param manticore . core . smtlib . Expression expr : Symbolic value to solve
 : return : Concrete value
 : rtype : list [ int ]"""

implementation:
if isinstance ( expr , int ) :
    return expr
expr = self . migrate_expression ( expr )
return self . _solver . minmax ( self . _constraints , expr )


signature:
def solve_buffer ( self , addr , nbytes , constrain = False ) :
    """Reads ` nbytes ` of symbolic data from a buffer in memory at ` addr ` and attempts to
 concretize it
 : param int address : Address of buffer to concretize
 : param int nbytes : Size of buffer to concretize
 : param bool constrain : If True , constrain the buffer to the concretized value
 : return : Concrete contents of buffer
 : rtype : list [ int ]"""

implementation:
buffer = self . cpu . read_bytes ( addr , nbytes )
result = [ ]
with self . _constraints as temp_cs :
    cs_to_use = self . constraints if constrain else temp_cs
    for c in buffer :
        result . append ( self . _solver . get_value ( cs_to_use , c ) )
        cs_to_use . add ( c == result [ - 1 ] )
return result


signature:
def symbolicate_buffer ( self , data , label = 'INPUT' , wildcard = '+' , string = False , taint = frozenset ( ) ) :
    """Mark parts of a buffer as symbolic ( demarked by the wildcard byte )
 : param str data : The string to symbolicate . If no wildcard bytes are provided ,
 this is the identity function on the first argument .
 : param str label : The label to assign to the value
 : param str wildcard : The byte that is considered a wildcard
 : param bool string : Ensure bytes returned can not be NULL
 : param taint : Taint identifier of the symbolicated data
 : type taint : tuple or frozenset
 : return : If data does not contain any wildcard bytes , data itself . Otherwise ,
 a list of values derived from data . Non - wildcard bytes are kept as
 is , wildcard bytes are replaced by Expression objects ."""

implementation:
if wildcard in data :
    size = len ( data )
    symb = self . _constraints . new_array ( name = label , index_max = size , taint = taint , avoid_collisions = True )
    self . _input_symbols . append ( symb )
    tmp = [ ]
    for i in range ( size ) :
        if data [ i ] == wildcard :
            tmp . append ( symb [ i ] )
        else :
            tmp . append ( data [ i ] )
    data = tmp
if string :
    for b in data :
        if issymbolic ( b ) :
            self . _constraints . add ( b != 0 )
        else :
            assert b != 0
return data


signature:
def _create_emulated_mapping ( self , uc , address ) :
    """Create a mapping in Unicorn and note that we ' ll need it if we retry .
 : param uc : The Unicorn instance .
 : param address : The address which is contained by the mapping .
 : rtype Map"""

implementation:
m = self . _cpu . memory . map_containing ( address )
permissions = UC_PROT_NONE
if 'r' in m . perms :
    permissions |= UC_PROT_READ
if 'w' in m . perms :
    permissions |= UC_PROT_WRITE
if 'x' in m . perms :
    permissions |= UC_PROT_EXEC
uc . mem_map ( m . start , len ( m ) , permissions )
self . _should_be_mapped [ m . start ] = ( len ( m ) , permissions )
return m


signature:
def _hook_xfer_mem ( self , uc , access , address , size , value , data ) :
    """Handle memory operations from unicorn ."""

implementation:
assert access in ( UC_MEM_WRITE , UC_MEM_READ , UC_MEM_FETCH )
if access == UC_MEM_WRITE :
    self . _cpu . write_int ( address , value , size * 8 )
# If client code is attempting to read a value , we need to bring it
# in from Manticore state . If we try to mem _ write it here , Unicorn
# will segfault . We add the value to a list of things that need to
# be written , and ask to restart the emulation .
elif access == UC_MEM_READ :
    value = self . _cpu . read_bytes ( address , size )
    if address in self . _should_be_written :
        return True
    self . _should_be_written [ address ] = value
    self . _should_try_again = True
    return False
return True


signature:
def _hook_unmapped ( self , uc , access , address , size , value , data ) :
    """We hit an unmapped region ; map it into unicorn ."""

implementation:
try :
    m = self . _create_emulated_mapping ( uc , address )
except MemoryException as e :
    self . _to_raise = e
    self . _should_try_again = False
    return False
self . _should_try_again = True
return False


signature:
def _interrupt ( self , uc , number , data ) :
    """Handle software interrupt ( SVC / INT )"""

implementation:
from . . native . cpu . abstractcpu import Interruption
# prevent circular imports
self . _to_raise = Interruption ( number )
return True


signature:
def emulate ( self , instruction ) :
    """Emulate a single instruction ."""

implementation:
# The emulation might restart if Unicorn needs to bring in a memory map
# or bring a value from Manticore state .
while True :
    self . reset ( )
    # Establish Manticore state , potentially from past emulation
    # attempts
    for base in self . _should_be_mapped :
        size , perms = self . _should_be_mapped [ base ]
        self . _emu . mem_map ( base , size , perms )
    for address , values in self . _should_be_written . items ( ) :
        for offset , byte in enumerate ( values , start = address ) :
            if issymbolic ( byte ) :
                from . . native . cpu . abstractcpu import ConcretizeMemory
                raise ConcretizeMemory ( self . _cpu . memory , offset , 8 , "Concretizing for emulation" )
        self . _emu . mem_write ( address , b'' . join ( values ) )
    # Try emulation
    self . _should_try_again = False
    self . _step ( instruction )
    if not self . _should_try_again :
        break


signature:
def _step ( self , instruction ) :
    """A single attempt at executing an instruction ."""

implementation:
logger . debug ( "0x%x:\t%s\t%s" % ( instruction . address , instruction . mnemonic , instruction . op_str ) )
registers = set ( self . _cpu . canonical_registers )
# Refer to EFLAGS instead of individual flags for x86
if self . _cpu . arch == CS_ARCH_X86 : # The last 8 canonical registers of x86 are individual flags ; replace
# with the eflags
    registers -= set ( [ 'CF' , 'PF' , 'AF' , 'ZF' , 'SF' , 'IF' , 'DF' , 'OF' ] )
    registers . add ( 'EFLAGS' )
    # TODO ( mark ) : Unicorn 1.0.1 does not support reading YMM registers ,
    # and simply returns back zero . If a unicorn emulated instruction writes to an
    # XMM reg , we will read back the corresponding YMM register , resulting in an
    # incorrect zero value being actually written to the XMM register . This is
    # fixed in Unicorn PR # 819 , so when that is included in a release , delete
    # these two lines .
    registers -= set ( [ 'YMM0' , 'YMM1' , 'YMM2' , 'YMM3' , 'YMM4' , 'YMM5' , 'YMM6' , 'YMM7' , 'YMM8' , 'YMM9' , 'YMM10' , 'YMM11' , 'YMM12' , 'YMM13' , 'YMM14' , 'YMM15' ] )
    registers |= set ( [ 'XMM0' , 'XMM1' , 'XMM2' , 'XMM3' , 'XMM4' , 'XMM5' , 'XMM6' , 'XMM7' , 'XMM8' , 'XMM9' , 'XMM10' , 'XMM11' , 'XMM12' , 'XMM13' , 'XMM14' , 'XMM15' ] )
# XXX ( yan ) : This concretizes the entire register state . This is overly
# aggressive . Once capstone adds consistent support for accessing
# referred registers , make this only concretize those registers being
# read from .
for reg in registers :
    val = self . _cpu . read_register ( reg )
    if issymbolic ( val ) :
        from . . native . cpu . abstractcpu import ConcretizeRegister
        raise ConcretizeRegister ( self . _cpu , reg , "Concretizing for emulation." , policy = 'ONE' )
    self . _emu . reg_write ( self . _to_unicorn_id ( reg ) , val )
# Bring in the instruction itself
instruction = self . _cpu . decode_instruction ( self . _cpu . PC )
text_bytes = self . _cpu . read_bytes ( self . _cpu . PC , instruction . size )
self . _emu . mem_write ( self . _cpu . PC , b'' . join ( text_bytes ) )
self . _emu . hook_add ( UC_HOOK_MEM_READ_UNMAPPED , self . _hook_unmapped )
self . _emu . hook_add ( UC_HOOK_MEM_WRITE_UNMAPPED , self . _hook_unmapped )
self . _emu . hook_add ( UC_HOOK_MEM_FETCH_UNMAPPED , self . _hook_unmapped )
self . _emu . hook_add ( UC_HOOK_MEM_READ , self . _hook_xfer_mem )
self . _emu . hook_add ( UC_HOOK_MEM_WRITE , self . _hook_xfer_mem )
self . _emu . hook_add ( UC_HOOK_INTR , self . _interrupt )
saved_PC = self . _cpu . PC
try :
    pc = self . _cpu . PC
    if self . _cpu . arch == CS_ARCH_ARM and self . _uc_mode == UC_MODE_THUMB :
        pc |= 1
    self . _emu . emu_start ( pc , self . _cpu . PC + instruction . size , count = 1 )
except UcError as e : # We request re - execution by signaling error ; if we we didn ' t set
# _ should _ try _ again , it was likely an actual error
    if not self . _should_try_again :
        raise
if self . _should_try_again :
    return
if logger . isEnabledFor ( logging . DEBUG ) :
    logger . debug ( "=" * 10 )
    for register in self . _cpu . canonical_registers :
        logger . debug ( f"Register {register:3s}  " f"Manticore: {self._cpu.read_register(register):08x}, " f"Unicorn {self._emu.reg_read(self._to_unicorn_id(register)):08x}" )
    logger . debug ( ">" * 10 )
# Bring back Unicorn registers to Manticore
for reg in registers :
    val = self . _emu . reg_read ( self . _to_unicorn_id ( reg ) )
    self . _cpu . write_register ( reg , val )
# Unicorn hack . On single step , unicorn wont advance the PC register
mu_pc = self . get_unicorn_pc ( )
if saved_PC == mu_pc :
    self . _cpu . PC = saved_PC + instruction . size
# Raise the exception from a hook that Unicorn would have eaten
if self . _to_raise :
    raise self . _to_raise
return


signature:
def rlp_encode ( item ) :
    r"""Recursive Length Prefix Encoding
 : param item : the object to encode , either a string , bytes , bytearray , int , long , or sequence
 https : / / github . com / ethereum / wiki / wiki / RLP
 > > > rlp _ encode ( ' dog ' )
 b ' \ x83dog '
 > > > rlp _ encode ( [ ' cat ' , ' dog ' ] )
 b ' \ xc8 \ x83cat \ x83dog '
 > > > rlp _ encode ( ' ' )
 b ' \ x80'
 > > > rlp _ encode ( [ ] )
 b ' \ xc0'
 > > > rlp _ encode ( 0)
 b ' \ x80'
 > > > rlp _ encode ( ' \ x00 ' )
 b ' \ x00'
 > > > rlp _ encode ( 15)
 b ' \ x0f '
 > > > rlp _ encode ( 1024)
 b ' \ x82 \ x04 \ x00'
 > > > rlp _ encode ( [ [ ] , [ [ ] ] , [ [ ] , [ [ ] ] ] ] )
 b ' \ xc7 \ xc0 \ xc1 \ xc0 \ xc3 \ xc0 \ xc1 \ xc0'"""

implementation:
if item is None or item == 0 :
    ret = b'\x80'
elif isinstance ( item , str ) :
    ret = rlp_encode ( item . encode ( 'utf8' ) )
elif isinstance ( item , ( bytearray , bytes ) ) :
    if len ( item ) == 1 and item [ 0 ] < 0x80 : # For a single byte whose value is in the [ 0x00 , 0x7f ] range , that byte is its own RLP encoding .
        ret = item
    else :
        ret = encode_length ( len ( item ) , 0x80 ) + item
elif isinstance ( item , collections . abc . Sequence ) :
    output = b'' . join ( map ( rlp_encode , item ) )
    ret = encode_length ( len ( output ) , 0xC0 ) + output
elif isinstance ( item , int ) :
    ret = rlp_encode ( int_to_bytes ( item ) )
else :
    raise Exception ( "Cannot encode object of type %s" % type ( item ) . __name__ )
return ret


signature:
def must_be_true ( self , constraints , expression ) -> bool :
    """Check if expression is True and that it can not be False with current constraints"""

implementation:
solutions = self . get_all_values ( constraints , expression , maxcnt = 2 , silent = True )
return solutions == [ True ]


signature:
def max ( self , constraints , X : BitVec , M = 10000 ) :
    """Iteratively finds the maximum value for a symbol within given constraints .
 : param X : a symbol or expression
 : param M : maximum number of iterations allowed"""

implementation:
assert isinstance ( X , BitVec )
return self . optimize ( constraints , X , 'maximize' , M )


signature:
def min ( self , constraints , X : BitVec , M = 10000 ) :
    """Iteratively finds the minimum value for a symbol within given constraints .
 : param constraints : constraints that the expression must fulfil
 : param X : a symbol or expression
 : param M : maximum number of iterations allowed"""

implementation:
assert isinstance ( X , BitVec )
return self . optimize ( constraints , X , 'minimize' , M )


signature:
def minmax ( self , constraints , x , iters = 10000 ) :
    """Returns the min and max possible values for x within given constraints"""

implementation:
if issymbolic ( x ) :
    m = self . min ( constraints , x , iters )
    M = self . max ( constraints , x , iters )
    return m , M
else :
    return x , x


signature:
def _solver_version ( self ) -> Version :
    """If we fail to parse the version , we assume z3 ' s output has changed , meaning it ' s a newer
 version than what ' s used now , and therefore ok .
 Anticipated version _ cmd _ output format : ' Z3 version 4.4.2'
 ' Z3 version 4.4.5 - 64 bit - build hashcode $ Z3GITHASH '"""

implementation:
self . _reset ( )
if self . _received_version is None :
    self . _send ( '(get-info :version)' )
    self . _received_version = self . _recv ( )
key , version = shlex . split ( self . _received_version [ 1 : - 1 ] )
return Version ( * map ( int , version . split ( '.' ) ) )


signature:
def _start_proc ( self ) :
    """Spawns z3 solver process"""

implementation:
assert '_proc' not in dir ( self ) or self . _proc is None
try :
    self . _proc = Popen ( shlex . split ( self . _command ) , stdin = PIPE , stdout = PIPE , bufsize = 0 , universal_newlines = True )
except OSError as e :
    print ( e , "Probably too many cached expressions? visitors._cache..." )
    # Z3 was removed from the system in the middle of operation
    raise Z3NotFoundError
# TODO ( mark ) don ' t catch this exception in two places
# run solver specific initializations
for cfg in self . _init :
    self . _send ( cfg )


signature:
def _stop_proc ( self ) :
    """Stops the z3 solver process by :
 - sending an exit command to it ,
 - sending a SIGKILL signal ,
 - waiting till the process terminates ( so we don ' t leave a zombie process )"""

implementation:
if self . _proc is None :
    return
if self . _proc . returncode is None :
    try :
        self . _send ( "(exit)" )
    except ( SolverError , IOError ) as e : # z3 was too fast to close
        logger . debug ( str ( e ) )
    finally :
        try :
            self . _proc . stdin . close ( )
        except IOError as e :
            logger . debug ( str ( e ) )
        try :
            self . _proc . stdout . close ( )
        except IOError as e :
            logger . debug ( str ( e ) )
        self . _proc . kill ( )
        # Wait for termination , to avoid zombies .
        self . _proc . wait ( )
self . _proc : Popen = None


signature:
def _reset ( self , constraints = None ) :
    """Auxiliary method to reset the smtlib external solver to initial defaults"""

implementation:
if self . _proc is None :
    self . _start_proc ( )
else :
    if self . support_reset :
        self . _send ( "(reset)" )
        for cfg in self . _init :
            self . _send ( cfg )
    else :
        self . _stop_proc ( )
        self . _start_proc ( )
if constraints is not None :
    self . _send ( constraints )