SSTG 0.1.0.4 → 0.1.0.5
raw patch · 17 files changed
+865/−708 lines, 17 files
Files
- README.md +66/−1
- SSTG.cabal +6/−5
- app/Main.hs +70/−18
- src/SSTG/Core/Execution.hs +4/−4
- src/SSTG/Core/Execution/Engine.hs +24/−17
- src/SSTG/Core/Execution/Namer.hs +0/−216
- src/SSTG/Core/Execution/Naming.hs +216/−0
- src/SSTG/Core/Execution/Rules.hs +5/−6
- src/SSTG/Core/Execution/Stepper.hs +0/−40
- src/SSTG/Core/Execution/Stepping.hs +49/−0
- src/SSTG/Core/Syntax.hs +2/−2
- src/SSTG/Core/Syntax/Typecheck.hs +46/−0
- src/SSTG/Core/Syntax/Typer.hs +0/−46
- src/SSTG/Utils.hs +4/−2
- src/SSTG/Utils/FileIO.hs +22/−0
- src/SSTG/Utils/PrettyPrint.hs +0/−351
- src/SSTG/Utils/Printing.hs +351/−0
README.md view
@@ -1,1 +1,66 @@-# SSTG+## SSTG+Haskell Symbolic Execution with STG Semantics++Based on the paper: [Making a Fast Curry: Push/Enter vs. Eval/Apply for Higher-order Languages][paper]++Hackage Page: https://hackage.haskell.org/package/SSTG++[paper]: http://community.haskell.org/~simonmar/papers/evalapplyjfp06.pdf++## Dependencies+* `ghc >= 8.0.1`++## Install+`cabal install SSTG`++## As an API+SSTG is designed for use as an API to perform extraction and symbolic execution of models extracted from Haskell source, curated by hand, or derived from other sources.++`import SSTG`++#### Program Model Extraction+SSTG represents [GHC StgSyn][stgsyn] as a near one-to-one translation of an internal language called [SSTG Lang][sstglang].++[stgsyn]: https://downloads.haskell.org/~ghc/8.0.1/docs/html/libraries/ghc-8.0.1/StgSyn.html+[sstglang]: https://github.com/AntonXue/SSTG/blob/master/src/SSTG/Core/Syntax/Language.hs++This can be extracted from Haskell source by performing a call to the function:++```+mkTargetBindings :: FilePath -> FilePath -> IO [SSTG.Binding]+mkTargetBinding proj src = ...+```++Here `proj` denotes the project directory, while `src` respresents the source file. This enables compilation of multiple Haskell files simultaneously, as GHC requires reference paths to a common project directory for compilation accuracy.++In a given file structure as follows:+```+path/to/stuff/+ +-- project/+ +-- folder-one/+ +-- source.hs+```+The corresponding `proj` and `src` would be equivalent to:+```+proj = path/to/stuff+src = path/to/stuff/folder-one/source.hs+```+The extracted `[SSTG.Binding]`, like almost everything in SSTG, is endowed with `Show, Equal, Read`. However, it is advised to use the pretty-print functions defined in `SSTG.Utils.Printing`. For instance:+```+pprBindingStr :: SSTG.Binding -> String+```++#### Defunctionalizatoin++#### Symbolic Execution++#### Constraint Solving+To come.++## TODO List+* Defunctionalization pre-processing+* SMT integration++## Shortcommings+* Uninterpreted function evaluations are abstracted as symbolic computations. This includes all functions defined in `Prelude` and those not defined in the scope of the target programs.+* There might be bugs, who knows? :)
SSTG.cabal view
@@ -1,5 +1,5 @@ name: SSTG-version: 0.1.0.4+version: 0.1.0.5 synopsis: STG Symbolic Execution description: Prototype of STG-based Symbolic Execution for Haskell. homepage: https://github.com/AntonXue/SSTG#readme@@ -21,15 +21,16 @@ , SSTG.Core.Translation.Haskell , SSTG.Core.Syntax , SSTG.Core.Syntax.Language- , SSTG.Core.Syntax.Typer+ , SSTG.Core.Syntax.Typecheck , SSTG.Core.Execution , SSTG.Core.Execution.Engine , SSTG.Core.Execution.Models- , SSTG.Core.Execution.Namer+ , SSTG.Core.Execution.Naming , SSTG.Core.Execution.Rules- , SSTG.Core.Execution.Stepper+ , SSTG.Core.Execution.Stepping , SSTG.Utils- , SSTG.Utils.PrettyPrint+ , SSTG.Utils.Printing+ , SSTG.Utils.FileIO ghc-options: -Wall -fmax-pmcheck-iterations=2000000 build-depends: base >= 4.7 && < 5 , ghc
app/Main.hs view
@@ -2,8 +2,57 @@ import SSTG +import qualified Data.Char as C+import qualified Data.List as L+import qualified Data.Map as M+ import System.Environment+import Text.Read +trim :: String -> String+trim = L.dropWhileEnd C.isSpace . L.dropWhile C.isSpace++trimSlash :: String -> String+trimSlash str = case trim str of+ "" -> ""+ trimmed -> case last trimmed of + '/' -> trimSlash (init trimmed)+ _ -> trimmed++matchArg :: String -> [String] -> (String -> a) -> a -> a+matchArg tgt args fun def = case L.elemIndex tgt args of+ Nothing -> def+ Just i -> if i >= length args+ then error ("Invalid use of " ++ tgt)+ else fun (args !! (i + 1)) -- fun (args !! (i + 1))++parseStepCount :: [String] -> Int+parseStepCount args = matchArg "--n" args read 200++parseStepType :: [String] -> StepType+parseStepType args = case matched of { Just t -> t; Nothing -> BFS }+ where matched = matchArg "--method" args (\a -> M.lookup a types) Nothing+ types = M.fromList [ ("bfs", BFS)+ , ("bfs-log", BFSLogged)+ , ("dfs", DFS)+ , ("dfs-log", DFSLogged) ]++parseDumpDir :: [String] -> Maybe FilePath+parseDumpDir args = case matchArg "--dump" args (readMaybe . show) Nothing of+ Nothing -> error "part1"+ Just raw -> case trimSlash raw of+ "" -> error "part2"+ ok -> Just ok++parseFlags :: [String] -> RunFlags+parseFlags args = RunFlags { step_count = parseStepCount args+ , step_type = parseStepType args+ , dump_dir = parseDumpDir args }++injDumpLocs :: String -> Int -> FilePath -> [FilePath]+injDumpLocs entry n dir = map (\i -> start ++ (show i) ++ ".txt") [1..n]+ where start = dir ++ "/" ++ entry+ main :: IO () main = do -- Get command line arguments.@@ -12,25 +61,28 @@ binds <- mkTargetBindings proj src -- Configure entry. let entry = if length tail_args > 0 then tail_args !! 0 else "main"-+ -- Get the flags.+ let flags = parseFlags tail_args -- Do the loading. let load_result = loadStateEntry entry (Program binds) putStrLn $ "binds: " ++ show (length binds)- -- putStrLn "Bindings"- -- mapM_ (putStrLn . pprBindingStr) binds-- case load_result of- LoadError str -> do- error str- LoadOkay state -> do- putStrLn" **************** INIT ***************"- putStrLn "Initial state:"- putStrLn $ pprStateStr state- putStrLn "*************** BEGIN ***************"- let lds = execute1 40 state- putStrLn $ pprLivesDeadsStr lds- LoadGuess state cands -> do- putStrLn $ pprStateStr state- putStrLn "Other possible candidates:"- putStrLn $ show cands+ -- Get the state from the loader.+ state <- case load_result of+ LoadError str -> error str+ LoadOkay state -> return state+ LoadGuess state cands -> do+ putStrLn "Other possible candidates:"+ putStrLn $ show cands+ return state+ putStrLn $ show flags+ -- Execution!+ let ldss = execute flags state+ case dump_dir flags of+ -- Dump to terminal.+ Nothing -> mapM_ (putStrLn . pprLivesDeadsStr) ldss+ -- Dump to file.+ Just dir -> do+ let locs = injDumpLocs entry (length ldss) dir+ putStrLn $ show (length ldss)+ mapM_ (\(fp, lds) -> writePrettyState fp lds) (zip locs ldss)
src/SSTG/Core/Execution.hs view
@@ -2,14 +2,14 @@ module SSTG.Core.Execution ( module SSTG.Core.Execution.Engine , module SSTG.Core.Execution.Models- , module SSTG.Core.Execution.Namer+ , module SSTG.Core.Execution.Naming , module SSTG.Core.Execution.Rules- , module SSTG.Core.Execution.Stepper+ , module SSTG.Core.Execution.Stepping ) where import SSTG.Core.Execution.Engine import SSTG.Core.Execution.Models-import SSTG.Core.Execution.Namer+import SSTG.Core.Execution.Naming import SSTG.Core.Execution.Rules-import SSTG.Core.Execution.Stepper+import SSTG.Core.Execution.Stepping
src/SSTG/Core/Execution/Engine.hs view
@@ -3,13 +3,16 @@ ( loadState , loadStateEntry , LoadResult (..)+ , RunFlags (..)+ , StepType (..)+ , execute , execute1 ) where import SSTG.Core.Syntax import SSTG.Core.Execution.Models-import SSTG.Core.Execution.Namer-import SSTG.Core.Execution.Stepper+import SSTG.Core.Execution.Naming+import SSTG.Core.Execution.Stepping import qualified Data.Map as M @@ -134,8 +137,7 @@ filter (\(var, _) -> st == (nameOccStr . varName) var) pairs -- | Load Code-loadCode :: Var -> BindRhs -> Locals -> Globals -> Heap ->- (Code, Globals, Heap)+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')@@ -165,21 +167,26 @@ | otherwise = base +-- | Run Flags+data RunFlags = RunFlags { step_count :: Int+ , step_type :: StepType+ , dump_dir :: Maybe FilePath+ } deriving (Show, Eq, Read)++-- | Step Type+data StepType = BFS | DFS | BFSLogged | DFSLogged deriving (Show, Eq, Read)++execute :: RunFlags -> State -> [([LiveState], [DeadState])]+execute flags state = step (step_count flags) state+ where step :: Int -> State -> [([LiveState], [DeadState])]+ step = case step_type flags of+ BFS -> \k s -> [runBoundedBFS k s]+ BFSLogged -> runBoundedBFSLogged+ DFS -> \k s -> [runBoundedDFS k s]+ DFSLogged -> runBoundedDFSLogged+ 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/Namer.hs
@@ -1,216 +0,0 @@--- | 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.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 (CaseFrame 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 ps expr locs) = exprNames expr ++ localsNames locs- ++ concatMap varNames ps---- | Symbol Names-symbolNames :: Symbol -> [Name]-symbolNames (Symbol sym mb_scls) = varNames sym ++ scls_names- where scls_names = case mb_scls of- Nothing -> []- Just (e, l) -> exprNames e ++ localsNames l---- | 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 t1 t2) = typeNames t1 ++ typeNames t2-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 tg ty tys) = conTagName tg : 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 (Promoted 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 _ bnd) = lhs ++ rhs- where lhs = concatMap (varNames . fst) bnd- rhs = concatMap (bindRhsNames . snd) bnd---- | Path Constraint Names-pconsNames :: PathCons -> [Name]-pconsNames [] = []-pconsNames (c:cs) = pcondNames c ++ pconsNames cs---- | Path Condition Names-pcondNames :: PathCond -> [Name]-pcondNames (PathCond (_, vars) expr locals _) = map varName vars ++- exprNames expr ++- localsNames locals---- | Symbolic Link Names-linksNames :: SymLinks -> [Name]-linksNames (SymLinks links) = concatMap (\(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' mdl ns unq'- where Name occ mdl 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/Naming.hs view
@@ -0,0 +1,216 @@+-- | Naming Module+module SSTG.Core.Execution.Naming+ ( allNames+ , freshString+ , freshName+ , freshSeededName+ , freshNameList+ , freshSeededNameList+ ) where++import SSTG.Core.Syntax+import SSTG.Core.Execution.Models++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 (CaseFrame 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 ps expr locs) = exprNames expr ++ localsNames locs+ ++ concatMap varNames ps++-- | Symbol Names+symbolNames :: Symbol -> [Name]+symbolNames (Symbol sym mb_scls) = varNames sym ++ scls_names+ where scls_names = case mb_scls of+ Nothing -> []+ Just (e, l) -> exprNames e ++ localsNames l++-- | 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 t1 t2) = typeNames t1 ++ typeNames t2+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 tg ty tys) = conTagName tg : 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 (Promoted 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 _ bnd) = lhs ++ rhs+ where lhs = concatMap (varNames . fst) bnd+ rhs = concatMap (bindRhsNames . snd) bnd++-- | Path Constraint Names+pconsNames :: PathCons -> [Name]+pconsNames [] = []+pconsNames (c:cs) = pcondNames c ++ pconsNames cs++-- | Path Condition Names+pcondNames :: PathCond -> [Name]+pcondNames (PathCond (_, vars) expr locals _) = map varName vars +++ exprNames expr +++ localsNames locals++-- | Symbolic Link Names+linksNames :: SymLinks -> [Name]+linksNames (SymLinks links) = concatMap (\(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' mdl ns unq'+ where Name occ mdl 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
@@ -7,7 +7,7 @@ import SSTG.Core.Syntax import SSTG.Core.Execution.Models-import SSTG.Core.Execution.Namer+import SSTG.Core.Execution.Naming -- | Rules data Rule = RuleAtomLit | RuleAtomLitPtr | RuleAtomValPtr | RuleAtomUnInt@@ -253,7 +253,7 @@ , state_code = Evaluate (Atom (LitAtom eval)) locals' , state_names = confs' }]) - -- | Rule Con App+ -- Rule Con App | Evaluate (ConApp dcon args) locals <- code = let pass_in = LiftAct args locals globals heap confs LiftAct vals _ globals' heap' confs' = liftAtomList pass_in@@ -264,7 +264,7 @@ , state_code = Return (MemVal addr) , state_names = confs' }]) - -- | Rule Fun App Exact+ -- Rule Fun App Exact | Evaluate (FunApp fun args) locals <- code , Just (_, hobj) <- vlookupHeap fun locals globals heap , FunObj params expr fun_locs <- hobj@@ -317,7 +317,7 @@ -- Rule Fun App Uninterpreted | Evaluate (FunApp ufun args) locals <- code- , Nothing <- vlookupHeap ufun locals globals heap =+ , Nothing <- vlookupHeap ufun locals globals heap = let pass_in = LiftAct ufun locals globals heap confs LiftAct _ locals' globals' heap' confs' = liftUnInt pass_in in Just (RuleFunAppUnInt@@ -368,8 +368,7 @@ , ConObj dcon _ <- hobj , [] <- matchDataAlts dcon alts , (Alt _ _ expr):_ <- defaultAlts alts =- let llist = (cvar, (MemVal addr)) : []- locals' = insertLocalsList llist locals+ let locals' = insertLocals cvar (MemVal addr) locals in Just (RuleCaseAnyConPtr ,[state { state_code = Evaluate expr locals' }])
− src/SSTG/Core/Execution/Stepper.hs
@@ -1,40 +0,0 @@-module SSTG.Core.Execution.Stepper- ( LiveState- , DeadState- , runBoundedBFS- , runBoundedDFS- ) where--import SSTG.Core.Execution.Models-import SSTG.Core.Execution.Rules--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 :: a-runBoundedDFS = undefined-
+ src/SSTG/Core/Execution/Stepping.hs view
@@ -0,0 +1,49 @@+module SSTG.Core.Execution.Stepping+ ( LiveState+ , DeadState+ , runBoundedBFS+ , runBoundedBFSLogged+ , runBoundedDFS+ , runBoundedDFSLogged+ ) where++import SSTG.Core.Execution.Models+import SSTG.Core.Execution.Rules++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++-- TODO: Optimize.+runBoundedBFSLogged :: Int -> State -> [([LiveState], [DeadState])]+runBoundedBFSLogged n state = map (\i -> runBoundedBFS i state) [1..n]++runBoundedDFS :: Int -> State -> ([LiveState], [DeadState])+runBoundedDFS = undefined++runBoundedDFSLogged :: Int -> State -> [([LiveState], [DeadState])]+runBoundedDFSLogged = undefined+
src/SSTG/Core/Syntax.hs view
@@ -1,9 +1,9 @@ -- | Export Module for SSTG.Syntax module SSTG.Core.Syntax ( module SSTG.Core.Syntax.Language- , module SSTG.Core.Syntax.Typer+ , module SSTG.Core.Syntax.Typecheck ) where import SSTG.Core.Syntax.Language-import SSTG.Core.Syntax.Typer+import SSTG.Core.Syntax.Typecheck
+ src/SSTG/Core/Syntax/Typecheck.hs view
@@ -0,0 +1,46 @@+-- | Typing Module+module SSTG.Core.Syntax.Typecheck+ ( module SSTG.Core.Syntax.Typecheck+ ) 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 (MachLabel _ _ ty) = ty+litType (BlankAddr) = Bottom+litType (AddrLit _) = Bottom+litType (SymLit var) = varType var+litType (SymLitEval pf args) = foldl AppTy (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) = foldl AppTy (primFunType pf) (map atomType args)+exprType (ConApp dcon _) = dataConType dcon+exprType (FunApp fun args) = foldl AppTy (varType fun) (map atomType args)+exprType (Let _ expr) = exprType expr+exprType (Case _ _ (a:_)) = altType a+exprType _ = Bottom+
− src/SSTG/Core/Syntax/Typer.hs
@@ -1,46 +0,0 @@--- | 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 (MachLabel _ _ ty) = ty-litType (BlankAddr) = Bottom-litType (AddrLit _) = Bottom-litType (SymLit var) = varType var-litType (SymLitEval pf args) = foldl AppTy (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) = foldl AppTy (primFunType pf) (map atomType args)-exprType (ConApp dcon _) = dataConType dcon-exprType (FunApp fun args) = foldl AppTy (varType fun) (map atomType args)-exprType (Let _ expr) = exprType expr-exprType (Case _ _ (a:_)) = altType a-exprType _ = Bottom-
src/SSTG/Utils.hs view
@@ -1,7 +1,9 @@ -- | Export Module for SSTG.Utils module SSTG.Utils- ( module SSTG.Utils.PrettyPrint+ ( module SSTG.Utils.FileIO+ , module SSTG.Utils.Printing ) where -import SSTG.Utils.PrettyPrint+import SSTG.Utils.FileIO+import SSTG.Utils.Printing
+ src/SSTG/Utils/FileIO.hs view
@@ -0,0 +1,22 @@+-- | File IO+module SSTG.Utils.FileIO+ ( writeState+ , readState+ , writePrettyState+ ) where++import SSTG.Core.Execution.Models+import SSTG.Core.Execution.Stepping+import SSTG.Utils.Printing++import Text.Read++writeState :: FilePath -> State -> IO ()+writeState file state = writeFile file (show state)++readState :: FilePath -> IO (Maybe State)+readState file = readFile file >>= \s -> return (readMaybe s :: Maybe State)++writePrettyState :: FilePath -> ([LiveState], [DeadState]) -> IO ()+writePrettyState file lds = writeFile file (pprLivesDeadsStr lds)+
− src/SSTG/Utils/PrettyPrint.hs
@@ -1,351 +0,0 @@-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] -------"- , fst ("", names_str) -- 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 (CaseFrame var alts locals) = injNewLine acc_strs- where header = "CaseFrame"- 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 = [header, addr_str]--pprSymClosureStr :: Maybe (Expr, Locals) -> String-pprSymClosureStr (Nothing) = "SymClosure ()"-pprSymClosureStr (Just (expr, locals)) = injSpace acc_strs- where header = "SymClosure"- expr_str = pprExprStr expr- locs_str = pprLocalsStr locals- acc_strs = [header, injIntoList [expr_str, locs_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 mb_scls)) = injSpace acc_strs- where header = "SymObj"- var_str = pprVarStr sym- scls_str = (sub . pprSymClosureStr) mb_scls- acc_strs = [header, var_str, scls_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- addr_str = pprMemAddrStr addr- kvs_strs = map (\(m, o) -> sub (m ++ "," ++ o)) zipd_strs- acc_strs = addr_str : kvs_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 _) = pprNameStr name--pprDataConStr :: DataCon -> String-pprDataConStr (DataCon tag ty tys) = injSpace acc_strs- where header = "DataCon"- tag_str = (sub . pprConTagStr) tag- ty_str = (sub . pprTypeStr) ty- tys_str = injIntoList (map pprTypeStr tys)- acc_strs = [header, tag_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]--pprAltConStr :: AltCon -> String-pprAltConStr (DataAlt dcon) = injSpace acc_strs- where header = "DataAlt"- dcon_str = (sub . pprDataConStr) dcon- acc_strs = [header, dcon_str]-pprAltConStr (LitAlt lit) = injSpace acc_strs- where header = "LitAlt"- lit_str = (sub . pprLitStr) lit- acc_strs = [header, lit_str]-pprAltConStr (Default) = "Default"--pprAltStr :: Alt -> String-pprAltStr (Alt acon var expr) = injSpace acc_strs- where header = "Alt"- acon_str = (sub . pprAltConStr) 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 bnd) = injSpace acc_strs- where header = case rec of { Rec -> "Rec"; NonRec -> "NonRec" }- bnds_str = injIntoList (map bindStr bnd)- 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 = fst ("__Type__", ty)---- | 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 (acon, params) expr locals hold) = injIntoList acc_strs- where acon_str = pprAltConStr acon- prms_str = injIntoList (map pprVarStr params)- expr_str = pprExprStr expr- locs_str = pprLocalsStr locals- hold_str = case hold of { True -> "Positive"; False -> "Negative" }- acc_strs = [acon_str, prms_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--
+ src/SSTG/Utils/Printing.hs view
@@ -0,0 +1,351 @@+module SSTG.Utils.Printing+ ( 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] -------"+ , fst ("", names_str) -- 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 (CaseFrame var alts locals) = injNewLine acc_strs+ where header = "CaseFrame"+ 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 = [header, addr_str]++pprSymClosureStr :: Maybe (Expr, Locals) -> String+pprSymClosureStr (Nothing) = "SymClosure ()"+pprSymClosureStr (Just (expr, locals)) = injSpace acc_strs+ where header = "SymClosure"+ expr_str = pprExprStr expr+ locs_str = pprLocalsStr locals+ acc_strs = [header, injIntoList [expr_str, locs_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 mb_scls)) = injSpace acc_strs+ where header = "SymObj"+ var_str = pprVarStr sym+ scls_str = (sub . pprSymClosureStr) mb_scls+ acc_strs = [header, var_str, scls_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+ addr_str = pprMemAddrStr addr+ kvs_strs = map (\(m, o) -> sub (m ++ "," ++ o)) zipd_strs+ acc_strs = addr_str : kvs_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 _) = pprNameStr name++pprDataConStr :: DataCon -> String+pprDataConStr (DataCon tag ty tys) = injSpace acc_strs+ where header = "DataCon"+ tag_str = (sub . pprConTagStr) tag+ ty_str = (sub . pprTypeStr) ty+ tys_str = injIntoList (map pprTypeStr tys)+ acc_strs = [header, tag_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]++pprAltConStr :: AltCon -> String+pprAltConStr (DataAlt dcon) = injSpace acc_strs+ where header = "DataAlt"+ dcon_str = (sub . pprDataConStr) dcon+ acc_strs = [header, dcon_str]+pprAltConStr (LitAlt lit) = injSpace acc_strs+ where header = "LitAlt"+ lit_str = (sub . pprLitStr) lit+ acc_strs = [header, lit_str]+pprAltConStr (Default) = "Default"++pprAltStr :: Alt -> String+pprAltStr (Alt acon var expr) = injSpace acc_strs+ where header = "Alt"+ acon_str = (sub . pprAltConStr) 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 bnd) = injSpace acc_strs+ where header = case rec of { Rec -> "Rec"; NonRec -> "NonRec" }+ bnds_str = injIntoList (map bindStr bnd)+ 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 = fst ("__Type__", ty)++-- | 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 (acon, params) expr locals hold) = injIntoList acc_strs+ where acon_str = pprAltConStr acon+ prms_str = injIntoList (map pprVarStr params)+ expr_str = pprExprStr expr+ locs_str = pprLocalsStr locals+ hold_str = case hold of { True -> "Positive"; False -> "Negative" }+ acc_strs = [acon_str, prms_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++