mirror of
https://github.com/GaloisInc/macaw.git
synced 2024-12-29 17:17:05 +03:00
Generalize ArchFn result type.
This commit is contained in:
parent
5617cd1429
commit
8a70d9aee4
@ -4,6 +4,7 @@ Maintainer : jhendrix@galois.com
|
|||||||
|
|
||||||
This defines the architecture-specific information needed for code discovery.
|
This defines the architecture-specific information needed for code discovery.
|
||||||
-}
|
-}
|
||||||
|
{-# LANGUAGE FlexibleContexts #-}
|
||||||
{-# LANGUAGE RankNTypes #-}
|
{-# LANGUAGE RankNTypes #-}
|
||||||
module Data.Macaw.Architecture.Info
|
module Data.Macaw.Architecture.Info
|
||||||
( ArchitectureInfo(..)
|
( ArchitectureInfo(..)
|
||||||
@ -75,7 +76,7 @@ data ArchitectureInfo arch
|
|||||||
-- The address is the entry point of the function.
|
-- The address is the entry point of the function.
|
||||||
, absEvalArchFn :: !(forall ids tp
|
, absEvalArchFn :: !(forall ids tp
|
||||||
. AbsProcessorState (ArchReg arch) ids
|
. AbsProcessorState (ArchReg arch) ids
|
||||||
-> ArchFn arch ids tp
|
-> ArchFn arch (Value arch ids) tp
|
||||||
-> AbsValue (RegAddrWidth (ArchReg arch)) tp)
|
-> AbsValue (RegAddrWidth (ArchReg arch)) tp)
|
||||||
-- ^ Evaluates an architecture-specific function
|
-- ^ Evaluates an architecture-specific function
|
||||||
, absEvalArchStmt :: !(forall ids
|
, absEvalArchStmt :: !(forall ids
|
||||||
@ -109,7 +110,9 @@ data ArchitectureInfo arch
|
|||||||
-- should return 'Just stmts' if this code looks like a function return.
|
-- should return 'Just stmts' if this code looks like a function return.
|
||||||
-- The stmts should be a subset of the statements, but may remove unneeded memory
|
-- The stmts should be a subset of the statements, but may remove unneeded memory
|
||||||
-- accesses like reading the stack pointer.
|
-- accesses like reading the stack pointer.
|
||||||
, rewriteArchFn :: (forall src tgt tp . ArchFn arch src tp -> Rewriter arch src tgt (Value arch tgt tp))
|
, rewriteArchFn :: (forall src tgt tp
|
||||||
|
. ArchFn arch (Value arch src) tp
|
||||||
|
-> Rewriter arch src tgt (Value arch tgt tp))
|
||||||
-- ^ This rewrites an architecture specific statement
|
-- ^ This rewrites an architecture specific statement
|
||||||
, rewriteArchStmt :: (forall src tgt . ArchStmt arch src -> Rewriter arch src tgt ())
|
, rewriteArchStmt :: (forall src tgt . ArchStmt arch src -> Rewriter arch src tgt ())
|
||||||
-- ^ This rewrites an architecture specific statement
|
-- ^ This rewrites an architecture specific statement
|
||||||
|
@ -7,12 +7,12 @@ Defines data types needed to represent values, assignments, and statements from
|
|||||||
This is a low-level CFG representation where the entire program is a
|
This is a low-level CFG representation where the entire program is a
|
||||||
single CFG.
|
single CFG.
|
||||||
-}
|
-}
|
||||||
|
{-# LANGUAGE ConstraintKinds #-}
|
||||||
{-# LANGUAGE DataKinds #-}
|
{-# LANGUAGE DataKinds #-}
|
||||||
{-# LANGUAGE FlexibleContexts #-}
|
{-# LANGUAGE FlexibleContexts #-}
|
||||||
{-# LANGUAGE FlexibleInstances #-}
|
{-# LANGUAGE FlexibleInstances #-}
|
||||||
{-# LANGUAGE GADTs #-}
|
{-# LANGUAGE GADTs #-}
|
||||||
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
|
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
|
||||||
{-# LANGUAGE KindSignatures #-}
|
|
||||||
{-# LANGUAGE MultiParamTypeClasses #-}
|
{-# LANGUAGE MultiParamTypeClasses #-}
|
||||||
{-# LANGUAGE PatternGuards #-}
|
{-# LANGUAGE PatternGuards #-}
|
||||||
{-# LANGUAGE PolyKinds #-}
|
{-# LANGUAGE PolyKinds #-}
|
||||||
@ -56,7 +56,7 @@ module Data.Macaw.CFG.Core
|
|||||||
, ppValue
|
, ppValue
|
||||||
, ppStmt
|
, ppStmt
|
||||||
, PrettyF(..)
|
, PrettyF(..)
|
||||||
, ArchConstraints(..)
|
, ArchConstraints
|
||||||
, PrettyRegValue(..)
|
, PrettyRegValue(..)
|
||||||
-- * Architecture type families
|
-- * Architecture type families
|
||||||
, ArchFn
|
, ArchFn
|
||||||
@ -70,16 +70,17 @@ module Data.Macaw.CFG.Core
|
|||||||
, asStackAddrOffset
|
, asStackAddrOffset
|
||||||
-- * References
|
-- * References
|
||||||
, StmtHasRefs(..)
|
, StmtHasRefs(..)
|
||||||
, FnHasRefs(..)
|
|
||||||
, refsInValue
|
, refsInValue
|
||||||
, refsInApp
|
, refsInApp
|
||||||
, refsInAssignRhs
|
, refsInAssignRhs
|
||||||
|
, IsArchFn(..)
|
||||||
-- ** Synonyms
|
-- ** Synonyms
|
||||||
, ArchAddrWidth
|
, ArchAddrWidth
|
||||||
, ArchAddrValue
|
, ArchAddrValue
|
||||||
, ArchAddrWord
|
, ArchAddrWord
|
||||||
, ArchMemAddr
|
, ArchMemAddr
|
||||||
, ArchSegmentOff
|
, ArchSegmentOff
|
||||||
|
, Data.Parameterized.TraversableFC.FoldableFC(..)
|
||||||
) where
|
) where
|
||||||
|
|
||||||
import Control.Exception (assert)
|
import Control.Exception (assert)
|
||||||
@ -96,6 +97,7 @@ import Data.Parameterized.NatRepr
|
|||||||
import Data.Parameterized.Nonce
|
import Data.Parameterized.Nonce
|
||||||
import Data.Parameterized.Some
|
import Data.Parameterized.Some
|
||||||
import Data.Parameterized.TraversableF
|
import Data.Parameterized.TraversableF
|
||||||
|
import Data.Parameterized.TraversableFC (FoldableFC(..))
|
||||||
import Data.Proxy
|
import Data.Proxy
|
||||||
import Data.Set (Set)
|
import Data.Set (Set)
|
||||||
import qualified Data.Set as Set
|
import qualified Data.Set as Set
|
||||||
@ -192,7 +194,7 @@ type family ArchReg (arch :: *) :: Type -> *
|
|||||||
--
|
--
|
||||||
-- The function may depend on the set of registers defined so far, and the type
|
-- The function may depend on the set of registers defined so far, and the type
|
||||||
-- of the result.
|
-- of the result.
|
||||||
type family ArchFn (arch :: *) :: * -> Type -> *
|
type family ArchFn (arch :: *) :: (Type -> *) -> Type -> *
|
||||||
|
|
||||||
-- | A type family for defining architecture-specific statements.
|
-- | A type family for defining architecture-specific statements.
|
||||||
--
|
--
|
||||||
@ -306,7 +308,7 @@ data AssignRhs (arch :: *) ids tp where
|
|||||||
-> AssignRhs arch ids tp
|
-> AssignRhs arch ids tp
|
||||||
|
|
||||||
-- Call an architecture specific function that returns some result.
|
-- Call an architecture specific function that returns some result.
|
||||||
EvalArchFn :: !(ArchFn arch ids tp)
|
EvalArchFn :: !(ArchFn arch (Value arch ids) tp)
|
||||||
-> !(TypeRepr tp)
|
-> !(TypeRepr tp)
|
||||||
-> AssignRhs arch ids tp
|
-> AssignRhs arch ids tp
|
||||||
|
|
||||||
@ -558,17 +560,13 @@ instance RegisterInfo (ArchReg arch) => Pretty (Value arch ids tp) where
|
|||||||
instance RegisterInfo (ArchReg arch) => Show (Value arch ids tp) where
|
instance RegisterInfo (ArchReg arch) => Show (Value arch ids tp) where
|
||||||
show = show . pretty
|
show = show . pretty
|
||||||
|
|
||||||
class ( RegisterInfo (ArchReg arch)
|
type ArchConstraints arch
|
||||||
|
= ( RegisterInfo (ArchReg arch)
|
||||||
, PrettyF (ArchStmt arch)
|
, PrettyF (ArchStmt arch)
|
||||||
, PrettyF (ArchTermStmt arch)
|
, PrettyF (ArchTermStmt arch)
|
||||||
) => ArchConstraints arch where
|
, FoldableFC (ArchFn arch)
|
||||||
|
, IsArchFn (ArchFn arch)
|
||||||
-- | A function for pretty printing an archFn of a given type.
|
)
|
||||||
ppArchFn :: Applicative m
|
|
||||||
=> (forall u . Value arch ids u -> m Doc)
|
|
||||||
-- ^ Function for pretty printing vlaue.
|
|
||||||
-> ArchFn arch ids tp
|
|
||||||
-> m Doc
|
|
||||||
|
|
||||||
-- | Pretty print an assignment right-hand side using operations parameterized
|
-- | Pretty print an assignment right-hand side using operations parameterized
|
||||||
-- over an application to allow side effects.
|
-- over an application to allow side effects.
|
||||||
@ -603,7 +601,7 @@ collectValueRep :: forall arch ids tp
|
|||||||
=> Prec
|
=> Prec
|
||||||
-> Value arch ids tp
|
-> Value arch ids tp
|
||||||
-> State (MapF (AssignId ids) DocF) Doc
|
-> State (MapF (AssignId ids) DocF) Doc
|
||||||
collectValueRep _ (AssignedValue a :: Value arch ids tp) = do
|
collectValueRep _ (AssignedValue a) = do
|
||||||
let lhs = assignId a
|
let lhs = assignId a
|
||||||
mr <- gets $ MapF.lookup lhs
|
mr <- gets $ MapF.lookup lhs
|
||||||
when (isNothing mr) $ do
|
when (isNothing mr) $ do
|
||||||
@ -721,9 +719,14 @@ instance ArchConstraints arch => Show (Stmt arch ids) where
|
|||||||
class StmtHasRefs f where
|
class StmtHasRefs f where
|
||||||
refsInStmt :: f ids -> Set (Some (AssignId ids))
|
refsInStmt :: f ids -> Set (Some (AssignId ids))
|
||||||
|
|
||||||
-- | Return refernces in a function type.
|
-- | Typeclass for folding over architecture-specific values.
|
||||||
class FnHasRefs (f :: * -> Type -> *) where
|
class IsArchFn (f :: (k -> *) -> k -> *) where
|
||||||
refsInFn :: f ids tp -> Set (Some (AssignId ids))
|
-- | A function for pretty printing an archFn of a given type.
|
||||||
|
ppArchFn :: Applicative m
|
||||||
|
=> (forall u . v u -> m Doc)
|
||||||
|
-- ^ Function for pretty printing vlaue.
|
||||||
|
-> f v tp
|
||||||
|
-> m Doc
|
||||||
|
|
||||||
refsInValue :: Value arch ids tp -> Set (Some (AssignId ids))
|
refsInValue :: Value arch ids tp -> Set (Some (AssignId ids))
|
||||||
refsInValue (AssignedValue (Assignment v _)) = Set.singleton (Some v)
|
refsInValue (AssignedValue (Assignment v _)) = Set.singleton (Some v)
|
||||||
@ -732,7 +735,7 @@ refsInValue _ = Set.empty
|
|||||||
refsInApp :: App (Value arch ids) tp -> Set (Some (AssignId ids))
|
refsInApp :: App (Value arch ids) tp -> Set (Some (AssignId ids))
|
||||||
refsInApp app = foldApp refsInValue app
|
refsInApp app = foldApp refsInValue app
|
||||||
|
|
||||||
refsInAssignRhs :: FnHasRefs (ArchFn arch)
|
refsInAssignRhs :: FoldableFC (ArchFn arch)
|
||||||
=> AssignRhs arch ids tp
|
=> AssignRhs arch ids tp
|
||||||
-> Set (Some (AssignId ids))
|
-> Set (Some (AssignId ids))
|
||||||
refsInAssignRhs rhs =
|
refsInAssignRhs rhs =
|
||||||
@ -740,4 +743,4 @@ refsInAssignRhs rhs =
|
|||||||
EvalApp v -> refsInApp v
|
EvalApp v -> refsInApp v
|
||||||
SetUndefined _ -> Set.empty
|
SetUndefined _ -> Set.empty
|
||||||
ReadMem v _ -> refsInValue v
|
ReadMem v _ -> refsInValue v
|
||||||
EvalArchFn f _ -> refsInFn f
|
EvalArchFn f _ -> foldMapFC refsInValue f
|
||||||
|
@ -28,8 +28,8 @@ type AssignIdSet ids = Set (Some (AssignId ids))
|
|||||||
-- resolve demand sets.
|
-- resolve demand sets.
|
||||||
data DemandContext arch ids
|
data DemandContext arch ids
|
||||||
= DemandContext { addArchStmtDemands :: !(ArchStmt arch ids -> DemandComp arch ids ())
|
= DemandContext { addArchStmtDemands :: !(ArchStmt arch ids -> DemandComp arch ids ())
|
||||||
, addArchFnDemands :: !(forall tp . ArchFn arch ids tp -> DemandComp arch ids ())
|
, addArchFnDemands :: !(forall tp . ArchFn arch (Value arch ids) tp -> DemandComp arch ids ())
|
||||||
, archFnHasSideEffects :: !(forall tp . ArchFn arch ids tp -> Bool)
|
, archFnHasSideEffects :: !(forall v tp . ArchFn arch v tp -> Bool)
|
||||||
-- ^ This returns true if the architecture function has implicit
|
-- ^ This returns true if the architecture function has implicit
|
||||||
-- side effects (and thus can be safely removed).
|
-- side effects (and thus can be safely removed).
|
||||||
}
|
}
|
||||||
|
@ -40,7 +40,7 @@ data RewriteContext arch src tgt
|
|||||||
= RewriteContext { rwctxNonceGen :: !(NonceGenerator (ST tgt) tgt)
|
= RewriteContext { rwctxNonceGen :: !(NonceGenerator (ST tgt) tgt)
|
||||||
-- ^ Generator for making new nonces in the target ST monad
|
-- ^ Generator for making new nonces in the target ST monad
|
||||||
, rwctxArchFn :: !(forall tp
|
, rwctxArchFn :: !(forall tp
|
||||||
. ArchFn arch src tp
|
. ArchFn arch (Value arch src) tp
|
||||||
-> Rewriter arch src tgt (Value arch tgt tp))
|
-> Rewriter arch src tgt (Value arch tgt tp))
|
||||||
-- ^ Rewriter for architecture-specific statements
|
-- ^ Rewriter for architecture-specific statements
|
||||||
, rwctxArchStmt :: !(ArchStmt arch src -> Rewriter arch src tgt ())
|
, rwctxArchStmt :: !(ArchStmt arch src -> Rewriter arch src tgt ())
|
||||||
@ -105,8 +105,8 @@ evalRewrittenRhs rhs = Rewriter $ do
|
|||||||
pure $! AssignedValue a
|
pure $! AssignedValue a
|
||||||
|
|
||||||
-- | Add an assignment statement that evaluates the architecture function.
|
-- | Add an assignment statement that evaluates the architecture function.
|
||||||
evalRewrittenArchFn :: HasRepr (ArchFn arch tgt) TypeRepr
|
evalRewrittenArchFn :: HasRepr (ArchFn arch (Value arch tgt)) TypeRepr
|
||||||
=> ArchFn arch tgt tp
|
=> ArchFn arch (Value arch tgt) tp
|
||||||
-> Rewriter arch src tgt (Value arch tgt tp)
|
-> Rewriter arch src tgt (Value arch tgt tp)
|
||||||
evalRewrittenArchFn f = evalRewrittenRhs (EvalArchFn f (typeRepr f))
|
evalRewrittenArchFn f = evalRewrittenRhs (EvalArchFn f (typeRepr f))
|
||||||
|
|
||||||
|
@ -6,11 +6,12 @@ This module provides a function for folding over the subexpressions in
|
|||||||
a value without revisiting shared subterms.
|
a value without revisiting shared subterms.
|
||||||
-}
|
-}
|
||||||
{-# LANGUAGE DataKinds #-}
|
{-# LANGUAGE DataKinds #-}
|
||||||
|
{-# LANGUAGE FlexibleContexts #-}
|
||||||
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
|
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
|
||||||
{-# LANGUAGE RankNTypes #-}
|
{-# LANGUAGE RankNTypes #-}
|
||||||
{-# LANGUAGE ScopedTypeVariables #-}
|
{-# LANGUAGE ScopedTypeVariables #-}
|
||||||
module Data.Macaw.Fold
|
module Data.Macaw.Fold
|
||||||
( CanFoldValues(..)
|
( Data.Parameterized.TraversableFC.FoldableFC(..)
|
||||||
, foldValueCached
|
, foldValueCached
|
||||||
) where
|
) where
|
||||||
|
|
||||||
@ -19,6 +20,7 @@ import Data.Map.Strict (Map)
|
|||||||
import qualified Data.Map.Strict as Map
|
import qualified Data.Map.Strict as Map
|
||||||
import Data.Parameterized.NatRepr
|
import Data.Parameterized.NatRepr
|
||||||
import Data.Parameterized.Some
|
import Data.Parameterized.Some
|
||||||
|
import Data.Parameterized.TraversableFC
|
||||||
|
|
||||||
import Data.Macaw.CFG
|
import Data.Macaw.CFG
|
||||||
|
|
||||||
@ -32,15 +34,7 @@ instance Monoid m => Monoid (StateMonadMonoid s m) where
|
|||||||
mempty = return mempty
|
mempty = return mempty
|
||||||
mappend m m' = mappend <$> m <*> m'
|
mappend m m' = mappend <$> m <*> m'
|
||||||
|
|
||||||
-- | Typeclass for folding over architecture-specific values.
|
foldAssignRHSValues :: (Monoid r, FoldableFC (ArchFn arch))
|
||||||
class CanFoldValues arch where
|
|
||||||
-- | Folding over ArchFn values
|
|
||||||
foldFnValues :: Monoid r
|
|
||||||
=> (forall vtp . Value arch ids vtp -> r)
|
|
||||||
-> ArchFn arch ids tp
|
|
||||||
-> r
|
|
||||||
|
|
||||||
foldAssignRHSValues :: (Monoid r, CanFoldValues arch)
|
|
||||||
=> (forall vtp . Value arch ids vtp -> r)
|
=> (forall vtp . Value arch ids vtp -> r)
|
||||||
-> AssignRhs arch ids tp
|
-> AssignRhs arch ids tp
|
||||||
-> r
|
-> r
|
||||||
@ -49,14 +43,14 @@ foldAssignRHSValues go v =
|
|||||||
EvalApp a -> foldApp go a
|
EvalApp a -> foldApp go a
|
||||||
SetUndefined _w -> mempty
|
SetUndefined _w -> mempty
|
||||||
ReadMem addr _ -> go addr
|
ReadMem addr _ -> go addr
|
||||||
EvalArchFn f _ -> foldFnValues go f
|
EvalArchFn f _ -> foldMapFC go f
|
||||||
|
|
||||||
-- | This folds over elements of a values in a values.
|
-- | This folds over elements of a values in a values.
|
||||||
--
|
--
|
||||||
-- It memoizes values so that it only evaluates assignments with the same id
|
-- It memoizes values so that it only evaluates assignments with the same id
|
||||||
-- once.
|
-- once.
|
||||||
foldValueCached :: forall m arch ids tp
|
foldValueCached :: forall m arch ids tp
|
||||||
. (Monoid m, CanFoldValues arch)
|
. (Monoid m, FoldableFC (ArchFn arch))
|
||||||
=> (forall n. NatRepr n -> Integer -> m)
|
=> (forall n. NatRepr n -> Integer -> m)
|
||||||
-- ^ Function for literals
|
-- ^ Function for literals
|
||||||
-> (ArchMemAddr arch -> m)
|
-> (ArchMemAddr arch -> m)
|
||||||
|
Loading…
Reference in New Issue
Block a user