|
|
|---|
|
|
|
|---|
Double-precision shift left or right.
(x86-shld/shrd proc-mode start-rip temp-rip
prefixes rex-byte opcode modr/m sib x86)
→
x86
Op/En: MRI
0F A4: SHLD r/m16, r16, imm8
0F A4: SHLD r/m32, r32, imm8
0F A4: SHLD r/m64, r64, imm8
Op/En: MRC
0F A5: SHLD r/m16, r16, CL
0F A5: SHLD r/m32, r32, CL
0F A5: SHLD r/m64, r64, CL
Op/En: MRI
0F AC: SHRD r/m16, r16, imm8
0F AC: SHRD r/m32, r32, imm8
0F AC: SHRD r/m64, r64, imm8
Op/En: MRC
0F AD: SHRD r/m16, r16, CL
0F AD: SHRD r/m32, r32, CL
0F AD: SHRD r/m64, r64, CL
Function:
(defun x86-shld/shrd (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-shld/shrd)) (declare (ignorable __function__)) (b* ((?ctx 'x86-shld/shrd) (?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 2 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 dst-value increment-rip-by dst-addr x86) (x86-operand-from-modr/m-and-sib-bytes proc-mode 0 operand-size inst-ac? nil seg-reg p4? temp-rip rex-byte r/m mod sib 1 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 flg)) (src-value (rgfi-size operand-size (reg-index reg rex-byte 2) rex-byte x86)) ((mv flg count x86) (case opcode ((164 172) (rme-size-opt proc-mode 1 temp-rip 1 :x nil x86)) ((165 173) (mv nil (rr08 *rcx* rex-byte x86) x86)) (otherwise (mv nil 0 x86)))) ((when flg) (!!ms-fresh :rme-size-error flg)) ((mv flg (the (signed-byte 48) temp-rip)) (case opcode ((164 172) (add-to-*ip proc-mode temp-rip 1 x86)) ((165 173) (mv nil temp-rip)) (otherwise (mv nil 0)))) ((when flg) (!!ms-fresh :rip-increment-error flg)) (badlength? (check-instruction-length start-rip temp-rip 0)) ((when badlength?) (!!fault-fresh :gp 0 :instruction-length badlength?)) (count-mask (if (logbitp 3 rex-byte) 63 31)) (count (logand count-mask count)) (input-rflags (the (unsigned-byte 32) (rflags x86))) ((mv result result-undefined? (the (unsigned-byte 32) output-rflags) (the (unsigned-byte 32) undefined-flags)) (case opcode ((164 165) (shld-spec operand-size dst-value src-value count input-rflags)) ((172 173) (shrd-spec operand-size dst-value src-value count input-rflags)) (otherwise (mv 0 nil 0 0)))) ((mv result x86) (if result-undefined? (undef-read x86) (mv result x86))) (x86 (write-user-rflags output-rflags undefined-flags x86)) ((mv flg x86) (x86-operand-to-reg/mem proc-mode operand-size inst-ac? nil (trunc operand-size result) seg-reg dst-addr rex-byte r/m mod x86)) ((when flg) (!!ms-fresh :x86-operand-to-reg/mem flg)) (x86 (write-*ip proc-mode temp-rip x86))) x86))))
Theorem:
(defthm x86p-of-x86-shld/shrd (implies (x86p x86) (b* ((x86 (x86-shld/shrd proc-mode start-rip temp-rip prefixes rex-byte opcode modr/m sib x86))) (x86p x86))) :rule-classes :rewrite)