|
|
|---|
|
|
|
|---|
(x86-fxrstor/fxrstor64 proc-mode start-rip temp-rip
prefixes rex-byte opcode modr/m sib x86)
→
x86Function:
(defun x86-fxrstor/fxrstor64 (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-fxrstor/fxrstor64)) (declare (ignorable __function__)) (b* ((?ctx 'x86-fxrstor/fxrstor64) (?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* ((p2 (prefixes->seg prefixes)) (p4? (equal 103 (prefixes->adr prefixes))) ((the (integer 1 8) operand-size) (select-operand-size proc-mode nil rex-byte nil prefixes nil nil nil x86)) (seg-reg (select-segment-register proc-mode p2 p4? mod r/m sib x86)) (inst-ac? t) ((mv flg & (the (unsigned-byte 3) increment-rip-by) (the (signed-byte 64) src-addr) x86) (x86-operand-from-modr/m-and-sib-bytes proc-mode 0 operand-size inst-ac? t seg-reg p4? temp-rip rex-byte r/m mod sib 0 x86)) ((when flg) (!!ms-fresh :x86-operand-from-modr/m-and-sib-bytes flg)) ((mv flg (the (signed-byte 48) temp-rip)) (add-to-*ip proc-mode temp-rip increment-rip-by x86)) ((when flg) (!!ms-fresh :rip-increment-error temp-rip)) ((unless (signed-byte-p 64 (+ 512 src-addr -1))) (!!ms-fresh :fxrstor-address-overflow)) ((mv flg fp-ctrl x86) (rme16 proc-mode src-addr seg-reg :r inst-ac? x86)) ((when flg) (!!ms-fresh :rme16 proc-mode flg)) (x86 (!fp-ctrl fp-ctrl x86)) ((mv flg fp-status x86) (rme16 proc-mode (+ 2 src-addr) seg-reg :r inst-ac? x86)) ((when flg) (!!ms-fresh :rme16 proc-mode flg)) (x86 (!fp-status fp-status x86)) ((mv flg ftw x86) (rme08 proc-mode (+ 4 src-addr) seg-reg :r x86)) ((when flg) (!!ms-fresh :rme08 proc-mode flg)) ((mv flg fp-opcode x86) (rme16 proc-mode (+ 6 src-addr) seg-reg :r inst-ac? x86)) ((when flg) (!!ms-fresh :rme16 proc-mode flg)) (x86 (!fp-opcode (loghead 11 fp-opcode) x86)) ((mv flg fp-last-inst x86) (rme32 proc-mode (+ 8 src-addr) seg-reg :r inst-ac? x86)) ((when flg) (!!ms-fresh :rme32 proc-mode flg)) (x86 (!fp-last-inst fp-last-inst x86)) ((mv flg fp-last-data x86) (rme32 proc-mode (+ 16 src-addr) seg-reg :r inst-ac? x86)) ((when flg) (!!ms-fresh :rme32 proc-mode flg)) (x86 (!fp-last-data fp-last-data x86)) ((mv flg mxcsr x86) (rme32 proc-mode (+ 24 src-addr) seg-reg :r inst-ac? x86)) ((when flg) (!!ms-fresh :rme32 proc-mode flg)) ((mv flg mxcsr-mask x86) (rme32 proc-mode (+ 28 src-addr) seg-reg :r inst-ac? x86)) ((when flg) (!!ms-fresh :rme32 proc-mode flg)) (mxcsr-mask (if (equal mxcsr-mask 0) 65471 mxcsr-mask)) (mxcsr (logand mxcsr mxcsr-mask)) ((when (not (equal (logand mxcsr 4294901760) 0))) (!!fault-fresh :gp 0 :mxcsr-error mxcsr)) (x86 (!mxcsr mxcsr x86)) ((mv flg x86) (read-mm-regs proc-mode inst-ac? seg-reg 0 (+ 32 src-addr) 8 x86)) ((when flg) x86) (x86 (set-fp-tag ftw x86)) ((mv flg x86) (read-xmm-regs proc-mode inst-ac? seg-reg 0 (+ 160 src-addr) (if (equal proc-mode *64-bit-mode*) 16 8) x86)) ((when flg) x86)) (write-*ip proc-mode temp-rip x86)))))
Theorem:
(defthm x86p-of-x86-fxrstor/fxrstor64 (implies (x86p x86) (b* ((x86 (x86-fxrstor/fxrstor64 proc-mode start-rip temp-rip prefixes rex-byte opcode modr/m sib x86))) (x86p x86))) :rule-classes :rewrite)