Read
(read-string-from-memory ptr nbytes x86) → (mv * * x86)
Function:
(defun read-string-from-memory (ptr nbytes x86) (declare (xargs :stobjs (x86))) (declare (type (signed-byte 49) ptr) (type (signed-byte 48) nbytes)) (declare (xargs :guard (and (integerp nbytes) (<= 0 nbytes) (integerp ptr) (<= (- *2^47*) ptr) (< (+ ptr nbytes) *2^47*)))) (let ((__function__ 'read-string-from-memory)) (declare (ignorable __function__)) (b* (((mv flg bytes x86) (read-bytes-from-memory ptr nbytes x86 nil)) ((when flg) (mv flg "nil" x86)) (charlist (bytes-to-charlist bytes))) (mv nil (coerce charlist 'string) x86))))
Theorem:
(defthm stringp-mv-nth-1-read-string-from-memory (implies (force (x86p x86)) (stringp (mv-nth 1 (read-string-from-memory ptr nbytes x86)))) :rule-classes :type-prescription)
Theorem:
(defthm x86p-mv-nth-2-read-string-from-memory (implies (x86p x86) (x86p (mv-nth 2 (read-string-from-memory ptr nbytes x86)))))