Merge remote-tracking branch 'remotes/origin/testing'

books/projects/x86isa/machine/guard-helpers.lisp

@@ -51,6 +51,55 @@
    (:mix (:nat a 8) (:nat b 8) (:nat c 8) (:nat d 8)))
   :rule-classes :linear)
 
+(def-gl-export rm48-guard-proof-helper
+  :hyp (and (n08p a) (n08p b) (n32p c))
+  :concl (equal (logior a (ash b 8) (ash c 16))
+                (logior a (ash (logior b (ash c 8)) 8)))
+  :g-bindings
+  (gl::auto-bindings
+   (:mix (:nat a 32) (:nat b 32) (:nat c 32)))
+  :rule-classes :linear)
+
+(def-gl-export rb-and-rm48-helper-1
+  :hyp (and (n08p a) (n08p b) (n08p c) (n08p d)
+            (n08p e) (n08p f))
+  :concl (equal (logior
+                 a
+                 (ash (logior
+                       b
+                       (ash (logior
+                             c
+                             (ash (logior
+                                   d (ash (logior e (ash f 8)) 8)) 8)) 8)) 8))
+                (logior
+                 a
+                 (ash b 8)
+                 (ash (logior
+                       c
+                       (ash (logior d (ash (logior e (ash f 8)) 8))
+                            8)) 16)))
+  :g-bindings
+  (gl::auto-bindings
+   (:mix (:nat a 8) (:nat b 8) (:nat c 8) (:nat d 8)
+         (:nat e 8) (:nat f 8))))
+
+(def-gl-export rb-and-rm48-helper-2
+  :hyp (and (n08p a) (n08p b) (n08p c) (n08p d)
+            (n08p e) (n08p f))
+  :concl (<
+          (logior
+           a
+           (ash b 8)
+           (ash (logior
+                 c
+                 (ash (logior d (ash (logior e (ash f 8)) 8))
+                      8)) 16))
+          #.*2^48*)
+  :g-bindings
+  (gl::auto-bindings
+   (:mix (:nat a 8) (:nat b 8) (:nat c 8) (:nat d 8)
+         (:nat e 8) (:nat f 8))))
+
 (def-gl-export rb-and-rvm64-helper
   :hyp (and (n08p a) (n08p b) (n08p c) (n08p d)
             (n08p e) (n08p f) (n08p g) (n08p h))
@@ -83,12 +132,61 @@
    (:mix (:nat a 32) (:nat b 32)))
   :rule-classes :linear)
 
-(in-theory (e/d ()                
+(def-gl-export rm80-guard-proof-helper
+  :hyp (and (n08p a) (n08p b) (n64p c))
+  :concl (equal (logior a (ash b 8) (ash c 16))
+                (logior a (ash (logior b (ash c 8)) 8)))
+  :g-bindings
+  (gl::auto-bindings
+   (:mix (:nat a 64) (:nat b 64) (:nat c 64)))
+  :rule-classes :linear)
+
+(def-gl-export rm80-in-system-level-mode-guard-proof-helper
+  :hyp (and (n08p a) (n08p b) (n08p c) (n08p d) (n08p e)
+            (n08p f) (n08p g) (n08p h) (n08p i) (n08p j))
+  :concl (<
+          (logior a
+                  (ash b 8)
+                  (ash (logior
+                        c
+                        (ash
+                         (logior
+                          d
+                          (ash
+                           (logior
+                            e
+                            (ash
+                             (logior
+                              f
+                              (ash
+                               (logior g
+                                       (ash (logior
+                                             h (ash
+                                                (logior i (ash j 8))
+                                                8)) 8)) 8)) 8)) 8)) 8)) 16))
+          *2^80*)
+  :g-bindings (gl::auto-bindings
+               (:mix (:nat a 8)
+                     (:nat b 8)
+                     (:nat c 8)
+                     (:nat d 8)
+                     (:nat e 8)
+                     (:nat f 8)
+                     (:nat g 8)
+                     (:nat h 8)
+                     (:nat i 8)
+                     (:nat j 8))))
+
+(in-theory (e/d ()
                 (rm16-guard-proof-helper
-                 rb-and-rvm32-helper                
+                 rm48-guard-proof-helper
+                 rb-and-rm48-helper-1
+                 rb-and-rm48-helper-2
+                 rb-and-rvm32-helper
                  rm32-guard-proof-helper
                  rb-and-rvm64-helper
-                 rm64-guard-proof-helper)))
+                 rm64-guard-proof-helper
+                 rm80-in-system-level-mode-guard-proof-helper)))
 
 (def-gl-export rm32-rb-system-level-mode-proof-helper
   :hyp (and (n08p a)

books/projects/x86isa/machine/instructions/fp/x86-fp-arithmetic-instructions.lisp

@@ -69,7 +69,9 @@
         t)
        ((mv flg0 xmm/mem (the (integer 0 4) increment-RIP-by) (the (signed-byte 64) ?v-addr) x86)
         (x86-operand-from-modr/m-and-sib-bytes
-         #.*xmm-access* operand-size inst-ac? p2 p4? temp-rip rex-byte r/m mod sib
+         #.*xmm-access* operand-size inst-ac?
+         nil ;; Not a memory pointer operand
+         p2 p4? temp-rip rex-byte r/m mod sib
          0 ;; No immediate operand
          x86))
        ((when flg0)
@@ -198,7 +200,9 @@
             (the (integer 0 4) increment-RIP-by)
             (the (signed-byte 64) ?v-addr) x86)
         (x86-operand-from-modr/m-and-sib-bytes
-         #.*xmm-access* 16 inst-ac? p2 p4? temp-rip rex-byte r/m mod sib
+         #.*xmm-access* 16 inst-ac?
+         nil ;; Not a memory pointer operand
+         p2 p4? temp-rip rex-byte r/m mod sib
          0 ;; No immediate operand
          x86))
 
