diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -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? :) diff --git a/SSTG.cabal b/SSTG.cabal --- a/SSTG.cabal +++ b/SSTG.cabal @@ -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 diff --git a/app/Main.hs b/app/Main.hs --- a/app/Main.hs +++ b/app/Main.hs @@ -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) diff --git a/src/SSTG/Core/Execution.hs b/src/SSTG/Core/Execution.hs --- a/src/SSTG/Core/Execution.hs +++ b/src/SSTG/Core/Execution.hs @@ -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 diff --git a/src/SSTG/Core/Execution/Engine.hs b/src/SSTG/Core/Execution/Engine.hs --- a/src/SSTG/Core/Execution/Engine.hs +++ b/src/SSTG/Core/Execution/Engine.hs @@ -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 --} diff --git a/src/SSTG/Core/Execution/Namer.hs b/src/SSTG/Core/Execution/Namer.hs deleted file mode 100644 --- a/src/SSTG/Core/Execution/Namer.hs +++ /dev/null @@ -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 - diff --git a/src/SSTG/Core/Execution/Naming.hs b/src/SSTG/Core/Execution/Naming.hs new file mode 100644 --- /dev/null +++ b/src/SSTG/Core/Execution/Naming.hs @@ -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 + diff --git a/src/SSTG/Core/Execution/Rules.hs b/src/SSTG/Core/Execution/Rules.hs --- a/src/SSTG/Core/Execution/Rules.hs +++ b/src/SSTG/Core/Execution/Rules.hs @@ -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' }]) diff --git a/src/SSTG/Core/Execution/Stepper.hs b/src/SSTG/Core/Execution/Stepper.hs deleted file mode 100644 --- a/src/SSTG/Core/Execution/Stepper.hs +++ /dev/null @@ -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 - diff --git a/src/SSTG/Core/Execution/Stepping.hs b/src/SSTG/Core/Execution/Stepping.hs new file mode 100644 --- /dev/null +++ b/src/SSTG/Core/Execution/Stepping.hs @@ -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 + diff --git a/src/SSTG/Core/Syntax.hs b/src/SSTG/Core/Syntax.hs --- a/src/SSTG/Core/Syntax.hs +++ b/src/SSTG/Core/Syntax.hs @@ -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 diff --git a/src/SSTG/Core/Syntax/Typecheck.hs b/src/SSTG/Core/Syntax/Typecheck.hs new file mode 100644 --- /dev/null +++ b/src/SSTG/Core/Syntax/Typecheck.hs @@ -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 + diff --git a/src/SSTG/Core/Syntax/Typer.hs b/src/SSTG/Core/Syntax/Typer.hs deleted file mode 100644 --- a/src/SSTG/Core/Syntax/Typer.hs +++ /dev/null @@ -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 - diff --git a/src/SSTG/Utils.hs b/src/SSTG/Utils.hs --- a/src/SSTG/Utils.hs +++ b/src/SSTG/Utils.hs @@ -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 diff --git a/src/SSTG/Utils/FileIO.hs b/src/SSTG/Utils/FileIO.hs new file mode 100644 --- /dev/null +++ b/src/SSTG/Utils/FileIO.hs @@ -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) + diff --git a/src/SSTG/Utils/PrettyPrint.hs b/src/SSTG/Utils/PrettyPrint.hs deleted file mode 100644 --- a/src/SSTG/Utils/PrettyPrint.hs +++ /dev/null @@ -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 - - diff --git a/src/SSTG/Utils/Printing.hs b/src/SSTG/Utils/Printing.hs new file mode 100644 --- /dev/null +++ b/src/SSTG/Utils/Printing.hs @@ -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 + +