GaloisInc/macaw
1
1
Fork 0
mirror of https://github.com/GaloisInc/macaw.git synced 2024-12-26 23:52:48 +03:00
Code Issues Projects Releases Wiki Activity

Merge branch 'master' into kwq/macaw-arm

Browse Source
This commit is contained in:
Kevin Quick 2018-01-10 11:30:05 -08:00
commit 8229de9ff7
13 changed files with 308 additions and 46 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -57,7 +57,7 @@ type PPC64 = PPC64.PPC
-- | The type tag for 32 bit PowerPC
type PPC32 = PPC32.PPC
archDemandContext :: (PPCArchConstraints ppc) => proxy ppc -> MDS.DemandContext ppc ids
archDemandContext :: (PPCArchConstraints ppc) => proxy ppc -> MDS.DemandContext ppc
archDemandContext _ =
MDS.DemandContext { MDS.demandConstraints = \a -> a
, MDS.archFnHasSideEffects = ppcPrimFnHasSideEffects

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

@ -76,13 +76,13 @@ data PPCStmt ppc (v :: MT.Type -> *) where
Sync :: PPCStmt ppc v
Isync :: PPCStmt ppc v
-- These are cache hints
Dcba :: v (MT.BVType (MC.RegAddrWidth (MC.ArchReg ppc))) -> PPCStmt ppc v
Dcbf :: v (MT.BVType (MC.RegAddrWidth (MC.ArchReg ppc))) -> PPCStmt ppc v
Dcbi :: v (MT.BVType (MC.RegAddrWidth (MC.ArchReg ppc))) -> PPCStmt ppc v
Dcbst :: v (MT.BVType (MC.RegAddrWidth (MC.ArchReg ppc))) -> PPCStmt ppc v
Dcbz :: v (MT.BVType (MC.RegAddrWidth (MC.ArchReg ppc))) -> PPCStmt ppc v
Dcbzl :: v (MT.BVType (MC.RegAddrWidth (MC.ArchReg ppc))) -> PPCStmt ppc v
Dcbt :: v (MT.BVType (MC.RegAddrWidth (MC.ArchReg ppc))) -> v (MT.BVType 5) -> PPCStmt ppc v
Dcba :: v (MT.BVType (MC.RegAddrWidth (MC.ArchReg ppc))) -> PPCStmt ppc v
Dcbf :: v (MT.BVType (MC.RegAddrWidth (MC.ArchReg ppc))) -> PPCStmt ppc v
Dcbi :: v (MT.BVType (MC.RegAddrWidth (MC.ArchReg ppc))) -> PPCStmt ppc v
Dcbst :: v (MT.BVType (MC.RegAddrWidth (MC.ArchReg ppc))) -> PPCStmt ppc v
Dcbz :: v (MT.BVType (MC.RegAddrWidth (MC.ArchReg ppc))) -> PPCStmt ppc v
Dcbzl :: v (MT.BVType (MC.RegAddrWidth (MC.ArchReg ppc))) -> PPCStmt ppc v
Dcbt :: v (MT.BVType (MC.RegAddrWidth (MC.ArchReg ppc))) -> v (MT.BVType 5) -> PPCStmt ppc v
Dcbtst :: v (MT.BVType (MC.RegAddrWidth (MC.ArchReg ppc))) -> v (MT.BVType 5) -> PPCStmt ppc v
instance TF.FunctorF (PPCStmt ppc) where
@ -144,6 +144,40 @@ 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 vector functions
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)
-> 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)
-> PPCPrimFn ppc f (MT.BVType 160)
instance (1 <= MC.RegAddrWidth (MC.ArchReg ppc)) => MT.HasRepr (PPCPrimFn ppc (MC.Value ppc ids)) MT.TypeRepr where
typeRepr f =
@ -151,6 +185,30 @@ instance (1 <= MC.RegAddrWidth (MC.ArchReg ppc)) => MT.HasRepr (PPCPrimFn ppc (M
UDiv rep _ _ -> MT.BVTypeRepr rep
SDiv rep _ _ -> MT.BVTypeRepr rep
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?
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
@ -158,6 +216,26 @@ ppcPrimFnHasSideEffects pf =
case pf of
UDiv {} -> False
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
Vec1 {} -> False
Vec2 {} -> False
Vec3 {} -> False
rewritePrimFn :: (PPCArchConstraints ppc, MC.ArchFn ppc ~ PPCPrimFn ppc)
=> PPCPrimFn ppc (MC.Value ppc src) tp
@ -170,12 +248,97 @@ rewritePrimFn f =
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
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
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 -> (\lhs' rhs' -> PP.text "ppc_udiv " PP.<> lhs' PP.<> PP.text " " PP.<> rhs') <$> pp lhs <*> pp rhs
SDiv _ lhs rhs -> (\lhs' rhs' -> PP.text "ppc_sdiv " PP.<> lhs' PP.<> PP.text " " PP.<> rhs') <$> pp lhs <*> pp rhs
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
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
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
@ -191,6 +354,26 @@ instance FC.TraversableFC (PPCPrimFn ppc) where
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
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
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

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

@ -98,6 +98,26 @@ absEvalArchFn _ _r f =
case f of
SDiv {} -> MA.TopV
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
Vec1 {} -> MA.TopV
Vec2 {} -> MA.TopV
Vec3 {} -> MA.TopV
-- | For now, none of the architecture-specific statements have an effect on the
-- abstract value.

6
macaw-ppc/src/Data/Macaw/PPC/PPCReg.hs
View File

@ -48,6 +48,7 @@ data PPCReg arch tp where
PPC_CR :: PPCReg arch (BVType 32)
PPC_XER :: (w ~ MC.RegAddrWidth (PPCReg arch), 1 <= w) => PPCReg arch (BVType w)
PPC_FPSCR :: PPCReg arch (BVType 32)
PPC_VSCR :: PPCReg arch (BVType 32)
deriving instance Eq (PPCReg arch tp)
deriving instance Ord (PPCReg arch tp)
@ -63,6 +64,7 @@ instance Show (PPCReg arch tp) where
PPC_CR -> "cr"
PPC_XER -> "xer"
PPC_FPSCR -> "fpscr"
PPC_VSCR -> "vscr"
instance ShowF (PPCReg arch) where
showF = show
@ -122,6 +124,7 @@ instance (ArchWidth ppc) => HasRepr (PPCReg ppc) TypeRepr where
PPC_CR -> BVTypeRepr n32
PPC_XER -> BVTypeRepr (pointerNatRepr (Proxy @ppc))
PPC_FPSCR -> BVTypeRepr n32
PPC_VSCR -> BVTypeRepr n32
instance ( ArchWidth ppc
@ -144,7 +147,7 @@ ppcRegs = concat [ gprs
, fprs
]
where
sprs = [ Some PPC_IP, Some PPC_LNK, Some PPC_CTR, Some PPC_CR, Some PPC_XER, Some PPC_FPSCR ]
sprs = [ Some PPC_IP, Some PPC_LNK, Some PPC_CTR, Some PPC_CR, Some PPC_XER, Some PPC_FPSCR, Some PPC_VSCR ]
gprs = [ Some (PPC_GP (D.GPR rnum))
| rnum <- [0..31]
]
@ -167,4 +170,5 @@ locToRegTH _ APPC.LocCTR = [| PPC_CTR |]
locToRegTH _ APPC.LocCR = [| PPC_CR |]
locToRegTH _ APPC.LocXER = [| PPC_XER |]
locToRegTH _ APPC.LocFPSCR = [| PPC_FPSCR |]
locToRegTH _ APPC.LocVSCR = [| PPC_VSCR |]
locToRegTH _ _ = [| undefined |]

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

@ -19,6 +19,7 @@ import qualified Data.Functor.Const as C
import Data.Proxy ( Proxy(..) )
import qualified Data.List as L
import Language.Haskell.TH
import Language.Haskell.TH.Syntax (lift)
import GHC.TypeLits
import Data.Parameterized.Classes
@ -32,6 +33,7 @@ import qualified SemMC.Architecture.Location as L
import qualified SemMC.Architecture.PPC.Eval as PE
import qualified SemMC.Architecture.PPC.Location as APPC
import qualified Data.Macaw.CFG as M
import qualified Data.Macaw.Memory as MM
import qualified Data.Macaw.Types as M
import qualified Data.Macaw.SemMC.Generator as G
@ -42,6 +44,10 @@ import Data.Macaw.SemMC.TH ( natReprTH, addEltTH, symFnName, asName )
import Data.Macaw.PPC.Arch
import Data.Macaw.PPC.PPCReg
getOpName :: S.Elt t x -> Maybe String
getOpName (S.NonceAppElt nae) = Just $ show $ S.nonceEltId nae
getOpName _ = Nothing
ppcNonceAppEval :: forall arch t tp
. (A.Architecture arch,
L.Location arch ~ APPC.Location arch,
@ -55,6 +61,39 @@ ppcNonceAppEval bvi nonceApp =
S.FnApp symFn args -> do
let fnName = symFnName symFn
case fnName of
"ppc_vec1" -> return $ do
case FC.toListFC Some args of
[Some op, Some rA, Some vscr] -> do
case getOpName op of
Just name -> do
valA <- addEltTH bvi rA
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
"ppc_vec2" -> return $ do
case FC.toListFC Some args of
[Some op, Some rA, Some rB, Some vscr] -> do
case getOpName op of
Just name -> do
valA <- addEltTH bvi rA
valB <- addEltTH bvi rB
valVscr <- addEltTH bvi vscr
liftQ [| addArchExpr $ Vec2 $(lift name) $(return valA) $(return valB) $(return valVscr) |]
Nothing -> fail $ "Invalid argument list for ppc.vec2: " ++ showF args
_ -> fail $ "Invalid argument list for ppc.vec2: " ++ showF args
"ppc_vec3" -> return $ do
case FC.toListFC Some args of
[Some op, Some rA, Some rB, Some rC, Some vscr] -> do
case getOpName op of
Just name -> do
valA <- addEltTH bvi rA
valB <- addEltTH bvi rB
valC <- addEltTH bvi rC
valVscr <- addEltTH bvi vscr
liftQ [| addArchExpr $ Vec3 $(lift name) $(return valA) $(return valB) $(return valC) $(return valVscr) |]
Nothing -> fail $ "Invalid argument list for ppc.vec3: " ++ showF args
_ -> fail $ "Invalid argument list for ppc.vec3: " ++ showF args
"ppc_is_r0" -> return $ do
case FC.toListFC Some args of
[Some operand] -> do
@ -87,6 +126,20 @@ ppcNonceAppEval bvi nonceApp =
elementaryFPName :: String -> Maybe String
elementaryFPName = L.stripPrefix "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))
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))
floatingPointTH :: forall arch t f c
. (L.Location arch ~ APPC.Location arch,
A.Architecture arch,
@ -103,74 +156,74 @@ floatingPointTH bvi fnName args =
case fnName of
"round_single" -> do
fpval <- addEltTH bvi a
liftQ [| G.addExpr (G.AppExpr (M.FPCvt M.DoubleFloatRepr $(return fpval) M.SingleFloatRepr)) |]
liftQ [| addArchExpr (FPCvt M.DoubleFloatRepr $(return fpval) M.SingleFloatRepr) |]
"single_to_double" -> do
fpval <- addEltTH bvi a
liftQ [| G.addExpr (G.AppExpr (M.FPCvt M.SingleFloatRepr $(return fpval) M.DoubleFloatRepr)) |]
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 [| G.addExpr (G.AppExpr (M.FPAbs M.DoubleFloatRepr $(return fpval))) |]
liftQ [| addArchExpr (FPAbs M.DoubleFloatRepr $(return fpval)) |]
"negate64" -> do
fpval <- addEltTH bvi a
liftQ [| G.addExpr (G.AppExpr (M.FPNeg M.DoubleFloatRepr $(return fpval))) |]
liftQ [| addArchExpr (FPNeg M.DoubleFloatRepr $(return fpval)) |]
"negate32" -> do
fpval <- addEltTH bvi a
liftQ [| G.addExpr (G.AppExpr (M.FPNeg M.SingleFloatRepr $(return fpval))) |]
liftQ [| addArchExpr (FPNeg M.SingleFloatRepr $(return fpval)) |]
"is_qnan32" -> do
fpval <- addEltTH bvi a
liftQ [| G.addExpr (G.AppExpr (M.FPIsQNaN M.SingleFloatRepr $(return fpval))) |]
liftQ [| addArchExpr (FPIsQNaN M.SingleFloatRepr $(return fpval)) |]
"is_qnan64" -> do
fpval <- addEltTH bvi a
liftQ [| G.addExpr (G.AppExpr (M.FPIsQNaN M.DoubleFloatRepr $(return fpval))) |]
liftQ [| addArchExpr (FPIsQNaN M.DoubleFloatRepr $(return fpval)) |]
"is_snan32" -> do
fpval <- addEltTH bvi a
liftQ [| G.addExpr (G.AppExpr (M.FPIsSNaN M.SingleFloatRepr $(return fpval))) |]
liftQ [| addArchExpr (FPIsSNaN M.SingleFloatRepr $(return fpval)) |]
"is_snan64" -> do
fpval <- addEltTH bvi a
liftQ [| G.addExpr (G.AppExpr (M.FPIsSNaN M.DoubleFloatRepr $(return fpval))) |]
liftQ [| addArchExpr (FPIsSNaN M.DoubleFloatRepr $(return fpval)) |]
_ -> 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 [| G.addExpr (G.AppExpr (M.FPAdd M.DoubleFloatRepr $(return valA) $(return valB))) |]
liftQ [| addArchExpr (FPAdd M.DoubleFloatRepr $(return valA) $(return valB)) |]
"add32" -> do
valA <- addEltTH bvi a
valB <- addEltTH bvi b
liftQ [| G.addExpr (G.AppExpr (M.FPAdd M.SingleFloatRepr $(return valA) $(return valB))) |]
liftQ [| addArchExpr (FPAdd M.SingleFloatRepr $(return valA) $(return valB)) |]
"sub64" -> do
valA <- addEltTH bvi a
valB <- addEltTH bvi b
liftQ [| G.addExpr (G.AppExpr (M.FPSub M.DoubleFloatRepr $(return valA) $(return valB))) |]
liftQ [| addArchExpr (FPSub M.DoubleFloatRepr $(return valA) $(return valB)) |]
"sub32" -> do
valA <- addEltTH bvi a
valB <- addEltTH bvi b
liftQ [| G.addExpr (G.AppExpr (M.FPSub M.SingleFloatRepr $(return valA) $(return valB))) |]
liftQ [| addArchExpr (FPSub M.SingleFloatRepr $(return valA) $(return valB)) |]
"mul64" -> do
valA <- addEltTH bvi a
valB <- addEltTH bvi b
liftQ [| G.addExpr (G.AppExpr (M.FPMul M.DoubleFloatRepr $(return valA) $(return valB))) |]
liftQ [| addArchExpr (FPMul M.DoubleFloatRepr $(return valA) $(return valB)) |]
"mul32" -> do
valA <- addEltTH bvi a
valB <- addEltTH bvi b
liftQ [| G.addExpr (G.AppExpr (M.FPMul M.SingleFloatRepr $(return valA) $(return valB))) |]
liftQ [| addArchExpr (FPMul M.SingleFloatRepr $(return valA) $(return valB)) |]
"div64" -> do
valA <- addEltTH bvi a
valB <- addEltTH bvi b
liftQ [| G.addExpr (G.AppExpr (M.FPDiv M.DoubleFloatRepr $(return valA) $(return valB))) |]
liftQ [| addArchExpr (FPDiv M.DoubleFloatRepr $(return valA) $(return valB)) |]
"div32" -> do
valA <- addEltTH bvi a
valB <- addEltTH bvi b
liftQ [| G.addExpr (G.AppExpr (M.FPDiv M.SingleFloatRepr $(return valA) $(return valB))) |]
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 [| G.addExpr (G.AppExpr (M.FPLt M.DoubleFloatRepr $(return valA) $(return valB))) |]
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
@ -180,16 +233,16 @@ floatingPointTH bvi fnName args =
valA <- addEltTH bvi a
valB <- addEltTH bvi b
valC <- addEltTH bvi c
liftQ [| do prodVal <- G.addExpr (G.AppExpr (M.FPMul M.DoubleFloatRepr $(return valA) $(return valC)))
G.addExpr (G.AppExpr (M.FPAdd M.DoubleFloatRepr prodVal $(return valB)))
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 <- G.addExpr (G.AppExpr (M.FPMul M.SingleFloatRepr $(return valA) $(return valC)))
G.addExpr (G.AppExpr (M.FPAdd M.SingleFloatRepr prodVal $(return valB)))
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)
@ -205,13 +258,11 @@ ppcAppEvaluator interps elt = case elt of
S.BVSdiv w bv1 bv2 -> return $ do
e1 <- addEltTH interps bv1
e2 <- addEltTH interps bv2
liftQ [| let divExp = SDiv $(natReprTH w) $(return e1) $(return e2)
in (G.ValueExpr . M.AssignedValue) <$> G.addAssignment (M.EvalArchFn divExp (M.typeRepr divExp))
liftQ [| addArchAssignment (SDiv $(natReprTH w) $(return e1) $(return e2))
|]
S.BVUdiv w bv1 bv2 -> return $ do
e1 <- addEltTH interps bv1
e2 <- addEltTH interps bv2
liftQ [| let divExp = UDiv $(natReprTH w) $(return e1) $(return e2)
in (G.ValueExpr . M.AssignedValue) <$> G.addAssignment (M.EvalArchFn divExp (M.typeRepr divExp))
liftQ [| addArchAssignment (UDiv $(natReprTH w) $(return e1) $(return e2))
|]
_ -> Nothing

8
macaw-ppc/tests/Shared.hs
View File

@ -44,10 +44,14 @@ withMemory :: forall w m a
-> (MM.Memory w -> m a)
-> m a
withMemory _ e k =
case MM.memoryForElf (MM.LoadOptions MM.LoadBySegment False) e of
-- case MM.memoryForElfSegments relaWidth e of
case MM.memoryForElf loadCfg e of
Left err -> C.throwM (MemoryLoadError err)
Right (_sim, mem) -> k mem
where
loadCfg = MM.LoadOptions { MM.loadStyle = MM.LoadBySegment
, MM.includeBSS = False
, MM.loadRegionIndex = 0
}
data ElfException = MemoryLoadError String
deriving (Typeable, Show)

2
macaw-semmc/src/Data/Macaw/SemMC/Generator.hs
View File

@ -261,7 +261,7 @@ liftST = Generator . lift . lift . lift
-- | Append an assignment statement to the list of statements in the current
-- 'PreBlock'
addAssignment :: AssignRhs arch ids tp
addAssignment :: AssignRhs arch (Value arch ids) tp
-> Generator arch ids s (Assignment arch ids tp)
addAssignment rhs = do
l <- newAssignId

2
submodules/crucible

@ -1 +1 @@
Subproject commit d91a62996c5d4b5fd597f381c89488aa6e6f6319
Subproject commit 1f580c71e05efbcd79828430234964829edebab5

2
submodules/dismantle

@ -1 +1 @@
Subproject commit 5bdb5146417b6d9739d3831413617a69b22d8e65
Subproject commit 183e26883166a865e3d07de881a6971ba25c5cf8

2
submodules/elf-edit

@ -1 +1 @@
Subproject commit 41f560ff320b96a6b90c4015b9c27821367eb1a1
Subproject commit 7fa0f79455e98bb298458632048f497757ddde02

2
submodules/macaw

@ -1 +1 @@
Subproject commit d26b7f47a3ca168e8d266ebd7b82be52dd47a936
Subproject commit eebc94cbe808e3b0ecfb036990a242b33a13658b

2
submodules/parameterized-utils

@ -1 +1 @@
Subproject commit e1b2c3f6b1f86b38336777fafa01e0dccd444616
Subproject commit 7c76b811a321a548af7d4fcf46390daf979f39b1

2
submodules/semmc

@ -1 +1 @@
Subproject commit 8cc92d942079031bb4436e9340bac1a64809e603
Subproject commit de3cef59472041fbfd69494978a8de28716d3f5f