• 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
        • Physical-memory
        • Decoding-and-spec-utils
          • Read-operands-and-write-results
          • Effective-address-computations
          • Select-operand-size
          • Instruction-pointer-operations
          • Stack-pointer-operations
          • Select-segment-register
          • Prefix-modrm-sib-decoding
          • Select-address-size
          • Rex-byte-from-vex-prefixes
          • Check-instruction-length
          • Error-objects
          • Rip-guard-okp
          • Sib-decoding
        • 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

• Decoding-and-spec-utils

Select-operand-size

Selecting the operand size for general-purpose instructions

Signature

(select-operand-size proc-mode byte-operand? 
                     rex-byte imm? prefixes default64? 
                     ignore-rex? ignore-p3-64? x86) 
 
  → 
size

Arguments

x86 — Guard (x86p x86).

Returns

size — Type (natp size).

select-operand-size selects the operand size of the instruction. It is cognizant of the instruction prefixes, the rex byte, the operand type (e.g., immediate operand or not), and the default operand size (obtained from the state).

This function was written by referring to the following:

1. Intel Manuals, Vol. 1, Section 3.6, Table 3-3
2. Intel Manuals, Vol. 1, Section 3.6, Table 3-4
3. Intel Manuals, Vol. 2, Section 2.2.1.2

The first image above has been captured from Volume 1: Basic Architecture, Intel(R) 64 and IA-32 Architectures Software Developer's Manual, Order Number: 253665-062US, March 2017.

The second image above has been captured from Volume 1: Basic Architecture, Intel(R) 64 and IA-32 Architectures Software Developer's Manual, Combined Volumes: 1, 2A, 2B, 2C, 3A, 3B and 3C, Order Number: 325462-054US, April 2015.

• Setting REX.W can be used to determine the operand size but does not solely determine operand width. Like the 66H size prefix, 64-bit operand size override has no effect on byte-specific operations.
• For non-byte operations: if a 66H prefix is used with prefix (REX.W = 1), 66H is ignored.
• If a 66H override is used with REX and REX.W = 0, the operand size is 16 bits.

This function also includes three additional boolean parameters that serve to accommodate instructions that do not quite follow the general rules specified by the table above:

• The default64? parameter says whether the default operand size in 64-bit mode should be 64 bits instead of 32 bits. Examples are x86-near-jmp-op/en-m and x86-push-general-register.
• The ignore-rex? parameter says whether, in 64-bit mode, REX.W should be ignored for the purpose of determining the operand size. Examples are x86-two-byte-jcc, x86-near-jmp-op/en-m, and x86-push-general-register.
• The ignore-p3-64? parameter says whether, in 64-bit mode, P3 should be ignored for the purpose of determining the operand size. Examples are x86-two-byte-jcc and x86-near-jmp-op/en-m.

Definitions and Theorems

Function: select-operand-size$inline

(defun select-operand-size$inline
       (proc-mode byte-operand?
                  rex-byte imm? prefixes default64?
                  ignore-rex? ignore-p3-64? x86)
 (declare (xargs :stobjs (x86)))
 (declare (type (integer 0 4) proc-mode)
          (type (or t nil) byte-operand?)
          (type (unsigned-byte 8) rex-byte)
          (type (or t nil) imm?)
          (type (unsigned-byte 52) prefixes)
          (type (or t nil) default64?)
          (type (or t nil) ignore-rex?)
          (type (or t nil) ignore-p3-64?))
 (declare (xargs :guard (x86p x86)))
 (declare (xargs :guard (prefixes-p prefixes)))
 (if byte-operand? 1
   (if (equal proc-mode 0)
       (if (and (logbitp 3 rex-byte)
                (not ignore-rex?))
           (if imm? 4 8)
         (if (and (eql 102
                       (the (unsigned-byte 8)
                            (prefixes->opr prefixes)))
                  (not ignore-p3-64?))
             2
           (if default64? 8 4)))
     (b* (((the (unsigned-byte 16) cs-attr)
           (seg-hidden-attri 1 x86))
          (cs.d (code-segment-descriptor-attributesbits->d cs-attr))
          (p3? (eql 102
                    (the (unsigned-byte 8)
                         (prefixes->opr prefixes)))))
       (if (= cs.d 1)
           (if p3? 2 4)
         (if p3? 4 2))))))

Theorem: natp-of-select-operand-size

(defthm natp-of-select-operand-size
 (b*
  ((size
       (select-operand-size$inline proc-mode byte-operand?
                                   rex-byte imm? prefixes default64?
                                   ignore-rex? ignore-p3-64? x86)))
  (natp size))
 :rule-classes :type-prescription)

Theorem: select-operand-size-range

(defthm select-operand-size-range
  (and (<= 1
           (select-operand-size proc-mode byte-operand?
                                rex-byte imm? prefixes default64?
                                ignore-rex? ignore-p3-64? x86))
       (<= (select-operand-size proc-mode byte-operand?
                                rex-byte imm? prefixes default64?
                                ignore-rex? ignore-p3-64? x86)
           8))
  :rule-classes :linear)

Theorem: select-operand-size-values

(defthm select-operand-size-values
  (or (equal (select-operand-size proc-mode byte-operand?
                                  rex-byte imm? prefixes default64?
                                  ignore-rex? ignore-p3-64? x86)
             1)
      (equal (select-operand-size proc-mode byte-operand?
                                  rex-byte imm? prefixes default64?
                                  ignore-rex? ignore-p3-64? x86)
             2)
      (equal (select-operand-size proc-mode byte-operand?
                                  rex-byte imm? prefixes default64?
                                  ignore-rex? ignore-p3-64? x86)
             4)
      (equal (select-operand-size proc-mode byte-operand?
                                  rex-byte imm? prefixes default64?
                                  ignore-rex? ignore-p3-64? x86)
             8)))