@@ -363,7 +367,9 @@
             (the (integer 0 4) increment-RIP-by)
             (the (signed-byte 64) ?v-addr) x86)
         (x86-operand-from-modr/m-and-sib-bytes
-         #.*xmm-access* 16 inst-ac? p2 p4? temp-rip rex-byte r/m mod sib
+         #.*xmm-access* 16 inst-ac?
+         nil ;; Not a memory pointer operand
+         p2 p4? temp-rip rex-byte r/m mod sib
          0 ;; No immediate operand
          x86))
 
@@ -507,7 +513,9 @@
         t)
        ((mv flg0 xmm/mem (the (integer 0 4) increment-RIP-by) (the (signed-byte 64) ?v-addr) x86)
         (x86-operand-from-modr/m-and-sib-bytes
-         #.*xmm-access* operand-size inst-ac? p2 p4? temp-rip rex-byte r/m mod sib
+         #.*xmm-access* operand-size inst-ac?
+         nil ;; Not a memory pointer operand
+         p2 p4? temp-rip rex-byte r/m mod sib
          0 ;; No immediate operand
          x86))
 
@@ -598,7 +606,9 @@
             (the (integer 0 4) increment-RIP-by)
             (the (signed-byte 64) ?v-addr) x86)
         (x86-operand-from-modr/m-and-sib-bytes
-         #.*xmm-access* 16 inst-ac? p2 p4? temp-rip rex-byte r/m mod sib
+         #.*xmm-access* 16 inst-ac?
+         nil ;; Not a memory pointer operand
+         p2 p4? temp-rip rex-byte r/m mod sib
          0 ;; No immediate operand
          x86))
 
@@ -732,7 +742,9 @@
             (the (integer 0 4) increment-RIP-by)
             (the (signed-byte 64) ?v-addr) x86)
         (x86-operand-from-modr/m-and-sib-bytes
-         #.*xmm-access* 16 inst-ac? p2 p4? temp-rip rex-byte r/m mod sib
+         #.*xmm-access* 16 inst-ac?
+         nil ;; Not a memory pointer operand
+         p2 p4? temp-rip rex-byte r/m mod sib
          0 ;; No immediate operand
          x86))
 

books/projects/x86isa/machine/instructions/fp/x86-fp-bitscan-instructions.lisp

@@ -104,7 +104,9 @@
             (the (signed-byte 64) ?v-addr)
             x86)
         (x86-operand-from-modr/m-and-sib-bytes
-         #.*rgf-access* operand-size inst-acc? p2 p4? temp-rip rex-byte r/m mod sib
+         #.*rgf-access* operand-size inst-acc?
+         nil ;; Not a memory pointer operand
+         p2 p4? temp-rip rex-byte r/m mod sib
          0 ;; No immediate operand
          x86))
 

books/projects/x86isa/machine/instructions/fp/x86-fp-convert-instructions.lisp

@@ -72,7 +72,9 @@
         t)
        ((mv flg0 xmm/mem (the (integer 0 4) increment-RIP-by) (the (signed-byte 64) ?v-addr) x86)
         (x86-operand-from-modr/m-and-sib-bytes
-         #.*xmm-access* xmm/mem-size inst-ac? p2 p4? temp-rip rex-byte r/m mod sib
+         #.*xmm-access* xmm/mem-size inst-ac?
+         nil ;; Not a memory pointer operand
+         p2 p4? temp-rip rex-byte r/m mod sib
          0 ;; No immediate operand
          x86))
 
