		Search-engine friendly clone of the ACL2 documentation.

States32

Write32-pc

Write the program counter.

Signature
(write32-pc pc stat) → new-stat
Arguments: pc — Guard (integerp pc).; stat — Guard (stat32ip stat).
Returns: new-stat — Type (stat32ip new-stat).

The value is any integer, signed or unsigned, which is converted to an unsigned 32-bit integer by keeping its low 32 bits.

The fact that the value to write is any integer is handy for callers, who can just pass the integer (e.g. the exact result of an operation) and let this writer function convert the integer for the register. [ISA:1.4] says that address computations wrap round ignoring overflow, i.e. the last address in the address space is adjacent to address 0.

Definitions and Theorems

Function: write32-pc

(defun write32-pc (pc stat)
  (declare (xargs :guard (and (integerp pc) (stat32ip stat))))
  (let ((__function__ 'write32-pc))
    (declare (ignorable __function__))
    (change-stat32i stat
                    :pc (loghead 32 pc))))

Theorem: stat32ip-of-write32-pc

(defthm stat32ip-of-write32-pc
  (b* ((new-stat (write32-pc pc stat)))
    (stat32ip new-stat))
  :rule-classes :rewrite)

Theorem: write32-pc-of-ifix-pc

(defthm write32-pc-of-ifix-pc
  (equal (write32-pc (ifix pc) stat)
         (write32-pc pc stat)))

Theorem: write32-pc-int-equiv-congruence-on-pc

(defthm write32-pc-int-equiv-congruence-on-pc
  (implies (acl2::int-equiv pc pc-equiv)
           (equal (write32-pc pc stat)
                  (write32-pc pc-equiv stat)))
  :rule-classes :congruence)

Theorem: write32-pc-of-stat32i-fix-stat

(defthm write32-pc-of-stat32i-fix-stat
  (equal (write32-pc pc (stat32i-fix stat))
         (write32-pc pc stat)))

Theorem: write32-pc-stat32i-equiv-congruence-on-stat

(defthm write32-pc-stat32i-equiv-congruence-on-stat
  (implies (stat32i-equiv stat stat-equiv)
           (equal (write32-pc pc stat)
                  (write32-pc pc stat-equiv)))
  :rule-classes :congruence)