x86: Fix semantics for pinsrw, add semantics for pinsr{b,d,q} (#183)

* x86: Fix semantics for pinsrw, add semantics for pinsr{b,d,q} * x86: Add comments on exec_pinsrx parameters
GaloisInc · Dec 22, 2020 · 2bd0633 · 2bd0633
1 parent 765d2e4
commit 2bd0633
Showing 1 changed file with 41 additions and 10 deletions.
diff --git 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 -- ^ 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
-  -- 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