		Search-engine friendly clone of the ACL2 documentation.

State-stobj

Read1-instruction

Signature
(read1-instruction addr stat1 feat) → *

Definitions and Theorems

Function: read1-instruction

(defun read1-instruction (addr stat1 feat)
 (declare (xargs :stobjs (stat1)))
 (declare (xargs :guard (and (stat1p stat1)
                             (b* ((stat (stat-from-stat1 stat1)))
                               (and (integerp addr)
                                    (statp stat)
                                    (featp feat)
                                    (stat-validp stat feat))))))
 (let ((__function__ 'read1-instruction))
  (declare (ignorable __function__))
  (if
   (mbt (stat1p stat1))
   (b* ((stat (stat-from-stat1 stat1)))
    (let* ((addr (loghead (feat->xlen feat) addr)))
     (and (= (mod addr 4) 0)
          (let* ((b0 (read-memory-unsigned8 addr stat feat))
                 (b1 (read-memory-unsigned8 (+ addr 1)
                                            stat feat))
                 (b2 (read-memory-unsigned8 (+ addr 2)
                                            stat feat))
                 (b3 (read-memory-unsigned8 (+ addr 3)
                                            stat feat)))
            (logapp 8 b0
                    (logapp 8 b1 (logapp 8 b2 (logapp 8 b3 0))))))))
   0)))