From 2247747bef73b938526c0dab76c8f0e9a1dd7241 Mon Sep 17 00:00:00 2001 From: Tristan Ravitch Date: Tue, 2 Jan 2018 18:17:32 -0800 Subject: [PATCH 01/12] Update submodules to the latest macaw (and others) Macaw has removed all floating point expression types, so we duplicate those as arch-specific functions for PowerPC until the more general floating point support is ready. --- macaw-ppc/src/Data/Macaw/PPC.hs | 2 +- macaw-ppc/src/Data/Macaw/PPC/Arch.hs | 143 +++++++++++++++++- macaw-ppc/src/Data/Macaw/PPC/Eval.hs | 17 +++ macaw-ppc/src/Data/Macaw/PPC/Semantics/TH.hs | 65 ++++---- macaw-ppc/tests/Shared.hs | 8 +- macaw-semmc/src/Data/Macaw/SemMC/Generator.hs | 2 +- submodules/crucible | 2 +- submodules/dismantle | 2 +- submodules/elf-edit | 2 +- submodules/macaw | 2 +- submodules/parameterized-utils | 2 +- submodules/semmc | 2 +- 12 files changed, 211 insertions(+), 38 deletions(-) diff --git a/macaw-ppc/src/Data/Macaw/PPC.hs b/macaw-ppc/src/Data/Macaw/PPC.hs index 668887a8..de05910e 100644 --- a/macaw-ppc/src/Data/Macaw/PPC.hs +++ b/macaw-ppc/src/Data/Macaw/PPC.hs @@ -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 diff --git a/macaw-ppc/src/Data/Macaw/PPC/Arch.hs b/macaw-ppc/src/Data/Macaw/PPC/Arch.hs index f18e4369..503ac7f6 100644 --- a/macaw-ppc/src/Data/Macaw/PPC/Arch.hs +++ b/macaw-ppc/src/Data/Macaw/PPC/Arch.hs @@ -144,12 +144,46 @@ 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) instance (1 <= MC.RegAddrWidth (MC.ArchReg ppc)) => MT.HasRepr (PPCPrimFn ppc (MC.Value ppc ids)) MT.TypeRepr where typeRepr f = case f of 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 -- | Right now, none of the primitive functions has a side effect. That will -- probably change. @@ -158,6 +192,23 @@ 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 rewritePrimFn :: (PPCArchConstraints ppc, MC.ArchFn ppc ~ PPCPrimFn ppc) => PPCPrimFn ppc (MC.Value ppc src) tp @@ -170,12 +221,83 @@ 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 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 + where + ppUnary s v' = PP.text s PP.<+> v' + ppBinary s v1' v2' = PP.text s PP.<+> v1' PP.<+> v2' instance MC.IsArchFn (PPCPrimFn ppc) where ppArchFn = ppPrimFn @@ -191,6 +313,23 @@ 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 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 fa04f4a5..e34c0561 100644 --- a/macaw-ppc/src/Data/Macaw/PPC/Eval.hs +++ b/macaw-ppc/src/Data/Macaw/PPC/Eval.hs @@ -98,6 +98,23 @@ 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 -- | 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 67daa2a1..a71805da 100644 --- a/macaw-ppc/src/Data/Macaw/PPC/Semantics/TH.hs +++ b/macaw-ppc/src/Data/Macaw/PPC/Semantics/TH.hs @@ -32,6 +32,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 @@ -87,6 +88,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 +118,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 +195,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 +220,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 diff --git a/macaw-ppc/tests/Shared.hs b/macaw-ppc/tests/Shared.hs index 3b08437f..17004286 100644 --- a/macaw-ppc/tests/Shared.hs +++ b/macaw-ppc/tests/Shared.hs @@ -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) diff --git a/macaw-semmc/src/Data/Macaw/SemMC/Generator.hs b/macaw-semmc/src/Data/Macaw/SemMC/Generator.hs index 5017e57c..6ae8829e 100644 --- a/macaw-semmc/src/Data/Macaw/SemMC/Generator.hs +++ b/macaw-semmc/src/Data/Macaw/SemMC/Generator.hs @@ -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 diff --git a/submodules/crucible b/submodules/crucible index d91a6299..b8c1f10b 160000 --- a/submodules/crucible +++ b/submodules/crucible @@ -1 +1 @@ -Subproject commit d91a62996c5d4b5fd597f381c89488aa6e6f6319 +Subproject commit b8c1f10bcb36d772d09799b0362442baae317807 diff --git a/submodules/dismantle b/submodules/dismantle index 5bdb5146..7f9c3121 160000 --- a/submodules/dismantle +++ b/submodules/dismantle @@ -1 +1 @@ -Subproject commit 5bdb5146417b6d9739d3831413617a69b22d8e65 +Subproject commit 7f9c312108e804e7cbb198aa6c28f538988417ad diff --git a/submodules/elf-edit b/submodules/elf-edit index 41f560ff..deadece3 160000 --- a/submodules/elf-edit +++ b/submodules/elf-edit @@ -1 +1 @@ -Subproject commit 41f560ff320b96a6b90c4015b9c27821367eb1a1 +Subproject commit deadece3c094d49d79f17604efd94fb9569ea2e4 diff --git a/submodules/macaw b/submodules/macaw index d26b7f47..deab9986 160000 --- a/submodules/macaw +++ b/submodules/macaw @@ -1 +1 @@ -Subproject commit d26b7f47a3ca168e8d266ebd7b82be52dd47a936 +Subproject commit deab99869d5a271ce4a96e76b9e0966b4c7f99e5 diff --git a/submodules/parameterized-utils b/submodules/parameterized-utils index e1b2c3f6..d33884a5 160000 --- a/submodules/parameterized-utils +++ b/submodules/parameterized-utils @@ -1 +1 @@ -Subproject commit e1b2c3f6b1f86b38336777fafa01e0dccd444616 +Subproject commit d33884a5199970fdb52374db24c3517eb34b5b1c diff --git a/submodules/semmc b/submodules/semmc index 8cc92d94..1916d2ac 160000 --- a/submodules/semmc +++ b/submodules/semmc @@ -1 +1 @@ -Subproject commit 8cc92d942079031bb4436e9340bac1a64809e603 +Subproject commit 1916d2ac4038fb9ed4ec59a66f508fa165738810 From d95b1f6b3febf24f7eee79c1900c276bc54edfd2 Mon Sep 17 00:00:00 2001 From: Ben Selfridge Date: Fri, 5 Jan 2018 13:27:53 -0800 Subject: [PATCH 02/12] Updated macaw-ppc code to handle VecN PPCPrimFns. --- macaw-ppc/src/Data/Macaw/PPC/Arch.hs | 74 ++++++++++++++++++-- macaw-ppc/src/Data/Macaw/PPC/Eval.hs | 3 + macaw-ppc/src/Data/Macaw/PPC/Semantics/TH.hs | 47 +++++++++++++ 3 files changed, 117 insertions(+), 7 deletions(-) diff --git a/macaw-ppc/src/Data/Macaw/PPC/Arch.hs b/macaw-ppc/src/Data/Macaw/PPC/Arch.hs index f18e4369..6003408d 100644 --- a/macaw-ppc/src/Data/Macaw/PPC/Arch.hs +++ b/macaw-ppc/src/Data/Macaw/PPC/Arch.hs @@ -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 @@ -145,11 +145,32 @@ data PPCPrimFn ppc f tp where -> f (MT.BVType (MC.RegAddrWidth (MC.ArchReg ppc))) -> PPCPrimFn ppc f (MT.BVType (MC.RegAddrWidth (MC.ArchReg ppc))) + -- | 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 = case f of UDiv rep _ _ -> MT.BVTypeRepr rep SDiv rep _ _ -> MT.BVTypeRepr 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. @@ -158,6 +179,9 @@ ppcPrimFnHasSideEffects pf = case pf of UDiv {} -> False SDiv {} -> False + Vec1 {} -> False + Vec2 {} -> False + Vec3 {} -> False rewritePrimFn :: (PPCArchConstraints ppc, MC.ArchFn ppc ~ PPCPrimFn ppc) => PPCPrimFn ppc (MC.Value ppc src) tp @@ -170,12 +194,45 @@ rewritePrimFn f = SDiv rep lhs rhs -> do tgtFn <- SDiv rep <$> rewriteValue lhs <*> rewriteValue rhs evalRewrittenArchFn tgtFn + Vec1 name op fpscr -> do + tgtFn <- Vec1 name <$> rewriteValue op <*> rewriteValue fpscr + evalRewrittenArchFn tgtFn + Vec2 name op1 op2 fpscr -> do + tgtFn <- Vec2 name <$> rewriteValue op1 <*> rewriteValue op2 <*> rewriteValue fpscr + evalRewrittenArchFn tgtFn + Vec3 name op1 op2 op3 fpscr -> do + tgtFn <- Vec3 name <$> rewriteValue op1 <*> rewriteValue op2 <*> rewriteValue op3 <*> rewriteValue fpscr + 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 + Vec1 n r1 fpscr -> + (\r1' fpscr' + -> PP.text "ppc_vec1 " PP.<> + PP.text n PP.<> PP.text " " PP.<> + r1' PP.<> PP.text " " PP.<> + fpscr') <$> + pp r1 <*> pp fpscr + Vec2 n r1 r2 fpscr -> + (\r1' r2' fpscr' -> + PP.text "ppc_vec1 " PP.<> + PP.text n PP.<> PP.text " " PP.<> + r1' PP.<> PP.text " " PP.<> + r2' PP.<> PP.text " " PP.<> + fpscr') <$> + pp r1 <*> pp r2 <*> pp fpscr + Vec3 n r1 r2 r3 fpscr -> + (\r1' r2' r3' fpscr' -> + PP.text "ppc_vec1 " PP.<> + PP.text n PP.<> PP.text " " PP.<> + r1' PP.<> PP.text " " PP.<> + r2' PP.<> PP.text " " PP.<> + r3' PP.<> PP.text " " PP.<> + fpscr') <$> + pp r1 <*> pp r2 <*> pp r3 <*> pp fpscr instance MC.IsArchFn (PPCPrimFn ppc) where ppArchFn = ppPrimFn @@ -191,6 +248,9 @@ 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 + Vec1 name op fpscr -> Vec1 name <$> go op <*> go fpscr + Vec2 name op1 op2 fpscr -> Vec2 name <$> go op1 <*> go op2 <*> go fpscr + Vec3 name op1 op2 op3 fpscr -> Vec3 name <$> go op1 <*> go op2 <*> go op3 <*> go fpscr 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 fa04f4a5..89bce5bb 100644 --- a/macaw-ppc/src/Data/Macaw/PPC/Eval.hs +++ b/macaw-ppc/src/Data/Macaw/PPC/Eval.hs @@ -98,6 +98,9 @@ absEvalArchFn _ _r f = case f of SDiv {} -> MA.TopV UDiv {} -> 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 67daa2a1..e52f1556 100644 --- a/macaw-ppc/src/Data/Macaw/PPC/Semantics/TH.hs +++ b/macaw-ppc/src/Data/Macaw/PPC/Semantics/TH.hs @@ -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 @@ -42,6 +43,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 +60,48 @@ 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 fpscr] -> do + case getOpName op of + Just name -> do + valA <- addEltTH bvi rA + valFpscr <- addEltTH bvi fpscr + liftQ [| do let vecFn = Vec1 $(lift name) $(return valA) $(return valFpscr) + vecExp <- G.addAssignment $ M.EvalArchFn vecFn (M.typeRepr vecFn) + return (M.AssignedValue vecExp) + |] + 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 fpscr] -> do + case getOpName op of + Just name -> do + valA <- addEltTH bvi rA + valB <- addEltTH bvi rB + valFpscr <- addEltTH bvi fpscr + liftQ [| do let vecFn = Vec2 $(lift name) $(return valA) $(return valB) $(return valFpscr) + vecExp <- G.addAssignment $ M.EvalArchFn vecFn (M.typeRepr vecFn) + return (M.AssignedValue vecExp) + |] + 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 fpscr] -> do + case getOpName op of + Just name -> do + valA <- addEltTH bvi rA + valB <- addEltTH bvi rB + valC <- addEltTH bvi rC + valFpscr <- addEltTH bvi fpscr + liftQ [| do let vecFn = Vec3 $(lift name) $(return valA) $(return valB) $(return valC) $(return valFpscr) + vecExp <- G.addAssignment $ M.EvalArchFn vecFn (M.typeRepr vecFn) + return (M.AssignedValue vecExp) + |] + 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 From d3f72ee39e1ee47f99b3b614ececccc6ad3b328e Mon Sep 17 00:00:00 2001 From: Ben Selfridge Date: Fri, 5 Jan 2018 13:30:12 -0800 Subject: [PATCH 03/12] Set semmc version to new. --- submodules/semmc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/submodules/semmc b/submodules/semmc index 8cc92d94..04c3ba3f 160000 --- a/submodules/semmc +++ b/submodules/semmc @@ -1 +1 @@ -Subproject commit 8cc92d942079031bb4436e9340bac1a64809e603 +Subproject commit 04c3ba3f93c0774d1133767a48ccc5f0efa660b8 From 5cf4c68498b92d93f3ced14ff6620a7c4ad8ec3e Mon Sep 17 00:00:00 2001 From: Ben Selfridge Date: Fri, 5 Jan 2018 14:23:11 -0800 Subject: [PATCH 04/12] Fixed a bug I introduced because of a delete in the wrong buffer --- macaw-semmc/src/Data/Macaw/SemMC/Generator.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/macaw-semmc/src/Data/Macaw/SemMC/Generator.hs b/macaw-semmc/src/Data/Macaw/SemMC/Generator.hs index 5017e57c..6ae8829e 100644 --- a/macaw-semmc/src/Data/Macaw/SemMC/Generator.hs +++ b/macaw-semmc/src/Data/Macaw/SemMC/Generator.hs @@ -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 From 63c2fec79b3d9e4cf80faf35ad73fa4d44836159 Mon Sep 17 00:00:00 2001 From: Ben Selfridge Date: Fri, 5 Jan 2018 14:58:15 -0800 Subject: [PATCH 05/12] Simplified code using addArchExpr. --- macaw-ppc/src/Data/Macaw/PPC/Semantics/TH.hs | 15 +++------------ 1 file changed, 3 insertions(+), 12 deletions(-) diff --git a/macaw-ppc/src/Data/Macaw/PPC/Semantics/TH.hs b/macaw-ppc/src/Data/Macaw/PPC/Semantics/TH.hs index 0a50418f..a3620f3c 100644 --- a/macaw-ppc/src/Data/Macaw/PPC/Semantics/TH.hs +++ b/macaw-ppc/src/Data/Macaw/PPC/Semantics/TH.hs @@ -68,10 +68,7 @@ ppcNonceAppEval bvi nonceApp = Just name -> do valA <- addEltTH bvi rA valFpscr <- addEltTH bvi fpscr - liftQ [| do let vecFn = Vec1 $(lift name) $(return valA) $(return valFpscr) - vecExp <- G.addAssignment $ M.EvalArchFn vecFn (M.typeRepr vecFn) - return (M.AssignedValue vecExp) - |] + liftQ [| addArchExpr $ Vec1 $(lift name) $(return valA) $(return valFpscr) |] Nothing -> fail $ "Invalid argument list for ppc.vec1: " ++ showF args _ -> fail $ "Invalid argument list for ppc.vec2: " ++ showF args "ppc_vec2" -> return $ do @@ -82,10 +79,7 @@ ppcNonceAppEval bvi nonceApp = valA <- addEltTH bvi rA valB <- addEltTH bvi rB valFpscr <- addEltTH bvi fpscr - liftQ [| do let vecFn = Vec2 $(lift name) $(return valA) $(return valB) $(return valFpscr) - vecExp <- G.addAssignment $ M.EvalArchFn vecFn (M.typeRepr vecFn) - return (M.AssignedValue vecExp) - |] + liftQ [| addArchExpr $ Vec2 $(lift name) $(return valA) $(return valB) $(return valFpscr) |] Nothing -> fail $ "Invalid argument list for ppc.vec2: " ++ showF args _ -> fail $ "Invalid argument list for ppc.vec2: " ++ showF args "ppc_vec3" -> return $ do @@ -97,10 +91,7 @@ ppcNonceAppEval bvi nonceApp = valB <- addEltTH bvi rB valC <- addEltTH bvi rC valFpscr <- addEltTH bvi fpscr - liftQ [| do let vecFn = Vec3 $(lift name) $(return valA) $(return valB) $(return valC) $(return valFpscr) - vecExp <- G.addAssignment $ M.EvalArchFn vecFn (M.typeRepr vecFn) - return (M.AssignedValue vecExp) - |] + liftQ [| addArchExpr $ Vec3 $(lift name) $(return valA) $(return valB) $(return valC) $(return valFpscr) |] Nothing -> fail $ "Invalid argument list for ppc.vec3: " ++ showF args _ -> fail $ "Invalid argument list for ppc.vec3: " ++ showF args "ppc_is_r0" -> return $ do From 77129fbe3e9005f75dda282e12ec77696429e044 Mon Sep 17 00:00:00 2001 From: Tristan Ravitch Date: Mon, 8 Jan 2018 11:57:41 -0800 Subject: [PATCH 06/12] Update the semmc submodule --- submodules/dismantle | 2 +- submodules/semmc | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/submodules/dismantle b/submodules/dismantle index 7f9c3121..484958a7 160000 --- a/submodules/dismantle +++ b/submodules/dismantle @@ -1 +1 @@ -Subproject commit 7f9c312108e804e7cbb198aa6c28f538988417ad +Subproject commit 484958a79006e5e374f56e56d1e1369d3cecaa56 diff --git a/submodules/semmc b/submodules/semmc index 04c3ba3f..e9d37639 160000 --- a/submodules/semmc +++ b/submodules/semmc @@ -1 +1 @@ -Subproject commit 04c3ba3f93c0774d1133767a48ccc5f0efa660b8 +Subproject commit e9d376390a0e5cc602a84e854f2e74aa573c16d3 From f256869311671245353e745361b0333a2cea9c0c Mon Sep 17 00:00:00 2001 From: Tristan Ravitch Date: Mon, 8 Jan 2018 15:32:25 -0800 Subject: [PATCH 07/12] Update crucible and parameterized-utils --- submodules/crucible | 2 +- submodules/parameterized-utils | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/submodules/crucible b/submodules/crucible index b8c1f10b..31406acd 160000 --- a/submodules/crucible +++ b/submodules/crucible @@ -1 +1 @@ -Subproject commit b8c1f10bcb36d772d09799b0362442baae317807 +Subproject commit 31406acd6f15eb6d9a10fddeab8a45afcb163430 diff --git a/submodules/parameterized-utils b/submodules/parameterized-utils index d33884a5..7c76b811 160000 --- a/submodules/parameterized-utils +++ b/submodules/parameterized-utils @@ -1 +1 @@ -Subproject commit d33884a5199970fdb52374db24c3517eb34b5b1c +Subproject commit 7c76b811a321a548af7d4fcf46390daf979f39b1 From f6face9136c7fb2ebc867c61fb70192b1f2ea1d2 Mon Sep 17 00:00:00 2001 From: Ben Selfridge Date: Mon, 8 Jan 2018 17:56:00 -0800 Subject: [PATCH 08/12] Added VSCR for vector semantics --- macaw-ppc/src/Data/Macaw/PPC/Arch.hs | 24 ++++++++++---------- macaw-ppc/src/Data/Macaw/PPC/PPCReg.hs | 6 ++++- macaw-ppc/src/Data/Macaw/PPC/Semantics/TH.hs | 18 +++++++-------- 3 files changed, 26 insertions(+), 22 deletions(-) diff --git a/macaw-ppc/src/Data/Macaw/PPC/Arch.hs b/macaw-ppc/src/Data/Macaw/PPC/Arch.hs index 5e20ae2e..206e71fe 100644 --- a/macaw-ppc/src/Data/Macaw/PPC/Arch.hs +++ b/macaw-ppc/src/Data/Macaw/PPC/Arch.hs @@ -299,14 +299,14 @@ rewritePrimFn f = FPNeg rep v -> do tgt <- FPNeg rep <$> rewriteValue v evalRewrittenArchFn tgt - Vec1 name op fpscr -> do - tgtFn <- Vec1 name <$> rewriteValue op <*> rewriteValue fpscr + Vec1 name op vscr -> do + tgtFn <- Vec1 name <$> rewriteValue op <*> rewriteValue vscr evalRewrittenArchFn tgtFn - Vec2 name op1 op2 fpscr -> do - tgtFn <- Vec2 name <$> rewriteValue op1 <*> rewriteValue op2 <*> rewriteValue fpscr + Vec2 name op1 op2 vscr -> do + tgtFn <- Vec2 name <$> rewriteValue op1 <*> rewriteValue op2 <*> rewriteValue vscr evalRewrittenArchFn tgtFn - Vec3 name op1 op2 op3 fpscr -> do - tgtFn <- Vec3 name <$> rewriteValue op1 <*> rewriteValue op2 <*> rewriteValue op3 <*> rewriteValue fpscr + 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 @@ -331,9 +331,9 @@ ppPrimFn pp f = 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 fpscr -> ppBinary ("ppc_vec1 " ++ n) <$> pp r1 <*> pp fpscr - Vec2 n r1 r2 fpscr -> pp3 ("ppc_vec2" ++ n) <$> pp r1 <*> pp r2 <*> pp fpscr - Vec3 n r1 r2 r3 fpscr -> pp4 ("ppc_vec3" ++ 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' @@ -371,9 +371,9 @@ instance FC.TraversableFC (PPCPrimFn ppc) where 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 fpscr -> Vec1 name <$> go op <*> go fpscr - Vec2 name op1 op2 fpscr -> Vec2 name <$> go op1 <*> go op2 <*> go fpscr - Vec3 name op1 op2 op3 fpscr -> Vec3 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/PPCReg.hs b/macaw-ppc/src/Data/Macaw/PPC/PPCReg.hs index de8fee5f..8d277a15 100644 --- a/macaw-ppc/src/Data/Macaw/PPC/PPCReg.hs +++ b/macaw-ppc/src/Data/Macaw/PPC/PPCReg.hs @@ -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 |] diff --git a/macaw-ppc/src/Data/Macaw/PPC/Semantics/TH.hs b/macaw-ppc/src/Data/Macaw/PPC/Semantics/TH.hs index a3620f3c..29f3cefc 100644 --- a/macaw-ppc/src/Data/Macaw/PPC/Semantics/TH.hs +++ b/macaw-ppc/src/Data/Macaw/PPC/Semantics/TH.hs @@ -63,35 +63,35 @@ ppcNonceAppEval bvi nonceApp = case fnName of "ppc_vec1" -> return $ do case FC.toListFC Some args of - [Some op, Some rA, Some fpscr] -> do + [Some op, Some rA, Some vscr] -> do case getOpName op of Just name -> do valA <- addEltTH bvi rA - valFpscr <- addEltTH bvi fpscr - liftQ [| addArchExpr $ Vec1 $(lift name) $(return valA) $(return valFpscr) |] + 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 fpscr] -> do + [Some op, Some rA, Some rB, Some vscr] -> do case getOpName op of Just name -> do valA <- addEltTH bvi rA valB <- addEltTH bvi rB - valFpscr <- addEltTH bvi fpscr - liftQ [| addArchExpr $ Vec2 $(lift name) $(return valA) $(return valB) $(return valFpscr) |] + 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 fpscr] -> do + [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 - valFpscr <- addEltTH bvi fpscr - liftQ [| addArchExpr $ Vec3 $(lift name) $(return valA) $(return valB) $(return valC) $(return valFpscr) |] + 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 From dc5659dc14cc4f6f514760f94fc6ded822b9031b Mon Sep 17 00:00:00 2001 From: Ben Selfridge Date: Tue, 9 Jan 2018 11:37:17 -0800 Subject: [PATCH 09/12] updated semmc --- submodules/semmc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/submodules/semmc b/submodules/semmc index e9d37639..00b27241 160000 --- a/submodules/semmc +++ b/submodules/semmc @@ -1 +1 @@ -Subproject commit e9d376390a0e5cc602a84e854f2e74aa573c16d3 +Subproject commit 00b27241afc843681972a01eef869a716186211b From 6780e14c81bf848e76c20d5d0583ca122f55d229 Mon Sep 17 00:00:00 2001 From: Ben Selfridge Date: Tue, 9 Jan 2018 11:45:08 -0800 Subject: [PATCH 10/12] merging to newest semmc --- submodules/semmc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/submodules/semmc b/submodules/semmc index 00b27241..559d91ac 160000 --- a/submodules/semmc +++ b/submodules/semmc @@ -1 +1 @@ -Subproject commit 00b27241afc843681972a01eef869a716186211b +Subproject commit 559d91ac04db853487f415d52279b7214d73e5e3 From 69087e88355c9ed0fc302598240e6683d67e195a Mon Sep 17 00:00:00 2001 From: Ben Selfridge Date: Tue, 9 Jan 2018 14:02:51 -0800 Subject: [PATCH 11/12] update semmc --- submodules/semmc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/submodules/semmc b/submodules/semmc index 559d91ac..de3cef59 160000 --- a/submodules/semmc +++ b/submodules/semmc @@ -1 +1 @@ -Subproject commit 559d91ac04db853487f415d52279b7214d73e5e3 +Subproject commit de3cef59472041fbfd69494978a8de28716d3f5f From 2c1a2e9b97878e3fc1796f1ca99a835f1b64f7c2 Mon Sep 17 00:00:00 2001 From: Tristan Ravitch Date: Tue, 9 Jan 2018 16:54:56 -0800 Subject: [PATCH 12/12] Submodule updates --- submodules/crucible | 2 +- submodules/dismantle | 2 +- submodules/elf-edit | 2 +- submodules/macaw | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) diff --git a/submodules/crucible b/submodules/crucible index 31406acd..1f580c71 160000 --- a/submodules/crucible +++ b/submodules/crucible @@ -1 +1 @@ -Subproject commit 31406acd6f15eb6d9a10fddeab8a45afcb163430 +Subproject commit 1f580c71e05efbcd79828430234964829edebab5 diff --git a/submodules/dismantle b/submodules/dismantle index 484958a7..183e2688 160000 --- a/submodules/dismantle +++ b/submodules/dismantle @@ -1 +1 @@ -Subproject commit 484958a79006e5e374f56e56d1e1369d3cecaa56 +Subproject commit 183e26883166a865e3d07de881a6971ba25c5cf8 diff --git a/submodules/elf-edit b/submodules/elf-edit index deadece3..7fa0f794 160000 --- a/submodules/elf-edit +++ b/submodules/elf-edit @@ -1 +1 @@ -Subproject commit deadece3c094d49d79f17604efd94fb9569ea2e4 +Subproject commit 7fa0f79455e98bb298458632048f497757ddde02 diff --git a/submodules/macaw b/submodules/macaw index deab9986..eebc94cb 160000 --- a/submodules/macaw +++ b/submodules/macaw @@ -1 +1 @@ -Subproject commit deab99869d5a271ce4a96e76b9e0966b4c7f99e5 +Subproject commit eebc94cbe808e3b0ecfb036990a242b33a13658b