diff --git a/AbsCF.hs b/AbsCF.hs new file mode 100644 --- /dev/null +++ b/AbsCF.hs @@ -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')] + diff --git a/CFGraph.hs b/CFGraph.hs new file mode 100644 --- /dev/null +++ b/CFGraph.hs @@ -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 + diff --git a/CPSPrint.hs b/CPSPrint.hs new file mode 100644 --- /dev/null +++ b/CPSPrint.hs @@ -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 + diff --git a/CPSScheme.hs b/CPSScheme.hs new file mode 100644 --- /dev/null +++ b/CPSScheme.hs @@ -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"]] + ] + ] + + diff --git a/Eval.hs b/Eval.hs new file mode 100644 --- /dev/null +++ b/Eval.hs @@ -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] diff --git a/ExCF.hs b/ExCF.hs new file mode 100644 --- /dev/null +++ b/ExCF.hs @@ -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] diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -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. diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,3 @@ +#!/usr/bin/env runhaskell +import Distribution.Simple +main = defaultMain diff --git a/shivers-cfg.cabal b/shivers-cfg.cabal new file mode 100644 --- /dev/null +++ b/shivers-cfg.cabal @@ -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