		Search-engine friendly clone of the ACL2 documentation.

One-byte-opcodes

X86-loop

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

Definitions and Theorems

Function: x86-loop

(defun x86-loop (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 (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-loop))
  (declare (ignorable __function__))
  (b* ((?ctx 'x86-loop))
   (b* ((badlength? (check-instruction-length start-rip temp-rip 1))
        ((when badlength?)
         (!!fault-fresh :gp 0
                        :instruction-length badlength?))
        (p4? (equal 103 (prefixes->adr prefixes)))
        ((the (integer 2 8) counter-size)
         (select-address-size proc-mode p4? x86))
        (counter (rgfi-size counter-size *rcx* rex-byte x86))
        (counter (trunc counter-size (1- counter)))
        ((the (unsigned-byte 1) zf)
         (flgi :zf x86))
        (branch-cond (if (equal opcode 226)
                         (not (equal counter 0))
                       (if (equal opcode 225)
                           (and (equal zf 1)
                                (not (equal counter 0)))
                         (and (equal zf 0)
                              (not (equal counter 0)))))))
     (if branch-cond
         (b* (((mv flg rel8 x86)
               (rime-size proc-mode 1 temp-rip 1 :x nil x86))
              ((when flg)
               (!!ms-fresh :rime-size-error flg))
              ((mv flg next-rip)
               (add-to-*ip proc-mode temp-rip (1+ rel8)
                           x86))
              ((when flg)
               (!!ms-fresh :rip-increment-error flg))
              (x86 (!rgfi-size counter-size
                               *rcx* counter rex-byte x86))
              (x86 (write-*ip proc-mode next-rip x86)))
           x86)
       (b* (((mv flg next-rip)
             (add-to-*ip proc-mode temp-rip 1 x86))
            ((when flg)
             (!!ms-fresh :rip-increment-error flg))
            (x86 (!rgfi-size counter-size
                             *rcx* counter rex-byte x86))
            (x86 (write-*ip proc-mode next-rip x86)))
         x86))))))

Theorem: x86p-of-x86-loop

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