diff --git a/.gitmodules b/.gitmodules index 972f01d6..856e6edb 100644 --- a/.gitmodules +++ b/.gitmodules @@ -19,3 +19,6 @@ [submodule "submodules/macaw"] path = submodules/macaw url = git@github.com:GaloisInc/macaw.git +[submodule "submodules/s-cargot"] + path = submodules/s-cargot + url = git@github.com:aisamanra/s-cargot.git diff --git a/macaw-ppc/src/Data/Macaw/PPC/Arch.hs b/macaw-ppc/src/Data/Macaw/PPC/Arch.hs index 206e71fe..f849bcc6 100644 --- a/macaw-ppc/src/Data/Macaw/PPC/Arch.hs +++ b/macaw-ppc/src/Data/Macaw/PPC/Arch.hs @@ -25,7 +25,9 @@ module Data.Macaw.PPC.Arch ( import GHC.TypeLits +import Control.Lens ( (^.) ) import qualified Text.PrettyPrint.ANSI.Leijen as PP +import Data.Parameterized.Classes ( knownRepr ) import qualified Data.Parameterized.NatRepr as NR import qualified Data.Parameterized.TraversableFC as FC import qualified Data.Parameterized.TraversableF as TF @@ -75,7 +77,7 @@ data PPCStmt ppc (v :: MT.Type -> *) where Attn :: PPCStmt ppc v Sync :: PPCStmt ppc v Isync :: PPCStmt ppc v - -- These are cache hints + -- These are data 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 @@ -84,6 +86,9 @@ data PPCStmt ppc (v :: MT.Type -> *) where 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 + -- Instruction cache hints + Icbi :: v (MT.BVType (MC.RegAddrWidth (MC.ArchReg ppc))) -> PPCStmt ppc v + Icbt :: v (MT.BVType (MC.RegAddrWidth (MC.ArchReg ppc))) -> v (MT.BVType 4) -> PPCStmt ppc v instance TF.FunctorF (PPCStmt ppc) where fmapF = TF.fmapFDefault @@ -105,6 +110,8 @@ instance TF.TraversableF (PPCStmt ppc) where Dcbzl ea -> Dcbzl <$> go ea Dcbt ea th -> Dcbt <$> go ea <*> go th Dcbtst ea th -> Dcbtst <$> go ea <*> go th + Icbi ea -> Icbi <$> go ea + Icbt ea ct -> Icbt <$> go ea <*> go ct instance MC.IsArchStmt (PPCStmt ppc) where ppArchStmt pp stmt = @@ -120,6 +127,8 @@ instance MC.IsArchStmt (PPCStmt ppc) where Dcbzl ea -> PP.text "ppc_dcbzl" PP.<+> pp ea Dcbt ea th -> PP.text "ppc_dcbt" PP.<+> pp ea PP.<+> pp th Dcbtst ea th -> PP.text "ppc_dcbtst" PP.<+> pp ea PP.<+> pp th + Icbi ea -> PP.text "ppc_icbi" PP.<+> pp ea + Icbt ea ct -> PP.text "ppc_icbt" PP.<+> pp ea PP.<+> pp ct type instance MC.ArchStmt PPC64.PPC = PPCStmt PPC64.PPC type instance MC.ArchStmt PPC32.PPC = PPCStmt PPC32.PPC @@ -144,39 +153,43 @@ data PPCPrimFn ppc f tp where -> f (MT.BVType (MC.RegAddrWidth (MC.ArchReg ppc))) -> f (MT.BVType (MC.RegAddrWidth (MC.ArchReg ppc))) -> PPCPrimFn ppc f (MT.BVType (MC.RegAddrWidth (MC.ArchReg ppc))) + FPIsQNaN :: !(MT.FloatInfoRepr flt) -> !(f (MT.FloatType flt)) -> PPCPrimFn ppc f MT.BoolType FPIsSNaN :: !(MT.FloatInfoRepr flt) -> !(f (MT.FloatType flt)) -> PPCPrimFn ppc f MT.BoolType - FPAdd :: !(MT.FloatInfoRepr flt) -> !(f (MT.FloatType flt)) -> !(f (MT.FloatType flt)) -> PPCPrimFn ppc f (MT.FloatType flt) - FPAddRoundedUp :: !(MT.FloatInfoRepr flt) -> !(f (MT.FloatType flt)) -> !(f (MT.FloatType flt)) -> PPCPrimFn ppc f MT.BoolType - FPSub :: !(MT.FloatInfoRepr flt) -> !(f (MT.FloatType flt)) -> !(f (MT.FloatType flt)) -> PPCPrimFn ppc f (MT.FloatType flt) - FPSubRoundedUp :: !(MT.FloatInfoRepr flt) -> !(f (MT.FloatType flt)) -> !(f (MT.FloatType flt)) -> PPCPrimFn ppc f MT.BoolType - FPMul :: !(MT.FloatInfoRepr flt) -> !(f (MT.FloatType flt)) -> !(f (MT.FloatType flt)) -> PPCPrimFn ppc f (MT.FloatType flt) - FPMulRoundedUp :: !(MT.FloatInfoRepr flt) -> !(f (MT.FloatType flt)) -> !(f (MT.FloatType flt)) -> PPCPrimFn ppc f MT.BoolType - FPDiv :: !(MT.FloatInfoRepr flt) -> !(f (MT.FloatType flt)) -> !(f (MT.FloatType flt)) -> PPCPrimFn ppc f (MT.FloatType flt) - FPLt :: !(MT.FloatInfoRepr flt) -> !(f (MT.FloatType flt)) -> !(f (MT.FloatType flt)) -> PPCPrimFn ppc f MT.BoolType - FPEq :: !(MT.FloatInfoRepr flt) -> !(f (MT.FloatType flt)) -> !(f (MT.FloatType flt)) -> PPCPrimFn ppc f MT.BoolType FPCvt :: !(MT.FloatInfoRepr flt) -> !(f (MT.FloatType flt)) -> !(MT.FloatInfoRepr flt') -> PPCPrimFn ppc f (MT.FloatType flt') - FPCvtRoundsUp :: !(MT.FloatInfoRepr flt) -> !(f (MT.FloatType flt)) -> !(MT.FloatInfoRepr flt') -> PPCPrimFn ppc f MT.BoolType - FPFromBV :: !(f (MT.BVType n)) -> !(MT.FloatInfoRepr flt) -> PPCPrimFn ppc f (MT.FloatType flt) - TruncFPToSignedBV :: (1 <= n) => MT.FloatInfoRepr flt -> f (MT.FloatType flt) -> NR.NatRepr n -> PPCPrimFn ppc f (MT.BVType n) - FPAbs :: !(MT.FloatInfoRepr flt) -> !(f (MT.FloatType flt)) -> PPCPrimFn ppc f (MT.FloatType flt) - FPNeg :: !(MT.FloatInfoRepr flt) -> !(f (MT.FloatType flt)) -> PPCPrimFn ppc f (MT.FloatType flt) + + -- | Uninterpreted floating point functions + FP1 :: !String -- ^ the name of the function + -> !(f (MT.BVType 128)) -- ^ arg 1 + -> !(f (MT.BVType 32)) -- ^ current fpscr + -> PPCPrimFn ppc f (MT.BVType 160) + FP2 :: !String + -> !(f (MT.BVType 128)) + -> !(f (MT.BVType 128)) + -> !(f (MT.BVType 32)) + -> PPCPrimFn ppc f (MT.BVType 160) + FP3 :: !String + -> !(f (MT.BVType 128)) + -> !(f (MT.BVType 128)) + -> !(f (MT.BVType 128)) + -> !(f (MT.BVType 32)) + -> PPCPrimFn ppc f (MT.BVType 160) -- | Uninterpreted vector functions - Vec1 :: String -- ^ the name of the function - -> f (MT.BVType 128) - -> f (MT.BVType 32) + Vec1 :: !String -- ^ the name of the function + -> !(f (MT.BVType 128)) + -> !(f (MT.BVType 32)) -> PPCPrimFn ppc f (MT.BVType 160) Vec2 :: String -- ^ the name of the function - -> f (MT.BVType 128) - -> f (MT.BVType 128) - -> f (MT.BVType 32) + -> !(f (MT.BVType 128)) + -> !(f (MT.BVType 128)) + -> !(f (MT.BVType 32)) -> PPCPrimFn ppc f (MT.BVType 160) Vec3 :: String -- ^ the name of the function - -> f (MT.BVType 128) - -> f (MT.BVType 128) - -> f (MT.BVType 128) - -> f (MT.BVType 32) + -> !(f (MT.BVType 128)) + -> !(f (MT.BVType 128)) + -> !(f (MT.BVType 128)) + -> !(f (MT.BVType 32)) -> PPCPrimFn ppc f (MT.BVType 160) instance (1 <= MC.RegAddrWidth (MC.ArchReg ppc)) => MT.HasRepr (PPCPrimFn ppc (MC.Value ppc ids)) MT.TypeRepr where @@ -187,23 +200,12 @@ instance (1 <= MC.RegAddrWidth (MC.ArchReg ppc)) => MT.HasRepr (PPCPrimFn ppc (M FPIsQNaN _ _ -> MT.BoolTypeRepr FPIsSNaN _ _ -> MT.BoolTypeRepr - FPAdd rep _ _ -> MT.floatTypeRepr rep - FPAddRoundedUp _ _ _ -> MT.BoolTypeRepr - FPSub rep _ _ -> MT.floatTypeRepr rep - FPSubRoundedUp _ _ _ -> MT.BoolTypeRepr - FPMul rep _ _ -> MT.floatTypeRepr rep - FPMulRoundedUp _ _ _ -> MT.BoolTypeRepr - FPDiv rep _ _ -> MT.floatTypeRepr rep - FPLt _ _ _ -> MT.BoolTypeRepr - FPEq _ _ _ -> MT.BoolTypeRepr FPCvt _ _ rep -> MT.floatTypeRepr rep - FPCvtRoundsUp _ _ _ -> MT.BoolTypeRepr - FPFromBV _ rep -> MT.floatTypeRepr rep - TruncFPToSignedBV _ _ rep -> MT.BVTypeRepr rep - FPAbs rep _ -> MT.floatTypeRepr rep - FPNeg rep _ -> MT.floatTypeRepr rep - -- FIXME: Is this right? + FP1 _ _ _ -> MT.BVTypeRepr MT.knownNat + FP2 _ _ _ _ -> MT.BVTypeRepr MT.knownNat + FP3 _ _ _ _ _ -> MT.BVTypeRepr MT.knownNat + Vec1 _ _ _ -> MT.BVTypeRepr MT.knownNat Vec2 _ _ _ _ -> MT.BVTypeRepr MT.knownNat Vec3 _ _ _ _ _ -> MT.BVTypeRepr MT.knownNat @@ -218,21 +220,10 @@ ppcPrimFnHasSideEffects pf = SDiv {} -> False FPIsQNaN {} -> False FPIsSNaN {} -> False - FPAdd {} -> False - FPAddRoundedUp {} -> False - FPSub {} -> False - FPSubRoundedUp {} -> False - FPMul {} -> False - FPMulRoundedUp {} -> False - FPDiv {} -> False - FPLt {} -> False - FPEq {} -> False FPCvt {} -> False - FPCvtRoundsUp {} -> False - FPFromBV {} -> False - TruncFPToSignedBV {} -> False - FPAbs {} -> False - FPNeg {} -> False + FP1 {} -> False + FP2 {} -> False + FP3 {} -> False Vec1 {} -> False Vec2 {} -> False Vec3 {} -> False @@ -254,51 +245,18 @@ rewritePrimFn f = FPIsSNaN info v -> do tgt <- FPIsSNaN info <$> rewriteValue v evalRewrittenArchFn tgt - FPAdd rep v1 v2 -> do - tgt <- FPAdd rep <$> rewriteValue v1 <*> rewriteValue v2 - evalRewrittenArchFn tgt - FPAddRoundedUp rep v1 v2 -> do - tgt <- FPAddRoundedUp rep <$> rewriteValue v1 <*> rewriteValue v2 - evalRewrittenArchFn tgt - FPSub rep v1 v2 -> do - tgt <- FPSub rep <$> rewriteValue v1 <*> rewriteValue v2 - evalRewrittenArchFn tgt - FPSubRoundedUp rep v1 v2 -> do - tgt <- FPSubRoundedUp rep <$> rewriteValue v1 <*> rewriteValue v2 - evalRewrittenArchFn tgt - FPMul rep v1 v2 -> do - tgt <- FPMul rep <$> rewriteValue v1 <*> rewriteValue v2 - evalRewrittenArchFn tgt - FPMulRoundedUp rep v1 v2 -> do - tgt <- FPMulRoundedUp rep <$> rewriteValue v1 <*> rewriteValue v2 - evalRewrittenArchFn tgt - FPDiv rep v1 v2 -> do - tgt <- FPDiv rep <$> rewriteValue v1 <*> rewriteValue v2 - evalRewrittenArchFn tgt - FPLt rep v1 v2 -> do - tgt <- FPLt rep <$> rewriteValue v1 <*> rewriteValue v2 - evalRewrittenArchFn tgt - FPEq rep v1 v2 -> do - tgt <- FPEq rep <$> rewriteValue v1 <*> rewriteValue v2 - evalRewrittenArchFn tgt FPCvt rep1 v rep2 -> do tgt <- FPCvt rep1 <$> rewriteValue v <*> pure rep2 evalRewrittenArchFn tgt - FPCvtRoundsUp rep1 v rep2 -> do - tgt <- FPCvtRoundsUp rep1 <$> rewriteValue v <*> pure rep2 - evalRewrittenArchFn tgt - FPFromBV bv rep -> do - tgt <- FPFromBV <$> rewriteValue bv <*> pure rep - evalRewrittenArchFn tgt - TruncFPToSignedBV info v rep -> do - tgt <- TruncFPToSignedBV info <$> rewriteValue v <*> pure rep - evalRewrittenArchFn tgt - FPAbs rep v -> do - tgt <- FPAbs rep <$> rewriteValue v - evalRewrittenArchFn tgt - FPNeg rep v -> do - tgt <- FPNeg rep <$> rewriteValue v - evalRewrittenArchFn tgt + FP1 name op fpscr -> do + tgtFn <- FP1 name <$> rewriteValue op <*> rewriteValue fpscr + evalRewrittenArchFn tgtFn + FP2 name op1 op2 fpscr -> do + tgtFn <- FP2 name <$> rewriteValue op1 <*> rewriteValue op2 <*> rewriteValue fpscr + evalRewrittenArchFn tgtFn + FP3 name op1 op2 op3 fpscr -> do + tgtFn <- FP3 name <$> rewriteValue op1 <*> rewriteValue op2 <*> rewriteValue op3 <*> rewriteValue fpscr + evalRewrittenArchFn tgtFn Vec1 name op vscr -> do tgtFn <- Vec1 name <$> rewriteValue op <*> rewriteValue vscr evalRewrittenArchFn tgtFn @@ -316,21 +274,10 @@ ppPrimFn pp f = SDiv _ lhs rhs -> ppBinary "ppc_sdiv" <$> pp lhs <*> pp rhs FPIsQNaN _info v -> ppUnary "ppc_fp_isqnan" <$> pp v FPIsSNaN _info v -> ppUnary "ppc_fp_issnan" <$> pp v - FPAdd _rep v1 v2 -> ppBinary "ppc_fp_add" <$> pp v1 <*> pp v2 - FPAddRoundedUp _rep v1 v2 -> ppBinary "ppc_fp_add_roundedup" <$> pp v1 <*> pp v2 - FPSub _rep v1 v2 -> ppBinary "ppc_fp_sub" <$> pp v1 <*> pp v2 - FPSubRoundedUp _rep v1 v2 -> ppBinary "ppc_fp_sub_roundedup" <$> pp v1 <*> pp v2 - FPMul _rep v1 v2 -> ppBinary "ppc_fp_mul" <$> pp v1 <*> pp v2 - FPMulRoundedUp _rep v1 v2 -> ppBinary "ppc_fp_mul_roundedup" <$> pp v1 <*> pp v2 - FPDiv _rep v1 v2 -> ppBinary "ppc_fp_div" <$> pp v1 <*> pp v2 - FPLt _rep v1 v2 -> ppBinary "ppc_fp_lt" <$> pp v1 <*> pp v2 - FPEq _rep v1 v2 -> ppBinary "ppc_fp_eq" <$> pp v1 <*> pp v2 FPCvt _rep1 v _rep2 -> ppUnary "ppc_fp_cvt" <$> pp v - FPCvtRoundsUp _rep1 v _rep2 -> ppUnary "ppc_fp_cvt_roundedup" <$> pp v - FPFromBV bv _rep -> ppUnary "ppc_fp_frombv" <$> pp bv - TruncFPToSignedBV _info v _rep -> ppUnary "ppc_fp_trunc_to_signed_bv" <$> pp v - FPAbs _rep v -> ppUnary "ppc_fp_abs" <$> pp v - FPNeg _rep v -> ppUnary "ppc_fp_neg" <$> pp v + FP1 n r1 fpscr -> ppBinary ("ppc_fp1 " ++ n) <$> pp r1 <*> pp fpscr + FP2 n r1 r2 fpscr -> pp3 ("ppc_fp2 " ++ n) <$> pp r1 <*> pp r2 <*> pp fpscr + FP3 n r1 r2 r3 fpscr -> pp4 ("ppc_fp3 " ++ n) <$> pp r1 <*> pp r2 <*> pp r3 <*> pp fpscr Vec1 n r1 vscr -> ppBinary ("ppc_vec1 " ++ n) <$> pp r1 <*> pp vscr Vec2 n r1 r2 vscr -> pp3 ("ppc_vec2" ++ n) <$> pp r1 <*> pp r2 <*> pp vscr Vec3 n r1 r2 r3 vscr -> pp4 ("ppc_vec3" ++ n) <$> pp r1 <*> pp r2 <*> pp r3 <*> pp vscr @@ -356,21 +303,10 @@ instance FC.TraversableFC (PPCPrimFn ppc) where SDiv rep lhs rhs -> SDiv rep <$> go lhs <*> go rhs FPIsQNaN info v -> FPIsQNaN info <$> go v FPIsSNaN info v -> FPIsSNaN info <$> go v - FPAdd rep v1 v2 -> FPAdd rep <$> go v1 <*> go v2 - FPAddRoundedUp rep v1 v2 -> FPAddRoundedUp rep <$> go v1 <*> go v2 - FPSub rep v1 v2 -> FPSub rep <$> go v1 <*> go v2 - FPSubRoundedUp rep v1 v2 -> FPSubRoundedUp rep <$> go v1 <*> go v2 - FPMul rep v1 v2 -> FPMul rep <$> go v1 <*> go v2 - FPMulRoundedUp rep v1 v2 -> FPMulRoundedUp rep <$> go v1 <*> go v2 - FPDiv rep v1 v2 -> FPDiv rep <$> go v1 <*> go v2 - FPLt rep v1 v2 -> FPLt rep <$> go v1 <*> go v2 - FPEq rep v1 v2 -> FPEq rep <$> go v1 <*> go v2 FPCvt rep1 v rep2 -> FPCvt rep1 <$> go v <*> pure rep2 - FPCvtRoundsUp rep1 v rep2 -> FPCvtRoundsUp rep1 <$> go v <*> pure rep2 - FPFromBV bv rep -> FPFromBV <$> go bv <*> pure rep - TruncFPToSignedBV info v rep -> TruncFPToSignedBV info <$> go v <*> pure rep - FPAbs rep v -> FPAbs rep <$> go v - FPNeg rep v -> FPNeg rep <$> go v + FP1 name op fpscr -> FP1 name <$> go op <*> go fpscr + FP2 name op1 op2 fpscr -> FP2 name <$> go op1 <*> go op2 <*> go fpscr + FP3 name op1 op2 op3 fpscr -> FP3 name <$> go op1 <*> go op2 <*> go op3 <*> go fpscr Vec1 name op vscr -> Vec1 name <$> go op <*> go vscr Vec2 name op1 op2 vscr -> Vec2 name <$> go op1 <*> go op2 <*> go vscr Vec3 name op1 op2 op3 vscr -> Vec3 name <$> go op1 <*> go op2 <*> go op3 <*> go vscr @@ -404,60 +340,100 @@ memrrToEffectiveAddress memrr = do b <- G.addExpr (G.AppExpr (MC.Mux (MT.BVTypeRepr repr) isr0 zero base)) G.addExpr (G.AppExpr (MC.BVAdd repr b offset)) +-- | A helper to increment the IP by 4, meant to be used to implement +-- arch-specific statements that need to update the IP (i.e., all but syscalls). +incrementIP :: (PPCArchConstraints ppc) => G.Generator ppc ids s () +incrementIP = do + rs <- G.getRegs + let ipVal = rs ^. MC.boundValue PPC_IP + e <- G.addExpr (G.AppExpr (MC.BVAdd knownRepr ipVal (MC.BVValue knownRepr 0x4))) + G.setRegVal PPC_IP e + -- | Manually-provided semantics for instructions whose full semantics cannot be -- expressed in our semantics format. -- -- This includes instructions with special side effects that we don't have a way -- to talk about in the semantics; especially useful for architecture-specific -- terminator statements. +-- +-- NOTE: For SC and TRAP (which we treat as system calls), we don't need to +-- update the IP here, as the update is handled in the abstract interpretation +-- of system calls in 'postPPCTermStmtAbsState'. ppcInstructionMatcher :: (PPCArchConstraints ppc) => D.Instruction -> Maybe (G.Generator ppc ids s ()) ppcInstructionMatcher (D.Instruction opc operands) = case opc of - D.SC -> Just (G.finishWithTerminator (MC.ArchTermStmt PPCSyscall)) - D.TRAP -> Just (G.finishWithTerminator (MC.ArchTermStmt PPCTrap)) - D.ATTN -> Just (G.addStmt (MC.ExecArchStmt Attn)) - D.SYNC -> Just (G.addStmt (MC.ExecArchStmt Sync)) - D.ISYNC -> Just (G.addStmt (MC.ExecArchStmt Isync)) + D.SC -> Just $ G.finishWithTerminator (MC.ArchTermStmt PPCSyscall) + D.TRAP -> Just $ G.finishWithTerminator (MC.ArchTermStmt PPCTrap) + D.ATTN -> Just $ do + incrementIP + G.addStmt (MC.ExecArchStmt Attn) + D.SYNC -> Just $ do + incrementIP + G.addStmt (MC.ExecArchStmt Sync) + D.ISYNC -> Just $ do + incrementIP + G.addStmt (MC.ExecArchStmt Isync) D.DCBA -> case operands of D.Memrr memrr D.:< D.Nil -> Just $ do + incrementIP ea <- memrrToEffectiveAddress memrr G.addStmt (MC.ExecArchStmt (Dcba ea)) D.DCBF -> case operands of D.Memrr memrr D.:< D.Nil -> Just $ do + incrementIP ea <- memrrToEffectiveAddress memrr G.addStmt (MC.ExecArchStmt (Dcbf ea)) D.DCBI -> case operands of D.Memrr memrr D.:< D.Nil -> Just $ do + incrementIP ea <- memrrToEffectiveAddress memrr G.addStmt (MC.ExecArchStmt (Dcbi ea)) D.DCBST -> case operands of D.Memrr memrr D.:< D.Nil -> Just $ do + incrementIP ea <- memrrToEffectiveAddress memrr G.addStmt (MC.ExecArchStmt (Dcbst ea)) D.DCBZ -> case operands of D.Memrr memrr D.:< D.Nil -> Just $ do + incrementIP ea <- memrrToEffectiveAddress memrr G.addStmt (MC.ExecArchStmt (Dcbz ea)) D.DCBZL -> case operands of D.Memrr memrr D.:< D.Nil -> Just $ do + incrementIP ea <- memrrToEffectiveAddress memrr G.addStmt (MC.ExecArchStmt (Dcbzl ea)) D.DCBT -> case operands of D.Memrr memrr D.:< D.U5imm imm D.:< D.Nil -> Just $ do + incrementIP ea <- memrrToEffectiveAddress memrr th <- O.extractValue imm G.addStmt (MC.ExecArchStmt (Dcbt ea th)) D.DCBTST -> case operands of D.Memrr memrr D.:< D.U5imm imm D.:< D.Nil -> Just $ do + incrementIP ea <- memrrToEffectiveAddress memrr th <- O.extractValue imm G.addStmt (MC.ExecArchStmt (Dcbtst ea th)) + D.ICBI -> + case operands of + D.Memrr memrr D.:< D.Nil -> Just $ do + incrementIP + ea <- memrrToEffectiveAddress memrr + G.addStmt (MC.ExecArchStmt (Icbi ea)) + D.ICBT -> + case operands of + D.Memrr memrr D.:< D.U4imm imm D.:< D.Nil -> Just $ do + incrementIP + ea <- memrrToEffectiveAddress memrr + ct <- O.extractValue imm + G.addStmt (MC.ExecArchStmt (Icbt ea ct)) _ -> Nothing diff --git a/macaw-ppc/src/Data/Macaw/PPC/Eval.hs b/macaw-ppc/src/Data/Macaw/PPC/Eval.hs index c3117e00..bd324330 100644 --- a/macaw-ppc/src/Data/Macaw/PPC/Eval.hs +++ b/macaw-ppc/src/Data/Macaw/PPC/Eval.hs @@ -100,21 +100,10 @@ absEvalArchFn _ _r f = UDiv {} -> MA.TopV FPIsQNaN {} -> MA.TopV FPIsSNaN {} -> MA.TopV - FPAdd {} -> MA.TopV - FPAddRoundedUp {} -> MA.TopV - FPSub {} -> MA.TopV - FPSubRoundedUp {} -> MA.TopV - FPMul {} -> MA.TopV - FPMulRoundedUp {} -> MA.TopV - FPDiv {} -> MA.TopV - FPLt {} -> MA.TopV - FPEq {} -> MA.TopV FPCvt {} -> MA.TopV - FPCvtRoundsUp {} -> MA.TopV - FPFromBV {} -> MA.TopV - TruncFPToSignedBV {} -> MA.TopV - FPAbs {} -> MA.TopV - FPNeg {} -> MA.TopV + FP1 {} -> MA.TopV + FP2 {} -> MA.TopV + FP3 {} -> MA.TopV Vec1 {} -> MA.TopV Vec2 {} -> MA.TopV Vec3 {} -> MA.TopV diff --git a/macaw-ppc/src/Data/Macaw/PPC/Semantics/TH.hs b/macaw-ppc/src/Data/Macaw/PPC/Semantics/TH.hs index 29f3cefc..229a2676 100644 --- a/macaw-ppc/src/Data/Macaw/PPC/Semantics/TH.hs +++ b/macaw-ppc/src/Data/Macaw/PPC/Semantics/TH.hs @@ -61,6 +61,39 @@ ppcNonceAppEval bvi nonceApp = S.FnApp symFn args -> do let fnName = symFnName symFn case fnName of + "ppc_fp1" -> return $ do + case FC.toListFC Some args of + [Some op, Some frA, Some fpscr] -> do + case getOpName op of + Just name -> do + valA <- addEltTH bvi frA + valFpscr <- addEltTH bvi fpscr + liftQ [| addArchExpr $ FP1 $(lift name) $(return valA) $(return valFpscr) |] + Nothing -> fail $ "Invalid argument list for ppc.fp1: " ++ showF args + _ -> fail $ "Invalid argument list for ppc.fp1: " ++ showF args + "ppc_fp2" -> return $ do + case FC.toListFC Some args of + [Some op, Some frA, Some frB, Some fpscr] -> do + case getOpName op of + Just name -> do + valA <- addEltTH bvi frA + valB <- addEltTH bvi frB + valFpscr <- addEltTH bvi fpscr + liftQ [| addArchExpr $ FP2 $(lift name) $(return valA) $(return valB) $(return valFpscr) |] + Nothing -> fail $ "Invalid argument list for ppc.fp2: " ++ showF args + _ -> fail $ "Invalid argument list for ppc.fp2: " ++ showF args + "ppc_fp3" -> return $ do + case FC.toListFC Some args of + [Some op, Some frA, Some frB, Some frC, Some fpscr] -> do + case getOpName op of + Just name -> do + valA <- addEltTH bvi frA + valB <- addEltTH bvi frB + valC <- addEltTH bvi frC + valFpscr <- addEltTH bvi fpscr + liftQ [| addArchExpr $ FP3 $(lift name) $(return valA) $(return valB) $(return valC) $(return valFpscr) |] + Nothing -> fail $ "Invalid argument list for ppc.fp2: " ++ showF args + _ -> fail $ "Invalid argument list for ppc.fp2: " ++ showF args "ppc_vec1" -> return $ do case FC.toListFC Some args of [Some op, Some rA, Some vscr] -> do @@ -70,7 +103,7 @@ ppcNonceAppEval bvi nonceApp = valVscr <- addEltTH bvi vscr liftQ [| addArchExpr $ Vec1 $(lift name) $(return valA) $(return valVscr) |] Nothing -> fail $ "Invalid argument list for ppc.vec1: " ++ showF args - _ -> fail $ "Invalid argument list for ppc.vec2: " ++ showF args + _ -> fail $ "Invalid argument list for ppc.vec1: " ++ showF args "ppc_vec2" -> return $ do case FC.toListFC Some args of [Some op, Some rA, Some rB, Some vscr] -> do @@ -160,18 +193,6 @@ floatingPointTH bvi fnName args = "single_to_double" -> do fpval <- addEltTH bvi a liftQ [| addArchExpr (FPCvt M.SingleFloatRepr $(return fpval) M.DoubleFloatRepr) |] - "abs" -> do - -- Note that fabs is only defined for doubles; the operation is the - -- same for single and double precision on PPC, so there is only a - -- single instruction. - fpval <- addEltTH bvi a - liftQ [| addArchExpr (FPAbs M.DoubleFloatRepr $(return fpval)) |] - "negate64" -> do - fpval <- addEltTH bvi a - liftQ [| addArchExpr (FPNeg M.DoubleFloatRepr $(return fpval)) |] - "negate32" -> do - fpval <- addEltTH bvi a - liftQ [| addArchExpr (FPNeg M.SingleFloatRepr $(return fpval)) |] "is_qnan32" -> do fpval <- addEltTH bvi a liftQ [| addArchExpr (FPIsQNaN M.SingleFloatRepr $(return fpval)) |] @@ -187,63 +208,9 @@ floatingPointTH bvi fnName args = _ -> fail ("Unsupported unary floating point intrinsic: " ++ fnName) [Some a, Some b] -> case fnName of - "add64" -> do - valA <- addEltTH bvi a - valB <- addEltTH bvi b - liftQ [| addArchExpr (FPAdd M.DoubleFloatRepr $(return valA) $(return valB)) |] - "add32" -> do - valA <- addEltTH bvi a - valB <- addEltTH bvi b - liftQ [| addArchExpr (FPAdd M.SingleFloatRepr $(return valA) $(return valB)) |] - "sub64" -> do - valA <- addEltTH bvi a - valB <- addEltTH bvi b - liftQ [| addArchExpr (FPSub M.DoubleFloatRepr $(return valA) $(return valB)) |] - "sub32" -> do - valA <- addEltTH bvi a - valB <- addEltTH bvi b - liftQ [| addArchExpr (FPSub M.SingleFloatRepr $(return valA) $(return valB)) |] - "mul64" -> do - valA <- addEltTH bvi a - valB <- addEltTH bvi b - liftQ [| addArchExpr (FPMul M.DoubleFloatRepr $(return valA) $(return valB)) |] - "mul32" -> do - valA <- addEltTH bvi a - valB <- addEltTH bvi b - liftQ [| addArchExpr (FPMul M.SingleFloatRepr $(return valA) $(return valB)) |] - "div64" -> do - valA <- addEltTH bvi a - valB <- addEltTH bvi b - liftQ [| addArchExpr (FPDiv M.DoubleFloatRepr $(return valA) $(return valB)) |] - "div32" -> do - valA <- addEltTH bvi a - valB <- addEltTH bvi b - liftQ [| addArchExpr (FPDiv M.SingleFloatRepr $(return valA) $(return valB)) |] - "lt" -> do - valA <- addEltTH bvi a - valB <- addEltTH bvi b - -- All comparisons are done as 64-bit comparisons in PPC - liftQ [| addArchExpr (FPLt M.DoubleFloatRepr $(return valA) $(return valB)) |] _ -> fail ("Unsupported binary floating point intrinsic: " ++ fnName) [Some a, Some b, Some c] -> case fnName of - "muladd64" -> do - -- FIXME: This is very wrong - we need a separate constructor for it - -- a * c + b - valA <- addEltTH bvi a - valB <- addEltTH bvi b - valC <- addEltTH bvi c - liftQ [| do prodVal <- addArchExpr (FPMul M.DoubleFloatRepr $(return valA) $(return valC)) - addArchExpr (FPAdd M.DoubleFloatRepr prodVal $(return valB)) - |] - "muladd32" -> do - -- a * c + b - valA <- addEltTH bvi a - valB <- addEltTH bvi b - valC <- addEltTH bvi c - liftQ [| do prodVal <- addArchExpr (FPMul M.SingleFloatRepr $(return valA) $(return valC)) - addArchExpr (FPAdd M.SingleFloatRepr prodVal $(return valB)) - |] _ -> fail ("Unsupported ternary floating point intrinsic: " ++ fnName) _ -> fail ("Unsupported floating point intrinsic: " ++ fnName) diff --git a/macaw-ppc/tests/PPC64InstructionCoverage.hs b/macaw-ppc/tests/PPC64InstructionCoverage.hs index 9d0cb33b..90c8a85e 100644 --- a/macaw-ppc/tests/PPC64InstructionCoverage.hs +++ b/macaw-ppc/tests/PPC64InstructionCoverage.hs @@ -38,7 +38,7 @@ testMacaw elf = let otherEntryAddrs :: [MM.MemAddr 64] otherEntryAddrs = E.tocEntryAddrsForElf (Proxy @PPC64.PPC) elf let otherEntries = mapMaybe (MM.asSegmentOff mem) otherEntryAddrs - let di = MD.cfgFromAddrs (RO.ppc64_linux_info tocBase) mem MD.emptySymbolAddrMap (entryPoint:otherEntries) [] + let di = MD.cfgFromAddrs (RO.ppc64_linux_info tocBase) mem M.empty (entryPoint:otherEntries) [] let allFoundBlockAddrs :: S.Set Word64 allFoundBlockAddrs = S.fromList [ fromIntegral (fromJust (MM.asAbsoluteAddr (MM.relativeSegmentAddr (MD.pblockAddr pbr)))) diff --git a/macaw-ppc/tests/PPC64Tests.hs b/macaw-ppc/tests/PPC64Tests.hs index b28e3690..3e83f621 100644 --- a/macaw-ppc/tests/PPC64Tests.hs +++ b/macaw-ppc/tests/PPC64Tests.hs @@ -82,7 +82,7 @@ testDiscovery expectedFilename elf = otherEntryAddrs :: [MM.MemAddr 64] otherEntryAddrs = E.tocEntryAddrsForElf (Proxy @PPC64.PPC) elf otherEntries = mapMaybe (MM.asSegmentOff mem) otherEntryAddrs - di = MD.cfgFromAddrs (RO.ppc64_linux_info tocBase) mem MD.emptySymbolAddrMap (entryPoint:otherEntries) [] + di = MD.cfgFromAddrs (RO.ppc64_linux_info tocBase) mem M.empty (entryPoint:otherEntries) [] expectedString <- readFile expectedFilename case readMaybe expectedString of -- Above: Read in the ExpectedResult from the contents of the file diff --git a/stack.yaml b/stack.yaml index aa01133c..b3fbee7f 100644 --- a/stack.yaml +++ b/stack.yaml @@ -3,20 +3,26 @@ flags: old-locale: false packages: - macaw-semmc/ +- macaw-arm/ - macaw-ppc/ - submodules/semmc/semmc - submodules/semmc/semmc-ppc +- submodules/semmc/semmc-arm - submodules/dismantle/dismantle-tablegen - submodules/dismantle/dismantle-ppc +- submodules/dismantle/dismantle-arm +- submodules/dismantle/dismantle-thumb - submodules/macaw/base - submodules/parameterized-utils - submodules/crucible/crucible - submodules/crucible/galois-matlab - submodules/dwarf - submodules/elf-edit +- submodules/s-cargot extra-deps: +- BoundedChan-1.0.3.0 - IntervalMap-0.5.2.0 -- Cabal-2.0.0.2 +- Only-0.1 - QuickCheck-2.10.0.1 - StateVar-1.1.0.4 - adjunctions-4.3 @@ -24,10 +30,11 @@ extra-deps: - ansi-wl-pprint-0.6.8.1 - async-2.1.1.1 - attoparsec-0.13.2.0 +- auto-update-0.1.4 - base-compat-0.9.3 - base-orphans-0.6 +- base16-bytestring-0.1.1.6 - bifunctors-5.4.2 -- binary-0.8.5.1 - bimap-0.3.3 - blaze-builder-0.4.0.2 - blaze-textual-0.2.1.0 @@ -35,18 +42,22 @@ extra-deps: - cabal-doctest-1.0.2 - call-stack-0.1.0 - case-insensitive-1.2.0.10 +- cereal-0.5.4.0 - clock-0.7.2 - comonad-5.0.2 +- conduit-1.2.12.1 +- conduit-extra-1.1.17 - constraints-0.9.1 -- containers-0.5.10.2 - contravariant-1.4 - direct-sqlite-2.3.21 - distributive-0.5.3 +- easy-file-0.2.1 - exceptions-0.8.3 - fail-4.9.0.0 +- fast-logger-2.4.10 - fgl-5.6.0.0 - filemanip-0.3.6.3 -- fingertree-0.1.1.0 +- finite-typelits-0.1.3.0 - free-4.12.4 - generic-deriving-1.11.2 - hashable-1.2.6.1 @@ -55,14 +66,19 @@ extra-deps: - io-streams-1.4.1.0 - kan-extensions-5.0.2 - lens-4.15.4 +- lifted-base-0.2.3.11 - located-base-0.1.1.1 - math-functions-0.2.1.0 - megaparsec-6.1.1 +- mmorph-1.1.0 +- monad-control-1.0.2.2 - monad-logger-0.3.25.1 +- monad-loops-0.4.3 - mtl-2.2.1 - mwc-random-0.13.6.0 - network-2.6.3.2 -- Only-0.1 +- old-locale-1.0.0.7 +- old-time-1.1.0.3 - optparse-applicative-0.14.0.0 - parallel-3.2.1.1 - parsec-3.1.11 @@ -77,60 +93,40 @@ extra-deps: - regex-tdfa-1.2.2 - regex-tdfa-text-1.0.0.3 - resourcet-1.1.9 -- s-cargot-0.1.2.0 +# - s-cargot-0.1.2.0 - scientific-0.3.5.1 - semigroupoids-5.2.1 - semigroups-0.18.3 -- smtLib-1.0.8 - split-0.2.3.2 - sqlite-simple-0.4.14.0 - stm-2.4.4.1 +- stm-chans-3.0.0.4 +- streaming-commons-0.1.18 - tagged-0.8.5 - tasty-0.11.2.5 - tasty-ant-xml-1.1.0 - tasty-expected-failure-0.11.0.4 -- tasty-hunit-0.9.2 +- tasty-hunit-0.10.0.1 - tasty-quickcheck-0.8.4 - temporary-1.2.1.1 - text-1.2.2.2 - tf-random-0.5 - th-abstraction-0.2.5.0 - time-locale-compat-0.1.1.3 +- transformers-base-0.4.4 - transformers-compat-0.5.1.4 - unbounded-delays-0.1.1.0 - unix-compat-0.4.3.1 +- unix-time-0.3.7 - unliftio-0.1.0.0 - unliftio-core-0.1.0.0 - unordered-containers-0.2.8.0 - utf8-string-1.0.1.1 - vector-0.12.0.1 +- vector-sized-0.6.1.0 - vector-th-unbox-0.2.1.6 - void-0.7.2 - xml-1.3.14 - zlib-0.6.1.2 - zlib-bindings-0.1.1.5 - -- conduit-1.2.12.1 -- conduit-extra-1.1.17 -- fast-logger-2.4.10 -- lifted-base-0.2.3.11 -- mmorph-1.1.0 -- monad-control-1.0.2.2 -- monad-loops-0.4.3 -- old-locale-1.0.0.7 -- stm-chans-3.0.0.4 -- transformers-base-0.4.4 - -- auto-update-0.1.4 -- easy-file-0.2.1 -- streaming-commons-0.1.18 -- unix-time-0.3.7 - -- old-time-1.1.0.3 - -- base16-bytestring-0.1.1.6 -- cereal-0.5.4.0 - - - resolver: ghc-8.2.1 diff --git a/submodules/crucible b/submodules/crucible index 1f580c71..256e47fa 160000 --- a/submodules/crucible +++ b/submodules/crucible @@ -1 +1 @@ -Subproject commit 1f580c71e05efbcd79828430234964829edebab5 +Subproject commit 256e47fab36245dd9ad3d987edc165bf3d4a4766 diff --git a/submodules/dismantle b/submodules/dismantle index 183e2688..5934a45f 160000 --- a/submodules/dismantle +++ b/submodules/dismantle @@ -1 +1 @@ -Subproject commit 183e26883166a865e3d07de881a6971ba25c5cf8 +Subproject commit 5934a45ffc1f84843482d5b5d6ff3ffab258b732 diff --git a/submodules/macaw b/submodules/macaw index eebc94cb..278b079a 160000 --- a/submodules/macaw +++ b/submodules/macaw @@ -1 +1 @@ -Subproject commit eebc94cbe808e3b0ecfb036990a242b33a13658b +Subproject commit 278b079a4963fa9ad70905a55fa07b6935b48788 diff --git a/submodules/parameterized-utils b/submodules/parameterized-utils index 7c76b811..3a589978 160000 --- a/submodules/parameterized-utils +++ b/submodules/parameterized-utils @@ -1 +1 @@ -Subproject commit 7c76b811a321a548af7d4fcf46390daf979f39b1 +Subproject commit 3a58997813693ffbb3b8dd11a24f24ec05c4d1ee diff --git a/submodules/s-cargot b/submodules/s-cargot new file mode 160000 index 00000000..68e8eb15 --- /dev/null +++ b/submodules/s-cargot @@ -0,0 +1 @@ +Subproject commit 68e8eb150f334ec81eac813f76e80c9a8dd4cc7f diff --git a/submodules/semmc b/submodules/semmc index de3cef59..fcb75a23 160000 --- a/submodules/semmc +++ b/submodules/semmc @@ -1 +1 @@ -Subproject commit de3cef59472041fbfd69494978a8de28716d3f5f +Subproject commit fcb75a23bb0d07aae42a53e89f6f9da76f7d78e9