Merge pull request #741 from shigoel/collaborate

Fixed a bug in the implementation of opcode 0x90, plus merging in some edits from Alessandro Coglio.

books/projects/x86isa/machine/instructions/x86-exchange-instructions.lisp

@@ -49,12 +49,9 @@
   ;; 90 +rw: XCHG ax, r16
   ;; 90 +rd: XCHG eax/rax, r32/r64
 
-  ;; Note that opcode #x90 is XCHG rAX, rAX, i.e. NOP.  However, we
-  ;; choose to model it separately as a NOP for the sake of execution
-  ;; efficiency.
+  ;; Note that opcode #x90 with REX.B = 0 is XCHG rAX, rAX, i.e., NOP.
 
   :parents (one-byte-opcodes)
-  :guard-debug t
   :guard-hints (("Goal" :in-theory (e/d* () (not))))
 
   :returns (x86 x86p :hyp (and (x86p x86)
@@ -65,6 +62,8 @@
                                       'x86-xchg)
     (add-to-implemented-opcodes-table 'XCHG #x87 '(:nil nil)
                                       'x86-xchg)
+    (add-to-implemented-opcodes-table 'XCHG #x90 '(:nil nil)
+                                      'x86-xchg)
     (add-to-implemented-opcodes-table 'XCHG #x91 '(:nil nil)
                                       'x86-xchg)
     (add-to-implemented-opcodes-table 'XCHG #x92 '(:nil nil)
@@ -288,39 +287,6 @@
 ;; INSTRUCTION: NOP
 ;; ======================================================================
 
-(def-inst x86-nop
-
-  ;; Note: With operand-size override prefix (#x66), the single byte
-  ;; NOP instruction is equivalent to XCHG ax, ax.
-
-  ;; Op/En: NP
-  ;; 90
-
-  :parents (one-byte-opcodes)
-  :guard-hints (("Goal" :in-theory (e/d (rim08 rim32) ())))
-
-  :returns (x86 x86p :hyp (and (x86p x86)
-                               (canonical-address-p temp-rip)))
-  :implemented
-  (add-to-implemented-opcodes-table 'NOP #x90 '(:nil nil) 'x86-nop)
-
-  :body
-
-
-  (b* ((ctx 'x86-nop)
-       (lock? (equal #.*lock* (prefixes-slice :group-1-prefix prefixes)))
-       ((when lock?)
-        (!!ms-fresh :lock-prefix prefixes)))
-
-    ;; We don't need to check for valid length for one-byte
-    ;; instructions.  The length will be more than 15 only if
-    ;; get-prefixes fetches 15 prefixes, and that error will be
-    ;; caught in x86-fetch-decode-execute, that is, before control
-    ;; reaches this function.
-
-    ;; Update the x86 state:
-    (!rip temp-rip x86)))
-
 (def-inst x86-two-byte-nop
 
   ;; Op/En: NP
@@ -368,18 +334,51 @@
                    :exec (<= #.*2^47*
                              (the (signed-byte
                                    #.*max-linear-address-size+1*)
-                               temp-rip))))
+                                  temp-rip))))
         (!!ms-fresh :next-rip-invalid temp-rip))
        ((the (signed-byte #.*max-linear-address-size+1*) addr-diff)
         (-
          (the (signed-byte #.*max-linear-address-size*)
-           temp-rip)
+              temp-rip)
          (the (signed-byte #.*max-linear-address-size*)
-           start-rip)))
+              start-rip)))
        ((when (< 15 addr-diff))
         (!!ms-fresh :instruction-length addr-diff))
        ;; Update the x86 state:
        (x86 (!rip temp-rip x86)))
     x86))
 
+;; (def-inst x86-nop
+
+;;   ;; Note: With operand-size override prefix (#x66), the single byte
+;;   ;; NOP instruction is equivalent to XCHG ax, ax.
+
+;;   ;; Op/En: NP
+;;   ;; 90
+
+;;   :parents (one-byte-opcodes)
+;;   :guard-hints (("Goal" :in-theory (e/d (rim08 rim32) ())))
+
+;;   :returns (x86 x86p :hyp (and (x86p x86)
+;;                                (canonical-address-p temp-rip)))
+;;   :implemented
+;;   (add-to-implemented-opcodes-table 'NOP #x90 '(:nil nil) 'x86-nop)
+
+;;   :body
+
+
+;;   (b* ((ctx 'x86-nop)
+;;        (lock? (equal #.*lock* (prefixes-slice :group-1-prefix prefixes)))
+;;        ((when lock?)
+;;         (!!ms-fresh :lock-prefix prefixes)))
+
+;;     ;; We don't need to check for valid length for one-byte
+;;     ;; instructions.  The length will be more than 15 only if
+;;     ;; get-prefixes fetches 15 prefixes, and that error will be
+;;     ;; caught in x86-fetch-decode-execute, that is, before control
+;;     ;; reaches this function.
+
+;;     ;; Update the x86 state:
+;;     (!rip temp-rip x86)))
+
 ;; ======================================================================

books/projects/x86isa/machine/x86.lisp

@@ -1998,14 +1998,14 @@
          x86))))
 
 
-    (#x90
-     "#x90:  (XCHG rAX/R8) or (NOP) or (PAUSE)"
-     (x86-nop start-rip temp-rip prefixes rex-byte opcode
-              modr/m sib x86))
+    ;; (#x90
+    ;;  "#x90:  (XCHG rAX/R8) or (NOP) or (PAUSE)"
+    ;;  (x86-nop start-rip temp-rip prefixes rex-byte opcode
+    ;;           modr/m sib x86))
 
 
-    ((#x91 #x92 #x93 #x94 #x95 #x96 #x97)
-     "#x91 -- #x97:  (XCHG .. ..)"
+    ((#x90 #x91 #x92 #x93 #x94 #x95 #x96 #x97)
+     "#x90 -- #x97:  (XCHG .. ..)"
      (x86-xchg start-rip temp-rip prefixes rex-byte opcode modr/m sib
                x86))
 

books/projects/x86isa/proofs/dataCopy/dataCopy.lisp

@@ -369,7 +369,9 @@
        (equal (xr :fault 0 x86) nil)
        ;; We are poised to run the copyData sub-routine.
        (equal (xr :rip 0 x86) addr)
-       (unsigned-byte-p 32 n)
+       ;; [Shilpi] This used to be (unsigned-byte-p 32 n), but I
+       ;; needed to make this change after fixing the NOP/XCHG bug.
+       (unsigned-byte-p 14 n) ;; 32?
        (equal (xr :rgf *rdx* x86) n)
        ;; All the stack addresses are canonical.
        (canonical-address-p (+ -8 (xr :rgf *rsp* x86)))
@@ -509,14 +511,24 @@
                             *copyData* x86)))
   :rule-classes :forward-chaining)
 
+(local
+ (defthm rdx-logsquash-lemma
+   (implies (unsigned-byte-p 14 rdx)
+            (equal (logext 64 (bitops::logsquash 16 (ash rdx 2)))
+                   0))
+   :hints (("Goal" :in-theory (e/d* (bitops::ihsext-recursive-redefs
+                                     bitops::ihsext-inductions
+                                     unsigned-byte-p)
+                                    ())))))
+
 (defthm effects-copyData-pre
   (implies
    (preconditions n addr x86)
    (equal
     (x86-run (pre-clk n) x86)
     (if (< 0 n)
         (XW
-         :RGF *RAX* (ASH (XR :RGF *RDX* X86) 2)
+         :RGF *RAX* (LOGHEAD 16 (ASH (XR :RGF *RDX* X86) 2))
          (XW
           :RGF *RSP* (+ -8 (XR :RGF *RSP* X86))
           (XW
@@ -602,6 +614,8 @@
                                     x86-operand-to-reg/mem
                                     wr64
                                     wr32
+                                    wr16
+                                    rr16
                                     rr32
                                     rr64
                                     rm32

books/projects/x86isa/tools/execution/examples/nop-sequence/nop.lsp

@@ -69,10 +69,54 @@
  ;; x86 state
  x86)
 
-(!log-file-name "nop.log") 
+(!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)
 
 ;; ======================================================================
+
+(defconst *xchg*
+  '(
+    ;;     #x48 #xc7 #xc0 #x01 #x00 #x00 #x00 ;; movq	$0x1, %rax
+    ;;     #x49 #xb8 #xff #xff #xff #xff #x00 #x00 #x00 #x00 ;; movabsq	$0xffffffff, %r8
+    ;;     #x49 #x90 ;; xchgq	%r8, %rax
+
+    #x48 #xc7 #xc0 #x01 #x00 #x00 #x00 ; movq	$0x1, %rax
+    #x49 #xb8 #xff #xff #xff #xff #x00 #x00 #x00 #x00 ; movabsq	$0xffffffff, %r8
+    #x66 #x41 #x90 ; xchgw	%r8w, %ax
+
+    ))
+
+
+;; 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 *xchg*)
+ ;; 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 *xchg*) 0)
+  *xchg*)
+ ;; x86 state
+ x86)
+
+(!log-file-name "xchg.log")
+(log_instr)
+
+;; Run the program for up to 1000000 steps or till the machine halts, whatever comes first:
+;; (x86-run-steps 1000000 x86)
+
+;; ----------------------------------------------------------------------

books/projects/x86isa/tools/execution/examples/nop-sequence/xchg.c

@@ -0,0 +1,38 @@
+// Shilpi Goel
+
+// gcc xchg.c -o xchg.o
+
+#include <stdio.h>
+#include <stdint.h>
+
+// See pre-defined macros supported by your GCC using:
+// gcc -dM -E - < /dev/null
+
+uint64_t xchg (void) {
+
+  uint64_t n,m;
+  __asm__ volatile
+    (
+     "mov  $0x1,        %%rax\n\t"
+     "mov  $0xFFFFFFFF, %%r8\n\t"
+     "xchg %%ax,       %%r8w\n\t"
+     "mov  %%r8,        %1\n\t"
+     : "=a"(n),"=g"(m)  // output list
+
+     :  // input list
+
+     : "cc", "memory");
+
+  printf("\nValue in rax: 0x%llx\n", n);
+  printf("\nValue in r8:  0x%llx\n", m);
+
+  return (0);
+}
+
+int main () {
+
+  xchg();
+
+  return 0;
+
+}