• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
      • X86isa
        • Program-execution
        • Sdm-instruction-set-summary
        • Tlb
        • Running-linux
        • Introduction
        • Asmtest
        • X86isa-build-instructions
        • Publications
        • Contributors
        • Machine
          • X86isa-state
          • Syscalls
          • Cpuid
          • Linear-memory
          • Rflag-specifications
          • Characterizing-undefined-behavior
          • Top-level-memory
          • App-view
          • X86-decoder
            • Get-prefixes
              • Vex-0f3a-execute
              • Vex-0f38-execute
              • Vex-0f-execute
              • Two-byte-opcode-execute
              • Second-three-byte-opcode-execute
              • One-byte-opcode-execute
              • First-three-byte-opcode-execute
              • Evex-0f3a-execute
              • Evex-0f38-execute
              • Evex-0f-execute
              • X86-fetch-decode-execute
              • Vex-decode-and-execute
              • Evex-decode-and-execute
              • X86-run
              • Implemented-opcodes
              • Three-byte-opcode-decode-and-execute
              • X86-run-halt-count
              • Two-byte-opcode-decode-and-execute
              • X86-run-steps
              • Opcode-maps
              • X86-run-halt
              • X86-fetch-decode-execute-halt
              • X86-run-steps1
            • Physical-memory
            • Decoding-and-spec-utils
            • Instructions
            • Register-readers-and-writers
            • X86-modes
            • Segmentation
            • Other-non-deterministic-computations
            • Environment
            • Paging
          • Implemented-opcodes
          • To-do
          • Proof-utilities
          • Peripherals
          • Model-validation
          • Modelcalls
          • Concrete-simulation-examples
          • Utils
          • Debugging-code-proofs
        • Axe
        • Execloader
      • Math
      • Testing-utilities
    • X86-decoder

    Get-prefixes

    Fetch and store legacy and REX prefixes, if any, of an instruction

    Signature
    (get-prefixes proc-mode start-rip prefixes rex-byte cnt x86) 
  → 
