Safe Haskell | None |
---|---|
Language | Haskell98 |
This module calculates an abstract control graph by evaluating a CPSScheme program, following the definitions in Olin Shivers' "Control-Flow Analysis of Higher-Order Languages".
- type Closure c = (Lambda, BEnv c)
- class (Show c, Eq c, Ord c) => Contour c where
- newtype CFA0 = CFA0 ()
- newtype CFA1 = CFA1 Label
- type BEnv c = Label :⇀ c
- type VEnv c = (Var :× c) :⇀ D c
- data Proc c
- type D c = [Proc c]
- type CCtxt c = Label :× BEnv c
- type CCache c = CCtxt c :⇀ D c
- type Ans c = CCache c
- type FState c = (Proc c, [D c], VEnv c, c)
- type CState c = (Call, BEnv c, VEnv c, c)
- type Memo c = Set (Either (FState c) (CState c))
- evalCPS :: Contour c => Prog -> Ans c
- evalCPS_CFA0 :: Prog -> Ans CFA0
- evalCPS_CFA1 :: Prog -> Ans CFA1
- evalV :: Contour c => Val -> BEnv c -> VEnv c -> D c
- evalF :: Contour c => FState c -> State (Memo c) (Ans c)
- evalC :: Contour c => CState c -> State (Memo c) (Ans c)
- graphToEdgelist :: Show c => Ans c -> [Label :× Label]
Types
type Closure c = (Lambda, BEnv c) Source
A closure is a lambda expression bound to a binding environment
class (Show c, Eq c, Ord c) => Contour c where Source
The abstract semantics are parametrized by a (finite) set of contours. Here, this is modeled via a type class.
:: c | The initial contour, used by evalCPS, but not used |
:: c | |
-> Label | |
-> c | Generating a new contour. This method has access to the label of the current call site, in case it wants to record this information. |
A possible contour set, the singleton set. Shivers calls this 0CFA, but in Haskell, types and constructor names have to start with an upper case letter.
CFA0 () |
A more detailed contour set, remembering the call site.
type VEnv c = (Var :× c) :⇀ D c Source
A variable environment maps variable names together with a contour to a value. The second parameter is required to allow for different, shadowed bindings of the same variable to coexist.
Here, we do not care about values any more, only about procedures:
For variables, we only remember the set of possible program values. We use a list here instead of a set for the more convenient sytanx (list comprehension etc.).
type CCtxt c = Label :× BEnv c Source
The origin of an edge in the control graph is a call position bundled with the binding environment at that point.
type CCache c = CCtxt c :⇀ D c Source
The resulting control flow graph has edges from call sites (annotated by
the current binding environment) to functions (e.g. lambdas with closure,
primitive operations, or Stop
)
The result of evaluating a program is an approximation to the control flow graph.
type Memo c = Set (Either (FState c) (CState c)) Source
We need memoization. This Data structure is used to remember all visited arguments
Evaluation functions
evalCPS :: Contour c => Prog -> Ans c Source
evalCPS evaluates a whole program, by initializing the envirnoments and passing the Stop continuation to the outermost lambda
evalCPS_CFA0 :: Prog -> Ans CFA0 Source
Variants fixing the coutour
evalCPS_CFA1 :: Prog -> Ans CFA1 Source
evalV :: Contour c => Val -> BEnv c -> VEnv c -> D c Source
evalC (called A by Shivers) evaluates a syntactical value to a semantical piece of data.
evalF :: Contour c => FState c -> State (Memo c) (Ans c) Source
evalF evaluates a function call, distinguishing between lambda
expressions, primitive operations and the special Stop continuation. It
calles evalC
for the function bodies.
Because we want to memoize the results of the recursive calls, and do not want to separate that code, the that to be