		Search-engine friendly clone of the ACL2 documentation.

One-byte-opcodes

X86-add/adc/sub/sbb/or/and/xor/cmp-test-rax-i

Operand Fetch and Execute for ADD, ADC, SUB, SBB, OR, AND, XOR, CMP, TEST: Addressing Mode = (rAX, I)

Signature
(x86-add/adc/sub/sbb/or/and/xor/cmp-test-rax-i operation proc-mode start-rip temp-rip prefixes rex-byte opcode modr/m sib x86) → x86
Returns: x86 — Type (x86p x86), given (x86p x86).

Op/En = I: [OP rAX, IMM] or [OP rAX, I]

where rAX is the destination operand and I is the source operand. Note that rAX stands for AL/AX/EAX/RAX, depending on the operand size, and I stands for immediate data.

[OP rAX, IMM] Flags Affected
04, 05: ADD c p a z s o
0C, 0D: OR p z s (o and c cleared, a undefined)
14, 15: ADC c p a z s o
1C, 1D: SBB c p a z s o
24, 25: AND p z s (o and c cleared, a undefined)
2C, 2D: SUB c p a z s o
34, 35: XOR p z s (o and c cleared, a undefined)
3C, 3D: CMP c p a z s o
A8, A9: TEST p z s (o and c cleared, a undefined)

Definitions and Theorems

Function: x86-add/adc/sub/sbb/or/and/xor/cmp-test-rax-i

(defun x86-add/adc/sub/sbb/or/and/xor/cmp-test-rax-i
       (operation proc-mode start-rip temp-rip
                  prefixes rex-byte opcode modr/m sib x86)
 (declare (xargs :stobjs (x86)))
 (declare (type (integer 0 38) operation)
          (type (integer 0 4) proc-mode)
          (type (signed-byte 48) start-rip)
          (type (signed-byte 48) temp-rip)
          (type (unsigned-byte 52) prefixes)
          (type (unsigned-byte 8) rex-byte)
          (type (unsigned-byte 8) opcode)
          (type (unsigned-byte 8) modr/m)
          (type (unsigned-byte 8) sib))
 (declare (ignorable proc-mode start-rip temp-rip
                     prefixes rex-byte opcode modr/m sib))
 (declare (xargs :guard (and (prefixes-p prefixes)
                             (modr/m-p modr/m)
                             (sib-p sib)
                             (rip-guard-okp proc-mode temp-rip)
                             (and (natp operation)
                                  (<= operation 8)))))
 (let
    ((__function__ 'x86-add/adc/sub/sbb/or/and/xor/cmp-test-rax-i))
  (declare (ignorable __function__))
  (b* ((?ctx 'x86-add/adc/sub/sbb/or/and/xor/cmp-test-rax-i))
   (b*
    ((byte-operand? (equal 0 (logand 1 opcode)))
     ((the (integer 1 8) operand-size)
      (select-operand-size proc-mode byte-operand?
                           rex-byte t prefixes nil nil nil x86))
     (rax-size (if (logbitp 3 rex-byte)
                   8
                 operand-size))
     (rax (rgfi-size rax-size *rax* rex-byte x86))
     ((mv ?flg imm x86)
      (rme-size-opt proc-mode
                    operand-size temp-rip 1 :x nil x86))
     ((when flg)
      (!!ms-fresh :rme-size-error flg))
     (imm
       (if
         (and (not byte-operand?)
              (equal rax-size 8))
         (the (unsigned-byte 64)
              (n64 (the (signed-byte 32)
                        (n32-to-i32 (the (unsigned-byte 32) imm)))))
         (the (unsigned-byte 32) imm)))
     ((mv flg (the (signed-byte 49) temp-rip))
      (add-to-*ip proc-mode temp-rip operand-size x86))
     ((when flg)
      (!!ms-fresh :rip-increment-error flg))
     (badlength? (check-instruction-length start-rip temp-rip 0))
     ((when badlength?)
      (!!fault-fresh :gp 0
                     :instruction-length badlength?))
     ((the (unsigned-byte 32) input-rflags)
      (rflags x86))
     ((mv result
          (the (unsigned-byte 32) output-rflags)
          (the (unsigned-byte 32)
               undefined-flags))
      (gpr-arith/logic-spec rax-size
                            operation rax imm input-rflags))
     (x86 (if (or (eql operation 8) (eql operation 7))
              x86
            (!rgfi-size rax-size *rax* result rex-byte x86)))
     (x86 (write-user-rflags output-rflags undefined-flags x86))
     (x86 (write-*ip proc-mode temp-rip x86)))
    x86))))

Theorem: x86p-of-x86-add/adc/sub/sbb/or/and/xor/cmp-test-rax-i

(defthm x86p-of-x86-add/adc/sub/sbb/or/and/xor/cmp-test-rax-i
  (implies (x86p x86)
           (b* ((x86 (x86-add/adc/sub/sbb/or/and/xor/cmp-test-rax-i
                          operation
                          proc-mode start-rip temp-rip prefixes
                          rex-byte opcode modr/m sib x86)))
             (x86p x86)))
  :rule-classes :rewrite)