Read memory as bytes till a zero is encountered
(read-memory-zero-terminated ptr x86 acc) → (mv * * x86)
Returns a list of bytes (byte at the smallest address is the first byte of the list).
Function:
(defun read-memory-zero-terminated (ptr x86 acc) (declare (xargs :stobjs (x86))) (declare (type (signed-byte 49) ptr)) (declare (xargs :guard (and (integerp ptr) (<= (- *2^47*) ptr) (<= ptr *2^47*) (nat-listp acc)))) (let ((__function__ 'read-memory-zero-terminated)) (declare (ignorable __function__)) (if (signed-byte-p 48 ptr) (b* (((mv flg (the (unsigned-byte 8) mem-val) x86) (rml08 ptr :r x86)) ((when flg) (mv flg acc x86))) (if (equal 0 mem-val) (mv nil (append (reverse acc) '(0)) x86) (read-memory-zero-terminated (the (signed-byte 49) (1+ ptr)) x86 (cons mem-val acc)))) (mv t (reverse acc) x86))))
Theorem:
(defthm byte-listp-mv-nth-1-read-memory-zero-terminated (implies (and (x86p x86) (byte-listp acc)) (byte-listp (mv-nth 1 (read-memory-zero-terminated ptr x86 acc)))) :rule-classes :type-prescription)
Theorem:
(defthm x86p-mv-nth-2-read-memory-zero-terminated (implies (x86p x86) (x86p (mv-nth 2 (read-memory-zero-terminated ptr x86 acc)))))