		Search-engine friendly clone of the ACL2 documentation.

States

Read-xreg-unsigned32

Read an unsigned 32-bit integer from a 64-bit x register.

Signature
(read-xreg-unsigned32 reg stat feat) → val
Arguments: reg — Guard (natp reg).; stat — Guard (statp stat).; feat — Guard (featp feat).
Returns: val — Type (ubyte32p val).

This is only defined when XLEN is 64; when it is 32, read-xreg-unsigned already returns a 32-bit integer. When XLEN is 64, several instructions read the low 32 bits of a register; so it is useful to introduce this abbreviation, which reads the whole integer and keeps the low 32 bits.

Definitions and Theorems

Function: read-xreg-unsigned32

(defun read-xreg-unsigned32 (reg stat feat)
 (declare (xargs :guard (and (natp reg)
                             (statp stat)
                             (featp feat))))
 (declare
  (xargs
      :type-prescription (natp (read-xreg-unsigned32 reg stat feat))
      :guard (and (stat-validp stat feat)
                  (feat-64p feat)
                  (< (lnfix reg) (feat->xnum feat)))))
 (let ((__function__ 'read-xreg-unsigned32))
   (declare (ignorable __function__))
   (loghead 32 (read-xreg-unsigned reg stat feat))))

Theorem: ubyte32p-of-read-xreg-unsigned32

(defthm ubyte32p-of-read-xreg-unsigned32
  (b* ((val (read-xreg-unsigned32 reg stat feat)))
    (ubyte32p val))
  :rule-classes :rewrite)

Theorem: read-xreg-unsigned32-of-nfix-reg

(defthm read-xreg-unsigned32-of-nfix-reg
  (equal (read-xreg-unsigned32 (nfix reg)
                               stat feat)
         (read-xreg-unsigned32 reg stat feat)))

Theorem: read-xreg-unsigned32-nat-equiv-congruence-on-reg

(defthm read-xreg-unsigned32-nat-equiv-congruence-on-reg
  (implies (acl2::nat-equiv reg reg-equiv)
           (equal (read-xreg-unsigned32 reg stat feat)
                  (read-xreg-unsigned32 reg-equiv stat feat)))
  :rule-classes :congruence)

Theorem: read-xreg-unsigned32-of-stat-fix-stat

(defthm read-xreg-unsigned32-of-stat-fix-stat
  (equal (read-xreg-unsigned32 reg (stat-fix stat)
                               feat)
         (read-xreg-unsigned32 reg stat feat)))

Theorem: read-xreg-unsigned32-stat-equiv-congruence-on-stat

(defthm read-xreg-unsigned32-stat-equiv-congruence-on-stat
  (implies (stat-equiv stat stat-equiv)
           (equal (read-xreg-unsigned32 reg stat feat)
                  (read-xreg-unsigned32 reg stat-equiv feat)))
  :rule-classes :congruence)

Theorem: read-xreg-unsigned32-of-feat-fix-feat

(defthm read-xreg-unsigned32-of-feat-fix-feat
  (equal (read-xreg-unsigned32 reg stat (feat-fix feat))
         (read-xreg-unsigned32 reg stat feat)))

Theorem: read-xreg-unsigned32-feat-equiv-congruence-on-feat

(defthm read-xreg-unsigned32-feat-equiv-congruence-on-feat
  (implies (feat-equiv feat feat-equiv)
           (equal (read-xreg-unsigned32 reg stat feat)
                  (read-xreg-unsigned32 reg stat feat-equiv)))
  :rule-classes :congruence)