(x86-loop proc-mode start-rip temp-rip prefixes rex-byte opcode modr/m sib x86) → x86
Function:
(defun x86-loop (proc-mode start-rip temp-rip prefixes rex-byte opcode modr/m sib x86) (declare (xargs :stobjs (x86))) (declare (type (integer 0 4) proc-mode) (type (signed-byte 48) start-rip) (type (signed-byte 48) temp-rip) (type (unsigned-byte 52) prefixes) (type (unsigned-byte 8) rex-byte) (type (unsigned-byte 8) opcode) (type (unsigned-byte 8) modr/m) (type (unsigned-byte 8) sib)) (declare (ignorable proc-mode start-rip temp-rip prefixes rex-byte opcode modr/m sib)) (declare (xargs :guard (and (prefixes-p prefixes) (modr/m-p modr/m) (sib-p sib) (rip-guard-okp proc-mode temp-rip)))) (let ((__function__ 'x86-loop)) (declare (ignorable __function__)) (b* ((?ctx 'x86-loop)) (b* ((badlength? (check-instruction-length start-rip temp-rip 1)) ((when badlength?) (!!fault-fresh :gp 0 :instruction-length badlength?)) (p4? (equal 103 (prefixes->adr prefixes))) ((the (integer 2 8) counter-size) (select-address-size proc-mode p4? x86)) (counter (rgfi-size counter-size *rcx* rex-byte x86)) (counter (trunc counter-size (1- counter))) ((the (unsigned-byte 1) zf) (flgi :zf x86)) (branch-cond (if (equal opcode 226) (not (equal counter 0)) (if (equal opcode 225) (and (equal zf 1) (not (equal counter 0))) (and (equal zf 0) (not (equal counter 0))))))) (if branch-cond (b* (((mv flg rel8 x86) (rime-size proc-mode 1 temp-rip 1 :x nil x86)) ((when flg) (!!ms-fresh :rime-size-error flg)) ((mv flg next-rip) (add-to-*ip proc-mode temp-rip (1+ rel8) x86)) ((when flg) (!!ms-fresh :rip-increment-error flg)) (x86 (!rgfi-size counter-size *rcx* counter rex-byte x86)) (x86 (write-*ip proc-mode next-rip x86))) x86) (b* (((mv flg next-rip) (add-to-*ip proc-mode temp-rip 1 x86)) ((when flg) (!!ms-fresh :rip-increment-error flg)) (x86 (!rgfi-size counter-size *rcx* counter rex-byte x86)) (x86 (write-*ip proc-mode next-rip x86))) x86))))))
Theorem:
(defthm x86p-of-x86-loop (implies (x86p x86) (b* ((x86 (x86-loop proc-mode start-rip temp-rip prefixes rex-byte opcode modr/m sib x86))) (x86p x86))) :rule-classes :rewrite)