Skip to content
This repository

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Browse code

Some experimental stuff to do with escaping values in k-CFA

  • Loading branch information...
commit 2d99c07da7b553bda6e71f6ed847b5a971bcb037 1 parent ab7a21d
Max Bolingbroke authored October 12, 2011

Showing 1 changed file with 58 additions and 16 deletions. Show diff stats Hide diff stats

  1. 74  0CFA.hs
74  0CFA.hs
@@ -7,6 +7,7 @@ import Control.Monad
7 7
 
8 8
 import qualified Data.Map as M
9 9
 import qualified Data.Set as S
  10
+import Data.List ((\\))
10 11
 
11 12
 import Debug.Trace
12 13
 
@@ -30,7 +31,7 @@ type Denotable = S.Set Value
30 31
 type Value = Clo
31 32
 -- Closures pair a lambda-term with a binding environment that determines
32 33
 -- the values of its free variables
33  
-data Clo = Closure (Label, [Var], Call) BEnv | HaltClosure deriving (Eq, Ord, Show)
  34
+data Clo = Closure (Label, [Var], Call) BEnv | HaltClosure | Arbitrary deriving (Eq, Ord, Show)
34 35
 -- Addresses can point to values in the store. In pure CPS, the only kind of addresses are bindings
35 36
 type Addr = Bind
36 37
 -- A binding is minted each time a variable gets bound to a value
@@ -59,27 +60,48 @@ tick l t = take k (l:t)
59 60
 atomEval :: BEnv -> Store -> Exp -> Denotable
60 61
 atomEval benv store Halt    = S.singleton HaltClosure
61 62
 atomEval benv store (Ref x) = case M.lookup x benv of
62  
-    Nothing   -> error "Var unbound in BEnv"
  63
+    Nothing   -> error $ "Variable unbound in BEnv: " ++ show x
63 64
     Just t -> case M.lookup (Binding x t) store of
64  
-        Nothing -> error "Address unbound in Store"
  65
+        Nothing -> error $ "Address unbound in Store: " ++ show (Binding x t)
65 66
         Just d  -> d
66 67
 atomEval benv _     (Lam l v c) = S.singleton (Closure (l, v, c) benv)
67 68
 
68  
-next :: State -> S.Set State
  69
+next :: State -> S.Set State -- Next states
69 70
 next s@(State (Call l fun args) benv store time)
