• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
    • X86isa
      • Program-execution
      • Introduction
      • X86isa-build-instructions
      • Publications
      • Contributors
      • Machine
        • Syscalls
        • Cpuid
        • X86isa-state
        • 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
          • Opcode-maps
          • X86-run
          • Implemented-opcodes
          • Three-byte-opcode-decode-and-execute
          • X86-run-halt-count
          • Two-byte-opcode-decode-and-execute
          • X86-run-steps
          • X86-fetch-decode-execute-halt
          • X86-run-halt
          • X86-run-steps1
        • Physical-memory
        • Decoding-and-spec-utils
        • Instructions
        • X86-modes
        • Segmentation
        • Register-readers-and-writers
        • Other-non-deterministic-computations
        • Environment
        • Paging
      • Implemented-opcodes
      • Proof-utilities
      • To-do
      • Concrete-simulation-examples
      • Model-validation
      • Utils
      • Debugging-code-proofs
    • Execloader
    • Axe
  • Testing-utilities
  • Math

• X86-decoder

X86-fetch-decode-execute

Top-level step function

Signature

(x86-fetch-decode-execute x86) → x86

x86-fetch-decode-execute is the step function of our x86 interpreter. It fetches one instruction by looking up the memory address indicated by the instruction pointer rip, decodes that instruction, and dispatches control to the appropriate instruction semantic function.

Definitions and Theorems

Function: x86-fetch-decode-execute

