GaloisInc/macaw
1
1
Fork 0
mirror of https://github.com/GaloisInc/macaw.git synced 2024-12-28 08:34:23 +03:00
Code Issues Projects Releases Wiki Activity

[x86] Add semantics for sqrtss and sqrtsd.

Browse Source
This commit is contained in:
Kevin Quick 2018-10-31 11:46:01 -07:00
parent aa87eb9a45
commit 6212a69233
No known key found for this signature in database
GPG Key ID: E6D7733599CC0A21
3 changed files with 16 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
x86/src/Data/Macaw/X86/ArchTypes.hs
View File

@ -200,6 +200,7 @@ data SSE_Op
| SSE_Div
| SSE_Min
| SSE_Max
| SSE_Sqrt
-- | Return the name of the mnemonic associated with the SSE op.
sseOpName :: SSE_Op -> String
@ -211,6 +212,7 @@ sseOpName f =
SSE_Div -> "div"
SSE_Min -> "min"
SSE_Max -> "max"
SSE_Sqrt -> "sqrt"
-- | A single or double value for floating-point restricted to this types.
data SSE_FloatType tp where

14
x86/src/Data/Macaw/X86/Semantics.hs
View File

@ -2033,7 +2033,11 @@ def_divps = def_xmm_packed SSE_Div
-- RCPPS Compute reciprocals of packed single-precision floating-point values
-- RCPSS Compute reciprocal of scalar single-precision floating-point values
-- SQRTPS Compute square roots of packed single-precision floating-point values
-- SQRTSS Compute square root of scalar single-precision floating-point values
-- |SQRTSS Compute square root of scalar single-precision floating-point values
def_sqrtss :: InstructionDef
def_sqrtss = def_xmm_ss SSE_Sqrt
-- RSQRTPS Compute reciprocals of square roots of packed single-precision floating-point values
-- RSQRTSS Compute reciprocal of square root of scalar single-precision floating-point values
@ -2322,7 +2326,11 @@ def_divsd = def_xmm_sd SSE_Div
-- DIVPD Divide packed double-precision floating-point values
-- SQRTPD Compute packed square roots of packed double-precision floating-point values
-- SQRTSD Compute scalar square root of scalar double-precision floating-point values
-- | SQRTSD Compute scalar square root of scalar double-precision floating-point values
def_sqrtsd :: InstructionDef
def_sqrtsd = def_xmm_sd SSE_Sqrt
-- MAXPD Return maximum packed double-precision floating-point values
-- MAXSD Return maximum scalar double-precision floating-point values
-- MINPD Return minimum packed double-precision floating-point values
@ -2813,6 +2821,8 @@ all_instructions =
, def_mulss
, def_divss
, def_minss
, def_sqrtss
, def_sqrtsd
, def_minps
, def_maxss
, def_maxps

2
x86_symbolic/src/Data/Macaw/X86/Crucible.hs
View File

@ -183,6 +183,8 @@ pureSem sym fn = do
iFloatMin @_ @(FloatInfoFromSSEType (M.BVType w)) symi x'' y''
M.SSE_Max ->
iFloatMax @_ @(FloatInfoFromSSEType (M.BVType w)) symi x'' y''
M.SSE_Sqrt ->
iFloatSqrt @_ @(FloatInfoFromSSEType (M.BVType w)) symi RTP x''
M.SSE_CMPSX op (tp :: M.SSE_FloatType tp) x y -> do
x' <- toValFloat symi tp x
y' <- toValFloat symi tp y