#77: wip

sdasgup3 · Jun 7, 2018 · 9af047a · 9af047a
1 parent a19b5de
commit 9af047a
Show file tree

Hide file tree

Showing 13 changed files with 87,119 additions and 145 deletions.
diff --git a/x86-semantics/semantics/immediateInstructions/pclmulqdq_xmm_xmm_imm8.k b/x86-semantics/semantics/immediateInstructions/pclmulqdq_xmm_xmm_imm8.k
@@ -67,78 +67,6 @@ module PCLMULQDQ-XMM-XMM-IMM8
             computePCLMULQDQ2(TEMP1, TEMP2, mi(128, 0), 64, 126) 
             ), R3)
   ...</k>
-
-  /*
-    For i = 0 to 63 {
-        TmpB [ i ]←(TEMP1[ 0 ] and TEMP2[ i ]);
-        For j = 1 to i {
-            TmpB [ i ]←TmpB [ i ] xor (TEMP1[ j ] and TEMP2[ i - j ])
-        }
-        DEST[ i ]←TmpB[ i ];
-    }
-  */   
-  syntax MInt ::= computePCLMULQDQ1(MInt, MInt, MInt, Int, Int) [function]
-  syntax MInt ::= computePCLMULQDQ1Refine(MInt, MInt, Int) [function]
-
-  rule computePCLMULQDQ1(TEMP1:MInt, TEMP2:MInt, DEST:MInt, N:Int, N:Int) => DEST
-
-  rule computePCLMULQDQ1(TEMP1:MInt, TEMP2:MInt, DEST:MInt, M:Int, N:Int) =>
-    computePCLMULQDQ1( 
-        TEMP1, TEMP2, plugInMask(DEST, computePCLMULQDQ1Refine(TEMP1, TEMP2, M), M), M +Int 1, N)
-
-  rule computePCLMULQDQ1Refine(TEMP1:MInt, TEMP2:MInt, M:Int) =>
-  refineHelper(TEMP1, TEMP2, 1, M, 
-        andMInt( 
-          extractMInt(TEMP1, 63, 64), extractMInt(TEMP2, 63 -Int M, 64 -Int M) 
-          )
-      )
-
-  /*
-     For i = 64 to 126 {
-    TmpB [ i ]←0;
-    For j = i - 63 to 63 {
-        TmpB [ i ]←TmpB [ i ] xor (TEMP1[ j ] and TEMP2[ i - j ])
-    }
-    DEST[ i ]←TmpB[ i ];
-  }
-  */
-
-  syntax MInt ::= computePCLMULQDQ2(MInt, MInt, MInt, Int, Int) [function]
-  syntax MInt ::= computePCLMULQDQ2Refine(MInt, MInt, Int) [function]
-
-  rule computePCLMULQDQ2(TEMP1:MInt, TEMP2:MInt, DEST:MInt, N:Int, N:Int) => DEST
-
-  rule computePCLMULQDQ2(TEMP1:MInt, TEMP2:MInt, DEST:MInt, M:Int, N:Int) =>
-    computePCLMULQDQ2( 
-        TEMP1, TEMP2, plugInMask(DEST, computePCLMULQDQ2Refine(TEMP1, TEMP2, M), M), M +Int 1, N)
-
-  rule computePCLMULQDQ2Refine(TEMP1:MInt, TEMP2:MInt, M:Int) =>
-  refineHelper(TEMP1, TEMP2, M -Int 63, 63,  mi(1, 0))
-
-
-  // Utils
-  syntax MInt ::= refineHelper(MInt, MInt, Int, Int, MInt) [function]
-  rule refineHelper(TEMP1:MInt, TEMP2:MInt, Q:Int, Q:Int,
-      RES:MInt) => RES
-
-  rule refineHelper(TEMP1:MInt, TEMP2:MInt, P:Int, Q:Int,
-      RES:MInt) => 
-    refineHelper(TEMP1, TEMP2, P +Int 1, Q, 
-        xorMInt(RES, 
-          andMInt(
-            extractMInt(TEMP1, 63 -Int P,         64 -Int P),
-            extractMInt(TEMP2, 63 -Int (P -Int Q), 64 -Int (P -Int Q))
-            )))
-
-  syntax MInt ::= selectSlice(MInt, MInt, Int, Int, Int) [function]
-
-  rule selectSlice(SRC1:MInt, Imm8:MInt, CheckBit:Int, Start1:Int, Start2:Int)
-  => extractMInt(SRC1, Start1, Start1 +Int 64)
-    requires  eqMInt(mi(1, 0), extractMInt(Imm8, CheckBit, CheckBit +Int 1))
-
-  rule selectSlice(SRC1:MInt, Imm8:MInt, CheckBit:Int, Start1:Int, Start2:Int)
-  => extractMInt(SRC1, Start2, Start2 +Int 64)
-    requires  eqMInt(mi(1, 1), extractMInt(Imm8, CheckBit, CheckBit +Int 1))
 endmodule
 
 module PCLMULQDQ-XMM-XMM-IMM8-SEMANTICS

