		Search-engine friendly clone of the ACL2 documentation.

States

Read-pc

Read the program counter.

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

The result is always an unsigned XLEN-bit integer, which is an address in memory; recall that the memory address space goes from 0 to 2^XLEN - 1, as explained in stat.

Definitions and Theorems

Function: read-pc

(defun read-pc (stat feat)
  (declare (xargs :guard (and (statp stat) (featp feat))))
  (declare (xargs :guard (stat-validp stat feat)))
  (let ((__function__ 'read-pc))
    (declare (ignorable __function__))
    (unsigned-byte-fix (feat->xlen feat)
                       (stat->pc stat))))

Theorem: return-type-of-read-pc

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

Theorem: natp-of-read-pc

(defthm natp-of-read-pc
  (b* ((pc (read-pc stat feat)))
    (natp pc))
  :rule-classes :type-prescription)

Theorem: ubyte32p-of-read-pc

(defthm ubyte32p-of-read-pc
  (implies (and (stat-validp stat feat)
                (feat-32p feat))
           (b* ((acl2::?pc (read-pc stat feat)))
             (ubyte32p pc))))

Theorem: ubyte64p-of-read-pc

(defthm ubyte64p-of-read-pc
  (implies (and (stat-validp stat feat)
                (feat-64p feat))
           (b* ((acl2::?pc (read-pc stat feat)))
             (ubyte64p pc))))

Theorem: read-pc-of-stat-fix-stat

(defthm read-pc-of-stat-fix-stat
  (equal (read-pc (stat-fix stat) feat)
         (read-pc stat feat)))

Theorem: read-pc-stat-equiv-congruence-on-stat

(defthm read-pc-stat-equiv-congruence-on-stat
  (implies (stat-equiv stat stat-equiv)
           (equal (read-pc stat feat)
                  (read-pc stat-equiv feat)))
  :rule-classes :congruence)

Theorem: read-pc-of-feat-fix-feat

(defthm read-pc-of-feat-fix-feat
  (equal (read-pc stat (feat-fix feat))
         (read-pc stat feat)))

Theorem: read-pc-feat-equiv-congruence-on-feat

(defthm read-pc-feat-equiv-congruence-on-feat
  (implies (feat-equiv feat feat-equiv)
           (equal (read-pc stat feat)
                  (read-pc stat feat-equiv)))
  :rule-classes :congruence)