		Search-engine friendly clone of the ACL2 documentation.

Linear-memory

Program-at

Predicate that makes a statement about a program's location in the memory

Signature
(program-at prog-addr bytes x86) → *

We use program-at to state that a program, given by as a list of bytes, is located at contiguous addresses from prog-addr to (len bytes) + prog-addr - 1 in the memory of the x86 state. Note that this function is non-executable; we use it only for reasoning about machine-code.

Definitions and Theorems

Function: program-at

(defun program-at (prog-addr bytes x86)
 (declare (xargs :stobjs (x86)))
 (declare
  (xargs
      :guard (and (canonical-address-p prog-addr)
                  (canonical-address-p (+ -1 (len bytes) prog-addr))
                  (byte-listp bytes))
      :non-executable t))
 (prog2$ (acl2::throw-nonexec-error 'program-at
                                    (list prog-addr bytes x86))
         (let ((__function__ 'program-at))
           (declare (ignorable __function__))
           (b* (((mv flg bytes-read ?x86)
                 (rb (len bytes) prog-addr :x x86)))
             (and (equal flg nil)
                  (equal bytes-read
                         (combine-n-bytes 0 (len bytes)
                                          bytes)))))))

Theorem: program-at-xw-in-app-view

(defthm program-at-xw-in-app-view
  (implies (and (app-view x86)
                (not (equal fld :mem))
                (not (equal fld :app-view)))
           (equal (program-at addr bytes (xw fld index value x86))
                  (program-at addr bytes x86))))