X86 RREIL Translator

X86 Specification

- Added semantics of: (V)PSRLDQ
- Bug fixes

specifications/x86/c/asm-test.s

@@ -388,13 +388,16 @@ main:
 	#psllw (%rax), %xmm1
 	#psllw $197, %xmm1
 	#pslld $20, %mm1
-	psllq $10, %mm1
-	vpslld %xmm1, %xmm2, %xmm3
+	#psllq $10, %mm1
+	#vpslld %xmm1, %xmm2, %xmm3
 	#vpsllq $33, %xmm1, %xmm2
 
-	psrad $42, %xmm1
-	vpsraw $22, %xmm1, %xmm2
-	vpsrad %xmm1, %xmm2, %xmm3
+	#psrad $42, %xmm1
+	#vpsraw $22, %xmm1, %xmm2
+	#vpsrad %xmm1, %xmm2, %xmm3
+
+	psrldq $73, %xmm1
+	vpsrldq $5, %xmm1, %xmm2
 
 	#vmovd %xmm5, %ebx
 

specifications/x86/x86-rreil-translator-m-z.ml

@@ -1637,7 +1637,7 @@ end
 val sem-psign element-size x = sem-psign-vpsign-opnd '0' element-size x.opnd1 x.opnd1 x.opnd2
 val sem-vpsign element-size x = sem-psign-vpsign-opnd '1' element-size x.opnd1 x.opnd2 x.opnd3
 
-val sem-pslldq-vpslldq-opnd avx-encoded opnd1 opnd2 opnd3 = do
+val sem-psxldq-vpsxldq-opnd avx-encoded shifter opnd1 opnd2 opnd3 = do
   size <- sizeof1 opnd1;
   src <- read size opnd2;
   dst <- lval size opnd1;
@@ -1655,13 +1655,13 @@ val sem-pslldq-vpslldq-opnd avx-encoded opnd1 opnd2 opnd3 = do
   );
 
   temp <- mktemp;
-  shl size temp src (imm amount);
+  shifter size temp src (imm amount);
 
   write-extend avx-encoded size dst (var temp)
 end
 
-val sem-pslldq x = sem-pslldq-vpslldq-opnd '0' x.opnd1 x.opnd1 x.opnd2
-val sem-vpslldq x = sem-pslldq-vpslldq-opnd '1' x.opnd1 x.opnd2 x.opnd3
+val sem-pslldq x = sem-psxldq-vpsxldq-opnd '0' shl x.opnd1 x.opnd1 x.opnd2
+val sem-vpslldq x = sem-psxldq-vpsxldq-opnd '1' shl x.opnd1 x.opnd2 x.opnd3
 
 val sem-ps-vps-opnd avx-encoded element-size shifter opnd1 opnd2 opnd3 = do
   size <- sizeof1 opnd1;
@@ -1691,6 +1691,9 @@ val sem-vpsll element-size x = sem-ps-vps-opnd '1' element-size shl x.opnd1 x.op
 val sem-psra element-size x = sem-ps-vps-opnd '0' element-size shrs x.opnd1 x.opnd1 x.opnd2
 val sem-vpsra element-size x = sem-ps-vps-opnd '1' element-size shrs x.opnd1 x.opnd2 x.opnd3
 
+val sem-psrldq x = sem-psxldq-vpsxldq-opnd '0' shr x.opnd1 x.opnd1 x.opnd2
+val sem-vpsrldq x = sem-psxldq-vpsxldq-opnd '1' shr x.opnd1 x.opnd2 x.opnd3
+
 val ps-push opnd-sz opnd = do
   mode64 <- mode64?;
   stack-addr-sz <- runtime-stack-address-size;

specifications/x86/x86-rreil-translator.ml

@@ -1429,7 +1429,7 @@ val semantics insn =
    | PSRAD x: sem-psra 32 x
    | PSRAW x: sem-psra 16 x
    | PSRLD x: sem-undef-arity2 x
-   | PSRLDQ x: sem-undef-arity2 x
+   | PSRLDQ x: sem-psrldq x
    | PSRLQ x: sem-undef-arity2 x
    | PSRLW x: sem-undef-arity2 x
    | PSUBB x: sem-undef-arity2 x
@@ -2090,7 +2090,10 @@ val semantics insn =
           VA3 x: sem-vpsra 16 x
        end
    | VPSRLD x: sem-undef-varity x
-   | VPSRLDQ x: sem-undef-varity x
+   | VPSRLDQ v:
+       case v of
+          VA3 x: sem-vpsrldq x
+       end
    | VPSRLQ x: sem-undef-varity x
    | VPSRLW x: sem-undef-varity x
    | VPSUBB x: sem-undef-varity x

specifications/x86/x86.ml

@@ -5019,7 +5019,7 @@ val /vex/66/0f/vexv [0x72 /4-reg] | vex128? = varity3 VPSRAD v/xmm xmm/reg128 im
 ### PSRLDQ
 ###  - Shift Double Quadword Right Logical
 val /66 [0x0f 0x73 /3-reg] = binop PSRLDQ xmm/reg128 imm8
-val /vex/66/0f [0x73 /3-reg] | vndd? & vex128? = varity3 VPSRLDQ v/xmm xmm/reg128 imm8
+val /vex/66/0f/vexv [0x73 /3-reg] | vndd? & vex128? = varity3 VPSRLDQ v/xmm xmm/reg128 imm8
 
 ### PSRLW/PSRLD/PSRLQ
 ###  - Shift Packed Data Right Logical