shivers-cfg (empty) → 0.1
raw patch · 9 files changed
+911/−0 lines, 9 filesdep +HPDFdep +basedep +containerssetup-changed
Dependencies added: HPDF, base, containers, directory, language-dot, mtl, pretty, process
Files
- AbsCF.hs +181/−0
- CFGraph.hs +124/−0
- CPSPrint.hs +130/−0
- CPSScheme.hs +211/−0
- Eval.hs +96/−0
- ExCF.hs +108/−0
- LICENSE +30/−0
- Setup.hs +3/−0
- shivers-cfg.cabal +28/−0
+ AbsCF.hs view
@@ -0,0 +1,181 @@+{-|+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\".+ -}+{-# LANGUAGE TypeOperators #-}+module AbsCF where++import Data.Map (empty, unions, fromList, toList, (!))+import Control.Monad.State+import Control.Applicative ((<$>))+import Data.Set (Set)+import qualified Data.Set as S++import CPSScheme+import Common++-- * Types++-- | A closure is a lambda expression bound to a binding environment+type Closure c = (Lambda, BEnv c)++-- | The abstract semantics are parametrized by a (finite) set of contours.+-- Here, this is modeled via a type class.+class (Show c, Eq c, Ord c) => Contour c where+ initial :: c -- ^ The initial contour, used by evalCPS, but not used+ nb :: 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.+newtype CFA0 = CFA0 ()+ deriving (Show, Eq, Ord)++instance Contour CFA0 where+ initial = CFA0 ()+ nb _ _ = CFA0 ()++-- | A more detailed contour set, remembering the call site. +newtype CFA1 = CFA1 Label+ deriving (Show, Eq, Ord)++instance Contour CFA1 where+ initial = CFA1 (-1)+ nb _ l = CFA1 l++-- | A binding environment maps the labels of 'Lambda' and 'Let' bindings to the+-- innermost contour generated for these expressions+type BEnv c = Label :⇀ 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.+type VEnv c = Var :× c :⇀ D c++-- | Here, we do not care about values any more, only about procedures:+data Proc c = PC (Closure c) -- ^ A closed lambda expression+ | PP Prim -- ^ A primitive operation+ | Stop+ deriving (Show, Eq, Ord)+++-- | 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 D c = [Proc c]++-- | The origin of an edge in the control graph is a call position bundled with+-- the binding environment at that point.+type CCtxt c = Label :× BEnv 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 CCache c = CCtxt c :⇀ D c++-- | The result of evaluating a program is an approximation to the control flow+-- graph.+type Ans c = CCache c++-- | The uncurried arguments of 'evalF'+type FState c = (Proc c, [D c], VEnv c, c)++-- | The uncurried arguments of 'evalC'+type CState c = (Call, BEnv c, VEnv c, c)++-- | We need memoization. This Data structure is used to remember all visited+-- arguments+type Memo c = Set (Either (FState c) (CState c))+++-- * Evaluation functions++-- | evalCPS evaluates a whole program, by initializing the envirnoments and+-- passing the Stop continuation to the outermost lambda+evalCPS :: Contour c => Prog -> Ans c+evalCPS lam = evalState (evalF (f, [[Stop]], ve, initial)) S.empty+ where ve = empty+ β = empty+ [f] = evalV (L lam) β ve++-- | Variants fixing the coutour+evalCPS_CFA0 :: Prog -> Ans CFA0+evalCPS_CFA0 = evalCPS++evalCPS_CFA1 :: Prog -> Ans CFA1+evalCPS_CFA1 = evalCPS++-- | evalC (called A by Shivers) evaluates a syntactical value to a semantical+-- piece of data.+evalV :: Contour c => Val -> BEnv c -> VEnv c -> D c+evalV (C _ int) β ve = []+evalV (P prim) β ve = [PP prim]+evalV (R _ var) β ve = ve ! (var, β ! binder var)+evalV (L lam) β ve = [PC (lam, β)]++-- | 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 +evalF :: Contour c => FState c -> State (Memo c) (Ans c)+evalF args = do+ seen <- gets (S.member (Left args))+ if seen then return empty else do+ modify (S.insert (Left args))+ case args of+ (PC (Lambda lab vs c, β), as, ve, b)+ -> if (length as /= length vs)+ then error $ "Wrong number of arguments to lambda expression " ++ show lab+ else evalC (c,β',ve',b)+ where β' = β `upd` [lab ↦ b]+ ve' = ve `upd` zipWith (\v a -> (v,b) ↦ a) vs as+ (PP (Plus c), [_, _, conts], ve, b)+ -> unionsM [ evalF (cont,[[]],ve,b') | cont <- conts ] `upd'` [ (c, β) ↦ conts ]+ where b' = nb b c+ β = empty `upd` [ c ↦ b ]+ (PP (If ct cf), [_, contt, contf], ve, b)+ -> unionsM (+ [ evalF (cont,[],ve,bt') | cont <- contt ] +++ [ evalF (cont,[],ve,bf') | cont <- contf ] )+ `upd'` [ (ct, βt) ↦ contt, (cf, βf) ↦ contf ]+ where bt' = nb b ct+ bf' = nb b cf+ βt = empty `upd` [ ct ↦ b ]+ βf = empty `upd` [ cf ↦ b ]+ (Stop,[_],_,_) -> return empty + (Stop,_,_,_) -> error $ "Stop called with wrong number or types of arguments"+ (PP prim,_,_,_) -> error $ "Primop " ++ show prim ++ " called with wrong arguments"++-- | evalC evaluates the body of a function, which can either be an application+-- (which is then evaluated using 'evalF') or a 'Let' statement.+evalC :: Contour c => CState c -> State (Memo c) (Ans c)+evalC args = do+ seen <- gets (S.member (Right args))+ if seen then return empty else do+ modify (S.insert (Right args))+ case args of+ (App lab f vs, β, ve, b)+ -> unionsM [evalF (f',as,ve,b') | f' <- fs ] `upd'` [ (lab,β) ↦ fs ]+ where fs = evalV f β ve+ as = map (\v -> evalV v β ve) vs+ b' = nb b lab+ (Let lab ls c', β, ve, b)+ -> evalC (c',β',ve',b')+ where b' = nb b lab+ β' = β `upd` [lab ↦ b']+ ve' = ve `upd` [(v,b') ↦ evalV (L l) β' ve | (v,l) <- ls]++-- | For the visualization, we need a list of edges from Label to Label. TODO: Handle STOP+graphToEdgelist :: Show c => Ans c -> [Label :× Label]+graphToEdgelist = concat . map go . toList+ where go ((l,_),ds) = concat $ map go' ds+ where go' Stop = []+ go' (PP (Plus l')) = [(l,l')]+ go' (PP (If l' _)) = [(l,l')]+ go' (PC (Lambda l' _ _ , _)) = [(l,l')]+
+ CFGraph.hs view
@@ -0,0 +1,124 @@+{- |+ Generates a visual representation of a control flow graph, by overlaying a+ pretty-printed syntax output with a graphviz-generated graph.++ This code uses the command line tools \"neato\", \"pdf2ps\" and \"pdftk\".+ -}+{-# LANGUAGE TypeOperators #-}+module CFGraph where++import Graphics.PDF+import Language.Dot+import Data.Map (keys,(!))+import Text.Printf+import System.Process+import System.Directory+import System.IO++import CPSScheme+import CPSPrint+import Common++-- | The font that is used to generate the code listings.+font :: PDFFont+font = PDFFont Courier 11++-- | Assuming a mono-spaced font, this is the width of a character.+theCharWidth :: PDFFloat+theCharWidth = charWidth font 'M'++-- | The height of a character.+theCharHeight :: PDFFloat+theCharHeight = getHeight font++-- | Creates a PDF file containing the given text, without any padding or+-- borders, using the font specified by 'font'+renderCodeToFile :: FilePath -> String -> IO ()+renderCodeToFile fn code = do+ runPdf fn standardDocInfo pageRect $ do+ page <- addPage Nothing+ drawWithPage page $ sequence $+ zipWith (\ln line -> drawText $ text font 0 (fromIntegral ln * theCharHeight) (toPDFString line))+ [lineNumber-1,lineNumber-2..0] ls+ where ls = lines (removeLambdas code)+ lineLength = maximum (map length ls) + lineNumber = length ls+ pageWidth = ceiling (fromIntegral lineLength * theCharWidth)+ pageHeight = ceiling (fromIntegral lineNumber * theCharHeight)+ pageRect = PDFRect 0 0 pageWidth pageHeight++-- | Creates a 'Graph'+createDotFromGraph :: Integer -- ^ number of lines+ -> Integer -- ^ number of columns+ -> [Label :× Label] -- ^ the list of edges to draw+ -> (Label :⇀ (Integer, Integer)) -- ^ the position of the+ -- nodes, in characters+ -> Graph+createDotFromGraph ls cs edges coords = Graph UnstrictGraph DirectedGraph Nothing (settings ++ nodes ++ edges')+ where settings =+ [ AttributeStatement GraphAttributeStatement+ [ AttributeSetValue (NameId "bb")+ (StringId (printf "0,0,%.4f,%.4f" (width) (height)))+ , AttributeSetValue (NameId "pad") (StringId "0")+ , AttributeSetValue (NameId "splines") (StringId "true")+ ]+ , AttributeStatement NodeAttributeStatement+ [ AttributeSetValue (NameId "shape") (StringId "point") + , AttributeSetValue (NameId "height") (StringId "0.03") + ]+ , AttributeStatement EdgeAttributeStatement+ [ AttributeSetValue (NameId "penwidth") (StringId "0.4")+ , AttributeSetValue (NameId "arrowsize") (StringId "0.2")+ , AttributeSetValue (NameId "color") (StringId "#0000FF80")+ ]+ ]+ nodes = map (\l -> let (x,y) = charToPt (coords ! l) in NodeStatement (labelToId l)+ [ AttributeSetValue (NameId "pos")+ (StringId (printf "%.4f,%.4f" x y))+ ]+ ) (keys coords)+ edges' = map (\(l1,l2) -> EdgeStatement [+ ENodeId NoEdge (labelToId l1),+ ENodeId DirectedEdge (labelToId l2)+ ] []) edges+ labelToId (Label i) = NodeId (IntegerId i) Nothing+ charToPt (r,c) = ( (fromIntegral c-0.5) * theCharWidth,+ (fromIntegral (ls-r)+0.2) * theCharHeight )+ width = fromIntegral $ ceiling (fromIntegral cs * theCharWidth) :: Double+ height = fromIntegral $ ceiling (fromIntegral ls * theCharHeight) :: Double++-- | Creates a 'Graph' given a program and a function generating the required+-- graph+createDotFromCode :: (Prog -> [Label :× Label]) -> Prog -> Graph+createDotFromCode eval prog = createDotFromGraph lineNumber lineLength edges coords+ where edges = eval prog+ (coords, code) = labelPositions '*' $ renderProg True prog+ ls = lines (removeLambdas code)+ lineLength = fromIntegral $ maximum (map length ls) + lineNumber = fromIntegral $ length ls++-- | The main function of this module. Writes out a PDF file containing both+-- code and control flow graph+createCodeWithGraph :: (Prog -> [Label :× Label]) -- ^ Generating a graph from a program+ -> FilePath -- ^ Wanted filename + -> Prog -- ^ Program to draw+ -> IO ()+createCodeWithGraph eval filename prog = do+ renderCodeToFile codeFileName code + let neato = (proc "neato" ["-n","-s","-Tps2"]) { std_in = CreatePipe, std_out = CreatePipe } + (Just input, Just pipe, _ ,_) <- createProcess neato+ hPutStr input graph+ hClose input+ let ps2pdf = (proc "ps2pdf" ["-", graphFileName]) { std_in = UseHandle pipe, std_out = CreatePipe }+ (_ , _ , _, ph) <- createProcess ps2pdf+ waitForProcess ph+ let pdftk = proc "pdftk" [graphFileName, "background", codeFileName, "output", filename]+ (_ , _ , _, ph) <- createProcess pdftk+ waitForProcess ph+ removeFile graphFileName+ removeFile codeFileName+ where code = removeLambdas $ snd $ labelPositions ' ' $ renderProg True prog+ codeFileName = filename ++ ".tmp1.pdf"+ graphFileName = filename ++ ".tmp2.pdf"+ graph = renderDot $ createDotFromCode eval prog+
+ CPSPrint.hs view
@@ -0,0 +1,130 @@+{-|+ A Pretty printer for 'CPSScheme'-files and control flow.+ -}+{-# LANGUAGE TypeOperators #-}+module CPSPrint where++import Text.PrettyPrint+import Data.Char+import Control.Arrow ((***))+import Data.Map (unions, singleton)+import Data.Monoid++import CPSScheme+import Common++-- * Pretty printer for 'CPSScheme' programs, omitting any labels++-- | Pretty-Prints a whole document. The first flag, if set to true, embedds the+-- label information by abusing high range unicode characters.+ppProg :: Bool -> Prog -> Doc+ppProg el = ppLambda el++-- | Renders to a String+renderProg :: Bool -> Prog -> String+renderProg el = render . ppProg el++ppLambda :: Bool -> Lambda -> Doc+ppLambda el (Lambda l vs c) = parens $ + embeddLabel el l <> text "λ" <+> sep+ [ hsep (map (\(Var _ n) -> text n) vs) <> text "." + , ppCall el c+ ]++ppCall :: Bool -> Call -> Doc+ppCall el (App l (P (If lt lf)) [b,c1,c2]) = sep+ [ embeddLabel el l <> text "if" <+> ppVal el b+ , embeddLabel el lt <> text "then" <+> ppVal el c1+ , embeddLabel el lf <> text "else" <+> ppVal el c2+ ]+ppCall el (App l f as) =+ embeddLabel el l <> ppVal el f <+> sep (map (ppVal el) as)+ppCall el (Let l binds c) =+ embeddLabel el l <> text "let" <+> vcat (map ppBind binds) $$+ text "in" <+> ppCall el c+ where ppBind (Var _ n,l) = text n <+> text "=" $$ nest 6 (ppLambda el l)++ppVal :: Bool -> Val -> Doc+ppVal el (L l) = ppLambda el l+ppVal el (R _ (Var _ v)) = text v+ppVal el (C _ c) = integer c+ppVal el (P (Plus l)) = embeddLabel el l <> text "(+)"+ppVal el (P (If l _)) = embeddLabel el l <> text "if"++-- * Label embedding trick++-- | First unicode point to embed labels with (Private Use Area)+startAt :: Integer+startAt = 0x100000++labelToChar :: Label -> Char+labelToChar (Label i) = chr (fromIntegral (startAt + i))++charToLabel :: Char -> Maybe Label+charToLabel c = if i >= startAt then Just $ Label (i - startAt)+ else Nothing+ where i = fromIntegral (ord c) ++embeddLabel :: Bool -> Label -> Doc+embeddLabel False _ = empty+embeddLabel True l = char (labelToChar l)++-- | Given a replacement function and a string containing embedded labels, this+-- function replaces the labels by the given replacement character and+-- calculates a map of labels to positions in the text (1-based row and column+-- indexing)+labelPositions :: Char -> String -> (Label :⇀ (Integer, Integer), String)+labelPositions rep = (unions *** unlines) . unzip . zipWith labelLines [1..] . lines+ where labelLines :: Integer -> String -> (Label :⇀ (Integer, Integer), String)+ labelLines row = (unions *** id) . unzip . zipWith labelChar [1..]+ where labelChar :: Integer -> Char -> (Label :⇀ (Integer, Integer), Char)+ labelChar col c = case charToLabel c of+ Just l -> (l `singleton` (row,col), rep)+ Nothing -> (mempty, c)++-- | HPDF can not print lambdas. Therefore, replace them by backslashes.+removeLambdas :: String -> String+removeLambdas = map (\c -> if c == 'λ' then '\\' else c)++-- * Printing to Isablle-Expression++-- | Converts the whole program into an expression that can be copy'n'pasted+-- into an Isabelle source file+ipProg :: Prog -> Doc+ipProg = ipLambda++-- | Renders to a String+renderProgToIsa :: Prog -> String+renderProgToIsa = renderStyle myStyle . ipProg+ where myStyle = style { mode = OneLineMode }+++ipLambda :: Lambda -> Doc+ipLambda (Lambda (Label i) vs c) = parens $ + text "Lambda" <+> integer i <+> sep+ [ brackets $ hsep (punctuate (char ',') (map ipVar vs))+ , ipCall c+ ]+ipVar :: Var -> Doc+ipVar (Var (Label i) n) = parens $ integer i <> char ',' <>+ text "''" <> text (quote n) <> text "''"+ where quote = map (\c -> if c == '\'' then '_' else c)++ipCall :: Call -> Doc+ipCall (App (Label l) f as) = parens $+ text "App" <+> integer l <+> ipVal f <+> brackets (sep (punctuate (char ',') (map ipVal as)))+ipCall (Let (Label l) binds c) = parens $+ text "Let" <+> integer l <+> brackets (sep (punctuate (char ',') (map ipBind binds))) $$+ ipCall c+ where ipBind (v,l) = parens $ ipVar v <> char ',' <> ipLambda l++ipVal :: Val -> Doc+ipVal (L l) = parens $ text "L" <+> ipLambda l+ipVal (R (Label l) v) = parens $ text "R" <+> integer l <+> ipVar v+ipVal (C (Label l) c) = parens $ text "C" <+> integer l <+> integer c+ipVal (P prim) = parens $ text "P" <+> ipPrim prim++ipPrim :: Prim -> Doc+ipPrim (Plus (Label l)) = parens $ text "Plus" <+> integer l+ipPrim (If (Label lt) (Label lf)) = parens $ text "If" <+> integer lt <+> integer lf+
+ CPSScheme.hs view
@@ -0,0 +1,211 @@+{-|+ This module defines the syntax of the simple, continuation-passing-style+ functional language used here, as well as some examples.+-}+{-# LANGUAGE GeneralizedNewtypeDeriving, OverloadedStrings, FlexibleInstances #-}+module CPSScheme where++import Data.String( IsString(..) )+import qualified Data.Map as M+import Control.Monad.State+import Control.Applicative ((<$>))++import Common++-- * The CPS styntax++-- | A program is defined as a lambda abstraction. The calling convention is+-- that the program has one paramater, the final continuation.+type Prog = Lambda++-- | Labels are used throughout the code to refer to various positions in the code.+--+-- Integers are used here, but they are wrapped in a newtype to hide them from+-- the implementation.+newtype Label = Label Integer+ deriving (Show, Num, Eq, Ord, Enum)++-- | Variable names are just strings. Again, they are wrapped so they can be+-- treated abstractly. They also carry the label of their binding position.+data Var = Var Label String+ deriving (Show, Eq, Ord)++-- | The label of the 'Lambda' or 'Let' that bound this variable.+binder :: Var -> Label+binder (Var l _) = l++-- | A lambda expression has a label, a list of abstract argument names and a body.+data Lambda = Lambda Label [Var] Call+ deriving (Show, Eq, Ord)++-- | The body of a lambda expression is either +data Call = App Label Val [Val]+ -- ^ an application of a value to a list of arguments, or+ | Let Label [(Var, Lambda)] Call+ -- ^ it is the definition of a list of (potentially mutable+ -- recursive) lambda expression, defined for a nother call+ -- expression.+ deriving (Show, Eq, Ord)++-- | A value can either be+data Val = L Lambda -- ^ a lambda abstraction,+ | R Label Var -- ^ a reference to a variable (which contains the+ -- label of the binding position of the variable+ -- for convenience),+ | C Label Const -- ^ a constant value or+ | P Prim -- ^ a primitive operation.+ deriving (Show, Eq, Ord)+++-- | As constants we only have integers.+type Const = Integer++-- | Primitive operations. The primitive operations are annotated by labels. These mark the (invisible) call sites that call the continuations, and are one per continuation.+data Prim = Plus Label -- ^ Integer addition. Expected parameters: two integers, one continuation.+ | If Label Label -- ^ Conditional branching. Expected paramters: one integer, one continuation to be called if the argument is nonzero, one continuation to be called if the argument is zero ("false")+ deriving (Show, Eq, Ord)++-- * Smart constructors++instance IsString Var where+ fromString s = Var noProg s+instance IsString Val where+ fromString s = R noProg (Var noProg s)+instance IsString a => IsString (Inv a) where+ fromString s = Inv $ fromString s++instance Num (Inv Val) where+ fromInteger i = Inv $ C noProg i+ (+) = error "Do not use the Num Val instance"+ (*) = error "Do not use the Num Val instance"+ abs = error "Do not use the Num Val instance"+ signum = error "Do not use the Num Val instance"+ negate (Inv (C _ i)) = Inv $ (C noProg (-i))+ negate _ = error "Do not use the Num Val instance"+++-- | This wrapper marks values created using the smart constructors that are+-- not yet finished by passing them to 'prog' and therefore invalid.+newtype Inv a = Inv { unsafeFinish :: a }+ deriving (Show, Eq)++-- | This converts code generated by the smart constructors below to a fully+-- annotated 'CPSScheme' syntax tree, by assigning labels and resolving references+prog :: Inv Lambda -> Prog+prog (Inv p) = evalState (pLambda M.empty p) [1..] + where next = do {l <- gets head ; modify tail; return l}+ pLambda env (Lambda _ vs c) = do+ l <- next+ let env' = env `upd` map (\(Var _ n) -> n ↦ l) vs+ vs' <- mapM (pVar env') vs+ c' <- pCall env' c+ return $ Lambda l vs' c'+ pCall env (App _ v vs) = do+ l <- next+ v' <- pVal env v+ vs' <- mapM (pVal env) vs+ return $ App l v' vs'+ pCall env (Let _ binds c) = do+ l <- next+ let env' = env `upd` map (\(Var _ n,_) -> (n ↦ l)) binds+ binds' <- forM binds $ \(v,l) -> do+ v' <- pVar env' v+ l' <- pLambda env' l+ return (v', l')+ c' <- pCall env' c+ return (Let l binds' c')+ pVal env (L lambda) = L <$> pLambda env lambda+ pVal env (R _ var) = do+ l <- next+ var' <- pVar env var+ return $ R l var'+ pVal env (C _ i) = do+ l <- next+ return $ C l i+ pVal env (P (Plus _)) = do + l <- next+ return $ P (Plus l)+ pVal env (P (If _ _)) = do + l1 <- next+ l2 <- next+ return $ P (If l1 l2)+ pVar env (Var _ n) = do+ let r = env M.! n+ return $ Var r n+++lambda :: [Inv Var] -> Inv Call -> Inv Lambda+lambda vs (Inv c) = Inv $ Lambda noProg (map unsafeFinish vs) c++app :: Inv Val -> [Inv Val] -> Inv Call+app (Inv v) vs = Inv $ App noProg v (map unsafeFinish vs)++let_ :: [(Inv Var, Inv Lambda)] -> Inv Call -> Inv Call+let_ binds (Inv c) = Inv $+ Let noProg (map (\(Inv v, Inv l) -> (v,l)) binds) c++l :: Inv Lambda -> Inv Val+l = Inv . L . unsafeFinish++c :: Const -> Inv Val+c = Inv . C noProg++plus :: Inv Val+plus = Inv $ P (Plus noProg)++if_ :: Inv Val+if_ = Inv $ P (If noProg noProg)++-- | Internal error value+noProg :: a+noProg = error "Smart constructors used without calling prog"++-- * Some example Programs++-- | Returns 0+ex1 :: Prog+ex1 = prog $ lambda ["cont"] $+ app "cont" [0]++-- | Returns 1 + 1+ex2 :: Prog+ex2 = prog $ lambda ["cont"] $ + app plus [1, 1, "cont"]++-- | Returns the sum of the first 10 integers +ex3 :: Prog+ex3 = prog $ lambda ["cont"] $+ let_ [("rec", lambda ["p", "i", "c'"] $+ app if_+ [ "i"+ , l $ lambda [] $+ app plus ["p", "i",+ l $ lambda ["p'"] $+ app plus ["i", -1,+ l $ lambda ["i'"] $+ app "rec" [ "p'", "i'", "c'" ]+ ]+ ]+ , l $ lambda [] $+ app "c'" ["p"]+ ]+ )] $ app "rec" [0, 10, "cont"]++-- | Does not Terminate+ex4 :: Prog+ex4 = prog $ lambda ["cont"] $+ let_ [("rec", lambda ["c"] $ app "rec" ["c"])] $+ app "rec" ["cont"]++-- | The puzzle from Shiver's dissertation+puzzle :: Prog+puzzle = prog $ lambda ["k"] $+ app (l $ lambda ["f"] $ app "f" [0, 42, l $ lambda ["v"] $ app "f" [1,"v","k"]])+ [l $ lambda ["x","h","k1"] $+ app if_ [ "x"+ , l $ lambda [] $ app "h" ["k1"]+ , l $ lambda [] $ app "k1" [l $ lambda ["k2"] $ app "k2" ["x"]]+ ]+ ]+ +
+ Eval.hs view
@@ -0,0 +1,96 @@+{-|+Here, a standard semantic for the language defined in "CPSScheme" is+implemented, following the definitions in Olin Shivers\' \"Control-Flow+Analysis of Higher-Order Languages\".+ -}+{-# LANGUAGE TypeOperators #-}+module Eval where++import Data.Map (empty, (!))++import CPSScheme+import Common++-- * Types++-- | A closure is a lambda expression bound to a binding environment+type Closure = (Lambda, BEnv)++-- | A contour is an identifier for the contours (or dynamic frames) generated+-- at each call of a lambda expression +type Contour = Integer++-- | A binding environment maps the labels of 'Lambda' and 'Let' bindings to the+-- innermost contour generated for these expressions+type BEnv = Label :⇀ Contour++-- | 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.+type VEnv = Var :× Contour :⇀ D++-- | A semantical value can either be+data D = DI Const -- ^ A constant+ | DC Closure -- ^ A closed lambda expression+ | DP Prim -- ^ A primitive value+ | Stop -- ^ The special continuation passed to the outermost+ -- lambda of a program+ deriving (Show)++-- | The result of evaluating is a constant (or a thrown exception)+-- value.+type Ans = Const++-- * Evaluation functions++-- | evalCPS evaluates a whole program, by initializing the envirnoments and+-- passing the Stop continuation to the outermost lambda+evalCPS :: Prog -> Ans+evalCPS lam = evalF f [Stop] ve 0+ where ve = empty+ β = empty+ f = evalV (L lam) β ve++-- | evalC (called A by Shivers) evaluates a syntactical value to a semantical+-- piece of data.+evalV :: Val -> BEnv -> VEnv -> D+evalV (C _ int) β ve = DI int+evalV (P prim) β ve = DP prim+evalV (R _ var) β ve = ve ! (var, β ! binder var)+evalV (L lam) β ve = DC (lam, β)++-- | evalF evaluates a function call, distinguishing between lambda+-- expressions, primitive operations and the special Stop continuation. It+-- calles 'evalC' for the function bodies.+evalF :: D -> [D] -> VEnv -> Contour -> Ans+evalF (DC (Lambda lab vs c, β)) as ve b+ | length as /= length vs = error $ "Wrong number of arguments to lambda expression " ++ show lab+ | otherwise = evalC c β' ve' b+ where β' = β `upd` [lab ↦ b]+ ve' = ve `upd` zipWith (\v a -> (v,b) ↦ a) vs as++evalF (DP (Plus c)) [DI a1, DI a2, cont] ve b = evalF cont [DI (a1 + a2)] ve b'+ where b' = succ b+evalF (DP (If ct cf)) [DI v, contt, contf] ve b+ | v /= 0 = evalF contt [] ve b'+ | v == 0 = evalF contf [] ve b'+ where b' = succ b++evalF Stop [DI int] _ _ = int ++evalF Stop _ _ _ = error $ "Stop called with wrong number or types of arguments"+evalF (DP prim) _ _ _ = error $ "Primop " ++ show prim ++ " called with wrong arguments"+evalF (DI int) _ _ _ = error $ "Cannot treat a constant value as a function"++-- | evalC evaluates the body of a function, which can either be an application+-- (which is then evaluated using 'evalF') or a 'Let' statement.+evalC :: Call -> BEnv -> VEnv -> Contour -> Ans+evalC (App lab f vs) β ve b = evalF f' as ve b'+ where f' = evalV f β ve+ as = map (\v -> evalV v β ve) vs+ b' = succ b++evalC (Let lab ls c') β ve b = evalC c' β' ve' b'+ where b' = succ b+ β' = β `upd` [lab ↦ b']+ ve' = ve `upd` [(v,b') ↦ evalV (L l) β' ve | (v,l) <- ls]
+ ExCF.hs view
@@ -0,0 +1,108 @@+{-|+ - This module calculates the exact control graph by evaluating a "CPSScheme"+ - program, following the definitions in Olin Shivers\' \"Control-Flow+ - Analysis of Higher-Order Languages\".+ -}+{-# LANGUAGE TypeOperators #-}+module ExCF where++import Data.Map (empty, (!))++import CPSScheme+import Common++-- * Types++-- | A closure is a lambda expression bound to a binding environment+type Closure = (Lambda, BEnv)++-- | A contour is an identifier for the contours (or dynamic frames) generated+-- at each call of a lambda expression +type Contour = Integer++-- | A binding environment maps the labels of 'Lambda' and 'Let' bindings to the+-- innermost contour generated for these expressions+type BEnv = Label :⇀ Contour++-- | 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.+type VEnv = Var :× Contour :⇀ D++-- | A semantical value can either be+data D = DI Const -- ^ A constant+ | DC Closure -- ^ A closed lambda expression+ | DP Prim -- ^ A primitive value+ | Stop -- ^ The special continuation passed to the outermost+ -- lambda of a program+ deriving (Show)++-- | The origin of an edge in the control graph is a call position bundled with+-- the binding environment at that point.+type CCtxt = Label :× BEnv++-- | 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 CCache = CCtxt :⇀ D++-- | The result of evaluating a program is the control flow graph.+type Ans = CCache++-- * Evaluation functions++-- | evalCPS evaluates a whole program, by initializing the envirnoments and+-- passing the Stop continuation to the outermost lambda+evalCPS :: Prog -> Ans+evalCPS lam = evalF f [Stop] ve 0+ where ve = empty+ β = empty+ f = evalV (L lam) β ve++-- | evalC (called A by Shivers) evaluates a syntactical value to a semantical+-- piece of data.+evalV :: Val -> BEnv -> VEnv -> D+evalV (C _ int) β ve = DI int+evalV (P prim) β ve = DP prim+evalV (R _ var) β ve = ve ! (var, β ! binder var)+evalV (L lam) β ve = DC (lam, β)++-- | evalF evaluates a function call, distinguishing between lambda+-- expressions, primitive operations and the special Stop continuation. It+-- calles 'evalC' for the function bodies.+evalF :: D -> [D] -> VEnv -> Contour -> Ans+evalF (DC (Lambda lab vs c, β)) as ve b+ | length as /= length vs = error $ "Wrong number of arguments to lambda expression " ++ show lab+ | otherwise = evalC c β' ve' b+ where β' = β `upd` [lab ↦ b]+ ve' = ve `upd` zipWith (\v a -> (v,b) ↦ a) vs as++evalF (DP (Plus c)) [DI a1, DI a2, cont] ve b = evalF cont [DI (a1 + a2)] ve b'+ `upd` [ (c, β) ↦ cont ]+ where b' = succ b+ β = empty `upd` [ c ↦ b ]+evalF (DP (If ct cf)) [DI v, contt, contf] ve b+ | v /= 0 = evalF contt [] ve b' `upd` [ (ct, βt) ↦ contt ]+ | v == 0 = evalF contf [] ve b' `upd` [ (cf, βf) ↦ contf ]+ where b' = succ b+ βt = empty `upd` [ ct ↦ b ]+ βf = empty `upd` [ cf ↦ b ]++evalF Stop [DI int] _ _ = empty ++evalF Stop _ _ _ = error $ "Stop called with wrong number or types of arguments"+evalF (DP prim) _ _ _ = error $ "Primop " ++ show prim ++ " called with wrong arguments"+evalF (DI int) _ _ _ = error $ "Cannot treat a constant value as a function"++-- | evalC evaluates the body of a function, which can either be an application+-- (which is then evaluated using 'evalF') or a 'Let' statement.+evalC :: Call -> BEnv -> VEnv -> Contour -> Ans+evalC (App lab f vs) β ve b = evalF f' as ve b' `upd` [ (lab,β) ↦ f' ]+ where f' = evalV f β ve+ as = map (\v -> evalV v β ve) vs+ b' = succ b++evalC (Let lab ls c') β ve b = evalC c' β' ve' b'+ where b' = succ b+ β' = β `upd` [lab ↦ b']+ ve' = ve `upd` [(v,b') ↦ evalV (L l) β' ve | (v,l) <- ls]
+ LICENSE view
@@ -0,0 +1,30 @@+Copyright Joachim Breitner 2010++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++ * Redistributions of source code must retain the above copyright+ notice, this list of conditions and the following disclaimer.++ * Redistributions in binary form must reproduce the above+ copyright notice, this list of conditions and the following+ disclaimer in the documentation and/or other materials provided+ with the distribution.++ * Neither the name of Joachim Breitner nor the names of other+ contributors may be used to endorse or promote products derived+ from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ Setup.hs view
@@ -0,0 +1,3 @@+#!/usr/bin/env runhaskell+import Distribution.Simple+main = defaultMain
+ shivers-cfg.cabal view
@@ -0,0 +1,28 @@+Name: shivers-cfg+Version: 0.1+Synopsis: Implementation of Shivers' Control-Flow Analysis+Description:+ In his 1991 dissertation, Olin Shivers introduces a concept+ of control flow graphs for functional languages, provides an algorithm+ to statically derive a safe approximation of the control flow graph and+ proves this algorithm correct. In our student research project,+ Shivers' algorithms and proofs are formalized using the theorem prover+ system Isabelle.+ . + This package contains the Haskell prototype of the Isabelle+ formalization, together with some pretty printing and rendering+ facilities. It is provided as a reference, not as a ready-to-use library.++License: BSD3+License-file: LICENSE+Author: Joachim Breitner+Maintainer: mail@joachim-breitner.de+Stability: Experimental+Category: Language+Build-type: Simple+Cabal-version: >=1.2++Library+ Build-depends: containers, base >=4 && <5, mtl, process, directory,+ pretty, HPDF, language-dot+ Exposed-modules: Eval, CPSScheme, ExCF, AbsCF, CPSPrint, CFGraph