(defun
 x86-fetch-decode-execute (x86)
 (declare (xargs :stobjs (x86)))
 (declare (xargs :guard t))
 (let
  ((__function__ 'x86-fetch-decode-execute))
  (declare (ignorable __function__))
  (b*
   ((ctx 'x86-fetch-decode-execute)
    ((when (or (ms x86) (fault x86))) x86)
    (proc-mode (x86-operation-mode x86))
    (64-bit-modep (equal proc-mode 0))
    (start-rip (the (signed-byte 48)
                    (read-*ip proc-mode x86)))
    ((mv flg (the (unsigned-byte 52) prefixes)
         (the (unsigned-byte 8) rex-byte)
         x86)
     (get-prefixes proc-mode start-rip 0 0 15 x86))
    ((when flg)
     (!!ms-fresh :error-in-reading-prefixes flg))
    ((the (unsigned-byte 8)
          opcode/vex/evex-byte)
     (prefixes->nxt prefixes))
    ((the (unsigned-byte 4) prefix-length)
     (prefixes->num prefixes))
    ((mv flg temp-rip)
     (add-to-*ip proc-mode start-rip (1+ prefix-length)
                 x86))
    ((when flg)
     (!!ms-fresh :increment-error flg))
    (vex-byte0? (or (equal opcode/vex/evex-byte 197)
                    (equal opcode/vex/evex-byte 196)))
    ((mv flg les/lds-distinguishing-byte x86)
     (if vex-byte0?
         (rme08-opt proc-mode temp-rip 1 :x x86)
         (mv nil 0 x86)))
    ((when flg)
     (!!ms-fresh :les/lds-distinguishing-byte-read-error flg))
    ((when
       (and vex-byte0?
            (or 64-bit-modep
                (and (not 64-bit-modep)
                     (equal (part-select les/lds-distinguishing-byte
                                         :low 6
                                         :high 7)
                            3)))))
     (b*
       (((mv flg temp-rip)
         (add-to-*ip proc-mode temp-rip 1 x86))
        ((when flg)
         (!!ms-fresh :vex-byte1-increment-error flg))
        (vex-prefixes (!vex-prefixes->byte0 opcode/vex/evex-byte 0))
        (vex-prefixes
             (!vex-prefixes->byte1 les/lds-distinguishing-byte
                                   vex-prefixes)))
       (vex-decode-and-execute proc-mode start-rip temp-rip
                               prefixes rex-byte vex-prefixes x86)))
    (opcode/evex-byte opcode/vex/evex-byte)
    (evex-byte0? (equal opcode/evex-byte 98))
    ((mv flg bound-distinguishing-byte x86)
     (if evex-byte0?
         (rme08-opt proc-mode temp-rip 1 :x x86)
         (mv nil 0 x86)))
    ((when flg)
     (!!ms-fresh :bound-distinguishing-byte-read-error flg))
    ((when
         (and evex-byte0?
              (or 64-bit-modep
                  (and (not 64-bit-modep)
                       (equal (part-select bound-distinguishing-byte
                                           :low 6
                                           :high 7)
                              3)))))
     (b* (((mv flg temp-rip)
           (add-to-*ip proc-mode temp-rip 1 x86))
          ((when flg)
           (!!ms-fresh :evex-byte1-increment-error flg))
          (evex-prefixes (!evex-prefixes->byte0 opcode/evex-byte 0))
          (evex-prefixes
               (!evex-prefixes->byte1 bound-distinguishing-byte
                                      evex-prefixes)))
         (evex-decode-and-execute
              proc-mode start-rip temp-rip
              prefixes rex-byte evex-prefixes x86)))
    (opcode-byte opcode/evex-byte)
    (modr/m? (one-byte-opcode-modr/m-p proc-mode opcode-byte))
    ((mv flg (the (unsigned-byte 8) modr/m)
         x86)
     (if modr/m?
         (if (or vex-byte0? evex-byte0?)
             (mv nil les/lds-distinguishing-byte x86)
             (rme08-opt proc-mode temp-rip 1 :x x86))
         (mv nil 0 x86)))
    ((when flg)
     (!!ms-fresh :modr/m-byte-read-error flg))
    ((mv flg temp-rip)
     (if modr/m?
         (add-to-*ip proc-mode temp-rip 1 x86)
         (mv nil temp-rip)))
    ((when flg)
     (!!ms-fresh :increment-error flg))
    (sib?
      (and modr/m?
           (b* ((p4? (eql 103
                          (the (unsigned-byte 8)
                               (prefixes->adr prefixes))))
                (16-bit-addressp
                     (eql 2
                          (select-address-size proc-mode p4? x86))))
               (x86-decode-sib-p modr/m 16-bit-addressp))))
    ((mv flg (the (unsigned-byte 8) sib) x86)
     (if sib?
         (rme08-opt proc-mode temp-rip 1 :x x86)
         (mv nil 0 x86)))
    ((when flg)
     (!!ms-fresh :sib-byte-read-error flg))
    ((mv flg temp-rip)
     (if sib?
         (add-to-*ip proc-mode temp-rip 1 x86)
         (mv nil temp-rip)))
    ((when flg)
     (!!ms-fresh :increment-error flg)))
   (one-byte-opcode-execute proc-mode start-rip temp-rip prefixes
                            rex-byte opcode-byte modr/m sib x86))))

Theorem: x86p-x86-fetch-decode-execute

(defthm x86p-x86-fetch-decode-execute
        (implies (x86p x86)
                 (x86p (x86-fetch-decode-execute x86))))

Theorem: ms-fault-and-x86-fetch-decode-and-execute

(defthm ms-fault-and-x86-fetch-decode-and-execute
        (implies (and (x86p x86)
                      (or (ms x86) (fault x86)))
                 (equal (x86-fetch-decode-execute x86)
                        x86)))

Theorem: x86-fetch-decode-execute-opener

(defthm
 x86-fetch-decode-execute-opener
 (implies
  (and
   (not (ms x86))
   (not (fault x86))
   (equal proc-mode (x86-operation-mode x86))
   (equal start-rip (read-*ip proc-mode x86))
   (not (mv-nth 0
                (get-prefixes proc-mode start-rip 0 0 15 x86)))
   (equal prefixes
          (mv-nth 1
                  (get-prefixes proc-mode start-rip 0 0 15 x86)))
   (equal rex-byte
          (mv-nth 2
                  (get-prefixes proc-mode start-rip 0 0 15 x86)))
   (equal opcode/vex/evex-byte
          (prefixes->nxt prefixes))
   (equal prefix-length (prefixes->num prefixes))
   (equal temp-rip0
          (mv-nth 1
                  (add-to-*ip proc-mode start-rip (1+ prefix-length)
                              x86)))
   (not (equal opcode/vex/evex-byte 196))
   (not (equal opcode/vex/evex-byte 197))
   (not (equal opcode/vex/evex-byte 98))
   (equal modr/m?
          (one-byte-opcode-modr/m-p proc-mode opcode/vex/evex-byte))
   (equal modr/m
          (if modr/m?
              (mv-nth 1 (rme08 proc-mode temp-rip0 1 :x x86))
              0))
   (equal temp-rip1
          (if modr/m?
              (mv-nth 1
                      (add-to-*ip proc-mode temp-rip0 1 x86))
              temp-rip0))
   (equal p4?
          (equal 103 (prefixes->adr prefixes)))
   (equal 16-bit-addressp
          (equal 2
                 (select-address-size proc-mode p4? x86)))
   (equal sib?
          (and modr/m?
               (x86-decode-sib-p modr/m 16-bit-addressp)))
   (equal sib
          (if sib?
              (mv-nth 1 (rme08 proc-mode temp-rip1 1 :x x86))
              0))
   (equal temp-rip2
          (if sib?
              (mv-nth 1
                      (add-to-*ip proc-mode temp-rip1 1 x86))
              temp-rip1))
   (or (app-view x86)
       (not (marking-view x86)))
   (not (mv-nth 0
                (add-to-*ip proc-mode start-rip (1+ prefix-length)
                            x86)))
   (if modr/m?
       (and (not (mv-nth 0
                         (add-to-*ip proc-mode temp-rip0 1 x86)))
            (not (mv-nth 0
                         (rme08 proc-mode temp-rip0 1 :x x86))))
       t)
   (if sib?
       (and (not (mv-nth 0
                         (add-to-*ip proc-mode temp-rip1 1 x86)))
            (not (mv-nth 0
                         (rme08 proc-mode temp-rip1 1 :x x86))))
       t)
   (x86p x86)
   (syntaxp
     (and (not (cw "~% [ x86instr @ rip: ~p0 ~%"
                   start-rip))
          (not (cw "              op0: ~s0 ] ~%"
                   (str::hexify (unquote opcode/vex/evex-byte)))))))
  (equal
    (x86-fetch-decode-execute x86)
    (one-byte-opcode-execute proc-mode
                             start-rip temp-rip2 prefixes rex-byte
                             opcode/vex/evex-byte modr/m sib x86))))