diff --git a/specifications/x86/c/asm-test.s b/specifications/x86/c/asm-test.s index 2686f20a2883d3e9b55838e92b15bc5e15e67e2f..41022570f7e84fbaa619877145fefa99b20a128f 100644 --- a/specifications/x86/c/asm-test.s +++ b/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 diff --git a/specifications/x86/x86-pretty.ml b/specifications/x86/x86-pretty.ml index 65a0b582eeb226e8b37b3514c647748ea985bec9..1061b247ee34694182292fdf9b06b73f14a08540 100644 --- a/specifications/x86/x86-pretty.ml +++ b/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 diff --git a/specifications/x86/x86-rreil-registermapping.ml b/specifications/x86/x86-rreil-registermapping.ml index 00f5668d5fafc8c5ccdf533c8437bc4707a8abce..fee4d556b0fc920a88b27efe25a597ce88591443 100644 --- a/specifications/x86/x86-rreil-registermapping.ml +++ b/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) diff --git a/specifications/x86/x86-rreil-translator-m-z.ml b/specifications/x86/x86-rreil-translator-m-z.ml index 4cde18ff490163ddc69ab7460ba680dad956a61e..f77fff838c8b51ff5d0c5ab789cd15f4c75e872b 100644 --- a/specifications/x86/x86-rreil-translator-m-z.ml +++ b/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>> diff --git a/specifications/x86/x86-rreil-translator.ml b/specifications/x86/x86-rreil-translator.ml index d0f3f0eacbf079a6b839237395e8dd922f83034d..4d4bc68d40145310634d33dc5706caee13c96c8a 100644 --- a/specifications/x86/x86-rreil-translator.ml +++ b/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