This commit adds AVX2 instruction vpand.

Signed-off-by: dkostic <[email protected]>

Author: dkostic

x86/allowed_asm

@@ -120,6 +120,7 @@
 : testq$
 : vpxor$
 : vpaddw$
+: vpand$
 : vpmulhw$
 : vpmullw$
 : vpsubw$

x86/proofs/decode.ml

@@ -594,6 +594,10 @@ let decode_aux = new_definition `!pfxs rex l. decode_aux pfxs rex l =
           let sz = vexL_size L in
           (read_ModRM rex l >>= \((reg,rm),l).
             SOME (VPMULLW (mmreg reg sz) (mmreg v sz) (simd_of_RM sz rm),l))
+        | [0xdb:8] ->
+          let sz = vexL_size L in
+          (read_ModRM rex l >>= \((reg,rm),l).
+            SOME (VPAND (mmreg reg sz) (mmreg v sz) (simd_of_RM sz rm),l))
         | [0xe5:8] ->
           let sz = vexL_size L in
           (read_ModRM rex l >>= \((reg,rm),l).

x86/proofs/instruction.ml

@@ -305,6 +305,7 @@ let instruction_INDUCTION,instruction_RECURSION = define_type
    | TEST operand operand
    | TZCNT operand operand
    | VPADDW operand operand operand
+   | VPAND operand operand operand
    | VPMULHW operand operand operand
    | VPMULLW operand operand operand
    | VPSUBW operand operand operand

x86/proofs/simulator.ml

@@ -296,6 +296,7 @@ let iclasses = iclasses @
  [0xc4; 0x41; 0x45; 0xfd; 0xdb]; (* VPADDW (%_% ymm11) (%_% ymm7) (%_% ymm11) *)
  [0xc5; 0x7d; 0xd5; 0xc9]; (* VPMULLW (%_% ymm1) (%_% ymm0) (%_% ymm9) *)
  [0xc5; 0x45; 0xe5; 0xfb]; (* VPMULHW (%_% ymm15) (%_% ymm7) (%_% ymm3) *)
+ [0xc5; 0xa5; 0xdb; 0xd2]; (* VPAND (%_% ymm2) (%_% ymm11) (%_% ymm2) *)
 ];;
 
 (* ------------------------------------------------------------------------- *)

x86/proofs/x86.ml

@@ -1367,6 +1367,13 @@ let x86_TZCNT = new_definition
          ZF := (val z = 0) ,,
          UNDEFINED_VALUES[OF;SF;PF;AF]) s`;;
 
+let x86_VPAND = new_definition
+ `x86_VPAND dest src1 src2 (s:x86state) =
+        let x = read src1 s
+        and y = read src2 s in
+        let z = word_and x y in
+        (dest := (z:N word)) s`;;
+
 let x86_VPXOR = new_definition
  `x86_VPXOR dest src1 src2 (s:x86state) =
         let x = read src1 s
@@ -2035,6 +2042,10 @@ let x86_execute = define
         (match operand_size dest with
           256 -> x86_VPXOR (OPERAND256 dest s) (OPERAND256 src1 s) (OPERAND256 src2 s)
         | 128 -> x86_VPXOR (OPERAND128 dest s) (OPERAND128 src1 s) (OPERAND128 src2 s)) s
+    | VPAND dest src1 src2 ->
+        (match operand_size dest with
+          256 -> x86_VPAND (OPERAND256 dest s) (OPERAND256 src1 s) (OPERAND256 src2 s)
+        | 128 -> x86_VPAND (OPERAND128 dest s) (OPERAND128 src1 s) (OPERAND128 src2 s)) s
     | XCHG dest src ->
         (match operand_size dest with
           64 -> x86_XCHG (OPERAND64 dest s) (OPERAND64 src s)
@@ -2776,7 +2787,7 @@ let X86_OPERATION_CLAUSES =
     x86_STC; x86_SUB_ALT; x86_TEST; x86_TZCNT; x86_XCHG; x86_XOR;
     (*** AVX2 instructions ***)
     x86_VPADDW_ALT; x86_VPMULHW_ALT; x86_VPMULLW_ALT; x86_VPSUBW_ALT;
-    x86_VPXOR;
+    x86_VPXOR; x86_VPAND;
     (*** 32-bit backups since the ALT forms are 64-bit only ***)
     INST_TYPE[`:32`,`:N`] x86_ADC;
     INST_TYPE[`:32`,`:N`] x86_ADCX;