AbsCF

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".

Types

type Closure c = (Lambda, BEnv c)

A closure is a lambda expression bound to a binding environment

class (Show c, Eq c, Ord c) => Contour c where

The abstract semantics are parametrized by a (finite) set of contours. Here, this is modeled via a type class.

Methods

initial

Arguments

:: c

The initial contour, used by evalCPS, but not used

nb

Arguments

:: 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.

Instances

Contour CFA1

Contour CFA0

newtype CFA0

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.

Constructors

CFA0 ()

Instances

Eq CFA0

Ord CFA0

Show CFA0

Contour CFA0

newtype CFA1

A more detailed contour set, remembering the call site.

Constructors

CFA1 Label

Instances

Eq CFA1

Ord CFA1

Show CFA1

Contour CFA1

type BEnv c = Label :⇀ c

A binding environment maps the labels of Lambda and Let bindings to the innermost contour generated for these expressions

type VEnv c = (Var :× c) :⇀ D c

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.

data Proc c

Here, we do not care about values any more, only about procedures:

Constructors

PC (Closure c)

A closed lambda expression

PP Prim

A primitive operation

Stop

Instances

Eq c => Eq (Proc c)

Ord c => Ord (Proc c)

Show c => Show (Proc c)

type D c = [Proc c]

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

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

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)

type Ans c = CCache c

The result of evaluating a program is an approximation to the control flow graph.

type FState c = (Proc c, [D c], VEnv c, c)

The uncurried arguments of evalF

type CState c = (Call, BEnv c, VEnv c, c)

The uncurried arguments of evalC

type Memo c = Set (Either (FState c) (CState c))

We need memoization. This Data structure is used to remember all visited arguments

Evaluation functions

evalCPS :: Contour c => Prog -> Ans c

evalCPS evaluates a whole program, by initializing the envirnoments and passing the Stop continuation to the outermost lambda

evalCPS_CFA0 :: Prog -> Ans CFA0

Variants fixing the coutour

evalCPS_CFA1 :: Prog -> Ans CFA1

evalV :: Contour c => Val -> BEnv c -> VEnv c -> D c

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)

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

evalC :: Contour c => CState c -> State (Memo c) (Ans c)

evalC evaluates the body of a function, which can either be an application (which is then evaluated using evalF) or a Let statement.

graphToEdgelist :: Show c => Ans c -> [Label :× Label]

For the visualization, we need a list of edges from Label to Label. TODO: Handle STOP