diff --git a/x86-semantics/semantics/immediateInstructions/vpclmulqdq_xmm_xmm_xmm_imm8.k b/x86-semantics/semantics/immediateInstructions/vpclmulqdq_xmm_xmm_xmm_imm8.k
@@ -38,79 +38,6 @@ module VPCLMULQDQ-XMM-XMM-XMM-IMM8
               computePCLMULQDQ2(TEMP1, TEMP2, mi(128, 0), 64, 126) 
             )), R4)
   ...</k>
-
-  /*
-    For i = 0 to 63 {
-        TmpB [ i ]←(TEMP1[ 0 ] and TEMP2[ i ]);
-        For j = 1 to i {
-            TmpB [ i ]←TmpB [ i ] xor (TEMP1[ j ] and TEMP2[ i - j ])
-        }
-        DEST[ i ]←TmpB[ i ];
-    }
-  */   
-  syntax MInt ::= computePCLMULQDQ1(MInt, MInt, MInt, Int, Int) [function]
-  syntax MInt ::= computePCLMULQDQ1Refine(MInt, MInt, Int) [function]
-
-  rule computePCLMULQDQ1(TEMP1:MInt, TEMP2:MInt, DEST:MInt, N:Int, N:Int) => DEST
-
-  rule computePCLMULQDQ1(TEMP1:MInt, TEMP2:MInt, DEST:MInt, M:Int, N:Int) =>
-    computePCLMULQDQ1( 
-        TEMP1, TEMP2, plugInMask(DEST, computePCLMULQDQ1Refine(TEMP1, TEMP2, M), M), M +Int 1, N)
-
-  rule computePCLMULQDQ1Refine(TEMP1:MInt, TEMP2:MInt, M:Int) =>
-  refineHelper(TEMP1, TEMP2, 1, M, 
-        andMInt( 
-          extractMInt(TEMP1, 63, 64), extractMInt(TEMP2, 63 -Int M, 64 -Int M) 
-          )
-      )
-
-  /*
-     For i = 64 to 126 {
-    TmpB [ i ]←0;
-    For j = i - 63 to 63 {
-        TmpB [ i ]←TmpB [ i ] xor (TEMP1[ j ] and TEMP2[ i - j ])
-    }
-    DEST[ i ]←TmpB[ i ];
-  }
-  */
-
-  syntax MInt ::= computePCLMULQDQ2(MInt, MInt, MInt, Int, Int) [function]
-  syntax MInt ::= computePCLMULQDQ2Refine(MInt, MInt, Int) [function]
-
-  rule computePCLMULQDQ2(TEMP1:MInt, TEMP2:MInt, DEST:MInt, N:Int, N:Int) => DEST
-
-  rule computePCLMULQDQ2(TEMP1:MInt, TEMP2:MInt, DEST:MInt, M:Int, N:Int) =>
-    computePCLMULQDQ2( 
-        TEMP1, TEMP2, plugInMask(DEST, computePCLMULQDQ2Refine(TEMP1, TEMP2, M), M), M +Int 1, N)
-
-  rule computePCLMULQDQ2Refine(TEMP1:MInt, TEMP2:MInt, M:Int) =>
-  refineHelper(TEMP1, TEMP2, M -Int 63, 63,  mi(1, 0))
-
-
-  // Utils
-  syntax MInt ::= refineHelper(MInt, MInt, Int, Int, MInt) [function]
-  rule refineHelper(TEMP1:MInt, TEMP2:MInt, Q:Int, Q:Int,
-      RES:MInt) => RES
-
-  rule refineHelper(TEMP1:MInt, TEMP2:MInt, P:Int, Q:Int,
-      RES:MInt) => 
-    refineHelper(TEMP1, TEMP2, P +Int 1, Q, 
-        xorMInt(RES, 
-          andMInt(
-            extractMInt(TEMP1, 63 -Int P,         64 -Int P),
-            extractMInt(TEMP2, 63 -Int (P -Int Q), 64 -Int (P -Int Q))
-            )))
-
-  syntax MInt ::= selectSlice(MInt, MInt, Int, Int, Int) [function]
-
-  rule selectSlice(SRC1:MInt, Imm8:MInt, CheckBit:Int, Start1:Int, Start2:Int)
-  => extractMInt(SRC1, Start1, Start1 +Int 64)
-    requires  eqMInt(mi(1, 0), extractMInt(Imm8, CheckBit, CheckBit +Int 1))
-
-  rule selectSlice(SRC1:MInt, Imm8:MInt, CheckBit:Int, Start1:Int, Start2:Int)
-  => extractMInt(SRC1, Start2, Start2 +Int 64)
-    requires  eqMInt(mi(1, 1), extractMInt(Imm8, CheckBit, CheckBit +Int 1))
-
 endmodule
 
 module VPCLMULQDQ-XMM-XMM-XMM-IMM8-SEMANTICS

