• 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
      • Implemented-opcodes
      • To-do
      • Proof-utilities
      • Peripherals
      • Model-validation
      • Modelcalls
        • X86-out
      • Concrete-simulation-examples
      • Utils
      • Debugging-code-proofs
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• One-byte-opcodes
• Modelcalls

X86-out

Signature

(x86-out proc-mode start-rip temp-rip 
         prefixes rex-byte opcode modr/m sib x86) 
 
  → 
x86

Returns

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

This isn't actually implemented because we don't have any port I/O peripherals modeled. Instead, we use this instruction to perform what are essentially modelcalls (i.e. calls from the software running on the model into the model). See modelcalls for more information.

Definitions and Theorems

Function: x86-out

(defun x86-out (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-out))
  (declare (ignorable __function__))
  (b* ((?ctx 'x86-out))
    (b*
     (((mv flg port-number x86)
       (rme-size-opt proc-mode 1 temp-rip 1 :x nil x86))
      ((when flg)
       (!!ms-fresh :rme-size-error flg))
      ((mv flg (the (signed-byte 48) temp-rip))
       (add-to-*ip proc-mode temp-rip 1 x86))
      ((when flg)
       (!!ms-fresh :increment-error flg))
      (x86 (case port-number
             (1 (modelcall-printk x86))
             (otherwise (!!ms-fresh :unhandled-port port-number)))))
     (write-*ip proc-mode temp-rip x86)))))

Theorem: x86p-of-x86-out

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