|
|
|---|
|
|
|
|---|
Absolute Indirect Jump: Far
(x86-far-jmp-op/en-d proc-mode start-rip temp-rip
prefixes rex-byte opcode modr/m sib x86)
→
x86Op/En: D
FF/5: JMP m16:16 or m16:32 or m16:64
Source: Intel Manuals (Vol. 2A) Instruction Set Reference: the text below has been edited to contain information only about the 64-bit mode.
The JMP instruction cannot be used to perform inter-privilege-level far jumps. The processor always uses the segment selector part of the far address to access the corresponding descriptor in the GDT or LDT. The descriptor type and access rights determine the type of jump to be performed.
Far Jump to a Conforming or Non-Conforming Code Segment: If the selected descriptor is for a code segment, a far jump to a code segment at the same privilege level is performed. If the selected code segment is at a different privilege level and the code segment is non-conforming, a general-protection exception is generated. The target operand specifies an absolute far address indirectly with a memory location (m16:16 or m16:32 or m16:64). The operand-size attribute and the REX.w bit determine the size of the offset (16 or 32 or 64 bits) in the far address. The new code segment selector and its descriptor are loaded into CS register, and the offset from the instruction is loaded into the RIP register.
Far Jump through a Call Gate: When executing a far jump through a call gate, the segment selector specified by the target operand identifies the call gate. The offset part of the target operand is ignored. The processor then jumps to the code segment specified in the call gate descriptor and begins executing the instruction at the offset specified in the call gate. No stack switch occurs. The target operand specifies the far address of the call gate indirectly with a memory location (m16:16 or m16:32 or m16:64).
Function:
(defun x86-far-jmp-op/en-d (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-far-jmp-op/en-d)) (declare (ignorable __function__)) (b* ((?ctx 'x86-far-jmp-op/en-d) (?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* (((when (equal mod 3)) (!!ms-fresh :source-operand-not-memory-location mod)) (p2 (prefixes->seg prefixes)) (p4? (equal 103 (prefixes->adr prefixes))) ((the (integer 2 8) offset-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 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 (the (integer 2 10) (+ 2 offset-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-error flg)) (badlength? (check-instruction-length start-rip temp-rip increment-rip-by)) ((when badlength?) (!!fault-fresh :gp 0 :instruction-length badlength?)) (selector (the (unsigned-byte 16) (n16 mem))) (offset (mbe :logic (part-select mem :low 16 :width (ash offset-size 3)) :exec (ash mem -16))) ((the (unsigned-byte 13) sel-index) (segment-selectorbits->index selector)) ((the (unsigned-byte 1) sel-ti) (segment-selectorbits->ti selector)) ((the (unsigned-byte 2) sel-rpl) (segment-selectorbits->rpl selector)) ((when (and (equal sel-ti 0) (equal sel-index 0))) (!!fault-fresh :gp 0 :gp-nullselector 0)) ((mv dt-base-addr dt-limit) (if (equal sel-ti 0) (b* ((gdtr (the (unsigned-byte 80) (stri 0 x86))) (gdtr-base (if (eql proc-mode 0) (gdtr/idtrbits->base-addr gdtr) (n32 (gdtr/idtrbits->base-addr gdtr)))) (gdtr-limit (gdtr/idtrbits->limit gdtr))) (mv gdtr-base gdtr-limit)) (b* ((ldtr-base (the (unsigned-byte 64) (ssr-hidden-basei 0 x86))) (ldtr-base (if (eql proc-mode 0) ldtr-base (n32 ldtr-base))) (ldtr-limit (the (unsigned-byte 32) (ssr-hidden-limiti 0 x86)))) (mv ldtr-base ldtr-limit)))) (largest-address (+ (ash sel-index 3) 7)) ((when (< dt-limit largest-address)) (!!fault-fresh :gp sel-index :gp-selector-limit-check-failed (list selector dt-base-addr dt-limit))) (descriptor-addr (+ dt-base-addr (the (unsigned-byte 16) (ash sel-index 3)))) ((when (not (canonical-address-p descriptor-addr))) (!!ms-fresh :descriptor-addr-virtual-memory-error descriptor-addr)) ((mv flg (the (unsigned-byte 64) descriptor) x86) (rml-size 8 descriptor-addr :x x86)) ((when flg) (!!ms-fresh :rml-size-error flg)) (s (code-segment-descriptorbits->s descriptor)) ((when (= s 1)) (b* ((msb-of-type (code-segment-descriptorbits->msb-of-type descriptor)) ((unless (= msb-of-type 1)) (!!fault-fresh :gp sel-index :jmp-far-data-segment sel-index)) (d (code-segment-descriptorbits->d descriptor)) ((when (and (eql proc-mode 0) (= d 1))) (!!fault-fresh :gp sel-index :cs.d=1-in-64-bit-mode sel-index)) (cpl (cpl x86)) (dpl (code-segment-descriptorbits->dpl descriptor)) (c (code-segment-descriptorbits->c descriptor)) (allowed (if (= c 1) (<= dpl cpl) (and (<= sel-rpl cpl) (equal cpl dpl)))) ((when (not allowed)) (!!fault-fresh :gp sel-index :privilege-check-fail (acons :dpl dpl (acons :cpl cpl (acons :rpl sel-rpl nil))))) (p (code-segment-descriptorbits->p descriptor)) ((unless (= p 1)) (!!fault-fresh :np sel-index :code-segment-not-present sel-index)) (jmp-addr (case offset-size (2 (n16 offset)) (4 (n32 offset)) (t (i64 offset)))) (jmp-addr-ok (if (eql proc-mode 0) (canonical-address-p jmp-addr) (b* ((limit15-0 (code-segment-descriptorbits->limit15-0 descriptor)) (limit19-16 (code-segment-descriptorbits->limit19-16 descriptor)) (limit (part-install limit15-0 (ash limit19-16 16) :low 0 :width 16)) (g (code-segment-descriptorbits->g descriptor)) (max-offset (if (= g 1) (1- (ash limit 12)) limit))) (< jmp-addr max-offset)))) ((unless jmp-addr-ok) (!!fault-fresh :gp 0 :noncanonical-or-outside-segment-limit jmp-addr)) (new-cs-visible (!segment-selectorbits->rpl cpl selector)) (x86 (!seg-visiblei 1 new-cs-visible x86)) (x86 (!seg-hidden-basei 1 dt-base-addr x86)) (x86 (!seg-hidden-limiti 1 dt-limit x86)) (x86 (!seg-hidden-attri 1 (make-code-segment-attr-field descriptor) x86)) (x86 (write-*ip proc-mode jmp-addr x86))) x86)) ((when (not (equal proc-mode 0))) (!!ms-fresh :far-jmp-system-unimplemented-in-32-bit-mode)) (largest-address (+ (ash sel-index 3) 15)) ((when (< dt-limit largest-address)) (!!fault-fresh :gp sel-index :gp-selector-limit-check-failed (list selector dt-base-addr dt-limit))) ((mv flg (the (unsigned-byte 128) descriptor) x86) (rml-size 16 descriptor-addr :x x86)) ((when flg) (!!ms-fresh :rml-size-error flg)) ((mv call-gate-desc? reason2) (ia32e-valid-call-gate-segment-descriptor-p descriptor)) ((when call-gate-desc?) (b* ((cpl (cpl x86)) (dpl (call-gate-descriptorbits->dpl descriptor)) ((when (not (and (<= cpl dpl) (<= sel-rpl dpl)))) (!!fault-fresh :gp sel-index :privilege-check-fail (acons :dpl dpl (acons :cpl cpl (acons :rpl sel-rpl nil))))) (cs-selector (call-gate-descriptorbits->selector descriptor)) ((the (unsigned-byte 13) cs-sel-index) (segment-selectorbits->index cs-selector)) ((the (unsigned-byte 1) cs-sel-ti) (segment-selectorbits->ti cs-selector)) ((the (unsigned-byte 2) cs-sel-rpl) (segment-selectorbits->rpl cs-selector)) ((when (and (equal cs-sel-ti 0) (equal cs-sel-index 0))) (!!fault-fresh :gp 0 :call-gate-code-segment-nullselector 0)) ((mv cs-dt-base-addr cs-dt-limit) (if (equal sel-ti 0) (b* ((gdtr (the (unsigned-byte 80) (stri 0 x86))) (gdtr-base (gdtr/idtrbits->base-addr gdtr)) (gdtr-base (if (eql proc-mode *64-bit-mode*) gdtr-base (n32 gdtr-base))) (gdtr-limit (gdtr/idtrbits->limit gdtr))) (mv gdtr-base gdtr-limit)) (b* ((ldtr-base (the (unsigned-byte 64) (ssr-hidden-basei 0 x86))) (ldtr-base (if (eql proc-mode 0) ldtr-base (n32 ldtr-base))) (ldtr-limit (the (unsigned-byte 32) (ssr-hidden-limiti 0 x86)))) (mv ldtr-base ldtr-limit)))) (largest-address (+ (ash cs-sel-index 3) 7)) ((when (< cs-dt-limit largest-address)) (!!fault-fresh :gp cs-sel-index :gp-selector-limit-check-failed (list cs-selector cs-dt-base-addr cs-dt-limit))) (cs-descriptor-addr (+ cs-dt-base-addr (the (unsigned-byte 16) (ash cs-sel-index 3)))) ((when (not (canonical-address-p cs-descriptor-addr))) (!!ms-fresh :cs-descriptor-addr-virtual-memory-error cs-descriptor-addr)) ((mv flg (the (unsigned-byte 64) cs-descriptor) x86) (rml-size 8 cs-descriptor-addr :x x86)) ((when flg) (!!ms-fresh :rml-size-error flg)) ((mv valid? reason) (ia32e-valid-code-segment-descriptor-p cs-descriptor)) ((when (not valid?)) (!!fault-fresh :gp cs-sel-index :call-gate-code-segment-descriptor-invalid (cons reason cs-descriptor))) (cs-dpl (code-segment-descriptorbits->dpl cs-descriptor)) (c-bit (code-segment-descriptorbits->c cs-descriptor)) ((when (or (and (equal c-bit 1) (not (<= cs-dpl cpl))) (and (equal c-bit 0) (not (eql cs-dpl cpl))))) (!!fault-fresh :gp cs-sel-index :privilege-check-fail (acons :c-bit c-bit (acons :cpl cpl (acons :cs-dpl cs-dpl nil))))) (call-gate-offset15-0 (call-gate-descriptorbits->offset15-0 descriptor)) (call-gate-offset31-16 (call-gate-descriptorbits->offset31-16 descriptor)) (call-gate-offset63-32 (call-gate-descriptorbits->offset63-32 descriptor)) (call-gate-offset31-0 (mbe :logic (part-install call-gate-offset15-0 (ash call-gate-offset31-16 16) :low 0 :width 16) :exec (the (unsigned-byte 32) (logior (the (unsigned-byte 16) call-gate-offset15-0) (the (unsigned-byte 32) (ash call-gate-offset31-16 16)))))) (call-gate-offset (mbe :logic (part-install call-gate-offset31-0 (ash call-gate-offset63-32 32) :low 0 :width 32) :exec (the (unsigned-byte 64) (logior (the (unsigned-byte 32) call-gate-offset31-0) (the (unsigned-byte 64) (ash call-gate-offset63-32 32)))))) (jmp-addr (case offset-size (2 (n16 call-gate-offset)) (4 (n32 call-gate-offset)) (t call-gate-offset))) ((when (not (canonical-address-p jmp-addr))) (!!ms-fresh :target-offset-virtual-memory-error jmp-addr)) (new-cs-visible (!segment-selectorbits->rpl cpl cs-selector)) (x86 (!seg-visiblei 1 new-cs-visible x86)) (x86 (!seg-hidden-basei 1 cs-dt-base-addr x86)) (x86 (!seg-hidden-limiti 1 cs-dt-limit x86)) (x86 (!seg-hidden-attri 1 (make-code-segment-attr-field cs-descriptor) x86)) (x86 (write-*ip proc-mode jmp-addr x86))) x86))) (!!fault-fresh :gp sel-index :either-both-code-segment-or-call-gate-are-absent-or-some-other-descriptor-is-present (cons reason2 descriptor))))))
Theorem:
(defthm x86p-of-x86-far-jmp-op/en-d (implies (x86p x86) (b* ((x86 (x86-far-jmp-op/en-d proc-mode start-rip temp-rip prefixes rex-byte opcode modr/m sib x86))) (x86p x86))) :rule-classes :rewrite)