• 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
            • X86-operand-from-modr/m-and-sib-bytes
            • Alignment-checking-enabled-p
            • X86-operand-to-zmm/mem
            • X86-operand-to-reg/mem
            • X86-operand-to-xmm/mem
          • 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

• Read-operands-and-write-results

Alignment-checking-enabled-p

Checking if alignment is enabled

Signature

(alignment-checking-enabled-p x86) → enabled

Returns

enabled — Type (booleanp enabled).

Source: Intel Manuals, Volume 3, Section 6.15, Exception and Interrupt Reference:

Interrupt 17 Alignment Check Exception (#AC)

Exception Class: Fault.

Description: Indicates that the processor detected an unaligned memory operand when alignment checking was enabled. Alignment checks are only carried out in data (or stack) accesses (not in code fetches or system segment accesses). An example of an alignment-check violation is a word stored at an odd byte address, or a doubleword stored at an address that is not an integer multiple of 4.

Note that the alignment check exception (#AC) is generated only for data types that must be aligned on word, doubleword, and quadword boundaries. A general-protection exception (#GP) is generated 128-bit data types that are not aligned on a 16-byte boundary.

To enable alignment checking, the following conditions must be true:

• AM flag in CR0 register is set.
• AC flag in the EFLAGS register is set.
• The CPL is 3 (protected mode or virtual-8086 mode).

Alignment-check exceptions (#AC) are generated only when operating at privilege level 3 (user mode). Memory references that default to privilege level 0, such as segment descriptor loads, do not generate alignment-check exceptions, even when caused by a memory reference made from privilege level 3.

Definitions and Theorems

Function: alignment-checking-enabled-p

(defun alignment-checking-enabled-p (x86)
  (declare (xargs :stobjs (x86)))
  (declare (xargs :guard t))
  (let ((__function__ 'alignment-checking-enabled-p))
    (declare (ignorable __function__))
    (b* ((cr0 (the (unsigned-byte 32)
                   (n32 (ctri 0 x86))))
         (am (cr0bits->am cr0))
         (ac (flgi :ac x86))
         (cpl (cpl x86)))
      (and (equal am 1)
           (equal ac 1)
           (equal cpl 3)))))

Theorem: booleanp-of-alignment-checking-enabled-p

(defthm booleanp-of-alignment-checking-enabled-p
  (b* ((enabled (alignment-checking-enabled-p x86)))
    (booleanp enabled))
  :rule-classes :type-prescription)

Theorem: alignment-checking-enabled-p-and-xw

(defthm alignment-checking-enabled-p-and-xw
  (implies
       (and (not (equal fld :ctr))
            (not (equal fld :seg-visible))
            (not (equal fld :rflags)))
       (equal (alignment-checking-enabled-p (xw fld index val x86))
              (alignment-checking-enabled-p x86))))

Theorem: alignment-checking-enabled-p-and-xw-ctr

(defthm alignment-checking-enabled-p-and-xw-ctr
 (implies
   (case-split (or (not (equal (nfix index) *cr0*))
                   (and (equal (nfix index) *cr0*)
                        (equal (cr0bits->am (loghead 32 val))
                               (cr0bits->am (xr :ctr *cr0* x86))))))
   (equal (alignment-checking-enabled-p (xw :ctr index val x86))
          (alignment-checking-enabled-p x86))))

Theorem: alignment-checking-enabled-p-and-xw-rflags

(defthm alignment-checking-enabled-p-and-xw-rflags
 (implies
      (equal (rflagsbits->ac val)
             (rflagsbits->ac (xr :rflags nil x86)))
      (equal (alignment-checking-enabled-p (xw :rflags nil val x86))
             (alignment-checking-enabled-p x86))))

Theorem: alignment-checking-enabled-p-and-xw-seg-visible

(defthm alignment-checking-enabled-p-and-xw-seg-visible
 (implies
  (case-split
   (or
    (not (equal index 1))
    (and (equal index 1)
         (equal (segment-selectorbits->rpl val)
                (segment-selectorbits->rpl (seg-visiblei 1 x86))))))
  (equal
      (alignment-checking-enabled-p (xw :seg-visible index val x86))
      (alignment-checking-enabled-p x86))))

Theorem: alignment-checking-enabled-p-and-mv-nth-1-wb

(defthm alignment-checking-enabled-p-and-mv-nth-1-wb
 (equal
     (alignment-checking-enabled-p (mv-nth 1 (wb n addr w val x86)))
     (alignment-checking-enabled-p x86)))

Theorem: alignment-checking-enabled-p-and-mv-nth-2-rb

(defthm alignment-checking-enabled-p-and-mv-nth-2-rb
  (equal
       (alignment-checking-enabled-p (mv-nth 2 (rb n addr r-x x86)))
       (alignment-checking-enabled-p x86)))

Theorem: alignment-checking-enabled-p-and-mv-nth-2-las-to-pas

(defthm alignment-checking-enabled-p-and-mv-nth-2-las-to-pas
  (equal (alignment-checking-enabled-p
              (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))
         (alignment-checking-enabled-p x86)))