Merge pull request #13 from GaloisInc/floating-point

Add support for floating-point.
2024-12-28 08:34:23 +03:00 · 2018-09-06 14:05:23 -07:00 · 2018-09-06 14:05:23 -07:00 · bd906c85a9
commit bd906c85a9
parent e2f25b8ce1 786a45c5e0
8 changed files with 201 additions and 150 deletions
--- a/base/macaw-base.cabal
+++ b/base/macaw-base.cabal
@ -40,6 +40,7 @@ library
    lens >= 4.7,
    mtl,
    parameterized-utils >= 1.0.1,
+    template-haskell,
    text,
    vector,
    QuickCheck >= 2.7
--- a/base/src/Data/Macaw/Types.hs
+++ b/base/src/Data/Macaw/Types.hs
@ -6,15 +6,20 @@ The type of machine words, including bit vectors and floating point
 -}
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DeriveLift #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FunctionalDependencies #-}
-{-# LANGUAGE KindSignatures #-}
-{-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE GADTs #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE PatternGuards #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE TypeSynonymInstances #-}
 {-# LANGUAGE UndecidableInstances #-}
 module Data.Macaw.Types
@ -27,8 +32,10 @@ module Data.Macaw.Types
 import           Data.Parameterized.Classes
 import qualified Data.Parameterized.List as P
 import           Data.Parameterized.NatRepr
+import           Data.Parameterized.TH.GADT
 import           Data.Parameterized.TraversableFC
 import           GHC.TypeLits
+import qualified Language.Haskell.TH.Syntax as TH
 import           Text.PrettyPrint.ANSI.Leijen hiding ((<$>))

 -- FIXME: move
@ -68,16 +75,8 @@ n256 = knownNat
 data Type
  = -- | A bitvector with the given number of bits.
    BVType Nat
-    -- | 64 bit binary IEE754
-  | DoubleFloat
-    -- | 32 bit binary IEE754
-  | SingleFloat
-    -- | X86 80-bit extended floats
-  | X86_80Float
-    -- | 128 bit binary IEE754
-  | QuadFloat
-    -- | 16 bit binary IEE754
-  | HalfFloat
+    -- | A floating point in the given format.
+  | FloatType FloatInfo
    -- | A Boolean value
  | BoolType
    -- | A tuple of types
@ -86,29 +85,21 @@ data Type

 -- Return number of bytes in the type.
 type family TypeBytes (tp :: Type) :: Nat where
-  TypeBytes (BVType  8) =  1
-  TypeBytes (BVType 16) =  2
-  TypeBytes (BVType 32) =  4
-  TypeBytes (BVType 64) =  8
-  TypeBytes HalfFloat   =  2
-  TypeBytes SingleFloat =  4
-  TypeBytes DoubleFloat =  8
-  TypeBytes QuadFloat   = 16
-  TypeBytes X86_80Float = 10
+  TypeBytes (BVType  8) = 1
+  TypeBytes (BVType 16) = 2
+  TypeBytes (BVType 32) = 4
+  TypeBytes (BVType 64) = 8
+  TypeBytes (FloatType fi) = FloatInfoBytes fi

 -- Return number of bits in the type.
 type family TypeBits (tp :: Type) :: Nat where
-  TypeBits (BVType n)  = n
-  TypeBits HalfFloat   = 16
-  TypeBits SingleFloat = 32
-  TypeBits DoubleFloat = 64
-  TypeBits QuadFloat   = 128
-  TypeBits X86_80Float = 80
-
-type FloatType tp = BVType (8 * TypeBytes tp)
+  TypeBits (BVType n) = n
+  TypeBits (FloatType fi) = 8 * FloatInfoBytes fi

 type BVType = 'BVType

+type FloatType = 'FloatType
+
 type BoolType = 'BoolType

 type TupleType = 'TupleType
@ -117,33 +108,16 @@ type TupleType = 'TupleType
 data TypeRepr (tp :: Type) where
  BoolTypeRepr :: TypeRepr BoolType
  BVTypeRepr :: (1 <= n) => !(NatRepr n) -> TypeRepr (BVType n)
+  FloatTypeRepr :: !(FloatInfoRepr fi) -> TypeRepr (FloatType fi)
  TupleTypeRepr :: !(P.List TypeRepr ctx) -> TypeRepr (TupleType ctx)

 type_width :: TypeRepr (BVType n) -> NatRepr n
 type_width (BVTypeRepr n) = n

-instance TestEquality TypeRepr where
-  testEquality BoolTypeRepr BoolTypeRepr = do
-    return Refl
-  testEquality (BVTypeRepr m) (BVTypeRepr n) = do
-    Refl <- testEquality m n
-    return Refl
-  testEquality _ _ = Nothing
-
-instance OrdF TypeRepr where
-  compareF BoolTypeRepr BoolTypeRepr = EQF
-  compareF BoolTypeRepr _ = LTF
-  compareF _ BoolTypeRepr = GTF
-  compareF (BVTypeRepr m) (BVTypeRepr n) = do
-    lexCompareF m n EQF
-  compareF BVTypeRepr{} _ = LTF
-  compareF _ BVTypeRepr{} = GTF
-  compareF (TupleTypeRepr x) (TupleTypeRepr y) =
-    lexCompareF x y EQF
-
 instance Show (TypeRepr tp) where
  show BoolTypeRepr = "bool"
  show (BVTypeRepr w) = "[" ++ show w ++ "]"
+  show (FloatTypeRepr fi) = show fi ++ "_float"
  show (TupleTypeRepr P.Nil) = "()"
  show (TupleTypeRepr (h P.:< z)) =
    "(" ++ show h ++ foldrFC (\tp r -> "," ++ show tp ++ r) ")" z
@ -154,96 +128,123 @@ instance KnownRepr TypeRepr BoolType where
 instance (KnownNat n, 1 <= n) => KnownRepr TypeRepr (BVType n) where
  knownRepr = BVTypeRepr knownNat

+instance (KnownRepr FloatInfoRepr fi) => KnownRepr TypeRepr (FloatType fi) where
+  knownRepr = FloatTypeRepr knownRepr
+
 instance (KnownRepr (P.List TypeRepr) l) => KnownRepr TypeRepr  (TupleType l) where
  knownRepr = TupleTypeRepr knownRepr

 ------------------------------------------------------------------------
 -- Floating point sizes

+data FloatInfo
+  = HalfFloat   -- ^ 16 bit binary IEE754
+  | SingleFloat -- ^ 32 bit binary IEE754
+  | DoubleFloat -- ^ 64 bit binary IEE754
+  | QuadFloat   -- ^ 128 bit binary IEE754
+  | X86_80Float -- ^ X86 80-bit extended floats
+
+type HalfFloat   = 'HalfFloat
 type SingleFloat = 'SingleFloat
 type DoubleFloat = 'DoubleFloat
-type X86_80Float = 'X86_80Float
 type QuadFloat   = 'QuadFloat
-type HalfFloat   = 'HalfFloat
+type X86_80Float = 'X86_80Float

-data FloatInfoRepr (flt::Type) where
-  DoubleFloatRepr :: FloatInfoRepr DoubleFloat
-  SingleFloatRepr :: FloatInfoRepr SingleFloat
-  X86_80FloatRepr :: FloatInfoRepr X86_80Float
-  QuadFloatRepr   :: FloatInfoRepr QuadFloat
+data FloatInfoRepr (fi :: FloatInfo) where
  HalfFloatRepr   :: FloatInfoRepr HalfFloat
+  SingleFloatRepr :: FloatInfoRepr SingleFloat
+  DoubleFloatRepr :: FloatInfoRepr DoubleFloat
+  QuadFloatRepr   :: FloatInfoRepr QuadFloat
+  X86_80FloatRepr :: FloatInfoRepr X86_80Float

-deriving instance Show (FloatInfoRepr tp)
+instance KnownRepr FloatInfoRepr HalfFloat where
+  knownRepr = HalfFloatRepr
+instance KnownRepr FloatInfoRepr SingleFloat where
+  knownRepr = SingleFloatRepr
+instance KnownRepr FloatInfoRepr DoubleFloat where
+  knownRepr = DoubleFloatRepr
+instance KnownRepr FloatInfoRepr QuadFloat where
+  knownRepr = QuadFloatRepr
+instance KnownRepr FloatInfoRepr X86_80Float where
+  knownRepr = X86_80FloatRepr
+
+instance Show (FloatInfoRepr fi) where
+  show HalfFloatRepr   = "half"
+  show SingleFloatRepr = "single"
+  show DoubleFloatRepr = "double"
+  show QuadFloatRepr   = "quad"
+  show X86_80FloatRepr = "x87_80"
+
+instance Pretty (FloatInfoRepr fi) where
+  pretty = text . show
+
+deriving instance TH.Lift (FloatInfoRepr fi)
+
+type family FloatInfoBytes (fi :: FloatInfo) :: Nat where
+  FloatInfoBytes HalfFloat   = 2
+  FloatInfoBytes SingleFloat = 4
+  FloatInfoBytes DoubleFloat = 8
+  FloatInfoBytes QuadFloat   = 16
+  FloatInfoBytes X86_80Float = 10
+
+floatInfoBytes :: FloatInfoRepr fi -> NatRepr (FloatInfoBytes fi)
+floatInfoBytes = \case
+  HalfFloatRepr   -> knownNat
+  SingleFloatRepr -> knownNat
+  DoubleFloatRepr -> knownNat
+  QuadFloatRepr   -> knownNat
+  X86_80FloatRepr -> knownNat
+
+floatInfoBytesIsPos :: FloatInfoRepr fi -> LeqProof 1 (FloatInfoBytes fi)
+floatInfoBytesIsPos = \case
+  HalfFloatRepr   -> LeqProof
+  SingleFloatRepr -> LeqProof
+  DoubleFloatRepr -> LeqProof
+  QuadFloatRepr   -> LeqProof
+  X86_80FloatRepr -> LeqProof
+
+type FloatInfoBits (fi :: FloatInfo) = 8 * FloatInfoBytes fi
+
+floatInfoBits :: FloatInfoRepr fi -> NatRepr (FloatInfoBits fi)
+floatInfoBits = natMultiply (knownNat @8) . floatInfoBytes
+
+floatInfoBitsIsPos :: FloatInfoRepr fi -> LeqProof 1 (FloatInfoBits fi)
+floatInfoBitsIsPos = \case
+  HalfFloatRepr   -> LeqProof
+  SingleFloatRepr -> LeqProof
+  DoubleFloatRepr -> LeqProof
+  QuadFloatRepr   -> LeqProof
+  X86_80FloatRepr -> LeqProof
+
+-- | The bitvector associted with the given floating-point format.
+type FloatBVType (fi :: FloatInfo) = BVType (FloatInfoBits fi)
+
+floatBVTypeRepr :: FloatInfoRepr fi -> TypeRepr (FloatBVType fi)
+floatBVTypeRepr fi | LeqProof <- floatInfoBitsIsPos fi =
+  BVTypeRepr $ floatInfoBits fi
+
+$(return [])
+
+instance TestEquality TypeRepr where
+  testEquality = $(structuralTypeEquality [t|TypeRepr|]
+    [ (ConType [t|NatRepr|] `TypeApp` AnyType, [|testEquality|])
+    , (ConType [t|FloatInfoRepr|] `TypeApp` AnyType, [|testEquality|])
+    , ( ConType [t|P.List|] `TypeApp` AnyType `TypeApp` AnyType
+      , [|testEquality|]
+      )
+    ])
+
+instance OrdF TypeRepr where
+  compareF = $(structuralTypeOrd [t|TypeRepr|]
+    [ (ConType [t|NatRepr|] `TypeApp` AnyType, [|compareF|])
+    , (ConType [t|FloatInfoRepr|] `TypeApp` AnyType, [|compareF|])
+    , (ConType [t|P.List|] `TypeApp` AnyType `TypeApp` AnyType, [|compareF|])
+    ])

 instance TestEquality FloatInfoRepr where
-  testEquality x y = orderingF_refl (compareF x y)
-
+  testEquality = $(structuralTypeEquality [t|FloatInfoRepr|] [])
 instance OrdF FloatInfoRepr where
-  compareF DoubleFloatRepr DoubleFloatRepr = EQF
-  compareF DoubleFloatRepr _               = LTF
-  compareF _               DoubleFloatRepr = GTF
-
-  compareF SingleFloatRepr SingleFloatRepr = EQF
-  compareF SingleFloatRepr _               = LTF
-  compareF _               SingleFloatRepr = GTF
-
-  compareF X86_80FloatRepr X86_80FloatRepr = EQF
-  compareF X86_80FloatRepr _               = LTF
-  compareF _               X86_80FloatRepr = GTF
-
-  compareF QuadFloatRepr   QuadFloatRepr   = EQF
-  compareF QuadFloatRepr   _               = LTF
-  compareF _               QuadFloatRepr   = GTF
-
-  compareF HalfFloatRepr   HalfFloatRepr   = EQF
-
-instance Pretty (FloatInfoRepr flt) where
-  pretty DoubleFloatRepr = text "double"
-  pretty SingleFloatRepr = text "single"
-  pretty X86_80FloatRepr = text "x87_80"
-  pretty QuadFloatRepr   = text "quad"
-  pretty HalfFloatRepr   = text "half"
-
-
-floatInfoBytes :: FloatInfoRepr flt -> NatRepr (TypeBytes flt)
-floatInfoBytes fir =
-  case fir of
-    HalfFloatRepr         -> knownNat
-    SingleFloatRepr       -> knownNat
-    DoubleFloatRepr       -> knownNat
-    QuadFloatRepr         -> knownNat
-    X86_80FloatRepr       -> knownNat
-
-floatInfoBytesIsPos :: FloatInfoRepr flt -> LeqProof 1 (TypeBytes flt)
-floatInfoBytesIsPos fir =
-  case fir of
-    HalfFloatRepr         -> LeqProof
-    SingleFloatRepr       -> LeqProof
-    DoubleFloatRepr       -> LeqProof
-    QuadFloatRepr         -> LeqProof
-    X86_80FloatRepr       -> LeqProof
-
-
-floatInfoBits :: FloatInfoRepr flt -> NatRepr (8 * TypeBytes flt)
-floatInfoBits fir = natMultiply (knownNat :: NatRepr 8) (floatInfoBytes fir)
-
-floatTypeRepr :: FloatInfoRepr flt -> TypeRepr (BVType (8 * TypeBytes flt))
-floatTypeRepr fir =
-  case fir of
-    HalfFloatRepr         -> knownRepr
-    SingleFloatRepr       -> knownRepr
-    DoubleFloatRepr       -> knownRepr
-    QuadFloatRepr         -> knownRepr
-    X86_80FloatRepr       -> knownRepr
-
-floatInfoBitsIsPos :: FloatInfoRepr flt -> LeqProof 1 (8 * TypeBytes flt)
-floatInfoBitsIsPos fir =
-  case fir of
-    HalfFloatRepr         -> LeqProof
-    SingleFloatRepr       -> LeqProof
-    DoubleFloatRepr       -> LeqProof
-    QuadFloatRepr         -> LeqProof
-    X86_80FloatRepr       -> LeqProof
+  compareF = $(structuralTypeOrd [t|FloatInfoRepr|] [])

 ------------------------------------------------------------------------
 --
--- a/symbolic/src/Data/Macaw/Symbolic.hs
+++ b/symbolic/src/Data/Macaw/Symbolic.hs
@ -26,6 +26,8 @@ module Data.Macaw.Symbolic
  , mkFunCFG
  , Data.Macaw.Symbolic.PersistentState.ArchRegContext
  , Data.Macaw.Symbolic.PersistentState.ToCrucibleType
+  , Data.Macaw.Symbolic.PersistentState.ToCrucibleFloatInfo
+  , Data.Macaw.Symbolic.PersistentState.floatInfoToCrucible
  , Data.Macaw.Symbolic.PersistentState.macawAssignToCrucM
  , Data.Macaw.Symbolic.CrucGen.ArchRegStruct
  , Data.Macaw.Symbolic.CrucGen.MacawCrucibleRegTypes
@ -52,6 +54,7 @@ import           Data.Parameterized.Context as Ctx
 import           Data.Word

 import qualified What4.FunctionName as C
+import           What4.InterpretedFloatingPoint
 import           What4.Interface
 import qualified What4.ProgramLoc as C
 import           What4.Symbol (userSymbol)
@ -459,6 +462,10 @@ freshValue sym str w ty =
             offs <- freshConstant sym nm (C.BaseBVRepr y)
             return (MM.LLVMPointer base offs)

+    M.FloatTypeRepr fi -> do
+      nm <- symName str
+      freshFloatConstant sym nm $ floatInfoToCrucible fi
+
    M.BoolTypeRepr ->
      do nm <- symName str
         freshConstant sym nm C.BaseBoolRepr
--- a/symbolic/src/Data/Macaw/Symbolic/CrucGen.hs
+++ b/symbolic/src/Data/Macaw/Symbolic/CrucGen.hs
@ -655,6 +655,7 @@ appToCrucible app = do
                  Just Refl -> evalMacawStmt (PtrEq rW xv yv)
                  Nothing ->
                    appAtom =<< C.BVEq n <$> toBits n xv <*> toBits n yv
+           M.FloatTypeRepr _ -> appAtom $ C.FloatEq xv yv
           M.TupleTypeRepr _ -> fail "XXX: Equality on tuples not yet done."


@ -670,6 +671,8 @@ appToCrucible app = do
                  Just Refl -> evalMacawStmt (PtrMux rW cond tv fv)
                  Nothing -> appBVAtom n =<<
                                C.BVIte cond n <$> toBits n tv <*> toBits n fv
+           M.FloatTypeRepr fi ->
+             appAtom $ C.FloatIte (floatInfoToCrucible fi) cond tv fv
           M.TupleTypeRepr _ -> fail "XXX: Mux on tuples not yet done."


--- a/symbolic/src/Data/Macaw/Symbolic/PersistentState.hs
+++ b/symbolic/src/Data/Macaw/Symbolic/PersistentState.hs
@ -8,6 +8,7 @@ This defines the monad used to map Reopt blocks to Crucible.
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE GADTs #-}
+{-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE PolyKinds #-}
@ -22,9 +23,13 @@ module Data.Macaw.Symbolic.PersistentState
  , initCrucPersistentState
    -- * Types
  , ToCrucibleType
+  , ToCrucibleFloatInfo
+  , FromCrucibleFloatInfo
  , CtxToCrucibleType
  , ArchRegContext
  , typeToCrucible
+  , floatInfoToCrucible
+  , floatInfoFromCrucible
  , typeCtxToCrucible
  , macawAssignToCrucM
  , memReprToCrucible
@ -59,9 +64,23 @@ type family ToCrucibleTypeList (l :: [M.Type]) :: Ctx C.CrucibleType where

 type family ToCrucibleType (tp :: M.Type) :: C.CrucibleType where
  ToCrucibleType (M.BVType w)     = MM.LLVMPointerType w
+  ToCrucibleType (M.FloatType fi) = C.FloatType (ToCrucibleFloatInfo fi)
  ToCrucibleType ('M.TupleType l) = C.StructType (ToCrucibleTypeList l)
  ToCrucibleType M.BoolType       = C.BaseToType C.BaseBoolType

+type family ToCrucibleFloatInfo (fi :: M.FloatInfo) :: C.FloatInfo where
+  ToCrucibleFloatInfo M.HalfFloat   = C.HalfFloat
+  ToCrucibleFloatInfo M.SingleFloat = C.SingleFloat
+  ToCrucibleFloatInfo M.DoubleFloat = C.DoubleFloat
+  ToCrucibleFloatInfo M.QuadFloat   = C.QuadFloat
+  ToCrucibleFloatInfo M.X86_80Float = C.X86_80Float
+
+type family FromCrucibleFloatInfo (fi :: C.FloatInfo) :: M.FloatInfo where
+  FromCrucibleFloatInfo C.HalfFloat   = M.HalfFloat
+  FromCrucibleFloatInfo C.SingleFloat = M.SingleFloat
+  FromCrucibleFloatInfo C.DoubleFloat = M.DoubleFloat
+  FromCrucibleFloatInfo C.QuadFloat   = M.QuadFloat
+  FromCrucibleFloatInfo C.X86_80Float = M.X86_80Float

 type family CtxToCrucibleType (mtp :: Ctx M.Type) :: Ctx C.CrucibleType where
  CtxToCrucibleType EmptyCtx   = EmptyCtx
@ -92,8 +111,29 @@ typeToCrucible tp =
  case tp of
    M.BoolTypeRepr  -> C.BoolRepr
    M.BVTypeRepr w  -> MM.LLVMPointerRepr w
+    M.FloatTypeRepr fi -> C.FloatRepr $ floatInfoToCrucible fi
    M.TupleTypeRepr a -> C.StructRepr (typeListToCrucible a)

+floatInfoToCrucible
+  :: M.FloatInfoRepr fi -> C.FloatInfoRepr (ToCrucibleFloatInfo fi)
+floatInfoToCrucible = \case
+  M.HalfFloatRepr   -> knownRepr
+  M.SingleFloatRepr -> knownRepr
+  M.DoubleFloatRepr -> knownRepr
+  M.QuadFloatRepr   -> knownRepr
+  M.X86_80FloatRepr -> knownRepr
+
+floatInfoFromCrucible
+  :: C.FloatInfoRepr fi -> M.FloatInfoRepr (FromCrucibleFloatInfo fi)
+floatInfoFromCrucible = \case
+  C.HalfFloatRepr   -> knownRepr
+  C.SingleFloatRepr -> knownRepr
+  C.DoubleFloatRepr -> knownRepr
+  C.QuadFloatRepr   -> knownRepr
+  C.X86_80FloatRepr -> knownRepr
+  fi ->
+    error $ "Unsupported Crucible floating-point format in Macaw: " ++ show fi
+
 typeListToCrucible ::
    P.List M.TypeRepr ctx ->
    Assignment C.TypeRepr (ToCrucibleTypeList ctx)
--- a/x86/src/Data/Macaw/X86/ArchTypes.hs
+++ b/x86/src/Data/Macaw/X86/ArchTypes.hs
@ -210,8 +210,8 @@ sseOpName f =

 -- | A single or double value for floating-point restricted to this types.
 data SSE_FloatType tp where
-   SSE_Single :: SSE_FloatType (FloatType SingleFloat)
-   SSE_Double :: SSE_FloatType (FloatType DoubleFloat)
+   SSE_Single :: SSE_FloatType (FloatBVType SingleFloat)
+   SSE_Double :: SSE_FloatType (FloatBVType DoubleFloat)

 instance Show (SSE_FloatType tp) where
  show SSE_Single = "single"
@ -225,9 +225,9 @@ instance HasRepr SSE_FloatType TypeRepr where
 -- X87 declarations

 data X87_FloatType tp where
-   X87_Single :: X87_FloatType (BVType 32)
-   X87_Double :: X87_FloatType (BVType 64)
-   X87_ExtDouble :: X87_FloatType (BVType 80)
+   X87_Single :: X87_FloatType (FloatBVType SingleFloat)
+   X87_Double :: X87_FloatType (FloatBVType DoubleFloat)
+   X87_ExtDouble :: X87_FloatType (FloatBVType X86_80Float)

 instance Show (X87_FloatType tp) where
  show X87_Single = "single"
@ -513,7 +513,7 @@ data X86PrimFn f tp where
  -- Guaranteed to not throw exception or have side effects.
  X87_Extend :: !(SSE_FloatType tp)
             -> !(f tp)
-             -> X86PrimFn f (BVType 80)
+             -> X86PrimFn f (FloatBVType X86_80Float)

  -- | This performs an 80-bit floating point add.
  --
@ -529,9 +529,9 @@ data X86PrimFn f tp where
  -- * @#U@ Result is too small for destination format.
  -- * @#O@ Result is too large for destination format.
  -- * @#P@ Value cannot be represented exactly in destination format.
-  X87_FAdd :: !(f (FloatType X86_80Float))
-           -> !(f (FloatType X86_80Float))
-           -> X86PrimFn f (TupleType [FloatType X86_80Float, BoolType])
+  X87_FAdd :: !(f (FloatBVType X86_80Float))
+           -> !(f (FloatBVType X86_80Float))
+           -> X86PrimFn f (TupleType [FloatBVType X86_80Float, BoolType])

  -- | This performs an 80-bit floating point subtraction.
  --
@ -547,9 +547,9 @@ data X86PrimFn f tp where
  -- * @#U@ Result is too small for destination format.
  -- * @#O@ Result is too large for destination format.
  -- * @#P@ Value cannot be represented exactly in destination format.
-  X87_FSub :: !(f (FloatType X86_80Float))
-           -> !(f (FloatType X86_80Float))
-           -> X86PrimFn f (TupleType [FloatType X86_80Float, BoolType])
+  X87_FSub :: !(f (FloatBVType X86_80Float))
+           -> !(f (FloatBVType X86_80Float))
+           -> X86PrimFn f (TupleType [FloatBVType X86_80Float, BoolType])

  -- | This performs an 80-bit floating point multiply.
  --
@ -565,9 +565,9 @@ data X86PrimFn f tp where
  -- * @#U@ Result is too small for destination format.
  -- * @#O@ Result is too large for destination format.
  -- * @#P@ Value cannot be represented exactly in destination format.
-  X87_FMul :: !(f (FloatType X86_80Float))
-           -> !(f (FloatType X86_80Float))
-           -> X86PrimFn f (TupleType [FloatType X86_80Float, BoolType])
+  X87_FMul :: !(f (FloatBVType X86_80Float))
+           -> !(f (FloatBVType X86_80Float))
+           -> X86PrimFn f (TupleType [FloatBVType X86_80Float, BoolType])

  -- | This rounds a floating number to single or double precision.
  --
@ -583,7 +583,7 @@ data X86PrimFn f tp where
  --   In the #P case, the C1 register will be set 1 if rounding up,
  --   and 0 otherwise.
  X87_FST :: !(SSE_FloatType tp)
-          -> !(f (BVType 80))
+          -> !(f (FloatBVType X86_80Float))
          -> X86PrimFn f tp

  -- | Unary operation on a vector.  Should have no side effects.
--- a/x86/src/Data/Macaw/X86/Monad.hs
+++ b/x86/src/Data/Macaw/X86/Monad.hs
@ -519,7 +519,7 @@ data Location addr (tp :: Type) where
  -- top, so X87Register 0 is the top, X87Register 1 is the second,
  -- and so forth.
  X87StackRegister :: !Int
-                   -> Location addr (FloatType X86_80Float)
+                   -> Location addr (FloatBVType X86_80Float)

 ------------------------------------------------------------------------
 -- Location
@ -743,14 +743,13 @@ c2_loc = fullRegister R.X87_C2
 c3_loc = fullRegister R.X87_C3

 -- | Maps float info repr to associated MemRepr.
-floatMemRepr :: FloatInfoRepr flt -> MemRepr (FloatType flt)
-floatMemRepr fir =
-  case floatInfoBytesIsPos fir of
-    LeqProof -> BVMemRepr (floatInfoBytes fir) LittleEndian
+floatMemRepr :: FloatInfoRepr fi -> MemRepr (FloatBVType fi)
+floatMemRepr fi | LeqProof <- floatInfoBytesIsPos fi =
+  BVMemRepr (floatInfoBytes fi) LittleEndian

 -- | Tuen an address into a location of size @n
-mkFPAddr :: FloatInfoRepr flt -> addr -> Location addr (FloatType flt)
-mkFPAddr fir addr = MemoryAddr addr (floatMemRepr fir)
+mkFPAddr :: FloatInfoRepr fi -> addr -> Location addr (FloatBVType fi)
+mkFPAddr fi addr = MemoryAddr addr (floatMemRepr fi)

 -- | Return MMX register corresponding to x87 register.
 --
@ -1629,7 +1628,7 @@ getSegmentBase seg =

 -- | X87 support --- these both affect the register stack for the
 -- x87 state.
-x87Push :: Expr ids (FloatType X86_80Float) -> X86Generator st ids ()
+x87Push :: Expr ids (FloatBVType X86_80Float) -> X86Generator st ids ()
 x87Push e = do
  v <- eval e
  topv <- getX87Top
--- a/x86/src/Data/Macaw/X86/Semantics.hs
+++ b/x86/src/Data/Macaw/X86/Semantics.hs
@ -1549,9 +1549,9 @@ def_fstX mnem doPop = defUnary mnem $ \_ val -> do

 type X87BinOp
   = forall f
-   . f (FloatType X86_80Float)
-   -> f (FloatType X86_80Float)
-   -> X86PrimFn f (TupleType [FloatType X86_80Float, BoolType])
+   . f (FloatBVType X86_80Float)
+   -> f (FloatBVType X86_80Float)
+   -> X86PrimFn f (TupleType [FloatBVType X86_80Float, BoolType])

 execX87BinOp :: X87BinOp
             -> Location (Addr ids) (BVType 80)