(mv flg new-prefixes new-rex-byte new-x86)
    Returns
    new-prefixes — Type (natp new-prefixes), given (forced-and (natp prefixes) (canonical-address-p start-rip) (x86p x86)) .
    new-rex-byte — Type (natp new-rex-byte), given (forced-and (natp rex-byte) (natp prefixes) (x86p x86)).
    new-x86 — Type (x86p new-x86), given (forced-and (x86p x86) (canonical-address-p start-rip)).

    The function get-prefixes fetches the legacy and REX prefixes of an instruction and also returns the first byte following the last such prefix. The input start-rip points to the first byte of an instruction, which may potentially be a legacy prefix. The initial value of cnt should be 15 so that the result (- 15 cnt) returned at the end of the recursion is the correct number of legacy and/or REX bytes parsed by this function.

    Legacy Prefixes

    From Intel Manual, Vol. 2, May 2018, Section 2.1.1 (Instruction Prefixes):

    Instruction prefixes are divided into four groups, each with a set of allowable prefix codes. For each instruction, it is only useful to include up to one prefix code from each of the four groups (Groups 1, 2, 3, 4). Groups 1 through 4 may be placed in any order relative to each other.

    Despite the quote from the Intel Manual above, the order of the legacy prefixes does matter when there is more than one prefix from the same group --- all but the last prefix from a single prefix group are ignored. The only exception in this case is for Group 1 prefixes --- see below for details.

    Examples:

    • 0x64_88_00 is mov byte ptr fs:[rax], al
    • 0x65_88_00 is mov byte ptr gs:[rax], al
    • 0x64_65_88_00 is mov byte ptr gs:[rax], al
    • 0x65_64_88_00 is mov byte ptr fs:[rax], al
    • 0xf2_a4 is repne movsb byte ptr [rdi], byte ptr [rsi]
    • 0xf3_a4 is repe movsb byte ptr [rdi], byte ptr [rsi]
    • 0xf2_f3_a4 is repe movsb byte ptr [rdi], byte ptr [rsi]
    • 0xf3_f2_a4 is repne movsb byte ptr [rdi], byte ptr [rsi]

    We now discuss the Group 1 exception below.

    0xf0_f2_a4 is NOT
    repne movsb byte ptr [rdi], byte ptr [rsi]
    It is:
    lock repne movsb byte ptr [rdi], byte ptr [rsi]
    Note that lock and rep/repne are Group 1 prefixes. It is important to record the lock prefix, even if it is overshadowed by a rep/repne prefix, because the former instruction will not #UD, but the latter instruction will. This is akin to the lock prefix being in a separate group than the rep/repne prefixes; in fact, AMD manuals (Section 1.2.1: Summary of Legacy Prefixes, Vol. 3 May 2018 Edition) treat them as such.

    For details about how mandatory prefixes are picked from legacy prefixes, see mandatory-prefixes-computation.

    REX Prefixes

    A REX prefix (applicable only to 64-bit mode) is treated as a null prefix if it is followed by a legacy prefix. Here is an illustrative example (using Intel's XED, x86 Encoder Decoder --- see https://intelxed.github.io/):

    • xed -64 -d 48670100 is add dword ptr [eax], eax; the REX.W prefix does not have any effect on the operand size, which remains 32 (i.e., the default operand size in the 64-bit mode).
    • xed -64 -d 67480100 is add qword ptr [eax], rax; the REX prefix has the intended effect of promoting the operand size to 64 bits.

    Note that the prefixes structure output of this function does not include the REX byte (which is a separate return value of this function), but its :num-prefixes field includes a count of the REX prefixes encountered. This is because adding an 8-bit field to the prefixes structure to store a REX byte will make it a bignum, thereby impacting execution efficiency.

    Definitions and Theorems

    Theorem: return-type-of-prefixes->num-linear

    (defthm return-type-of-prefixes->num-linear
  (< (prefixes->num prefixes) 16)
  :rule-classes :linear)

    Theorem: return-type-of-prefixes->lck-linear

    (defthm return-type-of-prefixes->lck-linear
  (< (prefixes->lck prefixes) 256)
  :rule-classes :linear)

    Theorem: return-type-of-prefixes->rep-linear

    (defthm return-type-of-prefixes->rep-linear
  (< (prefixes->rep prefixes) 256)
  :rule-classes :linear)

    Theorem: return-type-of-prefixes->seg-linear

    (defthm return-type-of-prefixes->seg-linear
  (< (prefixes->seg prefixes) 256)
  :rule-classes :linear)

    Theorem: return-type-of-prefixes->opr-linear

    (defthm return-type-of-prefixes->opr-linear
  (< (prefixes->opr prefixes) 256)
  :rule-classes :linear)

    Theorem: return-type-of-prefixes->adr-linear

    (defthm return-type-of-prefixes->adr-linear
  (< (prefixes->adr prefixes) 256)
  :rule-classes :linear)

    Theorem: return-type-of-prefixes->nxt-linear

    (defthm return-type-of-prefixes->nxt-linear
  (< (prefixes->nxt prefixes) 256)
  :rule-classes :linear)

    Theorem: return-type-of-prefixes->num-rewrite

    (defthm return-type-of-prefixes->num-rewrite
  (unsigned-byte-p 4 (prefixes->num prefixes))
  :rule-classes :rewrite)

    Theorem: return-type-of-prefixes->lck-rewrite

    (defthm return-type-of-prefixes->lck-rewrite
  (unsigned-byte-p 8 (prefixes->lck prefixes))
  :rule-classes :rewrite)

    Theorem: return-type-of-prefixes->rep-rewrite

    (defthm return-type-of-prefixes->rep-rewrite
  (unsigned-byte-p 8 (prefixes->rep prefixes))
  :rule-classes :rewrite)

    Theorem: return-type-of-prefixes->seg-rewrite

    (defthm return-type-of-prefixes->seg-rewrite
  (unsigned-byte-p 8 (prefixes->seg prefixes))
  :rule-classes :rewrite)

    Theorem: return-type-of-prefixes->opr-rewrite

    (defthm return-type-of-prefixes->opr-rewrite
  (unsigned-byte-p 8 (prefixes->opr prefixes))
  :rule-classes :rewrite)

    Theorem: return-type-of-prefixes->adr-rewrite

    (defthm return-type-of-prefixes->adr-rewrite
  (unsigned-byte-p 8 (prefixes->adr prefixes))
  :rule-classes :rewrite)

    Theorem: return-type-of-prefixes->nxt-rewrite

    (defthm return-type-of-prefixes->nxt-rewrite
  (unsigned-byte-p 8 (prefixes->nxt prefixes))
  :rule-classes :rewrite)

    Theorem: return-type-of-!prefixes->*-linear

    (defthm return-type-of-!prefixes->*-linear
  (and (unsigned-byte-p 52 (!prefixes->num x prefixes))
       (unsigned-byte-p 52 (!prefixes->lck x prefixes))
       (unsigned-byte-p 52 (!prefixes->rep x prefixes))
       (unsigned-byte-p 52 (!prefixes->seg x prefixes))
       (unsigned-byte-p 52 (!prefixes->opr x prefixes))
       (unsigned-byte-p 52 (!prefixes->adr x prefixes))
       (unsigned-byte-p 52 (!prefixes->nxt x prefixes)))
  :rule-classes
  ((:rewrite)
   (:linear :corollary (and (< (!prefixes->num x prefixes)
                               4503599627370496)
                            (< (!prefixes->lck x prefixes)
                               4503599627370496)
                            (< (!prefixes->rep x prefixes)
                               4503599627370496)
                            (< (!prefixes->seg x prefixes)
                               4503599627370496)
                            (< (!prefixes->opr x prefixes)
                               4503599627370496)
                            (< (!prefixes->adr x prefixes)
                               4503599627370496)
                            (< (!prefixes->nxt x prefixes)
                               4503599627370496)))))

    Theorem: loghead-ash-0

    (defthm loghead-ash-0
  (implies (and (natp i)
                (natp j)
                (natp x)
                (<= i j))
           (equal (loghead i (ash x j)) 0)))

    Function: get-prefixes

    (defun get-prefixes (proc-mode start-rip prefixes rex-byte cnt x86)
 (declare (xargs :stobjs (x86)))
 (declare (type (integer 0 4) proc-mode)
          (type (signed-byte 48) start-rip)
          (type (unsigned-byte 52) prefixes)
          (type (unsigned-byte 8) rex-byte)
          (type (integer 0 15) cnt))
 (declare (xargs :guard (prefixes-p prefixes)))
 (let ((__function__ 'get-prefixes))
  (declare (ignorable __function__))
  (if (mbe :logic (zp cnt) :exec (eql cnt 0))
      (mv t prefixes rex-byte x86)
   (b* ((ctx 'get-prefixes)
        ((mv flg (the (unsigned-byte 8) byte)
             x86)
         (rme08-opt proc-mode start-rip 1
                    :x x86))
        ((when flg)
         (mv (cons ctx flg) byte rex-byte x86))
        (prefix-byte-group-code
             (the (integer 0 4)
                  (get-one-byte-prefix-array-code byte))))
    (case prefix-byte-group-code
     (0 (b* ((rex? (and (eql proc-mode 0)
                        (equal (the (unsigned-byte 4) (ash byte -4))
                               4)))
             ((when rex?)
              (mv-let (flg next-rip)
                      (add-to-*ip proc-mode start-rip 1 x86)
                (if flg (mv flg prefixes rex-byte x86)
                  (get-prefixes proc-mode next-rip prefixes
                                byte (the (integer 0 15) (1- cnt))
                                x86)))))
          (let ((prefixes (the (unsigned-byte 52)
                               (!prefixes->nxt byte prefixes))))
            (mv nil
                (the (unsigned-byte 52)
                     (!prefixes->num (- 15 cnt) prefixes))
                rex-byte x86))))
     (1 (b* (((mv flg next-rip)
              (add-to-*ip proc-mode start-rip 1 x86))
             ((when flg)
              (mv flg prefixes rex-byte x86))
             ((the (unsigned-byte 52) prefixes)
              (if (equal byte 240)
                  (!prefixes->lck byte prefixes)
                (!prefixes->rep byte prefixes))))
          (get-prefixes proc-mode next-rip
                        prefixes 0 (the (integer 0 15) (1- cnt))
                        x86)))
     (2 (b* (((mv flg next-rip)
              (add-to-*ip proc-mode start-rip 1 x86))
             ((when flg)
              (mv flg prefixes rex-byte x86)))
          (if (or (and (eql proc-mode 0)
                       (or (equal byte 100) (equal byte 101)))
                  (not (eql proc-mode 0)))
              (get-prefixes proc-mode next-rip
                            (the (unsigned-byte 52)
                                 (!prefixes->seg byte prefixes))
                            0 (the (integer 0 15) (1- cnt))
                            x86)
            (get-prefixes proc-mode next-rip
                          prefixes 0 (the (integer 0 15) (1- cnt))
                          x86))))
     (3 (mv-let (flg next-rip)
                (add-to-*ip proc-mode start-rip 1 x86)
          (if flg (mv flg prefixes rex-byte x86)
            (get-prefixes proc-mode next-rip
                          (the (unsigned-byte 52)
                               (!prefixes->opr byte prefixes))
                          0 (the (integer 0 15) (1- cnt))
                          x86))))
     (4 (mv-let (flg next-rip)
                (add-to-*ip proc-mode start-rip 1 x86)
          (if flg (mv flg prefixes rex-byte x86)
            (get-prefixes proc-mode next-rip
                          (the (unsigned-byte 52)
                               (!prefixes->adr byte prefixes))
                          0 (the (integer 0 15) (1- cnt))
                          x86))))
     (otherwise (mv t prefixes rex-byte x86)))))))

    Theorem: natp-of-get-prefixes.new-prefixes

    (defthm natp-of-get-prefixes.new-prefixes
 (implies (forced-and (natp prefixes)
                      (canonical-address-p start-rip)
                      (x86p x86))
          (b* (((mv ?flg
                    ?new-prefixes ?new-rex-byte ?new-x86)
                (get-prefixes proc-mode
                              start-rip prefixes rex-byte cnt x86)))
            (natp new-prefixes)))
 :rule-classes :type-prescription)

    Theorem: natp-of-get-prefixes.new-rex-byte

    (defthm natp-of-get-prefixes.new-rex-byte
 (implies (forced-and (natp rex-byte)
                      (natp prefixes)
                      (x86p x86))
          (b* (((mv ?flg
                    ?new-prefixes ?new-rex-byte ?new-x86)
                (get-prefixes proc-mode
                              start-rip prefixes rex-byte cnt x86)))
            (natp new-rex-byte)))
 :rule-classes :type-prescription)

    Theorem: x86p-of-get-prefixes.new-x86

    (defthm x86p-of-get-prefixes.new-x86
 (implies (forced-and (x86p x86)
                      (canonical-address-p start-rip))
          (b* (((mv ?flg
                    ?new-prefixes ?new-rex-byte ?new-x86)
                (get-prefixes proc-mode
                              start-rip prefixes rex-byte cnt x86)))
            (x86p new-x86)))
 :rule-classes :rewrite)

    Theorem: prefixes-width-p-of-get-prefixes.new-prefixes

    (defthm prefixes-width-p-of-get-prefixes.new-prefixes
 (implies
  (and (unsigned-byte-p 52 prefixes)
       (canonical-address-p start-rip)
       (x86p x86))
  (unsigned-byte-p
       52
       (mv-nth 1
               (get-prefixes proc-mode
                             start-rip prefixes rex-byte cnt x86))))
 :rule-classes
 (:rewrite
  (:linear
   :corollary
   (implies
    (and (unsigned-byte-p 52 prefixes)
         (canonical-address-p start-rip)
         (x86p x86))
    (and
     (<=
        0
        (mv-nth 1
                (get-prefixes proc-mode
                              start-rip prefixes rex-byte cnt x86)))
     (< (mv-nth 1
                (get-prefixes proc-mode
                              start-rip prefixes rex-byte cnt x86))
        4503599627370496)))
   :hints
   (("Goal"
        :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))

    Theorem: byte-p-of-get-prefixes.new-rex-byte

    (defthm byte-p-of-get-prefixes.new-rex-byte
 (implies
  (and (unsigned-byte-p 8 rex-byte)
       (natp prefixes)
       (x86p x86))
  (unsigned-byte-p
       8
       (mv-nth 2
               (get-prefixes proc-mode
                             start-rip prefixes rex-byte cnt x86))))
 :rule-classes
 (:rewrite
  (:linear
   :corollary
   (implies
    (and (unsigned-byte-p 8 rex-byte)
         (natp prefixes)
         (x86p x86))
    (and
     (<=
        0
        (mv-nth 2
                (get-prefixes proc-mode
                              start-rip prefixes rex-byte cnt x86)))
     (< (mv-nth 2
                (get-prefixes proc-mode
                              start-rip prefixes rex-byte cnt x86))
        256)))
   :hints
   (("Goal"
        :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))

    Theorem: get-prefixes-does-not-modify-x86-state-in-app-view

    (defthm get-prefixes-does-not-modify-x86-state-in-app-view
  (b* (((mv ?flg
            ?new-prefixes ?new-rex-byte ?new-x86)
        (get-prefixes proc-mode
                      start-rip prefixes rex-byte cnt x86)))
    (implies (app-view x86)
             (equal new-x86 x86))))

    Theorem: num-prefixes-get-prefixes-bound

    (defthm num-prefixes-get-prefixes-bound
 (implies
  (and (<= cnt 15)
       (x86p x86)
       (canonical-address-p start-rip)
       (unsigned-byte-p 52 prefixes)
       (< (part-select prefixes :low 0 :high 2)
          5))
  (<=
   (prefixes->num
        (mv-nth 1
                (get-prefixes proc-mode
                              start-rip prefixes rex-byte cnt x86)))
   15))
 :rule-classes :linear)

    Theorem: get-prefixes-opener-lemma-zero-cnt

    (defthm get-prefixes-opener-lemma-zero-cnt
  (implies (zp cnt)
           (equal (get-prefixes proc-mode
                                start-rip prefixes rex-byte cnt x86)
                  (mv t prefixes rex-byte x86))))

    Theorem: get-prefixes-opener-lemma-no-prefix-byte

    (defthm get-prefixes-opener-lemma-no-prefix-byte
 (implies
  (b*
   (((mv flg byte &)
     (rme08 proc-mode start-rip 1 :x x86))
    (prefix-byte-group-code (get-one-byte-prefix-array-code byte)))
   (and (not flg)
        (zp prefix-byte-group-code)
        (if (equal proc-mode 0)
            (not (equal (ash byte -4) 4))
          t)
        (not (zp cnt))))
  (equal
    (get-prefixes proc-mode
                  start-rip prefixes rex-byte cnt x86)
    (let
     ((prefixes (!prefixes->nxt
                     (mv-nth 1 (rme08 proc-mode start-rip 1 :x x86))
                     prefixes)))
     (mv nil (!prefixes->num (- 15 cnt) prefixes)
         rex-byte
         (mv-nth 2
                 (rme08 proc-mode start-rip 1
                        :x x86)))))))

    Theorem: get-prefixes-opener-lemma-no-legacy-prefix-but-rex-prefix

    (defthm get-prefixes-opener-lemma-no-legacy-prefix-but-rex-prefix
 (implies
   (b*
    (((mv flg byte &)
      (rme08 proc-mode start-rip 1 :x x86))
     (prefix-byte-group-code (get-one-byte-prefix-array-code byte)))
    (and (equal proc-mode 0)
         (not flg)
         (zp prefix-byte-group-code)
         (equal (ash byte -4) 4)
         (not (zp cnt))))
   (equal (get-prefixes proc-mode
                        start-rip prefixes rex-byte cnt x86)
          (b* (((mv & byte byte-x86)
                (rme08 proc-mode start-rip 1 :x x86))
               ((mv flg next-rip)
                (add-to-*ip proc-mode start-rip 1 byte-x86)))
            (if flg (mv flg prefixes rex-byte byte-x86)
              (get-prefixes proc-mode
                            next-rip prefixes byte (1- cnt)
                            byte-x86))))))

    Theorem: get-prefixes-opener-lemma-group-1-prefix

    (defthm get-prefixes-opener-lemma-group-1-prefix
  (b*
    (((mv flg byte byte-x86)
      (rme08 proc-mode start-rip 1 :x x86))
     (prefix-byte-group-code (get-one-byte-prefix-array-code byte)))
    (implies
         (and (or (app-view x86)
                  (not (marking-view x86)))
              (not flg)
              (equal prefix-byte-group-code 1)
              (not (zp cnt))
              (not (mv-nth 0
                           (add-to-*ip proc-mode start-rip 1 x86))))
         (equal (get-prefixes proc-mode
                              start-rip prefixes rex-byte cnt x86)
                (let ((prefixes (if (equal byte 240)
                                    (!prefixes->lck byte prefixes)
                                  (!prefixes->rep byte prefixes))))
                  (get-prefixes proc-mode (1+ start-rip)
                                prefixes 0 (1- cnt)
                                byte-x86))))))

    Theorem: get-prefixes-opener-lemma-group-2-prefix

    (defthm get-prefixes-opener-lemma-group-2-prefix
  (b*
    (((mv flg byte byte-x86)
      (rme08 proc-mode start-rip 1 :x x86))
     (prefix-byte-group-code (get-one-byte-prefix-array-code byte)))
    (implies
         (and (or (app-view x86)
                  (and (not (app-view x86))
                       (not (marking-view x86))))
              (not flg)
              (equal prefix-byte-group-code 2)
              (not (zp cnt))
              (not (mv-nth 0
                           (add-to-*ip proc-mode start-rip 1 x86))))
         (equal (get-prefixes proc-mode
                              start-rip prefixes rex-byte cnt x86)
                (if (or (and (eql proc-mode 0)
                             (or (equal byte 100) (equal byte 101)))
                        (not (eql proc-mode 0)))
                    (get-prefixes proc-mode (1+ start-rip)
                                  (!prefixes->seg byte prefixes)
                                  0 (1- cnt)
                                  byte-x86)
                  (get-prefixes proc-mode (1+ start-rip)
                                prefixes 0 (1- cnt)
                                byte-x86))))))

    Theorem: get-prefixes-opener-lemma-group-3-prefix

    (defthm get-prefixes-opener-lemma-group-3-prefix
 (b*
   (((mv flg byte x862)
     (rme08 proc-mode start-rip 1 :x x86))
    (prefix-byte-group-code (get-one-byte-prefix-array-code byte)))
   (implies
        (and (not flg)
             (equal prefix-byte-group-code 3)
             (not (zp cnt))
             (not (mv-nth 0
                          (add-to-*ip proc-mode start-rip 1 x862))))
        (equal (get-prefixes proc-mode
                             start-rip prefixes rex-byte cnt x86)
               (get-prefixes proc-mode (1+ start-rip)
                             (!prefixes->opr byte prefixes)
                             0 (1- cnt)
                             x862)))))

    Theorem: get-prefixes-opener-lemma-group-4-prefix

    (defthm get-prefixes-opener-lemma-group-4-prefix
 (b*
   (((mv flg byte x862)
     (rme08 proc-mode start-rip 1 :x x86))
    (prefix-byte-group-code (get-one-byte-prefix-array-code byte)))
   (implies
        (and (not flg)
             (equal prefix-byte-group-code 4)
             (not (zp cnt))
             (not (mv-nth 0
                          (add-to-*ip proc-mode start-rip 1 x862))))
        (equal (get-prefixes proc-mode
                             start-rip prefixes rex-byte cnt x86)
               (get-prefixes proc-mode (1+ start-rip)
                             (!prefixes->adr byte prefixes)
                             0 (1- cnt)
                             x862)))))

    Theorem: 64-bit-modep-of-get-prefixes

    (defthm 64-bit-modep-of-get-prefixes
  (b* (((mv ?flg
            ?new-prefixes ?new-rex-byte ?new-x86)
        (get-prefixes proc-mode
                      start-rip prefixes rex-byte cnt x86)))
    (equal (64-bit-modep new-x86)
           (64-bit-modep x86))))

    Theorem: x86-operation-mode-of-get-prefixes

    (defthm x86-operation-mode-of-get-prefixes
  (b* (((mv ?flg
            ?new-prefixes ?new-rex-byte ?new-x86)
        (get-prefixes proc-mode
                      start-rip prefixes rex-byte cnt x86)))
    (equal (x86-operation-mode new-x86)
           (x86-operation-mode x86))))