		Search-engine friendly clone of the ACL2 documentation.

X86-modes

X86-operation-mode

Returns the current mode of operation of the x86 machine

Signature
(x86-operation-mode x86) → mode
Returns: mode — Type (natp mode).

We only support 64-bit, Compatibility, and 32-bit Protected Modes for now.

Definitions and Theorems

Function: x86-operation-mode

(defun x86-operation-mode (x86)
  (declare (xargs :stobjs (x86)))
  (declare (xargs :guard t))
  (let ((__function__ 'x86-operation-mode))
    (declare (ignorable __function__))
    (cond ((64-bit-modep x86) 0) (t 1))))

Theorem: natp-of-x86-operation-mode

(defthm natp-of-x86-operation-mode
  (b* ((mode (x86-operation-mode x86)))
    (natp mode))
  :rule-classes (:type-prescription :rewrite))

Theorem: range-of-x86-operation-mode

(defthm range-of-x86-operation-mode
  (b* ((?mode (x86-operation-mode x86)))
    (and (<= 0 mode) (< mode 5)))
  :rule-classes :linear)

Theorem: x86-operation-mode-of-xw

(defthm x86-operation-mode-of-xw
  (implies (and (not (equal fld :msr))
                (not (equal fld :seg-hidden-attr)))
           (equal (x86-operation-mode (xw fld index value x86))
                  (x86-operation-mode x86))))

Theorem: x86-operation-mode-of-write-user-rflags

(defthm x86-operation-mode-of-write-user-rflags
  (equal (x86-operation-mode (write-user-rflags vector mask x86))
         (x86-operation-mode x86)))