		Search-engine friendly clone of the ACL2 documentation.

States

Read-xreg-unsigned

Read an unsigned integer from an x register.

Signature
(read-xreg-unsigned reg stat feat) → val
Arguments: reg — Guard (natp reg).; stat — Guard (statp stat).; feat — Guard (featp feat).
Returns: val — Type (unsigned-byte-p (feat->xlen feat) val).

The index must be less than the number n of registers, so that the registers x0 to x<n> can be indexed. The result is a natural number in general; additionally, based on XLEN, it consists of either 32 or 64 bits.

As explained in stat, x0 is not modeled explicitly, since it is hardwired to 0. Thus, the 0 index is treated separately; the other cases are handled by decrementing the index by 1.

Definitions and Theorems

Function: read-xreg-unsigned

(defun read-xreg-unsigned (reg stat feat)
  (declare (xargs :guard (and (natp reg)
                              (statp stat)
                              (featp feat))))
  (declare (xargs :guard (and (stat-validp stat feat)
                              (< (lnfix reg) (feat->xnum feat)))))
  (let ((__function__ 'read-xreg-unsigned))
    (declare (ignorable __function__))
    (b* ((reg (lnfix reg)))
      (if (= reg 0)
          0
        (unsigned-byte-fix (feat->xlen feat)
                           (nth (1- reg) (stat->xregs stat)))))))

Theorem: return-type-of-read-xreg-unsigned

(defthm return-type-of-read-xreg-unsigned
  (b* ((val (read-xreg-unsigned reg stat feat)))
    (unsigned-byte-p (feat->xlen feat) val))
  :rule-classes :rewrite)

Theorem: ubyte32p-of-read-xreg-unsigned

(defthm ubyte32p-of-read-xreg-unsigned
  (implies (and (stat-validp stat feat)
                (feat-bits-case (feat->bits feat) :|32|)
                (< (lnfix reg) (feat->xnum feat)))
           (b* ((?val (read-xreg-unsigned reg stat feat)))
             (ubyte32p val))))

Theorem: ubyte64p-of-read-xreg-unsigned

(defthm ubyte64p-of-read-xreg-unsigned
  (implies (and (stat-validp stat feat)
                (feat-bits-case (feat->bits feat) :|64|)
                (< (lnfix reg) (feat->xnum feat)))
           (b* ((?val (read-xreg-unsigned reg stat feat)))
             (ubyte64p val))))

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

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

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

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

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

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

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

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

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

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

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

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