#77: wip

x86-semantics/semantics/immediateInstructions/mpsadbw_xmm_xmm_imm8.k

@@ -127,20 +127,6 @@ module MPSADBW-XMM-XMM-IMM8
       )) , R3)
 
   ...</k>
-
-  // Utils
-
-  syntax MInt ::= absoluteUnsignedDifference(MInt, MInt) [function]
-  rule absoluteUnsignedDifference(A:MInt, B:MInt) => subMInt(A, B)
-    requires ugtMInt(A, B)
-
-  rule absoluteUnsignedDifference(A:MInt, B:MInt) => subMInt(B, A)
-    requires notBool ugtMInt(A, B)
-
-  syntax MInt ::= selectSliceMPSAD(MInt, MInt, Int, Int) [function]
-  rule selectSliceMPSAD(DEST:MInt, Offset:MInt, High:Int, Low:Int) =>
-    concatenateMInt(mi(8, 0), extractMInt(DEST, (uvalueMInt(Offset) *Int 32)
-          +Int High, (uvalueMInt(Offset) *Int 32) +Int Low))
 endmodule
 
 module MPSADBW-XMM-XMM-IMM8-SEMANTICS

x86-semantics/semantics/immediateInstructions/vmpsadbw_xmm_xmm_xmm_imm8.k

@@ -37,7 +37,7 @@ module VMPSADBW-XMM-XMM-XMM-IMM8
           extractMInt(handleImmediateWithSignExtend(Imm8, 8, 8), 5, 6), 79, 72),
         selectSliceMPSAD(getRegisterValue(R3, RSMap),
           extractMInt(handleImmediateWithSignExtend(Imm8, 8, 8), 5, 6), 87, 80),
-        R3:Xmm, 
+        R4:Xmm, 
         .Operands)
   ...</k>   
     <regstate> RSMap </regstate>
@@ -48,7 +48,7 @@ module VMPSADBW-XMM-XMM-XMM-IMM8
         DestByte0:MInt, DestByte1:MInt, DestByte2:MInt, DestByte3:MInt,
         DestByte4:MInt, DestByte5:MInt, DestByte6:MInt, DestByte7:MInt,
         DestByte8:MInt, DestByte9:MInt, DestByte10:MInt,
-        R3:Xmm,  .Operands) =>
+        R4:Xmm,  .Operands) =>
   setParentValue(
   concatenateMInt(mi(128, 0),
     concatenateMInt(
@@ -125,23 +125,9 @@ module VMPSADBW-XMM-XMM-XMM-IMM8
               absoluteUnsignedDifference(DestByte2, SrcByte2),
               absoluteUnsignedDifference(DestByte3, SrcByte3))
           ))
-      ))) , R3)
+      ))) , R4)
 
   ...</k>
-
-  // Utils
-
-  syntax MInt ::= absoluteUnsignedDifference(MInt, MInt) [function]
-  rule absoluteUnsignedDifference(A:MInt, B:MInt) => subMInt(A, B)
-    requires ugtMInt(A, B)
-
-  rule absoluteUnsignedDifference(A:MInt, B:MInt) => subMInt(B, A)
-    requires notBool ugtMInt(A, B)
-
-  syntax MInt ::= selectSliceMPSAD(MInt, MInt, Int, Int) [function]
-  rule selectSliceMPSAD(DEST:MInt, Offset:MInt, High:Int, Low:Int) =>
-    concatenateMInt(mi(8, 0), extractMInt(DEST, (uvalueMInt(Offset) *Int 32)
-          +Int High, (uvalueMInt(Offset) *Int 32) +Int Low))
 endmodule
 
 module VMPSADBW-XMM-XMM-XMM-IMM8-SEMANTICS

x86-semantics/semantics/immediateInstructions/vmpsadbw_ymm_ymm_ymm_imm8.k

@@ -266,21 +266,6 @@ module VMPSADBW-YMM-YMM-YMM-IMM8
       ) , R4)
 
   ...</k>
-
-  // Utils
-
-  syntax MInt ::= absoluteUnsignedDifference(MInt, MInt) [function]
-  rule absoluteUnsignedDifference(A:MInt, B:MInt) => subMInt(A, B)
-    requires ugtMInt(A, B)
-
-  rule absoluteUnsignedDifference(A:MInt, B:MInt) => subMInt(B, A)
-    requires notBool ugtMInt(A, B)
-
-  syntax MInt ::= selectSliceMPSAD(MInt, MInt, Int, Int) [function]
-  rule selectSliceMPSAD(DEST:MInt, Offset:MInt, High:Int, Low:Int) =>
-    concatenateMInt(mi(8, 0), extractMInt(DEST, (uvalueMInt(Offset) *Int 32)
-          +Int High, (uvalueMInt(Offset) *Int 32) +Int Low))
-
 endmodule
 
 module VMPSADBW-YMM-YMM-YMM-IMM8-SEMANTICS

x86-semantics/semantics/x86-mint-wrapper.k

@@ -352,6 +352,13 @@ module MINT-WRAPPER-SYNTAX
   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]
+
+  /*@
+    mpsad
+  */  
+   syntax MInt ::= absoluteUnsignedDifference(MInt, MInt) [function]
+   syntax MInt ::= selectSliceMPSAD(MInt, MInt, Int, Int) [function]
+
 endmodule
 
 
@@ -890,7 +897,21 @@ module MINT-WRAPPER
   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))
-
+
+  /*@
+    mpsad
+  */  
+  rule absoluteUnsignedDifference(A:MInt, B:MInt) => subMInt(A, B)
+    requires ugtMInt(A, B)
+
+  rule absoluteUnsignedDifference(A:MInt, B:MInt) => subMInt(B, A)
+    requires notBool ugtMInt(A, B)
+
+  rule selectSliceMPSAD(DEST:MInt, Offset:MInt, High:Int, Low:Int) =>
+    concatenateMInt(mi(8, 0), 
+        //extractMInt(DEST, (uvalueMInt(Offset) *Int 32) +Int High, (uvalueMInt(Offset) *Int 32) +Int Low))
+        extractMask(DEST, High -Int Low +Int 1, (uvalueMInt(Offset) *Int 32) +Int Low))
+
 endmodule
 
 /*

x86-semantics/tests/Instructions/mpsadbw/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"