		Search-engine friendly clone of the ACL2 documentation.

Machine

X86isa-state

The state of the x86isa model

Definition of the x86isa state

The definition of the state uses nested and abstract stobjs by way of community books rstobj2::defrstobj, bigmem::bigmem, or bigmem-asymmetric::bigmem-asymmetric. It may be interesting to read about the old definition to see how the current definition supports all of its functionality but in a more maintainable way; see x86isa-state-history.

The bigmem and bigmem-asymmetric books define a memory model similar to the old x86isa memory model in that it provides a record representation for reasoning and an allocate-on-demand, array-like performance for execution. The x86 concrete stobj has the bigmem stobj for its memory field; defrstobj exports the bigmem memory accessor and updater functions alongside those of other x86 fields and gives us a state definition that's logically a multi-typed record. defrstobj also allows the definition of a universal accessor and updater, so we still retain that feature in the x86isa books.

Note that the bigmem books define a 64-bit address space, though the x86isa state restricts that to a 52-bit address space because the max. physical address allowed by the x86 architecture is 52 (as of this writing in mid-2021). If the max. allowed physical address is increased anywhere up to 64 bits, then we can simply change the size of the mem field in the x86isa stobj.

x86 ISA state components modeled by x86isa

Fields that govern the model's operation

These fields are an artifact of our x86 ISA model.

MS: Model state, used to indicate I/O or errors that our model does not handle yet. Basically, we use the model state to assert partial correctness. If the model state is nil till the end of execution, we expect the results to be correct. Otherwise, all bets are off.
```
(ms :type t :initially nil)
```
FAULT: We need some way to pass exceptions and such around. So we stuff them into the fault slot, to be processed by the step function.
```
(fault :type t :initially nil)
```

ENV: Environment for the programs running on our x86 model.

(env :type (satisfies env-alistp)
    :fix (ec-call (env-alist-fix x))
    :initially nil)

UNDEF: Field that seeds unknown values that characterize commonly occurring undefined behavior.
```
(undef :type t :initially 0)
```
APP-VIEW: This field acts as a switch. When its value is t, support for system features like paging is absent. When its value is nil, the model is in sys-view and support for system features is present.
```
(app-view :type (satisfies booleanp)
         :fix (acl2::bool-fix x)
         :initially t)
```
MARKING-VIEW: This field also acts as a switch. When its value is t, then accessed and dirty bits in the paging structures are set during those data structure traversals, as expected. Otherwise, these bits are not set. This switch is meaningful only in when the model is in sys-view.
```
(marking-view :type (satisfies booleanp)
             :fix (acl2::bool-fix x)
             :initially t)
```
ENABLE-PERIPHERALS: This field also acts as a switch. When its value is t, then the model's peripherals (timer and TTY) are enabled. Otherwise, the model acts like there are no peripherals. This only applies when the model is in sys-view.
```
(enable-peripherals :type (satisfies booleanp)
                   :fix (acl2::bool-fix x)
                   :initially t)
```
HANDLE-INTERRUPTS: This field also acts as a switch. When its value is t, then exceptions and interrupts are handled using handlers in the IDT. Otherwise, exceptions and interrupts cause the ms or fault fields to be set after instruction execution, which terminates execution when using x86-run. This only applies when the model is in sys-view. Note: The timer peripheral triggers interrupts, and they won't be handled unless this is t, so if you are using it, you probably want to enable this.
```
(handle-exceptions :type (satisfies booleanp)
                  :fix (acl2::bool-fix x)
                  :initially t)
```

OS-INFO: This field is meaningful only in app-view mode to model system call behavior.

(os-info :type (satisfies keywordp)
        :fix (ec-call (os-info-fix x))
        :initially :linux)

Components of the x86 state specified by this model

RGF: The general-purpose registers are just an array of signed 64-bit integers. Note that we choose to define the GPRs as signed integers for the sake of efficiency. For instance, -1 in unsigned format would occupy 64 bits, a bignum. But in the signed format, it would be a fixum. See Intel Volume 1, Section 3.4.1 (General-Purpose Registers) for information about these registers.
```
(rgf :type (array (signed-byte 64) (16))
    :initially 0
    :fix (logext 64 (ifix x))
    :resizable nil
    :accessor rgfi
    :updater !rgfi)
```
RIP: We choose the RIP to be a 48-bit signed integer. RIP can contain only canonical addresses, which range from 0 to 2^47-1 and 2^64-2^47 to 2^64-1, inclusive, for the 64-bit mode. So, in our model, 0 to 2^47-1 represents the lower range of canonical addresses and -2^47 to -1 represents the upper range of canonical addresses. See Intel manual, Jan'19, Volume 1, Section 3.5 for details about the instruction pointer.
```
(rip :type (signed-byte 48)
    :initially 0
    :fix (logext 48 (ifix x)))
```
RFLAGS: We define the rflags register as a 32-bit field, even though in the 64-bit mode, rflags is a 64-bit register --- this is justified because Intel says that the top 32 bits of rflags are reserved. See Intel manual, Jan'19A, Volume 1, Section 3.4.3 for details about rflags.
```
(rflags :type (unsigned-byte 32)
       :initially 2
       :fix (loghead 32 (ifix x)))
```

