		Search-engine friendly clone of the ACL2 documentation.

States

Read-xreg-signed32

Read a signed 32-bit integer from a 64-bit x register.

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

This is similar to read-xreg-unsigned32 in purpose, but it is useful when the 32 bits of the register are treated as a signed integer instead of unsigned.

Definitions and Theorems

Function: read-xreg-signed32

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

Theorem: sbyte32p-of-read-xreg-signed32

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

Theorem: read-xreg-signed32-of-x0

(defthm read-xreg-signed32-of-x0
  (equal (read-xreg-signed32 0 stat feat)
         0))

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

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

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

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

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

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

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

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

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

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

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

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