packages feed

SSTG 0.1.0.5 → 0.1.0.6

raw patch · 11 files changed

+272/−177 lines, 11 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

SSTG.cabal view
@@ -1,5 +1,5 @@ name:                SSTG-version:             0.1.0.5+version:             0.1.0.6 synopsis:            STG Symbolic Execution description:         Prototype of STG-based Symbolic Execution for Haskell. homepage:            https://github.com/AntonXue/SSTG#readme
src/SSTG/Core/Execution/Engine.hs view
@@ -22,13 +22,13 @@                 | LoadError String                 deriving (Show, Eq, Read) --- | Load State---   Guess the main function.+-- | Guess the main function as @"main"@, which is consistent with a few+-- experimental results. loadState :: Program -> LoadResult loadState prog = loadStateEntry main_occ_name prog   where main_occ_name = "main"  -- Based on a few experimental programs. --- | Specified Entry Point Load+-- | Load from a specified entry point. loadStateEntry :: String -> Program -> LoadResult loadStateEntry entry (Program bnds) = if length matches == 0     then LoadError ("No entry candidates found for: [" ++ entry ++ "]")@@ -122,8 +122,7 @@   where (heap', locals) = liftBinding bm globals heap         (res_heap, ls)  = liftBindings bms globals heap' --- | Entry Candidates---   Return a sub-list of bindings in which the entry candidate appears.+-- | Return a sub-list of bindings in which the entry candidate appears. entryMatches :: String -> [(Binding, Locals)] -> [(Binding, Locals)] entryMatches entry bnd_locs = filter (bindFilter entry) bnd_locs @@ -155,8 +154,7 @@         -- Set up code         code     = Evaluate (FunApp ent args) locals' --- | Trace Arguments---   We need to do stupid tracing if it's THUNK'D by default >:(+-- | We need to do stupid tracing if it's THUNK'D by default >:( traceArgs :: [Var] -> Expr -> Locals -> Globals -> Heap -> [Var] traceArgs base expr locals globals heap   | FunApp var []     <- expr@@ -167,15 +165,16 @@    | otherwise = base --- | Run Flags+-- | Run flags. data RunFlags = RunFlags { step_count :: Int                          , step_type  :: StepType                          , dump_dir   :: Maybe FilePath                          } deriving (Show, Eq, Read) --- | Step Type+-- | Step execution type. data StepType = BFS | DFS | BFSLogged | DFSLogged deriving (Show, Eq, Read) +-- | Perform execution on a `State` given the run flags. execute :: RunFlags -> State -> [([LiveState], [DeadState])] execute flags state = step (step_count flags) state   where step :: Int -> State -> [([LiveState], [DeadState])]@@ -185,6 +184,7 @@                    DFS       -> \k s -> [runBoundedDFS k s]                    DFSLogged -> runBoundedDFSLogged +-- | Simple `BFS` based execution on a state. execute1 :: Int -> State -> ([LiveState], [DeadState]) execute1 n state | n < 1     = ([([], state)], [])                  | otherwise = runBoundedBFS n state
src/SSTG/Core/Execution/Models.hs view
@@ -7,30 +7,29 @@  import qualified Data.Map as M --- | Symbolic Transformation---   We supply some state(s), it gives back those state(s) and some result.+-- | Symbolic Transformation represents transformations applied to some+-- State`(s). This is useful in allowing us to transfer from different actions+-- within the engine. newtype SymbolicT s a = SymbolicT { run :: s -> (s, a) } --- | Functor instance of Symbolic Transformation---   Apply transformations on the result.+-- | Functor instance of Symbolic Transformation. instance Functor (SymbolicT s) where     fmap f st = SymbolicT (\s0 -> let (s1, a1) = (run st) s0 in (s1, f a1)) --- | Applicative instance of Symbolic Transformation---   Can be used to chain together step-wise execution.+-- | Applicative instance of Symbolic Transformation. instance Applicative (SymbolicT s) where     pure a    = SymbolicT (\s -> (s, a))     sf <*> st = SymbolicT (\s0 -> let (s1, a1) = (run st) s0                                       (s2, f2) = (run sf) s1 in (s2, f2 a1)) --- | Monad instance of Symbolic Transformation---   Used for transitioning between different types of state manipulations.+-- | Monad instance of Symbolic Transformation. instance Monad (SymbolicT s) where     return a  = pure a     st >>= fs = SymbolicT (\s0 -> let (s1, a1) = (run st) s0                                       (s2, a2) = (run (fs a1)) s1 in (s2, a2)) --- | State+-- | `State` contains the information necessary to perform symbolic execution.+-- Eval/Apply graph reduction semantics are used. data State = State { state_status  :: Status                    , state_stack   :: Stack                    , state_heap    :: Heap@@ -41,37 +40,43 @@                    , state_links   :: SymLinks                    } deriving (Show, Eq, Read) --- | Symbolic+-- | Symbolic variables. The @Maybe (Expr, Locals)@ can be used to trace the+-- source from which the symbolic variable was generated. For instance, this is+-- useful during symbolic function application. data Symbol = Symbol Var (Maybe (Expr, Locals)) deriving (Show, Eq, Read) --- | Status+-- | State status. data Status = Status { steps :: Int                      } deriving (Show, Eq, Read) --- | Stack+-- | Execution stack used in graph reduction semnatics. newtype Stack = Stack [Frame] deriving (Show, Eq, Read) --- | Stack Frame+-- | Frames of a stack. data Frame = CaseFrame   Var [Alt] Locals            | ApplyFrame  [Atom]    Locals            | UpdateFrame MemAddr            deriving (Show, Eq, Read) --- | Memory Address+-- | Memory address for things on the `Heap`. newtype MemAddr = MemAddr Int deriving (Show, Eq, Read, Ord) --- | Value+-- | A `Value` is something that we aim to reduce our current expression down+-- into. `MemAddr` is a pointer to an object on the heap, such as `FunObj` or+-- `ConObj`, which are "returned" from expression evaluation in this form. data Value = LitVal Lit            | MemVal MemAddr            deriving (Show, Eq, Read) --- | Locals+-- | Locals binds a `Var`'s `Name` to its some `Value`. newtype Locals = Locals (M.Map Name Value) deriving (Show, Eq, Read) --- | Heap+-- | Heaps map `MemAddr` to `HeapObj`, while keeping track of the last address+-- that was allocated. This allows us to consistently allocate fresh addresses+-- on the `Heap`. data Heap = Heap (M.Map MemAddr HeapObj) MemAddr deriving (Show, Eq, Read) --- | Heap Object+-- | Heap objects. data HeapObj = LitObj Lit              | SymObj Symbol              | ConObj DataCon [Value]@@ -79,95 +84,101 @@              | Blackhole              deriving (Show, Eq, Read) --- | Globals+-- | Globals are statically loaded at the time when a `State` is loaded.+-- However, because uninterpreted / out-of-scope variables are made symbolic+-- at runtime, it can be modified during execution. newtype Globals = Globals (M.Map Name Value) deriving (Show, Eq, Read) --- | Evaluation State+-- | Evaluation of the current expression. We are either evaluating, or ready+-- to return with some `Value`. data Code = Evaluate Expr Locals           | Return   Value           deriving (Show, Eq, Read) --- | Path Constraints+-- | Path constraints. type PathCons = [PathCond] --- | Path Condition+-- | Path conditions denote logical paths taken in program execution thus far. data PathCond = PathCond (AltCon, [Var]) Expr Locals Bool               deriving (Show, Eq, Read) --- | Symbolic Link Table+-- | Symbolic link tables helps keep track of what names went to what, what? newtype SymLinks = SymLinks (M.Map Name Name) deriving (Show, Eq, Read)  --   Simple functions that require only the immediate data structure. --- | Name Occ String+-- | A `Name`'s occurrence string. nameOccStr :: Name -> String nameOccStr (Name occ _ _ _) = occ --- | Name Unique+-- | Name's unique `Int` key. nameUnique :: Name -> Int nameUnique (Name _ _ _ unq) = unq --- | Var Name+-- | Variable name. varName :: Var -> Name varName (Var name _) = name --- | Mem Addr Int+-- | `MemAddr`'s `Int` value. memAddrInt :: MemAddr -> Int memAddrInt (MemAddr int) = int --- | Lookup Locals+-- | `Locals` lookup. lookupLocals :: Var -> Locals -> Maybe Value lookupLocals var (Locals lmap) = M.lookup (varName var) lmap --- | Insert Locals+-- | `Locals` insertion. insertLocals :: Var -> Value -> Locals -> Locals insertLocals var val (Locals lmap) = Locals lmap'   where lmap' = M.insert (varName var) val lmap --- | Insert Locals List+-- | List insertion into `Locals`. insertLocalsList :: [(Var, Value)] -> Locals -> Locals insertLocalsList []               locals = locals insertLocalsList ((var, val):vvs) locals = insertLocalsList vvs locals'   where locals' = insertLocals var val locals --- | Lookup Heap+-- | `Heap` lookup. lookupHeap :: MemAddr -> Heap -> Maybe HeapObj lookupHeap addr (Heap hmap _) = M.lookup addr hmap --- | Allocate Heap+-- | `Heap` allocation. Updates the last `MemAddr` kept in the `Heap`. allocHeap :: HeapObj -> Heap -> (Heap, MemAddr) allocHeap hobj (Heap hmap prev) = (Heap hmap' addr, addr)   where addr  = MemAddr ((memAddrInt prev) + 1)         hmap' = M.insert addr hobj hmap --- | Allocate Heap List+-- | Allocate a list of `HeapObj` in a `Heap`, returning in the same order the+-- `MemAddr` at which they have been allocated at. allocHeapList :: [HeapObj] -> Heap -> (Heap, [MemAddr]) allocHeapList []           heap = (heap, []) allocHeapList (hobj:hobjs) heap = (heapf, addr : as)   where (heap', addr) = allocHeap hobj heap         (heapf, as)   = allocHeapList hobjs heap' --- | Insert Heap+-- | `Heap` direct insertion at a specific `MemAddr`. insertHeap :: MemAddr -> HeapObj -> Heap -> Heap insertHeap addr hobj (Heap hmap prev) = Heap hmap' prev   where hmap' = M.insert addr hobj hmap --- | Insert Heap List+-- | Insert a list of `HeapObj` at specified `MemAddr` locations. insertHeapList :: [(MemAddr, HeapObj)] -> Heap -> Heap insertHeapList []                 heap = heap insertHeapList ((addr, hobj):ahs) heap = insertHeapList ahs heap'   where heap' = insertHeap addr hobj heap --- | Lookup Globals+-- | `Globals` lookup. lookupGlobals :: Var -> Globals -> Maybe Value lookupGlobals var (Globals gmap) = M.lookup (varName var) gmap --- | Insert Globals+-- | `Globals` insertion. insertGlobals :: Var -> Value -> Globals -> Globals insertGlobals var val (Globals gmap) = Globals gmap'   where gmap' = M.insert (varName var) val gmap --- | Insert Globals List+-- | Insert a list of `Var` and `Value` pairs into `Globals`. This would+-- typically occur for new symbolic variables created from uninterpreted /+-- out-of-scope variables during runtime. insertGlobalsList :: [(Var, Value)] -> Globals -> Globals insertGlobalsList []               globals = globals insertGlobalsList ((var, val):vvs) globals = insertGlobalsList vvs globals'@@ -175,13 +186,13 @@  --   Complex functions that involve multiple data structures. --- | Lookup Value+-- | `Value` lookup from the `Locals` first, then `Globals`. lookupValue :: Var -> Locals -> Globals -> Maybe Value lookupValue var locals globals = case lookupLocals var locals of     Nothing -> lookupGlobals var globals     mb_val  -> mb_val --- | Lookup Heap by Variable+-- | `Heap` lookup. Returns the corresponding `MemAddr` and `HeapObj` if found. vlookupHeap :: Var -> Locals -> Globals -> Heap -> Maybe (MemAddr, HeapObj) vlookupHeap var locals globals heap = do     val <- lookupValue var locals globals@@ -189,7 +200,7 @@         LitVal _    -> Nothing         MemVal addr -> lookupHeap addr heap >>= \hobj -> Just (addr, hobj) --- | MemAddr Type+-- | Type of `HeapObj` held at `MemAddr`, if found. memAddrType :: MemAddr -> Heap -> Maybe Type memAddrType addr heap = do     hobj <- lookupHeap addr heap
src/SSTG/Core/Execution/Naming.hs view
@@ -15,7 +15,7 @@ import qualified Data.Map  as M import qualified Data.Set  as S --- | All Names in State+-- | All `Name`s in a `State`. allNames :: State -> [Name] allNames state = L.nub acc_ns   where stack_ns = stackNames   (state_stack   state)@@ -27,32 +27,32 @@         acc_ns   = stack_ns ++ heap_ns  ++ glbls_ns ++                    expr_ns  ++ pcons_ns ++ links_ns --- | Stack Names+-- | `Name`s in a `Stack`. stackNames :: Stack -> [Name] stackNames (Stack [])     = [] stackNames (Stack (f:fs)) = frameNames f ++ stackNames (Stack fs) --- | Frame Names+-- | `Name`s in a `Frame`. 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+-- | `Name`s in an `Alt`. altNames :: Alt -> [Name] altNames (Alt _ vars expr) = (concatMap varNames vars) ++ exprNames expr --- | Locals Names+-- | `Name`s in the `Locals` localsNames :: Locals -> [Name] localsNames (Locals lmap) = M.keys lmap --- | Heap Names+-- | `Name`s in the `Heap`. heapNames :: Heap -> [Name] heapNames (Heap heap _) = concatMap (heapObjNames . snd) kvs   where kvs = M.toList heap --- | Heap Object Names+-- | `Name`s in a `HeapObj`. heapObjNames :: HeapObj -> [Name] heapObjNames (Blackhole)           = [] heapObjNames (LitObj _)            = []@@ -61,37 +61,37 @@ heapObjNames (FunObj ps expr locs) = exprNames expr ++ localsNames locs                                                     ++ concatMap varNames ps --- | Symbol Names+-- | `Name`s in a `Symbol`. 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+-- | `Name`s in a `BindRhs`. bindRhsNames :: BindRhs -> [Name] bindRhsNames (FunForm prms expr) = (concatMap varNames prms) ++ exprNames expr bindRhsNames (ConForm dcon args) = dataNames dcon ++ concatMap atomNames args --- | Var Names+-- | `Name`s in a `Var`. varNames :: Var -> [Name] varNames (Var n t) = n : typeNames t --- | Atom Names+-- | `Name`s in an `Atom`. atomNames :: Atom -> [Name] atomNames (VarAtom var) = varNames var atomNames (LitAtom _)   = [] --- | Globals Names+-- | `Name`s in `Globals`. globalsNames :: Globals -> [Name] globalsNames (Globals gmap) = M.keys gmap --- | Eval State Names+-- | `Name`s in the current evaluation `Code`. codeNames :: Code -> [Name] codeNames (Return _)             = [] codeNames (Evaluate expr locals) = exprNames expr ++ localsNames locals --- | Expression Names+-- | `Name`s in an `Expr`. exprNames :: Expr -> [Name] exprNames (Atom atom)          = atomNames atom exprNames (FunApp fun args)    = varNames  fun  ++ concatMap atomNames args@@ -100,7 +100,7 @@ exprNames (Let binds expr)     = bindingNames binds ++ exprNames expr exprNames (Case expr var alts) = varNames var ++ exprNames expr                                               ++ concatMap altNames alts--- | Type Names+-- | `Name`s in a `Type`. typeNames :: Type -> [Name] typeNames (TyVarTy n ty)    = n : typeNames ty typeNames (AppTy t1 t2)     = typeNames t1  ++ typeNames t2@@ -112,24 +112,24 @@ typeNames (FunTy t1 t2)     = typeNames t1 ++ typeNames t2 typeNames (Bottom)          = [] --- | Prim Fun Names+-- | `Name`s in a `PrimFun`. pfunNames :: PrimFun -> [Name] pfunNames (PrimFun n ty) = n : typeNames ty --- | Data Constructor ID Names+-- | `Name`s in a `ConTag`. conTagName :: ConTag -> Name conTagName (ConTag n _) = n --- | Data Constructor Names+-- | `Name`s in a `DataCon`. dataNames :: DataCon -> [Name] dataNames (DataCon tg ty tys) = conTagName tg : concatMap typeNames (ty : tys) --- | Type Binder Names+-- | `Name`s in a `TyBinder`. tyBinderNames :: TyBinder -> [Name] tyBinderNames (NamedTyBndr n ty) = n : typeNames ty tyBinderNames (AnonTyBndr ty)    = typeNames ty --- | Type Constructor Names+-- | `Name`s in a `TyCon`. tyConNames :: TyCon -> [Name] tyConNames (FunTyCon n)      = [n] tyConNames (AlgTyCon n r)    = n : algTyRhsNames r@@ -139,40 +139,43 @@ tyConNames (TcTyCon n)       = [n] tyConNames (Promoted n dcon) = n : dataNames dcon --- | Coercion Names+-- | `Name`s in a `Coercion`. coercionNames :: Coercion -> [Name] coercionNames (Coercion t1 t2) = typeNames t1 ++ typeNames t2 --- | Type Alg Rhs Names+-- | `Name`s in a `AlgTyRhs`. algTyRhsNames :: AlgTyRhs -> [Name] algTyRhsNames (AbstractTyCon _) = [] algTyRhsNames (DataTyCon tags)  = map conTagName tags algTyRhsNames (TupleTyCon tag)  = [conTagName tag] algTyRhsNames (NewTyCon tag)    = [conTagName tag] --- | Binding Names+-- | `Name`s in a `Binding`. bindingNames :: Binding -> [Name] bindingNames (Binding _ bnd) = lhs ++ rhs   where lhs = concatMap (varNames . fst) bnd         rhs = concatMap (bindRhsNames . snd) bnd --- | Path Constraint Names+-- | `Name`s in a `PathCons`. pconsNames :: PathCons -> [Name] pconsNames []     = [] pconsNames (c:cs) = pcondNames c ++ pconsNames cs --- | Path Condition Names+-- | `Name`s in a `PathCond`. pcondNames :: PathCond -> [Name] pcondNames (PathCond (_, vars) expr locals _) = map varName vars ++                                                 exprNames expr   ++                                                 localsNames locals --- | Symbolic Link Names+-- | `Name`s in a `SymLinks`. linksNames :: SymLinks -> [Name] linksNames (SymLinks links) = concatMap (\(a, b) -> [a, b]) kvs   where kvs = M.toList links --- | Fresh String from Int Rand Seed+-- | Create a fresh seed given any `Int`, a `String` seed, and a `Set` of+-- `String`s that we do not want our new `String` to conflict with. The sole+-- purpose of the `Int` seed is to allow us tell us how much to multiply some+-- prime number to "orbit" an index around a fixed list of acceptable `Char`s. freshString :: Int -> String -> S.Set String -> String freshString rand seed confs = if S.member seed confs     then freshString (rand + 1) (seed ++ [pick]) confs@@ -186,12 +189,18 @@         upper = "ABCDEFGHIJKLMNOPQRSTUVWXYZ"         nums  = "1234567890" --- | Fresh Name from Conflict List+-- | Fresh `Name` given a list of `Name`s that acts as conflicts. The fresh+-- `Name`s generated in this manner are prefixed with @"fs?"@, which is not a+-- valid identifier in Haskell, but okay in SSTG. we also specify the+-- `NameSpace` under which the `Name` will be generated. This will generally+-- be `VarNSpace` in actual usage. freshName :: NameSpace -> [Name] -> Name freshName nspace confs = freshSeededName seed confs   where seed = Name "fs?" Nothing nspace 0 --- | Seeded Fresh Name from Conflict List+-- | A fresh `Name` generated from a seed `Name`, which will act as the prefix+-- of the new `Name`. We ues the same `NameSpace` as the seed `Name` when+-- generating this way. freshSeededName :: Name -> [Name] -> Name freshSeededName seed confs = Name occ' mdl ns unq'   where Name occ mdl ns unq = seed@@ -200,14 +209,15 @@         alls = map nameOccStr confs         maxs = L.maximum (unq : map nameUnique confs) --- | List of Fresh Names+-- | Generate a list of `Name`s, each corresponding to the appropriate element+-- of the `NameSpace` list. 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+-- | List of seeded fresh `Name`s. freshSeededNameList :: [Name] -> [Name] -> [Name] freshSeededNameList []     _     = [] freshSeededNameList (n:ns) confs = name' : freshSeededNameList ns confs'
src/SSTG/Core/Execution/Rules.hs view
@@ -9,7 +9,7 @@ import SSTG.Core.Execution.Models import SSTG.Core.Execution.Naming --- | Rules+-- | `Rule`s that are applied during STG reduction. data Rule = RuleAtomLit | RuleAtomLitPtr | RuleAtomValPtr | RuleAtomUnInt           | RulePrimApp           | RuleConApp@@ -33,17 +33,17 @@  --  Stack Independent Rules --- | Is Heap Normal Form?---   Does not include LitObj. i.e. if something points to this, nothing to do.+-- | Does not include `LitObj`. i.e. if something points to this, we have+-- nothing to do in terms of reducitons. isHeapValueForm :: HeapObj -> Bool isHeapValueForm (SymObj _)         = True isHeapValueForm (ConObj _ _)       = True isHeapValueForm (FunObj (_:_) _ _) = True isHeapValueForm _                  = False --- | Is Value Form---   Either a lit or points to a heap value (not LitObj!). If we find nothing---   in the heap, then this means we can still upcast the var to a symbolic.+-- | Either a `Lit` or points to a `Heap` value (not LitObj!). If we find+-- nothing in the `Heap`, then this means we can still upcast the var to a+-- symbolic that we create additional mappings to in the `Globals`. isExprValueForm :: Expr -> Locals -> Globals -> Heap -> Bool isExprValueForm (Atom (LitAtom _))   _      _       _    = True isExprValueForm (Atom (VarAtom var)) locals globals heap =@@ -52,7 +52,7 @@         Nothing        -> False isExprValueForm _                    _      _       _    = False --- | Is State Value?+-- | Is the `State` in a normal form that cannot be reduced further? isStateValueForm :: State -> Bool isStateValueForm State { state_stack = stack                        , state_heap  = heap@@ -67,22 +67,22 @@    | otherwise = False --- | Value to Lit+-- | `Value` to `Lit`. valueToLit :: Value -> Lit valueToLit (LitVal lit)  = lit valueToLit (MemVal addr) = AddrLit (memAddrInt addr) --- | Uneven Zipping+-- | Uneven `zip` of two `List`s, with the leftover stored. unevenZip :: [a] -> [b] -> ([(a, b)], Either [a] [b]) unevenZip as     []     = ([], Left as) unevenZip []     bs     = ([], Right bs) unevenZip (a:as) (b:bs) = ((a, b) : acc, excess)   where (acc, excess) = unevenZip as bs --- | Lift Action Wrap Type+-- | Lift action wrapper type. data LiftAct a = LiftAct  a Locals Globals Heap [Name] --- | Lift Uninterpreted Variable+-- | Lift uninterpreted `Var`s into `Globals`. liftUnInt :: LiftAct Var -> LiftAct MemAddr liftUnInt (LiftAct var locals globals heap confs) = pass_out   where sname    = freshSeededName (varName var) confs@@ -92,7 +92,7 @@         confs'   = sname : confs         pass_out = LiftAct addr locals globals' heap' confs' --- | Lift Atom+-- | Lift `Atom` if necessary (i.e. uinterpreted / out-of-scope). liftAtom :: LiftAct Atom -> LiftAct Value liftAtom (LiftAct atom locals globals heap confs) = pass_out   where pass_out = LiftAct aval locals globals' heap' confs'@@ -104,7 +104,7 @@                                 LiftAct addr _ g' h' c' = liftUnInt pass_in                             in (MemVal addr, g', h', c') --- | Lift Atom List+-- | Lift a list of `Atom`s. liftAtomList :: LiftAct [Atom] -> LiftAct [Value] liftAtomList (LiftAct []        locals globals heap confs) = pass_out   where pass_out  = LiftAct [] locals globals heap confs@@ -115,7 +115,7 @@         LiftAct vs  localsf globalsf heapf confsf = liftAtomList pass_rest         pass_out  = LiftAct (val : vs) localsf globalsf heapf confsf --- | Lift Bind Rhs+-- | Lift `BindRhs`. liftBindRhs :: LiftAct BindRhs -> LiftAct HeapObj liftBindRhs (LiftAct (FunForm prms expr) locals globals heap confs) = pass_out   where pass_out = LiftAct (FunObj prms expr locals) locals globals heap confs@@ -124,7 +124,7 @@         LiftAct vals locals' globals' heap' confs' = liftAtomList pass_in         pass_out = LiftAct (ConObj dcon vals) locals' globals' heap' confs' --- | Lift Bind Rhs List+-- | Lift `BindRhs` list. liftBindRhsList :: LiftAct [BindRhs] -> LiftAct [HeapObj] liftBindRhsList (LiftAct []       locals globals heap confs) = pass_out   where pass_out  = LiftAct [] locals globals heap confs@@ -135,7 +135,7 @@         LiftAct hos localsf globalsf heapf confsf = liftBindRhsList pass_rest         pass_out  = LiftAct (hobj : hos) localsf globalsf heapf confsf --- | Lift Binding+-- | Lift `Binding`. liftBinding :: LiftAct Binding -> LiftAct () liftBinding (LiftAct (Binding NonRec bnd) locals globals heap confs) = pass_out   where pass_in  = LiftAct (map snd bnd) locals globals heap confs@@ -156,27 +156,27 @@         heapf    = insertHeapList (zip addrs hobjs) heap''         pass_out = LiftAct () localsf globals' heapf confs' --- | Default Alts+-- | `Default` `Alt` branches in a `Case`. defaultAlts :: [Alt] -> [Alt] defaultAlts alts = [a | a @ (Alt Default _ _) <- alts] --- | AltCon Based Alts+-- | `AltCon` `Alt` branches in a `Case`. altConAlts :: [Alt] -> [Alt] altConAlts alts = [a | a @ (Alt acon _ _) <- alts, acon /= Default] --- | Match Lit Alts+-- | Match `LitAlt` `Alt` branches. matchLitAlts :: Lit -> [Alt] -> [Alt] matchLitAlts lit alts = [a | a @ (Alt (LitAlt alit) _ _) <- alts, lit == alit] --- | Match Data Alts+-- | Match `DataCon` `Alt` branches. matchDataAlts :: DataCon -> [Alt] -> [Alt] matchDataAlts dc alts = [a | a @ (Alt (DataAlt adc) _ _) <- alts, dc == adc] --- | Negate Path Cons+-- | Negate `PathCons`. negatePathCons :: PathCons -> PathCons negatePathCons pcs = map (\(PathCond a e l b) -> (PathCond a e l (not b))) pcs --- | Lift Sym Alt+-- | Lift `Alt`s during branching caused by symbolics. liftSymAlt :: LiftAct (Var, MemAddr, Var, Alt) -> LiftAct (Expr, PathCons) liftSymAlt (LiftAct args locals globals heap confs) = pass_out   where (mvar, addr, cvar, Alt ac params expr) = args@@ -192,7 +192,7 @@         confs'   = snames ++ confs         pass_out = LiftAct (expr, pcons) locals' globals heap' confs' --- | Alt Closure to State+-- | `Alt` closure to `State`. liftedAltToState :: State -> LiftAct (Expr, PathCons) -> State liftedAltToState state (LiftAct args locals globals heap confs) = state'   where (expr, pcons) = args@@ -202,7 +202,8 @@                        , state_names   = confs                        , state_paths   = pcons ++ state_paths state } --- | Reduce+-- | Reduce the state if it matches some type of reduction `Rule`. Return+-- `Nothing` to denote that rule application has completely failed. reduce :: State -> Maybe (Rule, [State]) reduce state @ State { state_stack   = stack                      , state_heap    = heap
src/SSTG/Core/Execution/Stepping.hs view
@@ -1,3 +1,4 @@+-- | Stepping Methods module SSTG.Core.Execution.Stepping     ( LiveState     , DeadState@@ -10,40 +11,56 @@ import SSTG.Core.Execution.Models import SSTG.Core.Execution.Rules +-- | A `State` that is not in value form yet, capable of being evaluated. A+-- list of `Rule`s is kept to denote reduction history. type LiveState = ([Rule], State) +-- | A `State` that is in value form. A list of `Rule`s is kept to denote+-- reduction history. type DeadState = ([Rule], State) +-- | Increment the `steps` counter of a `Status`. incStatus :: Status -> Status incStatus status = status { steps = (steps status) + 1 } +-- | Increment the `steps` counter inside the `state_status`. incState :: State -> State incState state = state { state_status = incStatus (state_status state) } +-- | Given a list of `State` along with its list of past `Rule` reductions,+-- apply STG reduction. If reduction yields `Nothing`, simply return itself. 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 +-- | This is what we use the `<*>` over. 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 +-- | Run bounded breadth-first-search of the execution space with an `Int` to+-- denote the maximum number of steps to take. 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.+-- | Run bounded breadth-first-search of the execution state with an `Int` to+-- denote the maximum number of steps to take. We keep track of a list to track+-- a history of all the execution snapshots. As it stands, this is currently+-- very NOT optimized. runBoundedBFSLogged :: Int -> State -> [([LiveState], [DeadState])] runBoundedBFSLogged n state = map (\i -> runBoundedBFS i state) [1..n] +-- | Currently @undefined@. runBoundedDFS :: Int -> State -> ([LiveState], [DeadState]) runBoundedDFS = undefined +-- | Currently @undefined@. runBoundedDFSLogged :: Int -> State -> [([LiveState], [DeadState])] runBoundedDFSLogged = undefined
src/SSTG/Core/Syntax/Language.hs view
@@ -22,21 +22,31 @@ type TyCon    = GenTyCon    Name type AlgTyRhs = GenAlgTyRhs Name --- | STG Program+-- | A Program is defined as a list of bindings. The @bnd@ is an identifier+-- that determines a unique binder to the @var@. In practice, these are defined+-- to be `Name` and `Var` respectively. newtype GenProgram bnd var = Program [GenBinding bnd var]                            deriving (Show, Eq, Read)--- | NameSpace++-- | Variables, data constructors, type variables, and type constructors. data NameSpace = VarNSpace | DataNSpace | TvNSpace | TcClsNSpace                deriving (Show, Eq, Read, Ord) --- | Name+-- | The occurrence name is defined as a string, with a `Maybe` module name+-- appearing. The `Int` denotes a `Unique` translated from GHC. For instance,+-- in the case of @Map.empty@, the occurrence name is @"empty"@, while the+-- module name is some variant of @Just \"Data.Map\"@. data Name = Name String (Maybe String) NameSpace Int           deriving (Show, Eq, Read, Ord) --- | Variable+-- | Variables consist of a `Name` and a `Type`. data Var = Var Name (GenType Name) deriving (Show, Eq, Read) --- | Literal+-- | Literals are largely augmented from the original GHC implementation, with+-- additional annotations to denote `BlankAddr` for lifting, `AddrLit` for+-- value deriviation, `SymLit` for symbolic literals, and `SymLitEval` to+-- represent symbolic literal evaluation, as literal manipulation functions+-- are defined in the Haskell Prelude, and thus outside of scope for us. data GenLit bnd var = MachChar   Char     (GenType bnd)                     | MachStr    String   (GenType bnd)                     | MachInt    Int      (GenType bnd)@@ -51,15 +61,16 @@                     | SymLitEval (GenPrimFun bnd var) [GenLit bnd var]                     deriving (Show, Eq, Read) --- | Atomic+-- | Atomic objects. `VarAtom` may be used for variable lookups, while+-- `LitAtom` is used to denote literals. data GenAtom bnd var = VarAtom var                      | LitAtom (GenLit bnd var)                      deriving (Show, Eq, Read) --- | Primitive Operation+-- | Primitive functions. data GenPrimFun bnd var = PrimFun bnd (GenType bnd) deriving (Show, Eq, Read) --- | GenExpression+-- | Expressions closely correspond to their representation in GHC. data GenExpr bnd var = Atom    (GenAtom bnd var)                      | PrimApp (GenPrimFun bnd var)  [GenAtom bnd var]                      | ConApp  (GenDataCon bnd)      [GenAtom bnd var]@@ -68,7 +79,8 @@                      | Case    (GenExpr bnd var) var [GenAlt bnd var]                      deriving (Show, Eq, Read) --- | Case Alt+-- | Alternatives utilize an `AltCon`, a list of parameters of that match to+-- the appropriate `DataAlt` as applicable, and an expression for the result. data GenAlt bnd var = Alt (GenAltCon bnd var) [var] (GenExpr bnd var)                     deriving (Show, Eq, Read) @@ -85,19 +97,23 @@ -- | Recursive? data RecForm = Rec | NonRec deriving (Show, Eq, Read) --- | Form of Bind Rhs+-- | `BindRhs` taken straight from STG can be either in constructor form, or+-- function form. Empty parameter list denotes a thunk. data GenBindRhs bnd var = ConForm (GenDataCon bnd) [GenAtom bnd var]                         | FunForm [var]            (GenExpr bnd var)                         deriving (Show, Eq, Read) --- | Data Constructor ID+-- | Data Constructor tag that uniquely identifiers data constructors. data GenConTag bnd = ConTag bnd Int deriving (Show, Eq, Read) --- | Data Constructor+-- | Data Constructor consists of its tag, the type that corresponds to its+-- ADT, and a list of paramters it takes. data GenDataCon bnd = DataCon (GenConTag bnd) (GenType bnd) [GenType bnd]                     deriving (Show, Eq, Read) --- | Type+-- | Types are information that are useful to keep during symbolic execution+-- in order to generate correct feeds into the SMT solver. Overapproxmation is+-- currently performed, and is likely to be cut back in the future. data GenType bnd = TyVarTy    bnd               (GenType bnd)                  | AppTy      (GenType bnd)     (GenType bnd)                  | ForAllTy   (GenTyBinder bnd) (GenType bnd)@@ -109,21 +125,21 @@                  | Bottom                  deriving (Show, Eq, Read) --- | TyBinder+-- | Type binder for `ForAllTy`. data GenTyBinder bnd = NamedTyBndr bnd (GenType bnd)                      | AnonTyBndr      (GenType bnd)                      deriving (Show, Eq, Read) --- | TyLit+-- | `Type` literal. data TyLit = NumTyLit Int            | StrTyLit String            deriving (Show, Eq, Read) --- | Coercion+-- | Coercion. I have no idea what this does :) data GenCoercion bnd = Coercion (GenType bnd) (GenType bnd)                      deriving (Show, Eq, Read) --- | TyCon+-- | Type constructor. data GenTyCon bnd = FunTyCon     bnd                   | AlgTyCon     bnd (GenAlgTyRhs bnd)                   | SynonymTyCon bnd@@ -133,7 +149,7 @@                   | TcTyCon      bnd                   deriving (Show, Eq, Read) --- | Algebraic Type Constructor RHS+-- | ADT RHS. data GenAlgTyRhs bnd = AbstractTyCon Bool                      | DataTyCon     [GenConTag bnd]                      | TupleTyCon    (GenConTag bnd)
src/SSTG/Core/Syntax/Typecheck.hs view
@@ -5,9 +5,11 @@  import SSTG.Core.Syntax.Language +-- | Variable type. varType :: Var -> Type varType (Var _ ty) = ty +-- | Literal type. litType :: Lit -> Type litType (MachChar _ ty)      = ty litType (MachStr _ ty)       = ty@@ -22,24 +24,29 @@ litType (SymLit var)         = varType var litType (SymLitEval pf args) = foldl AppTy (primFunType pf) (map litType args) +-- | Atom type. atomType :: Atom -> Type atomType (VarAtom var) = varType var atomType (LitAtom lit) = litType lit +-- | Primitive function type. primFunType :: PrimFun -> Type primFunType (PrimFun _ ty) = ty +-- | Data constructor type denoted as a function. dataConType :: DataCon -> Type-dataConType (DataCon _ ty _) = ty+dataConType (DataCon _ ty tys) = foldr FunTy ty tys +-- | Alt type altType :: Alt -> Type altType (Alt _ _ expr) = exprType expr +-- | I wonder what this could possibly be? 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 (ConApp dc args)  = foldl AppTy (dataConType dc) (map atomType args)+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/Translation/Haskell.hs view
@@ -1,5 +1,4 @@ -- | Haskell Translation---   Extracts SSTG from Haskell source. module SSTG.Core.Translation.Haskell     ( mkCompileClosure     , mkTargetBindings@@ -30,15 +29,15 @@  import qualified Data.Maybe  as MB --- | Make IO String from Outputable+-- | Make IO String from Outputable. mkIOStr :: (Outputable a) => a -> IO String mkIOStr obj = runGhc (Just libdir) $ do     dflags <- getSessionDynFlags     let ppr_str = showPpr dflags obj     return ppr_str --- | Make Target Bindings---   Given project directory and source target, make binds, with dependencies.+-- | Given the project directory and the source file path, compiles the+-- `ModuleGraph` and translates it into a SSTG `Binding`s. mkTargetBindings :: FilePath -> FilePath -> IO [SL.Binding] mkTargetBindings proj src = do     (sums_gutss, dflags, env) <- mkCompileClosure proj src@@ -55,11 +54,10 @@     let sl_bnds = map mkBinding (concat s_bndss)     return sl_bnds --- | Make Compilation Closure---   Captures a snapshot of the DynFlags and HscEnv in addition to---   the ModGuts in the ModuleGraph. This allows compilation to be, intheory,---   more portable across different applications, since ModGuts is a crucial---   intermediary for compilation in general.+-- | Captures a snapshot of the `DynFlags` and `HscEnv` in addition to the+-- `ModGuts` in the `ModuleGraph`. This allows compilation to be, in theory,+-- more portable across different applications, since `ModGuts` is a crucial+-- intermediary for compilation in general. mkCompileClosure :: FilePath -> FilePath ->                     IO ([(ModSummary, ModGuts)], DynFlags, HscEnv) mkCompileClosure proj src = runGhc (Just libdir) $ do@@ -79,12 +77,12 @@     let zipd   = (zip mod_graph m_gtss, dflags, env)     return zipd --- | Make SSTG Expr+-- | Make SSTG `Expr`. mkExpr :: StgExpr -> SL.Expr mkExpr (StgLit lit) = SL.Atom (SL.LitAtom (mkLit lit))-mkExpr (StgApp occ args)    = SL.FunApp (mkVar occ) (map mkArg args)-mkExpr (StgConApp dc args)  = SL.ConApp (mkData dc) (map mkArg args)-mkExpr (StgOpApp op args _) = SL.PrimApp (mkPrimOp op) (map mkArg args)+mkExpr (StgApp occ args)    = SL.FunApp (mkVar occ) (map mkAtom args)+mkExpr (StgConApp dc args)  = SL.ConApp (mkData dc) (map mkAtom args)+mkExpr (StgOpApp op args _) = SL.PrimApp (mkPrimOp op) (map mkAtom args) mkExpr (StgTick _ expr)     = mkExpr expr mkExpr (StgLam _ _)         = error "mkExpr: StgLam detected" mkExpr (StgLet bnd expr)    = SL.Let (mkBinding bnd) (mkExpr expr)@@ -92,12 +90,12 @@ mkExpr (StgCase mexpr _ _ bndr _ _ alts) =     SL.Case (mkExpr mexpr) (mkVar bndr) (map mkAlt alts) --- | Make SSTG Arg-mkArg :: StgArg -> SL.Atom-mkArg (StgVarArg occ) = SL.VarAtom (mkVar occ)-mkArg (StgLitArg lit) = SL.LitAtom (mkLit lit)+-- | Make SSTG `Atom`.+mkAtom :: StgArg -> SL.Atom+mkAtom (StgVarArg occ) = SL.VarAtom (mkVar occ)+mkAtom (StgLitArg lit) = SL.LitAtom (mkLit lit) --- | Make SSTG Name+-- | Make SSTG `Name`. mkName :: Name -> SL.Name mkName name = SL.Name occ mdl ns unq   where occ = (occNameString . nameOccName) name@@ -107,7 +105,7 @@             Nothing -> Nothing             Just md -> Just ((moduleNameString . moduleName) md) --- | Make SSTG NameSpace+-- | Make SSTG `NameSpace`. mkNameSpace :: NameSpace -> SL.NameSpace mkNameSpace ns | isVarNameSpace ns     = SL.VarNSpace                | isTvNameSpace  ns     = SL.TvNSpace@@ -127,13 +125,13 @@ mkBinding (StgRec bnd) = SL.Binding SL.Rec                                     (map (\(b, r) -> (mkVar b, mkRhs r)) bnd) --- | Make SSTG Rhs+-- | Make SSTG `BindRhs`. mkRhs :: StgRhs -> SL.BindRhs-mkRhs (StgRhsCon _ dc args) = SL.ConForm (mkData dc) (map mkArg args)+mkRhs (StgRhsCon _ dc args) = SL.ConForm (mkData dc) (map mkAtom args) mkRhs (StgRhsClosure _ _ _ _ _ params expr) =     SL.FunForm (map mkVar params) (mkExpr expr) --- | Make SSTG Lit+-- | Make SSTG `Lit`. mkLit :: Literal -> SL.Lit mkLit lit = case lit of   (MachChar chr)    -> SL.MachChar chr ((mkType . literalType) lit)@@ -148,20 +146,20 @@   MachNullAddr      -> SL.MachNullAddr ((mkType . literalType) lit)   (MachLabel f m _) -> SL.MachLabel (unpackFS f) m ((mkType . literalType) lit) --- | Make SSTG Data Constructor ID+-- | Make SSTG `ConTag`. mkDataTag :: DataCon -> SL.ConTag mkDataTag datacon = SL.ConTag name tag   where name = (mkName . dataConName) datacon         tag  = dataConTag datacon --- | Make SSTG Data Constructor+-- | Make SSTG `DataCon`. mkData :: DataCon -> SL.DataCon mkData datacon = SL.DataCon dcid ty args   where dcid = mkDataTag datacon         ty   = (mkType . dataConRepType) datacon         args = map mkType (dataConOrigArgTys datacon) --- | Make SSTG Primitive Operation+-- | Make SSTG `PrimFun`. mkPrimOp :: StgOp -> SL.PrimFun mkPrimOp (StgPrimOp op) = SL.PrimFun (SL.Name occ Nothing ns unq) ty   where occname = primOpOcc op@@ -171,17 +169,17 @@         ty      = (mkType . primOpType) op mkPrimOp _              = error "mkPrimOp: got StgPrimCallOp or StgFCallOp" --- | Make SSTG Alt+-- | Make SSTG `Alt`. mkAlt :: StgAlt -> SL.Alt mkAlt (a, b, _, e) = SL.Alt (mkAltCon a) (map mkVar b) (mkExpr e) --- | Make SSTG Alt Constructor+-- | Make SSTG `AltCon`. mkAltCon :: AltCon -> SL.AltCon mkAltCon (DataAlt dc) = SL.DataAlt (mkData dc) mkAltCon (LitAlt lit) = SL.LitAlt  (mkLit lit) mkAltCon (DEFAULT)    = SL.Default --- | Make SSTG Type+-- | Make SSTG `Type`. mkType :: Type -> SL.Type mkType (TyVarTy v) = SL.TyVarTy (mkName (V.varName v)) (mkType (varType v)) mkType (AppTy t1 t2)    = SL.AppTy (mkType t1) (mkType t2)@@ -191,7 +189,7 @@ mkType (CastTy ty cor)  = SL.CastTy (mkType ty) (mkCoercion cor) mkType (CoercionTy cor) = SL.CoercionTy (mkCoercion cor) --- | Make SSTG Type Constructor+-- | Make SSTG `TyCon`. mkTyCon :: TyCon -> SL.TyCon mkTyCon tc | isFunTyCon         tc = SL.FunTyCon     name            | isAlgTyCon         tc = SL.AlgTyCon     name algrhs@@ -205,25 +203,25 @@         algrhs = (mkAlgTyConRhs . algTyConRhs) tc         dcon   = (mkData . MB.fromJust . isPromotedDataCon_maybe) tc --- | Make SSTG Algebraic Type Constructor RHS+-- | Make SSTG `AlgTyRhs`. mkAlgTyConRhs :: AlgTyConRhs -> SL.AlgTyRhs mkAlgTyConRhs (AbstractTyCon b) = SL.AbstractTyCon b mkAlgTyConRhs (DataTyCon {data_cons = dcs}) = SL.DataTyCon  (map mkDataTag dcs) mkAlgTyConRhs (TupleTyCon {data_con = dc})  = SL.TupleTyCon (mkDataTag dc) mkAlgTyConRhs (NewTyCon {data_con = dc})    = SL.NewTyCon   (mkDataTag dc) --- | make SSTG Type Binder+-- | make SSTG `TyBinder`. mkTyBndr :: TyBinder -> SL.TyBinder mkTyBndr (Anon ty)   = SL.AnonTyBndr  (mkType ty) mkTyBndr (Named v _) = SL.NamedTyBndr (mkName (V.varName v))                                       (mkType (varType v)) --- | Make SSTG Type Literal+-- | Make SSTG `Type` literals. mkTyLit :: TyLit -> SL.TyLit mkTyLit (NumTyLit i)  = SL.NumTyLit (fromInteger i) mkTyLit (StrTyLit fs) = SL.StrTyLit (unpackFS fs) --- | Make SSTG Coercion+-- | Make SSTG `Coercion`. mkCoercion :: Coercion -> SL.Coercion mkCoercion coer = SL.Coercion (mkType a) (mkType b)   where (a, b) = (unPair . coercionKind) coer
src/SSTG/Utils/FileIO.hs view
@@ -11,12 +11,16 @@  import Text.Read +-- | Write `State` to a target file. writeState :: FilePath -> State -> IO () writeState file state = writeFile file (show state) +-- | Recover a `State` from a stored file. `Nothing` denotes failure. readState :: FilePath -> IO (Maybe State) readState file = readFile file >>= \s -> return (readMaybe s :: Maybe State) +-- | Write a pretty-printed state to a file. Do not use this for execution+-- `State` recovery; use `writeState` instead. writePrettyState :: FilePath -> ([LiveState], [DeadState]) -> IO () writePrettyState file lds = writeFile file (pprLivesDeadsStr lds)
src/SSTG/Utils/Printing.hs view
@@ -1,3 +1,4 @@+-- | Pretty Printing module SSTG.Utils.Printing     ( pprStateStr     , pprLivesDeadsStr@@ -9,6 +10,7 @@ import qualified Data.Map  as M import qualified Data.List as L +-- | Print `LiveState` and `DeadState` that yield from execution snapshots. pprLivesDeadsStr :: ([LiveState], [DeadState]) -> String pprLivesDeadsStr (lives, deads) = injNewLineSeps10 acc_strs   where header   = "(Lives, Deads)"@@ -16,6 +18,7 @@         dd_str   = (injNewLineSeps5 . map pprDeadStr) deads         acc_strs = [header, lv_str, dd_str] +-- | Print `LiveState`. pprLiveStr :: LiveState -> String pprLiveStr (rules, state) = injNewLine acc_strs   where header   = "Live"@@ -23,6 +26,7 @@         st_str   = pprStateStr state         acc_strs = [header, rule_str, st_str] +-- | Print `DeadState`. pprDeadStr :: LiveState -> String pprDeadStr (rules, state) = injNewLine acc_strs   where header   = "Dead"@@ -30,13 +34,14 @@         st_str   = pprStateStr state         acc_strs = [header, rule_str, st_str] +-- | Print `Rule`. pprRuleStr :: Rule -> String pprRuleStr rule = show rule  pprRulesStr :: [Rule] -> String pprRulesStr rules = injIntoList (map pprRuleStr rules) --- | Make String from State+-- | Print `State`. pprStateStr :: State -> String pprStateStr state   = injNewLine acc_strs   where status_str  = (pprStatusStr   . state_status)  state@@ -65,52 +70,59 @@                       , links_str                       , "<<<<<<<<<<<<<<<<<<<<<<<<<<<<<" ] --- | Sub Member String Wrapping+-- | Inject `String` into parantheses. sub :: String -> String sub str = "(" ++ str ++ ")" --- | Inject with " "+-- | Inject a list of `String`s with space. injSpace :: [String] -> String injSpace strs = L.intercalate " " strs --- | Inject with ","+-- | Inject a list of `String`s with commas. injComma :: [String] -> String injComma strs = L.intercalate "," strs --- | Inject New Line+-- | Inject a list of `String`s with newlines. injNewLine :: [String] -> String injNewLine strs = L.intercalate "\n" strs --- | Inj into List+-- | Inject a list of `String`s into a single string with commas and brackets. injIntoList :: [String] -> String injIntoList strs = "[" ++ (injComma strs) ++ "]" --- | In Newline Separators+-- | Inject a list of `String`s with newline separators of dashes length 5. injNewLineSeps5 :: [String] -> String injNewLineSeps5 strs = L.intercalate seps strs   where seps = "\n-----\n" +-- | Inject a list of `String`s wit hnewline separators of dashes length 10. injNewLineSeps10 :: [String] -> String injNewLineSeps10 strs = L.intercalate seps strs   where seps = "\n----------\n" +-- | Print `MemAddr`. pprMemAddrStr :: MemAddr -> String pprMemAddrStr (MemAddr int) = show int +-- | Print `Name`. pprNameStr :: Name -> String pprNameStr name = show name +-- | Print `Lit`. pprLitStr :: Lit -> String pprLitStr lit = show lit +-- | Print `Status`. pprStatusStr :: Status -> String pprStatusStr status = show status +-- | Print `Stack`. pprStackStr :: Stack -> String pprStackStr (Stack stack) = injNewLineSeps10 acc_strs   where frame_strs = map pprFrameStr stack         acc_strs   = "Stack" : frame_strs +-- | Print `Frame`. pprFrameStr :: Frame -> String pprFrameStr (CaseFrame var alts locals) = injNewLine acc_strs   where header   = "CaseFrame"@@ -128,6 +140,7 @@         addr_str = pprMemAddrStr addr         acc_strs = [header, addr_str] +-- | Print the @Maybe (Expr, Locals)@. pprSymClosureStr :: Maybe (Expr, Locals) -> String pprSymClosureStr (Nothing)             = "SymClosure ()" pprSymClosureStr (Just (expr, locals)) = injSpace acc_strs@@ -136,6 +149,7 @@         locs_str = pprLocalsStr locals         acc_strs = [header, injIntoList [expr_str, locs_str]] +-- | Print `HeapObj`. pprHeapObjStr :: HeapObj -> String pprHeapObjStr (Blackhole) = "Blackhole!!!" pprHeapObjStr (LitObj lit) = injSpace acc_strs@@ -159,6 +173,7 @@         locs_str = pprLocalsStr locals         acc_strs = [header, prms_str, expr_str, locs_str] +-- | Print `Heap`. pprHeapStr :: Heap -> String pprHeapStr (Heap hmap addr) = injNewLine (map (\k -> ">" ++ k) acc_strs)   where kvs  = M.toList hmap@@ -169,6 +184,7 @@         kvs_strs  = map (\(m, o) -> sub (m ++ "," ++ o)) zipd_strs         acc_strs  = addr_str : kvs_strs +-- | Print `Globals`. pprGlobalsStr :: Globals -> String pprGlobalsStr (Globals gmap) = injNewLine (map (\k -> ">" ++ k) acc_strs)   where kvs  = M.toList gmap@@ -177,6 +193,7 @@         zipd_strs = zip name_strs val_strs         acc_strs  = map (\(n, v) -> sub (n ++ "," ++ v)) zipd_strs +-- | Print `Locals`. pprLocalsStr :: Locals -> String pprLocalsStr (Locals lmap) = injIntoList acc_strs   where kvs  = M.toList lmap@@ -185,6 +202,7 @@         zipd_strs = zip name_strs val_strs         acc_strs  = map (\(n, v) -> sub (n ++ "," ++ v)) zipd_strs +-- | Print `Value`. pprValueStr :: Value -> String pprValueStr (LitVal lit) = injSpace acc_strs   where header   = "LitVal"@@ -195,6 +213,7 @@         ptr_str  = pprMemAddrStr addr         acc_strs = [header, ptr_str] +-- | Print `Var`. pprVarStr :: Var -> String pprVarStr (Var name ty) = injSpace acc_strs   where header   = "Var"@@ -202,6 +221,7 @@         type_str = (sub . pprTypeStr) ty         acc_strs = [header, name_str, type_str] +-- | Print `Atom`. pprAtomStr :: Atom -> String pprAtomStr (VarAtom var) = injSpace acc_strs   where header   = "VarAtom"@@ -212,9 +232,11 @@         lit_str  = (sub . pprLitStr) lit         acc_strs = [header, lit_str] +-- | Print `ConTag`. pprConTagStr :: ConTag -> String pprConTagStr (ConTag name _) = pprNameStr name +-- | Print `DataCon`. pprDataConStr :: DataCon -> String pprDataConStr (DataCon tag ty tys) = injSpace acc_strs   where header   = "DataCon"@@ -223,6 +245,7 @@         tys_str  = injIntoList (map pprTypeStr tys)         acc_strs = [header, tag_str, ty_str, tys_str] +-- | Print `PrimFun`. pprPrimFunStr :: PrimFun -> String pprPrimFunStr (PrimFun name ty) = injSpace acc_strs   where header   = "PrimFun"@@ -230,6 +253,7 @@         type_str = (sub . pprTypeStr) ty         acc_strs = [header, name_str, type_str] +-- | Print `AltCon`. pprAltConStr :: AltCon -> String pprAltConStr (DataAlt dcon) = injSpace acc_strs   where header   = "DataAlt"@@ -241,6 +265,7 @@         acc_strs = [header, lit_str] pprAltConStr (Default) = "Default" +-- | Print `Alt`. pprAltStr :: Alt -> String pprAltStr (Alt acon var expr) = injSpace acc_strs   where header   = "Alt"@@ -249,9 +274,11 @@         expr_str = (sub . pprExprStr) expr         acc_strs = [header, acon_str, vars_str, expr_str] +-- | Print a list of `Alt`s. pprAltsStr :: [Alt] -> String pprAltsStr alts = injIntoList (map pprAltStr alts) +-- | Print `BindRhs`. pprBindRhsStr :: BindRhs -> String pprBindRhsStr (FunForm params expr) = injSpace acc_strs   where header   = "FunForm"@@ -264,18 +291,21 @@         args_str = injIntoList (map pprAtomStr args)         acc_strs = [header, dcon_str, args_str] -bindStr :: (Var, BindRhs) -> String-bindStr (var, lamf) = (sub . injComma) acc_strs+-- | Print @(Var, BindRhs)@.+pprBindStr :: (Var, BindRhs) -> String+pprBindStr (var, lamf) = (sub . injComma) acc_strs   where var_str  = pprVarStr var         lamf_str = pprBindRhsStr lamf         acc_strs = [var_str, lamf_str] +-- | Print `Binding`. 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)+        bnds_str = injIntoList (map pprBindStr bnd)         acc_strs = [header, bnds_str] +-- | Print `Expr`. pprExprStr :: Expr -> String pprExprStr (Atom atom) = injSpace acc_strs   where header   = "Atom"@@ -308,10 +338,12 @@         expr_str = (sub . pprExprStr) expr         acc_strs = [header, bnd_str, expr_str] +-- | Print `Type`. NOTE: currently only prints @"__TyPE__"@ because there is+-- a lot of `Type` information which makes analysis of dumps hard otherwise. pprTypeStr :: Type -> String pprTypeStr ty = fst ("__Type__", ty) --- | State Code String+-- | Print `Code`. pprCodeStr :: Code -> String pprCodeStr (Evaluate expr locals) = injSpace acc_strs   where header   = "Evaluate"@@ -323,16 +355,16 @@         val_str  = pprValueStr val         acc_strs = [header, val_str] --- | All Names String+-- | Print a list of `Name`s. pprNamesStr :: [Name] -> String pprNamesStr names = injIntoList (map pprNameStr names) --- | Path Constraints String+-- | Print `PathCons`. pprPConsStr :: PathCons -> String pprPConsStr pathcons = injNewLineSeps5 strs   where strs = map pprPCondStr pathcons --- | Path Condition String+-- | Print `PathCond`. pprPCondStr :: PathCond -> String pprPCondStr (PathCond (acon, params) expr locals hold) = injIntoList acc_strs   where acon_str = pprAltConStr acon@@ -342,10 +374,9 @@         hold_str = case hold of { True -> "Positive"; False -> "Negative" }         acc_strs = [acon_str, prms_str, expr_str, locs_str, hold_str] --- | Symbolic Links String+-- | Print `SymLinks`. pprLinksStr :: SymLinks -> String pprLinksStr (SymLinks links) = injNewLineSeps5 acc_strs   where kvs      = M.toList links         acc_strs = map (\(k, v) -> pprNameStr k ++ " -> " ++ pprNameStr v) kvs-