(x86-lldt proc-mode start-rip temp-rip prefixes rex-byte opcode modr/m sib x86) → x86
If bits 2-15 of the source operand are 0, LDTR is marked invalid and the LLDT instruction completes silently. However, all subsequent references to descriptors in the LDT (except by the LAR, VERR, VERW or LSL instructions) cause a general protection exception.
The operand-size attribute has no effect on this instruction. In 64-bit mode, the operand size is fixed at 16 bits.
TO-DO: If a memory address referencing the SS segment is in a non-canonical form, raise the SS exception.
Function:
(defun x86-lldt (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-lldt)) (declare (ignorable __function__)) (b* ((?ctx 'x86-lldt) (?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 (app-view x86)) (!!ms-fresh :lldt-unimplemented)) (p2 (prefixes->seg prefixes)) (p4? (equal 103 (prefixes->adr prefixes))) (seg-reg (select-segment-register proc-mode p2 p4? mod r/m sib x86)) (inst-ac? nil) ((mv flg0 selector (the (unsigned-byte 3) increment-rip-by) (the (signed-byte 64) addr) x86) (x86-operand-from-modr/m-and-sib-bytes proc-mode *gpr-access* 2 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)) ((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?)) ((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 (equal sel-ti 1)) (!!ms-fresh :gp-selector-does-not-point-to-gdt selector)) ((the (unsigned-byte 80) gdtr) (stri *gdtr* x86)) ((the (unsigned-byte 64) gdtr-base) (if (eql proc-mode 0) (gdtr/idtrbits->base-addr gdtr) (n32 (gdtr/idtrbits->base-addr gdtr)))) ((the (unsigned-byte 16) gdtr-limit) (gdtr/idtrbits->limit gdtr)) (largest-address (+ (ash sel-index 3) (if (eql proc-mode *64-bit-mode*) 15 7))) ((when (< gdtr-limit largest-address)) (!!ms-fresh :gp-selector-limit-check-failed (cons selector gdtr))) (x86 (if (equal sel-index 0) (!ssr-visiblei *ldtr* selector x86) (b* ((descriptor-addr (+ gdtr-base (the (unsigned-byte 16) (ash sel-index 3)))) ((when (not (canonical-address-p descriptor-addr))) (!!ms-fresh :descriptor-addr-virtual-memory-error descriptor-addr)) (descriptor-size (if (eql proc-mode *64-bit-mode*) 16 8)) ((mv flg (the (unsigned-byte 128) descriptor) x86) (rml-size descriptor-size descriptor-addr :x x86)) ((when flg) (!!ms-fresh :rml-size-error flg)) ((mv descriptor-valid? reason) (ia32e-valid-ldt-segment-descriptor-p descriptor)) ((when (not descriptor-valid?)) (!!ms-fresh :invalid-segment-descriptor reason)) (ldtr-base15-0 (system-segment-descriptorbits->base15-0 descriptor)) (ldtr-base23-16 (system-segment-descriptorbits->base23-16 descriptor)) (ldtr-base31-24 (system-segment-descriptorbits->base31-24 descriptor)) (ldtr-base63-32 (system-segment-descriptorbits->base63-32 descriptor)) ((the (unsigned-byte 40) ldtr-base63-24) (part-install ldtr-base31-24 (ash ldtr-base63-32 8) :low 0 :width 8)) ((the (unsigned-byte 24) ldtr-base23-0) (part-install ldtr-base15-0 (ash ldtr-base23-16 16) :low 0 :width 16)) ((the (unsigned-byte 64) ldtr-base) (part-install ldtr-base23-0 (ash ldtr-base63-24 24) :low 0 :width 24)) (ldtr-limit15-0 (system-segment-descriptorbits->limit15-0 descriptor)) (ldtr-limit19-16 (system-segment-descriptorbits->limit19-16 descriptor)) ((the (unsigned-byte 32) ldtr-limit) (part-install ldtr-limit15-0 (ash ldtr-limit19-16 16) :low 0 :width 16)) (ldtr-attr (the (unsigned-byte 16) (make-system-segment-attr-field descriptor))) (x86 (!ssr-visiblei 0 selector x86)) (x86 (!ssr-hidden-basei 0 ldtr-base x86)) (x86 (!ssr-hidden-limiti 0 ldtr-limit x86)) (x86 (!ssr-hidden-attri 0 ldtr-attr x86))) x86))) (x86 (write-*ip proc-mode temp-rip x86))) x86))))
Theorem:
(defthm x86p-of-x86-lldt (implies (x86p x86) (b* ((x86 (x86-lldt proc-mode start-rip temp-rip prefixes rex-byte opcode modr/m sib x86))) (x86p x86))) :rule-classes :rewrite)