From ef77efc363f4cf03157a21193909400e04d5c1a6 Mon Sep 17 00:00:00 2001
From: Samuel Breese <samuel@chame.co>
Date: Thu, 17 Dec 2020 15:23:29 -0500
Subject: [PATCH 1/2] x86: Fix semantics for pinsrw, add semantics for
 pinsr{b,d,q}

---
 x86/src/Data/Macaw/X86/Semantics.hs | 51 +++++++++++++++++++++++------
 1 file changed, 41 insertions(+), 10 deletions(-)

diff --git a/x86/src/Data/Macaw/X86/Semantics.hs b/x86/src/Data/Macaw/X86/Semantics.hs
index 32029293..9b337657 100644
--- a/x86/src/Data/Macaw/X86/Semantics.hs
+++ b/x86/src/Data/Macaw/X86/Semantics.hs
@@ -2450,23 +2450,51 @@ def_pselect mnem op sz = defBinaryLV mnem $ \l v -> do
 -- PEXTRW Extract word
 
 -- | PINSRW Insert word
-exec_pinsrw :: Location (Addr ids) XMMType -> BVExpr ids 16 -> Word8 -> X86Generator st ids ()
-exec_pinsrw l v off = do
+exec_pinsrx :: (1 <= w, 1 <= c)
+            => NatRepr w
+            -> NatRepr c
+            -> Location (Addr ids) (BVType c)
+            -> BVExpr ids w
+            -> Word8
+            -> X86Generator st ids ()
+exec_pinsrx w c l v off = do
   lv <- get l
-  -- FIXME: is this the right way around?
-  let ls = bvVectorize n16 lv
-      (lower, _ : upper) = splitAt (fromIntegral off - 1) ls
+  let ls = bvVectorize w lv
+      (lower, _ : upper) = splitAt (length ls - fromIntegral off - 1) ls
       ls' = lower ++ [v] ++ upper
-  l .= bvUnvectorize knownNat ls'
+  l .= bvUnvectorize c ls'
 
 def_pinsrw :: InstructionDef
 def_pinsrw = defTernary "pinsrw" $ \_ loc val imm -> do
-  l  <- getBVLocation loc knownNat
-  v  <- truncateBVValue knownNat =<< getSomeBVValue val
+  SomeBV l  <- getSomeBVLocation loc
+  v  <- truncateBVValue n16 =<< getSomeBVValue val
   case imm of
-    F.ByteImm off -> exec_pinsrw l v off
+    F.ByteImm off
+      | Just Refl <- testEquality (typeWidth l) n64
+        -> exec_pinsrx n16 n64 l v $ off Bits..&. 0x3
+      | Just Refl <- testEquality (typeWidth l) n128
+        -> exec_pinsrx n16 n128 l v $ off Bits..&. 0x7
+      | otherwise -> fail "pinsrw: Unknown bit width"
     _ -> fail "Bad offset to pinsrw"
 
+-- | PINSRB Insert byte
+-- PINSRD Insert doubleword
+-- PINSRQ Insert quadword
+def_pinsrx :: (1 <= w)
+          => String
+          -> NatRepr w
+          -> Word8
+          -> InstructionDef
+def_pinsrx mnem w mask = defTernary mnem $ \_ loc val imm -> do
+  l  <- getBVLocation loc n128
+  v  <- truncateBVValue w =<< getSomeBVValue val
+  case imm of
+    F.ByteImm off
+      | Just Refl <- testEquality (typeWidth l) n128
+        -> exec_pinsrx w n128 l v $ off Bits..&. mask
+      | otherwise -> fail $ mnem ++ ": Unknown bit width"
+    _ -> fail $ "Bad offset to " ++ mnem
+
 -- PMAXUB Maximum of packed unsigned byte integers
 -- PMAXSW Maximum of packed signed word integers
 -- PMINUB Minimum of packed unsigned byte integers
@@ -2963,7 +2991,10 @@ all_instructions =
   , def_cvtsi2sX "cvtsi2ss" SSE_Single
   , def_cvttsX2si "cvttsd2si" SSE_Double
   , def_cvttsX2si "cvttss2si" SSE_Single
-  , def_pinsrw
+  , def_pinsrx "pinsrb" n8 0xF
+  , def_pinsrw -- pinsrw is defined separately since it can be applied to both MMX and XMM registers
+  , def_pinsrx "pinsrd" n32 0x3
+  , def_pinsrx "pinsrq" n64 0x1
   , def_cmpsX "cmpsd" SSE_Double
   , def_cmpsX "cmpss" SSE_Single
   , def_andpd

From 90b7ddac6c21c5983606e9682f7f97b51d0439b9 Mon Sep 17 00:00:00 2001
From: Samuel Breese <samuel@chame.co>
Date: Tue, 22 Dec 2020 12:48:24 -0500
Subject: [PATCH 2/2] x86: Add comments on exec_pinsrx parameters

---
 x86/src/Data/Macaw/X86/Semantics.hs | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/x86/src/Data/Macaw/X86/Semantics.hs b/x86/src/Data/Macaw/X86/Semantics.hs
index 9b337657..86c7ce09 100644
--- a/x86/src/Data/Macaw/X86/Semantics.hs
+++ b/x86/src/Data/Macaw/X86/Semantics.hs
@@ -2451,11 +2451,11 @@ def_pselect mnem op sz = defBinaryLV mnem $ \l v -> do
 
 -- | PINSRW Insert word
 exec_pinsrx :: (1 <= w, 1 <= c)
-            => NatRepr w
-            -> NatRepr c
-            -> Location (Addr ids) (BVType c)
-            -> BVExpr ids w
-            -> Word8
+            => NatRepr w -- ^ Width of element to insert
+            -> NatRepr c -- ^ Width of destination registr
+            -> Location (Addr ids) (BVType c) -- ^ Destination operand
+            -> BVExpr ids w -- ^ Source operand
+            -> Word8 -- ^ Offset in destination
             -> X86Generator st ids ()
 exec_pinsrx w c l v off = do
   lv <- get l