diff --git a/books/projects/x86isa/machine/x86-decoding-and-spec-utils.lisp b/books/projects/x86isa/machine/x86-decoding-and-spec-utils.lisp index 811c4d6d242..1740749879b 100644 --- a/books/projects/x86isa/machine/x86-decoding-and-spec-utils.lisp +++ b/books/projects/x86isa/machine/x86-decoding-and-spec-utils.lisp @@ -860,7 +860,7 @@ made from privilege level 3." ,@(and trunc `((trunc booleanp))) (start-rip :type (signed-byte #.*max-linear-address-size*)) (temp-rip :type (signed-byte #.*max-linear-address-size*)) - (prefixes :type (unsigned-byte 43)) + (prefixes :type (unsigned-byte 44)) (rex-byte :type (unsigned-byte 8)) (opcode :type (unsigned-byte 8)) (modr/m :type (unsigned-byte 8)) @@ -911,7 +911,7 @@ made from privilege level 3." ((byte-operand? :type (or t nil)) (rex-byte :type (unsigned-byte 8)) (imm? :type (or t nil)) - (prefixes :type (unsigned-byte 43))) + (prefixes :type (unsigned-byte 44))) :inline t :parents (x86-decoding-and-spec-utils) diff --git a/books/projects/x86isa/machine/x86.lisp b/books/projects/x86isa/machine/x86.lisp index 1ed0a400afe..b535424b9b8 100644 --- a/books/projects/x86isa/machine/x86.lisp +++ b/books/projects/x86isa/machine/x86.lisp @@ -988,7 +988,7 @@ ((start-rip :type (signed-byte #.*max-linear-address-size*)) (temp-rip :type (signed-byte #.*max-linear-address-size*)) - (prefixes :type (unsigned-byte 43)) + (prefixes :type (unsigned-byte 44)) (rex-byte :type (unsigned-byte 8)) (opcode :type (unsigned-byte 8)) (modr/m :type (unsigned-byte 8)) @@ -1024,7 +1024,7 @@ (define two-byte-opcode-decode-and-execute ((start-rip :type (signed-byte #.*max-linear-address-size*)) (temp-rip :type (signed-byte #.*max-linear-address-size*)) - (prefixes :type (unsigned-byte 43)) + (prefixes :type (unsigned-byte 44)) (rex-byte :type (unsigned-byte 8)) (escape-byte :type (unsigned-byte 8)) x86) @@ -2554,7 +2554,7 @@ ((start-rip :type (signed-byte #.*max-linear-address-size*)) (temp-rip :type (signed-byte #.*max-linear-address-size*)) - (prefixes :type (unsigned-byte 43)) + (prefixes :type (unsigned-byte 44)) (rex-byte :type (unsigned-byte 8)) (opcode :type (unsigned-byte 8)) (modr/m :type (unsigned-byte 8)) @@ -2591,8 +2591,8 @@ (define get-prefixes ((start-rip :type (signed-byte #.*max-linear-address-size*)) - (prefixes :type (unsigned-byte 43)) - (cnt :type (integer 0 5)) + (prefixes :type (unsigned-byte 44)) + (cnt :type (integer 0 15)) x86) :guard-hints (("Goal" :in-theory @@ -2662,20 +2662,20 @@ () (local (include-book "arithmetic-5/top" :dir :system)) - (defthm negative-logand-to-positive-logand-with-n43p-x + (defthm negative-logand-to-positive-logand-with-n44p-x (implies (and (< n 0) (syntaxp (quotep n)) - (equal m 43) + (equal m 44) (integerp n) - (n43p x)) + (n44p x)) (equal (logand n x) (logand (logand (1- (ash 1 m)) n) x))))))) (if (mbe :logic (zp cnt) :exec (eql cnt 0)) - ;; Error, too many prefix bytes - (mv nil prefixes x86) + ;; Error, too many prefix bytes --- invalid instruction length. + (mv t prefixes x86) (b* ((ctx 'get-prefixes) ((mv flg (the (unsigned-byte 8) byte) x86) @@ -2693,7 +2693,7 @@ ;; following the prefixes in "prefixes"... (let ((prefixes (!prefixes-slice :next-byte byte prefixes))) - (mv nil (!prefixes-slice :num-prefixes (- 5 cnt) prefixes) + (mv nil (!prefixes-slice :num-prefixes (- 15 cnt) prefixes) x86)) (case prefix-byte-group-code @@ -2713,11 +2713,11 @@ #.*2^47*)) ;; Storing the group 1 prefix and going on... (get-prefixes next-rip - (the (unsigned-byte 43) + (the (unsigned-byte 44) (!prefixes-slice :group-1-prefix byte prefixes)) - (the (integer 0 5) (1- cnt)) x86) + (the (integer 0 15) (1- cnt)) x86) (mv (cons 'non-canonical-address next-rip) prefixes x86))) ;; We do not tolerate more than one prefix from a prefix group. (mv t prefixes x86)))) @@ -2741,7 +2741,7 @@ (!prefixes-slice :group-2-prefix byte prefixes) - (the (integer 0 5) (1- cnt)) x86) + (the (integer 0 15) (1- cnt)) x86) (mv (cons 'non-canonical-address next-rip) prefixes x86))) ;; We do not tolerate more than one prefix from a prefix group. @@ -2767,7 +2767,7 @@ (!prefixes-slice :group-3-prefix byte prefixes) - (the (integer 0 5) (1- cnt)) x86) + (the (integer 0 15) (1- cnt)) x86) (mv (cons 'non-canonical-address next-rip) prefixes x86))) ;; We do not tolerate more than one prefix from a prefix group. @@ -2792,7 +2792,7 @@ (!prefixes-slice :group-4-prefix byte prefixes) - (the (integer 0 5) (1- cnt)) x86) + (the (integer 0 15) (1- cnt)) x86) (mv (cons 'non-canonical-address next-rip) prefixes x86))) ;; We do not tolerate more than one prefix from a prefix group. @@ -2822,11 +2822,11 @@ bitops::unsigned-byte-p-when-unsigned-byte-p-less)))) :rule-classes :type-prescription) - (defthm-usb n43p-get-prefixes - :hyp (and (n43p prefixes) + (defthm-usb n44p-get-prefixes + :hyp (and (n44p prefixes) (canonical-address-p start-rip) (x86p x86)) - :bound 43 + :bound 44 :concl (mv-nth 1 (get-prefixes start-rip prefixes cnt x86)) :hints (("Goal" :in-theory (e/d () (signed-byte-p @@ -2873,7 +2873,7 @@ bitops::basic-signed-byte-p-of-+ default-<-1 negative-logand-to-positive-logand-with-integerp-x - negative-logand-to-positive-logand-with-n43p-x + negative-logand-to-positive-logand-with-n44p-x force (force)))))) (defthm get-prefixes-does-not-modify-x86-state-in-programmer-level-mode @@ -2912,16 +2912,16 @@ (defthm num-prefixes-get-prefixes-bound - (implies (and (<= cnt 5) + (implies (and (<= cnt 15) (x86p x86) (canonical-address-p start-rip) - (n43p prefixes) + (n44p prefixes) (< (part-select prefixes :low 0 :high 2) 5)) - (< + (<= (prefixes-slice :num-prefixes (mv-nth 1 (get-prefixes start-rip prefixes cnt x86))) - 5)) + 15)) :hints (("Goal" :induct (get-prefixes start-rip prefixes cnt x86) :in-theory (e/d (rm08-value-when-error) @@ -2951,7 +2951,7 @@ (defthm get-prefixes-opener-lemma-zero-cnt (implies (zp cnt) (equal (get-prefixes start-rip prefixes cnt x86) - (mv nil prefixes x86))) + (mv t prefixes x86))) :hints (("Goal" :in-theory (e/d (get-prefixes) ())))) (defthm get-prefixes-opener-lemma-no-prefix-byte @@ -2973,7 +2973,7 @@ (!prefixes-slice :next-byte (mv-nth 1 (rm08 start-rip :x x86)) prefixes))) - (!prefixes-slice :num-prefixes (- 5 cnt) prefixes)))))) + (!prefixes-slice :num-prefixes (- 15 cnt) prefixes)))))) (defthm get-prefixes-opener-lemma-group-1-prefix (implies (and (or (programmer-level-mode x86) @@ -2996,7 +2996,7 @@ (1- cnt) x86))) :hints (("Goal" :in-theory (e/d* () (unsigned-byte-p - negative-logand-to-positive-logand-with-n43p-x + negative-logand-to-positive-logand-with-n44p-x negative-logand-to-positive-logand-with-integerp-x))))) (defthm get-prefixes-opener-lemma-group-2-prefix @@ -3020,7 +3020,7 @@ (1- cnt) x86))) :hints (("Goal" :in-theory (e/d* () (unsigned-byte-p - negative-logand-to-positive-logand-with-n43p-x + negative-logand-to-positive-logand-with-n44p-x negative-logand-to-positive-logand-with-integerp-x))))) (defthm get-prefixes-opener-lemma-group-3-prefix @@ -3044,7 +3044,7 @@ (1- cnt) x86))) :hints (("Goal" :in-theory (e/d* () (unsigned-byte-p - negative-logand-to-positive-logand-with-n43p-x + negative-logand-to-positive-logand-with-n44p-x negative-logand-to-positive-logand-with-integerp-x))))) (defthm get-prefixes-opener-lemma-group-4-prefix @@ -3068,7 +3068,7 @@ (1- cnt) x86))) :hints (("Goal" :in-theory (e/d* () (unsigned-byte-p - negative-logand-to-positive-logand-with-n43p-x + negative-logand-to-positive-logand-with-n44p-x negative-logand-to-positive-logand-with-integerp-x)))))) ;; ====================================================================== @@ -3084,6 +3084,7 @@ address indicated by the instruction pointer @('rip'), decodes that instruction, and dispatches control to the appropriate instruction semantic function.

" + :guard-debug t :prepwork ((local (in-theory (e/d* () (unsigned-byte-p not))))) @@ -3099,13 +3100,15 @@ semantic function.

" (start-rip (the (signed-byte #.*max-linear-address-size*) (rip x86))) - ((mv flg0 (the (unsigned-byte 43) prefixes) x86) - (get-prefixes start-rip 0 5 x86)) - ;; Among other errors, if get-prefixes detects a non-canonical + ((mv flg0 (the (unsigned-byte 44) prefixes) x86) + (get-prefixes start-rip 0 15 x86)) + ;; Among other errors (including if there are 15 prefix bytes, + ;; which leaves no room for an opcode byte in a legal + ;; instruction), if get-prefixes detects a non-canonical ;; address while attempting to fetch prefixes, flg0 will be ;; non-nil. ((when flg0) - (!!ms-fresh :memory-error-in-reading-prefixes flg0)) + (!!ms-fresh :error-in-reading-prefixes flg0)) ((the (unsigned-byte 8) opcode/rex/escape-byte) (prefixes-slice :next-byte prefixes)) @@ -3265,7 +3268,7 @@ semantic function.

" (defthm x86-fetch-decode-execute-opener (implies (and (equal start-rip (rip x86)) - (equal prefixes (mv-nth 1 (get-prefixes start-rip 0 5 x86))) + (equal prefixes (mv-nth 1 (get-prefixes start-rip 0 15 x86))) (equal opcode/rex/escape-byte (prefixes-slice :next-byte prefixes)) (equal prefix-length (prefixes-slice :num-prefixes prefixes)) @@ -3294,7 +3297,7 @@ semantic function.

" (not (page-structure-marking-mode x86)))) (not (ms x86)) (not (fault x86)) - (not (mv-nth 0 (get-prefixes start-rip 0 5 x86))) + (not (mv-nth 0 (get-prefixes start-rip 0 15 x86))) (canonical-address-p temp-rip0) (if (and (equal prefix-length 0) (equal rex-byte 0) diff --git a/books/projects/x86isa/portcullis/sharp-dot-constants.lisp b/books/projects/x86isa/portcullis/sharp-dot-constants.lisp index ed8e05e071d..8c2395717e3 100644 --- a/books/projects/x86isa/portcullis/sharp-dot-constants.lisp +++ b/books/projects/x86isa/portcullis/sharp-dot-constants.lisp @@ -9,27 +9,27 @@ (defun power-of-2-measure (x) (cond ((or (not (natp x)) - (<= x 1)) - 0) - (t (floor x 1)))) + (<= x 1)) + 0) + (t (floor x 1)))) (defn power-of-2 (x count) (declare (xargs :measure (power-of-2-measure x) - :guard (natp count))) + :guard (natp count))) (if (natp x) (if (<= x 1) - count - (power-of-2 (* 1/2 x) (1+ count))) + count + (power-of-2 (* 1/2 x) (1+ count))) count)) (defun gl-int (start by count) (declare (xargs :guard (and (natp start) - (natp by) - (natp count)))) + (natp by) + (natp count)))) (if (zp count) nil (cons start - (gl-int (+ by start) by (1- count))))) + (gl-int (+ by start) by (1- count))))) ;; ====================================================================== ;; Some expt constants: @@ -65,6 +65,7 @@ (defconst *2^32* (expt 2 32)) (defconst *2^35* (expt 2 35)) (defconst *2^43* (expt 2 43)) +(defconst *2^44* (expt 2 44)) (defconst *2^45* (expt 2 45)) (defconst *2^47* (expt 2 47)) (defconst *-2^47* (- (expt 2 47))) @@ -219,14 +220,14 @@ (defconst *flg-names* (list *cf* *pf* *af* *zf* *sf* *tf* *if* *df* - *of* *iopl* *nt* *rf* *vm* *ac* *vif* *vip* *id*)) + *of* *iopl* *nt* *rf* *vm* *ac* *vif* *vip* *id*)) (defun max-list (l) (if (or (endp l) - (equal (len l) 1)) + (equal (len l) 1)) (car l) (if (> (car l) (max-list (cdr l))) - (car l) + (car l) (max-list (cdr l))))) (defconst *max-flg-index* @@ -251,7 +252,7 @@ (defconst *fp-status-names* (list *fp-ie* *fp-de* *fp-ze* *fp-oe* *fp-ue* *fp-pe* *fp-sf* - *fp-es* *fp-c0* *fp-c1* *fp-c2* *fp-top* *fp-c3* *fp-b*)) + *fp-es* *fp-c0* *fp-c1* *fp-c2* *fp-top* *fp-c3* *fp-b*)) ;; MXCSR (Intel Manual, Feb'14, Vol. 1, Section 10.2.3) @@ -281,9 +282,9 @@ (defconst *mxcsr-names* (list *mxcsr-ie* *mxcsr-de* *mxcsr-ze* *mxcsr-oe* *mxcsr-ue* - *mxcsr-pe* *mxcsr-daz* *mxcsr-im* *mxcsr-dm* *mxcsr-zm* - *mxcsr-om* *mxcsr-um* *mxcsr-pm* *mxcsr-rc* *mxcsr-fz* - *mxcsr-reserved*)) + *mxcsr-pe* *mxcsr-daz* *mxcsr-im* *mxcsr-dm* *mxcsr-zm* + *mxcsr-om* *mxcsr-um* *mxcsr-pm* *mxcsr-rc* *mxcsr-fz* + *mxcsr-reserved*)) ;; Access RGF or XMM @@ -317,13 +318,13 @@ (defconst *ieee-dp-frac-width* 52) (defconst *ia32_efer-sce* 0) ;; Syscall Enable (R/W) --- enables - ;; SYSCALL/SYSRET + ;; SYSCALL/SYSRET (defconst *ia32_efer-lme* 8) ;; Long Mode Enabled (R/W) (defconst *ia32_efer-lma* 10) ;; Long Mode Active (R) (defconst *ia32_efer-nxe* 11) ;; Execute Disable Bit Enable (R/W) - ;; (Enables page access restriction by - ;; preventing instruction fetches from - ;; PAE pages with the XD bit set) + ;; (Enables page access restriction by + ;; preventing instruction fetches from + ;; PAE pages with the XD bit set) (defconst *ia32_efer-names* (list *ia32_efer-sce* *ia32_efer-lme* *ia32_efer-lma* *ia32_efer-nxe*)) @@ -447,7 +448,7 @@ (defconst *mem-table-size* ;; Size of table for address-to-pseudo-page translation (floor *mem-size-in-bytes* - *pseudo-page-size-in-bytes*)) + *pseudo-page-size-in-bytes*)) (defconst *mem-table-size-bits* (power-of-2 *mem-table-size* 0)) @@ -480,73 +481,73 @@ (defun define-general-purpose-registers () `(defconsts (*RAX* *RCX* *RDX* *RBX* *RSP* *RBP* *RSI* *RDI* - *R8* *R9* *R10* *R11* *R12* *R13* *R14* *R15* - *64-bit-general-purpose-registers-len*) + *R8* *R9* *R10* *R11* *R12* *R13* *R14* *R15* + *64-bit-general-purpose-registers-len*) ,(b* ((lst (gl-int 0 1 16)) - (len (len lst))) - (cons 'mv (append lst (list len)))))) + (len (len lst))) + (cons 'mv (append lst (list len)))))) (defun define-segment-registers () `(defconsts (*ES* *CS* *SS* *DS* *FS* *GS* - *segment-register-names-len*) + *segment-register-names-len*) ,(b* ((lst (gl-int 0 1 6)) - (len (len lst))) - (cons 'mv (append lst (list len)))))) + (len (len lst))) + (cons 'mv (append lst (list len)))))) (defun define-gdtr/idtr-registers () `(defconsts (*GDTR* *IDTR* *gdtr-idtr-names-len*) ,(b* ((lst (gl-int 0 1 2)) - (len (len lst))) - (cons 'mv (append lst (list len)))))) + (len (len lst))) + (cons 'mv (append lst (list len)))))) (defun define-ldtr/tr-registers () `(defconsts (*LDTR* *TR* *ldtr-tr-names-len*) ,(b* ((lst (gl-int 0 1 2)) - (len (len lst))) - (cons 'mv (append lst (list len)))))) + (len (len lst))) + (cons 'mv (append lst (list len)))))) ;; Source: Intel Manual, Feb-14, Vol. 3A, Section 2.5 (defun define-control-registers () `(defconsts (*CR0* ;; cr0 controls operating mode and states of - ;; processor - *CR1* ;; cr1 is reserved - *CR2* ;; cr2 holds the page fault linear address (the - ;; one that caused the page fault) - *CR3* ;; cr3 is associated with paging - *CR4* ;; cr4 enables or indicates support for processor - ;; extensions - *CR5* ;; cr5 is reserved - *CR6* ;; cr6 is reserved - *CR7* ;; cr7 is reserved - *CR8* ;; cr8 provides read/write access to the TPR. - ;; (Task Priority Register) available only in 64 - ;; bit mode - ;; cr9 thru cr15 are not implemented in our model yet. - *CR9* *CR10* *CR11* *CR12* *CR13* *CR14* *CR15* - *XCR0* - *control-register-names-len*) + ;; processor + *CR1* ;; cr1 is reserved + *CR2* ;; cr2 holds the page fault linear address (the + ;; one that caused the page fault) + *CR3* ;; cr3 is associated with paging + *CR4* ;; cr4 enables or indicates support for processor + ;; extensions + *CR5* ;; cr5 is reserved + *CR6* ;; cr6 is reserved + *CR7* ;; cr7 is reserved + *CR8* ;; cr8 provides read/write access to the TPR. + ;; (Task Priority Register) available only in 64 + ;; bit mode + ;; cr9 thru cr15 are not implemented in our model yet. + *CR9* *CR10* *CR11* *CR12* *CR13* *CR14* *CR15* + *XCR0* + *control-register-names-len*) ,(b* ((lst (gl-int 0 1 17)) - (len (len lst))) - (cons 'mv (append lst (list len)))))) + (len (len lst))) + (cons 'mv (append lst (list len)))))) (defun define-debug-registers () `(defconsts (*DR0* ;; dr0 holds breakpoint 0 virtual address, 64/32 bit - *DR1* ;; dr1 holds breakpoint 1 virtual address, 64/32 bit - *DR2* ;; dr2 holds breakpoint 2 virtual address, 64/32 bit - *DR3* ;; dr3 holds breakpoint 3 virtual address, 64/32 bit - *DR4* ;; dr4 is reserved - *DR5* ;; dr5 is reserved - *DR6* ;; dr6 - *DR7* ;; dr7 - *debug-register-names-len*) + *DR1* ;; dr1 holds breakpoint 1 virtual address, 64/32 bit + *DR2* ;; dr2 holds breakpoint 2 virtual address, 64/32 bit + *DR3* ;; dr3 holds breakpoint 3 virtual address, 64/32 bit + *DR4* ;; dr4 is reserved + *DR5* ;; dr5 is reserved + *DR6* ;; dr6 + *DR7* ;; dr7 + *debug-register-names-len*) ,(b* ((lst (gl-int 0 1 8)) - (len (len lst))) - (cons 'mv (append lst (list len)))))) + (len (len lst))) + (cons 'mv (append lst (list len)))))) (defun define-fp-registers () ;; 80-bit registers @@ -556,11 +557,11 @@ ;; FP7. `(defconsts (*FP0* *FP1* *FP2* *FP3* *FP4* *FP5* *FP6* *FP7* - *fp-data-register-names-len*) + *fp-data-register-names-len*) ,(b* ((lst (gl-int 0 1 8)) - (len (len lst))) - (cons 'mv (append lst (list len)))))) + (len (len lst))) + (cons 'mv (append lst (list len)))))) (defun define-mmx-registers () ;; 64-bit registers @@ -569,23 +570,23 @@ ;; of the FPU data registers. `(defconsts (*MM0* *MM1* *MM2* *MM3* *MM4* *MM5* *MM6* *MM7* - *mmx-register-names-len*) + *mmx-register-names-len*) ,(b* ((lst (gl-int 0 1 8)) - (len (len lst))) - (cons 'mv (append lst (list len)))))) + (len (len lst))) + (cons 'mv (append lst (list len)))))) (defun define-xmm-registers () ;; 128-bit registers `(defconsts (*XMM0* *XMM1* *XMM2* *XMM3* *XMM4* *XMM5* *XMM6* *XMM7* - *XMM8* *XMM9* *XMM10* *XMM11* - *XMM12* *XMM13* *XMM14* *XMM15* - *xmm-register-names-len*) + *XMM8* *XMM9* *XMM10* *XMM11* + *XMM12* *XMM13* *XMM14* *XMM15* + *xmm-register-names-len*) ,(b* ((lst (gl-int 0 1 16)) - (len (len lst))) - (cons 'mv (append lst (list len)))))) + (len (len lst))) + (cons 'mv (append lst (list len)))))) (defun define-model-specific-registers () ;; At this point, we only model the MSRs that we need. Remember, @@ -597,61 +598,61 @@ `(defconsts ( - ;; extended features enables --- If - ;; CPUID.80000001.EDX.[bit 20] or - ;; CPUID.80000001.EDX.[bit 29] - *IA32_EFER* - *IA32_EFER-IDX* - - ;; Map of BASE Address of FS (R/W) --- If - ;; CPUID.80000001.EDX.[bit 29] = 1 - *IA32_FS_BASE* - *IA32_FS_BASE-IDX* - - ;; Map of BASE Address of GB (R/W) --- If - ;; CPUID.80000001.EDX.[bit 29] = 1 - *IA32_GS_BASE* - *IA32_GS_BASE-IDX* - - ;; Swap Target of BASE Address of GS (R/W) --- If - ;; CPUID.80000001.EDX.[bit 29] = 1 - *IA32_KERNEL_GS_BASE* - *IA32_KERNEL_GS_BASE-IDX* - - ;; System Call Target Address (R/W) --- If - ;; CPUID.80000001.EDX.[bit 29] = 1 - *IA32_STAR* - *IA32_STAR-IDX* - - ;; IA-32e Mode System Call Target Address (R/W) --- If - ;; CPUID.80000001.EDX.[bit 29] = 1 - *IA32_LSTAR* - *IA32_LSTAR-IDX* - - ;; System Call Flag Mask (R/W) --- If - ;; CPUID.80000001.EDX.[bit 29] = 1 - *IA32_FMASK* - *IA32_FMASK-IDX* - - *model-specific-register-names-len*) + ;; extended features enables --- If + ;; CPUID.80000001.EDX.[bit 20] or + ;; CPUID.80000001.EDX.[bit 29] + *IA32_EFER* + *IA32_EFER-IDX* + + ;; Map of BASE Address of FS (R/W) --- If + ;; CPUID.80000001.EDX.[bit 29] = 1 + *IA32_FS_BASE* + *IA32_FS_BASE-IDX* + + ;; Map of BASE Address of GB (R/W) --- If + ;; CPUID.80000001.EDX.[bit 29] = 1 + *IA32_GS_BASE* + *IA32_GS_BASE-IDX* + + ;; Swap Target of BASE Address of GS (R/W) --- If + ;; CPUID.80000001.EDX.[bit 29] = 1 + *IA32_KERNEL_GS_BASE* + *IA32_KERNEL_GS_BASE-IDX* + + ;; System Call Target Address (R/W) --- If + ;; CPUID.80000001.EDX.[bit 29] = 1 + *IA32_STAR* + *IA32_STAR-IDX* + + ;; IA-32e Mode System Call Target Address (R/W) --- If + ;; CPUID.80000001.EDX.[bit 29] = 1 + *IA32_LSTAR* + *IA32_LSTAR-IDX* + + ;; System Call Flag Mask (R/W) --- If + ;; CPUID.80000001.EDX.[bit 29] = 1 + *IA32_FMASK* + *IA32_FMASK-IDX* + + *model-specific-register-names-len*) ,(b* ((lst (list #uxC000_0080 ;; ia32_efer and idx - 0 - #uxC000_0100 ;; ia32_fs_base and idx - 1 - #uxC000_0101 ;; ia32_gs_base and idx - 2 - #uxC000_0102 ;; ia32_kernel_gs_base and idx - 3 - #uxC000_0081 ;; ia32_star and idx - 4 - #uxC000_0082 ;; ia32_lstar and idx - 5 - #uxC000_0084 ;; ia32_fmask and idx - 6 - )) - (len (/ (len lst) 2))) - (cons 'mv (append lst (list len)))))) + 0 + #uxC000_0100 ;; ia32_fs_base and idx + 1 + #uxC000_0101 ;; ia32_gs_base and idx + 2 + #uxC000_0102 ;; ia32_kernel_gs_base and idx + 3 + #uxC000_0081 ;; ia32_star and idx + 4 + #uxC000_0082 ;; ia32_lstar and idx + 5 + #uxC000_0084 ;; ia32_fmask and idx + 6 + )) + (len (/ (len lst) 2))) + (cons 'mv (append lst (list len)))))) (make-event (define-general-purpose-registers)) (make-event (define-segment-registers)) diff --git a/books/projects/x86isa/proofs/utilities/system-level-mode/marking-mode-top.lisp b/books/projects/x86isa/proofs/utilities/system-level-mode/marking-mode-top.lisp index c385786d2a6..a925d65c448 100644 --- a/books/projects/x86isa/proofs/utilities/system-level-mode/marking-mode-top.lisp +++ b/books/projects/x86isa/proofs/utilities/system-level-mode/marking-mode-top.lisp @@ -143,8 +143,8 @@ (define get-prefixes-alt ((start-rip :type (signed-byte #.*max-linear-address-size*)) - (prefixes :type (unsigned-byte 43)) - (cnt :type (integer 0 5)) + (prefixes :type (unsigned-byte 44)) + (cnt :type (integer 0 15)) x86) :non-executable t :guard (canonical-address-p (+ cnt start-rip)) @@ -180,15 +180,15 @@ ()))) :rule-classes :type-prescription) - (defthm-usb n43p-get-prefixes-alt - :hyp (and (n43p prefixes) + (defthm-usb n44p-get-prefixes-alt + :hyp (and (n44p prefixes) (canonical-address-p start-rip) (x86p x86)) - :bound 43 + :bound 44 :concl (mv-nth 1 (get-prefixes-alt start-rip prefixes cnt x86)) :hints (("Goal" - :use ((:instance n43p-get-prefixes)) - :in-theory (e/d () (n43p-get-prefixes)))) + :use ((:instance n44p-get-prefixes)) + :in-theory (e/d () (n44p-get-prefixes)))) :gen-linear t) (defthm x86p-get-prefixes-alt @@ -316,7 +316,7 @@ (not (programmer-level-mode x86)) (canonical-address-p start-rip)) (equal (get-prefixes-alt start-rip prefixes cnt x86) - (mv nil prefixes x86))) + (mv t prefixes x86))) :hints (("Goal" :use ((:instance get-prefixes-opener-lemma-zero-cnt)) :in-theory (e/d () (get-prefixes-opener-lemma-zero-cnt @@ -353,7 +353,7 @@ (!prefixes-slice :next-byte (mv-nth 1 (rm08 start-rip :x x86)) prefixes))) - (!prefixes-slice :num-prefixes (- 5 cnt) prefixes))))) + (!prefixes-slice :num-prefixes (- 15 cnt) prefixes))))) :hints (("Goal" :use ((:instance get-prefixes-opener-lemma-no-prefix-byte)) :in-theory (e/d* () (get-prefixes-opener-lemma-no-prefix-byte))))) @@ -856,7 +856,7 @@ (:rewrite subset-p-cdr-x) (:type-prescription n52p-mv-nth-1-ia32e-la-to-pa) (:linear <=-logior) - (:linear n43p-get-prefixes) + (:linear n44p-get-prefixes) (:rewrite get-prefixes-opener-lemma-group-4-prefix) (:rewrite get-prefixes-opener-lemma-group-3-prefix) (:rewrite get-prefixes-opener-lemma-group-2-prefix) @@ -864,7 +864,7 @@ (:rewrite unsigned-byte-p-of-ash) (:linear bitops::logior->=-0-linear) (:rewrite rb-in-terms-of-rb-subset-p-in-system-level-mode) - (:definition n43p$inline) + (:definition n44p$inline) (:rewrite bitops::logtail-of-logtail) (:rewrite mv-nth-2-las-to-pas-system-level-non-marking-mode) (:rewrite mv-nth-1-las-to-pas-when-error) @@ -896,7 +896,7 @@ (:type-prescription all-translation-governing-addresses) (:rewrite acl2::unsigned-byte-p-loghead) (:rewrite bitops::loghead-of-ash-same) - (:type-prescription n43p$inline) + (:type-prescription n44p$inline) (:type-prescription ash) (:rewrite bitops::loghead-of-0-i) (:rewrite acl2::equal-constant-+) @@ -2060,7 +2060,7 @@ ;; Start: binding hypotheses. (equal start-rip (rip x86)) ;; get-prefixes-alt: - (equal three-vals-of-get-prefixes (get-prefixes-alt start-rip 0 5 x86)) + (equal three-vals-of-get-prefixes (get-prefixes-alt start-rip 0 15 x86)) (equal flg-get-prefixes (mv-nth 0 three-vals-of-get-prefixes)) (equal prefixes (mv-nth 1 three-vals-of-get-prefixes)) (equal x86-1 (mv-nth 2 three-vals-of-get-prefixes)) @@ -2146,7 +2146,7 @@ (mv-nth 1 (las-to-pas - (create-canonical-address-list 5 (xr :rip 0 x86)) + (create-canonical-address-list 15 (xr :rip 0 x86)) :x (cpl x86) (double-rewrite x86))) (open-qword-paddr-list (gather-all-paging-structure-qword-addresses (double-rewrite x86)))) @@ -2154,7 +2154,7 @@ (mv-nth 0 (las-to-pas - (create-canonical-address-list 5 (xr :rip 0 x86)) + (create-canonical-address-list 15 (xr :rip 0 x86)) :x (cpl x86) (double-rewrite x86))))) (equal (x86-fetch-decode-execute x86) (top-level-opcode-execute diff --git a/books/projects/x86isa/tools/execution/examples/nop-sequence/acl2-customization.lsp b/books/projects/x86isa/tools/execution/examples/nop-sequence/acl2-customization.lsp new file mode 100644 index 00000000000..977a63070f1 --- /dev/null +++ b/books/projects/x86isa/tools/execution/examples/nop-sequence/acl2-customization.lsp @@ -0,0 +1,7 @@ +;; Shilpi Goel + +(ld "~/acl2-customization.lsp" :ld-missing-input-ok t) +(set-deferred-ttag-notes t state) + +(ld "cert.acl2" :ld-missing-input-ok t) +(in-package "X86ISA") diff --git a/books/projects/x86isa/tools/execution/examples/nop-sequence/cert.acl2 b/books/projects/x86isa/tools/execution/examples/nop-sequence/cert.acl2 new file mode 100644 index 00000000000..2ad3dbde7d5 --- /dev/null +++ b/books/projects/x86isa/tools/execution/examples/nop-sequence/cert.acl2 @@ -0,0 +1,9 @@ +;; Shilpi Goel + +;; ====================================================================== + +(set-waterfall-parallelism t) +(include-book "../../../../portcullis/sharp-dot-constants") +;; cert-flags: ? t :ttags (:include-raw :syscall-exec :other-non-det :undef-flg :instrument) :skip-proofs-okp t + +;; ====================================================================== \ No newline at end of file diff --git a/books/projects/x86isa/tools/execution/examples/nop-sequence/nop.lsp b/books/projects/x86isa/tools/execution/examples/nop-sequence/nop.lsp new file mode 100644 index 00000000000..017129fa9cd --- /dev/null +++ b/books/projects/x86isa/tools/execution/examples/nop-sequence/nop.lsp @@ -0,0 +1,78 @@ +;; Author: Shilpi Goel + +;; Checking if the "Recommended multi-byte sequence of NOP +;; Instruction" (Intel Vol. 2B, NOP Instruction-Set Reference) is +;; supported by the x86isa model: + +(in-package "X86ISA") + +(include-book "../../top" :ttags :all) + +;; ====================================================================== + +;; Set the OS-Info: +(!programmer-level-mode t x86) + +;; Recommended NOP Sequence: + +;; 1. #x66 #x90 +;; 2. #x0F #x1F #x00 +;; 3. #x0F #x1F #x40 #x00 +;; 4. #x0F #x1F #x44 #x00 #x00 +;; 5. #x66 #x0F #x1F #x44 #x00 #x00 +;; 6. #x0F #x1F #x80 #x00 #x00 #x00 #x00 +;; 7. #x0F #x1F #x84 #x00 #x00 #x00 #x00 #x00 +;; 8. #x66 #x0F #x1F #x84 #x00 #x00 #x00 #x00 #x00 + +(defconst *nop* + '( + ;; RIP: 0 + #x66 #x90 + ;; RIP: 2 + #x0F #x1F #x00 + ;; RIP: 5 + #x0F #x1F #x40 #x00 + ;; RIP: 9 + #x0F #x1F #x44 #x00 #x00 + ;; RIP: 0E + #x66 #x0F #x1F #x44 #x00 #x00 + ;; RIP: 14 + #x0F #x1F #x80 #x00 #x00 #x00 #x00 + ;; RIP: 1B + #x0F #x1F #x84 #x00 #x00 #x00 #x00 #x00 + ;; The following instruction is the odd one out. Note #x67 prefix. + ;; RIP: 23 + #x67 #x66 #x0F #x1F #x84 #x00 #x00 #x00 #x00 #x00 + ;; RIP: 2D + #x66 #x0F #x1F #x84 #x00 #x00 #x00 #x00 #x00)) + +;; Initialize the x86 state: +(init-x86-state + ;; Status (MS and fault field) + nil + ;; Start Address --- set the RIP to this address + 0 + ;; Halt Address --- overwrites this address by #xF4 (HLT) + (len *nop*) + ;; Initial values of General-Purpose Registers + nil + ;; Control Registers + nil + ;; Model-Specific Registers + nil + ;; Rflags Register + 2 + ;; Memory image + (pairlis$ + (create-canonical-address-list (len *nop*) 0) + *nop*) + ;; x86 state + x86) + +(!log-file-name "nop.log") +(log_instr) + +;; Run the program for up to 1000000 steps or till the machine halts, whatever comes first: +;; (x86-run-steps 1000000 x86) + +;; ====================================================================== diff --git a/books/projects/x86isa/utils/decoding-utilities.lisp b/books/projects/x86isa/utils/decoding-utilities.lisp index 1f98df0c488..de40c24ea9b 100644 --- a/books/projects/x86isa/utils/decoding-utilities.lisp +++ b/books/projects/x86isa/utils/decoding-utilities.lisp @@ -1638,23 +1638,23 @@ v1: VEX128 & SSE forms only exist (no VEX256), when can t be inferred :short "Functions to detect and decode ModR/M and SIB bytes" (defconst *prefixes-layout* - '((:num-prefixes 0 3) ;; Number of prefixes - (:group-1-prefix 3 8) ;; Lock, Repeat prefix - (:group-2-prefix 11 8) ;; Segment Override prefix - (:group-3-prefix 19 8) ;; Operand-Size Override prefix - (:group-4-prefix 27 8) ;; Address-Size Override prefix - (:next-byte 35 8) ;; Byte following the prefixes + '((:num-prefixes 0 4) ;; Number of prefixes + (:group-1-prefix 4 8) ;; Lock, Repeat prefix + (:group-2-prefix 12 8) ;; Segment Override prefix + (:group-3-prefix 20 8) ;; Operand-Size Override prefix + (:group-4-prefix 28 8) ;; Address-Size Override prefix + (:next-byte 36 8) ;; Byte following the prefixes )) (defthm prefixes-table-ok - (layout-constant-alistp *prefixes-layout* 0 43) + (layout-constant-alistp *prefixes-layout* 0 44) :rule-classes nil) (defmacro prefixes-slice (flg prefixes) - (slice flg prefixes 43 *prefixes-layout*)) + (slice flg prefixes 44 *prefixes-layout*)) (defmacro !prefixes-slice (flg val reg) - (!slice flg val reg 43 *prefixes-layout*)) + (!slice flg val reg 44 *prefixes-layout*)) ) diff --git a/books/projects/x86isa/utils/utilities.lisp b/books/projects/x86isa/utils/utilities.lisp index afa22e02459..0ffdaa26dbe 100644 --- a/books/projects/x86isa/utils/utilities.lisp +++ b/books/projects/x86isa/utils/utilities.lisp @@ -554,7 +554,7 @@ constants and functions; it also proves some associated lemmas.

" (cons 'progn (np-defs lst))) (defuns-np 1 2 3 4 5 6 8 9 11 12 16 17 18 20 21 22 24 25 26 27 28 - 30 32 33 35 43 45 47 48 49 51 52 59 60 64 65 80 112 120 128) + 30 32 33 35 43 44 45 47 48 49 51 52 59 60 64 65 80 112 120 128) (defmacro n-size (n x)