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

Top-level specification function for the x86 ISA model

Signature

(x86-run n x86) → x86

Returns

x86 — Type (x86p x86), given (x86p x86).

x86-run returns the x86 state obtained by executing n instructions or until it halts, whatever comes first. It simply called the step function x86-fetch-decode-execute recursively.

Definitions and Theorems

Function: x86-run

(defun x86-run (n x86)
  (declare (xargs :stobjs (x86)))
  (declare (type (unsigned-byte 59) n))
  (let ((__function__ 'x86-run))
    (declare (ignorable __function__))
    (cond ((fault x86) x86)
          ((ms x86) x86)
          ((mbe :logic (zp n) :exec (equal 0 n))
           x86)
          (t (let* ((x86 (x86-fetch-decode-execute x86))
                    (n (the (unsigned-byte 59) (1- n))))
               (x86-run n x86))))))

Theorem: x86p-of-x86-run

(defthm x86p-of-x86-run
  (implies (x86p x86)
           (b* ((x86 (x86-run n x86))) (x86p x86)))
  :rule-classes :rewrite)

Theorem: x86-run-and-x86-fetch-decode-and-execute-commutative

(defthm x86-run-and-x86-fetch-decode-and-execute-commutative
  (implies (and (natp k)
                (x86p x86)
                (not (ms x86))
                (not (fault x86)))
           (equal (x86-run k (x86-fetch-decode-execute x86))
                  (x86-fetch-decode-execute (x86-run k x86)))))

Theorem: x86-run-halted

(defthm x86-run-halted
  (implies (or (ms x86) (fault x86))
           (equal (x86-run n x86) x86)))

Theorem: x86-run-opener-not-ms-not-fault-zp-n

(defthm x86-run-opener-not-ms-not-fault-zp-n
  (implies (and (syntaxp (quotep n)) (zp n))
           (equal (x86-run n x86) x86)))

Theorem: x86-run-opener-not-ms-not-zp-n

(defthm x86-run-opener-not-ms-not-zp-n
  (implies (and (not (ms x86))
                (not (fault x86))
                (syntaxp (quotep n))
                (not (zp n)))
           (equal (x86-run n x86)
                  (x86-run (1- n)
                           (x86-fetch-decode-execute x86)))))

Theorem: x86-run-plus

(defthm x86-run-plus
  (implies (and (natp n1)
                (natp n2)
                (syntaxp (quotep n1)))
           (equal (x86-run (clk+ n1 n2) x86)
                  (x86-run n2 (x86-run n1 x86)))))

Theorem: x86-run-plus-1

(defthm x86-run-plus-1
  (implies (and (natp n1)
                (natp n2)
                (syntaxp (quotep n1)))
           (equal (x86-run (clk+ n1 n2) x86)
                  (x86-run n1 (x86-run n2 x86)))))