		Search-engine friendly clone of the ACL2 documentation.

Top-level-memory

Address-aligned-p

Check the alignment of a linear address.

Signature
(address-aligned-p addr operand-size memory-ptr?) → yes/no
Arguments: memory-ptr? — Guard (booleanp memory-ptr?).
Returns: yes/no — Type (booleanp yes/no).

Besides the address to check for alignment, this function takes as argument the operand size (from which the alignment to check is determined) and a flag indicating whether the address to check for alignment contains a memory operand of the form m16:16, m16:32, or m16:64 (see Intel manual, Mar'17, Volume 2, Section 3.1.1.3).

Words, doublewords, quadwords, and double quadwords must be aligned at boundaries of 2, 4, 8, or 16 bytes. Memory pointers of the form m16:xx must be aligned so that their xx portion is aligned as a word, doubleword, or quadword; this automatically guarantees that their m16 portion is aligned as a word. See Intel manual, Mar'17, Volume 1, Section 4.1.1. See AMD manual, Dec'17, Volume 2, Table 8-7 (note that the table does not mention explicitly memory pointers of the form m16:64).

If the operand size is 6, the operand must be an m16:32 pointer. If the operand size is 10, the operand must an m16:64 pointer. If the operand size is 4, it may be either an m16:16 pointer or not; in this case, the memory-ptr? argument is used to determine whether the address should be aligned at a word or doubleword boundary. If the operand size is 1, 2, 8, or 16, it cannot be a memory pointer of the form m16:xx.

Definitions and Theorems

Function: address-aligned-p$inline

(defun address-aligned-p$inline (addr operand-size memory-ptr?)
  (declare (type (signed-byte 48) addr)
           (type (member 1 2 4 6 8 10 16 32 64)
                 operand-size))
  (declare (xargs :guard (booleanp memory-ptr?)))
  (b* ((addr (the (signed-byte 48) addr))
       (operand-size (the (integer 0 65) operand-size)))
    (case operand-size
      (1 t)
      (6 (equal (logand addr 3) 0))
      (10 (equal (logand addr 7) 0))
      (otherwise
           (if (and memory-ptr? (eql operand-size 4))
               (equal (logand addr 1) 0)
             (equal (logand addr
                            (the (integer 0 65) (- operand-size 1)))
                    0))))))

Theorem: booleanp-of-address-aligned-p

(defthm booleanp-of-address-aligned-p
  (b*
    ((yes/no
          (address-aligned-p$inline addr operand-size memory-ptr?)))
    (booleanp yes/no))
  :rule-classes :type-prescription)

Theorem: memory-byte-accesses-are-always-aligned

(defthm memory-byte-accesses-are-always-aligned
  (equal (address-aligned-p addr 1 mem-ptr?)
         t))

Theorem: address-aligned-p-mem-ptr-input-irrelevant-for-all-but-bytes=4

(defthm
     address-aligned-p-mem-ptr-input-irrelevant-for-all-but-bytes=4
  (implies (and (syntaxp (not (equal mem-ptr? ''nil)))
                (not (equal nbytes 4)))
           (equal (address-aligned-p addr nbytes mem-ptr?)
                  (address-aligned-p addr nbytes nil))))