|
|
|---|
|
|
|
|---|
(x86-div proc-mode start-rip temp-rip
prefixes rex-byte opcode modr/m sib x86)
→
x86F6/6:
DIV r/m8: (AX div r/m8), AH := Remainder, AL := Quotient
F7/6:
DIV r/m16: (DX:AX div r/m16), DX := Remainder, AX := Quotient
DIV r/m32: (EDX:EAX div r/m8), EDX := Remainder, EAX := Quotient
DIV r/m64: (RDX:RAX div r/m8), RDX := Remainder, RAX := Quotient
Function:
(defun x86-div (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) (equal (modr/m->reg modr/m) 6)))) (let ((__function__ 'x86-div)) (declare (ignorable __function__)) (b* ((?ctx 'x86-div) (?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))) (select-byte-operand (equal opcode 246)) ((the (integer 1 8) reg/mem-size) (select-operand-size proc-mode select-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) (the (signed-byte 64) ?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 0 x86)) ((when flg0) (!!ms-fresh :x86-operand-from-modr/m-and-sib-bytes flg0)) ((when (equal reg/mem 0)) (!!fault-fresh :de nil :de-exception-source-operand-zero reg/mem)) ((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)) (badlength? (check-instruction-length start-rip temp-rip 0)) ((when badlength?) (!!fault-fresh :gp 0 :instruction-length badlength?)) (rax (rgfi-size (if select-byte-operand 2 reg/mem-size) *rax* rex-byte x86)) (rdx (if select-byte-operand 0 (rgfi-size reg/mem-size *rdx* rex-byte x86))) (dividend (if select-byte-operand rax (mbe :logic (part-install rdx rax :low (ash reg/mem-size 3) :width (ash reg/mem-size 3)) :exec (logior (ash rdx (ash reg/mem-size 3)) rax)))) ((mv overflow? quotient remainder) (div-spec reg/mem-size dividend reg/mem)) ((when overflow?) (!!ms-fresh :unsigned-divide-error-overflow (cons 'dividend dividend) (cons 'divisor reg/mem))) (x86 (case reg/mem-size (1 (let* ((result (mbe :logic (part-install remainder quotient :low 8 :width 8) :exec (logior (ash (the (unsigned-byte 8) remainder) 8) (the (unsigned-byte 8) quotient)))) (x86 (!rgfi-size 2 *rax* result rex-byte x86))) x86)) (otherwise (let* ((x86 (!rgfi-size reg/mem-size *rax* quotient rex-byte x86)) (x86 (!rgfi-size reg/mem-size *rdx* remainder rex-byte x86))) x86)))) (x86 (!flgi-undefined :cf x86)) (x86 (!flgi-undefined :pf x86)) (x86 (!flgi-undefined :af x86)) (x86 (!flgi-undefined :zf x86)) (x86 (!flgi-undefined :sf x86)) (x86 (!flgi-undefined :of x86)) (x86 (write-*ip proc-mode temp-rip x86))) x86))))
Theorem:
(defthm x86p-of-x86-div (implies (x86p x86) (b* ((x86 (x86-div proc-mode start-rip temp-rip prefixes rex-byte opcode modr/m sib x86))) (x86p x86))) :rule-classes :rewrite)