User Segment Registers:

Visible portion:

16-bit selector INDEX(13)::TI(1)::RPL(2)

Hidden/Cache portion (see Intel manual, Mar'17, Vol. 3A, Figure 3-7):

16-bit Attributes
       32-bit Limit
       64-bit Base Address

See Intel manual, Jan'19, Volume 1, Section 3.4.2 and Intel manual, Jan'19, Volume 3, Sections 3.4.2 and 3.4.3 for details.

(seg-visible :type (array (unsigned-byte 16) (6))
            :initially 0
            :fix (loghead 16 (ifix x))
            :resizable nil
            :accessor seg-visiblei
            :updater !seg-visiblei)

(seg-hidden-base :type (array (unsigned-byte 64) (6))
                :fix (loghead 64 (ifix x))
                :initially 0
                :resizable nil
                :accessor seg-hidden-basei
                :updater !seg-hidden-basei)

(seg-hidden-limit :type (array (unsigned-byte 32) (6))
                 :fix (loghead 32 (ifix x))
                 :initially 0
                 :resizable nil
                 :accessor seg-hidden-limiti
                 :updater !seg-hidden-limiti)

(seg-hidden-attr :type (array (unsigned-byte 16) (6))
                :fix (loghead 16 (ifix x))
                :initially 0
                :resizable nil
                :accessor seg-hidden-attri
                :updater !seg-hidden-attri)

System Table Registers (GDTR and IDTR): These registers point to bounded tables of (up to 8192) segment descriptors. In 64-bit mode, the system table registers are extended from 48 to 80 bits. See Intel manual, Jan'19, Volume 3, Figure 2-6.
```
(str :type (array (unsigned-byte 80) (2))
    :fix (loghead 80 (ifix x))
    :initially 0
    :resizable nil
    :accessor stri
    :updater !stri)
```

System Segment Registers (Task Register and LDTR):

Visible portion:

16-bit selector INDEX(13)::TI(1)::RPL(2)

Hidden/Cache portion:

16-bit Attributes
       32-bit Limit
       64-bit Base Address

See Intel manual, Jan'19, Volume 3, Figure 2-6 for details.

(ssr-visible :type (array (unsigned-byte 16) (2))
            :initially 0
            :fix (loghead 16 (ifix x))
            :resizable nil
            :accessor ssr-visiblei
            :updater !ssr-visiblei)

(ssr-hidden-base :type (array (unsigned-byte 64) (2))
                :initially 0
                :fix (loghead 64 (ifix x))
                :resizable nil
                :accessor ssr-hidden-basei
                :updater !ssr-hidden-basei)

(ssr-hidden-limit :type (array (unsigned-byte 32) (2))
                 :initially 0
                 :fix (loghead 32 (ifix x))
                 :resizable nil
                 :accessor ssr-hidden-limiti
                 :updater !ssr-hidden-limiti)

(ssr-hidden-attr :type (array (unsigned-byte 16) (2))
                :fix (loghead 16 (ifix x))
                :initially 0
                :resizable nil
                :accessor ssr-hidden-attri
                :updater !ssr-hidden-attri)

CTR: Control registers --- See Intel manual, Jan'19, Volume 3, Section 2.5.

(ctr :type (array (unsigned-byte 64) (17))
    :fix (loghead 64 (ifix x))
    :initially 0
    :resizable nil
    :accessor ctri
    :updater !ctri)

DBG: Debug registers --- See Intel manual, Jan'19, Volume 3, Section 17.2.

(dbg :type (array (unsigned-byte 64) (8))
    :initially 0
    :fix (loghead 64 (ifix x))
    :resizable nil
    :accessor dbgi
    :updater !dbgi)

FPU 80-bit data registers: The MMX registers (MM0 through MM7) are aliased to the low 64-bits of the FPU data registers. See Intel manual, Jan'19, Volume 1, Section 8.1.2.
```
(fp-data :type (array (unsigned-byte 80) (8))
        :fix (loghead 80 (ifix x))
        :initially 0
        :resizable nil
        :accessor fp-datai
        :updater !fp-datai)
```

FPU 16-bit control register: See Intel manual, Jan'19, Volume 1, Section 8.1.5.

(fp-ctrl :type (unsigned-byte 16)
        :fix (loghead 16 (ifix x))
        :initially 0)

FPU 16-bit status register: See Intel manual, Jan'19, Volume 1, Section 8.1.3.

(fp-status :type (unsigned-byte 16)
          :fix (loghead 16 (ifix x))
          :initially 0)

FPU 16-bit tag register: See Intel manual, Jan'19, Volume 1, Section 8.1.7.

(fp-tag :type (unsigned-byte 16)
       :fix (loghead 16 (ifix x))
       :initially 0)

FPU 48-bit last instruction pointer: See Intel manual, Jan'19, Volume 1, Figure 8-1.

(fp-last-inst :type (unsigned-byte 48)
             :fix (loghead 48 (ifix x))
             :initially 0)

FPU 48-bit last data (operand) pointer: See Intel manual, Jan'19, Volume 1, Figure 8-1.

(fp-last-data :type (unsigned-byte 48)
             :fix (loghead 48 (ifix x))
             :initially 0)

FPU 11-bit opcode: See Intel manual, Jan'19, Volume 1, Figure 8-1.

(fp-opcode :type (unsigned-byte 11)
          :fix (loghead 11 (ifix x))
          :initially 0)

MXCSR register

(mxcsr :type (unsigned-byte 32)
      :fix (loghead 32 (ifix x))
      :initially 8064)

OPMASK: 8 opmask registers are used for conditional execution and merging of data elements in the destination operands of AVX-512 EVEX-encoded instructions. They are also used as operands in opmask instructions like KMOV, etc.
```
(opmsk :type (array (unsigned-byte 64) (8))
      :fix (loghead 64 (ifix x))
      :initially 0
      :resizable nil
      :accessor opmski
      :updater !opmski)
```
ZMM: ZMM 512-bit data registers --- the lower 256-bits of the ZMM registers are aliased to the respective 256-bit YMM registers and the lower 128-bit are aliased to the respective 128-bit XMM registers. Note that registers YMM16/XMM16 to YMM31/XMM31 are available only via the EVEX prefix (AVX-512).
```
(zmm :type (array (unsigned-byte 512) (32))
    :fix (loghead 512 (ifix x))
    :initially 0
    :resizable nil
    :accessor zmmi
    :updater !zmmi)
```

MSR: Model-specific registers

(msr :type (array (unsigned-byte 64) (11))
    :fix (loghead 64 (ifix x))
    :initially 0
    :resizable nil
    :accessor msri
    :updater !msri)

MEM: Field modeling 2^52 bytes of physical memory in sys-view and 2^48 bytes of linear memory in app-view.

(mem :type (array (unsigned-byte 8)
                 (4503599627370496))
    :initially 0
    :fix (loghead 8 (ifix x))
    :child-stobj bigmem::mem
    :child-accessor bigmem::read-mem
    :child-updater bigmem::write-mem
    :accessor memi
    :updater !memi)

Inhibit Interrupts One Instruction: The Intel manual states that some instructions, like the STI instruction, inhibit interrupts for one instruction after execution, despite the interrupt flag being set immediately. This flag is used to implement that. It is t when interrupts should not be allows and is cleared after executing an instruction if it was set at the beginning of the instruction. Consult the documentation for STI in Volume 2B 4.3 in the Intel manual.
```
(inhibit-interrupts-one-instruction :type (satisfies booleanp)
                                   :initially nil
                                   :fix (acl2::bool-fix x))
```

Time Stamp Counter: This keeps track of how many instructions have been executed for the RDTSC instruction.

(time-stamp-counter :type (satisfies natp)
                   :initially 0
                   :fix (nfix x))

Last Clock Event: Our clock device sends a clock event every 100,000 instructions. When interrupts are disabled, however, we can't send a clock event. Instead of sending one on every 100,000 instructions, we send an interrupt if interrupts are enabled and the last clock event was 100,000 or more instructions ago. This keeps track of how many instructions have been executed since the last clock event.
```
(last-clock-event :type (satisfies natp)
                 :initially 0
                 :fix (nfix x))
```
Implicit Supervisor Access: This field is a boolean flag that, when t, tells the address translation system that all translations should be treated as implicit supervisor accesses, regardless of current privilege level.
```
(implicit-supervisor-access :type (satisfies booleanp)
                           :initially nil
                           :fix (acl2::bool-fix x))
```
TLB: This field models a (number of) TLB(s). See tlb for a detailed discussion about our address translation caching scheme and its consistency with the x86 ISA. It is a fast alist that is tlbp. Invalid translations are not cached.
```
(tlb :type (satisfies tlbp)
    :initially :tlb
    :fix (tlb-fix x))
```

TTY-in: This field models the input buffer of the TTY device.

(tty-in :type (satisfies tty-bufferp)
       :initially nil
       :fix (tty-buffer-fix x))

TTY-out: This field models the output buffer of the TTY device.

(tty-out :type (satisfies tty-bufferp)
        :initially nil
        :fix (tty-buffer-fix x))

Subtopics

X86isa-state-history: A short history of the definition of the x86 state
Environment-field: An environment field that includes a simple model of the file system and an oracle
Physical-memory-model: How to change physical memory models
Save-restore: Tools for saving and restoring the x86 state