GaloisInc/macaw
1
1
Fork 0
mirror of https://github.com/GaloisInc/macaw.git synced 2024-11-29 21:44:11 +03:00
Code Issues Projects Releases Wiki Activity

Add symbolic semantics for X86 sse_ucomis and sse_cvttsx2si.

Browse Source
This commit is contained in:
Andrei Stefanescu 2018-09-19 18:47:47 -07:00
parent c5f0806751
commit 59b756c185
3 changed files with 24 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
symbolic/src/Data/Macaw/Symbolic/CrucGen.hs
View File

@ -71,9 +71,11 @@ import qualified Data.Map.Strict as Map
import Data.Maybe
import Data.Parameterized.Classes
import Data.Parameterized.Context as Ctx
import qualified Data.Parameterized.List as P
import Data.Parameterized.Map (MapF)
import qualified Data.Parameterized.Map as MapF
import Data.Parameterized.NatRepr
import Data.Parameterized.Some
import qualified Data.Parameterized.TH.GADT as U
import Data.Parameterized.TraversableF
import Data.Parameterized.TraversableFC
@ -676,8 +678,14 @@ appToCrucible app = do
M.TupleTypeRepr _ -> fail "XXX: Mux on tuples not yet done."
M.TupleField tps x i ->
undefined tps x i -- TODO: Fix this
M.TupleField tps x i -> do
let tps' = typeListToCrucible tps
tp' = typeToCrucible $ tps P.!! i
x' <- v2c x
case Ctx.intIndex (fromIntegral $ P.indexValue i) (Ctx.size tps') of
Just (Some i') | Just Refl <- testEquality tp' (tps' Ctx.! i') ->
appAtom $ C.GetStruct x' i' tp'
_ -> fail ""
-- Booleans

1
symbolic/src/Data/Macaw/Symbolic/PersistentState.hs
View File

@ -31,6 +31,7 @@ module Data.Macaw.Symbolic.PersistentState
, floatInfoToCrucible
, floatInfoFromCrucible
, typeCtxToCrucible
, typeListToCrucible
, macawAssignToCrucM
, memReprToCrucible
-- * Register index map

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

@ -209,7 +209,18 @@ pureSem sym fn = do
zeros <- minUnsignedBV symi knownNat
ones <- maxUnsignedBV symi knownNat
llvmPointer_bv symi =<< bvIte symi res ones zeros
M.SSE_UCOMIS {} -> error "SSE_UCOMIS"
M.SSE_UCOMIS (tp :: M.SSE_FloatType tp) x y -> do
x' <- toValFloat symi tp x
y' <- toValFloat symi tp y
is_eq <- iFloatFpEq @_ @(FloatInfoFromSSEType tp) symi x' y'
is_lt <- iFloatLt @_ @(FloatInfoFromSSEType tp) symi x' y'
x_is_nan <- iFloatIsNaN @_ @(FloatInfoFromSSEType tp) symi x'
y_is_nan <- iFloatIsNaN @_ @(FloatInfoFromSSEType tp) symi y'
is_unord <- orPred symi x_is_nan y_is_nan
zf <- orPred symi is_eq is_unord
cf <- orPred symi is_lt is_unord
let pf = is_unord
return $ empty `extend` (RV zf) `extend` (RV pf) `extend` (RV cf)
M.SSE_CVTSS2SD x ->
fromValFloat symi M.SSE_Double
=<< iFloatCast @_ @DoubleFloat @SingleFloat symi knownRepr RNE
@ -224,7 +235,7 @@ pureSem sym fn = do
=<< toValBV symi x
M.SSE_CVTTSX2SI w (tp :: M.SSE_FloatType tp) x ->
llvmPointer_bv symi
=<< iFloatToSBV @_ @_ @(FloatInfoFromSSEType tp) symi w RNE
=<< iFloatToSBV @_ @_ @(FloatInfoFromSSEType tp) symi w RTZ
=<< toValFloat symi tp x
M.EvenParity x0 ->