|
|
|---|
|
|
|
|---|
(x86-sal/sar/shl/shr/rcl/rcr/rol/ror
proc-mode start-rip temp-rip
prefixes rex-byte opcode modr/m sib x86)
→
x86
Op/En: MI
C0/0: ROL r/m8, imm8
C0/1: ROR r/m8, imm8
C0/2: RCL r/m8, imm8
C0/3: RCR r/m8, imm8
C0/4: SAL/SHL r/m8, imm8
C0/5: SHR r/m8, imm8
C0/7: SAR r/m8, imm8
C1/0: ROL r/m16/32/64, imm8
C1/1: ROR r/m16/32/64, imm8
C1/2: RCL r/m16/32/64, imm8
C1/3: RCR r/m16/32/64, imm8
C1/4: SAL/SHL r/m16/32/64, imm8
C1/5: SHR r/m16/32/64, imm8
C1/7: SAR r/m16/32/64. imm8
Op/En: M1
D0/0: ROL r/m8, 1
D0/1: ROR r/m8, 1
D0/2: RCL r/m8, 1
D0/3: RCR r/m8, 1
D0/4: SAL/SHL r/m8, 1
D0/5: SHR r/m8, 1
D0/7: SAR r/m8, 1
D1/0: ROL r/m16/32/64, 1
D1/1: ROR r/m16/32/64, 1
D1/2: RCL r/m16/32/64, 1
D1/3: RCR r/m16/32/64, 1
D1/4: SAL/SHL r/m16/32/64, 1
D1/5: SHR r/m16/32/64, 1
D1/7: SAR r/m16/32/64, 1
Op/En: MC
D2/0: ROL r/m8, CL
D2/1: ROR r/m8, CL
D2/2: RCL r/m8, CL
D2/3: RCR r/m8, CL
D2/4: SAL/SHL r/m8, CL
D2/5: SHR r/m8, CL
D2/7: SAR r/m8, CL
D3/0: ROL r/m16/32/64, CL
D3/1: ROR r/m16/32/64, CL
D3/2: RCL r/m16/32/64, CL
D3/3: RCR r/m16/32/64, CL
D3/4: SAL/SHL r/m16/32/64, CL
D3/5: SHR r/m16/32/64, CL
D3/7: SAR r/m16/32/64, CL
Function:
(defun x86-sal/sar/shl/shr/rcl/rcr/rol/ror (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) (not (equal (modr/m->reg modr/m) 6))))) (let ((__function__ 'x86-sal/sar/shl/shr/rcl/rcr/rol/ror)) (declare (ignorable __function__)) (b* ((?ctx 'x86-sal/sar/shl/shr/rcl/rcr/rol/ror) (?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))) (byte-operand? (or (equal opcode 192) (equal opcode 208) (equal opcode 210))) ((the (integer 0 8) ?reg/mem-size) (select-operand-size proc-mode byte-operand? 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 flg0 ?reg/mem (the (unsigned-byte 3) increment-rip-by) addr x86) (x86-operand-from-modr/m-and-sib-bytes proc-mode 0 reg/mem-size inst-ac? nil seg-reg p4? temp-rip rex-byte r/m mod sib (if (or (equal opcode 192) (equal opcode 193)) 1 0) x86)) ((when flg0) (!!ms-fresh :x86-operand-from-modr/m-and-sib-bytes flg0)) ((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)) ((mv flg1 shift/rotate-by x86) (case opcode ((208 209) (mv nil 1 x86)) ((210 211) (mv nil (rr08 *rcx* rex-byte x86) x86)) ((192 193) (rme-size-opt proc-mode 1 temp-rip 1 :x nil x86)) (otherwise (mv nil 0 x86)))) ((when flg1) (!!ms-fresh :rme-size-error flg1)) (countmask (if (logbitp 3 rex-byte) 63 31)) (shift/rotate-by (logand countmask shift/rotate-by)) ((mv flg (the (signed-byte 49) temp-rip)) (if (or (equal opcode 192) (equal opcode 193)) (add-to-*ip proc-mode temp-rip 1 x86) (mv nil temp-rip))) ((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?)) (input-rflags (the (unsigned-byte 32) (rflags x86))) ((mv result (the (unsigned-byte 32) output-rflags) (the (unsigned-byte 32) undefined-flags)) (case reg (0 (rol-spec reg/mem-size reg/mem shift/rotate-by input-rflags)) (1 (ror-spec reg/mem-size reg/mem shift/rotate-by input-rflags)) (2 (rcl-spec reg/mem-size reg/mem shift/rotate-by input-rflags)) (3 (rcr-spec reg/mem-size reg/mem shift/rotate-by input-rflags)) (4 (sal/shl-spec reg/mem-size reg/mem shift/rotate-by input-rflags)) (5 (shr-spec reg/mem-size reg/mem shift/rotate-by input-rflags)) (7 (sar-spec reg/mem-size reg/mem shift/rotate-by input-rflags)) (otherwise (mv 0 0 0)))) (x86 (write-user-rflags output-rflags undefined-flags x86)) ((mv flg2 x86) (x86-operand-to-reg/mem proc-mode reg/mem-size inst-ac? nil (trunc reg/mem-size result) seg-reg addr rex-byte r/m mod x86)) ((when flg2) (!!ms-fresh :x86-operand-to-reg/mem flg2)) (x86 (write-*ip proc-mode temp-rip x86))) x86))))
Theorem:
(defthm x86p-of-x86-sal/sar/shl/shr/rcl/rcr/rol/ror (implies (x86p x86) (b* ((x86 (x86-sal/sar/shl/shr/rcl/rcr/rol/ror proc-mode start-rip temp-rip prefixes rex-byte opcode modr/m sib x86))) (x86p x86))) :rule-classes :rewrite)