(x86-cmps proc-mode start-rip temp-rip prefixes rex-byte opcode modr/m sib x86) → x86
Function:
(defun x86-cmps (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-cmps)) (declare (ignorable __function__)) (b* ((?ctx 'x86-cmps) (?r/m (the (unsigned-byte 3) (modr/m->r/m modr/m))) (?mod (the (unsigned-byte 2) (modr/m->mod modr/m))) (?reg (the (unsigned-byte 3) (modr/m->reg modr/m)))) (b* ((group-1-prefix (the (unsigned-byte 8) (prefixes->rep prefixes))) (badlength? (check-instruction-length start-rip temp-rip 0)) ((when badlength?) (!!fault-fresh :gp 0 :instruction-length badlength?)) (p2 (the (unsigned-byte 8) (prefixes->seg prefixes))) (p4? (equal 103 (the (unsigned-byte 8) (prefixes->adr prefixes)))) ((the (unsigned-byte 1) df) (flgi :df x86)) ((the (integer 2 8) counter/addr-size) (select-address-size proc-mode p4? x86)) (counter (rgfi-size counter/addr-size 1 rex-byte x86)) ((when (and (equal group-1-prefix 243) (equal counter 0))) (write-*ip proc-mode temp-rip x86)) (select-byte-operand (equal 166 opcode)) ((the (integer 1 8) operand-size) (select-operand-size proc-mode select-byte-operand rex-byte nil prefixes nil nil nil x86)) (counter/addr-size-2/4? (or (eql counter/addr-size 2) (eql counter/addr-size 4))) (src-addr (if counter/addr-size-2/4? (rgfi-size counter/addr-size 6 rex-byte x86) (rgfi 6 x86))) ((when (and (not counter/addr-size-2/4?) (not (canonical-address-p src-addr)))) (!!ms-fresh :src-addr-not-canonical src-addr)) (inst-ac? (alignment-checking-enabled-p x86)) (seg-reg (select-segment-register proc-mode p2 p4? mod r/m sib x86)) ((mv flg0 src x86) (rme-size-opt proc-mode operand-size src-addr seg-reg :r inst-ac? x86)) ((when flg0) (!!ms-fresh :src-rme-size-error flg0)) (dst-addr (if counter/addr-size-2/4? (rgfi-size counter/addr-size 7 rex-byte x86) (rgfi 7 x86))) ((when (and (not counter/addr-size-2/4?) (not (canonical-address-p dst-addr)))) (!!ms-fresh :dst-addr-not-canonical dst-addr)) ((mv flg0 dst x86) (rme-size-opt proc-mode operand-size dst-addr 0 :r inst-ac? x86)) ((when flg0) (!!ms-fresh :dst-rme-size-error flg0)) ((the (unsigned-byte 32) input-rflags) (rflags x86)) ((mv ?result (the (unsigned-byte 32) output-rflags) (the (unsigned-byte 32) undefined-flags)) (gpr-arith/logic-spec operand-size 4 dst src input-rflags)) (x86 (write-user-rflags output-rflags undefined-flags x86)) ((mv (the (signed-byte 49) src-addr) (the (signed-byte 49) dst-addr)) (case operand-size (1 (if (equal df 0) (mv (+ (the (signed-byte 48) src-addr) 1) (+ (the (signed-byte 48) dst-addr) 1)) (mv (- (the (signed-byte 48) src-addr) 1) (- (the (signed-byte 48) dst-addr) 1)))) (2 (if (equal df 0) (mv (+ (the (signed-byte 48) src-addr) 2) (+ (the (signed-byte 48) dst-addr) 2)) (mv (- (the (signed-byte 48) src-addr) 2) (- (the (signed-byte 48) dst-addr) 2)))) (4 (if (equal df 0) (mv (+ (the (signed-byte 48) src-addr) 4) (+ (the (signed-byte 48) dst-addr) 4)) (mv (- (the (signed-byte 48) src-addr) 4) (- (the (signed-byte 48) dst-addr) 4)))) (otherwise (if (equal df 0) (mv (+ (the (signed-byte 48) src-addr) 8) (+ (the (signed-byte 48) dst-addr) 8)) (mv (- (the (signed-byte 48) src-addr) 8) (- (the (signed-byte 48) dst-addr) 8)))))) (x86 (if (equal group-1-prefix 243) (!rgfi-size counter/addr-size 1 (1- counter) rex-byte x86) (write-*ip proc-mode temp-rip x86))) (x86 (case counter/addr-size (2 (!rgfi-size 2 6 (n16 (the (signed-byte 49) src-addr)) rex-byte x86)) (4 (!rgfi-size 4 6 (n32 (the (signed-byte 49) src-addr)) rex-byte x86)) (t (!rgfi 6 (the (signed-byte 49) src-addr) x86)))) (x86 (case counter/addr-size (2 (!rgfi-size 2 7 (n16 (the (signed-byte 49) dst-addr)) rex-byte x86)) (4 (!rgfi-size 4 7 (n32 (the (signed-byte 49) dst-addr)) rex-byte x86)) (t (!rgfi 7 (the (signed-byte 49) dst-addr) x86))))) x86))))
Theorem:
(defthm x86p-of-x86-cmps (implies (x86p x86) (b* ((x86 (x86-cmps proc-mode start-rip temp-rip prefixes rex-byte opcode modr/m sib x86))) (x86p x86))) :rule-classes :rewrite)