mirror of
https://github.com/GaloisInc/macaw.git
synced 2024-12-29 17:17:05 +03:00
Add floats to Macaw-PPC.
This commit is contained in:
Andrei Stefanescu
parent
54e33d8f5c
commit
2886c86e2b
@ -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,34 +382,69 @@ 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
|
||||
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
|
||||
ppcPrimFnHasSideEffects = \case
|
||||
UDiv{} -> False
|
||||
SDiv{} -> False
|
||||
FPIsQNaN {} -> False
|
||||
FPIsSNaN {} -> False
|
||||
FPCvt {} -> 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
|
||||
@ -307,23 +455,47 @@ ppcPrimFnHasSideEffects pf =
|
||||
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
|
||||
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
|
||||
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
|
||||
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
|
||||
@ -344,13 +516,31 @@ rewritePrimFn f =
|
||||
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
|
||||
ppPrimFn pp = \case
|
||||
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
|
||||
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
|
||||
@ -373,13 +563,31 @@ instance FC.FoldableFC (PPCPrimFn ppc) where
|
||||
foldMapFC = FC.foldMapFCDefault
|
||||
|
||||
instance FC.TraversableFC (PPCPrimFn ppc) where
|
||||
traverseFC go f =
|
||||
case f of
|
||||
traverseFC go = \case
|
||||
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
|
||||
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
|
||||
|
||||
@ -1,6 +1,7 @@
|
||||
{-# LANGUAGE DataKinds #-}
|
||||
{-# LANGUAGE FlexibleContexts #-}
|
||||
{-# LANGUAGE GADTs #-}
|
||||
{-# LANGUAGE LambdaCase #-}
|
||||
{-# LANGUAGE RankNTypes #-}
|
||||
{-# LANGUAGE TypeOperators #-}
|
||||
module Data.Macaw.PPC.Eval (
|
||||
@ -96,13 +97,31 @@ absEvalArchFn :: (PPCArchConstraints ppc)
|
||||
-> AbsProcessorState (ArchReg ppc) ids
|
||||
-> ArchFn ppc (Value ppc ids) tp
|
||||
-> AbsValue (RegAddrWidth (ArchReg ppc)) tp
|
||||
absEvalArchFn _ _r f =
|
||||
case f of
|
||||
absEvalArchFn _ _r = \case
|
||||
SDiv{} -> MA.TopV
|
||||
UDiv{} -> MA.TopV
|
||||
FPIsQNaN {} -> MA.TopV
|
||||
FPIsSNaN {} -> MA.TopV
|
||||
FPCvt {} -> 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
|
||||
|
||||
@ -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)
|
||||
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 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)
|
||||
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 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
|
||||
[Some a] -> case fnName of
|
||||
"double_to_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)) |]
|
||||
liftQ [|
|
||||
addArchExpr $
|
||||
FPCoerce M.SingleFloatRepr M.DoubleFloatRepr $(return fpval)
|
||||
|]
|
||||
_ -> fail ("Unsupported unary floating point intrinsic: " ++ fnName)
|
||||
[Some a, Some b] ->
|
||||
[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
|
||||
|
||||
Loading…
Reference in New Issue
Block a user