diff --git a/x86-semantics/semantics/x86-mint-wrapper.k b/x86-semantics/semantics/x86-mint-wrapper.k
@@ -344,6 +344,14 @@ module MINT-WRAPPER-SYNTAX
   syntax MInt ::= rol(MInt, MInt) [function]
   syntax MInt ::= ror(MInt, MInt) [function]
 
+  /*@
+    pclmulqdq
+  */
+  syntax MInt ::= computePCLMULQDQ1(MInt, MInt, MInt, Int, Int) [function]
+  syntax MInt ::= computePCLMULQDQ1Refine(MInt, MInt, Int) [function]
+  syntax MInt ::= computePCLMULQDQ2(MInt, MInt, MInt, Int, Int) [function]
+  syntax MInt ::= computePCLMULQDQ2Refine(MInt, MInt, Int) [function]
+  syntax MInt ::= selectSlice(MInt, MInt, Int, Int, Int) [function]
 endmodule
 
 
@@ -808,6 +816,81 @@ module MINT-WRAPPER
         )
       ), N, M +Int 1)  
   requires M <Int N
+
+  /*@
+    pclmulqdq
+  */
+  /*
+    For i = 0 to 63 {
+        TmpB [ i ]←(TEMP1[ 0 ] and TEMP2[ i ]);
+        For j = 1 to i {
+            TmpB [ i ]←TmpB [ i ] xor (TEMP1[ j ] and TEMP2[ i - j ])
+        }
+        DEST[ i ]←TmpB[ i ];
+    }
+  */   
+  rule computePCLMULQDQ1(TEMP1:MInt, TEMP2:MInt, DEST:MInt, M:Int, N:Int) => DEST
+      requires M ==Int N
+
+  rule computePCLMULQDQ1(TEMP1:MInt, TEMP2:MInt, DEST:MInt, M:Int, N:Int) =>
+    computePCLMULQDQ1( 
+        TEMP1, TEMP2, plugInMask(DEST, computePCLMULQDQ1Refine(TEMP1, TEMP2, M), M), M +Int 1, N)
+      requires M <Int N
+
+  rule computePCLMULQDQ1Refine(TEMP1:MInt, TEMP2:MInt, M:Int) =>
+  refineHelper(TEMP1, TEMP2, 1, M, 
+        andMInt( 
+          extractMInt(TEMP1, 63, 64), extractMInt(TEMP2, 63 -Int M, 64 -Int M) 
+          )
+      )
+
+  /*
+     For i = 64 to 126 {
+    TmpB [ i ]←0;
+    For j = i - 63 to 63 {
+        TmpB [ i ]←TmpB [ i ] xor (TEMP1[ j ] and TEMP2[ i - j ])
+    }
+    DEST[ i ]←TmpB[ i ];
+  }
+  */
+
+  rule computePCLMULQDQ2(TEMP1:MInt, TEMP2:MInt, DEST:MInt, M:Int, N:Int) => DEST
+      requires M ==Int N
+
+  rule computePCLMULQDQ2(TEMP1:MInt, TEMP2:MInt, DEST:MInt, M:Int, N:Int) =>
+    computePCLMULQDQ2( 
+        TEMP1, TEMP2, plugInMask(DEST, computePCLMULQDQ2Refine(TEMP1, TEMP2, M), M), M +Int 1, N)
+      requires M <Int N
+
+  rule computePCLMULQDQ2Refine(TEMP1:MInt, TEMP2:MInt, M:Int) =>
+  refineHelper(TEMP1, TEMP2, M -Int 63, 63,  mi(1, 0))
+
+
+  // Utils
+  syntax MInt ::= refineHelper(MInt, MInt, Int, Int, MInt) [function]
+  rule refineHelper(TEMP1:MInt, TEMP2:MInt, P:Int, Q:Int,
+      RES:MInt) => RES
+      requires P >=Int Q
+
+  rule refineHelper(TEMP1:MInt, TEMP2:MInt, P:Int, Q:Int,
+      RES:MInt) => 
+    refineHelper(TEMP1, TEMP2, P +Int 1, Q, 
+        xorMInt(RES, 
+          andMInt(
+            extractMInt(TEMP1, 63 -Int P,         64 -Int P),
+            extractMInt(TEMP2, 63 -Int (P -Int Q), 64 -Int (P -Int Q))
+            )))
+      requires P <Int Q
+
+
+  rule selectSlice(SRC1:MInt, Imm8:MInt, CheckBit:Int, Start1:Int, Start2:Int)
+  => extractMInt(SRC1, Start1, Start1 +Int 64)
+    requires  eqMInt(mi(1, 0), extractMInt(Imm8, CheckBit, CheckBit +Int 1))
+
+  rule selectSlice(SRC1:MInt, Imm8:MInt, CheckBit:Int, Start1:Int, Start2:Int)
+  => extractMInt(SRC1, Start2, Start2 +Int 64)
+    requires  eqMInt(mi(1, 1), extractMInt(Imm8, CheckBit, CheckBit +Int 1))
+
 endmodule
 
 /*