mirror of
https://github.com/GaloisInc/macaw.git
synced 2024-11-24 00:42:28 +03:00
[ppc] Add division and a few arch-specific statements
The arch-specific statements are for memory synchronization
This commit is contained in:
parent
48dfa4d192
commit
bbd00f7ef2
@ -20,20 +20,21 @@ module Data.Macaw.PPC.Arch (
|
|||||||
PPCArchConstraints
|
PPCArchConstraints
|
||||||
) where
|
) where
|
||||||
|
|
||||||
import GHC.TypeLits
|
import GHC.TypeLits
|
||||||
|
|
||||||
import qualified Text.PrettyPrint.ANSI.Leijen as PP
|
import qualified Text.PrettyPrint.ANSI.Leijen as PP
|
||||||
|
import qualified Data.Parameterized.NatRepr as NR
|
||||||
import qualified Data.Parameterized.TraversableFC as FC
|
import qualified Data.Parameterized.TraversableFC as FC
|
||||||
import qualified Data.Parameterized.TraversableF as TF
|
import qualified Data.Parameterized.TraversableF as TF
|
||||||
import qualified Data.Macaw.CFG as MC
|
import qualified Data.Macaw.CFG as MC
|
||||||
import Data.Macaw.CFG.Rewriter ( Rewriter, rewriteValue, evalRewrittenArchFn )
|
import Data.Macaw.CFG.Rewriter ( Rewriter, rewriteValue, evalRewrittenArchFn, appendRewrittenArchStmt )
|
||||||
import qualified Data.Macaw.Memory as MM
|
import qualified Data.Macaw.Memory as MM
|
||||||
import qualified Data.Macaw.Types as MT
|
import qualified Data.Macaw.Types as MT
|
||||||
|
|
||||||
import qualified SemMC.Architecture.PPC32 as PPC32
|
import qualified SemMC.Architecture.PPC32 as PPC32
|
||||||
import qualified SemMC.Architecture.PPC64 as PPC64
|
import qualified SemMC.Architecture.PPC64 as PPC64
|
||||||
|
|
||||||
import Data.Macaw.PPC.PPCReg
|
import Data.Macaw.PPC.PPCReg
|
||||||
|
|
||||||
data PPCTermStmt ids where
|
data PPCTermStmt ids where
|
||||||
-- | A representation of the PowerPC @sc@ instruction
|
-- | A representation of the PowerPC @sc@ instruction
|
||||||
@ -61,14 +62,17 @@ rewriteTermStmt s =
|
|||||||
PPCSyscall -> pure PPCSyscall
|
PPCSyscall -> pure PPCSyscall
|
||||||
PPCTrap -> pure PPCTrap
|
PPCTrap -> pure PPCTrap
|
||||||
|
|
||||||
-- | We currently have no PPC-specific statements. Remove 'None' if we add some.
|
|
||||||
data PPCStmt ppc (v :: MT.Type -> *) where
|
data PPCStmt ppc (v :: MT.Type -> *) where
|
||||||
None :: PPCStmt ppc v
|
Attn :: PPCStmt ppc v
|
||||||
|
Sync :: PPCStmt ppc v
|
||||||
|
Isync :: PPCStmt ppc v
|
||||||
|
|
||||||
instance MC.PrettyF (PPCStmt ppc) where
|
instance MC.PrettyF (PPCStmt ppc) where
|
||||||
prettyF s =
|
prettyF s =
|
||||||
case s of
|
case s of
|
||||||
None -> PP.text "None"
|
Attn -> PP.text "ppc_attn"
|
||||||
|
Sync -> PP.text "ppc_sync"
|
||||||
|
Isync -> PP.text "ppc_isync"
|
||||||
|
|
||||||
instance TF.FunctorF (PPCStmt ppc) where
|
instance TF.FunctorF (PPCStmt ppc) where
|
||||||
fmapF = TF.fmapFDefault
|
fmapF = TF.fmapFDefault
|
||||||
@ -79,50 +83,66 @@ instance TF.FoldableF (PPCStmt ppc) where
|
|||||||
instance TF.TraversableF (PPCStmt ppc) where
|
instance TF.TraversableF (PPCStmt ppc) where
|
||||||
traverseF _go stmt =
|
traverseF _go stmt =
|
||||||
case stmt of
|
case stmt of
|
||||||
None -> pure None
|
Attn -> pure Attn
|
||||||
|
Sync -> pure Sync
|
||||||
|
Isync -> pure Isync
|
||||||
|
|
||||||
instance MC.IsArchStmt (PPCStmt ppc) where
|
instance MC.IsArchStmt (PPCStmt ppc) where
|
||||||
ppArchStmt _pp stmt =
|
ppArchStmt _pp stmt =
|
||||||
case stmt of
|
case stmt of
|
||||||
None -> PP.text "none"
|
Attn -> PP.text "ppc_attn"
|
||||||
|
Sync -> PP.text "ppc_sync"
|
||||||
|
Isync -> PP.text "ppc_isync"
|
||||||
|
|
||||||
type instance MC.ArchStmt PPC64.PPC = PPCStmt PPC64.PPC
|
type instance MC.ArchStmt PPC64.PPC = PPCStmt PPC64.PPC
|
||||||
type instance MC.ArchStmt PPC32.PPC = PPCStmt PPC32.PPC
|
type instance MC.ArchStmt PPC32.PPC = PPCStmt PPC32.PPC
|
||||||
|
|
||||||
rewriteStmt :: PPCStmt ppc (MC.Value ppc src) -> Rewriter ppc s src tgt ()
|
rewriteStmt :: (MC.ArchStmt ppc ~ PPCStmt ppc) => PPCStmt ppc (MC.Value ppc src) -> Rewriter ppc s src tgt ()
|
||||||
rewriteStmt _ = return ()
|
rewriteStmt s = do
|
||||||
|
s' <- TF.traverseF rewriteValue s
|
||||||
|
appendRewrittenArchStmt s'
|
||||||
|
|
||||||
data PPCPrimFn ppc f tp where
|
data PPCPrimFn ppc f tp where
|
||||||
IDiv :: proxy ppc
|
UDiv :: NR.NatRepr (MC.RegAddrWidth (MC.ArchReg ppc))
|
||||||
|
-> 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)))
|
||||||
|
SDiv :: NR.NatRepr (MC.RegAddrWidth (MC.ArchReg ppc))
|
||||||
-> f (MT.BVType (MC.RegAddrWidth (MC.ArchReg ppc)))
|
-> f (MT.BVType (MC.RegAddrWidth (MC.ArchReg ppc)))
|
||||||
-> 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)))
|
-> PPCPrimFn ppc f (MT.BVType (MC.RegAddrWidth (MC.ArchReg ppc)))
|
||||||
|
|
||||||
instance MT.HasRepr (PPCPrimFn ppc (MC.Value ppc ids)) MT.TypeRepr where
|
instance (1 <= MC.RegAddrWidth (MC.ArchReg ppc)) => MT.HasRepr (PPCPrimFn ppc (MC.Value ppc ids)) MT.TypeRepr where
|
||||||
typeRepr f =
|
typeRepr f =
|
||||||
case f of
|
case f of
|
||||||
IDiv {} -> undefined
|
UDiv rep _ _ -> MT.BVTypeRepr rep
|
||||||
|
SDiv rep _ _ -> MT.BVTypeRepr rep
|
||||||
|
|
||||||
-- | Right now, none of the primitive functions has a side effect. That will
|
-- | Right now, none of the primitive functions has a side effect. That will
|
||||||
-- probably change.
|
-- probably change.
|
||||||
ppcPrimFnHasSideEffects :: PPCPrimFn ppc f tp -> Bool
|
ppcPrimFnHasSideEffects :: PPCPrimFn ppc f tp -> Bool
|
||||||
ppcPrimFnHasSideEffects pf =
|
ppcPrimFnHasSideEffects pf =
|
||||||
case pf of
|
case pf of
|
||||||
IDiv {} -> False
|
UDiv {} -> False
|
||||||
|
SDiv {} -> False
|
||||||
|
|
||||||
rewritePrimFn :: (PPCArchConstraints ppc, MC.ArchFn ppc ~ PPCPrimFn ppc)
|
rewritePrimFn :: (PPCArchConstraints ppc, MC.ArchFn ppc ~ PPCPrimFn ppc)
|
||||||
=> PPCPrimFn ppc (MC.Value ppc src) tp
|
=> PPCPrimFn ppc (MC.Value ppc src) tp
|
||||||
-> Rewriter ppc s src tgt (MC.Value ppc tgt tp)
|
-> Rewriter ppc s src tgt (MC.Value ppc tgt tp)
|
||||||
rewritePrimFn f =
|
rewritePrimFn f =
|
||||||
case f of
|
case f of
|
||||||
IDiv p lhs rhs -> do
|
UDiv rep lhs rhs -> do
|
||||||
tgtFn <- IDiv p <$> rewriteValue lhs <*> rewriteValue rhs
|
tgtFn <- UDiv rep <$> rewriteValue lhs <*> rewriteValue rhs
|
||||||
|
evalRewrittenArchFn tgtFn
|
||||||
|
SDiv rep lhs rhs -> do
|
||||||
|
tgtFn <- SDiv rep <$> rewriteValue lhs <*> rewriteValue rhs
|
||||||
evalRewrittenArchFn tgtFn
|
evalRewrittenArchFn tgtFn
|
||||||
|
|
||||||
ppPrimFn :: (Applicative m) => (forall u . f u -> m PP.Doc) -> PPCPrimFn ppc f tp -> m PP.Doc
|
ppPrimFn :: (Applicative m) => (forall u . f u -> m PP.Doc) -> PPCPrimFn ppc f tp -> m PP.Doc
|
||||||
ppPrimFn _pp f =
|
ppPrimFn pp f =
|
||||||
case f of
|
case f of
|
||||||
IDiv {} -> pure (PP.text "idiv")
|
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
|
||||||
|
|
||||||
instance MC.IsArchFn (PPCPrimFn ppc) where
|
instance MC.IsArchFn (PPCPrimFn ppc) where
|
||||||
ppArchFn = ppPrimFn
|
ppArchFn = ppPrimFn
|
||||||
@ -136,7 +156,8 @@ instance FC.FoldableFC (PPCPrimFn ppc) where
|
|||||||
instance FC.TraversableFC (PPCPrimFn ppc) where
|
instance FC.TraversableFC (PPCPrimFn ppc) where
|
||||||
traverseFC go f =
|
traverseFC go f =
|
||||||
case f of
|
case f of
|
||||||
IDiv p lhs rhs -> IDiv p <$> go lhs <*> go rhs
|
UDiv rep lhs rhs -> UDiv rep <$> go lhs <*> go rhs
|
||||||
|
SDiv rep lhs rhs -> SDiv rep <$> go lhs <*> go rhs
|
||||||
|
|
||||||
type instance MC.ArchFn PPC64.PPC = PPCPrimFn PPC64.PPC
|
type instance MC.ArchFn PPC64.PPC = PPCPrimFn PPC64.PPC
|
||||||
type instance MC.ArchFn PPC32.PPC = PPCPrimFn PPC32.PPC
|
type instance MC.ArchFn PPC32.PPC = PPCPrimFn PPC32.PPC
|
||||||
|
@ -80,7 +80,8 @@ absEvalArchFn :: (PPCArchConstraints ppc)
|
|||||||
-> AbsValue (RegAddrWidth (ArchReg ppc)) tp
|
-> AbsValue (RegAddrWidth (ArchReg ppc)) tp
|
||||||
absEvalArchFn _ _r f =
|
absEvalArchFn _ _r f =
|
||||||
case f of
|
case f of
|
||||||
IDiv {} -> MA.TopV
|
SDiv {} -> MA.TopV
|
||||||
|
UDiv {} -> MA.TopV
|
||||||
|
|
||||||
-- | For now, none of the architecture-specific statements have an effect on the
|
-- | For now, none of the architecture-specific statements have an effect on the
|
||||||
-- abstract value.
|
-- abstract value.
|
||||||
|
@ -111,6 +111,9 @@ specialSemanticsCases :: [MatchQ]
|
|||||||
specialSemanticsCases =
|
specialSemanticsCases =
|
||||||
[ match (conP 'D.SC []) (normalB syscallBody) []
|
[ match (conP 'D.SC []) (normalB syscallBody) []
|
||||||
, match (conP 'D.TRAP []) (normalB trapBody) []
|
, match (conP 'D.TRAP []) (normalB trapBody) []
|
||||||
|
, match (conP 'D.ATTN []) (normalB [| Just (addStmt (M.ExecArchStmt Attn)) |]) []
|
||||||
|
, match (conP 'D.SYNC []) (normalB [| Just (addStmt (M.ExecArchStmt Sync)) |]) []
|
||||||
|
, match (conP 'D.ISYNC []) (normalB [| Just (addStmt (M.ExecArchStmt Isync)) |]) []
|
||||||
]
|
]
|
||||||
where
|
where
|
||||||
syscallBody = [| Just (finishWithTerminator (M.ArchTermStmt PPCSyscall)) |]
|
syscallBody = [| Just (finishWithTerminator (M.ArchTermStmt PPCSyscall)) |]
|
||||||
@ -727,6 +730,20 @@ crucAppToExprTH elt interps = case elt of
|
|||||||
bval2 <- $(addEltTH interps bv2)
|
bval2 <- $(addEltTH interps bv2)
|
||||||
return (AppExpr (M.BVMul rep bval1 bval2))
|
return (AppExpr (M.BVMul rep bval1 bval2))
|
||||||
|]
|
|]
|
||||||
|
S.BVSdiv w bv1 bv2 ->
|
||||||
|
[| do let rep = $(natReprTH w)
|
||||||
|
bval1 <- $(addEltTH interps bv1)
|
||||||
|
bval2 <- $(addEltTH interps bv2)
|
||||||
|
let divExp = SDiv rep bval1 bval2
|
||||||
|
(ValueExpr . M.AssignedValue) <$> addAssignment (M.EvalArchFn divExp (M.typeRepr divExp))
|
||||||
|
|]
|
||||||
|
S.BVUdiv w bv1 bv2 ->
|
||||||
|
[| do let rep = $(natReprTH w)
|
||||||
|
bval1 <- $(addEltTH interps bv1)
|
||||||
|
bval2 <- $(addEltTH interps bv2)
|
||||||
|
let divExp = UDiv rep bval1 bval2
|
||||||
|
(ValueExpr . M.AssignedValue) <$> addAssignment (M.EvalArchFn divExp (M.typeRepr divExp))
|
||||||
|
|]
|
||||||
S.BVShl w bv1 bv2 ->
|
S.BVShl w bv1 bv2 ->
|
||||||
[| do let rep = $(natReprTH w)
|
[| do let rep = $(natReprTH w)
|
||||||
bval1 <- $(addEltTH interps bv1)
|
bval1 <- $(addEltTH interps bv1)
|
||||||
|
@ -1 +1 @@
|
|||||||
Subproject commit 19dcdeed7fdc07f02197a6fb4ad590b7e9969db1
|
Subproject commit 2e5ce7f6797466c09cd9e5799a351aaa16016a12
|
Loading…
Reference in New Issue
Block a user