70  
-  = -- trace ("next" ++ show s) $
71  
-    S.fromList [ State call' benv'' store' time'
  71
+  = trace ("next" ++ show s) $
  72
+    S.fromList [ state'
72 73
                | clo <- S.toList procs
73  
-               , (formals, call', benv') <- case clo of
74  
-                    Closure (_, formals, call') benv' -> [(formals, call', benv')]
75  
-                    HaltClosure                       -> []
76  
-               , let benv'' = foldr (\formal benv' -> M.insert formal time benv') benv' formals
77  
-               , params <- S.toList (transpose paramss)
78  
-               , let store' = foldr (\(formal, params) store  -> storeInsert (Binding formal time) params store) store (formals `zip` params)]
  74
+               , state' <- case clo of
  75
+                    HaltClosure -> []
  76
+                    Closure (_, formals, call') benv'
  77
+                      | let benv'' = foldr (\formal benv' -> M.insert formal time benv') benv' formals
  78
+                      -> [ State call' benv'' store' time'
  79
+                         | params <- S.toList (transpose paramss)
  80
+                         , let store' = foldr (\(formal, params) store  -> storeInsert (Binding formal time) params store) store (formals `zip` params)
  81
+                         ]
  82
+                    Arbitrary
  83
+                      -> [ state'
  84
+                         | params <- S.toList (transpose paramss)
  85
+                         , param <- params
  86
+                         , Just state' <- [escape param store]
  87
+                         ]
  88
+               ]
79 89
   where time' = tick l time
80 90
         procs  = atomEval benv store fun
81 91
         paramss = map (atomEval benv store) args
82 92
 
  93
+-- Extension of my own design to allow CFA in the presence of arbitrary values.
  94
+-- Similar to "sub-0CFA" where locations are inferred to either have either a single
  95
+-- lambda flow to them, no lambdas, or all lambdas
  96
+escape :: Value -> Store -> Maybe State
  97
+escape Arbitrary                          _     = Nothing -- If an arbitrary value from outside escapes we don't care
  98
+escape HaltClosure                        _     = Nothing
  99
+escape (Closure (_l, formals, call) benv) store = Just (State call (benv `M.union` benv') (store `storeJoin` store') [])
  100
+  where (benv', store') = fvStuff formals
  101
+
  102
+fvStuff :: [Var] -> (BEnv, Store)
  103
+fvStuff xs = (M.fromList [(x, []) | x <- xs], M.fromList [(Binding x [], S.singleton Arbitrary) | x <- xs])
  104
+
83 105
 transpose :: Ord a => [S.Set a] -> S.Set [a]
84 106
 transpose []         = S.singleton []
85 107
 transpose (arg:args) = S.fromList [arg:args | args <- S.toList (transpose args), arg <- S.toList arg]
@@ -110,9 +132,19 @@ monovariantStore store = M.foldrWithKey (\(Binding x _) d res -> M.alter (\mb_ex
110 132
 monovariantValue :: Value -> Exp
111 133
 monovariantValue (Closure (l, v, c) _) = Lam l v c
112 134
 monovariantValue HaltClosure           = Halt
  135
+monovariantValue Arbitrary             = Ref "unknown"
113 136
 
114 137
 analyse :: Call -> M.Map Var (S.Set Exp)
115  
-analyse e = monovariantStore (summarize (explore S.empty [State e M.empty M.empty []]))
  138
+analyse e = monovariantStore (summarize (explore S.empty [State e benv store []]))
  139
+  where (benv, store) = fvStuff (S.toList (fvsCall e))
  140
+
  141
+fvsCall :: Call -> S.Set Var
  142
+fvsCall (Call _ fun args) = fvsExp fun `S.union` S.unions (map fvsExp args)
  143
+
  144
+fvsExp :: Exp -> S.Set Var
  145
+fvsExp Halt         = S.empty
  146
+fvsExp (Ref x)      = S.singleton x
  147
+fvsExp (Lam _ xs c) = fvsCall c S.\\ S.fromList xs
116 148
 
117 149
 -- Helper functions for constructing syntax trees
118 150
 
@@ -155,7 +187,17 @@ standardExample =
155 187
                    lam ["a"] (call (ref "id") [lam ["y"] (halt (ref "y")),
156 188
                                                lam ["b"] (halt (ref "b"))])]
157 189
 
  190
+-- Example with free varibles (showing escapes):
  191
+fvExample :: UniqM Call
  192
+fvExample = 
  193
+  let_ "id" (lam ["x", "k"] (call (ref "k") [ref "x"])) $
  194
+  call (ref "id") [lam ["z"] (call (ref "escape") [ref "z"]),
  195
+                   lam ["a"] (call (ref "id") [lam ["y"] (call (ref "escape") [ref "y"]),
  196
+                                               lam ["b"] (call (ref "escape") [ref "b"])])]
  197
+
158 198
 
159  
-main = forM_ (M.toList (analyse (runUniqM standardExample))) $ \(x, es) -> do
160  
-    putStrLn (x ++ ":")
161  
-    mapM_ (putStrLn . ("  " ++) . show) (S.toList es)
  199
+main = forM_ [fvExample, standardExample] $ \example -> do
  200
+         putStrLn "====="
  201
+         forM_ (M.toList (analyse (runUniqM example))) $ \(x, es) -> do
  202
+           putStrLn (x ++ ":")
  203
+           mapM_ (putStrLn . ("  " ++) . show) (S.toList es)

0 notes on commit 2d99c07

Please sign in to comment.
Something went wrong with that request. Please try again.