|
|
|---|
|
|
|
|---|
Refine read-mem64 to use the stobj states.
Function:
(defun read1-mem64{0} (addr stat feat) (declare (xargs :non-executable t)) (declare (xargs :guard (non-exec (and (stat1p stat) (integerp addr) (statp (stat-from-stat1 stat)) (featp feat) (stat-validp (stat-from-stat1 stat) feat))))) (prog2$ (acl2::throw-nonexec-error 'read1-mem64{0} (list addr stat feat)) (let ((feat1 (stat1p stat))) (cond ((acl2::mbt$ feat1) (let ((b0 (read-mem8 addr (stat-from-stat1 stat) feat)) (stat (stat-from-stat1 stat))) (let* ((b1 (read-mem8 (+ (lifix addr) 1) stat feat)) (b2 (read-mem8 (+ (lifix addr) 2) stat feat)) (b3 (read-mem8 (+ (lifix addr) 3) stat feat)) (b4 (read-mem8 (+ (lifix addr) 4) stat feat)) (b5 (read-mem8 (+ (lifix addr) 5) stat feat)) (b6 (read-mem8 (+ (lifix addr) 6) stat feat)) (b7 (read-mem8 (+ (lifix addr) 7) stat feat))) (cond ((feat-little-endianp feat) (logapp 8 b0 (logapp 8 b1 (logapp 8 b2 (logapp 8 b3 (logapp 8 b4 (logapp 8 b5 (logapp 8 b6 (logapp 8 b7 0))))))))) ((feat-big-endianp feat) (logapp 8 b7 (logapp 8 b6 (logapp 8 b5 (logapp 8 b4 (logapp 8 b3 (logapp 8 b2 (logapp 8 b1 (logapp 8 b0 0))))))))) (t (acl2::impossible-fn)))))) (t 0)))))
Theorem:
(defthm read1-mem64{0}-to-read-mem64 (implies (stat1p stat) (equal (read1-mem64{0} addr stat feat) (read-mem64 addr (stat-from-stat1 stat) feat))) :rule-classes :rewrite)
Theorem:
(defthm read-mem64-to-read1-mem64{0} (implies (statp stat) (equal (read-mem64 addr stat feat) (read1-mem64{0} addr (stat1-from-stat stat) feat))) :rule-classes :rewrite)