@@ -201,7 +203,9 @@
         t)
        ((mv flg0 reg/mem (the (integer 0 4) increment-RIP-by) (the (signed-byte 64) ?v-addr) x86)
         (x86-operand-from-modr/m-and-sib-bytes
-         #.*rgf-access* reg/mem-size inst-ac? p2 p4? temp-rip rex-byte r/m mod sib
+         #.*rgf-access* reg/mem-size inst-ac?
+         nil ;; Not a memory pointer operand
+         p2 p4? temp-rip rex-byte r/m mod sib
          0 ;; No immediate operand
          x86))
 
@@ -316,7 +320,9 @@
         t)
        ((mv flg0 xmm/mem (the (integer 0 4) increment-RIP-by) (the (signed-byte 64) ?v-addr) x86)
         (x86-operand-from-modr/m-and-sib-bytes
-         #.*xmm-access* xmm/mem-size inst-ac? p2 p4? temp-rip rex-byte r/m mod sib
+         #.*xmm-access* xmm/mem-size inst-ac?
+         nil ;; Not a memory pointer operand
+         p2 p4? temp-rip rex-byte r/m mod sib
          0 ;; No immediate operand
          x86))
 
@@ -412,7 +418,9 @@
             (the (integer 0 4) increment-RIP-by)
             (the (signed-byte 64) ?v-addr) x86)
         (x86-operand-from-modr/m-and-sib-bytes
-         #.*xmm-access* 8 inst-ac? p2 p4? temp-rip rex-byte r/m mod sib
+         #.*xmm-access* 8 inst-ac?
+         nil ;; Not a memory pointer operand
+         p2 p4? temp-rip rex-byte r/m mod sib
          0 ;; No immediate operand
          x86))
 
@@ -521,7 +529,9 @@
             (the (integer 0 4) increment-RIP-by)
             (the (signed-byte 64) ?v-addr) x86)
         (x86-operand-from-modr/m-and-sib-bytes
-         #.*xmm-access* 16 inst-ac? p2 p4? temp-rip rex-byte r/m mod sib
+         #.*xmm-access* 16 inst-ac?
+         nil ;; Not a memory pointer operand
+         p2 p4? temp-rip rex-byte r/m mod sib
          0 ;; No immediate operand
          x86))
 

books/projects/x86isa/machine/instructions/fp/x86-fp-logical-instructions.lisp

@@ -80,7 +80,9 @@
             (the (integer 0 4) increment-RIP-by)
             (the (signed-byte 64) ?v-addr) x86)
         (x86-operand-from-modr/m-and-sib-bytes
-         #.*xmm-access* 16 inst-ac? p2 p4? temp-rip rex-byte r/m mod sib
+         #.*xmm-access* 16 inst-ac?
+         nil ;; Not a memory pointer operand
+         p2 p4? temp-rip rex-byte r/m mod sib
          0 ;; No immediate operand
          x86))
 
@@ -219,7 +221,9 @@
 
        ((mv flg0 xmm/mem (the (integer 0 4) increment-RIP-by) (the (signed-byte 64) ?v-addr) x86)
         (x86-operand-from-modr/m-and-sib-bytes
-         #.*xmm-access* operand-size inst-ac? p2 p4? temp-rip rex-byte r/m mod sib
+         #.*xmm-access* operand-size inst-ac?
+         nil ;; Not a memory pointer operand
+         p2 p4? temp-rip rex-byte r/m mod sib
          1 ;; One-byte immediate operand
          x86))
 
@@ -326,7 +330,9 @@
             (the (integer 0 4) increment-RIP-by)
             (the (signed-byte 64) ?v-addr) x86)
         (x86-operand-from-modr/m-and-sib-bytes
-         #.*xmm-access* 16 inst-ac? p2 p4? temp-rip rex-byte r/m mod sib
+         #.*xmm-access* 16 inst-ac?
+         nil ;; Not a memory pointer operand
+         p2 p4? temp-rip rex-byte r/m mod sib
          1 ;; One-byte immediate operand
          x86))
 
@@ -491,7 +497,9 @@
             (the (integer 0 4) increment-RIP-by)
             (the (signed-byte 64) ?v-addr) x86)
         (x86-operand-from-modr/m-and-sib-bytes
-         #.*xmm-access* 16 inst-ac? p2 p4? temp-rip rex-byte r/m mod sib
+         #.*xmm-access* 16 inst-ac?
+         nil ;; Not a memory pointer operand
+         p2 p4? temp-rip rex-byte r/m mod sib
          1 ;; One-byte immediate operand
          x86))
 
