diff --git a/macaw-ppc/src/Data/Macaw/PPC/Arch.hs b/macaw-ppc/src/Data/Macaw/PPC/Arch.hs
index 2a957a38..ed92768b 100644
--- a/macaw-ppc/src/Data/Macaw/PPC/Arch.hs
+++ b/macaw-ppc/src/Data/Macaw/PPC/Arch.hs
@@ -5,6 +5,7 @@
 {-# LANGUAGE FlexibleInstances     #-}
 {-# LANGUAGE GADTs                 #-}
 {-# LANGUAGE KindSignatures        #-}
+{-# LANGUAGE LambdaCase            #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE RankNTypes            #-}
 {-# LANGUAGE ScopedTypeVariables   #-}
@@ -230,9 +231,121 @@ data PPCPrimFn ppc f tp where
        -> f (MT.BVType (MC.RegAddrWidth (MC.ArchReg ppc)))
        -> PPCPrimFn ppc f (MT.BVType (MC.RegAddrWidth (MC.ArchReg ppc)))
 
-  FPIsQNaN :: !(MT.FloatInfoRepr flt) -> !(f (MT.FloatType flt)) -> PPCPrimFn ppc f MT.BoolType
-  FPIsSNaN :: !(MT.FloatInfoRepr flt) -> !(f (MT.FloatType flt)) -> PPCPrimFn ppc f MT.BoolType
-  FPCvt :: !(MT.FloatInfoRepr flt) -> !(f (MT.FloatType flt)) -> !(MT.FloatInfoRepr flt') -> PPCPrimFn ppc f (MT.FloatType flt')
+  -- | Interpreted floating point functions.
+  FPNeg
+    :: !(MT.FloatInfoRepr fi)
+    -> !(f (MT.FloatType fi))
+    -> PPCPrimFn ppc f (MT.FloatType fi)
+  FPAbs
+    :: !(MT.FloatInfoRepr fi)
+    -> !(f (MT.FloatType fi))
+    -> PPCPrimFn ppc f (MT.FloatType fi)
+  FPSqrt
+    :: !(MT.FloatInfoRepr fi)
+    -> !(f (MT.FloatType fi))
+    -> PPCPrimFn ppc f (MT.FloatType fi)
+
+  FPAdd
+    :: !(MT.FloatInfoRepr fi)
+    -> !(f (MT.FloatType fi))
+    -> !(f (MT.FloatType fi))
+    -> PPCPrimFn ppc f (MT.FloatType fi)
+  FPSub
+    :: !(MT.FloatInfoRepr fi)
+    -> !(f (MT.FloatType fi))
+    -> !(f (MT.FloatType fi))
+    -> PPCPrimFn ppc f (MT.FloatType fi)
+  FPMul
+    :: !(MT.FloatInfoRepr fi)
+    -> !(f (MT.FloatType fi))
+    -> !(f (MT.FloatType fi))
+    -> PPCPrimFn ppc f (MT.FloatType fi)
+  FPDiv
+    :: !(MT.FloatInfoRepr fi)
+    -> !(f (MT.FloatType fi))
+    -> !(f (MT.FloatType fi))
+    -> PPCPrimFn ppc f (MT.FloatType fi)
+  FPFMA
+    :: !(MT.FloatInfoRepr fi)
+    -> !(f (MT.FloatType fi))
+    -> !(f (MT.FloatType fi))
+    -> !(f (MT.FloatType fi))
+    -> PPCPrimFn ppc f (MT.FloatType fi)
+
+  FPLt
+    :: !(f (MT.FloatType fi))
+    -> !(f (MT.FloatType fi))
+    -> PPCPrimFn ppc f MT.BoolType
+  FPEq
+    :: !(f (MT.FloatType fi))
+    -> !(f (MT.FloatType fi))
+    -> PPCPrimFn ppc f MT.BoolType
+
+  FPIsNaN :: !(f (MT.FloatType fi)) -> PPCPrimFn ppc f MT.BoolType
+
+  FPCast
+    :: !(MT.FloatInfoRepr fi)
+    -> !(f (MT.FloatType fi'))
+    -> PPCPrimFn ppc f (MT.FloatType fi)
+  -- | Treat a floating-point as a bitvector.
+  FPToBinary
+    :: (1 <= MT.FloatInfoBits fi)
+    => !(MT.FloatInfoRepr fi)
+    -> !(f (MT.FloatType fi))
+    -> PPCPrimFn ppc f (MT.FloatBVType fi)
+  -- | Treat a bitvector as a floating-point.
+  FPFromBinary
+    :: !(MT.FloatInfoRepr fi)
+    -> !(f (MT.FloatBVType fi))
+    -> PPCPrimFn ppc f (MT.FloatType fi)
+  FPToSBV
+    :: (1 <= w)
+    => !(MT.NatRepr w)
+    -> !(f (MT.FloatType fi))
+    -> PPCPrimFn ppc f (MT.BVType w)
+  FPToUBV
+    :: (1 <= w)
+    => !(MT.NatRepr w)
+    -> !(f (MT.FloatType fi))
+    -> PPCPrimFn ppc f (MT.BVType w)
+  FPFromSBV
+    :: (1 <= w)
+    => !(MT.FloatInfoRepr fi)
+    -> !(f (MT.BVType w))
+    -> PPCPrimFn ppc f (MT.FloatType fi)
+  FPFromUBV
+    :: (1 <= w)
+    => !(MT.FloatInfoRepr fi)
+    -> !(f (MT.BVType w))
+    -> PPCPrimFn ppc f (MT.FloatType fi)
+
+  -- | Coerce a floating-point to another precision format without
+  --   precision loss.
+  FPCoerce
+    :: !(MT.FloatInfoRepr fi)
+    -> !(MT.FloatInfoRepr fi')
+    -> !(f (MT.FloatType fi'))
+    -> PPCPrimFn ppc f (MT.FloatType fi)
+
+  -- | Uninterpreted floating point functions
+  FPSCR1
+    :: !String
+    -> !(f (MT.BVType 128))
+    -> !(f (MT.BVType 32))
+    -> PPCPrimFn ppc f (MT.BVType 32)
+  FPSCR2
+    :: !String
+    -> !(f (MT.BVType 128))
+    -> !(f (MT.BVType 128))
+    -> !(f (MT.BVType 32))
+    -> PPCPrimFn ppc f (MT.BVType 32)
+  FPSCR3
+    :: !String
+    -> !(f (MT.BVType 128))
+    -> !(f (MT.BVType 128))
+    -> !(f (MT.BVType 128))
+    -> !(f (MT.BVType 32))
+    -> PPCPrimFn ppc f (MT.BVType 32)
 
   -- | Uninterpreted floating point functions
   FP1 :: !String -- the name of the function
@@ -269,99 +382,176 @@ data PPCPrimFn ppc f tp where
        -> PPCPrimFn ppc f (MT.BVType 160)
 
 instance (1 <= MC.RegAddrWidth (MC.ArchReg ppc)) => MT.HasRepr (PPCPrimFn ppc v) MT.TypeRepr where
-  typeRepr f =
-    case f of
-      UDiv rep _ _ -> MT.BVTypeRepr rep
-      SDiv rep _ _ -> MT.BVTypeRepr rep
+  typeRepr = \case
+    UDiv rep _ _ -> MT.BVTypeRepr rep
+    SDiv rep _ _ -> MT.BVTypeRepr rep
 
-      FPIsQNaN _ _ -> MT.BoolTypeRepr
-      FPIsSNaN _ _ -> MT.BoolTypeRepr
-      FPCvt _ _ rep -> MT.floatTypeRepr rep
+    FPNeg  fi _    -> MT.FloatTypeRepr fi
+    FPAbs  fi _    -> MT.FloatTypeRepr fi
+    FPSqrt fi _    -> MT.FloatTypeRepr fi
+    FPAdd fi _ _   -> MT.FloatTypeRepr fi
+    FPSub fi _ _   -> MT.FloatTypeRepr fi
+    FPMul fi _ _   -> MT.FloatTypeRepr fi
+    FPDiv fi _ _   -> MT.FloatTypeRepr fi
+    FPFMA fi _ _ _ -> MT.FloatTypeRepr fi
+    FPLt{}    -> knownRepr
+    FPEq{}    -> knownRepr
+    FPIsNaN{} -> knownRepr
+    FPCast       fi _ -> MT.FloatTypeRepr fi
+    FPToBinary   fi _ -> MT.floatBVTypeRepr fi
+    FPFromBinary fi _ -> MT.FloatTypeRepr fi
+    FPToSBV      w  _ -> MT.BVTypeRepr w
+    FPToUBV      w  _ -> MT.BVTypeRepr w
+    FPFromSBV    fi _ -> MT.FloatTypeRepr fi
+    FPFromUBV    fi _ -> MT.FloatTypeRepr fi
+    FPCoerce fi _ _ -> MT.FloatTypeRepr fi
+    FPSCR1{} -> MT.BVTypeRepr MT.knownNat
+    FPSCR2{} -> MT.BVTypeRepr MT.knownNat
+    FPSCR3{} -> MT.BVTypeRepr MT.knownNat
 
-      FP1 _    _ _      -> MT.BVTypeRepr MT.knownNat
-      FP2 _    _ _ _    -> MT.BVTypeRepr MT.knownNat
-      FP3 _    _ _ _ _  -> MT.BVTypeRepr MT.knownNat
-
-      Vec1 _   _ _      -> MT.BVTypeRepr MT.knownNat
-      Vec2 _   _ _ _    -> MT.BVTypeRepr MT.knownNat
-      Vec3 _   _ _ _ _  -> MT.BVTypeRepr MT.knownNat
+    FP1{} -> MT.BVTypeRepr MT.knownNat
+    FP2{} -> MT.BVTypeRepr MT.knownNat
+    FP3{} -> MT.BVTypeRepr MT.knownNat
 
+    Vec1{} -> MT.BVTypeRepr MT.knownNat
+    Vec2{} -> MT.BVTypeRepr MT.knownNat
+    Vec3{} -> MT.BVTypeRepr MT.knownNat
 
 -- | Right now, none of the primitive functions has a side effect.  That will
 -- probably change.
 ppcPrimFnHasSideEffects :: PPCPrimFn ppc f tp -> Bool
-ppcPrimFnHasSideEffects pf =
-  case pf of
-    UDiv {} -> False
-    SDiv {} -> False
-    FPIsQNaN {} -> False
-    FPIsSNaN {} -> False
-    FPCvt {} -> False
-    FP1 {} -> False
-    FP2 {} -> False
-    FP3 {} -> False
-    Vec1 {} -> False
-    Vec2 {} -> False
-    Vec3 {} -> False
+ppcPrimFnHasSideEffects = \case
+  UDiv{}         -> False
+  SDiv{}         -> False
+  FPNeg{}        -> False
+  FPAbs{}        -> False
+  FPSqrt{}       -> False
+  FPAdd{}        -> False
+  FPSub{}        -> False
+  FPMul{}        -> False
+  FPDiv{}        -> False
+  FPFMA{}        -> False
+  FPLt{}         -> False
+  FPEq{}         -> False
+  FPIsNaN{}      -> False
+  FPCast{}       -> False
+  FPToBinary{}   -> False
+  FPFromBinary{} -> False
+  FPToSBV{}      -> False
+  FPToUBV{}      -> False
+  FPFromSBV{}    -> False
+  FPFromUBV{}    -> False
+  FPCoerce{}     -> False
+  FPSCR1{}       -> False
+  FPSCR2{}       -> False
+  FPSCR3{}       -> False
+  FP1{}          -> False
+  FP2{}          -> False
+  FP3{}          -> False
+  Vec1{}         -> False
+  Vec2{}         -> False
+  Vec3{}         -> False
 
 rewritePrimFn :: (PPCArchConstraints ppc, MC.ArchFn ppc ~ PPCPrimFn ppc)
               => PPCPrimFn ppc (MC.Value ppc src) tp
               -> Rewriter ppc s src tgt (MC.Value ppc tgt tp)
-rewritePrimFn f =
-  case f of
-    UDiv rep lhs rhs -> do
-      tgtFn <- UDiv rep <$> rewriteValue lhs <*> rewriteValue rhs
-      evalRewrittenArchFn tgtFn
-    SDiv rep lhs rhs -> do
-      tgtFn <- SDiv rep <$> rewriteValue lhs <*> rewriteValue rhs
-      evalRewrittenArchFn tgtFn
-    FPIsQNaN info v -> do
-      tgt <- FPIsQNaN info <$> rewriteValue v
-      evalRewrittenArchFn tgt
-    FPIsSNaN info v -> do
-      tgt <- FPIsSNaN info <$> rewriteValue v
-      evalRewrittenArchFn tgt
-    FPCvt rep1 v rep2 -> do
-      tgt <- FPCvt rep1 <$> rewriteValue v <*> pure rep2
-      evalRewrittenArchFn tgt
-    FP1 name op fpscr -> do
-      tgtFn <- FP1 name <$> rewriteValue op <*> rewriteValue fpscr
-      evalRewrittenArchFn tgtFn
-    FP2 name op1 op2 fpscr -> do
-      tgtFn <- FP2 name <$> rewriteValue op1 <*> rewriteValue op2 <*> rewriteValue fpscr
-      evalRewrittenArchFn tgtFn
-    FP3 name op1 op2 op3 fpscr -> do
-      tgtFn <- FP3 name <$> rewriteValue op1 <*> rewriteValue op2 <*> rewriteValue op3 <*> rewriteValue fpscr
-      evalRewrittenArchFn tgtFn
-    Vec1 name op vscr -> do
-      tgtFn <- Vec1 name <$> rewriteValue op <*> rewriteValue vscr
-      evalRewrittenArchFn tgtFn
-    Vec2 name op1 op2 vscr -> do
-      tgtFn <- Vec2 name <$> rewriteValue op1 <*> rewriteValue op2 <*> rewriteValue vscr
-      evalRewrittenArchFn tgtFn
-    Vec3 name op1 op2 op3 vscr -> do
-      tgtFn <- Vec3 name <$> rewriteValue op1 <*> rewriteValue op2 <*> rewriteValue op3 <*> rewriteValue vscr
-      evalRewrittenArchFn tgtFn
+rewritePrimFn = \case
+  UDiv rep lhs rhs -> do
+    tgtFn <- UDiv rep <$> rewriteValue lhs <*> rewriteValue rhs
+    evalRewrittenArchFn tgtFn
+  SDiv rep lhs rhs -> do
+    tgtFn <- SDiv rep <$> rewriteValue lhs <*> rewriteValue rhs
+    evalRewrittenArchFn tgtFn
+  FPNeg  fi x -> evalRewrittenArchFn =<< (FPNeg fi <$> rewriteValue x)
+  FPAbs  fi x -> evalRewrittenArchFn =<< (FPAbs fi <$> rewriteValue x)
+  FPSqrt fi x -> evalRewrittenArchFn =<< (FPSqrt fi <$> rewriteValue x)
+  FPAdd fi x y ->
+    evalRewrittenArchFn =<< (FPAdd fi <$> rewriteValue x <*> rewriteValue y)
+  FPSub fi x y ->
+    evalRewrittenArchFn =<< (FPSub fi <$> rewriteValue x <*> rewriteValue y)
+  FPMul fi x y ->
+    evalRewrittenArchFn =<< (FPMul fi <$> rewriteValue x <*> rewriteValue y)
+  FPDiv fi x y ->
+    evalRewrittenArchFn =<< (FPDiv fi <$> rewriteValue x <*> rewriteValue y)
+  FPFMA fi x y z ->
+    evalRewrittenArchFn
+      =<< (FPFMA fi <$> rewriteValue x <*> rewriteValue y <*> rewriteValue z)
+  FPLt x y ->
+    evalRewrittenArchFn =<< (FPLt <$> rewriteValue x <*> rewriteValue y)
+  FPEq x y ->
+    evalRewrittenArchFn =<< (FPEq <$> rewriteValue x <*> rewriteValue y)
+  FPIsNaN x -> evalRewrittenArchFn =<< (FPIsNaN <$> rewriteValue x)
+  FPCast fi x -> evalRewrittenArchFn =<< (FPCast fi <$> rewriteValue x)
+  FPToBinary fi x -> evalRewrittenArchFn =<< (FPToBinary fi <$> rewriteValue x)
+  FPFromBinary fi x ->
+    evalRewrittenArchFn =<< (FPFromBinary fi <$> rewriteValue x)
+  FPToSBV   w  x -> evalRewrittenArchFn =<< (FPToSBV w <$> rewriteValue x)
+  FPToUBV   w  x -> evalRewrittenArchFn =<< (FPToUBV w <$> rewriteValue x)
+  FPFromSBV fi x -> evalRewrittenArchFn =<< (FPFromSBV fi <$> rewriteValue x)
+  FPFromUBV fi x -> evalRewrittenArchFn =<< (FPFromUBV fi <$> rewriteValue x)
+  FPCoerce fi fi' x -> evalRewrittenArchFn =<< (FPCoerce fi fi' <$> rewriteValue x)
+  FPSCR1 name op fpscr ->
+    evalRewrittenArchFn =<< (FPSCR1 name <$> rewriteValue op <*> rewriteValue fpscr)
+  FPSCR2 name op1 op2 fpscr ->
+    evalRewrittenArchFn =<< (FPSCR2 name <$> rewriteValue op1 <*> rewriteValue op2 <*> rewriteValue fpscr)
+  FPSCR3 name op1 op2 op3 fpscr ->
+    evalRewrittenArchFn =<< (FPSCR3 name <$> rewriteValue op1 <*> rewriteValue op2 <*> rewriteValue op3 <*> rewriteValue fpscr)
+  FP1 name op fpscr -> do
+    tgtFn <- FP1 name <$> rewriteValue op <*> rewriteValue fpscr
+    evalRewrittenArchFn tgtFn
+  FP2 name op1 op2 fpscr -> do
+    tgtFn <- FP2 name <$> rewriteValue op1 <*> rewriteValue op2 <*> rewriteValue fpscr
+    evalRewrittenArchFn tgtFn
+  FP3 name op1 op2 op3 fpscr -> do
+    tgtFn <- FP3 name <$> rewriteValue op1 <*> rewriteValue op2 <*> rewriteValue op3 <*> rewriteValue fpscr
+    evalRewrittenArchFn tgtFn
+  Vec1 name op vscr -> do
+    tgtFn <- Vec1 name <$> rewriteValue op <*> rewriteValue vscr
+    evalRewrittenArchFn tgtFn
+  Vec2 name op1 op2 vscr -> do
+    tgtFn <- Vec2 name <$> rewriteValue op1 <*> rewriteValue op2 <*> rewriteValue vscr
+    evalRewrittenArchFn tgtFn
+  Vec3 name op1 op2 op3 vscr -> do
+    tgtFn <- Vec3 name <$> rewriteValue op1 <*> rewriteValue op2 <*> rewriteValue op3 <*> rewriteValue vscr
+    evalRewrittenArchFn tgtFn
 
 ppPrimFn :: (Applicative m) => (forall u . f u -> m PP.Doc) -> PPCPrimFn ppc f tp -> m PP.Doc
-ppPrimFn pp f =
-  case f of
-    UDiv _ lhs rhs -> ppBinary "ppc_udiv" <$> pp lhs <*> pp rhs
-    SDiv _ lhs rhs -> ppBinary "ppc_sdiv" <$> pp lhs <*> pp rhs
-    FPIsQNaN _info v -> ppUnary "ppc_fp_isqnan" <$> pp v
-    FPIsSNaN _info v -> ppUnary "ppc_fp_issnan" <$> pp v
-    FPCvt _rep1 v _rep2 -> ppUnary "ppc_fp_cvt" <$> pp v
-    FP1 n r1 fpscr -> ppBinary ("ppc_fp1 " ++ n) <$> pp r1 <*> pp fpscr
-    FP2 n r1 r2 fpscr -> pp3 ("ppc_fp2 " ++ n) <$> pp r1 <*> pp r2 <*> pp fpscr
-    FP3 n r1 r2 r3 fpscr -> pp4 ("ppc_fp3 " ++ n) <$> pp r1 <*> pp r2 <*> pp r3 <*> pp fpscr
-    Vec1 n r1 vscr -> ppBinary ("ppc_vec1 " ++ n) <$> pp r1 <*> pp vscr
-    Vec2 n r1 r2 vscr -> pp3 ("ppc_vec2" ++ n) <$> pp r1 <*> pp r2 <*> pp vscr
-    Vec3 n r1 r2 r3 vscr -> pp4 ("ppc_vec3" ++ n) <$> pp r1 <*> pp r2 <*> pp r3 <*> pp vscr
-  where
-    ppUnary s v' = PP.text s PP.<+> v'
-    ppBinary s v1' v2' = PP.text s PP.<+> v1' PP.<+> v2'
-    pp3 s v1' v2' v3' = PP.text s PP.<+> v1' PP.<+> v2' PP.<+> v3'
-    pp4 s v1' v2' v3' v4' = PP.text s PP.<+> v1' PP.<+> v2' PP.<+> v3' PP.<+> v4'
+ppPrimFn pp = \case
+  UDiv _ lhs rhs -> ppBinary "ppc_udiv" <$> pp lhs <*> pp rhs
+  SDiv _ lhs rhs -> ppBinary "ppc_sdiv" <$> pp lhs <*> pp rhs
+  FPNeg  _fi x -> ppUnary "ppc_fp_neg" <$> pp x
+  FPAbs  _fi x -> ppUnary "ppc_fp_abs" <$> pp x
+  FPSqrt _fi x -> ppUnary "ppc_fp_sqrt" <$> pp x
+  FPAdd _fi x y -> ppBinary "ppc_fp_add" <$> pp x <*> pp y
+  FPSub _fi x y -> ppBinary "ppc_fp_sub" <$> pp x <*> pp y
+  FPMul _fi x y -> ppBinary "ppc_fp_mul" <$> pp x <*> pp y
+  FPDiv _fi x y -> ppBinary "ppc_fp_div" <$> pp x <*> pp y
+  FPFMA _fi x y z -> pp3 "ppc_fp_fma" <$> pp x <*> pp y <*> pp z
+  FPLt x y -> ppBinary "ppc_fp_lt" <$> pp x <*> pp y
+  FPEq x y -> ppBinary "ppc_fp_eq" <$> pp x <*> pp y
+  FPIsNaN x -> ppUnary "ppc_fp_is_nan" <$> pp x
+  FPCast       _fi x -> ppUnary "ppc_fp_cast" <$> pp x
+  FPToBinary   _fi x -> ppUnary "ppc_fp_to_binary" <$> pp x
+  FPFromBinary _fi x -> ppUnary "ppc_fp_from_binary" <$> pp x
+  FPToSBV      _w  x -> ppUnary "ppc_fp_to_sbv" <$> pp x
+  FPToUBV      _w  x -> ppUnary "ppc_fp_to_ubv" <$> pp x
+  FPFromSBV    _fi x -> ppUnary "ppc_fp_from_sbv" <$> pp x
+  FPFromUBV    _fi x -> ppUnary "ppc_fp_from_ubv" <$> pp x
+  FPCoerce _fi _fi' x -> ppUnary "ppc_fp_coerce" <$> pp x
+  FPSCR1 n r1 fpscr -> ppBinary ("ppc_fp_un_op_fpscr " ++ n) <$> pp r1 <*> pp fpscr
+  FPSCR2 n r1 r2 fpscr -> pp3 ("ppc_fp_bin_op_fpscr " ++ n) <$> pp r1 <*> pp r2 <*> pp fpscr
+  FPSCR3 n r1 r2 r3 fpscr -> pp4 ("ppc_fp_tern_op_fpscr " ++ n) <$> pp r1 <*> pp r2 <*> pp r3 <*> pp fpscr
+  FP1 n r1 fpscr -> ppBinary ("ppc_fp1 " ++ n) <$> pp r1 <*> pp fpscr
+  FP2 n r1 r2 fpscr -> pp3 ("ppc_fp2 " ++ n) <$> pp r1 <*> pp r2 <*> pp fpscr
+  FP3 n r1 r2 r3 fpscr -> pp4 ("ppc_fp3 " ++ n) <$> pp r1 <*> pp r2 <*> pp r3 <*> pp fpscr
+  Vec1 n r1 vscr -> ppBinary ("ppc_vec1 " ++ n) <$> pp r1 <*> pp vscr
+  Vec2 n r1 r2 vscr -> pp3 ("ppc_vec2" ++ n) <$> pp r1 <*> pp r2 <*> pp vscr
+  Vec3 n r1 r2 r3 vscr -> pp4 ("ppc_vec3" ++ n) <$> pp r1 <*> pp r2 <*> pp r3 <*> pp vscr
+ where
+  ppUnary s v' = PP.text s PP.<+> v'
+  ppBinary s v1' v2' = PP.text s PP.<+> v1' PP.<+> v2'
+  pp3 s v1' v2' v3' = PP.text s PP.<+> v1' PP.<+> v2' PP.<+> v3'
+  pp4 s v1' v2' v3' v4' = PP.text s PP.<+> v1' PP.<+> v2' PP.<+> v3' PP.<+> v4'
 
 instance MC.IsArchFn (PPCPrimFn ppc) where
   ppArchFn = ppPrimFn
@@ -373,19 +563,37 @@ instance FC.FoldableFC (PPCPrimFn ppc) where
   foldMapFC = FC.foldMapFCDefault
 
 instance FC.TraversableFC (PPCPrimFn ppc) where
-  traverseFC go f =
-    case f of
-      UDiv rep lhs rhs -> UDiv rep <$> go lhs <*> go rhs
-      SDiv rep lhs rhs -> SDiv rep <$> go lhs <*> go rhs
-      FPIsQNaN info v -> FPIsQNaN info <$> go v
-      FPIsSNaN info v -> FPIsSNaN info <$> go v
-      FPCvt rep1 v rep2 -> FPCvt rep1 <$> go v <*> pure rep2
-      FP1 name op fpscr -> FP1 name <$> go op <*> go fpscr
-      FP2 name op1 op2 fpscr -> FP2 name <$> go op1 <*> go op2 <*> go fpscr
-      FP3 name op1 op2 op3 fpscr -> FP3 name <$> go op1 <*> go op2 <*> go op3 <*> go fpscr
-      Vec1 name op vscr -> Vec1 name <$> go op <*> go vscr
-      Vec2 name op1 op2 vscr -> Vec2 name <$> go op1 <*> go op2 <*> go vscr
-      Vec3 name op1 op2 op3 vscr -> Vec3 name <$> go op1 <*> go op2 <*> go op3 <*> go vscr
+  traverseFC go = \case
+    UDiv rep lhs rhs -> UDiv rep <$> go lhs <*> go rhs
+    SDiv rep lhs rhs -> SDiv rep <$> go lhs <*> go rhs
+    FPNeg  fi x -> FPNeg fi <$> go x
+    FPAbs  fi x -> FPAbs fi <$> go x
+    FPSqrt fi x -> FPSqrt fi <$> go x
+    FPAdd fi x y -> FPAdd fi <$> go x <*> go y
+    FPSub fi x y -> FPSub fi <$> go x <*> go y
+    FPMul fi x y -> FPMul fi <$> go x <*> go y
+    FPDiv fi x y -> FPDiv fi <$> go x <*> go y
+    FPFMA fi x y z -> FPFMA fi <$> go x <*> go y <*> go z
+    FPLt x y -> FPLt <$> go x <*> go y
+    FPEq x y -> FPEq <$> go x <*> go y
+    FPIsNaN x -> FPIsNaN <$> go x
+    FPCast       fi x -> FPCast fi <$> go x
+    FPToBinary   fi x -> FPToBinary fi <$> go x
+    FPFromBinary fi x -> FPFromBinary fi <$> go x
+    FPToSBV      w  x -> FPToSBV w <$> go x
+    FPToUBV      w  x -> FPToUBV w <$> go x
+    FPFromSBV    fi x -> FPFromSBV fi <$> go x
+    FPFromUBV    fi x -> FPFromUBV fi <$> go x
+    FPCoerce fi fi' x -> FPCoerce fi fi' <$> go x
+    FPSCR1 name op fpscr -> FPSCR1 name <$> go op <*> go fpscr
+    FPSCR2 name op1 op2 fpscr -> FPSCR2 name <$> go op1 <*> go op2 <*> go fpscr
+    FPSCR3 name op1 op2 op3 fpscr -> FPSCR3 name <$> go op1 <*> go op2 <*> go op3 <*> go fpscr
+    FP1 name op fpscr -> FP1 name <$> go op <*> go fpscr
+    FP2 name op1 op2 fpscr -> FP2 name <$> go op1 <*> go op2 <*> go fpscr
+    FP3 name op1 op2 op3 fpscr -> FP3 name <$> go op1 <*> go op2 <*> go op3 <*> go fpscr
+    Vec1 name op vscr -> Vec1 name <$> go op <*> go vscr
+    Vec2 name op1 op2 vscr -> Vec2 name <$> go op1 <*> go op2 <*> go vscr
+    Vec3 name op1 op2 op3 vscr -> Vec3 name <$> go op1 <*> go op2 <*> go op3 <*> go vscr
 
 type instance MC.ArchFn PPC64.PPC = PPCPrimFn PPC64.PPC
 type instance MC.ArchFn PPC32.PPC = PPCPrimFn PPC32.PPC
diff --git a/macaw-ppc/src/Data/Macaw/PPC/Eval.hs b/macaw-ppc/src/Data/Macaw/PPC/Eval.hs
index 2e72adbc..5d3adc4d 100644
--- a/macaw-ppc/src/Data/Macaw/PPC/Eval.hs
+++ b/macaw-ppc/src/Data/Macaw/PPC/Eval.hs
@@ -1,6 +1,7 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE GADTs #-}
+{-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE TypeOperators #-}
 module Data.Macaw.PPC.Eval (
@@ -96,19 +97,37 @@ absEvalArchFn :: (PPCArchConstraints ppc)
               -> AbsProcessorState (ArchReg ppc) ids
               -> ArchFn ppc (Value ppc ids) tp
               -> AbsValue (RegAddrWidth (ArchReg ppc)) tp
-absEvalArchFn _ _r f =
-  case f of
-    SDiv {} -> MA.TopV
-    UDiv {} -> MA.TopV
-    FPIsQNaN {} -> MA.TopV
-    FPIsSNaN {} -> MA.TopV
-    FPCvt {} -> MA.TopV
-    FP1 {} -> MA.TopV
-    FP2 {} -> MA.TopV
-    FP3 {} -> MA.TopV
-    Vec1 {} -> MA.TopV
-    Vec2 {} -> MA.TopV
-    Vec3 {} -> MA.TopV
+absEvalArchFn _ _r = \case
+  SDiv{}         -> MA.TopV
+  UDiv{}         -> MA.TopV
+  FPNeg{}        -> MA.TopV
+  FPAbs{}        -> MA.TopV
+  FPSqrt{}       -> MA.TopV
+  FPAdd{}        -> MA.TopV
+  FPSub{}        -> MA.TopV
+  FPMul{}        -> MA.TopV
+  FPDiv{}        -> MA.TopV
+  FPFMA{}        -> MA.TopV
+  FPLt{}         -> MA.TopV
+  FPEq{}         -> MA.TopV
+  FPIsNaN{}      -> MA.TopV
+  FPCast{}       -> MA.TopV
+  FPToBinary{}   -> MA.TopV
+  FPFromBinary{} -> MA.TopV
+  FPToSBV{}      -> MA.TopV
+  FPToUBV{}      -> MA.TopV
+  FPFromSBV{}    -> MA.TopV
+  FPFromUBV{}    -> MA.TopV
+  FPCoerce{}     -> MA.TopV
+  FPSCR1{}       -> MA.TopV
+  FPSCR2{}       -> MA.TopV
+  FPSCR3{}       -> MA.TopV
+  FP1{}          -> MA.TopV
+  FP2{}          -> MA.TopV
+  FP3{}          -> MA.TopV
+  Vec1{}         -> MA.TopV
+  Vec2{}         -> MA.TopV
+  Vec3{}         -> MA.TopV
 
 -- | For now, none of the architecture-specific statements have an effect on the
 -- abstract value.
diff --git a/macaw-ppc/src/Data/Macaw/PPC/Semantics/TH.hs b/macaw-ppc/src/Data/Macaw/PPC/Semantics/TH.hs
index cd462761..cb5fbde5 100644
--- a/macaw-ppc/src/Data/Macaw/PPC/Semantics/TH.hs
+++ b/macaw-ppc/src/Data/Macaw/PPC/Semantics/TH.hs
@@ -2,6 +2,7 @@
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
@@ -27,6 +28,7 @@ import qualified Data.Parameterized.Map as Map
 import           Data.Parameterized.Some ( Some(..) )
 import qualified Data.Parameterized.TraversableFC as FC
 import qualified What4.Expr.Builder as S
+import qualified What4.Interface as S
 
 import qualified SemMC.Architecture as A
 import qualified SemMC.Architecture.Location as L
@@ -39,7 +41,7 @@ import qualified Data.Macaw.Types as M
 import qualified Data.Macaw.SemMC.Generator as G
 import qualified Data.Macaw.SemMC.Operands as O
 import           Data.Macaw.SemMC.TH.Monad
-import           Data.Macaw.SemMC.TH ( natReprTH, addEltTH, symFnName, asName )
+import           Data.Macaw.SemMC.TH ( natReprTH, floatInfoFromPrecisionTH, addEltTH, symFnName, asName )
 
 import           Data.Macaw.PPC.Arch
 import           Data.Macaw.PPC.PPCReg
@@ -61,6 +63,56 @@ ppcNonceAppEval bvi nonceApp =
     S.FnApp symFn args -> do
       let fnName = symFnName symFn
       case fnName of
+        "uf_fp_un_op_fpscr" -> return $
+          case FC.toListFC Some args of
+            [Some op, Some frA, Some fpscr] -> case getOpName op of
+              Just name -> do
+                valA <- addEltTH bvi frA
+                valFpscr <- addEltTH bvi fpscr
+                liftQ [|
+                    addArchExpr $
+                      FPSCR1 $(lift name) $(return valA) $(return valFpscr)
+                  |]
+              Nothing ->
+                fail $ "Invalid argument list for un_op_fpscr: " ++ showF args
+            _ -> fail $ "Invalid argument list for un_op_fpscr: " ++ showF args
+        "uf_fp_bin_op_fpscr" -> return $
+          case FC.toListFC Some args of
+            [Some op, Some frA, Some frB, Some fpscr] -> case getOpName op of
+              Just name -> do
+                valA <- addEltTH bvi frA
+                valB <- addEltTH bvi frB
+                valFpscr <- addEltTH bvi fpscr
+                liftQ [|
+                    addArchExpr $ FPSCR2
+                      $(lift name)
+                      $(return valA)
+                      $(return valB)
+                      $(return valFpscr)
+                  |]
+              Nothing ->
+                fail $ "Invalid argument list for un_op_fpscr: " ++ showF args
+            _ -> fail $ "Invalid argument list for bin_op_fpscr: " ++ showF args
+        "uf_fp_tern_op_fpscr" -> return $
+          case FC.toListFC Some args of
+            [Some op, Some frA, Some frB, Some frC, Some fpscr] ->
+              case getOpName op of
+                Just name -> do
+                  valA <- addEltTH bvi frA
+                  valB <- addEltTH bvi frB
+                  valC <- addEltTH bvi frC
+                  valFpscr <- addEltTH bvi fpscr
+                  liftQ [|
+                      addArchExpr $ FPSCR3
+                        $(lift name)
+                        $(return valA)
+                        $(return valB)
+                        $(return valC)
+                        $(return valFpscr)
+                    |]
+                Nothing -> fail $
+                  "Invalid argument list for un_op_fpscr: " ++ showF args
+            _ -> fail $ "Invalid argument list for tern_op_fpscr: " ++ showF args
         "uf_ppc_fp1" -> return $ do
           case FC.toListFC Some args of
             [Some op, Some frA, Some fpscr] -> do
@@ -159,19 +211,21 @@ ppcNonceAppEval bvi nonceApp =
 elementaryFPName :: String -> Maybe String
 elementaryFPName = L.stripPrefix "uf_fp_"
 
-addArchAssignment :: (M.HasRepr (M.ArchFn arch (M.Value arch ids)) M.TypeRepr)
-                  => M.ArchFn arch (M.Value arch ids) tp
-                  -> G.Generator arch ids s (G.Expr arch ids tp)
-addArchAssignment expr = (G.ValueExpr . M.AssignedValue) <$> G.addAssignment (M.EvalArchFn expr (M.typeRepr expr))
+addArchAssignment
+  :: (M.HasRepr (M.ArchFn arch (M.Value arch ids)) M.TypeRepr)
+  => M.ArchFn arch (M.Value arch ids) tp
+  -> G.Generator arch ids s (G.Expr arch ids tp)
+addArchAssignment expr = G.ValueExpr . M.AssignedValue <$>
+  G.addAssignment (M.EvalArchFn expr (M.typeRepr expr))
 
-addArchExpr :: (MM.MemWidth (M.RegAddrWidth (M.ArchReg arch)),
-                OrdF (M.ArchReg arch),
-                M.HasRepr (M.ArchFn arch (M.Value arch ids)) M.TypeRepr)
-            => M.ArchFn arch (M.Value arch ids) tp
-            -> G.Generator arch ids s (M.Value arch ids tp)
-addArchExpr archfn = do
-  asgn <- G.addAssignment (M.EvalArchFn archfn (M.typeRepr archfn))
-  G.addExpr (G.ValueExpr (M.AssignedValue asgn))
+addArchExpr
+  :: ( MM.MemWidth (M.RegAddrWidth (M.ArchReg arch))
+     , OrdF (M.ArchReg arch)
+     , M.HasRepr (M.ArchFn arch (M.Value arch ids)) M.TypeRepr
+     )
+  => M.ArchFn arch (M.Value arch ids) tp
+  -> G.Generator arch ids s (M.Value arch ids tp)
+addArchExpr expr = G.addExpr =<< addArchAssignment expr
 
 floatingPointTH :: forall arch t fs f c
                  . (L.Location arch ~ APPC.Location arch,
@@ -185,31 +239,18 @@ floatingPointTH :: forall arch t fs f c
                  -> MacawQ arch t fs Exp
 floatingPointTH bvi fnName args =
   case FC.toListFC Some args of
-    [Some a] ->
-      case fnName of
-        "round_single" -> do
-          fpval <- addEltTH bvi a
-          liftQ [| addArchExpr (FPCvt M.DoubleFloatRepr $(return fpval) M.SingleFloatRepr) |]
-        "single_to_double" -> do
-          fpval <- addEltTH bvi a
-          liftQ [| addArchExpr (FPCvt M.SingleFloatRepr $(return fpval) M.DoubleFloatRepr) |]
-        "is_qnan32" -> do
-          fpval <- addEltTH bvi a
-          liftQ [| addArchExpr (FPIsQNaN M.SingleFloatRepr $(return fpval)) |]
-        "is_qnan64" -> do
-          fpval <- addEltTH bvi a
-          liftQ [| addArchExpr (FPIsQNaN M.DoubleFloatRepr $(return fpval)) |]
-        "is_snan32" -> do
-          fpval <- addEltTH bvi a
-          liftQ [| addArchExpr (FPIsSNaN M.SingleFloatRepr $(return fpval)) |]
-        "is_snan64" -> do
-          fpval <- addEltTH bvi a
-          liftQ [| addArchExpr (FPIsSNaN M.DoubleFloatRepr $(return fpval)) |]
-        _ -> fail ("Unsupported unary floating point intrinsic: " ++ fnName)
-    [Some a, Some b] ->
+    [Some a] -> case fnName of
+      "double_to_single" -> do
+        fpval <- addEltTH bvi a
+        liftQ [|
+            addArchExpr $
+              FPCoerce M.SingleFloatRepr M.DoubleFloatRepr $(return fpval)
+          |]
+      _ -> fail ("Unsupported unary floating point intrinsic: " ++ fnName)
+    [Some _a, Some _b] ->
       case fnName of
         _ -> fail ("Unsupported binary floating point intrinsic: " ++ fnName)
-    [Some a, Some b, Some c] ->
+    [Some _a, Some _b, Some _c] ->
       case fnName of
         _ -> fail ("Unsupported ternary floating point intrinsic: " ++ fnName)
     _ -> fail ("Unsupported floating point intrinsic: " ++ fnName)
@@ -221,7 +262,7 @@ ppcAppEvaluator :: (L.Location arch ~ APPC.Location arch,
                 => BoundVarInterpretations arch t fs
                 -> S.App (S.Expr t) ctp
                 -> Maybe (MacawQ arch t fs Exp)
-ppcAppEvaluator interps elt = case elt of
+ppcAppEvaluator interps = \case
   S.BVSdiv w bv1 bv2 -> return $ do
     e1 <- addEltTH interps bv1
     e2 <- addEltTH interps bv2
@@ -232,4 +273,111 @@ ppcAppEvaluator interps elt = case elt of
     e2 <- addEltTH interps bv2
     liftQ [| addArchAssignment (UDiv $(natReprTH w) $(return e1) $(return e2))
            |]
+
+  S.FloatNeg fpp fp -> return $ do
+    e <- addEltTH interps fp
+    liftQ [|
+        addArchAssignment $ FPNeg $(floatInfoFromPrecisionTH fpp) $(return e)
+      |]
+  S.FloatAbs fpp fp -> return $ do
+    e <- addEltTH interps fp
+    liftQ [|
+        addArchAssignment $ FPAbs $(floatInfoFromPrecisionTH fpp) $(return e)
+      |]
+  S.FloatSqrt fpp S.RNE fp -> return $ do
+    e <- addEltTH interps fp
+    liftQ [|
+        addArchAssignment $ FPSqrt $(floatInfoFromPrecisionTH fpp) $(return e)
+      |]
+
+  S.FloatAdd fpp S.RNE fp1 fp2 -> return $ do
+    e1 <- addEltTH interps fp1
+    e2 <- addEltTH interps fp2
+    liftQ [|
+        addArchAssignment $
+          FPAdd $(floatInfoFromPrecisionTH fpp) $(return e1) $(return e2)
+      |]
+  S.FloatSub fpp S.RNE fp1 fp2 -> return $ do
+    e1 <- addEltTH interps fp1
+    e2 <- addEltTH interps fp2
+    liftQ [|
+        addArchAssignment $
+          FPSub $(floatInfoFromPrecisionTH fpp) $(return e1) $(return e2)
+      |]
+  S.FloatMul fpp S.RNE fp1 fp2 -> return $ do
+    e1 <- addEltTH interps fp1
+    e2 <- addEltTH interps fp2
+    liftQ [|
+        addArchAssignment $
+          FPMul $(floatInfoFromPrecisionTH fpp) $(return e1) $(return e2)
+      |]
+  S.FloatDiv fpp S.RNE fp1 fp2 -> return $ do
+    e1 <- addEltTH interps fp1
+    e2 <- addEltTH interps fp2
+    liftQ [|
+        addArchAssignment $
+          FPDiv $(floatInfoFromPrecisionTH fpp) $(return e1) $(return e2)
+      |]
+
+  S.FloatFMA fpp S.RNE fp1 fp2 fp3 -> return $ do
+    e1 <- addEltTH interps fp1
+    e2 <- addEltTH interps fp2
+    e3 <- addEltTH interps fp3
+    liftQ [|
+        addArchAssignment $ FPFMA
+          $(floatInfoFromPrecisionTH fpp)
+          $(return e1)
+          $(return e2)
+          $(return e3)
+      |]
+
+  S.FloatLt fp1 fp2 -> return $ do
+    e1 <- addEltTH interps fp1
+    e2 <- addEltTH interps fp2
+    liftQ [| addArchAssignment $ FPLt $(return e1) $(return e2) |]
+  S.FloatFpEq fp1 fp2 -> return $ do
+    e1 <- addEltTH interps fp1
+    e2 <- addEltTH interps fp2
+    liftQ [| addArchAssignment $ FPEq $(return e1) $(return e2) |]
+
+  S.FloatIsNaN fp -> return $ do
+    e <- addEltTH interps fp
+    liftQ [| addArchAssignment $ FPIsNaN $(return e) |]
+
+  S.FloatCast fpp S.RNE fp -> return $ do
+    e <- addEltTH interps fp
+    liftQ [|
+        addArchAssignment $ FPCast $(floatInfoFromPrecisionTH fpp) $(return e)
+      |]
+  S.FloatToBinary fpp fp -> return $ do
+    e <- addEltTH interps fp
+    liftQ [|
+        addArchAssignment $
+          FPToBinary $(floatInfoFromPrecisionTH fpp) $(return e)
+      |]
+  S.FloatFromBinary fpp fp -> return $ do
+    e <- addEltTH interps fp
+    liftQ [|
+        addArchAssignment $
+          FPFromBinary $(floatInfoFromPrecisionTH fpp) $(return e)
+      |]
+  S.FloatToSBV w S.RNE fp -> return $ do
+    e <- addEltTH interps fp
+    liftQ [| addArchAssignment $ FPToSBV $(natReprTH w) $(return e) |]
+  S.FloatToBV w S.RNE fp -> return $ do
+    e <- addEltTH interps fp
+    liftQ [| addArchAssignment $ FPToUBV $(natReprTH w) $(return e) |]
+  S.SBVToFloat fpp S.RNE fp -> return $ do
+    e <- addEltTH interps fp
+    liftQ [|
+        addArchAssignment $
+          FPFromUBV $(floatInfoFromPrecisionTH fpp) $(return e)
+      |]
+  S.BVToFloat fpp S.RNE fp -> return $ do
+    e <- addEltTH interps fp
+    liftQ [|
+        addArchAssignment $
+          FPFromUBV $(floatInfoFromPrecisionTH fpp) $(return e)
+      |]
+
   _ -> Nothing