• 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-address-size

Address size of an instruction, in bytes.

Signature

(select-address-size proc-mode p4? x86) → address-size

Arguments

p4? — Guard (booleanp p4?).

x86 — Guard (x86p x86).

Returns

address-size — Type (member-equal address-size '(2 4 8)).

This is based on AMD manual, Dec'17, Volume 3, Table 1-3, and AMD manual, Dec'17, Volume 2, Sections 4.7 and 4.8.

In 64-bit mode, the address size is 64 bits if there is no address override prefix, 32 bits if there is an address override prefix. In 32-bit mode, the address size is 32 bits if either (i) the default address size is 32 bits and there is no address override prefix, or (ii) the default address size is 16 bits and there is an eddress override prefix; otherwise, the address size is 16 bits. In 32-bit mode, the default address size is determined by the CS.D bit of the code segment: 32 bits if CS.D is 1, 16 bits if CS.D is 0.

The boolean argument of this function indicates whether there is an override prefix or not.

Definitions and Theorems

Function: select-address-size$inline

(defun select-address-size$inline (proc-mode p4? x86)
 (declare (xargs :stobjs (x86)))
 (declare (type (integer 0 4) proc-mode))
 (declare (xargs :guard (and (booleanp p4?) (x86p x86))))
 (case proc-mode
  (0 (if p4? 4 8))
  (otherwise
    (b* (((the (unsigned-byte 16) cs-attr)
          (seg-hidden-attri 1 x86))
         (cs.d (code-segment-descriptor-attributesbits->d cs-attr)))
      (if (= cs.d 1)
          (if p4? 2 4)
        (if p4? 4 2))))))

Theorem: return-type-of-select-address-size

(defthm return-type-of-select-address-size
 (b* ((address-size (select-address-size$inline proc-mode p4? x86)))
   (member-equal address-size '(2 4 8)))
 :rule-classes :rewrite)

Theorem: select-address-size-not-2-when-64-bit-modep

(defthm select-address-size-not-2-when-64-bit-modep
  (not (equal 2 (select-address-size 0 p4? x86))))