		Search-engine friendly clone of the ACL2 documentation.

States

Read-xreg-signed

Read a signed integer from an x register.

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

We read an unsigned integer, and we convert it to signed according to XLEN.

This is a convenience operation, to interpret registers as signed, even though their representation in the state is always unsigned. Several instructions interpret registers as signed.

Definitions and Theorems

Function: read-xreg-signed

(defun read-xreg-signed (reg stat feat)
 (declare (xargs :guard (and (natp reg)
                             (statp stat)
                             (featp feat))))
 (declare
  (xargs
      :type-prescription (integerp (read-xreg-signed reg stat feat))
      :guard (and (stat-validp stat feat)
                  (< (lnfix reg) (feat->xnum feat)))))
 (let ((__function__ 'read-xreg-signed))
   (declare (ignorable __function__))
   (logext (feat->xlen feat)
           (read-xreg-unsigned reg stat feat))))

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

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

Theorem: sbyte32p-of-read-xreg-signed

(defthm sbyte32p-of-read-xreg-signed
  (implies (and (stat-validp stat feat)
                (feat-32p feat)
                (< (lnfix reg) (feat->xnum feat)))
           (b* ((?val (read-xreg-signed reg stat feat)))
             (sbyte32p val))))

Theorem: sbyte64p-of-read-xreg-signed

(defthm sbyte64p-of-read-xreg-signed
  (implies (and (stat-validp stat feat)
                (feat-64p feat)
                (< (lnfix reg) (feat->xnum feat)))
           (b* ((?val (read-xreg-signed reg stat feat)))
             (sbyte64p val))))

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

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

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

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

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

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

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

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

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

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

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

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