Add AVX2 VPBLENDD instruction

[jakemas]

Issue #, if available:
N/A
Description of changes:
This change models the AVX2 Vector Packed Blend Doublewords (VPBLENDD) instruction.

Callouts:
I had to add a new section | VEXM_0F3A -> within decode.ml

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

[jakemas]

Having some issues with this one getting picked up correctly by decode.ml. My thoughts are that the new section VEXM_0F3A -> may not be implemented correctly.

[jakemas]

Ok I think I got it!

[pennyannn]

In order to support VPBLENDD in the simd way, I added a couple new functions msimd16,msimd8,.msimd4 and msimd2 that would allow us to take in a third input that represents the imm8 used for masking. Ultimately these functions should go to HOL Light? @jargh

When testing the instruction, I found that the existing tests might have some issues.

[jargh]

Yes, I think @pennyannn's addition of the "msimd" constructs is a good idea, since these make the definition here quite clean and structurally similar to the others. If we add these here we can move them upstream into HOL Light at a later date.

[aqjune-aws]

Hey - do you have any idea why the x86 cosimulator is failing? It hits this bytecode 0xc4e37302ca00 and it seems this is an illegal instruction.

[jakemas]

Hey - do you have any idea why the x86 cosimulator is failing? It hits this bytecode 0xc4e37302ca00 and it seems this is an illegal instruction.

I'm confused, I ran a simple test, and the decoder picked it up as a VPBLENDD as intended:

# let test_bytes = [0xc4; 0xe3; 0x73; 0x02; 0xca; 0x00];;
val test_bytes : int list = [196; 227; 115; 2; 202; 0]
#let test_list = mk_flist (map (curry mk_comb `word:num->byte` o mk_small_numeral) test_bytes);;
val test_list : term =
  `[word 196; word 227; word 115; word 2; word 202; word 0]`
# DECODE_CONV (mk_comb (`decode`, test_list));;
val it : thm =
  |- decode [word 196; word 227; word 115; word 2; word 202; word 0] =
     SOME (VPBLENDD (%_% xmm1) (%_% xmm1) (%_% xmm2) (Imm8 (word 0)),[])
# 

XMM cases failing, YMM cases working? Indicates my test cases are fine, the decoder is working, its a problem with the definition, working on that now (so far 30min cosimulating no issues).

got it :) 01e778f

[aqjune-aws]

I confirmed that running the cosimulator with the new instruction patterns ran successfully.

Moved msimd* to common/words2.ml, and slightly increased the running times of arm/x86 cosimulators from 30 mins to 45 mins because both of these are having more patterns than before (when it was set to 30min :).