		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 and bigmem::bigmem. 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 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)
```

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) (8))
    :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)

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