From 59b756c18517f321a6994b7047b5d7568580fc78 Mon Sep 17 00:00:00 2001
From: Andrei Stefanescu <andrei@galois.com>
Date: Wed, 19 Sep 2018 18:47:47 -0700
Subject: [PATCH] Add symbolic semantics for X86 sse_ucomis and sse_cvttsx2si.

---
 symbolic/src/Data/Macaw/Symbolic/CrucGen.hs       | 12 ++++++++++--
 .../src/Data/Macaw/Symbolic/PersistentState.hs    |  1 +
 x86_symbolic/src/Data/Macaw/X86/Crucible.hs       | 15 +++++++++++++--
 3 files changed, 24 insertions(+), 4 deletions(-)

diff --git a/symbolic/src/Data/Macaw/Symbolic/CrucGen.hs b/symbolic/src/Data/Macaw/Symbolic/CrucGen.hs
index 9cca2476..c8c08198 100644
--- a/symbolic/src/Data/Macaw/Symbolic/CrucGen.hs
+++ b/symbolic/src/Data/Macaw/Symbolic/CrucGen.hs
@@ -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
diff --git a/symbolic/src/Data/Macaw/Symbolic/PersistentState.hs b/symbolic/src/Data/Macaw/Symbolic/PersistentState.hs
index f0b451b5..b553be3f 100644
--- a/symbolic/src/Data/Macaw/Symbolic/PersistentState.hs
+++ b/symbolic/src/Data/Macaw/Symbolic/PersistentState.hs
@@ -31,6 +31,7 @@ module Data.Macaw.Symbolic.PersistentState
   , floatInfoToCrucible
   , floatInfoFromCrucible
   , typeCtxToCrucible
+  , typeListToCrucible
   , macawAssignToCrucM
   , memReprToCrucible
     -- * Register index map
diff --git a/x86_symbolic/src/Data/Macaw/X86/Crucible.hs b/x86_symbolic/src/Data/Macaw/X86/Crucible.hs
index b851dd83..55d3a000 100644
--- a/x86_symbolic/src/Data/Macaw/X86/Crucible.hs
+++ b/x86_symbolic/src/Data/Macaw/X86/Crucible.hs
@@ -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 ->