diff --git a/x86/src/Data/Macaw/X86/ArchTypes.hs b/x86/src/Data/Macaw/X86/ArchTypes.hs index 5c18ae7c..8889687e 100644 --- a/x86/src/Data/Macaw/X86/ArchTypes.hs +++ b/x86/src/Data/Macaw/X86/ArchTypes.hs @@ -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 diff --git a/x86/src/Data/Macaw/X86/Semantics.hs b/x86/src/Data/Macaw/X86/Semantics.hs index 644e6858..d768d799 100644 --- a/x86/src/Data/Macaw/X86/Semantics.hs +++ b/x86/src/Data/Macaw/X86/Semantics.hs @@ -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 diff --git a/x86_symbolic/src/Data/Macaw/X86/Crucible.hs b/x86_symbolic/src/Data/Macaw/X86/Crucible.hs index 32978d00..dfdb3bca 100644 --- a/x86_symbolic/src/Data/Macaw/X86/Crucible.hs +++ b/x86_symbolic/src/Data/Macaw/X86/Crucible.hs @@ -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