#77: wip

sdasgup3 · Jun 7, 2018 · 6c087ba · 6c087ba
1 parent 8675d76
commit 6c087ba
Show file tree

Hide file tree

Showing 10 changed files with 155 additions and 12,133 deletions.
diff --git a/x86-semantics/scripts/genfromtemplate.pl b/x86-semantics/scripts/genfromtemplate.pl
@@ -5,8 +5,8 @@
 use File::Compare;
 use File::Basename;
 
-use lib qw( ./ );
-use ktestutils;
+use lib qw( /home/sdasgup3/x86-semantics/scripts/ );
+use kutils;
 
 my $gendir = "";
 my $templatedir = "";

diff --git a/x86-semantics/scripts/gentests.pl b/x86-semantics/scripts/gentests.pl
@@ -6,7 +6,7 @@
 use File::Basename;
 use File::Find;
 
-use lib qw( ../../scripts/ );
+use lib qw( /home/sdasgup3/x86-semantics/scripts/ );
 use kutils;
 
 my $help = "";

diff --git a/x86-semantics/scripts/process_spec.pl b/x86-semantics/scripts/process_spec.pl
@@ -258,14 +258,18 @@ sub createSingleFileDefn {
     my $memoryInstructionsPath    = "memoryInstructions/";
     my $systemInstructionsPath    = "systemInstructions/";
     my $customInstructionsPath    = "customInstructions/";
+    my $UTInstructionsPath        = "underTestInstructions/";
 
     if ( "" ne $useuif ) {
         $baseInstrPath    = "instructions_with_uif/baseInstructions/";
         $derivedInstrPath = "instructions_with_uif/derivedInstructions/";
     }
 
-    print("\tMerging customInstructionsPath\n");
-    find( \&mergeToSingleFile, $customInstructionsPath );
+    print("\tMerging UTInstructionsPath\n");
+    find( \&mergeToSingleFile, $UTInstructionsPath );
+
+    #print("\tMerging customInstructionsPath\n");
+    #find( \&mergeToSingleFile, $customInstructionsPath );
 
     #print("\tMerging $registerInstructionsPath\n");
     #find( \&mergeToSingleFile, $registerInstructionsPath );
@@ -274,8 +278,8 @@ sub createSingleFileDefn {
     #print("\tMerging $memoryInstructionsPath\n");
     #find( \&mergeToSingleFile, $memoryInstructionsPath );
 
-    print("\tMerging $systemInstructionsPath\n");
-    find( \&mergeToSingleFile, $systemInstructionsPath );
+    #print("\tMerging $systemInstructionsPath\n");
+    #find( \&mergeToSingleFile, $systemInstructionsPath );
 
     #print $sfp "endmodule";
     #    close($sfp);

diff --git a/x86-semantics/semantics/memoryInstructions/pdepl_r32_r32_m32.k b/x86-semantics/semantics/memoryInstructions/pdepl_r32_r32_m32.k
@@ -19,42 +19,7 @@ module PDEPL-R32-R32-M32
   memLoadValue(MemVal:MInt):MemLoadValue ~> 
     execinstr (pdepl memOffset( MemOff), R2, R3, .Operands) =>
       setRegisterValue(mi(32, 0), R3) ~> 
-      parallelBitDeposit(MemVal, R2, R3, 0, 0)
+      parallelBitDeposit32(MemVal, R2, R3, 0, 0)
   ...</k>
     <regstate> RSMap:Map </regstate>
-
-  syntax KItem ::= parallelBitDeposit(MInt, Register, Register, Int, Int)
-
-  // Base Condition
-  rule <k>
-    parallelBitDeposit(Mask:MInt, TempR:Register, DestR:Register, 31:Int, K:Int) => 
-      setRegisterBitsAtPositon(getRegisterBitsAtPositon(TempR, 1, K, RSMap),
-          DestR, 31)
-  ...</k>  
-    <regstate> RSMap:Map </regstate>
-      requires eqMInt( extractMInt(Mask, 0, 1), mi(1, 1))
-
-  rule <k>
-    parallelBitDeposit(Mask:MInt, TempR:Register, DestR:Register, 31:Int, K:Int) => 
-    .
-  ...</k>  
-    requires eqMInt( extractMInt(Mask, 0, 1), mi(1, 0))
-
-  // General Condition
-  rule <k>
-    parallelBitDeposit(Mask:MInt, TempR:Register, DestR:Register, M:Int, K:Int) => 
-      setRegisterBitsAtPositon(getRegisterBitsAtPositon(TempR, 1, K, RSMap), DestR, M)
-  ~>  parallelBitDeposit(Mask, TempR, DestR, M +Int 1, K +Int 1)
-  ...</k>  
-    <regstate> RSMap:Map </regstate>
-      requires eqMInt( extractMInt(Mask, 31 -Int M, 32 -Int M), mi(1, 1))
-
-  rule <k>
-    parallelBitDeposit(Mask:MInt, TempR:Register, DestR:Register, M:Int, K:Int) => 
-        parallelBitDeposit(Mask, TempR, DestR, M +Int 1, K)
-  ...</k>  
-    requires eqMInt( extractMInt(Mask, 31 -Int M, 32 -Int M), mi(1, 0))
-
-
-
 endmodule
diff --git a/x86-semantics/semantics/memoryInstructions/pdepq_r64_r64_m64.k b/x86-semantics/semantics/memoryInstructions/pdepq_r64_r64_m64.k
@@ -19,42 +19,7 @@ module PDEPQ-R64-R64-M64
   memLoadValue(MemVal:MInt):MemLoadValue ~> 
     execinstr (pdepq memOffset( MemOff), R2, R3, .Operands) =>
       setRegisterValue(mi(64, 0), R3) ~> 
-      parallelBitDeposit(MemVal, R2, R3, 0, 0)
+      parallelBitDeposit64(MemVal, R2, R3, 0, 0)
   ...</k>
     <regstate> RSMap:Map </regstate>
-
-
-  syntax KItem ::= parallelBitDeposit(MInt, Register, Register, Int, Int)
-
-  // Base Condition
-  rule <k>
-    parallelBitDeposit(Mask:MInt, TempR:Register, DestR:Register, 63:Int, K:Int) => 
-      setRegisterBitsAtPositon(getRegisterBitsAtPositon(TempR, 1, K, RSMap),
-          DestR, 63)
-  ...</k>  
-    <regstate> RSMap:Map </regstate>
-      requires eqMInt( extractMInt(Mask, 0, 1), mi(1, 1))
-
-  rule <k>
-    parallelBitDeposit(Mask:MInt, TempR:Register, DestR:Register, 63:Int, K:Int) => 
-    .
-  ...</k>  
-    requires eqMInt( extractMInt(Mask, 0, 1), mi(1, 0))
-
-  // General Condition
-  rule <k>
-    parallelBitDeposit(Mask:MInt, TempR:Register, DestR:Register, M:Int, K:Int) => 
-      setRegisterBitsAtPositon(getRegisterBitsAtPositon(TempR, 1, K, RSMap), DestR, M)
-  ~>  parallelBitDeposit(Mask, TempR, DestR, M +Int 1, K +Int  1)
-  ...</k>  
-    <regstate> RSMap:Map </regstate>
-      requires eqMInt( extractMInt(Mask, 63 -Int M, 64 -Int M), mi(1, 1))
-
-  rule <k>
-    parallelBitDeposit(Mask:MInt, TempR:Register, DestR:Register, M:Int, K:Int) => 
-        parallelBitDeposit(Mask, TempR, DestR, M +Int 1, K)
-  ...</k>  
-    requires eqMInt( extractMInt(Mask, 63 -Int M, 64 -Int M), mi(1, 0))
-
-
 endmodule
diff --git a/x86-semantics/semantics/registerInstructions/pdepl_r32_r32_r32.k b/x86-semantics/semantics/registerInstructions/pdepl_r32_r32_r32.k
@@ -19,43 +19,8 @@ module PDEPL-R32-R32-R32
 
   rule <k>
     execinstr (pdepl R1:R32, R2:R32, R3:R32, .Operands) => 
-      setRegisterValue(mi(32, 0), R3) ~> parallelBitDeposit(getRegisterValue(R1,
+      setRegisterValue(mi(32, 0), R3) ~> parallelBitDeposit32(getRegisterValue(R1,
             RSMap), R2, R3, 0, 0)
   ...</k>
     <regstate> RSMap:Map </regstate>
-
-
-  syntax KItem ::= parallelBitDeposit(MInt, Register, Register, Int, Int)
-
-  // Base Condition
-  rule <k>
-    parallelBitDeposit(Mask:MInt, TempR:Register, DestR:Register, 31:Int, K:Int) => 
-      setRegisterBitsAtPositon(getRegisterBitsAtPositon(TempR, 1, K, RSMap),
-          DestR, 31)
-  ...</k>  
-    <regstate> RSMap:Map </regstate>
-      requires eqMInt( extractMInt(Mask, 0, 1), mi(1, 1))
-
-  rule <k>
-    parallelBitDeposit(Mask:MInt, TempR:Register, DestR:Register, 31:Int, K:Int) => 
-    .
-  ...</k>  
-    requires eqMInt( extractMInt(Mask, 0, 1), mi(1, 0))
-
-  // General Condition
-  rule <k>
-    parallelBitDeposit(Mask:MInt, TempR:Register, DestR:Register, M:Int, K:Int) => 
-      setRegisterBitsAtPositon(getRegisterBitsAtPositon(TempR, 1, K, RSMap), DestR, M)
-  ~>  parallelBitDeposit(Mask, TempR, DestR, M +Int 1, K +Int 1)
-  ...</k>  
-    <regstate> RSMap:Map </regstate>
-      requires eqMInt( extractMInt(Mask, 31 -Int M, 32 -Int M), mi(1, 1))
-
-  rule <k>
-    parallelBitDeposit(Mask:MInt, TempR:Register, DestR:Register, M:Int, K:Int) => 
-        parallelBitDeposit(Mask, TempR, DestR, M +Int 1, K)
-  ...</k>  
-    requires eqMInt( extractMInt(Mask, 31 -Int M, 32 -Int M), mi(1, 0))
-
-
 endmodule
diff --git a/x86-semantics/semantics/registerInstructions/pdepq_r64_r64_r64.k b/x86-semantics/semantics/registerInstructions/pdepq_r64_r64_r64.k
@@ -19,43 +19,8 @@ module PDEPQ-R64-R64-R64
 
   rule <k>
     execinstr (pdepq R1:R64, R2:R64, R3:R64, .Operands) => 
-      setRegisterValue(mi(64, 0), R3) ~> parallelBitDeposit(getRegisterValue(R1,
+      setRegisterValue(mi(64, 0), R3) ~> parallelBitDeposit64(getRegisterValue(R1,
             RSMap), R2, R3, 0, 0)
   ...</k>
     <regstate> RSMap:Map </regstate>
-
-
-  syntax KItem ::= parallelBitDeposit(MInt, Register, Register, Int, Int)
-
-  // Base Condition
-  rule <k>
-    parallelBitDeposit(Mask:MInt, TempR:Register, DestR:Register, 63:Int, K:Int) => 
-      setRegisterBitsAtPositon(getRegisterBitsAtPositon(TempR, 1, K, RSMap),
-          DestR, 63)
-  ...</k>  
-    <regstate> RSMap:Map </regstate>
-      requires eqMInt( extractMInt(Mask, 0, 1), mi(1, 1))
-
-  rule <k>
-    parallelBitDeposit(Mask:MInt, TempR:Register, DestR:Register, 63:Int, K:Int) => 
-    .
-  ...</k>  
-    requires eqMInt( extractMInt(Mask, 0, 1), mi(1, 0))
-
-  // General Condition
-  rule <k>
-    parallelBitDeposit(Mask:MInt, TempR:Register, DestR:Register, M:Int, K:Int) => 
-      setRegisterBitsAtPositon(getRegisterBitsAtPositon(TempR, 1, K, RSMap), DestR, M)
-  ~>  parallelBitDeposit(Mask, TempR, DestR, M +Int 1, K +Int  1)
-  ...</k>  
-    <regstate> RSMap:Map </regstate>
-      requires eqMInt( extractMInt(Mask, 63 -Int M, 64 -Int M), mi(1, 1))
-
-  rule <k>
-    parallelBitDeposit(Mask:MInt, TempR:Register, DestR:Register, M:Int, K:Int) => 
-        parallelBitDeposit(Mask, TempR, DestR, M +Int 1, K)
-  ...</k>  
-    requires eqMInt( extractMInt(Mask, 63 -Int M, 64 -Int M), mi(1, 0))
-
-
 endmodule
diff --git a/x86-semantics/semantics/x86-abstract-semantics.k b/x86-semantics/semantics/x86-abstract-semantics.k
@@ -361,6 +361,75 @@ module X86-ABSTRACT-SEMANTICS
         "RSP" |-> addMInt({RSMap["RSP"]}:>MInt, mi(64, I)))
     </regstate>
 
+  /*@
+    pdepq/l
+  */
+  // Base Condition
+  rule <k>
+    parallelBitDeposit64(Mask:MInt, TempR:Register, DestR:Register, M:Int, K:Int) => 
+      setRegisterBitsAtPositon(getRegisterBitsAtPositon(TempR, 1, K, RSMap),
+          DestR, 63)
+  ...</k>  
+    <regstate> RSMap:Map </regstate>
+      requires eqMInt( extractMInt(Mask, 0, 1), mi(1, 1)) andBool M ==Int 63
+
+  rule <k>
+    parallelBitDeposit64(Mask:MInt, TempR:Register, DestR:Register, M:Int, K:Int) => 
+    .
+  ...</k>  
+    requires eqMInt( extractMInt(Mask, 0, 1), mi(1, 0)) andBool M ==Int 63
+
+  // General Condition
+  rule <k>
+    parallelBitDeposit64(Mask:MInt, TempR:Register, DestR:Register, M:Int, K:Int) => 
+      setRegisterBitsAtPositon(getRegisterBitsAtPositon(TempR, 1, K, RSMap), DestR, M)
+  ~>  parallelBitDeposit64(Mask, TempR, DestR, M +Int 1, K +Int  1)
+  ...</k>  
+    <regstate> RSMap:Map </regstate>
+      requires eqMInt( extractMInt(Mask, 63 -Int M, 64 -Int M), mi(1, 1))
+                andBool M =/=Int 63
+
+  rule <k>
+    parallelBitDeposit64(Mask:MInt, TempR:Register, DestR:Register, M:Int, K:Int) => 
+        parallelBitDeposit64(Mask, TempR, DestR, M +Int 1, K)
+  ...</k>  
+    requires eqMInt( extractMInt(Mask, 63 -Int M, 64 -Int M), mi(1, 0))
+                andBool M =/=Int 63
+
+
+  // Base Condition
+  rule <k>
+    parallelBitDeposit32(Mask:MInt, TempR:Register, DestR:Register, M:Int, K:Int) => 
+      setRegisterBitsAtPositon(getRegisterBitsAtPositon(TempR, 1, K, RSMap),
+          DestR, 31)
+  ...</k>  
+    <regstate> RSMap:Map </regstate>
+      requires eqMInt( extractMInt(Mask, 0, 1), mi(1, 1)) andBool M ==Int 31
+
+  rule <k>
+    parallelBitDeposit32(Mask:MInt, TempR:Register, DestR:Register, M:Int, K:Int) => 
+    .
+  ...</k>  
+    requires eqMInt( extractMInt(Mask, 0, 1), mi(1, 0)) andBool M ==Int 31
+
+  // General Condition
+  rule <k>
+    parallelBitDeposit32(Mask:MInt, TempR:Register, DestR:Register, M:Int, K:Int) => 
+      setRegisterBitsAtPositon(getRegisterBitsAtPositon(TempR, 1, K, RSMap), DestR, M)
+  ~>  parallelBitDeposit32(Mask, TempR, DestR, M +Int 1, K +Int 1)
+  ...</k>  
+    <regstate> RSMap:Map </regstate>
+      requires eqMInt( extractMInt(Mask, 31 -Int M, 32 -Int M), mi(1, 1))
+                andBool M =/=Int 31
+
+  rule <k>
+    parallelBitDeposit32(Mask:MInt, TempR:Register, DestR:Register, M:Int, K:Int) => 
+        parallelBitDeposit32(Mask, TempR, DestR, M +Int 1, K)
+  ...</k>  
+    requires eqMInt( extractMInt(Mask, 31 -Int M, 32 -Int M), mi(1, 0))
+                andBool M =/=Int 31
+
+
 
 endmodule
 

diff --git a/x86-semantics/semantics/x86-abstract-syntax.k b/x86-semantics/semantics/x86-abstract-syntax.k
@@ -136,4 +136,10 @@ module X86-ASBTRACT-SYNTAX
   syntax KItem ::= decRSPInBytes(Int) 
   syntax KItem ::= incRSPInBytes(Int) 
 
+  /*@
+    pdepl/q
+  */
+  syntax KItem ::= parallelBitDeposit64(MInt, Register, Register, Int, Int)
+  syntax KItem ::= parallelBitDeposit32(MInt, Register, Register, Int, Int)
+
 endmodule