		Search-engine friendly clone of the ACL2 documentation.

Three-byte-opcodes

X86-adcx/adox

Operand Fetch and Execute for ADCX/ADOX

Signature
(x86-adcx/adox adcx proc-mode start-rip temp-rip prefixes rex-byte opcode modr/m sib x86) → x86
Arguments: adcx — Guard (booleanp adcx).
Returns: x86 — Type (x86p x86), given (x86p x86).

Op/En = RM: [OP REG, R/M] or [OP G, E]

where G is the destination operand and E is the source operand. Note that G stands for a general-purpose register specified by the ModRM.reg field, and E stands for a general-purpose register or memory operand specified by the ModRM.r/m field.

These instructions are essentially variations of ADC with different flag behavior. ADCX sums the two operands and the CF flag (just like ADC), then sets the CF flag according to unsigned overflow (just like ADC), but doesn't modify any other flags. ADOX is the same as ADCX but uses/sets OF in place of CF.

Definitions and Theorems

Function: x86-adcx/adox

(defun x86-adcx/adox (adcx proc-mode start-rip temp-rip
                           prefixes rex-byte opcode modr/m sib x86)
 (declare (xargs :stobjs (x86)))
 (declare (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 (xargs :guard (booleanp adcx)))
 (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))))
 (let ((__function__ 'x86-adcx/adox))
  (declare (ignorable __function__))
  (b* ((?ctx 'x86-adcx/adox)
       (?r/m (the (unsigned-byte 3)
                  (modr/m->r/m modr/m)))
       (?mod (the (unsigned-byte 2)
                  (modr/m->mod modr/m)))
       (?reg (the (unsigned-byte 3)
                  (modr/m->reg modr/m))))
   (b*
    ((p2 (prefixes->seg prefixes))
     (p4? (eql 103 (prefixes->adr prefixes)))
     (operand-size (if (logbitp *w* rex-byte) 8 4))
     (g (rgfi-size operand-size
                   (the (unsigned-byte 4)
                        (reg-index reg rex-byte 2))
                   rex-byte x86))
     (seg-reg
         (select-segment-register proc-mode p2 p4? mod r/m sib x86))
     (inst-ac? t)
     ((mv flg0 e
          (the (unsigned-byte 3) increment-rip-by)
          (the (signed-byte 64) e-addr)
          x86)
      (x86-operand-from-modr/m-and-sib-bytes
           proc-mode
           0 operand-size inst-ac? nil seg-reg p4?
           temp-rip rex-byte r/m mod sib 0 x86))
     ((when flg0)
      (!!ms-fresh :x86-operand-from-modr/m-and-sib-bytes flg0))
     ((mv flg (the (signed-byte 48) temp-rip))
      (add-to-*ip proc-mode
                  temp-rip increment-rip-by 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))
      (case operand-size
        (8 (gpr-adcx/adox-spec-8 adcx g e input-rflags))
        (t (gpr-adcx/adox-spec-4 adcx g e input-rflags))))
     (x86 (!rgfi-size operand-size (reg-index reg rex-byte 2)
                      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-adcx/adox

(defthm x86p-of-x86-adcx/adox
 (implies
      (x86p x86)
      (b* ((x86 (x86-adcx/adox adcx
                               proc-mode start-rip temp-rip prefixes
                               rex-byte opcode modr/m sib x86)))
        (x86p x86)))
 :rule-classes :rewrite)