		Search-engine friendly clone of the ACL2 documentation.

One-byte-opcodes

X86-ret

Signature
(x86-ret 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-ret

(defun x86-ret (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-ret))
  (declare (ignorable __function__))
  (b* ((?ctx 'x86-ret))
   (b*
    ((rsp (read-*sp proc-mode x86))
     ((the (integer 2 8) operand-size)
      (select-operand-size proc-mode nil rex-byte nil 0 t t t x86))
     ((mv flg (the (signed-byte 48) new-rsp)
          x86)
      (if (not (equal opcode 194))
          (b* (((mv flg1 new-rsp)
                (add-to-*sp proc-mode rsp operand-size x86))
               ((when flg1) (mv flg1 0 x86)))
            (mv nil new-rsp x86))
        (b* (((mv flg1 (the (unsigned-byte 16) imm16)
                  x86)
              (rme16-opt proc-mode temp-rip 1 :x nil x86))
             ((when flg1) (mv flg1 0 x86))
             ((mv flg1 new-rsp)
              (add-to-*sp proc-mode rsp (+ operand-size imm16)
                          x86))
             ((when flg1) (mv flg1 0 x86)))
          (mv nil new-rsp x86))))
     ((when flg)
      (!!ms-fresh :imm-rml16-error flg))
     (badlength?
          (and (eql opcode 194)
               (check-instruction-length start-rip temp-rip 2)))
     ((when badlength?)
      (!!fault-fresh :gp 0
                     :instruction-length badlength?))
     (check-alignment? (alignment-checking-enabled-p x86))
     ((mv flg (the (signed-byte 64) tos) x86)
      (if (= operand-size 8)
          (rime-size-opt proc-mode operand-size
                         rsp 2 :r check-alignment? x86
                         :mem-ptr? nil
                         :check-canonicity t)
        (rme-size-opt proc-mode operand-size
                      rsp 2 :r check-alignment? x86
                      :mem-ptr? nil)))
     ((when flg)
      (cond ((and (consp flg)
                  (eql (car flg) :non-canonical-address))
             (!!fault-fresh :ss 0 :riml64-error flg))
            ((and (consp flg)
                  (eql (car flg)
                       :unaligned-linear-address))
             (!!fault-fresh :ac 0
                            :memory-access-unaligned rsp))
            (t (!!fault-fresh flg))))
     ((unless (if (equal proc-mode 0)
                  (canonical-address-p tos)
                (b* (((the (unsigned-byte 32) cs.limit)
                      (seg-hidden-limiti 1 x86)))
                  (or (equal opcode 203)
                      (and (<= 0 tos) (<= tos cs.limit))))))
      (!!fault-fresh :gp 0
                     :bad-return-address tos))
     ((mv new-rsp x86)
      (if
       (equal opcode 203)
       (b*
        (((mv flg cs-selector x86)
          (rme-size-opt proc-mode operand-size
                        new-rsp 2 :r check-alignment? x86
                        :mem-ptr? nil))
         ((when flg)
          (b*
           ((x86
                (cond ((and (consp flg)
                            (eql (car flg) :non-canonical-address))
                       (!!fault-fresh :ss 0 :riml64-error flg))
                      ((and (consp flg)
                            (eql (car flg)
                                 :unaligned-linear-address))
                       (!!fault-fresh :ac 0
                                      :memory-access-unaligned rsp))
                      (t (!!fault-fresh flg)))))
           (mv 0 x86)))
         (cs-selector (loghead 16 cs-selector))
         ((mv flg cs-descriptor x86)
          (get-segment-descriptor 1 cs-selector x86))
         ((when flg)
          (b* (((when (equal flg t))
                (b* ((x86 (!!ms-fresh :get-segment-descriptor)))
                  (mv 0 x86)))
               (x86 (!!fault-fresh (car flg)
                                   (cadr flg)
                                   (caddr flg))))
            (mv 0 x86)))
         (x86 (load-segment-reg 1 cs-selector cs-descriptor x86))
         ((mv flg new-rsp)
          (add-to-*sp proc-mode new-rsp operand-size x86))
         ((when flg)
          (b* ((x86 (!!fault-fresh :ss 0 :pop flg)))
            (mv 0 x86))))
        (mv new-rsp x86))
       (mv new-rsp x86)))
     ((when (or (fault x86) (ms x86))) x86)
     (x86 (write-*sp proc-mode new-rsp x86))
     (x86 (!rip (the (signed-byte 48) tos) x86)))
    x86))))

Theorem: x86p-of-x86-ret

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