Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Merged
merged 3 commits into from
Dec 22, 2020
Merged

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

Changes from 2 commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
ef77efc
x86: Fix semantics for pinsrw, add semantics for pinsr{b,d,q}
chameco Dec 17, 2020
c6baae5
Merge branch 'master' into sb/pinsrx
chameco Dec 21, 2020
90b7dda
x86: Add comments on exec_pinsrx parameters
chameco Dec 22, 2020
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
51 changes: 41 additions & 10 deletions x86/src/Data/Macaw/X86/Semantics.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Could we get a comment explaining what w and c are here?

Are the mask values just taken from the ISA manual?

Copy link
Contributor Author

@chameco chameco Dec 22, 2020 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I've added some Haddock comments to those parameters.

The ISA manual specifies to use the 1, 2, 3, or 4 least significant bits of the immediate (depending on the instruction / whether the destination is MMX or XMM for pinsrw). I can add comments explaining the masks in this light if you'd like. I could also use a binary literal which makes the masks more apparent, but this would require enabling the BinaryLiterals extension.

-> 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
Expand Down Expand Up @@ -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
Expand Down