SSTG (empty) → 0.1.0.1
raw patch · 21 files changed
+2067/−0 lines, 21 filesdep +SSTGdep +basedep +containerssetup-changed
Dependencies added: SSTG, base, containers, ghc, ghc-paths
Files
- LICENSE +30/−0
- README.md +1/−0
- SSTG.cabal +61/−0
- Setup.hs +2/−0
- app/Main.hs +37/−0
- src/SSTG.hs +9/−0
- src/SSTG/Core.hs +11/−0
- src/SSTG/Core/Execution.hs +15/−0
- src/SSTG/Core/Execution/Engine.hs +193/−0
- src/SSTG/Core/Execution/Models.hs +206/−0
- src/SSTG/Core/Execution/Namer.hs +215/−0
- src/SSTG/Core/Execution/Rules.hs +446/−0
- src/SSTG/Core/Execution/Stepper.hs +42/−0
- src/SSTG/Core/Syntax.hs +9/−0
- src/SSTG/Core/Syntax/Language.hs +143/−0
- src/SSTG/Core/Syntax/Typer.hs +45/−0
- src/SSTG/Core/Translation.hs +7/−0
- src/SSTG/Core/Translation/Haskell.hs +247/−0
- src/SSTG/Utils.hs +7/−0
- src/SSTG/Utils/PrettyPrint.hs +339/−0
- test/Spec.hs +2/−0
+ LICENSE view
@@ -0,0 +1,30 @@+Copyright Author name here (c) 2017++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 Author name here 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.
+ README.md view
@@ -0,0 +1,1 @@+# SSTG
+ SSTG.cabal view
@@ -0,0 +1,61 @@+name: SSTG+version: 0.1.0.1+synopsis: STG Symbolic Execution+description: Prototype of STG-based Symbolic Execution for Haskell.+homepage: https://github.com/AntonXue/SSTG#readme+license: BSD3+license-file: LICENSE+author: Anton Xue+maintainer: anton.xue@yale.edu+copyright: 2017 Anton Xue+category: Web+build-type: Simple+extra-source-files: README.md+cabal-version: >=1.10++library+ hs-source-dirs: src+ exposed-modules: SSTG+ , SSTG.Core+ , SSTG.Core.Translation+ , SSTG.Core.Translation.Haskell+ , SSTG.Core.Syntax+ , SSTG.Core.Syntax.Language+ , SSTG.Core.Syntax.Typer+ , SSTG.Core.Execution+ , SSTG.Core.Execution.Engine+ , SSTG.Core.Execution.Models+ , SSTG.Core.Execution.Namer+ , SSTG.Core.Execution.Rules+ , SSTG.Core.Execution.Stepper+ , SSTG.Utils+ , SSTG.Utils.PrettyPrint+ build-depends: base >= 4.7 && < 5+ , ghc+ , ghc-paths+ , containers >= 0.5 && < 0.6+ default-language: Haskell2010++executable SSTG-exe+ hs-source-dirs: app+ main-is: Main.hs+ ghc-options: -threaded -rtsopts -with-rtsopts=-N+ build-depends: base+ , SSTG+ , containers >= 0.5 && < 0.6+ default-language: Haskell2010++test-suite SSTG-test+ type: exitcode-stdio-1.0+ hs-source-dirs: test+ main-is: Spec.hs+ build-depends: base+ , SSTG+ , containers >= 0.5 && < 0.6+ ghc-options: -threaded -rtsopts -with-rtsopts=-N+ default-language: Haskell2010++source-repository head+ type: git+ location: https://github.com/AntonXue/SSTG+
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ app/Main.hs view
@@ -0,0 +1,37 @@+module Main where++import SSTG++import qualified Data.Map as M++import System.Environment++main :: IO ()+main = do+ -- Get command line arguments.+ (proj:src:tail_args) <- getArgs+ -- Make bindings.+ binds <- mkTargetBindings proj src+ -- Configure entry.+ let entry = if length tail_args > 0 then tail_args !! 0 else "main"++ -- Do the loading.+ let load_result = loadStateEntry entry (Program binds)+ putStrLn $ "binds: " ++ show (length binds)+ case load_result of+ LoadError str -> do+ error str+ LoadOkay state -> do+ -- putStrLn "Bindings"+ -- mapM_ (putStrLn . pprBindingStr) binds+ putStrLn" **************** INIT ***************"+ putStrLn "Initial state:"+ putStrLn $ pprStateStr state+ let lds = execute1 100 state+ putStrLn "*************** BEGIN ***************"+ putStrLn $ pprLivesDeadsStr lds+ LoadGuess state cands -> do+ putStrLn $ pprStateStr state+ putStrLn "Other possible candidates:"+ putStrLn $ show cands+
+ src/SSTG.hs view
@@ -0,0 +1,9 @@+-- | Export Module for SSTG+module SSTG+ ( module SSTG.Core+ , module SSTG.Utils+ ) where++import SSTG.Core+import SSTG.Utils+
+ src/SSTG/Core.hs view
@@ -0,0 +1,11 @@+-- | Import Module for SSTG.Core+module SSTG.Core+ ( module SSTG.Core.Execution+ , module SSTG.Core.Syntax+ , module SSTG.Core.Translation+ ) where++import SSTG.Core.Execution+import SSTG.Core.Syntax+import SSTG.Core.Translation+
+ src/SSTG/Core/Execution.hs view
@@ -0,0 +1,15 @@+-- | Export Module for SSTG.Core.Execution+module SSTG.Core.Execution+ ( module SSTG.Core.Execution.Engine+ , module SSTG.Core.Execution.Models+ , module SSTG.Core.Execution.Namer+ , module SSTG.Core.Execution.Rules+ , module SSTG.Core.Execution.Stepper+ ) where++import SSTG.Core.Execution.Engine+import SSTG.Core.Execution.Models+import SSTG.Core.Execution.Namer+import SSTG.Core.Execution.Rules+import SSTG.Core.Execution.Stepper+
+ src/SSTG/Core/Execution/Engine.hs view
@@ -0,0 +1,193 @@+-- | Symbolic STG Execution Engine+module SSTG.Core.Execution.Engine+ ( loadState+ , loadStateEntry+ , LoadResult (..)+ , execute1+ ) where++import SSTG.Core.Syntax+import SSTG.Core.Execution.Models+import SSTG.Core.Execution.Namer+import SSTG.Core.Execution.Stepper++import qualified Data.List as L+import qualified Data.Map as M++-- | Load Result+data LoadResult = LoadOkay State+ | LoadGuess State [Binding]+ | LoadError String+ deriving (Show, Eq, Read)++-- | Load State+-- Guess the main function.+loadState :: Program -> LoadResult+loadState prog = loadStateEntry main_occ_name prog+ where main_occ_name = "main" -- Based on a few experimental programs.++-- | Specified Entry Point Load+loadStateEntry :: String -> Program -> LoadResult+loadStateEntry entry (Program bnds) = if length matches == 0+ then LoadError ("No entry candidates found for: [" ++ entry ++ "]")+ else if length others == 0+ then LoadOkay state+ else LoadGuess state (map fst others)+ where -- Status or something.+ status = Status { steps = 0 }+ -- Stack initialized to empty.+ stack = Stack []+ -- Globals and Heap are loaded together. They are still beta forms now.+ heap0 = Heap M.empty (MemAddr 0)+ (glist, heap1, bnd_addrss) = initGlobals bnds heap0+ globals0 = Globals (M.fromList glist)+ (heap2, localss) = liftBindings bnd_addrss globals0 heap1+ bnd_locs = zip bnds localss+ -- Code loading. Completes heap and globals with symbolic injection.+ matches = entryMatches entry bnd_locs+ ((tgt_bnd, tgt_loc):others) = matches+ ((tgt_var, tgt_rhs):_) = lhsMatches entry tgt_bnd+ (code, globals, heap) = loadCode tgt_var tgt_rhs tgt_loc globals0 heap2+ -- Ready to fill the state.+ state0 = State { state_status = status+ , state_stack = stack+ , state_heap = heap+ , state_globals = globals+ , state_code = code+ , state_names = []+ , state_paths = []+ , state_links = SymLinks M.empty }++ -- Gather information on all variables.+ names = allNames state0+ state = state0 { state_names = allNames state0 }++-- | Allocate Binding+allocBinding :: Binding -> Heap -> (Heap, [MemAddr])+allocBinding (Binding _ pairs) heap = (heap', addrs)+ where hfakes = map (const Blackhole) pairs+ (heap', addrs) = allocHeapList hfakes heap++-- | Allocate List of Bindings+allocBindingList :: [Binding] -> Heap -> (Heap, [[MemAddr]])+allocBindingList [] heap = (heap, [])+allocBindingList (b:bs) heap = (res_heap, addrs : as)+ where (heap', addrs) = allocBinding b heap+ (res_heap, as) = allocBindingList bs heap'++-- | Binding Address to Name Values+bndAddrsToNameVals :: (Binding, [MemAddr]) -> [(Name, Value)]+bndAddrsToNameVals (Binding _ rhss, addrs) = zip names pointers+ where names = map (varName . fst) rhss+ pointers = map (\a -> MemVal a) addrs++-- | Initialize Globals+initGlobals :: [Binding] -> Heap ->+ ([(Name, Value)], Heap, [(Binding, [MemAddr])])+initGlobals bnds heap = (name_vals, heap', bnd_addrss)+ where (heap', addrss) = allocBindingList bnds heap+ bnd_addrss = zip bnds addrss+ name_vals = concatMap bndAddrsToNameVals bnd_addrss++-- | Force Get Address+forceLookupAddr :: Var -> Globals -> MemAddr+forceLookupAddr var globals = case lookupGlobals var globals of+ Just (MemVal addr) -> addr+ otherwise -> MemAddr (-1)++-- | Force Atom Lookup+forceLookupValue :: Atom -> Locals -> Globals -> Value+forceLookupValue (LitAtom lit) _ _ = LitVal lit+forceLookupValue (VarAtom var) locals globals =+ case lookupValue var locals globals of+ Nothing -> LitVal BlankAddr -- An error, but I want to not crash.+ Just val -> val++-- | Full Rhs Object+forceRhsObj :: BindRhs -> Locals -> Globals -> HeapObj+forceRhsObj (FunForm prms expr) locals _ = FunObj prms expr locals+forceRhsObj (ConForm dcon args) locals globals = ConObj dcon arg_vals+ where arg_vals = map (\a -> forceLookupValue a locals globals) args++-- | Lift Binding+liftBinding :: (Binding, [MemAddr]) -> Globals -> Heap -> (Heap, Locals)+liftBinding (Binding rec pairs, addrs) globals heap = (heap', locals)+ where (vars, rhss) = unzip pairs+ mem_vals = map (\a -> MemVal a) addrs+ e_locs = Locals M.empty+ r_locs = insertLocalsList (zip vars mem_vals) e_locs+ locals = case rec of { Rec -> r_locs; NonRec -> e_locs }+ hobjs = map (\r -> forceRhsObj r locals globals) rhss+ heap' = insertHeapList (zip addrs hobjs) heap++-- | Lift Binding List+liftBindings :: [(Binding, [MemAddr])] -> Globals -> Heap -> (Heap, [Locals])+liftBindings [] _ heap = (heap, [])+liftBindings (bm:bms) globals heap = (res_heap, locals : ls)+ where (heap', locals) = liftBinding bm globals heap+ (res_heap, ls) = liftBindings bms globals heap'++-- | Entry Candidates+-- Return a sub-list of bindings in which the entry candidate appears.+entryMatches :: String -> [(Binding, Locals)] -> [(Binding, Locals)]+entryMatches entry bnd_locs = filter (bindFilter entry) bnd_locs++-- | Bind Filtering+bindFilter :: String -> (Binding, Locals) -> Bool+bindFilter entry (bnd, loc) = lhsMatches entry bnd /= []++-- | Sub-Bindings String Match+lhsMatches :: String -> Binding -> [(Var, BindRhs)]+lhsMatches st (Binding _ pairs) =+ filter (\(var, _) -> st == (nameOccStr . varName) var) pairs++-- | Load Code+loadCode :: Var -> BindRhs -> Locals -> Globals -> Heap ->+ (Code, Globals, Heap)+loadCode ent (ConForm _ _) locals globals heap = (code, globals, heap)+ where code = Evaluate (Atom (VarAtom ent)) locals+loadCode ent (FunForm params expr) locals globals heap = (code, globals, heap')+ where actuals = traceArgs params expr locals globals heap+ confs = map varName actuals+ names' = freshSeededNameList confs confs+ adjusted = map (\(n, t) -> Var n t) (zip names' (map varType actuals))+ -- Throw the parameters on heap as symbolic objects+ sym_objs = map (\p -> SymObj (Symbol p)) adjusted+ (heap', addrs) = allocHeapList sym_objs heap+ -- make Atom representations for arguments and shove into locals.+ mem_vals = map (\a -> MemVal a) addrs+ locals' = insertLocalsList (zip adjusted mem_vals) locals+ args = map (\p -> VarAtom p) adjusted+ -- Set up code+ code = Evaluate (FunApp ent args) locals'++-- | Trace Arguments+-- We need to do stupid tracing if it's THUNK'D by default >:(+traceArgs :: [Var] -> Expr -> Locals -> Globals -> Heap -> [Var]+traceArgs base expr locals globals heap+ | FunApp var [] <- expr+ , Just (_, hobj) <- vlookupHeap var locals globals heap+ , FunObj params _ _ <- hobj+ , length params > 0+ , length base == 0 = params++ | otherwise = base++execute1 :: Int -> State -> ([LiveState], [DeadState])+execute1 n state | n < 1 = ([([], state)], [])+ | otherwise = runBoundedBFS n state+++{-+liveStep :: LiveState -> ([LiveState], [DeadState])+liveStep (rules, state) = let (lives, deadfun) = pass+++-- | Historical execution+execute2 :: Int -> [([LiveState], [DeadState])] -> [([LiveState], [DeadState])]+execute2 n lvs_dds+ | n < 1 = lvs_dds+ | otherwise = let lives = concatMap fst lvs_dds+ deads = concatMap snd lvs_dds+ in undefined+-}
+ src/SSTG/Core/Execution/Models.hs view
@@ -0,0 +1,206 @@+-- | Symbolic STG Execution Models+module SSTG.Core.Execution.Models+ ( module SSTG.Core.Execution.Models+ ) where++import SSTG.Core.Syntax++import qualified Data.Map as M++-- | Symbolic Transformation+-- We supply some state(s), it gives back those state(s) and some result.+newtype SymbolicT s a = SymbolicT { run :: s -> (s, a) }++-- | Functor instance of Symbolic Transformation+-- Apply transformations on the result.+instance Functor (SymbolicT s) where+ fmap f st = SymbolicT (\s0 -> let (s1, a1) = (run st) s0 in (s1, f a1))++-- | Applicative instance of Symbolic Transformation+-- Can be used to chain together step-wise execution.+instance Applicative (SymbolicT s) where+ pure a = SymbolicT (\s -> (s, a))+ sf <*> st = SymbolicT (\s0 -> let (s1, a1) = (run st) s0+ (s2, f2) = (run sf) s1 in (s2, f2 a1))++-- | Monad instance of Symbolic Transformation+-- Used for transitioning between different types of state manipulations.+instance Monad (SymbolicT s) where+ return a = pure a+ st >>= fs = SymbolicT (\s0 -> let (s1, a1) = (run st) s0+ (s2, a2) = (run (fs a1)) s2 in (s2, a2))++-- | State+data State = State { state_status :: Status+ , state_stack :: Stack+ , state_heap :: Heap+ , state_globals :: Globals+ , state_code :: Code+ , state_names :: [Name]+ , state_paths :: PathCons+ , state_links :: SymLinks+ } deriving (Show, Eq, Read)++-- | Symbolic+newtype Symbol = Symbol Var deriving (Show, Eq, Read)++-- | Status+data Status = Status { steps :: Int+ } deriving (Show, Eq, Read)++-- | Stack+newtype Stack = Stack [Frame] deriving (Show, Eq, Read)++-- | Stack Frame+data Frame = AltFrame Var [Alt] Locals+ | ApplyFrame [Atom] Locals+ | UpdateFrame MemAddr+ deriving (Show, Eq, Read)++-- | Memory Address+newtype MemAddr = MemAddr Int deriving (Show, Eq, Read, Ord)++-- | Value+data Value = LitVal Lit+ | MemVal MemAddr+ deriving (Show, Eq, Read)++-- | Locals+newtype Locals = Locals (M.Map Name Value) deriving (Show, Eq, Read)++-- | Heap+data Heap = Heap (M.Map MemAddr HeapObj) MemAddr deriving (Show, Eq, Read)++-- | Heap Object+data HeapObj = LitObj Lit+ | SymObj Symbol+ | ConObj DataCon [Value]+ | FunObj [Var] Expr Locals+ | Blackhole+ deriving (Show, Eq, Read)++-- | Globals+newtype Globals = Globals (M.Map Name Value) deriving (Show, Eq, Read)++-- | Evaluation State+data Code = Evaluate Expr Locals+ | Return Value+ deriving (Show, Eq, Read)++-- | Path Constraints+type PathCons = [PathCond]++-- | Path Condition+data PathCond = PathCond Alt Expr Locals Bool deriving (Show, Eq, Read)++-- | Symbolic Link Table+newtype SymLinks = SymLinks (M.Map Name Name) deriving (Show, Eq, Read)++-- Simple functions that require only the immediate data structure.++-- | Name Occ String+nameOccStr :: Name -> String+nameOccStr (Name occ _ _ _) = occ++-- | Name Unique+nameUnique :: Name -> Int+nameUnique (Name _ _ _ unq) = unq++-- | Var Name+varName :: Var -> Name+varName (Var name _) = name++-- | Mem Addr Int+memAddrInt :: MemAddr -> Int+memAddrInt (MemAddr int) = int++-- | Lookup Locals+lookupLocals :: Var -> Locals -> Maybe Value+lookupLocals var (Locals lmap) = M.lookup (varName var) lmap++-- | Insert Locals+insertLocals :: Var -> Value -> Locals -> Locals+insertLocals var val (Locals lmap) = Locals lmap'+ where lmap' = M.insert (varName var) val lmap++-- | Insert Locals List+insertLocalsList :: [(Var, Value)] -> Locals -> Locals+insertLocalsList [] locals = locals+insertLocalsList ((var, val):vvs) locals = insertLocalsList vvs locals'+ where locals' = insertLocals var val locals++-- | Lookup Heap+lookupHeap :: MemAddr -> Heap -> Maybe HeapObj+lookupHeap addr (Heap hmap _) = M.lookup addr hmap++-- | Allocate Heap+allocHeap :: HeapObj -> Heap -> (Heap, MemAddr)+allocHeap hobj (Heap hmap prev) = (Heap hmap' addr, addr)+ where addr = MemAddr ((memAddrInt prev) + 1)+ hmap' = M.insert addr hobj hmap++-- | Allocate Heap List+allocHeapList :: [HeapObj] -> Heap -> (Heap, [MemAddr])+allocHeapList [] heap = (heap, [])+allocHeapList (hobj:hobjs) heap = (res_heap, addr : as)+ where (heap', addr) = allocHeap hobj heap+ (res_heap, as) = allocHeapList hobjs heap'++-- | Insert Heap+insertHeap :: MemAddr -> HeapObj -> Heap -> Heap+insertHeap addr hobj (Heap hmap prev) = Heap hmap' prev+ where hmap' = M.insert addr hobj hmap++-- | Insert Heap List+insertHeapList :: [(MemAddr, HeapObj)] -> Heap -> Heap+insertHeapList [] heap = heap+insertHeapList ((addr, hobj):ahs) heap = insertHeapList ahs heap'+ where heap' = insertHeap addr hobj heap++-- | Lookup Globals+lookupGlobals :: Var -> Globals -> Maybe Value+lookupGlobals var (Globals gmap) = M.lookup (varName var) gmap++-- | Insert Globals+insertGlobals :: Var -> Value -> Globals -> Globals+insertGlobals var val (Globals gmap) = Globals gmap'+ where gmap' = M.insert (varName var) val gmap++-- | Insert Globals List+insertGlobalsList :: [(Var, Value)] -> Globals -> Globals+insertGlobalsList [] globals = globals+insertGlobalsList ((var, val):vvs) globals = insertGlobalsList vvs globals'+ where globals' = insertGlobals var val globals++-- Complex functions that involve multiple data structures.++-- | Lookup Value+lookupValue :: Var -> Locals -> Globals -> Maybe Value+lookupValue var locals globals = case lookupLocals var locals of+ Nothing -> lookupGlobals var globals+ mb_value -> mb_value++-- | Look Up Value by Atom+alookupValue :: Atom -> Locals -> Globals -> Maybe Value+alookupValue (LitAtom lit) _ _ = Just (LitVal lit)+alookupValue (VarAtom var) locals globals = lookupValue var locals globals++-- | Lookup Heap by Variable+vlookupHeap :: Var -> Locals -> Globals -> Heap -> Maybe (MemAddr, HeapObj)+vlookupHeap var locals globals heap = do+ val <- lookupValue var locals globals+ case val of+ LitVal lit -> Nothing+ MemVal addr -> lookupHeap addr heap >>= \hobj -> return (addr, hobj)++-- | MemAddr Type+memAddrType :: MemAddr -> Heap -> Maybe Type+memAddrType addr heap = do+ hobj <- lookupHeap addr heap+ return $ case hobj of+ Blackhole -> Bottom+ LitObj lit -> litType lit+ SymObj (Symbol svar) -> varType svar+ ConObj dcon _ -> dataConType dcon+ FunObj params expr _ -> FunTy (map varType params ++ [exprType expr])+
+ src/SSTG/Core/Execution/Namer.hs view
@@ -0,0 +1,215 @@+-- | Naming Module+module SSTG.Core.Execution.Namer+ ( allNames+ , freshString+ , freshName+ , freshSeededName+ , freshNameList+ , freshSeededNameList+ ) where++import SSTG.Core.Syntax+import SSTG.Core.Execution.Models++import qualified Data.Char as C+import qualified Data.IntMap as IM+import qualified Data.List as L+import qualified Data.Map as M+import qualified Data.Set as S++-- | All Names in State+allNames :: State -> [Name]+allNames state = L.nub acc_ns+ where stack_ns = stackNames (state_stack state)+ heap_ns = heapNames (state_heap state)+ glbls_ns = globalsNames (state_globals state)+ expr_ns = codeNames (state_code state)+ pcons_ns = pconsNames (state_paths state)+ links_ns = linksNames (state_links state)+ acc_ns = stack_ns ++ heap_ns ++ glbls_ns +++ expr_ns ++ pcons_ns ++ links_ns++-- | Stack Names+stackNames :: Stack -> [Name]+stackNames (Stack []) = []+stackNames (Stack (f:fs)) = frameNames f ++ stackNames (Stack fs)++-- | Frame Names+frameNames :: Frame -> [Name]+frameNames (UpdateFrame _) = []+frameNames (ApplyFrame as lcs) = concatMap atomNames as ++ localsNames lcs+frameNames (AltFrame var alts lcs) = varNames var ++ (concatMap altNames alts)+ ++ localsNames lcs++-- | Alt Names+altNames :: Alt -> [Name]+altNames (Alt _ vars expr) = (concatMap varNames vars) ++ exprNames expr++-- | Locals Names+localsNames :: Locals -> [Name]+localsNames (Locals lmap) = M.keys lmap++-- | Heap Names+heapNames :: Heap -> [Name]+heapNames (Heap heap _) = concatMap (heapObjNames . snd) kvs+ where kvs = M.toList heap++-- | Heap Object Names+heapObjNames :: HeapObj -> [Name]+heapObjNames Blackhole = []+heapObjNames (LitObj _) = []+heapObjNames (SymObj sym) = symbolNames sym+heapObjNames (ConObj dcon _) = dataNames dcon+heapObjNames (FunObj prms expr locals) =+ concatMap varNames prms ++ exprNames expr ++ localsNames locals++-- | Symbol Names+symbolNames :: Symbol -> [Name]+symbolNames (Symbol sym) = varNames sym++-- | Lambda Form Names+bindRhsNames :: BindRhs -> [Name]+bindRhsNames (FunForm prms expr) = (concatMap varNames prms) ++ exprNames expr+bindRhsNames (ConForm dcon args) = dataNames dcon ++ concatMap atomNames args++-- | Var Names+varNames :: Var -> [Name]+varNames (Var n t) = n : typeNames t++-- | Atom Names+atomNames :: Atom -> [Name]+atomNames (VarAtom var) = varNames var+atomNames (LitAtom _) = []++-- | Globals Names+globalsNames :: Globals -> [Name]+globalsNames (Globals gmap) = M.keys gmap++-- | Eval State Names+codeNames :: Code -> [Name]+codeNames (Return _) = []+codeNames (Evaluate expr locals) = exprNames expr ++ localsNames locals++-- | Expression Names+exprNames :: Expr -> [Name]+exprNames (Atom atom) = atomNames atom+exprNames (FunApp fun args) = varNames fun ++ concatMap atomNames args+exprNames (PrimApp prim args) = pfunNames prim ++ concatMap atomNames args+exprNames (ConApp dcon args) = dataNames dcon ++ concatMap atomNames args+exprNames (Let binds expr) = bindingNames binds ++ exprNames expr+exprNames (Case expr var alts) = varNames var ++ exprNames expr +++ concatMap altNames alts+-- | Type Names+typeNames :: Type -> [Name]+typeNames (TyVarTy n ty) = n : typeNames ty+typeNames (AppTy t1 t2) = typeNames t1 ++ typeNames t2+typeNames (ForAllTy bnd ty) = tyBinderNames bnd ++ typeNames ty+typeNames (CastTy ty coer) = typeNames ty ++ coercionNames coer+typeNames (TyConApp tc ty) = tyConNames tc ++ concatMap typeNames ty+typeNames (CoercionTy coer) = coercionNames coer+typeNames (LitTy _) = []+typeNames (FunTy tys) = concatMap typeNames tys+typeNames (TyClosure ty ts) = concatMap typeNames (ty : ts)+typeNames (Bottom) = []++-- | Prim Fun Names+pfunNames :: PrimFun -> [Name]+pfunNames (PrimFun n ty) = n : typeNames ty++-- | Data Constructor ID Names+conTagName :: ConTag -> Name+conTagName (ConTag n _) = n++-- | Data Constructor Names+dataNames :: DataCon -> [Name]+dataNames (DataCon id ty tys) = conTagName id : concatMap typeNames (ty : tys)++-- | Type Binder Names+tyBinderNames :: TyBinder -> [Name]+tyBinderNames (NamedTyBndr n ty) = n : typeNames ty+tyBinderNames (AnonTyBndr ty) = typeNames ty++-- | Type Constructor Names+tyConNames :: TyCon -> [Name]+tyConNames (FunTyCon n) = [n]+tyConNames (AlgTyCon n r) = n : algTyRhsNames r+tyConNames (SynonymTyCon n) = [n]+tyConNames (FamilyTyCon n) = [n]+tyConNames (PrimTyCon n) = [n]+tyConNames (TcTyCon n) = [n]+tyConNames (PromotedDataCon n dcon) = n : dataNames dcon++-- | Coercion Names+coercionNames :: Coercion -> [Name]+coercionNames (Coercion t1 t2) = typeNames t1 ++ typeNames t2++-- | Type Alg Rhs Names+algTyRhsNames :: AlgTyRhs -> [Name]+algTyRhsNames (AbstractTyCon _) = []+algTyRhsNames (DataTyCon tags) = map conTagName tags+algTyRhsNames (TupleTyCon tag) = [conTagName tag]+algTyRhsNames (NewTyCon tag) = [conTagName tag]++-- | Binding Names+bindingNames :: Binding -> [Name]+bindingNames (Binding _ bnds) = lhs ++ rhs+ where lhs = concatMap (varNames . fst) bnds+ rhs = concatMap (bindRhsNames . snd) bnds++-- | Path Constraint Names+pconsNames :: PathCons -> [Name]+pconsNames [] = []+pconsNames (c:cs) = pcondNames c ++ pconsNames cs++-- | Path Condition Names+pcondNames :: PathCond -> [Name]+pcondNames (PathCond alt expr locals _) = altNames alt ++ exprNames expr+ ++ localsNames locals++-- | Symbolic Link Names+linksNames :: SymLinks -> [Name]+linksNames (SymLinks links) = [] -- map (\(a, b) -> [a, b]) kvs+ where kvs = M.toList links++-- | Fresh String from Int Rand Seed+freshString :: Int -> String -> S.Set String -> String+freshString rand seed confs = if S.member seed confs+ then freshString (rand + 1) (seed ++ [pick]) confs+ else seed+ where pick = bank !! index+ index = raw_i `mod` (length bank)+ raw_i = (abs rand) * prime+ prime = 151 -- The original? :)+ bank = lower ++ upper ++ nums+ lower = "abcdefghijlkmnopqrstuvwxyz"+ upper = "ABCDEFGHIJKLMNOPQRSTUVWXYZ"+ nums = "1234567890"++-- | Fresh Name from Conflict List+freshName :: NameSpace -> [Name] -> Name+freshName nspace confs = freshSeededName seed confs+ where seed = Name "fs?" Nothing nspace 0++-- | Seeded Fresh Name from Conflict List+freshSeededName :: Name -> [Name] -> Name+freshSeededName seed confs = Name occ' mod ns unq'+ where Name occ mod ns unq = seed+ occ' = freshString 1 occ (S.fromList alls)+ unq' = maxs + 1+ alls = map nameOccStr confs+ maxs = L.maximum (unq : map nameUnique confs)++-- | List of Fresh Names+freshNameList :: [NameSpace] -> [Name] -> [Name]+freshNameList [] _ = []+freshNameList (nspace:nss) confs = name' : freshNameList nss confs'+ where name' = freshName nspace confs+ confs' = name' : confs++-- | List of Seeded Fresh Names+freshSeededNameList :: [Name] -> [Name] -> [Name]+freshSeededNameList [] _ = []+freshSeededNameList (n:ns) confs = name' : freshSeededNameList ns confs'+ where name' = freshSeededName n confs+ confs' = name' : confs+
+ src/SSTG/Core/Execution/Rules.hs view
@@ -0,0 +1,446 @@+-- | Rules+module SSTG.Core.Execution.Rules+ ( Rule(..)+ , reduce+ , isStateValueForm+ ) where++import SSTG.Core.Syntax+import SSTG.Core.Execution.Models+import SSTG.Core.Execution.Namer++import qualified Data.Map as M++-- | Rules+data Rule = RuleAtomLit | RuleAtomLitPtr | RuleAtomValPtr | RuleAtomUnInt+ | RulePrimApp+ | RuleConApp+ | RuleFunAppExact | RuleFunAppUnder | RuleFunAppSym | RuleFunAppUnInt+ | RuleLet+ | RuleCaseLit | RuleCaseConPtr | RuleCaseAnyLit | RuleCaseAnyConPtr+ | RuleCaseSym++ | RuleUpdateCThunk+ | RuleUpdateDLit | RuleUpdateDValPtr++ | RuleAltCCaseNonVal+ | RuleAltDLit | RuleAltDValPtr++ | RuleApplyCFunThunk | RuleApplyCFunAppOver+ | RuleApplyDReturnFun | RuleApplyDReturnSym++ | RuleIdentity+ deriving (Show, Eq, Read, Ord)++-- Stack Independent Rules++-- | Is Heap Normal Form?+-- Does not include LitObj. i.e. if something points to this, nothing to do.+isHeapValueForm :: HeapObj -> Bool+isHeapValueForm (SymObj _) = True+isHeapValueForm (ConObj _ _) = True+isHeapValueForm (FunObj (_:_) _ _) = True+isHeapValueForm _ = False++-- | Is Value Form+-- Either a lit or points to a heap value (not LitObj!)+isExprValueForm :: Expr -> Locals -> Globals -> Heap -> Bool+isExprValueForm (Atom (LitAtom _)) _ _ _ = True+isExprValueForm (Atom (VarAtom var)) locals globals heap =+ case vlookupHeap var locals globals heap of+ Just (_, hobj) -> isHeapValueForm hobj+ Nothing -> False+isExprValueForm _ _ _ _ = False++-- | Is State Value?+isStateValueForm :: State -> Bool+isStateValueForm State { state_stack = stack+ , state_heap = heap+ , state_code = code }+ | Stack [] <- stack+ , Return (LitVal _) <- code = True++ | Stack [] <- stack+ , Return (MemVal addr) <- code+ , Just hobj <- lookupHeap addr heap+ , isHeapValueForm hobj = True++ | otherwise = False++-- | Value to Lit+valueToLit :: Value -> Lit+valueToLit (LitVal lit) = lit+valueToLit (MemVal addr) = AddrLit (memAddrInt addr)++-- | Uneven Zipping+unevenZip :: [a] -> [b] -> ([(a, b)], Either [a] [b])+unevenZip as [] = ([], Left as)+unevenZip [] bs = ([], Right bs)+unevenZip (a:as) (b:bs) = ((a, b) : acc, rem)+ where (acc, rem) = unevenZip as bs++-- | Inject Type Closure+injTyClosure :: Type -> [Atom] -> Type+injTyClosure ty args = TyClosure ty (map atomType args)++-- | Bind Rhs to Heap Object+rhsToObj :: BindRhs -> Locals -> Globals -> Maybe HeapObj+rhsToObj (FunForm prms expr) locals _ = Just (FunObj prms expr locals)+rhsToObj (ConForm dcon args) locals globals = do+ arg_vals <- mapM (\a -> alookupValue a locals globals) args+ return (ConObj dcon arg_vals)++-- | Lift Let Binding+liftBinding :: Binding -> Locals -> Globals -> Heap -> Maybe (Heap, Locals)+liftBinding (Binding NonRec bnd) locals globals heap = do+ hobjs <- mapM (\r -> rhsToObj r locals globals) (map snd bnd)+ let (heap', addrs) = allocHeapList hobjs heap+ return (heap', locals)+liftBinding (Binding Rec bnd) (Locals lmap) globals heap = do+ let names = map (varName . fst) bnd+ let hfakes = map (const Blackhole) bnd+ -- Allocate dummy BlackholeS+ let (heap', addrs) = allocHeapList hfakes heap+ let mem_vals = map (\a -> MemVal a) addrs+ -- Use the allocated BlackholeS to construct the locals closure.+ let lmap' = M.fromList (zip names mem_vals)+ let locals' = Locals (M.union lmap' lmap)+ hobjs <- mapM (\r -> rhsToObj r locals' globals) (map snd bnd)+ let injects = zip addrs hobjs+ return (insertHeapList injects heap', locals')++-- | Default Alts+defaultAlts :: [Alt] -> [Alt]+defaultAlts alts = [a | a @ (Alt Default _ _) <- alts]++-- | AltCon Based Alts+altConAlts :: [Alt] -> [Alt]+altConAlts alts = [a | a @ (Alt acon _ _) <- alts, acon /= Default]++-- | Match Lit Alts+matchLitAlts :: Lit -> [Alt] -> [Alt]+matchLitAlts lit alts = [a | a @ (Alt (LitAlt alit) _ _) <- alts, lit == alit]++-- | Match Data Alts+matchDataAlts :: DataCon -> [Alt] -> [Alt]+matchDataAlts dc alts = [a | a @ (Alt (DataAlt adc) _ _) <- alts, dc == adc]++-- | Negate Path Cons+negatePathCons :: PathCons -> PathCons+negatePathCons pcs = map (\(PathCond a e l b) -> (PathCond a e l (not b))) pcs++-- | Lift Sym Alt+liftSymAlt :: Var -> MemAddr -> Var -> Locals -> Heap -> [Name] -> Alt ->+ (Expr, Locals, Heap, PathCons, [Name])+liftSymAlt mvar addr cvar locals heap confs (Alt ac params expr) =+ (expr, locals', heap', pcons, confs')+ where pre_names = freshSeededNameList (map varName params) confs+ sym_vars = map (\(p, n) -> Var n (varType p)) (zip params pre_names)+ sym_objs = map (\v -> SymObj (Symbol v)) sym_vars+ (heap', addrs) = allocHeapList sym_objs heap+ mem_vals = map (\a -> MemVal a) addrs+ llist = (cvar, MemVal addr) : zip params mem_vals+ locals' = insertLocalsList llist locals+ mxpr = Atom (VarAtom mvar)+ pcons = [PathCond (Alt ac params expr) mxpr locals' True]+ confs' = pre_names ++ confs++-- | Alt Closure to State+altClosureToState :: State -> (Expr, Locals, Heap, PathCons, [Name]) -> State+altClosureToState state (expr, locals, heap, pcons, confs) = state'+ where state' = state { state_heap = heap+ , state_code = Evaluate expr locals+ , state_names = confs ++ state_names state+ , state_paths = pcons ++ state_paths state }++-- | Reduce+reduce :: State -> Maybe (Rule, [State])+reduce state @ State { state_stack = stack+ , state_heap = heap+ , state_globals = globals+ , state_code = code+ , state_names = confs+ , state_paths = paths }++ -- Stack Independent Rules++ -- Atom Lit+ | Evaluate (Atom (LitAtom lit)) _ <- code = do+ return ( RuleAtomLit+ , [state { state_code = Return (LitVal lit) }])++ -- Atom Lit Pointer+ | Evaluate (Atom (VarAtom var)) locals <- code+ , Just (_, hobj) <- vlookupHeap var locals globals heap+ , LitObj lit <- hobj = do+ return ( RuleAtomLitPtr+ , [state { state_code = Evaluate (Atom (LitAtom lit)) locals }])++ -- Rule Atom Val Pointer+ | Evaluate (Atom (VarAtom var)) locals <- code+ , Just (addr, hobj) <- vlookupHeap var locals globals heap+ , isHeapValueForm hobj = do+ return ( RuleAtomValPtr+ , [state { state_code = Return (MemVal addr) }])++ -- Rule Atom Uninterpreted+ | Evaluate (Atom (VarAtom uvar)) locals <- code+ , Nothing <- vlookupHeap uvar locals globals heap = do+ let sname = freshSeededName (varName uvar) confs+ let svar = Var sname (varType uvar)+ let sym = Symbol svar+ let (heap', addr) = allocHeap (SymObj sym) heap+ let globals' = insertGlobals uvar (MemVal addr) globals+ return ( RuleAtomUnInt+ , [state { state_heap = heap'+ , state_globals = globals'+ , state_code = Evaluate (Atom (VarAtom uvar)) locals+ , state_names = sname : confs }])++ -- Prim Function App+ | Evaluate (PrimApp pfun args) locals <- code = do+ arg_vals <- mapM (\a -> alookupValue a locals globals) args+ let eval = SymLitEval pfun (map valueToLit arg_vals)+ return ( RulePrimApp+ , [state { state_code = Evaluate (Atom (LitAtom eval)) locals }])++ -- | Rule Con App+ | Evaluate (ConApp dcon args) locals <- code = do+ arg_vals <- mapM (\a -> alookupValue a locals globals) args+ let (heap', addr) = allocHeap (ConObj dcon arg_vals) heap+ return ( RuleConApp+ , [state { state_heap = heap'+ , state_code = Return (MemVal addr) }])++ -- | Rule Fun App Exact+ | Evaluate (FunApp fun args) locals <- code+ , Just (_, hobj) <- vlookupHeap fun locals globals heap+ , FunObj params expr fun_locs <- hobj+ , length params == length args = do+ arg_vals <- mapM (\a -> alookupValue a locals globals) args+ let fun_locs' = insertLocalsList (zip params arg_vals) fun_locs+ return ( RuleFunAppExact+ , [state { state_code = Evaluate expr fun_locs' }])++ -- Rule Fun App Under+ | Evaluate (FunApp fun args) locals <- code+ , Just (_, hobj) <- vlookupHeap fun locals globals heap+ , FunObj params expr fun_locs <- hobj+ , (_, Left ex_prms) <- unevenZip params args = do+ -- Set up existing closure first.+ arg_vals <- mapM (\a -> alookupValue a locals globals) args+ let fun_locs' = insertLocalsList (zip params arg_vals) fun_locs+ -- New Fun Object.+ let pfobj = FunObj ex_prms expr fun_locs'+ let (heap', pfaddr) = allocHeap pfobj heap+ return ( RuleFunAppUnder+ , [state { state_heap = heap'+ , state_code = Return (MemVal pfaddr) }])++ -- Rule Fun App Symbolic+ | Evaluate (FunApp sfun args) locals <- code+ , Just (_, hobj) <- vlookupHeap sfun locals globals heap+ , SymObj (Symbol svar) <- hobj = do+ let sname = freshSeededName (varName svar) confs+ let svar' = Var sname (injTyClosure (varType svar) args)+ let sym = Symbol svar'+ let (heap', addr) = allocHeap (SymObj sym) heap+ return ( RuleFunAppSym+ , [state { state_heap = heap'+ , state_code = Return (MemVal addr)+ , state_names = sname : confs }])++ -- Rule Fun App Uninterpreted+ | Evaluate (FunApp ufun args) locals <- code+ , Nothing <- vlookupHeap ufun locals globals heap = do+ let sname = freshSeededName (varName ufun) confs+ let svar = Var sname (varType ufun)+ let sym = Symbol svar+ let (heap', addr) = allocHeap (SymObj sym) heap+ let globals' = insertGlobals ufun (MemVal addr) globals+ return ( RuleFunAppUnInt+ , [state { state_heap = heap'+ , state_globals = globals'+ , state_code = Evaluate (FunApp ufun args) locals+ , state_names = sname : confs }])++ -- Rule Let+ | Evaluate (Let bnd expr) locals <- code = do+ (heap', locals') <- liftBinding bnd locals globals heap+ return ( RuleLet+ , [state { state_heap = heap'+ , state_code = Evaluate expr locals' }])++ -- Rule Case Lit+ | Evaluate (Case (Atom (LitAtom lit)) cvar alts) locals <- code+ , (Alt _ _ expr):_ <- matchLitAlts lit alts = do+ -- Account for cvar.+ let locals' = insertLocals cvar (LitVal lit) locals+ return ( RuleCaseLit+ , [state { state_code = Evaluate expr locals' }])++ -- Rule Case Con Pointer+ | Evaluate (Case (Atom (VarAtom mvar)) cvar alts) locals <- code+ , Just (addr, hobj) <- vlookupHeap mvar locals globals heap+ , ConObj dcon vals <- hobj+ , (Alt _ params expr):_ <- matchDataAlts dcon alts+ , length params == length vals = do+ -- Account for cvar.+ let llist = (cvar, MemVal addr) : zip params vals+ let locals' = insertLocalsList llist locals+ return ( RuleCaseConPtr+ , [state { state_code = Evaluate expr locals' }])++ -- Rule Case Any Lit+ | Evaluate (Case (Atom (LitAtom lit)) cvar alts) locals <- code+ , [] <- matchLitAlts lit alts+ , (Alt _ _ expr):_ <- defaultAlts alts = do+ -- Account for cvar.+ let locals' = insertLocals cvar (LitVal lit) locals+ return ( RuleCaseAnyLit+ , [state { state_code = Evaluate expr locals' }])++ -- Rule Case Any Con Pointer+ | Evaluate (Case (Atom (VarAtom mvar)) cvar alts) locals <- code+ , Just (addr, hobj) <- vlookupHeap mvar locals globals heap+ , ConObj dcon _ <- hobj+ , [] <- matchDataAlts dcon alts+ , (Alt _ _ expr):_ <- defaultAlts alts = do+ -- Account for cvar.+ let llist = (cvar, (MemVal addr)) : []+ let locals' = insertLocalsList llist locals+ return ( RuleCaseAnyConPtr+ , [state { state_code = Evaluate expr locals' }])++ -- Rule Case Sym+ | Evaluate (Case (Atom (VarAtom mvar)) cvar alts) locals <- code+ , Just (addr, hobj) <- vlookupHeap mvar locals globals heap+ , SymObj _ <- hobj+ , (acon_alts, def_alts) <- (altConAlts alts, defaultAlts alts)+ , length (acon_alts ++ def_alts) > 0 = do+ -- Remember to account for cvar.+ let acon_clss = map (liftSymAlt mvar addr cvar locals heap confs) acon_alts+ let def_clss = map (liftSymAlt mvar addr cvar locals heap confs) def_alts+ -- Make AltCon states first.+ let acon_sts = map (altClosureToState state) acon_clss+ -- Make Default states next.+ let all_pcons = concatMap (\(_, _, _, pc, _) -> pc) acon_clss+ let neg_pcons = negatePathCons all_pcons+ let def_clss' = map (\(e, l, h, p, c) -> (e, l, h, neg_pcons, c)) def_clss+ let def_sts = map (altClosureToState state) def_clss'+ return (RuleCaseSym, acon_sts ++ def_sts)++ -- Stack Dependent Rules++ -- Rule Update Frame Create Thunk+ | Stack frames <- stack+ , Evaluate (Atom (VarAtom var)) locals <- code+ , Just (addr, hobj) <- vlookupHeap var locals globals heap+ , FunObj [] expr fun_locs <- hobj = do -- Thunk form.+ return ( RuleUpdateCThunk+ , [state { state_stack = Stack (UpdateFrame addr : frames)+ , state_heap = insertHeap addr Blackhole heap+ , state_code = Evaluate expr fun_locs }])++ -- Rule Update Frame Delete Lit+ | Stack (UpdateFrame frm_addr : rest) <- stack+ , Return (LitVal lit) <- code = do+ return ( RuleUpdateDLit+ , [state { state_stack = Stack rest+ , state_heap = insertHeap frm_addr (LitObj lit) heap+ , state_code = Return (LitVal lit) }])++ -- Rule Update Frame Delete Val Pointer+ | Stack (UpdateFrame frm_addr : rest) <- stack+ , Return (MemVal addr) <- code+ , Just hobj <- lookupHeap addr heap+ , isHeapValueForm hobj = do+ return ( RuleUpdateDValPtr+ , [state { state_stack = Stack rest+ , state_heap = insertHeap frm_addr hobj heap+ , state_code = Return (MemVal addr) }])++ -- Rule Alt Frame Create Case Non LitVal or MemVal+ | Stack frames <- stack+ , Evaluate (Case mxpr cvar alts) locals <- code+ , not (isExprValueForm mxpr locals globals heap) = do+ return ( RuleAltCCaseNonVal+ , [state { state_stack = Stack (AltFrame cvar alts locals : frames)+ , state_code = Evaluate mxpr locals }])++ -- Rule Alt Frame Delete Lit+ | Stack (AltFrame cvar alts frm_locs : rest) <- stack+ , Return (LitVal lit) <- code = do+ let mxpr = Atom (LitAtom lit)+ return ( RuleAltDLit+ , [state { state_stack = Stack rest+ , state_code = Evaluate (Case mxpr cvar alts) frm_locs }])++ -- Rule Alt Frame Delete Heap Value+ | Stack (AltFrame cvar alts frm_locs : rest) <- stack+ , Return (MemVal addr) <- code+ , Just hobj <- lookupHeap addr heap+ , isHeapValueForm hobj = do+ let vname = freshSeededName (varName cvar) confs+ let vvar = Var vname (varType cvar)+ let mxpr = Atom (VarAtom vvar)+ let frm_locs' = insertLocals vvar (MemVal addr) frm_locs+ return ( RuleAltDValPtr+ , [state { state_stack = Stack rest+ , state_code = Evaluate (Case mxpr cvar alts) frm_locs'+ , state_names = vname : confs }])++ -- Rule Apply Frame Create Function Thunk+ | Stack frames <- stack+ , Evaluate (FunApp fun args) locals <- code+ , Just (_, hobj) <- vlookupHeap fun locals globals heap+ , FunObj [] expr fun_locs <- hobj = do+ return ( RuleApplyCFunThunk+ , [state { state_stack = Stack (ApplyFrame args locals : frames)+ , state_code = Evaluate expr fun_locs }])++ -- Rule Apply Frame Create Function Over Application+ | Stack frames <- stack+ , Evaluate (FunApp fun args) locals <- code+ , Just (_, hobj) <- vlookupHeap fun locals globals heap+ , FunObj params expr fun_locs <- hobj+ , (_, Right ex_args) <- unevenZip params args = do+ arg_vals <- mapM (\a -> alookupValue a locals globals) args+ let fun_locs' = insertLocalsList (zip params arg_vals) fun_locs+ return ( RuleApplyCFunAppOver+ , [state { state_stack = Stack (ApplyFrame ex_args locals : frames)+ , state_code = Evaluate expr fun_locs' }])++ -- Rule Apply Frame Delete ReturnPtr Function+ | Stack (ApplyFrame args frm_locs : rest) <- stack+ , Return (MemVal addr) <- code+ , Just hobj <- lookupHeap addr heap+ , FunObj _ _ _ <- hobj = do+ ftype <- memAddrType addr heap+ let fname = freshName VarNSpace confs+ let fvar = Var fname ftype+ let frm_locs' = insertLocals fvar (MemVal addr) frm_locs+ return ( RuleApplyDReturnFun+ , [state { state_stack = Stack rest+ , state_code = Evaluate (FunApp fvar args) frm_locs'+ , state_names = fname : confs }])++ -- Rule Apply Frame Delete ReturnPtr Sym+ | Stack (ApplyFrame args frm_locs : rest) <- stack+ , Return (MemVal addr) <- code+ , Just hobj <- lookupHeap addr heap+ , SymObj (Symbol sym) <- hobj = do+ let sname = freshSeededName (varName sym) confs+ let svar = Var sname (varType sym)+ let frm_locs' = insertLocals svar (MemVal addr) frm_locs+ return ( RuleApplyDReturnSym+ , [state { state_stack = Stack rest+ , state_code = Evaluate (FunApp svar args) frm_locs'+ , state_names = sname : confs }])++ -- State is Value Form+ | isStateValueForm state = return (RuleIdentity, [state])++ -- Everything Broke!!!+ | otherwise = Nothing+
+ src/SSTG/Core/Execution/Stepper.hs view
@@ -0,0 +1,42 @@+module SSTG.Core.Execution.Stepper+ ( LiveState+ , DeadState+ , runBoundedBFS+ , runBoundedDFS+ ) where++import SSTG.Core.Syntax+import SSTG.Core.Execution.Models+import SSTG.Core.Execution.Rules++import qualified Data.Map as M++type LiveState = ([Rule], State)++type DeadState = ([Rule], State)++incStatus :: Status -> Status+incStatus status = status { steps = (steps status) + 1 }++incState :: State -> State+incState state = state { state_status = incStatus (state_status state) }++step :: ([Rule], State) -> [([Rule], State)]+step (hist, state) = case reduce state of+ Nothing -> [(hist, state)]+ Just (rule, states) -> map (\s -> (hist ++ [rule], incState s)) states++pass :: [LiveState] -> ([LiveState], [DeadState] -> [DeadState])+pass rule_states = (lives, \prev -> prev ++ deads)+ where stepped = concatMap step rule_states+ lives = filter (not . isStateValueForm . snd) stepped+ deads = filter (isStateValueForm . snd) stepped++runBoundedBFS :: Int -> State -> ([LiveState], [DeadState])+runBoundedBFS n state = (run execution) [([], state)]+ where passes = take n (repeat (SymbolicT { run = pass }))+ start = SymbolicT { run = (\lives -> (lives, [])) }+ execution = foldl (\acc s -> s <*> acc) start passes++runBoundedDFS = undefined+
+ src/SSTG/Core/Syntax.hs view
@@ -0,0 +1,9 @@+-- | Export Module for SSTG.Syntax+module SSTG.Core.Syntax+ ( module SSTG.Core.Syntax.Language+ , module SSTG.Core.Syntax.Typer+ ) where++import SSTG.Core.Syntax.Language+import SSTG.Core.Syntax.Typer+
+ src/SSTG/Core/Syntax/Language.hs view
@@ -0,0 +1,143 @@+-- | SSTG Syntax Definitions+module SSTG.Core.Syntax.Language+ ( module SSTG.Core.Syntax.Language+ ) where++type Program = GenProgram Name Var++type Lit = GenLit Name Var+type Atom = GenAtom Name Var+type PrimFun = GenPrimFun Name Var+type Expr = GenExpr Name Var+type Alt = GenAlt Name Var+type AltCon = GenAltCon Name Var+type Binding = GenBinding Name Var+type BindRhs = GenBindRhs Name Var++type ConTag = GenConTag Name+type DataCon = GenDataCon Name+type Type = GenType Name+type TyBinder = GenTyBinder Name+type Coercion = GenCoercion Name+type TyCon = GenTyCon Name+type AlgTyRhs = GenAlgTyRhs Name++-- | STG Program+newtype GenProgram bnd var = Program [GenBinding bnd var]+ deriving (Show, Eq, Read)+-- | NameSpace+data NameSpace = VarNSpace | DataNSpace | TvNSpace | TcClsNSpace+ deriving (Show, Eq, Read, Ord)++-- | Name+data Name = Name String (Maybe String) NameSpace Int+ deriving (Show, Eq, Read, Ord)++-- | Variable+data Var = Var Name (GenType Name) deriving (Show, Eq, Read)++-- | Literal+data GenLit bnd var = MachChar Char (GenType bnd)+ | MachStr String (GenType bnd)+ | MachInt Int (GenType bnd)+ | MachWord Int (GenType bnd)+ | MachFloat Rational (GenType bnd)+ | MachDouble Rational (GenType bnd)+ | MachNullAddr (GenType bnd)+ | MachLabel String (Maybe Int) (GenType bnd)+ | BlankAddr+ | AddrLit Int+ | SymLit var+ | SymLitEval (GenPrimFun bnd var) [GenLit bnd var]+ deriving (Show, Eq, Read)++-- | Atomic+data GenAtom bnd var = VarAtom var+ | LitAtom (GenLit bnd var)+ deriving (Show, Eq, Read)++-- | Primitive Operation+data GenPrimFun bnd var = PrimFun bnd (GenType bnd) deriving (Show, Eq, Read)++-- | GenExpression+data GenExpr bnd var = Atom (GenAtom bnd var)+ | PrimApp (GenPrimFun bnd var) [GenAtom bnd var]+ | ConApp (GenDataCon bnd) [GenAtom bnd var]+ | FunApp var [GenAtom bnd var]+ | Let (GenBinding bnd var) (GenExpr bnd var)+ | Case (GenExpr bnd var) var [GenAlt bnd var]+ deriving (Show, Eq, Read)++-- | Case Alt+data GenAlt bnd var = Alt (GenAltCon bnd var) [var] (GenExpr bnd var)+ deriving (Show, Eq, Read)++-- | Alt Constructor+data GenAltCon bnd var = DataAlt (GenDataCon bnd)+ | LitAlt (GenLit bnd var)+ | Default+ deriving (Show, Eq, Read)++-- | Binding+data GenBinding bnd var = Binding RecForm [(var, GenBindRhs bnd var)]+ deriving (Show, Eq, Read)++-- | Recursive?+data RecForm = Rec | NonRec deriving (Show, Eq, Read)++-- | Form of Bind Rhs+data GenBindRhs bnd var = ConForm (GenDataCon bnd) [GenAtom bnd var]+ | FunForm [var] (GenExpr bnd var)+ deriving (Show, Eq, Read)++-- | Data Constructor ID+data GenConTag bnd = ConTag bnd Int deriving (Show, Eq, Read)++-- | Data Constructor+data GenDataCon bnd = DataCon (GenConTag bnd) (GenType bnd) [GenType bnd]+ deriving (Show, Eq, Read)++-- | Type+data GenType bnd = TyVarTy bnd (GenType bnd)+ | AppTy (GenType bnd) (GenType bnd)+ | ForAllTy (GenTyBinder bnd) (GenType bnd)+ | CastTy (GenType bnd) (GenCoercion bnd)+ | TyConApp (GenTyCon bnd) [GenType bnd]+ | CoercionTy (GenCoercion bnd)+ | LitTy TyLit+ | FunTy [GenType bnd]+ | TyClosure (GenType bnd) [GenType bnd]+ | Bottom+ deriving (Show, Eq, Read)++-- | TyBinder+data GenTyBinder bnd = NamedTyBndr bnd (GenType bnd)+ | AnonTyBndr (GenType bnd)+ deriving (Show, Eq, Read)++-- | TyLit+data TyLit = NumTyLit Int+ | StrTyLit String+ deriving (Show, Eq, Read)++-- | Coercion+data GenCoercion bnd = Coercion (GenType bnd) (GenType bnd)+ deriving (Show, Eq, Read)++-- | TyCon+data GenTyCon bnd = FunTyCon bnd+ | AlgTyCon bnd (GenAlgTyRhs bnd)+ | SynonymTyCon bnd+ | FamilyTyCon bnd+ | PrimTyCon bnd+ | PromotedDataCon bnd (GenDataCon bnd)+ | TcTyCon bnd+ deriving (Show, Eq, Read)++-- | Algebraic Type Constructor RHS+data GenAlgTyRhs bnd = AbstractTyCon Bool+ | DataTyCon [GenConTag bnd]+ | TupleTyCon (GenConTag bnd)+ | NewTyCon (GenConTag bnd)+ deriving (Show, Eq, Read)+
+ src/SSTG/Core/Syntax/Typer.hs view
@@ -0,0 +1,45 @@+-- | Typing Module+module SSTG.Core.Syntax.Typer+ ( module SSTG.Core.Syntax.Typer+ ) where++import SSTG.Core.Syntax.Language++varType :: Var -> Type+varType (Var _ ty) = ty++litType :: Lit -> Type+litType (MachChar _ ty) = ty+litType (MachStr _ ty) = ty+litType (MachInt _ ty) = ty+litType (MachWord _ ty) = ty+litType (MachFloat _ ty) = ty+litType (MachDouble _ ty) = ty+litType (MachNullAddr ty) = ty+litType (BlankAddr) = Bottom+litType (AddrLit addr) = Bottom+litType (SymLit var) = varType var+litType (SymLitEval pf args) = TyClosure (primFunType pf) (map litType args)++atomType :: Atom -> Type+atomType (VarAtom var) = varType var+atomType (LitAtom lit) = litType lit++primFunType :: PrimFun -> Type+primFunType (PrimFun _ ty) = ty++dataConType :: DataCon -> Type+dataConType (DataCon _ ty _) = ty++altType :: Alt -> Type+altType (Alt _ _ expr) = exprType expr++exprType :: Expr -> Type+exprType (Atom atom) = atomType atom+exprType (PrimApp pf args) = TyClosure (primFunType pf) (map atomType args)+exprType (ConApp dcon _) = dataConType dcon+exprType (FunApp fun args) = TyClosure (varType fun) (map atomType args)+exprType (Let _ expr) = exprType expr+exprType (Case _ _ (a:_)) = altType a+exprType _ = Bottom+
+ src/SSTG/Core/Translation.hs view
@@ -0,0 +1,7 @@+-- | Export Module for SSTG.Translation+module SSTG.Core.Translation+ ( module SSTG.Core.Translation.Haskell+ ) where++import SSTG.Core.Translation.Haskell+
+ src/SSTG/Core/Translation/Haskell.hs view
@@ -0,0 +1,247 @@+-- | Haskell Translation+-- Extracts SSTG from Haskell source.+module SSTG.Core.Translation.Haskell+ ( mkTargetBindings+ , mkIOStr+ ) where++import qualified SSTG.Core.Syntax.Language as SL++import BasicTypes+import Coercion+import CorePrep+import CoreSyn+import CoreToStg+import CostCentre+import DataCon+import FastString+import ForeignCall+import GHC+import GHC.Paths+import GhcMonad+import HscTypes+import Literal+import Module+import Name+import Outputable+import Pair+import PrimOp+import SrcLoc+import StgSyn+import TyCon+import TyCoRep+import Type+import UniqSet+import Unique+import Var as V++import System.IO++import qualified Data.IntMap as IM+import qualified Data.Maybe as MB++-- | Make IO String from Outputable+mkIOStr :: (Outputable a) => a -> IO String+mkIOStr obj = runGhc (Just libdir) $ do+ dflags <- getSessionDynFlags+ let ppr_str = showPpr dflags obj+ return ppr_str++-- | Make Target Bindings+-- Given project directory and source target, make binds, with dependencies.+mkTargetBindings :: FilePath -> FilePath -> IO [SL.Binding]+mkTargetBindings proj src = do+ (sums_gutss, dflags, env) <- mkCompileClosure proj src+ let (sums, gutss) = (map fst sums_gutss, map snd sums_gutss)+ let mod_lcs = map (\s -> (ms_mod s, ms_location s)) sums+ let m_bndss = map mg_binds gutss+ let m_tcss = map mg_tcs gutss++ let z1 = zip3 mod_lcs m_bndss m_tcss+ preps <- sequence $ map (\((m, l), b, t) -> corePrepPgm env m l b t) z1++ let z2 = zip (map fst mod_lcs) preps+ stg_bndss <- sequence $ map (\(m, p) -> coreToStg dflags m p) z2++ let sl_bnds = map mkBinding (concat stg_bndss)+ return sl_bnds++-- | Make Compilation Closure+-- Captures a snapshot of the DynFlags and HscEnv in addition to+-- the ModGuts in the ModuleGraph. This allows compilation to be, intheory,+-- more portable across different applications, since ModGuts is a crucial+-- intermediary for compilation in general.+mkCompileClosure :: FilePath -> FilePath ->+ IO ([(ModSummary, ModGuts)], DynFlags, HscEnv)+mkCompileClosure proj src = runGhc (Just libdir) $ do+ beta_flags <- getSessionDynFlags+ let dflags = beta_flags { importPaths = [proj] }+ setSessionDynFlags dflags+ env <- getSession+ target <- guessTarget src Nothing+ setTargets [target]+ load LoadAllTargets++ mod_graph <- getModuleGraph+ pmods <- (sequence . map parseModule) mod_graph+ tmods <- (sequence . map typecheckModule) pmods+ dmods <- (sequence . map desugarModule) tmods+ let mod_gutss = map coreModule dmods++ let zipd = (zip mod_graph mod_gutss, dflags, env)+ return zipd++-- | Make SSTG Expr+mkExpr :: StgExpr -> SL.Expr+mkExpr (StgLit lit) = SL.Atom (SL.LitAtom (mkLit lit))+mkExpr (StgApp occ args) = SL.FunApp (mkVar occ) (map mkArg args)+mkExpr (StgConApp dc args) = SL.ConApp (mkData dc) (map mkArg args)+mkExpr (StgOpApp op args _) = SL.PrimApp (mkPrimOp op) (map mkArg args)+mkExpr (StgTick _ expr) = mkExpr expr+mkExpr (StgLam _ _) = error "mkExpr: StgLam detected"+mkExpr (StgLet bnd expr) = SL.Let (mkBinding bnd) (mkExpr expr)+mkExpr (StgLetNoEscape _ _ bnd expr) = mkExpr (StgLet bnd expr)+mkExpr (StgCase mexpr _ _ bndr _ _ alts) =+ SL.Case (mkExpr mexpr) (mkVar bndr) (map mkAlt alts)++-- | Make SSTG Arg+mkArg :: StgArg -> SL.Atom+mkArg (StgVarArg occ) = SL.VarAtom (mkVar occ)+mkArg (StgLitArg lit) = SL.LitAtom (mkLit lit)++-- | Make SSTG Name+mkName :: Name -> SL.Name+mkName name = SL.Name occ mod ns unq+ where occ = (occNameString . nameOccName) name+ ns = (mkNameSpace . occNameSpace . nameOccName) name+ unq = (getKey . nameUnique) name+ mod = case nameModule_maybe name of+ Nothing -> Nothing+ Just md -> Just ((moduleNameString . moduleName) md)++-- | Make SSTG NameSpace+mkNameSpace :: NameSpace -> SL.NameSpace+mkNameSpace ns | isVarNameSpace ns = SL.VarNSpace+ | isTvNameSpace ns = SL.TvNSpace+ | isDataConNameSpace ns = SL.DataNSpace+ | isTcClsNameSpace ns = SL.TcClsNSpace+ | otherwise = error "mkNameSpace: unrecognized namespace"++-- | Make SSTG Var+mkVar :: Var -> SL.Var+mkVar var = SL.Var vname vtype+ where vname = (mkName . V.varName) var+ vtype = (mkType . varType) var++-- | Make SSTG Binding+mkBinding :: StgBinding -> SL.Binding+mkBinding (StgNonRec bnd rhs) = SL.Binding SL.NonRec [(mkVar bnd, mkRhs rhs)]+mkBinding (StgRec bnds) = SL.Binding SL.Rec+ (map (\(b, r) -> (mkVar b, mkRhs r)) bnds)++-- | Make SSTG Rhs+mkRhs :: StgRhs -> SL.BindRhs+mkRhs (StgRhsCon _ dc args) = SL.ConForm (mkData dc) (map mkArg args)+mkRhs (StgRhsClosure _ _ _ _ _ params expr) =+ SL.FunForm (map mkVar params) (mkExpr expr)++-- | Make SSTG Lit+mkLit :: Literal -> SL.Lit+mkLit lit = case lit of+ (MachChar char) -> SL.MachChar char ((mkType . literalType) lit)+ (MachStr bstr) -> SL.MachStr (show bstr) ((mkType . literalType) lit)+ (MachInt i) -> SL.MachInt (fromInteger i) ((mkType . literalType) lit)+ (MachInt64 i) -> SL.MachInt (fromInteger i) ((mkType . literalType) lit)+ (MachWord i) -> SL.MachWord (fromInteger i) ((mkType . literalType) lit)+ (MachWord64 i) -> SL.MachWord (fromInteger i) ((mkType . literalType) lit)+ (MachFloat rat) -> SL.MachFloat rat ((mkType . literalType) lit)+ (MachDouble rat) -> SL.MachDouble rat ((mkType . literalType) lit)+ (LitInteger i _) -> SL.MachInt (fromInteger i) ((mkType . literalType) lit)+ MachNullAddr -> SL.MachNullAddr ((mkType . literalType) lit)+ (MachLabel f m _) -> SL.MachLabel (unpackFS f) m ((mkType . literalType) lit)++-- | Make SSTG Data Constructor ID+mkDataId :: DataCon -> SL.ConTag+mkDataId datacon = SL.ConTag name tag+ where name = (mkName . dataConName) datacon+ tag = dataConTag datacon++-- | Make SSTG Data Constructor+mkData :: DataCon -> SL.DataCon+mkData datacon = SL.DataCon dcid ty args+ where dcid = mkDataId datacon+ ty = (mkType . dataConRepType) datacon+ args = map mkType (dataConOrigArgTys datacon)++-- | Make SSTG Primitive Operation+mkPrimOp :: StgOp -> SL.PrimFun+mkPrimOp (StgPrimOp op) = SL.PrimFun (SL.Name occ Nothing ns unq) ty+ where occname = primOpOcc op+ occ = occNameString occname+ ns = (mkNameSpace . occNameSpace) occname+ unq = primOpTag op+ ty = (mkType . primOpType) op+mkPrimOp otherwise = error "mkPrimOp: got StgPrimCallOp or StgFCallOp"++-- | Make SSTG Alt+mkAlt :: StgAlt -> SL.Alt+mkAlt (a, b, _, e) = SL.Alt (mkAltCon a) (map mkVar b) (mkExpr e)++-- | Make SSTG Alt Constructor+mkAltCon :: AltCon -> SL.AltCon+mkAltCon (DataAlt dc) = SL.DataAlt (mkData dc)+mkAltCon (LitAlt lit) = SL.LitAlt (mkLit lit)+mkAltCon DEFAULT = SL.Default++-- | Make SSTG Type+mkType :: Type -> SL.Type+mkType (TyVarTy v) = SL.TyVarTy (mkName (V.varName v)) (mkType (varType v))+mkType (AppTy t1 t2) = SL.AppTy (mkType t1) (mkType t2)+mkType (TyConApp tc ts) = SL.TyConApp (mkTyCon tc) (map mkType ts)+mkType (ForAllTy b ty) = SL.ForAllTy (mkTyBndr b) (mkType ty)+mkType (LitTy tlit) = SL.LitTy (mkTyLit tlit)+mkType (CastTy ty cor) = SL.CastTy (mkType ty) (mkCoercion cor)+mkType (CoercionTy cor) = SL.CoercionTy (mkCoercion cor)++-- | Make SSTG Kind+mkKind :: Kind -> SL.Type+mkKind = mkType++-- | Make SSTG Type Constructor+mkTyCon :: TyCon -> SL.TyCon+mkTyCon tc | isFunTyCon tc = SL.FunTyCon name+ | isAlgTyCon tc = SL.AlgTyCon name algrhs+ | isFamilyTyCon tc = SL.FamilyTyCon name+ | isPrimTyCon tc = SL.PrimTyCon name+ | isTcTyCon tc = SL.TcTyCon name+ | isTypeSynonymTyCon tc = SL.SynonymTyCon name+ | isPromotedDataCon tc = SL.PromotedDataCon name dcon+ | otherwise = error "mkTyCon: unrecognized TyCon"+ where name = (mkName . tyConName) tc+ kind = (mkKind . tyConKind) tc+ algrhs = (mkAlgTyConRhs . algTyConRhs) tc+ dcon = (mkData . MB.fromJust . isPromotedDataCon_maybe) tc++-- | Make SSTG Algebraic Type Constructor RHS+mkAlgTyConRhs :: AlgTyConRhs -> SL.AlgTyRhs+mkAlgTyConRhs (AbstractTyCon b) = SL.AbstractTyCon b+mkAlgTyConRhs (DataTyCon {data_cons = dcs}) = SL.DataTyCon (map mkDataId dcs)+mkAlgTyConRhs (TupleTyCon {data_con = dc}) = SL.TupleTyCon (mkDataId dc)+mkAlgTyConRhs (NewTyCon {data_con = dc}) = SL.NewTyCon (mkDataId dc)++-- | make SSTG Type Binder+mkTyBndr :: TyBinder -> SL.TyBinder+mkTyBndr (Anon ty) = SL.AnonTyBndr (mkType ty)+mkTyBndr (Named v f) = SL.NamedTyBndr (mkName (V.varName v))+ (mkType (varType v))++-- | Make SSTG Type Literal+mkTyLit :: TyLit -> SL.TyLit+mkTyLit (NumTyLit int) = SL.NumTyLit (fromInteger int)+mkTyLit (StrTyLit fs) = SL.StrTyLit (unpackFS fs)++-- | Make SSTG Coercion+mkCoercion :: Coercion -> SL.Coercion+mkCoercion coer = SL.Coercion (mkType a) (mkType b)+ where (a, b) = (unPair . coercionKind) coer+
+ src/SSTG/Utils.hs view
@@ -0,0 +1,7 @@+-- | Export Module for SSTG.Utils+module SSTG.Utils+ ( module SSTG.Utils.PrettyPrint+ ) where++import SSTG.Utils.PrettyPrint+
+ src/SSTG/Utils/PrettyPrint.hs view
@@ -0,0 +1,339 @@+module SSTG.Utils.PrettyPrint+ ( pprStateStr+ , pprLivesDeadsStr+ , pprBindingStr+ ) where++import SSTG.Core++import qualified Data.Map as M+import qualified Data.List as L++pprLivesDeadsStr :: ([LiveState], [DeadState]) -> String+pprLivesDeadsStr (lives, deads) = injNewLineSeps10 acc_strs+ where header = "(Lives, Deads)"+ lv_str = (injNewLineSeps5 . map pprLiveStr) lives+ dd_str = (injNewLineSeps5 . map pprDeadStr) deads+ acc_strs = [header, lv_str, dd_str]++pprLiveStr :: LiveState -> String+pprLiveStr (rules, state) = injNewLine acc_strs+ where header = "Live"+ rule_str = pprRulesStr rules+ st_str = pprStateStr state+ acc_strs = [header, rule_str, st_str]++pprDeadStr :: LiveState -> String+pprDeadStr (rules, state) = injNewLine acc_strs+ where header = "Dead"+ rule_str = pprRulesStr rules+ st_str = pprStateStr state+ acc_strs = [header, rule_str, st_str]++pprRuleStr :: Rule -> String+pprRuleStr rule = show rule++pprRulesStr :: [Rule] -> String+pprRulesStr rules = injIntoList (map pprRuleStr rules)++-- | Make String from State+pprStateStr :: State -> String+pprStateStr state = injNewLine acc_strs+ where status_str = (pprStatusStr . state_status) state+ stack_str = (pprStackStr . state_stack) state+ heap_str = (pprHeapStr . state_heap) state+ globals_str = (pprGlobalsStr . state_globals) state+ expr_str = (pprCodeStr . state_code) state+ names_str = (pprNamesStr . state_names) state+ pcons_str = (pprPConsStr . state_paths) state+ links_str = (pprLinksStr . state_links) state+ acc_strs = [ ">>>>> [State] >>>>>>>>>>>>>>>"+ , status_str+ , "----- [Stack] ---------------"+ , stack_str+ , "----- [Heap] ----------------"+ , heap_str+ , "----- [Globals] -------------"+ , globals_str+ , "----- [Expression] ----------"+ , expr_str+ , "----- [All Names] -------"+ , "" -- names_str+ , "----- [Path Constraint] -----"+ , pcons_str+ , "----- [Symbolic Links] ------"+ , links_str+ , "<<<<<<<<<<<<<<<<<<<<<<<<<<<<<" ]++-- | Sub Member String Wrapping+sub :: String -> String+sub str = "(" ++ str ++ ")"++-- | Inject with " "+injSpace :: [String] -> String+injSpace strs = L.intercalate " " strs++-- | Inject with ","+injComma :: [String] -> String+injComma strs = L.intercalate "," strs++-- | Inject New Line+injNewLine :: [String] -> String+injNewLine strs = L.intercalate "\n" strs++-- | Inj into List+injIntoList :: [String] -> String+injIntoList strs = "[" ++ (injComma strs) ++ "]"++-- | In Newline Separators+injNewLineSeps5 :: [String] -> String+injNewLineSeps5 strs = L.intercalate seps strs+ where seps = "\n-----\n"++injNewLineSeps10 :: [String] -> String+injNewLineSeps10 strs = L.intercalate seps strs+ where seps = "\n----------\n"++pprMemAddrStr :: MemAddr -> String+pprMemAddrStr (MemAddr int) = show int++pprNameStr :: Name -> String+pprNameStr name = show name++pprLitStr :: Lit -> String+pprLitStr lit = show lit++pprStatusStr :: Status -> String+pprStatusStr status = show status++pprStackStr :: Stack -> String+pprStackStr (Stack stack) = injNewLineSeps10 acc_strs+ where frame_strs = map pprFrameStr stack+ acc_strs = "Stack" : frame_strs++pprFrameStr :: Frame -> String+pprFrameStr (AltFrame var alts locals) = injNewLine acc_strs+ where header = "AltFrame"+ var_str = pprVarStr var+ alts_str = pprAltsStr alts+ locs_str = pprLocalsStr locals+ acc_strs = [header, var_str, alts_str, locs_str]+pprFrameStr (ApplyFrame args locals) = injNewLine acc_strs+ where header = "ApplyFrame"+ args_str = injIntoList (map pprAtomStr args)+ locs_str = pprLocalsStr locals+ acc_strs = [header, args_str, locs_str]+pprFrameStr (UpdateFrame addr) = injNewLine acc_strs+ where header = "UpdateFrame"+ addr_str = pprMemAddrStr addr+ acc_strs = [addr_str]++pprHeapObjStr :: HeapObj -> String+pprHeapObjStr Blackhole = "Blackhole!!!"+pprHeapObjStr (LitObj lit) = injSpace acc_strs+ where header = "LitObj"+ lit_str = pprLitStr lit+ acc_strs = [header, lit_str]+pprHeapObjStr (SymObj (Symbol sym)) = injSpace acc_strs+ where header = "SymObj"+ var_str = pprVarStr sym+ acc_strs = [header, var_str]+pprHeapObjStr (ConObj dcon vals) = injSpace acc_strs+ where header = "ConObj"+ dcon_str = pprDataConStr dcon+ vals_str = injIntoList (map pprValueStr vals)+ acc_strs = [header, dcon_str, vals_str]+pprHeapObjStr (FunObj params expr locals) = injSpace acc_strs+ where header = "FunObj"+ prms_str = injIntoList (map pprVarStr params)+ expr_str = pprExprStr expr+ locs_str = pprLocalsStr locals+ acc_strs = [header, prms_str, expr_str, locs_str]++pprHeapStr :: Heap -> String+pprHeapStr (Heap hmap addr) = injNewLine (map (\k -> ">" ++ k) acc_strs)+ where kvs = M.toList hmap+ addr_strs = map (pprMemAddrStr . fst) kvs+ hobj_strs = map (pprHeapObjStr . snd) kvs+ zipd_strs = zip addr_strs hobj_strs+ acc_strs = map (\(m, o) -> sub (m ++ "," ++ o)) zipd_strs++pprGlobalsStr :: Globals -> String+pprGlobalsStr (Globals gmap) = injNewLine (map (\k -> ">" ++ k) acc_strs)+ where kvs = M.toList gmap+ name_strs = map (pprNameStr . fst) kvs+ val_strs = map (pprValueStr . snd) kvs+ zipd_strs = zip name_strs val_strs+ acc_strs = map (\(n, v) -> sub (n ++ "," ++ v)) zipd_strs++pprLocalsStr :: Locals -> String+pprLocalsStr (Locals lmap) = injIntoList acc_strs+ where kvs = M.toList lmap+ name_strs = map (pprNameStr . fst) kvs+ val_strs = map (pprValueStr . snd) kvs+ zipd_strs = zip name_strs val_strs+ acc_strs = map (\(n, v) -> sub (n ++ "," ++ v)) zipd_strs++pprValueStr :: Value -> String+pprValueStr (LitVal lit) = injSpace acc_strs+ where header = "LitVal"+ lit_str = pprLitStr lit+ acc_strs = [header, lit_str]+pprValueStr (MemVal addr) = injSpace acc_strs+ where header = "MemVal"+ ptr_str = pprMemAddrStr addr+ acc_strs = [header, ptr_str]++pprVarStr :: Var -> String+pprVarStr (Var name ty) = injSpace acc_strs+ where header = "Var"+ name_str = (sub . pprNameStr) name+ type_str = (sub . pprTypeStr) ty+ acc_strs = [header, name_str, type_str]++pprAtomStr :: Atom -> String+pprAtomStr (VarAtom var) = injSpace acc_strs+ where header = "VarAtom"+ var_str = (sub . pprVarStr) var+ acc_strs = [header, var_str]+pprAtomStr (LitAtom lit) = injSpace acc_strs+ where header = "LitAtom"+ lit_str = (sub . pprLitStr) lit+ acc_strs = [header, lit_str]++pprConTagStr :: ConTag -> String+pprConTagStr (ConTag name int) = pprNameStr name++pprDataConStr :: DataCon -> String+pprDataConStr (DataCon id ty tys) = injSpace acc_strs+ where header = "DataCon"+ id_str = (sub . pprConTagStr) id+ ty_str = (sub . pprTypeStr) ty+ tys_str = injIntoList (map pprTypeStr tys)+ acc_strs = [header, id_str, ty_str, tys_str]++pprPrimFunStr :: PrimFun -> String+pprPrimFunStr (PrimFun name ty) = injSpace acc_strs+ where header = "PrimFun"+ name_str = (sub . pprNameStr) name+ type_str = (sub . pprTypeStr) ty+ acc_strs = [header, name_str, type_str]++pprAltCon :: AltCon -> String+pprAltCon (DataAlt dcon) = injSpace acc_strs+ where header = "DataAlt"+ dcon_str = (sub . pprDataConStr) dcon+ acc_strs = [header, dcon_str]+pprAltCon (LitAlt lit) = injSpace acc_strs+ where header = "LitAlt"+ lit_str = (sub . pprLitStr) lit+ acc_strs = [header, lit_str]+pprAltCon Default = "Default"++pprAltStr :: Alt -> String+pprAltStr (Alt acon var expr) = injSpace acc_strs+ where header = "Alt"+ acon_str = (sub . pprAltCon) acon+ vars_str = injIntoList (map pprVarStr var)+ expr_str = (sub . pprExprStr) expr+ acc_strs = [header, acon_str, vars_str, expr_str]++pprAltsStr :: [Alt] -> String+pprAltsStr alts = injIntoList (map pprAltStr alts)++pprBindRhsStr :: BindRhs -> String+pprBindRhsStr (FunForm params expr) = injSpace acc_strs+ where header = "FunForm"+ prms_str = injIntoList (map pprVarStr params)+ expr_str = (sub . pprExprStr) expr+ acc_strs = [header, prms_str, expr_str]+pprBindRhsStr (ConForm dcon args) = injSpace acc_strs+ where header = "ConForm"+ dcon_str = (sub . pprDataConStr) dcon+ args_str = injIntoList (map pprAtomStr args)+ acc_strs = [header, dcon_str, args_str]++bindStr :: (Var, BindRhs) -> String+bindStr (var, lamf) = (sub . injComma) acc_strs+ where var_str = pprVarStr var+ lamf_str = pprBindRhsStr lamf+ acc_strs = [var_str, lamf_str]++pprBindingStr :: Binding -> String+pprBindingStr (Binding rec bnds) = injSpace acc_strs+ where header = case rec of { Rec -> "Rec-Bind"; NonRec -> "NonRec-Bind" }+ bnds_str = injIntoList (map bindStr bnds)+ acc_strs = [header, bnds_str]++pprExprStr :: Expr -> String+pprExprStr (Atom atom) = injSpace acc_strs+ where header = "Atom"+ atom_str = (sub . pprAtomStr) atom+ acc_strs = [header, atom_str]+pprExprStr (FunApp var args) = injSpace acc_strs+ where header = "FunApp"+ var_str = (sub . pprVarStr) var+ args_str = injIntoList (map pprAtomStr args)+ acc_strs = [header, var_str, args_str]+pprExprStr (PrimApp pfun args) = injSpace acc_strs+ where header = "PrimApp"+ pfun_str = (sub . pprPrimFunStr) pfun+ args_str = injIntoList (map pprAtomStr args)+ acc_strs = [header, pfun_str, args_str]+pprExprStr (ConApp dcon args) = injSpace acc_strs+ where header = "ConApp"+ dcon_str = (sub . pprDataConStr) dcon+ args_str = injIntoList (map pprAtomStr args)+ acc_strs = [header, dcon_str, args_str]+pprExprStr (Case expr var alts) = injSpace acc_strs+ where header = "Case"+ expr_str = (sub . pprExprStr) expr+ var_str = (sub . pprVarStr) var+ alts_str = pprAltsStr alts+ acc_strs = [header, expr_str, var_str, alts_str]+pprExprStr (Let bnd expr) = injSpace acc_strs+ where header = "Let"+ bnd_str = (sub . pprBindingStr) bnd+ expr_str = (sub . pprExprStr) expr+ acc_strs = [header, bnd_str, expr_str]++pprTypeStr :: Type -> String+pprTypeStr ty = "__Type__"++-- | State Code String+pprCodeStr :: Code -> String+pprCodeStr (Evaluate expr locals) = injSpace acc_strs+ where header = "Evaluate"+ expr_str = (sub . pprExprStr) expr+ loc_str = (sub . pprLocalsStr) locals+ acc_strs = [header, expr_str, loc_str]+pprCodeStr (Return val) = injSpace acc_strs+ where header = "Return"+ val_str = pprValueStr val+ acc_strs = [header, val_str]++-- | All Names String+pprNamesStr :: [Name] -> String+pprNamesStr names = injIntoList (map pprNameStr names)++-- | Path Constraints String+pprPConsStr :: PathCons -> String+pprPConsStr pathcons = injNewLineSeps5 strs+ where strs = map pprPCondStr pathcons++-- | Path Condition String+pprPCondStr :: PathCond -> String+pprPCondStr (PathCond alt expr locals hold) = injIntoList acc_strs+ where alt_str = pprAltStr alt+ expr_str = pprExprStr expr+ locs_str = pprLocalsStr locals+ hold_str = case hold of { True -> "Positive"; False -> "Negative" }+ acc_strs = [alt_str, expr_str, locs_str, hold_str]++-- | Symbolic Links String+pprLinksStr :: SymLinks -> String+pprLinksStr (SymLinks links) = injNewLineSeps5 acc_strs+ where kvs = M.toList links+ acc_strs = map (\(k, v) -> pprNameStr k ++ " -> " ++ pprNameStr v) kvs++
+ test/Spec.hs view
@@ -0,0 +1,2 @@+main :: IO ()+main = putStrLn "Test suite not yet implemented"