@@ -636,7 +644,9 @@
 
        ((mv flg0 xmm/mem (the (integer 0 4) increment-RIP-by) (the (signed-byte 64) ?v-addr) x86)
         (x86-operand-from-modr/m-and-sib-bytes
-         #.*xmm-access* operand-size inst-ac? p2 p4? temp-rip rex-byte r/m mod sib
+         #.*xmm-access* operand-size inst-ac?
+         nil ;; Not a memory pointer operand
+         p2 p4? temp-rip rex-byte r/m mod sib
          0 ;; No immediate operand
          x86))
 

books/projects/x86isa/machine/instructions/fp/x86-fp-mov-instructions.lisp

@@ -53,7 +53,9 @@
 
        ((mv flg0 xmm/mem (the (integer 0 4) increment-RIP-by) (the (signed-byte 64) ?v-addr) x86)
         (x86-operand-from-modr/m-and-sib-bytes
-         #.*xmm-access* operand-size inst-ac? p2 p4? temp-rip rex-byte r/m mod sib
+         #.*xmm-access* operand-size inst-ac?
+         nil ;; Not a memory pointer operand
+         p2 p4? temp-rip rex-byte r/m mod sib
          0 ;; No immediate operand
          x86))
 
@@ -229,7 +231,9 @@
             (the (signed-byte 64) ?v-addr)
             x86)
         (x86-operand-from-modr/m-and-sib-bytes
-         #.*xmm-access* 16 inst-ac? p2 p4? temp-rip rex-byte r/m mod sib
+         #.*xmm-access* 16 inst-ac?
+         nil ;; Not a memory pointer operand
+         p2 p4? temp-rip rex-byte r/m mod sib
          0 ;; No immediate operand
          x86))
 
@@ -400,7 +404,9 @@
             (the (signed-byte 64) ?v-addr)
             x86)
         (x86-operand-from-modr/m-and-sib-bytes
-         #.*xmm-access* 16 inst-ac? p2 p4? temp-rip rex-byte r/m mod sib
+         #.*xmm-access* 16 inst-ac?
+         nil ;; Not a memory pointer operand
+         p2 p4? temp-rip rex-byte r/m mod sib
          0 ;; No immediate operand
          x86))
 
@@ -577,7 +583,9 @@
             (the (signed-byte 64) ?v-addr)
             x86)
         (x86-operand-from-modr/m-and-sib-bytes
-         #.*xmm-access* 8 inst-ac? p2 p4? temp-rip rex-byte r/m mod sib
+         #.*xmm-access* 8 inst-ac?
+         nil ;; Not a memory pointer operand
+         p2 p4? temp-rip rex-byte r/m mod sib
          0 ;; No immediate operand
          x86))
 
@@ -738,7 +746,9 @@
             (the (signed-byte 64) ?v-addr)
             x86)
         (x86-operand-from-modr/m-and-sib-bytes
-         #.*xmm-access* 8 inst-ac? p2 p4? temp-rip rex-byte r/m mod sib
+         #.*xmm-access* 8 inst-ac?
+         nil ;; Not a memory pointer operand
+         p2 p4? temp-rip rex-byte r/m mod sib
          0 ;; No immediate operand
          x86))
 

books/projects/x86isa/machine/instructions/fp/x86-fp-mxcsr-instructions.lisp

@@ -49,7 +49,9 @@
             (the (signed-byte 64) v-addr)
             x86)
         (x86-operand-from-modr/m-and-sib-bytes
-         #.*rgf-access* 4 inst-ac? p2 p4? temp-rip rex-byte r/m mod sib
+         #.*rgf-access* 4 inst-ac?
+         nil ;; Not a memory pointer operand
+         p2 p4? temp-rip rex-byte r/m mod sib
          0 ;; No immediate operand
          x86))
 
@@ -87,7 +89,9 @@
            (b* ((mxcsr (the (unsigned-byte 32) (mxcsr x86)))
                 ((mv flg1 x86)
                  (x86-operand-to-reg/mem
-                  4 inst-ac? mxcsr v-addr rex-byte r/m mod x86))
+                  4 inst-ac?
+                  nil ;; Not a memory pointer operand
+                  mxcsr v-addr rex-byte r/m mod x86))
                 ;; Note: If flg1 is non-nil, we bail out without changing the
                 ;; x86 state.
                 ((when flg1)