Handle conversions for Float Mux in macaw-ppc.

macaw-ppc/macaw-ppc.cabal

@@ -39,6 +39,7 @@ library
                        semmc,
                        semmc-ppc,
                        macaw-semmc,
+                       macaw-symbolic,
                        macaw-loader,
                        macaw-loader-ppc,
                        lens,

macaw-ppc/src/Data/Macaw/PPC/Semantics/Base.hs

@@ -9,9 +9,10 @@
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
-{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE UndecidableInstances #-}
 
 module Data.Macaw.PPC.Semantics.Base
   ( crucAppToExpr
@@ -28,12 +29,14 @@ import qualified What4.BaseTypes as S
 import qualified What4.Expr.BoolMap as BooM
 import qualified What4.Expr.Builder as S
 import qualified What4.Expr.WeightedSum as WSum
+import qualified What4.InterpretedFloatingPoint as SFP
 import qualified What4.SemiRing as SR
 
 import qualified SemMC.Architecture.PPC as SP
 import qualified SemMC.Architecture.PPC.Location as APPC
 import qualified Data.Macaw.CFG as M
 import qualified Data.Macaw.Types as M
+import qualified Data.Macaw.Symbolic as MS
 
 import Data.Parameterized.NatRepr ( knownNat
                                   , addNat
@@ -48,6 +51,8 @@ import           Data.Macaw.PPC.PPCReg
 type family FromCrucibleBaseType (btp :: S.BaseType) :: M.Type where
   FromCrucibleBaseType (S.BaseBVType w) = M.BVType w
   FromCrucibleBaseType (S.BaseBoolType) = M.BoolType
+  FromCrucibleBaseType (S.BaseFloatType fpp) =
+    M.FloatType (MS.FromCrucibleFloatInfo (SFP.FloatPrecisionToInfo fpp))
 
 crucAppToExpr :: (M.ArchConstraints ppc) =>
                  S.App (S.Expr t) ctp
@@ -61,10 +66,10 @@ crucAppToExpr (S.BaseIte bt _ test t f) = AppExpr <$>
       M.Mux <$> pure M.BoolTypeRepr <*> addElt test <*> addElt t <*> addElt f
     S.BaseBVRepr w ->
       M.Mux <$> pure (M.BVTypeRepr w) <*> addElt test <*> addElt t <*> addElt f
-    -- S.BaseFloatRepr fpp ->
+    S.BaseFloatRepr fpp ->
-      -- M.Mux
+      M.Mux
-      -- <$> pure (M.FloatTypeRepr (floatInfoFromPrecision fpp))
+      (M.FloatTypeRepr (MS.floatInfoFromCrucible $ SFP.floatPrecisionToInfoRepr fpp))
-      -- <*> addElt test <*> addElt t <*> addElt f
+      <$> addElt test <*> addElt t <*> addElt f
     _ -> error "unsupported BaseITE repr for macaw PPC base semantics"
 crucAppToExpr (S.BaseEq _bt bv1 bv2) =
   AppExpr <$> do M.Eq <$> addElt bv1 <*> addElt bv2

symbolic/src/Data/Macaw/Symbolic.hs

@@ -20,7 +20,7 @@
 -- library.  There are two main portions of the API:
 --
 -- 1. Translation of Macaw IR into Crucible CFGs
--- 2. Symbolic execution of Crucible CFGs generated from MAcaw
+-- 2. Symbolic execution of Crucible CFGs generated from Macaw
 --
 -- There are examples of each use case in the relevant sections of the haddocks.
 --
@@ -41,6 +41,7 @@
 --   do not necessarily hold for all machine code programs, but that do hold for
 --   (correct) C and C++ programs.  The current state of memory is held in a
 --   Crucible global value that is modified by all code.
+--
 -- * Each function takes a single argument (the full set of machine registers)
 --   and returns a single value (the full set of machine registers reflecting
 --   any modifications)
@@ -77,6 +78,7 @@ module Data.Macaw.Symbolic
   , CG.crucArchRegTypes
   , PS.ToCrucibleType
   , PS.ToCrucibleFloatInfo
+  , PS.FromCrucibleFloatInfo
   , PS.floatInfoToCrucible
   , PS.floatInfoFromCrucible
   , PS.ArchRegContext