Add AVX2 VPBLENDD instruction

arm/proofs/simulator.ml

@@ -595,7 +595,7 @@ let run_random_simulation() =
     let decoded, result = run_random_memopsimulation() in
     decoded,result,false;;
 
-let time_limit_sec = 1800.0;;
+let time_limit_sec = 2400.0;;
 let tested_reg_instances = ref 0;;
 let tested_mem_instances = ref 0;;
 

common/words2.ml

@@ -429,3 +429,26 @@ let READ_WORD_CONV =
   | Comb(Const("read_int64",_),l') ->
     let ls,f = prove_hyps 8 l' in f (INST ls pthi8)
   | _ -> failwith "READ_WORD_CONV";;
+
+(* ------------------------------------------------------------------------- *)
+(* Extension of the simd function family to 3 operands.                      *)
+(* ------------------------------------------------------------------------- *)
+
+let msimd2 = new_definition
+ `(msimd2:(M word->N word->N word->N word)->
+        ((M)tybit0)word->((N)tybit0)word->((N)tybit0) word->((N)tybit0) word) f m x y =
+    word_join (f (word_subword m (dimindex(:M),dimindex(:M)))
+                 (word_subword x (dimindex(:N),dimindex(:N)))
+                 (word_subword y (dimindex(:N),dimindex(:N))))
+              (f (word_subword m (0,dimindex(:M)))
+                 (word_subword x (0,dimindex(:N)))
+                 (word_subword y (0,dimindex(:N))))`;;
+
+let msimd4 = new_definition
+ `msimd4 (f:M word->N word->N word->N word) = msimd2 (msimd2 f)`;;
+
+let msimd8 = new_definition
+ `msimd8 (f:M word->N word->N word->N word) = msimd2 (msimd4 f)`;;
+
+let msimd16 = new_definition
+ `msimd16 (f:M word->N word->N word->N word) = msimd2 (msimd8 f)`;;

x86/allowed_asm

@@ -124,6 +124,7 @@
 : vpaddw$
 : vpaddd$
 : vpand$
+: vpblendd$
 : vpbroadcastd$
 : vpmuldq$
 : vmovdqa$

x86/proofs/decode.ml

@@ -697,6 +697,15 @@ let decode_aux = new_definition `!pfxs rex l. decode_aux pfxs rex l =
               | _ -> NONE))
             | _ -> NONE)
           | _ -> NONE)
+    | VEXM_0F3A ->
+        read_byte l >>= \(b,l).
+        (bitmatch b with
+        | [0x02:8] ->
+          let sz = vexL_size L in
+          (read_ModRM rex l >>= \((reg,rm),l).
+            read_imm Byte l >>= \(imm8,l).
+            SOME (VPBLENDD (mmreg reg sz) (mmreg v sz) (simd_of_RM sz rm) imm8,l))
+        | _ -> NONE)
     | _ -> NONE)
   | [0b1100011:7; v] -> if has_unhandled_pfxs pfxs then NONE else
     let sz = op_size_W rex v pfxs in

x86/proofs/instruction.ml

@@ -310,6 +310,7 @@ let instruction_INDUCTION,instruction_RECURSION = define_type
    | VPADDW operand operand operand
    | VPADDD operand operand operand
    | VPAND operand operand operand
+   | VPBLENDD operand operand operand operand
    | VPBROADCASTD operand operand
    | VPMULDQ operand operand operand
    | VPMULHW operand operand operand

x86/proofs/simulator.ml

@@ -374,6 +374,24 @@ let iclasses = iclasses @
  [0xc5; 0x85; 0xf9; 0xf6]; (* VPSUBW (%_% ymm6) (%_% ymm15) (%_% ymm6) *)
  [0xc5; 0x45; 0xfd; 0xd9]; (* VPADDW (%_% ymm11) (%_% ymm7) (%_% ymm11) *)
  [0xc5; 0x41; 0xfd; 0xd9]; (* VPADDW (%_% ymm11) (%_% ymm7) (%_% ymm11) *)
+ [0xc4; 0xe3; 0x7d; 0x02; 0xc1; 0xff]; (* VPBLENDD ymm0, ymm0, ymm1, 0xff *)
+ [0xc4; 0xe3; 0x75; 0x02; 0xca; 0x00]; (* VPBLENDD ymm1, ymm1, ymm2, 0x00 *)
+ [0xc4; 0xe3; 0x6d; 0x02; 0xd3; 0x55]; (* VPBLENDD ymm2, ymm2, ymm3, 0x55 *)
+ [0xc4; 0xe3; 0x65; 0x02; 0xdc; 0xaa]; (* VPBLENDD ymm3, ymm3, ymm4, 0xaa *)
+ [0xc4; 0xe3; 0x5d; 0x02; 0xe5; 0x0f]; (* VPBLENDD ymm4, ymm4, ymm5, 0x0f *)
+ [0xc4; 0xe3; 0x55; 0x02; 0xee; 0xf0]; (* VPBLENDD ymm5, ymm5, ymm6, 0xf0 *)
+ [0xc4; 0x43; 0x7d; 0x02; 0xc1; 0xf0]; (* VPBLENDD ymm8, ymm8, ymm9, 0xf0 *)
+ [0xc4; 0x43; 0x5d; 0x02; 0xd3; 0x33]; (* VPBLENDD ymm10, ymm10, ymm11, 0x33 *)
+ [0xc4; 0x43; 0x3d; 0x02; 0xe5; 0xcc]; (* VPBLENDD ymm12, ymm12, ymm13, 0xcc *)
+ [0xc4; 0x43; 0x1d; 0x02; 0xf7; 0x3c]; (* VPBLENDD ymm14, ymm14, ymm15, 0x3c *)
+ [0xc4; 0xe3; 0x79; 0x02; 0xc1; 0x0f]; (* VPBLENDD xmm0, xmm0, xmm1, 0x0f *)
+ [0xc4; 0xe3; 0x71; 0x02; 0xca; 0x00]; (* VPBLENDD xmm1, xmm1, xmm2, 0x00 *)
+ [0xc4; 0xe3; 0x69; 0x02; 0xd3; 0x05]; (* VPBLENDD xmm2, xmm2, xmm3, 0x05 *)
+ [0xc4; 0xe3; 0x61; 0x02; 0xdc; 0x0a]; (* VPBLENDD xmm3, xmm3, xmm4, 0x0a *)
+ [0xc4; 0x43; 0x39; 0x02; 0xc1; 0x0a]; (* VPBLENDD xmm8, xmm8, xmm9, 0x0a *)
+ [0xc4; 0x43; 0x59; 0x02; 0xd3; 0x0c]; (* VPBLENDD xmm10, xmm10, xmm11, 0x0c *)
+ [0xc4; 0x43; 0x19; 0x02; 0xe5; 0x06]; (* VPBLENDD xmm12, xmm12, xmm13, 0x06 *)
+ [0xc4; 0x43; 0x09; 0x02; 0xf7; 0x03]; (* VPBLENDD xmm14, xmm14, xmm15, 0x03 *)
  [0xc4; 0xe2; 0x79; 0x58; 0xc1]; (* VPBROADCASTD xmm0, xmm1 *)
  [0xc4; 0xe2; 0x79; 0x58; 0xca]; (* VPBROADCASTD xmm1, xmm2 *)
  [0xc4; 0xe2; 0x7d; 0x58; 0xd3]; (* VPBROADCASTD ymm2, xmm3 *)
@@ -1042,7 +1060,7 @@ let run_random_simulation() =
     let decoded, result = run_random_memopsimulation() in
     decoded,result,false;;
 
-let time_limit_sec = 1800.0;;
+let time_limit_sec = 2400.0;;
 let tested_reg_instances = ref 0;;
 let tested_mem_instances = ref 0;;
 

x86/proofs/x86.ml

@@ -1312,7 +1312,7 @@ let x86_VMOVDQA = new_definition
   `x86_VMOVDQA dest src (s:x86state) =
       let (x:N word) = read src s in
       (dest := (word_zx x):N word) s`;;
-
+       
 let x86_VMOVSHDUP = new_definition
   `x86_VMOVSHDUP dest src (s:x86state) =
       let (x:N word) = read src s in
@@ -1327,7 +1327,17 @@ let x86_VMOVSHDUP = new_definition
           (word_zx x) in
         (dest := (word_zx res):N word) s`;;
 
-
+let x86_VPADDD = new_definition
+  `x86_VPADDD dest src1 src2 (s:x86state) =
+      let (x:N word) = read src1 s
+      and (y:N word) = read src2 s in
+      if dimindex(:N) = 256 then
+        let res:(256)word = simd8 word_add (word_zx x) (word_zx y) in
+        (dest := (word_zx res):N word) s
+      else
+        let res:(128)word = simd4 word_add (word_zx x) (word_zx y) in
+        (dest := (word_zx res):N word) s`;;
+
 let x86_VPADDW = new_definition
   `x86_VPADDW dest src1 src2 (s:x86state) =
       let (x:N word) = read src1 s
@@ -1339,15 +1349,17 @@ let x86_VPADDW = new_definition
         let res:(128)word = simd8 word_add (word_zx x) (word_zx y) in
         (dest := (word_zx res):N word) s`;;
 
-let x86_VPADDD = new_definition
-  `x86_VPADDD dest src1 src2 (s:x86state) =
+let x86_VPBLENDD = new_definition
+  `x86_VPBLENDD dest src1 src2 imm8 (s:x86state) =
       let (x:N word) = read src1 s
-      and (y:N word) = read src2 s in
+      and (y:N word) = read src2 s
+      and imm8 = read imm8 s in
+      let fn = \(i:1 word) (x:32 word) (y:32 word). if i = word 1 then y else x in
       if dimindex(:N) = 256 then
-        let res:(256)word = simd8 word_add (word_zx x) (word_zx y) in
+        let res:(256)word = msimd8 fn (word_zx imm8) (word_zx x) (word_zx y) in
         (dest := (word_zx res):N word) s
       else
-        let res:(128)word = simd4 word_add (word_zx x) (word_zx y) in
+        let res:(128)word = msimd4 fn (word_zx imm8) (word_zx x) (word_zx y) in
         (dest := (word_zx res):N word) s`;;
 
 let x86_VPBROADCASTD = new_definition
@@ -2172,14 +2184,18 @@ let x86_execute = define
         (match operand_size dest with
           256 -> x86_VMOVSHDUP (OPERAND256 dest s) (OPERAND256 src s)
         | 128 -> x86_VMOVSHDUP (OPERAND128 dest s) (OPERAND128 src s)) s
+    | VPADDD dest src1 src2 ->
+        (match operand_size dest with
+          256 -> x86_VPADDD (OPERAND256 dest s) (OPERAND256 src1 s) (OPERAND256 src2 s)
+        | 128 -> x86_VPADDD (OPERAND128 dest s) (OPERAND128 src1 s) (OPERAND128 src2 s)) s
     | VPADDW dest src1 src2 ->
         (match operand_size dest with
           256 -> x86_VPADDW (OPERAND256 dest s) (OPERAND256 src1 s) (OPERAND256 src2 s)
         | 128 -> x86_VPADDW (OPERAND128 dest s) (OPERAND128 src1 s) (OPERAND128 src2 s)) s
-    | VPADDD dest src1 src2 ->
+    | VPBLENDD dest src1 src2 imm8 ->
         (match operand_size dest with
-          256 -> x86_VPADDD (OPERAND256 dest s) (OPERAND256 src1 s) (OPERAND256 src2 s)
-        | 128 -> x86_VPADDD (OPERAND128 dest s) (OPERAND128 src1 s) (OPERAND128 src2 s)) s
+          256 -> x86_VPBLENDD (OPERAND256 dest s) (OPERAND256 src1 s) (OPERAND256 src2 s) (OPERAND8 imm8 s)
+        | 128 -> x86_VPBLENDD (OPERAND128 dest s) (OPERAND128 src1 s) (OPERAND128 src2 s) (OPERAND8 imm8 s)) s
     | VPBROADCASTD dest src ->
         (match operand_size dest with
           256 -> x86_VPBROADCASTD (OPERAND256 dest s) (OPERAND128 src s)
@@ -2941,7 +2957,7 @@ let x86_RET_POP_RIP = prove
 (*** Simplify word operations in SIMD instructions ***)
 
 let all_simd_rules =
-   [usimd16;usimd8;usimd4;usimd2;simd16;simd8;simd4;simd2];;
+   [usimd16;usimd8;usimd4;usimd2;simd16;simd8;simd4;simd2;msimd16;msimd8;msimd4;msimd2];;
 
 let EXPAND_SIMD_RULE =
   CONV_RULE (TOP_DEPTH_CONV WORD_SIMPLE_SUBWORD_CONV) o
@@ -2956,6 +2972,7 @@ let x86_VMOVDQA_ALT = EXPAND_SIMD_RULE x86_VMOVDQA;;
 let x86_VMOVSHDUP_ALT = EXPAND_SIMD_RULE x86_VMOVSHDUP;;
 let x86_VPADDD_ALT = EXPAND_SIMD_RULE x86_VPADDD;;
 let x86_VPADDW_ALT = EXPAND_SIMD_RULE x86_VPADDW;;
+let x86_VPBLENDD_ALT = EXPAND_SIMD_RULE x86_VPBLENDD;;
 let x86_VPBROADCASTD_ALT = EXPAND_SIMD_RULE x86_VPBROADCASTD;;
 let x86_VPMULDQ_ALT = EXPAND_SIMD_RULE x86_VPMULDQ;;
 let x86_VPMULHW_ALT = EXPAND_SIMD_RULE x86_VPMULHW;;
@@ -2988,7 +3005,7 @@ let X86_OPERATION_CLAUSES =
     x86_VPADDD_ALT; x86_VPADDW_ALT; x86_VPMULHW_ALT; x86_VPMULLD_ALT; x86_VPMULLW_ALT;
     x86_VPSUBD_ALT; x86_VPSUBW_ALT; x86_VPXOR; x86_VPAND; x86_VPSRAD_ALT; x86_VPSRAW_ALT;
     x86_VPSRLW_ALT; x86_VPBROADCASTD_ALT; x86_VPSLLQ_ALT; x86_VMOVDQA_ALT; x86_VPMULDQ_ALT;
-    x86_VMOVSHDUP_ALT;
+    x86_VMOVSHDUP_ALT; x86_VPBLENDD_ALT;
     (*** 32-bit backups since the ALT forms are 64-bit only ***)
     INST_TYPE[`:32`,`:N`] x86_ADC;
     INST_TYPE[`:32`,`:N`] x86_ADCX;