(x86-syscall-link x86) → x86
Function:
(defun x86-syscall-link (x86) (declare (xargs :stobjs (x86))) (declare (xargs :guard t)) (let ((__function__ 'x86-syscall-link)) (declare (ignorable __function__)) (b* ((ctx 'x86-syscall-link) (old-path-ptr (rgfi *rdi* x86)) (new-path-ptr (rgfi *rsi* x86)) ((when (not (canonical-address-p old-path-ptr))) (!ms (list ctx :syscall-link-oldpath-ptr-overflow) x86)) ((mv flg old-path x86) (read-string-zero-terminated old-path-ptr x86)) ((when flg) (!ms (list ctx :old-path flg) x86)) ((when (not (canonical-address-p new-path-ptr))) (!ms (list ctx :syscall-link-newpath-ptr-overflow) x86)) ((mv flg new-path x86) (read-string-zero-terminated new-path-ptr x86)) ((when flg) (!ms (list ctx :new-path flg) x86)) ((mv ret x86) (syscall-link old-path new-path x86)) ((when (or (ms x86) (not (i64p ret)))) (!ms (list ctx :ret-val-or-ms-for-syscall-write ret) x86)) (x86 (!rgfi *rax* ret x86))) x86)))
Theorem:
(defthm x86p-of-x86-syscall-link (implies (and (x86p x86)) (b* ((x86 (x86-syscall-link x86))) (x86p x86))) :rule-classes :rewrite)