Implement vpinsrq and structore for the rest of the vector insert instruction

x86/src/Data/Macaw/X86.hs

@@ -346,6 +346,7 @@ transferAbsValue r f =
     Pointwise2 {} -> TopV
     PointwiseShiftL {} -> TopV
     VExtractF128 {} -> TopV
+    VInsert {} -> TopV
 
 -- | Disassemble block, returning either an error, or a list of blocks
 -- and ending PC.

x86/src/Data/Macaw/X86/ArchTypes.hs

@@ -536,6 +536,15 @@ data X86PrimFn f tp where
     !(f (BVType n)) -> {- /\ second operand -}
     X86PrimFn f (BVType n)
 
+  {- | Update an element of a vector -}
+  VInsert :: (1 <= elSize, 1 <= elNum, (i + 1) <= elNum) =>
+    !(NatRepr elNum)                {- ^ Number of elements in vector -} ->
+    !(NatRepr elSize)               {- ^ Size of each element in bits -} ->
+    !(f (BVType (elNum * elSize)))  {- ^ Insert in this vector -}        ->
+    !(f (BVType elSize))            {- ^ Insert this value -}            ->
+    !(NatRepr i)                    {- ^ At this index -}                ->
+    X86PrimFn f (BVType (elNum * elSize))
+
   {- | Shift left each element in the vector by the given amount.
        The new ("shifted-in") bits are 0 -}
   PointwiseShiftL :: (1 <= elSize, 1 <= elNum, 1 <= sz) =>
@@ -595,6 +604,7 @@ instance HasRepr (X86PrimFn f) TypeRepr where
       X87_FMul{} -> knownRepr
       X87_FST tp _ -> typeRepr tp
       PointwiseShiftL n w _ _ _ -> packedAVX n w
+      VInsert n w _ _ _ -> packedAVX n w
       VOp1 w _ _ -> BVTypeRepr w
       VOp2 w _ _ _ -> BVTypeRepr w
       Pointwise2 n w _ _ _ -> packedAVX n w
@@ -656,6 +666,7 @@ instance TraversableFC X86PrimFn where
       PointwiseShiftL e n s x y -> PointwiseShiftL e n s <$> go x <*> go y
       Pointwise2 n w o x y -> Pointwise2 n w o <$> go x <*> go y
       VExtractF128 x i -> (`VExtractF128` i) <$> go x
+      VInsert n w v e i -> (\v' e' -> VInsert n w v' e' i) <$> go v <*> go e
 
 instance IsArchFn X86PrimFn where
   ppArchFn pp f = do
@@ -699,6 +710,13 @@ instance IsArchFn X86PrimFn where
       Pointwise2 _ w o x y -> sexprA (show o)
                                 [ ppShow (widthVal w) , pp x , pp y ]
       VExtractF128 x i -> sexprA "vextractf128" [ pp x, ppShow i ]
+      VInsert n w v e i -> sexprA "vinsert" [ ppShow (widthVal n)
+                                            , ppShow (widthVal w)
+                                            , pp v
+                                            , pp e
+                                            , ppShow (widthVal i)
+                                            ]
+
 
 -- | This returns true if evaluating the primitive function implicitly
 -- changes the processor state in some way.
@@ -741,6 +759,7 @@ x86PrimFnHasSideEffects f =
     PointwiseShiftL {} -> False
     Pointwise2 {} -> False
     VExtractF128 {} -> False
+    VInsert {} -> False
 
 ------------------------------------------------------------------------
 -- X86Stmt

x86/src/Data/Macaw/X86/Semantics/AVX.hs

@@ -6,6 +6,7 @@ import Data.Int(Int8)
 import Control.Monad(forM_)
 
 import Data.Parameterized.NatRepr
+import Data.Parameterized.Some
 
 import Flexdis86.Register (ymmReg)
 import qualified Flexdis86 as F
@@ -145,6 +146,34 @@ avxPointwiseShiftL mnem sz =
              _ -> fail ("[" ++ mnem ++ "]: invalid arguments")
 
 
+avxInsert :: String -> InstructionDef
+avxInsert mnem =
+  avx4 mnem $ \arg1 arg2 arg3 arg4 ->
+    do SomeBV vec <- getSomeBVValue arg2
+       SomeBV el  <- getSomeBVValue arg3
+       Some i     <- case someNat (fromIntegral arg4) of
+                       Just ok -> return ok
+                       Nothing -> err "Invalid index"
+       let vw  = typeWidth vec
+           elw = typeWidth el
+
+       LeqProof <- case testLeq n1 elw of
+                     Just ok -> return ok
+                     _       -> err "Invalid element width"
+
+       withDivModNat vw elw $ \elN remi ->
+          case ( testEquality remi n0
+               , testLeq n1 elN
+               , testLeq (addNat i n1) elN
+               ) of
+            ( Just Refl, Just LeqProof, Just LeqProof ) ->
+              do v <- eval vec
+                 e <- eval el
+                 arg1 <~ VInsert elN elw v e i
+            _ -> err "Invalid operands"
+  where
+  err :: String -> X86Generator st ids a
+  err msg = fail ("[" ++ mnem ++ "] " ++ show msg)
 
 all_instructions :: [InstructionDef]
 all_instructions =
@@ -196,6 +225,8 @@ all_instructions =
            _ -> fail "[vextractf128] Unexpected operands"
 
   , avxOp2I "vpclmulqdq" VPCLMULQDQ
+
+  , avxInsert "vpinsrq"
   ]
 
 

x86_symbolic/src/Data/Macaw/X86/Crucible.hs

@@ -230,6 +230,8 @@ pureSem sym fn =
 
 
 
+
+
     M.PointwiseShiftL elNum elSz shSz bits amt ->
       do amt' <- getBitVal (symIface sym) amt
          vecOp1 sym LittleEndian (natMultiply elNum elSz) elSz bits $ \xs ->
@@ -239,6 +241,11 @@ pureSem sym fn =
       vecOp2 sym LittleEndian (natMultiply elNum elSz) elSz v1 v2 $ \xs ys ->
         V.zipWith (semPointwise op elSz) xs ys
 
+    M.VInsert elNum elSz vec el i ->
+      do e <- getBitVal (symIface sym) el
+         vecOp1 sym LittleEndian (natMultiply elNum elSz) elSz vec $ \xs ->
+           case mulCancelR elNum (V.length xs) elSz of
+             Refl -> V.insertAt i e xs
 
 semPointwise :: (1 <= w) =>
   M.AVXPointWiseOp2 -> NatRepr w ->