|
|
|---|
|
|
|
|---|
(x86-stos proc-mode start-rip temp-rip
prefixes rex-byte opcode modr/m sib x86)
→
x86Function:
(defun x86-stos (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-stos)) (declare (ignorable __function__)) (b* ((?ctx 'x86-stos)) (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?)) (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/addr-size-2/4? (or (eql counter/addr-size 2) (eql counter/addr-size 4))) (counter (rgfi-size counter/addr-size 1 rex-byte x86)) ((when (and (equal group-1-prefix *repe*) (equal counter 0))) (write-*ip proc-mode temp-rip x86)) (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)) (select-byte-operand (equal 170 opcode)) ((the (integer 1 8) operand-size) (select-operand-size proc-mode select-byte-operand rex-byte nil prefixes nil nil nil x86)) (rax (rgfi-size operand-size 0 rex-byte x86)) (inst-ac? (alignment-checking-enabled-p x86)) ((mv flg0 x86) (wme-size proc-mode operand-size dst-addr 0 rax inst-ac? x86)) ((when flg0) (!!ms-fresh :wme-size-error flg0)) ((the (signed-byte 49) dst-addr) (case operand-size (1 (if (equal df 0) (+ 1 (the (signed-byte 48) dst-addr)) (+ -1 (the (signed-byte 48) dst-addr)))) (2 (if (equal df 0) (+ 2 (the (signed-byte 48) dst-addr)) (+ -2 (the (signed-byte 48) dst-addr)))) (4 (if (equal df 0) (+ 4 (the (signed-byte 48) dst-addr)) (+ -4 (the (signed-byte 48) dst-addr)))) (otherwise (if (equal df 0) (+ 8 (the (signed-byte 48) dst-addr)) (+ -8 (the (signed-byte 48) dst-addr)))))) (x86 (if (equal group-1-prefix *repe*) (!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 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-stos (implies (x86p x86) (b* ((x86 (x86-stos proc-mode start-rip temp-rip prefixes rex-byte opcode modr/m sib x86))) (x86p x86))) :rule-classes :rewrite)