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

Updated macaw-ppc to handle floating-point UFs

Browse Source
This commit is contained in:
Ben Selfridge 2018-01-17 12:54:30 -08:00
parent 8229de9ff7
commit 7e47db94a3
4 changed files with 88 additions and 205 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

173
macaw-ppc/src/Data/Macaw/PPC/Arch.hs
View File

@ -144,39 +144,43 @@ data PPCPrimFn ppc f tp where
-> f (MT.BVType (MC.RegAddrWidth (MC.ArchReg ppc)))
-> 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
FPAdd :: !(MT.FloatInfoRepr flt) -> !(f (MT.FloatType flt)) -> !(f (MT.FloatType flt)) -> PPCPrimFn ppc f (MT.FloatType flt)
FPAddRoundedUp :: !(MT.FloatInfoRepr flt) -> !(f (MT.FloatType flt)) -> !(f (MT.FloatType flt)) -> PPCPrimFn ppc f MT.BoolType
FPSub :: !(MT.FloatInfoRepr flt) -> !(f (MT.FloatType flt)) -> !(f (MT.FloatType flt)) -> PPCPrimFn ppc f (MT.FloatType flt)
FPSubRoundedUp :: !(MT.FloatInfoRepr flt) -> !(f (MT.FloatType flt)) -> !(f (MT.FloatType flt)) -> PPCPrimFn ppc f MT.BoolType
FPMul :: !(MT.FloatInfoRepr flt) -> !(f (MT.FloatType flt)) -> !(f (MT.FloatType flt)) -> PPCPrimFn ppc f (MT.FloatType flt)
FPMulRoundedUp :: !(MT.FloatInfoRepr flt) -> !(f (MT.FloatType flt)) -> !(f (MT.FloatType flt)) -> PPCPrimFn ppc f MT.BoolType
FPDiv :: !(MT.FloatInfoRepr flt) -> !(f (MT.FloatType flt)) -> !(f (MT.FloatType flt)) -> PPCPrimFn ppc f (MT.FloatType flt)
FPLt :: !(MT.FloatInfoRepr flt) -> !(f (MT.FloatType flt)) -> !(f (MT.FloatType flt)) -> PPCPrimFn ppc f MT.BoolType
FPEq :: !(MT.FloatInfoRepr flt) -> !(f (MT.FloatType 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')
FPCvtRoundsUp :: !(MT.FloatInfoRepr flt) -> !(f (MT.FloatType flt)) -> !(MT.FloatInfoRepr flt') -> PPCPrimFn ppc f MT.BoolType
FPFromBV :: !(f (MT.BVType n)) -> !(MT.FloatInfoRepr flt) -> PPCPrimFn ppc f (MT.FloatType flt)
TruncFPToSignedBV :: (1 <= n) => MT.FloatInfoRepr flt -> f (MT.FloatType flt) -> NR.NatRepr n -> PPCPrimFn ppc f (MT.BVType n)
FPAbs :: !(MT.FloatInfoRepr flt) -> !(f (MT.FloatType flt)) -> PPCPrimFn ppc f (MT.FloatType flt)
FPNeg :: !(MT.FloatInfoRepr flt) -> !(f (MT.FloatType flt)) -> PPCPrimFn ppc f (MT.FloatType flt)
-- | Uninterpreted floating point functions
FP1 :: !String -- ^ the name of the function
-> !(f (MT.BVType 128)) -- ^ arg 1
-> !(f (MT.BVType 32)) -- ^ current fpscr
-> PPCPrimFn ppc f (MT.BVType 160)
FP2 :: !String
-> !(f (MT.BVType 128))
-> !(f (MT.BVType 128))
-> !(f (MT.BVType 32))
-> PPCPrimFn ppc f (MT.BVType 160)
FP3 :: !String
-> !(f (MT.BVType 128))
-> !(f (MT.BVType 128))
-> !(f (MT.BVType 128))
-> !(f (MT.BVType 32))
-> PPCPrimFn ppc f (MT.BVType 160)
-- | Uninterpreted vector functions
Vec1 :: String -- ^ the name of the function
-> f (MT.BVType 128)
-> f (MT.BVType 32)
Vec1 :: !String -- ^ the name of the function
-> !(f (MT.BVType 128))
-> !(f (MT.BVType 32))
-> PPCPrimFn ppc f (MT.BVType 160)
Vec2 :: String -- ^ the name of the function
-> f (MT.BVType 128)
-> f (MT.BVType 128)
-> f (MT.BVType 32)
-> !(f (MT.BVType 128))
-> !(f (MT.BVType 128))
-> !(f (MT.BVType 32))
-> PPCPrimFn ppc f (MT.BVType 160)
Vec3 :: String -- ^ the name of the function
-> f (MT.BVType 128)
-> f (MT.BVType 128)
-> f (MT.BVType 128)
-> f (MT.BVType 32)
-> !(f (MT.BVType 128))
-> !(f (MT.BVType 128))
-> !(f (MT.BVType 128))
-> !(f (MT.BVType 32))
-> PPCPrimFn ppc f (MT.BVType 160)
instance (1 <= MC.RegAddrWidth (MC.ArchReg ppc)) => MT.HasRepr (PPCPrimFn ppc (MC.Value ppc ids)) MT.TypeRepr where
@ -187,23 +191,12 @@ instance (1 <= MC.RegAddrWidth (MC.ArchReg ppc)) => MT.HasRepr (PPCPrimFn ppc (M
FPIsQNaN _ _ -> MT.BoolTypeRepr
FPIsSNaN _ _ -> MT.BoolTypeRepr
FPAdd rep _ _ -> MT.floatTypeRepr rep
FPAddRoundedUp _ _ _ -> MT.BoolTypeRepr
FPSub rep _ _ -> MT.floatTypeRepr rep
FPSubRoundedUp _ _ _ -> MT.BoolTypeRepr
FPMul rep _ _ -> MT.floatTypeRepr rep
FPMulRoundedUp _ _ _ -> MT.BoolTypeRepr
FPDiv rep _ _ -> MT.floatTypeRepr rep
FPLt _ _ _ -> MT.BoolTypeRepr
FPEq _ _ _ -> MT.BoolTypeRepr
FPCvt _ _ rep -> MT.floatTypeRepr rep
FPCvtRoundsUp _ _ _ -> MT.BoolTypeRepr
FPFromBV _ rep -> MT.floatTypeRepr rep
TruncFPToSignedBV _ _ rep -> MT.BVTypeRepr rep
FPAbs rep _ -> MT.floatTypeRepr rep
FPNeg rep _ -> MT.floatTypeRepr rep
-- FIXME: Is this right?
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
@ -218,21 +211,10 @@ ppcPrimFnHasSideEffects pf =
SDiv {} -> False
FPIsQNaN {} -> False
FPIsSNaN {} -> False
FPAdd {} -> False
FPAddRoundedUp {} -> False
FPSub {} -> False
FPSubRoundedUp {} -> False
FPMul {} -> False
FPMulRoundedUp {} -> False
FPDiv {} -> False
FPLt {} -> False
FPEq {} -> False
FPCvt {} -> False
FPCvtRoundsUp {} -> False
FPFromBV {} -> False
TruncFPToSignedBV {} -> False
FPAbs {} -> False
FPNeg {} -> False
FP1 {} -> False
FP2 {} -> False
FP3 {} -> False
Vec1 {} -> False
Vec2 {} -> False
Vec3 {} -> False
@ -254,51 +236,18 @@ rewritePrimFn f =
FPIsSNaN info v -> do
tgt <- FPIsSNaN info <$> rewriteValue v
evalRewrittenArchFn tgt
FPAdd rep v1 v2 -> do
tgt <- FPAdd rep <$> rewriteValue v1 <*> rewriteValue v2
evalRewrittenArchFn tgt
FPAddRoundedUp rep v1 v2 -> do
tgt <- FPAddRoundedUp rep <$> rewriteValue v1 <*> rewriteValue v2
evalRewrittenArchFn tgt
FPSub rep v1 v2 -> do
tgt <- FPSub rep <$> rewriteValue v1 <*> rewriteValue v2
evalRewrittenArchFn tgt
FPSubRoundedUp rep v1 v2 -> do
tgt <- FPSubRoundedUp rep <$> rewriteValue v1 <*> rewriteValue v2
evalRewrittenArchFn tgt
FPMul rep v1 v2 -> do
tgt <- FPMul rep <$> rewriteValue v1 <*> rewriteValue v2
evalRewrittenArchFn tgt
FPMulRoundedUp rep v1 v2 -> do
tgt <- FPMulRoundedUp rep <$> rewriteValue v1 <*> rewriteValue v2
evalRewrittenArchFn tgt
FPDiv rep v1 v2 -> do
tgt <- FPDiv rep <$> rewriteValue v1 <*> rewriteValue v2
evalRewrittenArchFn tgt
FPLt rep v1 v2 -> do
tgt <- FPLt rep <$> rewriteValue v1 <*> rewriteValue v2
evalRewrittenArchFn tgt
FPEq rep v1 v2 -> do
tgt <- FPEq rep <$> rewriteValue v1 <*> rewriteValue v2
evalRewrittenArchFn tgt
FPCvt rep1 v rep2 -> do
tgt <- FPCvt rep1 <$> rewriteValue v <*> pure rep2
evalRewrittenArchFn tgt
FPCvtRoundsUp rep1 v rep2 -> do
tgt <- FPCvtRoundsUp rep1 <$> rewriteValue v <*> pure rep2
evalRewrittenArchFn tgt
FPFromBV bv rep -> do
tgt <- FPFromBV <$> rewriteValue bv <*> pure rep
evalRewrittenArchFn tgt
TruncFPToSignedBV info v rep -> do
tgt <- TruncFPToSignedBV info <$> rewriteValue v <*> pure rep
evalRewrittenArchFn tgt
FPAbs rep v -> do
tgt <- FPAbs rep <$> rewriteValue v
evalRewrittenArchFn tgt
FPNeg rep v -> do
tgt <- FPNeg rep <$> rewriteValue v
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
@ -316,21 +265,10 @@ ppPrimFn pp f =
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
FPAdd _rep v1 v2 -> ppBinary "ppc_fp_add" <$> pp v1 <*> pp v2
FPAddRoundedUp _rep v1 v2 -> ppBinary "ppc_fp_add_roundedup" <$> pp v1 <*> pp v2
FPSub _rep v1 v2 -> ppBinary "ppc_fp_sub" <$> pp v1 <*> pp v2
FPSubRoundedUp _rep v1 v2 -> ppBinary "ppc_fp_sub_roundedup" <$> pp v1 <*> pp v2
FPMul _rep v1 v2 -> ppBinary "ppc_fp_mul" <$> pp v1 <*> pp v2
FPMulRoundedUp _rep v1 v2 -> ppBinary "ppc_fp_mul_roundedup" <$> pp v1 <*> pp v2
FPDiv _rep v1 v2 -> ppBinary "ppc_fp_div" <$> pp v1 <*> pp v2
FPLt _rep v1 v2 -> ppBinary "ppc_fp_lt" <$> pp v1 <*> pp v2
FPEq _rep v1 v2 -> ppBinary "ppc_fp_eq" <$> pp v1 <*> pp v2
FPCvt _rep1 v _rep2 -> ppUnary "ppc_fp_cvt" <$> pp v
FPCvtRoundsUp _rep1 v _rep2 -> ppUnary "ppc_fp_cvt_roundedup" <$> pp v
FPFromBV bv _rep -> ppUnary "ppc_fp_frombv" <$> pp bv
TruncFPToSignedBV _info v _rep -> ppUnary "ppc_fp_trunc_to_signed_bv" <$> pp v
FPAbs _rep v -> ppUnary "ppc_fp_abs" <$> pp v
FPNeg _rep v -> ppUnary "ppc_fp_neg" <$> 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
@ -356,21 +294,10 @@ instance FC.TraversableFC (PPCPrimFn ppc) where
SDiv rep lhs rhs -> SDiv rep <$> go lhs <*> go rhs
FPIsQNaN info v -> FPIsQNaN info <$> go v
FPIsSNaN info v -> FPIsSNaN info <$> go v
FPAdd rep v1 v2 -> FPAdd rep <$> go v1 <*> go v2
FPAddRoundedUp rep v1 v2 -> FPAddRoundedUp rep <$> go v1 <*> go v2
FPSub rep v1 v2 -> FPSub rep <$> go v1 <*> go v2
FPSubRoundedUp rep v1 v2 -> FPSubRoundedUp rep <$> go v1 <*> go v2
FPMul rep v1 v2 -> FPMul rep <$> go v1 <*> go v2
FPMulRoundedUp rep v1 v2 -> FPMulRoundedUp rep <$> go v1 <*> go v2
FPDiv rep v1 v2 -> FPDiv rep <$> go v1 <*> go v2
FPLt rep v1 v2 -> FPLt rep <$> go v1 <*> go v2
FPEq rep v1 v2 -> FPEq rep <$> go v1 <*> go v2
FPCvt rep1 v rep2 -> FPCvt rep1 <$> go v <*> pure rep2
FPCvtRoundsUp rep1 v rep2 -> FPCvtRoundsUp rep1 <$> go v <*> pure rep2
FPFromBV bv rep -> FPFromBV <$> go bv <*> pure rep
TruncFPToSignedBV info v rep -> TruncFPToSignedBV info <$> go v <*> pure rep
FPAbs rep v -> FPAbs rep <$> go v
FPNeg rep v -> FPNeg rep <$> go v
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

17
macaw-ppc/src/Data/Macaw/PPC/Eval.hs
View File

@ -100,21 +100,10 @@ absEvalArchFn _ _r f =
UDiv {} -> MA.TopV
FPIsQNaN {} -> MA.TopV
FPIsSNaN {} -> MA.TopV
FPAdd {} -> MA.TopV
FPAddRoundedUp {} -> MA.TopV
FPSub {} -> MA.TopV
FPSubRoundedUp {} -> MA.TopV
FPMul {} -> MA.TopV
FPMulRoundedUp {} -> MA.TopV
FPDiv {} -> MA.TopV
FPLt {} -> MA.TopV
FPEq {} -> MA.TopV
FPCvt {} -> MA.TopV
FPCvtRoundsUp {} -> MA.TopV
FPFromBV {} -> MA.TopV
TruncFPToSignedBV {} -> MA.TopV
FPAbs {} -> MA.TopV
FPNeg {} -> MA.TopV
FP1 {} -> MA.TopV
FP2 {} -> MA.TopV
FP3 {} -> MA.TopV
Vec1 {} -> MA.TopV
Vec2 {} -> MA.TopV
Vec3 {} -> MA.TopV

101
macaw-ppc/src/Data/Macaw/PPC/Semantics/TH.hs
View File

@ -61,6 +61,39 @@ ppcNonceAppEval bvi nonceApp =
S.FnApp symFn args -> do
let fnName = symFnName symFn
case fnName of
"ppc_fp1" -> return $ do
case FC.toListFC Some args of
[Some op, Some frA, Some fpscr] -> do
case getOpName op of
Just name -> do
valA <- addEltTH bvi frA
valFpscr <- addEltTH bvi fpscr
liftQ [| addArchExpr $ FP1 $(lift name) $(return valA) $(return valFpscr) |]
Nothing -> fail $ "Invalid argument list for ppc.fp1: " ++ showF args
_ -> fail $ "Invalid argument list for ppc.fp1: " ++ showF args
"ppc_fp2" -> return $ do
case FC.toListFC Some args of
[Some op, Some frA, Some frB, Some fpscr] -> do
case getOpName op of
Just name -> do
valA <- addEltTH bvi frA
valB <- addEltTH bvi frB
valFpscr <- addEltTH bvi fpscr
liftQ [| addArchExpr $ FP2 $(lift name) $(return valA) $(return valB) $(return valFpscr) |]
Nothing -> fail $ "Invalid argument list for ppc.fp2: " ++ showF args
_ -> fail $ "Invalid argument list for ppc.fp2: " ++ showF args
"ppc_fp3" -> return $ do
case FC.toListFC Some args of
[Some op, Some frA, Some frB, Some frC, Some fpscr] -> do
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 $ FP3 $(lift name) $(return valA) $(return valB) $(return valC) $(return valFpscr) |]
Nothing -> fail $ "Invalid argument list for ppc.fp2: " ++ showF args
_ -> fail $ "Invalid argument list for ppc.fp2: " ++ showF args
"ppc_vec1" -> return $ do
case FC.toListFC Some args of
[Some op, Some rA, Some vscr] -> do
@ -70,7 +103,7 @@ ppcNonceAppEval bvi nonceApp =
valVscr <- addEltTH bvi vscr
liftQ [| addArchExpr $ Vec1 $(lift name) $(return valA) $(return valVscr) |]
Nothing -> fail $ "Invalid argument list for ppc.vec1: " ++ showF args
_ -> fail $ "Invalid argument list for ppc.vec2: " ++ showF args
_ -> fail $ "Invalid argument list for ppc.vec1: " ++ showF args
"ppc_vec2" -> return $ do
case FC.toListFC Some args of
[Some op, Some rA, Some rB, Some vscr] -> do
@ -160,18 +193,6 @@ floatingPointTH bvi fnName args =
"single_to_double" -> do
fpval <- addEltTH bvi a
liftQ [| addArchExpr (FPCvt M.SingleFloatRepr $(return fpval) M.DoubleFloatRepr) |]
"abs" -> do
-- Note that fabs is only defined for doubles; the operation is the
-- same for single and double precision on PPC, so there is only a
-- single instruction.
fpval <- addEltTH bvi a
liftQ [| addArchExpr (FPAbs M.DoubleFloatRepr $(return fpval)) |]
"negate64" -> do
fpval <- addEltTH bvi a
liftQ [| addArchExpr (FPNeg M.DoubleFloatRepr $(return fpval)) |]
"negate32" -> do
fpval <- addEltTH bvi a
liftQ [| addArchExpr (FPNeg M.SingleFloatRepr $(return fpval)) |]
"is_qnan32" -> do
fpval <- addEltTH bvi a
liftQ [| addArchExpr (FPIsQNaN M.SingleFloatRepr $(return fpval)) |]
@ -187,63 +208,9 @@ floatingPointTH bvi fnName args =
_ -> fail ("Unsupported unary floating point intrinsic: " ++ fnName)
[Some a, Some b] ->
case fnName of
"add64" -> do
valA <- addEltTH bvi a
valB <- addEltTH bvi b
liftQ [| addArchExpr (FPAdd M.DoubleFloatRepr $(return valA) $(return valB)) |]
"add32" -> do
valA <- addEltTH bvi a
valB <- addEltTH bvi b
liftQ [| addArchExpr (FPAdd M.SingleFloatRepr $(return valA) $(return valB)) |]
"sub64" -> do
valA <- addEltTH bvi a
valB <- addEltTH bvi b
liftQ [| addArchExpr (FPSub M.DoubleFloatRepr $(return valA) $(return valB)) |]
"sub32" -> do
valA <- addEltTH bvi a
valB <- addEltTH bvi b
liftQ [| addArchExpr (FPSub M.SingleFloatRepr $(return valA) $(return valB)) |]
"mul64" -> do
valA <- addEltTH bvi a
valB <- addEltTH bvi b
liftQ [| addArchExpr (FPMul M.DoubleFloatRepr $(return valA) $(return valB)) |]
"mul32" -> do
valA <- addEltTH bvi a
valB <- addEltTH bvi b
liftQ [| addArchExpr (FPMul M.SingleFloatRepr $(return valA) $(return valB)) |]
"div64" -> do
valA <- addEltTH bvi a
valB <- addEltTH bvi b
liftQ [| addArchExpr (FPDiv M.DoubleFloatRepr $(return valA) $(return valB)) |]
"div32" -> do
valA <- addEltTH bvi a
valB <- addEltTH bvi b
liftQ [| addArchExpr (FPDiv M.SingleFloatRepr $(return valA) $(return valB)) |]
"lt" -> do
valA <- addEltTH bvi a
valB <- addEltTH bvi b
-- All comparisons are done as 64-bit comparisons in PPC
liftQ [| addArchExpr (FPLt M.DoubleFloatRepr $(return valA) $(return valB)) |]
_ -> fail ("Unsupported binary floating point intrinsic: " ++ fnName)
[Some a, Some b, Some c] ->
case fnName of
"muladd64" -> do
-- FIXME: This is very wrong - we need a separate constructor for it
-- a * c + b
valA <- addEltTH bvi a
valB <- addEltTH bvi b
valC <- addEltTH bvi c
liftQ [| do prodVal <- addArchExpr (FPMul M.DoubleFloatRepr $(return valA) $(return valC))
addArchExpr (FPAdd M.DoubleFloatRepr prodVal $(return valB))
|]
"muladd32" -> do
-- a * c + b
valA <- addEltTH bvi a
valB <- addEltTH bvi b
valC <- addEltTH bvi c
liftQ [| do prodVal <- addArchExpr (FPMul M.SingleFloatRepr $(return valA) $(return valC))
addArchExpr (FPAdd M.SingleFloatRepr prodVal $(return valB))
|]
_ -> fail ("Unsupported ternary floating point intrinsic: " ++ fnName)
_ -> fail ("Unsupported floating point intrinsic: " ++ fnName)

2
submodules/semmc

@ -1 +1 @@
Subproject commit de3cef59472041fbfd69494978a8de28716d3f5f
Subproject commit c3a8cbb52bcc7f3f44d73b5590fda11d1e609200