		Search-engine friendly clone of the ACL2 documentation.

Linear-memory

Write-canonical-address-to-memory

Signature
(write-canonical-address-to-memory lin-addr canonical-address x86) → (mv * x86)

Definitions and Theorems

Function: write-canonical-address-to-memory

(defun write-canonical-address-to-memory
       (lin-addr canonical-address x86)
  (declare (xargs :stobjs (x86)))
  (declare (type (signed-byte 48) lin-addr)
           (type (signed-byte 48)
                 canonical-address))
  (let ((__function__ 'write-canonical-address-to-memory))
    (declare (ignorable __function__))
    (let* ((7+lin-addr (the (signed-byte 50) (+ 7 lin-addr))))
      (if (mbe :logic (canonical-address-p 7+lin-addr)
               :exec (< (the (signed-byte 50) 7+lin-addr)
                        140737488355328))
          (if (app-view x86)
              (mbe :logic (wb 8 lin-addr
                              :w (loghead 64 canonical-address)
                              x86)
                   :exec (write-canonical-address-to-memory-user-exec
                              lin-addr canonical-address x86))
            (b* ((canonical-address-unsigned-val
                      (mbe :logic (loghead 64 canonical-address)
                           :exec (logand 18446744073709551615
                                         canonical-address))))
              (wml64 lin-addr
                     canonical-address-unsigned-val x86)))
        (mv 'write-canonical-address-to-memory-error
            x86)))))

Theorem: x86p-write-canonical-address-to-memory

(defthm x86p-write-canonical-address-to-memory
  (implies (force (x86p x86))
           (x86p (mv-nth 1
                         (write-canonical-address-to-memory
                              lin-addr canonical-address x86))))
  :rule-classes (:rewrite :type-prescription))