|
|
|---|
|
|
|
|---|
(x86-inc/dec-4x proc-mode start-rip temp-rip
prefixes rex-byte opcode modr/m sib x86)
→
x86Function:
(defun x86-inc/dec-4x (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-inc/dec-4x)) (declare (ignorable __function__)) (b* ((?ctx 'x86-inc/dec-4x)) (b* (((the (integer 2 4) operand-size) (select-operand-size proc-mode nil 0 nil prefixes nil nil nil x86)) (badlength? (check-instruction-length start-rip temp-rip 0)) ((when badlength?) (!!fault-fresh :gp 0 :instruction-length badlength?)) (reg (the (unsigned-byte 3) (logand 7 opcode))) (operand (rgfi-size operand-size reg 0 x86)) ((the (unsigned-byte 32) input-rflags) (rflags x86)) ((the (unsigned-byte 1) old-cf) (rflagsbits->cf input-rflags)) ((mv result output-rflags undefined-flags) (gpr-arith/logic-spec operand-size (if (logbitp 3 opcode) 4 0) operand 1 input-rflags)) (output-rflags (the (unsigned-byte 32) (!rflagsbits->cf old-cf output-rflags))) (x86 (write-user-rflags output-rflags undefined-flags x86)) (x86 (!rgfi-size operand-size reg result 0 x86)) (x86 (write-*ip proc-mode temp-rip x86))) x86))))
Theorem:
(defthm x86p-of-x86-inc/dec-4x (implies (x86p x86) (b* ((x86 (x86-inc/dec-4x proc-mode start-rip temp-rip prefixes rex-byte opcode modr/m sib x86))) (x86p x86))) :rule-classes :rewrite)