X86 RREIL Translator

X86 Pretty Printer

- Added semantics of: VZEROUPPER
- Fixed printing of: MASKMOVQ

specifications/x86/c/asm-test.s

@@ -39,8 +39,8 @@ main:
 
 	#movbeq (%rax), %rbx
 
-	#maskmovq %mm3, %mm1
-	#vmaskmovdqu %xmm3, %xmm1
+	maskmovq %mm3, %mm1
+	vmaskmovdqu %xmm3, %xmm1
 
 	#loop main
 	#loope main
@@ -552,7 +552,8 @@ main:
 	#maskmovdqu %xmm2, %xmm1
 	#vmaskmovdqu %xmm2, %xmm1
 
-	vzeroall
+	#vzeroall
+	#vzeroupper
 
 	#pushq	%rbp
 	.cfi_def_cfa_offset 16

specifications/x86/x86-pretty.ml

@@ -506,7 +506,7 @@ val show/instruction insn =
     | LSS x: "LSS" -++ show/arity2 x
     | LTR x: "LTR" -++ show/arity1 x
     | MASKMOVDQU x: "MASKMOVDQU" -++ show/arity3 x
-    | MASKMOVQ x: "MASKMOVQ" -++ show/arity2 x
+    | MASKMOVQ x: "MASKMOVQ" -++ show/arity3 x
     | MAXPD x: "MAXPD" -++ show/arity2 x
     | MAXPS x: "MAXPS" -++ show/arity2 x
     | MAXSD x: "MAXSD" -++ show/arity2 x

specifications/x86/x86-rreil-registermapping.ml

@@ -202,6 +202,12 @@ val semantic-register-of r = case r of
    | RIP   : {id=Sem_IP, offset=0, size=64}
 end
 
+val semantic-register-of-offset r offset = let
+  val q = semantic-register-of r
+in
+  {id=q.id,offset=offset,size=q.size}
+end
+
 val semantic-register-of-operand-with-size opnd size =
   case opnd of
      REG r: @{size=size} (semantic-register-of r)

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

@@ -2659,6 +2659,47 @@ val sem-vzeroall = do
     return void
 end
 
+val sem-vzeroupper = do
+  size <- return 128;
+  mode64 <- mode64?;
+
+  xmm0 <- return (semantic-register-of-offset XMM0 size);
+  mov size xmm0 (imm 0);
+  xmm1 <- return (semantic-register-of-offset XMM1 size);
+  mov size xmm1 (imm 0);
+  xmm2 <- return (semantic-register-of-offset XMM2 size);
+  mov size xmm2 (imm 0);
+  xmm3 <- return (semantic-register-of-offset XMM3 size);
+  mov size xmm3 (imm 0);
+  xmm4 <- return (semantic-register-of-offset XMM4 size);
+  mov size xmm4 (imm 0);
+  xmm5 <- return (semantic-register-of-offset XMM5 size);
+  mov size xmm5 (imm 0);
+  xmm6 <- return (semantic-register-of-offset XMM6 size);
+  mov size xmm6 (imm 0);
+  xmm7 <- return (semantic-register-of-offset XMM7 size);
+  mov size xmm7 (imm 0);
+  if mode64 then do
+    xmm8 <- return (semantic-register-of-offset XMM8 size);
+    mov size xmm8 (imm 0);
+    xmm9 <- return (semantic-register-of-offset XMM9 size);
+    mov size xmm9 (imm 0);
+    xmm10 <- return (semantic-register-of-offset XMM10 size);
+    mov size xmm10 (imm 0);
+    xmm11 <- return (semantic-register-of-offset XMM11 size);
+    mov size xmm11 (imm 0);
+    xmm12 <- return (semantic-register-of-offset XMM12 size);
+    mov size xmm12 (imm 0);
+    xmm13 <- return (semantic-register-of-offset XMM13 size);
+    mov size xmm13 (imm 0);
+    xmm14 <- return (semantic-register-of-offset XMM14 size);
+    mov size xmm14 (imm 0);
+    xmm15 <- return (semantic-register-of-offset XMM15 size);
+    mov size xmm15 (imm 0)
+  end else
+    return void
+end
+
 ## W>>
 ## X>>
 

specifications/x86/x86-rreil-translator.ml

@@ -604,7 +604,8 @@ end
 
 val sem-undef-varity x = do
   case x of
-     VA1 x: sem-undef-arity1 x
+     VA0 x: sem-undef-arity0 x
+   | VA1 x: sem-undef-arity1 x
    | VA2 x: sem-undef-arity2 x
    | VA3 x: sem-undef-arity3 x
    | VA4 x: sem-undef-arity4 x
@@ -2227,7 +2228,7 @@ val semantics insn =
    | VUNPCKLPS x: sem-undef-varity x
    | VXORPS x: sem-undef-varity x
    | VZEROALL v: sem-vzeroall
-   | VZEROUPPER x: sem-undef-varity x
+   | VZEROUPPER v: sem-vzeroupper
    | WAIT x: sem-undef-arity0 x
    | WBINVD x: sem-undef-arity0 x
    | WRFSBASE x: sem-undef-arity1 x