#77: wip

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

Hide file tree

Showing 21 changed files with 213,064 additions and 141 deletions.
diff --git a/x86-semantics/semantics/memoryInstructions/pextl_r32_r32_m32.k b/x86-semantics/semantics/memoryInstructions/pextl_r32_r32_m32.k
@@ -19,42 +19,7 @@ module PEXTL-R32-R32-M32
   memLoadValue(MemVal:MInt):MemLoadValue ~> 
     execinstr (pextl memOffset( MemOff), R2, R3, .Operands) =>
       setRegisterValue(mi(32, 0), R3) ~> 
-      parallelBitExtract(MemVal, R2, R3, 0, 0)
+      parallelBitExtract32(MemVal, R2, R3, 0, 0)
   ...</k>
     <regstate> RSMap:Map </regstate>
-
-  syntax KItem ::= parallelBitExtract(MInt, Register, Register, Int, Int)
-
-  // Base Condition
-  rule <k>
-    parallelBitExtract(Mask:MInt, TempR:Register, DestR:Register, 31:Int, K:Int) => 
-      setRegisterBitsAtPositon(getRegisterBitsAtPositon(TempR, 1, 31, RSMap), DestR, K)
-  ...</k>  
-    <regstate> RSMap:Map </regstate>
-      requires eqMInt( extractMInt(Mask, 0, 1), mi(1, 1))
-
-  rule <k>
-    parallelBitExtract(Mask:MInt, TempR:Register, DestR:Register, 31:Int, K:Int) => 
-    .
-  ...</k>  
-    requires eqMInt( extractMInt(Mask, 0, 1), mi(1, 0))
-
-  // General Condition
-  rule <k>
-    parallelBitExtract(Mask:MInt, TempR:Register, DestR:Register, M:Int, K:Int) => 
-      setRegisterBitsAtPositon(getRegisterBitsAtPositon(TempR, 1, M, RSMap), DestR, K)
-  ~>  parallelBitExtract(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>
-    parallelBitExtract(Mask:MInt, TempR:Register, DestR:Register, M:Int, K:Int) => 
-        parallelBitExtract(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/pextq_r64_r64_m64.k b/x86-semantics/semantics/memoryInstructions/pextq_r64_r64_m64.k
@@ -19,41 +19,7 @@ module PEXTQ-R64-R64-M64
   memLoadValue(MemVal:MInt):MemLoadValue ~> 
     execinstr (pextq memOffset( MemOff), R2, R3, .Operands) =>
       setRegisterValue(mi(64, 0), R3) ~> 
-      parallelBitExtract(MemVal, R2, R3, 0, 0)
+      parallelBitExtract64(MemVal, R2, R3, 0, 0)
   ...</k>
     <regstate> RSMap:Map </regstate>
-
-  syntax KItem ::= parallelBitExtract(MInt, Register, Register, Int, Int)
-
-  // Base Condition
-  rule <k>
-    parallelBitExtract(Mask:MInt, TempR:Register, DestR:Register, 63:Int, K:Int) => 
-      setRegisterBitsAtPositon(getRegisterBitsAtPositon(TempR, 1, 63, RSMap), DestR, K)
-  ...</k>  
-    <regstate> RSMap:Map </regstate>
-      requires eqMInt( extractMInt(Mask, 0, 1), mi(1, 1))
-
-  rule <k>
-    parallelBitExtract(Mask:MInt, TempR:Register, DestR:Register, 63:Int, K:Int) => 
-    .
-  ...</k>  
-    requires eqMInt( extractMInt(Mask, 0, 1), mi(1, 0))
-
-  // General Condition
-  rule <k>
-    parallelBitExtract(Mask:MInt, TempR:Register, DestR:Register, M:Int, K:Int) => 
-      setRegisterBitsAtPositon(getRegisterBitsAtPositon(TempR, 1, M, RSMap), DestR, K)
-  ~>  parallelBitExtract(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>
-    parallelBitExtract(Mask:MInt, TempR:Register, DestR:Register, M:Int, K:Int) => 
-        parallelBitExtract(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/pextl_r32_r32_r32.k b/x86-semantics/semantics/registerInstructions/pextl_r32_r32_r32.k
@@ -19,42 +19,8 @@ module PEXTL-R32-R32-R32
 
   rule <k>
     execinstr (pextl R1:R32, R2:R32, R3:R32, .Operands) => 
-      setRegisterValue(mi(32, 0), R3) ~> parallelBitExtract(getRegisterValue(R1,
+      setRegisterValue(mi(32, 0), R3) ~> parallelBitExtract32(getRegisterValue(R1,
             RSMap), R2, R3, 0, 0)
   ...</k>
     <regstate> RSMap:Map </regstate>
-
-
-  syntax KItem ::= parallelBitExtract(MInt, Register, Register, Int, Int)
-
-  // Base Condition
-  rule <k>
-    parallelBitExtract(Mask:MInt, TempR:Register, DestR:Register, 31:Int, K:Int) => 
-      setRegisterBitsAtPositon(getRegisterBitsAtPositon(TempR, 1, 31, RSMap), DestR, K)
-  ...</k>  
-    <regstate> RSMap:Map </regstate>
-      requires eqMInt( extractMInt(Mask, 0, 1), mi(1, 1))
-
-  rule <k>
-    parallelBitExtract(Mask:MInt, TempR:Register, DestR:Register, 31:Int, K:Int) => 
-    .
-  ...</k>  
-    requires eqMInt( extractMInt(Mask, 0, 1), mi(1, 0))
-
-  // General Condition
-  rule <k>
-    parallelBitExtract(Mask:MInt, TempR:Register, DestR:Register, M:Int, K:Int) => 
-      setRegisterBitsAtPositon(getRegisterBitsAtPositon(TempR, 1, M, RSMap), DestR, K)
-  ~>  parallelBitExtract(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>
-    parallelBitExtract(Mask:MInt, TempR:Register, DestR:Register, M:Int, K:Int) => 
-        parallelBitExtract(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/pextq_r64_r64_r64.k b/x86-semantics/semantics/registerInstructions/pextq_r64_r64_r64.k
@@ -19,42 +19,8 @@ module PEXTQ-R64-R64-R64
 
   rule <k>
     execinstr (pextq R1:R64, R2:R64, R3:R64, .Operands) => 
-      setRegisterValue(mi(64, 0), R3) ~> parallelBitExtract(getRegisterValue(R1,
+      setRegisterValue(mi(64, 0), R3) ~> parallelBitExtract64(getRegisterValue(R1,
             RSMap), R2, R3, 0, 0)
   ...</k>
     <regstate> RSMap:Map </regstate>
-
-
-  syntax KItem ::= parallelBitExtract(MInt, Register, Register, Int, Int)
-
-  // Base Condition
-  rule <k>
-    parallelBitExtract(Mask:MInt, TempR:Register, DestR:Register, 63:Int, K:Int) => 
-      setRegisterBitsAtPositon(getRegisterBitsAtPositon(TempR, 1, 63, RSMap), DestR, K)
-  ...</k>  
-    <regstate> RSMap:Map </regstate>
-      requires eqMInt( extractMInt(Mask, 0, 1), mi(1, 1))
-
-  rule <k>
-    parallelBitExtract(Mask:MInt, TempR:Register, DestR:Register, 63:Int, K:Int) => 
-    .
-  ...</k>  
-    requires eqMInt( extractMInt(Mask, 0, 1), mi(1, 0))
-
-  // General Condition
-  rule <k>
-    parallelBitExtract(Mask:MInt, TempR:Register, DestR:Register, M:Int, K:Int) => 
-      setRegisterBitsAtPositon(getRegisterBitsAtPositon(TempR, 1, M, RSMap), DestR, K)
-  ~>  parallelBitExtract(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>
-    parallelBitExtract(Mask:MInt, TempR:Register, DestR:Register, M:Int, K:Int) => 
-        parallelBitExtract(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
@@ -430,6 +430,71 @@ module X86-ABSTRACT-SEMANTICS
                 andBool M =/=Int 31
 
 
+  /*@
+    pextl/q
+  */
+   // Base Condition
+  rule <k>
+    parallelBitExtract32(Mask:MInt, TempR:Register, DestR:Register, M:Int, K:Int) => 
+      setRegisterBitsAtPositon(getRegisterBitsAtPositon(TempR, 1, 31, RSMap), DestR, K)
+  ...</k>  
+    <regstate> RSMap:Map </regstate>
+      requires eqMInt( extractMInt(Mask, 0, 1), mi(1, 1)) andBool M ==Int 31
+
+  rule <k>
+    parallelBitExtract32(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>
+    parallelBitExtract32(Mask:MInt, TempR:Register, DestR:Register, M:Int, K:Int) => 
+      setRegisterBitsAtPositon(getRegisterBitsAtPositon(TempR, 1, M, RSMap), DestR, K)
+  ~>  parallelBitExtract32(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>
+    parallelBitExtract32(Mask:MInt, TempR:Register, DestR:Register, M:Int, K:Int) => 
+        parallelBitExtract32(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
+
+
+  // Base Condition
+  rule <k>
+    parallelBitExtract64(Mask:MInt, TempR:Register, DestR:Register, M:Int, K:Int) => 
+      setRegisterBitsAtPositon(getRegisterBitsAtPositon(TempR, 1, 63, RSMap), DestR, K)
+  ...</k>  
+    <regstate> RSMap:Map </regstate>
+      requires eqMInt( extractMInt(Mask, 0, 1), mi(1, 1)) andBool M ==Int 63
+
+  rule <k>
+    parallelBitExtract64(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>
+    parallelBitExtract64(Mask:MInt, TempR:Register, DestR:Register, M:Int, K:Int) => 
+      setRegisterBitsAtPositon(getRegisterBitsAtPositon(TempR, 1, M, RSMap), DestR, K)
+  ~>  parallelBitExtract64(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>
+    parallelBitExtract64(Mask:MInt, TempR:Register, DestR:Register, M:Int, K:Int) => 
+        parallelBitExtract64(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               
 
 endmodule
 

diff --git a/x86-semantics/semantics/x86-abstract-syntax.k b/x86-semantics/semantics/x86-abstract-syntax.k
@@ -142,4 +142,11 @@ module X86-ASBTRACT-SYNTAX
   syntax KItem ::= parallelBitDeposit64(MInt, Register, Register, Int, Int)
   syntax KItem ::= parallelBitDeposit32(MInt, Register, Register, Int, Int)
 
+  /*@
+    pextl/q
+  */
+  syntax KItem ::= parallelBitExtract64(MInt, Register, Register, Int, Int)
+  syntax KItem ::= parallelBitExtract32(MInt, Register, Register, Int, Int)
+
+
 endmodule
diff --git a/x86-semantics/tests/Instructions/pdepl/Makefile b/x86-semantics/tests/Instructions/pdepl/Makefile
@@ -0,0 +1,54 @@
+TESTS=$(shell find . -maxdepth 1   -name "*.s" | sort -V)
+
+OUTDIR=Output
+KSTATES=$(patsubst %.s, ${OUTDIR}/%.kstate, $(TESTS))
+XSTATES=$(patsubst %.s, ${OUTDIR}/%.xstate, $(TESTS))
+CSTATES=$(patsubst %.s, %.cstate, $(TESTS))
+
+Mkdir=@mkdir -p $(@D)
+RUN_SH=../../../scripts/run.pl
+
+
+
+all:	kstate xstate compare
+
+kstate: ${KSTATES}
+xstate: ${XSTATES}
+compare:${CSTATES}
+
+${OUTDIR}/%.kstate: %.s
+	@echo ""
+	@echo  "Generate: $@ "
+	@mkdir -p ${OUTDIR}
+	${RUN_SH} --file $< --krun --output $@
+
+${OUTDIR}/%.xstate: %.s
+	@echo ""
+	@echo  "Generate: $@ "
+	@mkdir -p ${OUTDIR}
+	${RUN_SH} --file $< --xrun --output $@
+
+%.cstate: ${OUTDIR}/%.kstate ${OUTDIR}/%.xstate
+	@echo ""
+	@echo  "Compare: ${OUTDIR}/$@ "
+	${RUN_SH} --file $< --compare 
+
+allclean:
+	@echo "All Cleaning"
+	rm -rf ${OUTDIR}
+
+clean:
+	@echo "Cleaning .exe & .o"
+	rm -rf ${OUTDIR}/*.exec
+	rm -rf ${OUTDIR}/*.o
+
+cleankstate:
+	@echo "K Cleaning"
+	rm -rf ${OUTDIR}/*.kstate
+
+cleanxstate:
+	@echo "X Cleaning"
+	rm -rf ${OUTDIR}/*.xstate
+
+test:
+	@echo "T Cleaning"