		Search-engine friendly clone of the ACL2 documentation.

Initialize-x86-state

Load-program-into-memory

Loading a program into the model's memory.

Signature
(load-program-into-memory n64-bytes-lst x86) → (mv * x86)
Arguments: n64-bytes-lst — Required to be a n64p-byte-alistp.

load-program-into-memory expects a program represented in the form of a n64p-byte-alistp, and loads that program, byte-by-byte, into the model's memory. Obviously, this function is not efficient, but the speed with which we load a program into the memory has not yet proved to be a deal-breaker in our experiments so far.

Note on dealing with linear addresses emitted by GCC/LLVM:

GCC and LLVM might not always output addresses satisfying our definition of canonical-address-p (i.e., essentially i48p). These tools will output 64-bit addresses. Therefore, this function needs to be able to take a 64-bit address, check if it is canonical in the "real" world, and if so, convert it into a canonical address in our world.

if (canonical-address-p (n64-to-i64 address)) 
    address = (n64-to-i64 address) 
else 
    error!

Definitions and Theorems

Function: load-program-into-memory

(defun load-program-into-memory (n64-bytes-lst x86)
  (declare (xargs :stobjs (x86)))
  (declare (xargs :guard (n64p-byte-alistp n64-bytes-lst)))
  (let ((__function__ 'load-program-into-memory))
    (declare (ignorable __function__))
    (cond ((endp n64-bytes-lst) (mv nil x86))
          (t (b* ((n64-addr (caar n64-bytes-lst))
                  (byte (cdar n64-bytes-lst))
                  ((mv flg addr)
                   (let ((i48-addr (n64-to-i64 n64-addr)))
                     (if (canonical-address-p i48-addr)
                         (mv nil i48-addr)
                       (mv t n64-addr))))
                  ((when flg)
                   (mv (cons 'load-program-into-memory
                             'non-canonical-address)
                       x86))
                  ((mv flg x86) (wml08 addr byte x86))
                  ((when flg)
                   (mv (cons 'load-program-into-memory
                             'wml08-error)
                       x86)))
               (load-program-into-memory (cdr n64-bytes-lst)
                                         x86))))))

Theorem: x86p-mv-nth-1-load-program-into-memory

(defthm x86p-mv-nth-1-load-program-into-memory
 (implies
    (x86p x86)
    (x86p (mv-nth 1
                  (load-program-into-memory n64-program-lst x86)))))