• 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
      • Booting-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

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*
   (((when (or (ms x86) (fault x86))) x86)
    (app-view? (app-view x86))
    (inhibit-interrupts-one-instruction?
         (inhibit-interrupts-one-instruction x86))
    (x86
     (b*
      ((ctx 'x86-fetch-decode-execute)
       (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))
       (x86 (one-byte-opcode-execute
                 proc-mode start-rip temp-rip prefixes
                 rex-byte opcode-byte modr/m sib x86)))
      x86))
    ((when app-view?) x86)
    (x86 (if (enable-peripherals x86)
             (x86-exec-peripherals x86)
           x86))
    (x86 (if (and (fault x86)
                  (handle-exceptions x86))
             (handle-faults x86)
           x86))
    (x86 (if inhibit-interrupts-one-instruction?
             (!inhibit-interrupts-one-instruction nil x86)
           x86)))
   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
   (app-view x86)
   (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))))