SSTG 0.1.1.3 → 0.1.1.4

raw patch · 14 files changed

+583/−625 lines, 14 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• SSTG.cabal +2/−2
• app/Main.hs +19/−19
• src/SSTG/Core/Execution.hs +2/−0
• src/SSTG/Core/Execution/Engine.hs +50/−48
• src/SSTG/Core/Execution/Rules.hs +29/−27
• src/SSTG/Core/Execution/Stepping.hs +3/−3
• src/SSTG/Core/Execution/Support.hs +340/−0
• src/SSTG/Core/Language.hs +0/−2
• src/SSTG/Core/Language/Naming.hs +60/−106
• src/SSTG/Core/Language/Support.hs +0/−351
• src/SSTG/Core/Language/Syntax.hs +10/−11
• src/SSTG/Core/Language/Typing.hs +7/−8
• src/SSTG/Core/Translation/Haskell.hs +18/−17
• src/SSTG/Utils/Printing.hs +43/−31

@@ -1,5 +1,5 @@ name:                SSTG-version:             0.1.1.3+version:             0.1.1.4 synopsis:            STG Symbolic Execution description:         Prototype of STG-based Symbolic Execution for Haskell. homepage:            https://github.com/AntonXue/SSTG#readme@@ -19,7 +19,6 @@                      , SSTG.Core                      , SSTG.Core.Language                      , SSTG.Core.Language.Naming-                     , SSTG.Core.Language.Support                      , SSTG.Core.Language.Syntax                      , SSTG.Core.Language.Typing                      , SSTG.Core.Preprocessing@@ -32,6 +31,7 @@                      , SSTG.Core.Execution.Engine                      , SSTG.Core.Execution.Rules                      , SSTG.Core.Execution.Stepping+                     , SSTG.Core.Execution.Support                      , SSTG.Utils                      , SSTG.Utils.Printing                      , SSTG.Utils.FileIO

@@ -4,7 +4,7 @@  import qualified Data.Char as C import qualified Data.List as L-import qualified Data.Map  as M+import qualified Data.Map as M  import System.Environment import Text.Read@@ -14,17 +14,17 @@  trimSlash :: String -> String trimSlash str = case trim str of-    ""      -> ""+    "" -> ""     trimmed -> case last trimmed of          '/' -> trimSlash (init trimmed)-        _   -> trimmed+        _ -> trimmed  matchArg :: String -> [String] -> (String -> a) -> a -> a matchArg tgt args fun def = case L.elemIndex tgt args of+    Just i -> if i >= length args+                  then error ("Invalid use of " ++ tgt)+                  else fun (args !! (i + 1))  -- fun (args !! (i + 1))     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@@ -32,22 +32,22 @@ 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)+        types = M.fromList [ ("bfs", BFS)                            , ("bfs-log", BFSLogged)-                           , ("dfs",     DFS)+                           , ("dfs", DFS)                            , ("dfs-log", DFSLogged) ]  parseDumpDir :: [String] -> Maybe FilePath parseDumpDir args = case matchArg "--dump" args (readMaybe . show) Nothing of-    Nothing  -> Nothing     Just raw -> case trimSlash raw of                     "" -> error ("Invalid use of " ++ raw)                     ok -> Just ok+    Nothing -> Nothing  parseFlags :: [String] -> RunFlags parseFlags args = RunFlags { flag_step_count = parseStepCount args-                           , flag_step_type  = parseStepType  args-                           , flag_dump_dir   = parseDumpDir   args }+                           , flag_step_type = parseStepType args+                           , flag_dump_dir = parseDumpDir args }  injDumpLocs :: String -> Int -> FilePath -> [FilePath] injDumpLocs entry n dir = map (\i -> start ++ (show i) ++ ".txt") [1..n]@@ -58,31 +58,31 @@     -- Get command line arguments.     (proj:src:tail_args) <- getArgs     -- Make bindings.-    binds <- mkTargetBinds proj src+    bindss <- mkTargetBindsList 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)+    let load_result = loadStateEntry entry (Program bindss)+    putStrLn $ "binds: " ++ show (length bindss)     -- Get the state from the loader.     state <- case load_result of-                 LoadError str         -> error str-                 LoadOkay state        -> return state+                 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+    let ldss = execute flags state     case flag_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)+        -- Dump to terminal.+        Nothing -> mapM_ (putStrLn . pprLivesDeadsStr) ldss 

@@ -3,9 +3,11 @@     ( module SSTG.Core.Execution.Engine     , module SSTG.Core.Execution.Rules     , module SSTG.Core.Execution.Stepping+    , module SSTG.Core.Execution.Support     ) where  import SSTG.Core.Execution.Engine import SSTG.Core.Execution.Rules import SSTG.Core.Execution.Stepping+import SSTG.Core.Execution.Support 

@@ -10,11 +10,13 @@     ) where  import SSTG.Core.Language+ import SSTG.Core.Execution.Stepping+import SSTG.Core.Execution.Support  -- | Load Result data LoadResult = LoadOkay State-                | LoadGuess State [Bind]+                | LoadGuess State [Binds]                 | LoadError String                 deriving (Show, Eq, Read) @@ -27,7 +29,7 @@  -- | Load from a specified entry point. loadStateEntry :: String -> Program -> LoadResult-loadStateEntry entry (Program bnds) = if length matches == 0+loadStateEntry entry (Program bindss) = if length matches == 0     then LoadError ("No entry candidates found for: [" ++ entry ++ "]")     else if length others == 0         then LoadOkay state@@ -39,14 +41,14 @@     stack = empty_stack     -- Globals and Heap are loaded together. They are still beta forms now.     heap0 = empty_heap-    (glist, heap1, bnd_addrss) = initGlobals bnds heap0+    (glist, heap1, binds_addrss) = initGlobals bindss heap0     globals0 = insertGlobalsList glist empty_globals-    (heap2, localss) = liftBinds bnd_addrss globals0 heap1-    bnd_locs = zip bnds localss+    (heap2, localss) = liftBindsList binds_addrss globals0 heap1+    binds_locs = zip bindss localss     -- Code loading. Completes heap and globals with symbolic injection.-    matches = entryMatches entry bnd_locs-    ((tgt_bnd, tgt_loc):others) = matches-    ((tgt_var, tgt_rhs):_) = lhsMatches entry tgt_bnd+    matches = entryMatches entry binds_locs+    ((tgt_binds, tgt_loc):others) = matches+    ((tgt_var, tgt_rhs):_) = lhsMatches entry tgt_binds     (code, globals, heap) = loadCode tgt_var tgt_rhs tgt_loc globals0 heap2     -- Ready to fill the state.     state0 = State { state_status = status@@ -58,44 +60,44 @@                    , state_paths = empty_pathcons }      -- Gather information on all variables.-    state = state0 { state_names = allNames state0 }+    state = state0 { state_names = allNames (Program bindss) } --- | Allocate Bind-allocBind :: Bind -> Heap -> (Heap, [MemAddr])-allocBind (Bind _ pairs) heap = (heap', addrs)+-- | Allocate Binds+allocBinds :: Binds -> Heap -> (Heap, [MemAddr])+allocBinds (Binds _ kvs) heap = (heap', addrs)   where-    hfakes = map (const Blackhole) pairs+    hfakes = map (const Blackhole) kvs     (heap', addrs) = allocHeapList hfakes heap --- | Allocate List of `Bind`s-allocBindList :: [Bind] -> Heap -> (Heap, [[MemAddr]])-allocBindList [] heap = (heap, [])-allocBindList (b:bs) heap = (heapf, addrs : as)+-- | Allocate List of `Binds`s+allocBindsList :: [Binds] -> Heap -> (Heap, [[MemAddr]])+allocBindsList [] heap = (heap, [])+allocBindsList (b:bs) heap = (heapf, addrs : as)   where-    (heap', addrs) = allocBind b heap-    (heapf, as) = allocBindList bs heap'+    (heap', addrs) = allocBinds b heap+    (heapf, as) = allocBindsList bs heap' --- | Bind Address to Name Values-bndAddrsToVarVals :: (Bind, [MemAddr]) -> [(Var, Value)]-bndAddrsToVarVals (Bind _ rhss, addrs) = zip (map fst rhss) mem_vals+-- | Binds Address to Name Values+bindsAddrsToVarVals :: (Binds, [MemAddr]) -> [(Var, Value)]+bindsAddrsToVarVals (Binds _ kvs, addrs) = zip (map fst kvs) mem_vals   where     mem_vals = map (\a -> MemVal a) addrs  -- | Initialize Globals-initGlobals :: [Bind] -> Heap -> ([(Var, Value)], Heap, [(Bind, [MemAddr])])-initGlobals bnds heap = (var_vals, heap', bnd_addrss)+initGlobals :: [Binds] -> Heap -> ([(Var, Value)], Heap, [(Binds, [MemAddr])])+initGlobals bindss heap = (var_vals, heap', binds_addrss)   where-    (heap', addrss) = allocBindList bnds heap-    bnd_addrss = zip bnds addrss-    var_vals = concatMap bndAddrsToVarVals bnd_addrss+    (heap', addrss) = allocBindsList bindss heap+    binds_addrss = zip bindss addrss+    var_vals = concatMap bindsAddrsToVarVals binds_addrss  -- | Force Atom Lookup forceLookupValue :: Atom -> Locals -> Globals -> Value forceLookupValue (LitAtom lit) _ _ = LitVal lit forceLookupValue (VarAtom var) locals globals =     case lookupValue var locals globals of-        Nothing -> LitVal BlankAddr  -- An error, but I want to not crash.         Just val -> val+        Nothing -> LitVal BlankAddr  -- An error, but I want to not crash.  -- | Full Rhs Object forceRhsObj :: BindRhs -> Locals -> Globals -> HeapObj@@ -104,38 +106,38 @@   where     arg_vals = map (\a -> forceLookupValue a locals globals) args --- | Lift `Bind`.-liftBind :: (Bind, [MemAddr]) -> Globals -> Heap -> (Heap, Locals)-liftBind (Bind rec pairs, addrs) globals heap = (heap', locals)+-- | Lift `Binds`.+liftBinds :: (Binds, [MemAddr]) -> Globals -> Heap -> (Heap, Locals)+liftBinds (Binds rec kvs, addrs) globals heap = (heap', locals)   where-    (vars, rhss) = unzip pairs+    (vars, rhss) = unzip kvs     mem_vals = map (\a -> MemVal a) addrs     e_locs = empty_locals     r_locs = insertLocalsList (zip vars mem_vals) e_locs     locals = case rec of { Rec -> r_locs; NonRec -> e_locs }     hobjs = map (\r -> forceRhsObj r locals globals) rhss-    heap' = insertHeapList (zip addrs hobjs) heap+    heap' = insertHeapObjList (zip addrs hobjs) heap --- | Lift Bind List-liftBinds :: [(Bind, [MemAddr])] -> Globals -> Heap -> (Heap, [Locals])-liftBinds [] _ heap = (heap, [])-liftBinds (bm:bms) globals heap = (heapf, locals : ls)+-- | Lift Binds List+liftBindsList :: [(Binds, [MemAddr])] -> Globals -> Heap -> (Heap, [Locals])+liftBindsList [] _ heap = (heap, [])+liftBindsList (bm:bms) globals heap = (heapf, locals : ls)   where-    (heap', locals) = liftBind bm globals heap-    (heapf, ls) = liftBinds bms globals heap'+    (heap', locals) = liftBinds bm globals heap+    (heapf, ls) = liftBindsList bms globals heap'  -- | Return a sub-list of binds in which the entry candidate appears.-entryMatches :: String -> [(Bind, Locals)] -> [(Bind, Locals)]-entryMatches entry bnd_locs = filter (bindFilter entry) bnd_locs+entryMatches :: String -> [(Binds, Locals)] -> [(Binds, Locals)]+entryMatches entry binds_locs = filter (isEntryBinds entry) binds_locs --- | Bind Filtering-bindFilter :: String -> (Bind, Locals) -> Bool-bindFilter entry (bnd, _) = lhsMatches entry bnd /= []+-- | Binds Filtering+isEntryBinds :: String -> (Binds, Locals) -> Bool+isEntryBinds entry (binds, _) = lhsMatches entry binds /= [] --- | Sub-Binds String Match-lhsMatches :: String -> Bind -> [(Var, BindRhs)]-lhsMatches st (Bind _ pairs) =-    filter (\(var, _) -> st == (nameOccStr . varName) var) pairs+-- | Sub-Bindss String Match+lhsMatches :: String -> Binds -> [(Var, BindRhs)]+lhsMatches st (Binds _ kvs) =+    filter (\(var, _) -> st == (nameOccStr . varName) var) kvs  -- | Load Code loadCode :: Var -> BindRhs -> Locals -> Globals -> Heap -> (Code,Globals,Heap)

@@ -7,6 +7,8 @@  import SSTG.Core.Language +import SSTG.Core.Execution.Support+ -- | `Rule`s that are applied during STG reduction. data Rule = RuleAtomLit | RuleAtomLitPtr | RuleAtomValPtr | RuleAtomUnInt           | RulePrimApp@@ -66,7 +68,7 @@ -- | `Value` to `Lit`. valueToLit :: Value -> Lit valueToLit (LitVal lit) = lit-valueToLit (MemVal addr) = AddrLit (addrInt addr)+valueToLit (MemVal addr) = AddrLit (memAddrInt addr)  -- | Uneven `zip` of two `List`s, with the leftover stored. unevenZip :: [a] -> [b] -> ([(a, b)], Either [a] [b])@@ -140,26 +142,26 @@     LiftAct hobj locals' globals' heap' confs' = liftBindRhs pass_in     LiftAct hos localsf globalsf heapf confsf = liftBindRhsList pass_rest --- | Lift `Bind`.-liftBind :: LiftAct Bind -> LiftAct ()-liftBind (LiftAct (Bind NonRec bnd) locals globals heap confs) = pass_out+-- | Lift `Binds`.+liftBinds :: LiftAct Binds -> LiftAct ()+liftBinds (LiftAct (Binds NonRec kvs) locals globals heap confs) = pass_out   where     (heapf, addrs) = allocHeapList hobjs heap'     mem_vals = map MemVal addrs-    localsf = insertLocalsList (zip (map fst bnd) mem_vals) locals'-    pass_in = LiftAct (map snd bnd) locals globals heap confs+    localsf = insertLocalsList (zip (map fst kvs) mem_vals) locals'+    pass_in = LiftAct (map snd kvs) locals globals heap confs     pass_out = LiftAct () localsf globals' heapf confs'     LiftAct hobjs locals' globals' heap' confs' = liftBindRhsList pass_in-liftBind (LiftAct (Bind Rec bnd) locals globals heap confs) = pass_out+liftBinds (LiftAct (Binds Rec kvs) locals globals heap confs) = pass_out   where-    hfakes = map (const Blackhole) bnd+    hfakes = map (const Blackhole) kvs     -- Allocate dummy BLACKHOLEs     (heap', addrs) = allocHeapList hfakes heap     mem_vals = map MemVal addrs     -- Use the reigstered loca BLACKHOLEs to construct the locals closure.-    locals' = insertLocalsList (zip (map fst bnd) mem_vals) locals-    heapf = insertHeapList (zip addrs hobjs) heap''-    pass_in = LiftAct (map snd bnd) locals' globals heap' confs+    locals' = insertLocalsList (zip (map fst kvs) mem_vals) locals+    heapf = insertHeapObjList (zip addrs hobjs) heap''+    pass_in = LiftAct (map snd kvs) locals' globals heap' confs     pass_out = LiftAct () localsf globals' heapf confs'     LiftAct hobjs localsf globals' heap'' confs' = liftBindRhsList pass_in @@ -195,8 +197,8 @@     mem_vals = map MemVal addrs     kvs = (cvar, MemVal addr) : zip params mem_vals     locals' = insertLocalsList kvs locals-    mxpr = Atom (VarAtom mvar)-    conss = [Constraint (ac, params) mxpr locals' True]+    mexpr = Atom (VarAtom mvar)+    conss = [Constraint (ac, params) mexpr locals' True]     confs' = snames ++ confs     pass_out = LiftAct (expr, conss) locals' globals heap' confs' @@ -257,7 +259,7 @@   | Evaluate (PrimApp pfun args) locals <- code =     let pass_in = LiftAct args locals globals heap confs         LiftAct vals locals' globals' heap' confs' = liftAtomList pass_in-        eval = SymLitEval pfun (map valueToLit vals)+        eval = LitEval pfun (map valueToLit vals)     in Just (RulePrimApp             ,[state { state_heap = heap'                     , state_globals = globals'@@ -338,9 +340,9 @@                     , state_names = confs' }])    -- Rule Let-  | Evaluate (Let bnd expr) locals <- code =-    let pass_in = LiftAct bnd locals globals heap confs-        LiftAct _ locals' globals' heap' confs' = liftBind pass_in+  | Evaluate (Let binds expr) locals <- code =+    let pass_in = LiftAct binds locals globals heap confs+        LiftAct _ locals' globals' heap' confs' = liftBinds pass_in     in Just (RuleLet             ,[state { state_heap = heap'                     , state_globals = globals'@@ -414,7 +416,7 @@     let frame = UpdateFrame addr     in Just (RuleUpdateCThunk             ,[state { state_stack = pushStack frame stack-                    , state_heap = insertHeap (addr, Blackhole) heap+                    , state_heap = insertHeapObj (addr, Blackhole) heap                     , state_code = Evaluate expr fun_locs }])    -- Rule Update Frame Delete Lit@@ -422,7 +424,7 @@   , Return (LitVal lit) <- code =     Just (RuleUpdateDLit          ,[state { state_stack = stack'-                 , state_heap = insertHeap (frm_addr, LitObj lit) heap+                 , state_heap = insertHeapObj (frm_addr, LitObj lit) heap                  , state_code = Return (LitVal lit) }])    -- Rule Update Frame Delete Val Pointer@@ -432,24 +434,24 @@   , isHeapValueForm hobj =     Just (RuleUpdateDValPtr          ,[state { state_stack = stack'-                 , state_heap = insertHeap (frm_addr, AddrObj addr) heap+                 , state_heap = insertHeapRedir (frm_addr, addr) heap                  , state_code = Return (MemVal addr) }])    -- Rule Case Frame Create Case Non LitVal or MemVal-  | Evaluate (Case mxpr cvar alts) locals <- code-  , not (isExprValueForm mxpr locals globals heap) =+  | Evaluate (Case mexpr cvar alts) locals <- code+  , not (isExprValueForm mexpr locals globals heap) =     let frame = CaseFrame cvar alts locals     in Just (RuleCaseCCaseNonVal             ,[state { state_stack = pushStack frame stack-                    , state_code = Evaluate mxpr locals }])+                    , state_code = Evaluate mexpr locals }])      -- Rule Case Frame Delete Lit   | Just (CaseFrame cvar alts frm_locs, stack') <- popStack stack   , Return (LitVal lit) <- code =-    let mxpr = Atom (LitAtom lit)+    let cexpr = Case (Atom (LitAtom lit)) cvar alts     in Just (RuleCaseDLit             ,[state { state_stack = stack'-                    , state_code = Evaluate (Case mxpr cvar alts) frm_locs }])+                    , state_code = Evaluate cexpr frm_locs }])    -- Rule Case Frame Delete Heap Value   | Just (CaseFrame cvar alts frm_locs, stack') <- popStack stack@@ -458,11 +460,11 @@   , isHeapValueForm hobj =     let vname = freshSeededName (varName cvar) confs         vvar = Var vname (varType cvar)-        mxpr = Atom (VarAtom vvar)+        cexpr = Case (Atom (VarAtom vvar)) cvar alts         frm_locs' = insertLocals (vvar, MemVal addr) frm_locs     in Just (RuleCaseDValPtr             ,[state { state_stack = stack'-                    , state_code = Evaluate (Case mxpr cvar alts) frm_locs'+                    , state_code = Evaluate cexpr frm_locs'                     , state_names = vname : confs }])    -- Rule Apply Frame Create Function Thunk

@@ -8,8 +8,8 @@     , runBoundedDFSLogged     ) where -import SSTG.Core.Language import SSTG.Core.Execution.Rules+import SSTG.Core.Execution.Support  import qualified Data.Char as C import qualified Data.List as L@@ -37,20 +37,20 @@   where     status = state_status state     status' = case mb_id of+                  Just int -> incStatusSteps (updateStatusId int status)                   Nothing -> incStatusSteps status-                  Just id' -> incStatusSteps (updateStatusId id' status)  -- | 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, start) = case reduce start of-    Nothing -> [(hist, start)]     Just (rule, results) ->         let trace = hist ++ [rule]             mb_id = if length results > 1                         then Just (hash trace)                         else Nothing         in map (\s -> (trace, incStatus mb_id s)) results+    Nothing -> [(hist, start)]  -- | This is what we use the `<*>` over. pass :: [LiveState] -> ([LiveState], [DeadState] -> [DeadState])

@@ -0,0 +1,340 @@+-- | Symbolic STG Execution Support Architecture+module SSTG.Core.Execution.Support+    ( SymbolicT(..)+    , fmap+    , pure+    , (<*>)+    , return+    , (>>=)++    , State(..)+    , Symbol(..)+    , Status(..)+    , Stack+    , Frame(..)+    , MemAddr+    , Value(..)+    , Locals+    , Heap+    , HeapObj(..)+    , Globals+    , Code(..)+    , PathCons+    , Constraint(..)++    , null_addr+    , memAddrInt++    , init_status+    , incStatusSteps+    , updateStatusId++    , empty_stack+    , popStack+    , pushStack+    , stackToList++    , empty_locals+    , lookupLocals+    , insertLocals+    , insertLocalsList+    , localsToList++    , empty_heap+    , lookupHeap+    , insertHeapObj+    , insertHeapObjList+    , insertHeapRedir+    , allocHeap+    , allocHeapList+    , heapToList++    , empty_globals+    , lookupGlobals+    , insertGlobals+    , insertGlobalsList+    , globalsToList++    , empty_pathcons+    , insertPathCons+    , insertPathConsList+    , pathconsToList++    , lookupValue+    , vlookupHeap+    , memAddrType+    ) where++import SSTG.Core.Language++import qualified Data.Map as M++-- | 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.+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.+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.+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` 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+                   , state_globals :: !Globals+                   , state_code :: !Code+                   , state_names :: ![Name]+                   , state_paths :: !PathCons+                   } deriving (Show, Eq, Read)++-- | 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)++-- | State status.+data Status = Status { status_id :: !Int+                     , status_parent :: !Int+                     , status_steps :: !Int+                     } deriving (Show, Eq, Read)++-- | Execution stack used in graph reduction semnatics.+newtype Stack = Stack [Frame] deriving (Show, Eq, Read)++-- | Frames of a stack.+data Frame = CaseFrame Var [Alt] Locals+           | ApplyFrame [Atom] Locals+           | UpdateFrame MemAddr+           deriving (Show, Eq, Read)++-- | Memory address for things on the `Heap`.+newtype MemAddr = MemAddr Int deriving (Show, Eq, Read, Ord)++-- | 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 binds a `Var`'s `Name` to its some `Value`.+newtype Locals = Locals (M.Map Name Value) deriving (Show, Eq, Read)++-- | 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 (Either MemAddr HeapObj)) MemAddr+          deriving (Show, Eq, Read)++-- | Heap objects.+data HeapObj = LitObj Lit+             | SymObj Symbol+             | ConObj DataCon [Value]+             | FunObj [Var] Expr Locals+             | Blackhole+             deriving (Show, Eq, Read)++-- | 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 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 are the conjunctive normal form of `Constraint`s.+newtype PathCons = PathCons [Constraint] deriving (Show, Eq, Read)++-- | Constraints denote logical paths taken in program execution thus far.+data Constraint = Constraint (AltCon, [Var]) Expr Locals Bool+                deriving (Show, Eq, Read)++-- Simple functions that require only the immediate data structure.++-- | Null `MemAddr`.+null_addr :: MemAddr+null_addr = MemAddr 0++-- | `MemAddr`'s `Int` value.+memAddrInt :: MemAddr -> Int+memAddrInt (MemAddr int) = int++-- | Initial `Status`.+init_status :: Status+init_status = Status { status_id = 1+                     , status_parent = 0+                     , status_steps = 0 }++-- | Increment `Status` steps.+incStatusSteps :: Status -> Status+incStatusSteps status = status { status_steps = (status_steps status) + 1 }++-- | Update the `Status` id.+updateStatusId :: Int -> Status -> Status+updateStatusId int status = status { status_id = int+                                   , status_parent = status_id status }++-- | Empty `Stack.+empty_stack :: Stack+empty_stack = Stack []++-- | `Stack` pop.+popStack :: Stack -> Maybe (Frame, Stack)+popStack (Stack []) = Nothing+popStack (Stack (frame:frames)) = Just (frame, Stack frames)++-- | `Stack` push.+pushStack :: Frame -> Stack -> Stack+pushStack frame (Stack frames) = Stack (frame : frames)++-- | `Stack` as list of `Frame`s.+stackToList :: Stack -> [Frame]+stackToList (Stack frames) = frames++-- | Empty `Locals`.+empty_locals :: Locals+empty_locals = Locals M.empty++-- | `Locals` lookup.+lookupLocals :: Var -> Locals -> Maybe Value+lookupLocals var (Locals lmap) = M.lookup (varName var) lmap++-- | `Locals` insertion.+insertLocals :: (Var, Value) -> Locals -> Locals+insertLocals (k, v) (Locals lmap) = Locals (M.insert (varName k) v lmap)++-- | List insertion into `Locals`.+insertLocalsList :: [(Var, Value)] -> Locals -> Locals+insertLocalsList kvs locals = foldr insertLocals locals kvs++-- | `Locals` to key value pairs.+localsToList :: Locals -> [(Name, Value)]+localsToList (Locals lmap) = M.toList lmap++-- | Empty `Heap`.+empty_heap :: Heap+empty_heap = Heap M.empty null_addr++-- | `Heap` lookup.+lookupHeap :: MemAddr -> Heap -> Maybe HeapObj+lookupHeap addr (Heap hmap prev) = case M.lookup addr hmap of+    Just (Left redir) -> lookupHeap redir (Heap hmap prev)+    Just (Right hobj) -> Just hobj+    Nothing -> Nothing++-- | `Heap` direct insertion at a specific `MemAddr`.+insertHeapObj :: (MemAddr, HeapObj) -> Heap -> Heap+insertHeapObj (k, v) (Heap hmap prev) = Heap (M.insert k (Right v) hmap) prev++-- | Insert a list of `HeapObj` at specified `MemAddr` locations.+insertHeapObjList :: [(MemAddr, HeapObj)] -> Heap -> Heap+insertHeapObjList kvs heap = foldr insertHeapObj heap kvs++-- | Insert a redirection `MemAddr` into the `Heap`.+insertHeapRedir :: (MemAddr, MemAddr) -> Heap -> Heap+insertHeapRedir (a, r) (Heap hmap prev) = Heap (M.insert a (Left r) hmap) prev++-- | `Heap` allocation. Updates the last `MemAddr` kept in the `Heap`.+allocHeap :: HeapObj -> Heap -> (Heap, MemAddr)+allocHeap hobj (Heap hmap prev) = (heap', addr)+  where+    addr = MemAddr ((memAddrInt prev) + 1)+    heap' = insertHeapObj (addr, hobj) (Heap hmap addr)++-- | 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'++-- | `Heap` to key value pairs.+heapToList :: Heap -> [(MemAddr, Either MemAddr HeapObj)]+heapToList (Heap hmap _) = M.toList hmap++-- | Empty `Globals`.+empty_globals :: Globals+empty_globals = Globals M.empty++-- | `Globals` lookup.+lookupGlobals :: Var -> Globals -> Maybe Value+lookupGlobals var (Globals gmap) = M.lookup (varName var) gmap++-- | `Globals` insertion.+insertGlobals :: (Var, Value) -> Globals -> Globals+insertGlobals (k, v) (Globals gmap) = Globals (M.insert (varName k) v gmap)++-- | 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 kvs globals = foldr insertGlobals globals kvs++-- | `Globals` to key value pairs.+globalsToList :: Globals -> [(Name, Value)]+globalsToList (Globals gmap) = M.toList gmap++-- | Empty `PathCons`.+empty_pathcons :: PathCons+empty_pathcons = PathCons []++-- | `PathCons` insertion.+insertPathCons :: Constraint -> PathCons -> PathCons+insertPathCons cons (PathCons conss) = PathCons (cons : conss)++-- | Insert a list of `Constraint`s into a `PathCons`.+insertPathConsList :: [Constraint] -> PathCons -> PathCons+insertPathConsList conss pathcons = foldr insertPathCons pathcons conss++-- | `PathCons` to list of `Constraint`s.+pathconsToList :: PathCons -> [Constraint]+pathconsToList (PathCons conss) = conss++-- Complex functions that involve multiple data structures.++-- | `Value` lookup from the `Locals` first, then `Globals`.+lookupValue :: Var -> Locals -> Globals -> Maybe Value+lookupValue var locals globals = case lookupLocals var locals of+    Just val -> Just val+    Nothing -> lookupGlobals var globals++-- | `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+    case val of+        LitVal _ -> Nothing+        MemVal addr -> lookupHeap addr heap >>= \hobj -> Just (addr, hobj)++-- | Type of `HeapObj` held at `MemAddr`, if found.+memAddrType :: MemAddr -> Heap -> Maybe Type+memAddrType addr heap = do+    hobj <- lookupHeap addr heap+    case hobj of+        LitObj lit -> Just (litType lit)+        SymObj (Symbol svar _) -> Just (varType svar)+        ConObj dcon _ -> Just (dataConType dcon)+        FunObj ps expr _ -> Just (foldr FunTy (exprType expr) (map varType ps))+        Blackhole -> Just Bottom+

@@ -1,13 +1,11 @@ -- | Export Module for SSTG.Syntax module SSTG.Core.Language     ( module SSTG.Core.Language.Naming-    , module SSTG.Core.Language.Support     , module SSTG.Core.Language.Syntax     , module SSTG.Core.Language.Typing     ) where  import SSTG.Core.Language.Naming-import SSTG.Core.Language.Support import SSTG.Core.Language.Syntax import SSTG.Core.Language.Typing 

@@ -1,6 +1,9 @@ -- | Naming Module module SSTG.Core.Language.Naming     ( allNames+    , varName+    , nameOccStr+    , nameInt     , freshString     , freshName     , freshSeededName@@ -8,156 +11,107 @@     , freshSeededNameList     ) where -import SSTG.Core.Language.Support import SSTG.Core.Language.Syntax  import qualified Data.List as L import qualified Data.Set as S  -- | All `Name`s in a `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)-    acc_ns = stack_ns ++ heap_ns ++ glbls_ns ++ expr_ns ++ pcons_ns---- | `Name`s in a `Stack`.-stackNames :: Stack -> [Name]-stackNames stack = concatMap frameNames (stackToList stack)---- | `Name`s in a `Frame`.-frameNames :: Frame -> [Name]-frameNames (UpdateFrame _) = []-frameNames (ApplyFrame as ls) = localsNames ls ++ concatMap atomNames as-frameNames (CaseFrame var alts ls) = localsNames ls ++ concatMap altNames alts-                                                    ++ varNames var---- | `Name`s in an `Alt`.-altNames :: Alt -> [Name]-altNames (Alt _ vars expr) = concatMap varNames vars ++ exprNames expr---- | `Name`s in the `Locals`-localsNames :: Locals -> [Name]-localsNames locals = map fst (localsToList locals)+allNames :: Program -> [Name]+allNames (Program bindss) = concatMap bindsNames bindss --- | `Name`s in the `Heap`.-heapNames :: Heap -> [Name]-heapNames heap = concatMap (heapObjNames . snd) (heapToList heap)+-- | `Name`s in a `Binds`.+bindsNames :: Binds -> [Name]+bindsNames (Binds _ kvs) = lhs ++ rhs+  where+    lhs = concatMap (varNames . fst) kvs+    rhs = concatMap (bindRhsNames . snd) kvs --- | `Name`s in a `HeapObj`.-heapObjNames :: HeapObj -> [Name]-heapObjNames (AddrObj _) = []-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+-- | A `Var`'s `Name`. Not to be confused with the other function.+varName :: Var -> Name+varName (Var name _) = name --- | `Name`s in a `Symbol`.-symbolNames :: Symbol -> [Name]-symbolNames (Symbol sym mb_scls) = varNames sym ++ scls_ns-  where-    scls_ns = case mb_scls of-                  Nothing -> []-                  Just (e, l) -> exprNames e ++ localsNames l+-- | `Name`s in a `Var`.+varNames :: Var -> [Name]+varNames (Var name ty) = name : typeNames ty  -- | `Name`s in a `BindRhs`. bindRhsNames :: BindRhs -> [Name] bindRhsNames (FunForm prms expr) = concatMap varNames prms ++ exprNames expr bindRhsNames (ConForm dcon args) = concatMap atomNames args ++ dataNames dcon --- | `Name`s in a `Var`.-varNames :: Var -> [Name]-varNames (Var n t) = n : typeNames t---- | `Name`s in an `Atom`.-atomNames :: Atom -> [Name]-atomNames (LitAtom _) = []-atomNames (VarAtom var) = varNames var---- | `Name`s in `Globals`.-globalsNames :: Globals -> [Name]-globalsNames globals = map fst (globalsToList globals)---- | `Name`s in the current evaluation `Code`.-codeNames :: Code -> [Name]-codeNames (Return _) = []-codeNames (Evaluate expr locals) = exprNames expr ++ localsNames locals- -- | `Name`s in an `Expr`. exprNames :: Expr -> [Name] exprNames (Atom atom) = atomNames atom-exprNames (Let bnd expr) = exprNames expr ++ bindNames bnd+exprNames (Let binds expr) = exprNames expr ++ bindsNames binds 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 (Case expr var alts) = exprNames expr ++ concatMap altNames alts                                                 ++ varNames var--- | `Name`s in a `Type`.-typeNames :: Type -> [Name]-typeNames (TyVarTy n ty) = n : typeNames ty-typeNames (CoercionTy coer) = coercionNames coer-typeNames (AppTy t1 t2) = typeNames t1 ++ typeNames t2-typeNames (CastTy ty coer) = typeNames ty ++ coercionNames coer-typeNames (ForAllTy bnd ty) = typeNames ty ++ tyBinderNames bnd-typeNames (FunTy t1 t2) = typeNames t1 ++ typeNames t2-typeNames (TyConApp tc ty) = tyConNames tc ++ concatMap typeNames ty-typeNames (LitTy _) = []-typeNames (Bottom) = [] +-- | `Name`s in an `Atom`.+atomNames :: Atom -> [Name]+atomNames (LitAtom _) = []+atomNames (VarAtom var) = varNames var+ -- | `Name`s in a `PrimFun`. pfunNames :: PrimFun -> [Name]-pfunNames (PrimFun n ty) = n : typeNames ty+pfunNames (PrimFun name ty) = name : typeNames ty  -- | `Name`s in a `DataCon`. dataNames :: DataCon -> [Name]-dataNames (DataCon n ty tys) = n : concatMap typeNames (ty : tys)+dataNames (DataCon name ty tys) = name : concatMap typeNames (ty : tys) +-- | `Name`s in an `Alt`.+altNames :: Alt -> [Name]+altNames (Alt _ vars expr) = concatMap varNames vars ++ exprNames expr++-- | `Name`s in a `Type`.+typeNames :: Type -> [Name]+typeNames (TyVarTy var) = varNames var+typeNames (AppTy ty1 ty2) = typeNames ty1 ++ typeNames ty2+typeNames (ForAllTy bndr ty) = typeNames ty ++ tyBinderNames bndr+typeNames (FunTy ty1 ty2) = typeNames ty1 ++ typeNames ty2+typeNames (TyConApp tycon ty) = tyConNames tycon ++ concatMap typeNames ty+typeNames (CoercionTy coer) = coercionNames coer+typeNames (CastTy ty coer) = typeNames ty ++ coercionNames coer+typeNames (LitTy _) = []+typeNames (Bottom) = []+ -- | `Name`s in a `TyBinder`. tyBinderNames :: TyBinder -> [Name] tyBinderNames (AnonTyBndr) = []-tyBinderNames (NamedTyBndr n) = [n]+tyBinderNames (NamedTyBndr name) = [name]  -- | `Name`s in a `TyCon`. tyConNames :: TyCon -> [Name]-tyConNames (FamilyTyCon n ns) = n : ns-tyConNames (SynonymTyCon n ns) = n : ns-tyConNames (AlgTyCon n ns r) = n : ns ++ algTyRhsNames r-tyConNames (FunTyCon n bs) = n : concatMap tyBinderNames bs-tyConNames (PrimTyCon n bs) = n : concatMap tyBinderNames bs-tyConNames (Promoted n bs dc) = n : concatMap tyBinderNames bs ++ dataNames dc+tyConNames (FamilyTyCon name params) = name : params+tyConNames (SynonymTyCon name params) = name : params+tyConNames (AlgTyCon name params rhs) = name : params ++ algTyRhsNames rhs+tyConNames (FunTyCon name bndrs) = name : concatMap tyBinderNames bndrs+tyConNames (PrimTyCon name bndrs) = name : concatMap tyBinderNames bndrs+tyConNames (Promoted name bndrs dcon) = name : concatMap tyBinderNames bndrs+                                            ++ dataNames dcon  -- | `Name`s in a `Coercion`. coercionNames :: Coercion -> [Name]-coercionNames (Coercion t1 t2) = typeNames t1 ++ typeNames t2+coercionNames (Coercion ty1 ty2) = typeNames ty1 ++ typeNames ty2  -- | `Name`s in a `AlgTyRhs`. algTyRhsNames :: AlgTyRhs -> [Name] algTyRhsNames (AbstractTyCon _) = []-algTyRhsNames (DataTyCon ns) = ns-algTyRhsNames (TupleTyCon n) = [n]-algTyRhsNames (NewTyCon n) = [n]---- | `Name`s in a `Bind`.-bindNames :: Bind -> [Name]-bindNames (Bind _ bnd) = lhs ++ rhs-  where-    lhs = concatMap (varNames . fst) bnd-    rhs = concatMap (bindRhsNames . snd) bnd+algTyRhsNames (DataTyCon names) = names+algTyRhsNames (TupleTyCon name) = [name]+algTyRhsNames (NewTyCon name) = [name] --- | `Name`s in a `PathCons`.-pconsNames :: PathCons -> [Name]-pconsNames pathcons = concatMap constraintNames (pathconsToList pathcons)+-- | A `Name`'s occurrence string.+nameOccStr :: Name -> String+nameOccStr (Name occ _ _ _) = occ --- | `Name`s in a `PathCons`.-constraintNames :: Constraint -> [Name]-constraintNames (Constraint (_, vs) e locs _) = exprNames e ++ localsNames locs-                                                            ++ map varName vs+-- | A `Name`'s unique int.+nameInt :: Name -> Int+nameInt (Name _ _ _ int) = int  -- | 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@@ -196,7 +150,7 @@     occ' = freshString 1 occ (S.fromList alls)     unq' = maxs + 1     alls = map nameOccStr confs-    maxs = L.maximum (unq : map nameUnique confs)+    maxs = L.maximum (unq : map nameInt confs)  -- | Generate a list of `Name`s, each corresponding to the appropriate element -- of the `NameSpace` list.

@@ -1,351 +0,0 @@--- | Symbolic STG Execution Support Architecture-module SSTG.Core.Language.Support-    ( SymbolicT(..)-    , fmap-    , pure-    , (<*>)-    , return-    , (>>=)--    , State(..)-    , Symbol(..)-    , Status(..)-    , Stack-    , Frame(..)-    , MemAddr-    , Value(..)-    , Locals-    , Heap-    , HeapObj(..)-    , Globals-    , Code(..)-    , PathCons-    , Constraint(..)--    , nameOccStr-    , nameUnique-    , varName-    , null_addr-    , addrInt--    , init_status-    , incStatusSteps-    , updateStatusId--    , empty_stack-    , popStack-    , pushStack-    , stackToList--    , empty_locals-    , lookupLocals-    , insertLocals-    , insertLocalsList-    , localsToList--    , empty_heap-    , lookupHeap-    , allocHeap-    , allocHeapList-    , insertHeap-    , insertHeapList-    , heapToList--    , empty_globals-    , lookupGlobals-    , insertGlobals-    , insertGlobalsList-    , globalsToList--    , empty_pathcons-    , insertPathCons-    , insertPathConsList-    , pathconsToList--    , lookupValue-    , vlookupHeap-    , memAddrType-    ) where--import SSTG.Core.Language.Syntax-import SSTG.Core.Language.Typing--import qualified Data.Map as M---- | 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.-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.-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.-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` 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-                   , state_globals :: !Globals-                   , state_code :: !Code-                   , state_names :: ![Name]-                   , state_paths :: !PathCons-                   } deriving (Show, Eq, Read)---- | 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)---- | State status.-data Status = Status { status_id :: !Int-                     , status_parent :: !Int-                     , status_steps :: !Int-                     } deriving (Show, Eq, Read)---- | Execution stack used in graph reduction semnatics.-newtype Stack = Stack [Frame] deriving (Show, Eq, Read)---- | Frames of a stack.-data Frame = CaseFrame Var [Alt] Locals-           | ApplyFrame [Atom] Locals-           | UpdateFrame MemAddr-           deriving (Show, Eq, Read)---- | Memory address for things on the `Heap`.-newtype MemAddr = MemAddr Int deriving (Show, Eq, Read, Ord)---- | 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 binds a `Var`'s `Name` to its some `Value`.-newtype Locals = Locals (M.Map Name Value) deriving (Show, Eq, Read)---- | 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 objects.-data HeapObj = LitObj Lit-             | SymObj Symbol-             | ConObj DataCon [Value]-             | FunObj [Var] Expr Locals-             | AddrObj MemAddr-             | Blackhole-             deriving (Show, Eq, Read)---- | 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 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 are the conjunctive normal form of `Constraint`s.-newtype PathCons = PathCons [Constraint] deriving (Show, Eq, Read)---- | Constraints denote logical paths taken in program execution thus far.-data Constraint = Constraint (AltCon, [Var]) Expr Locals Bool-                deriving (Show, Eq, Read)---- Simple functions that require only the immediate data structure.---- | A `Name`'s occurrence string.-nameOccStr :: Name -> String-nameOccStr (Name occ _ _ _) = occ---- | `Name` imique `Int`.-nameUnique :: Name -> Int-nameUnique (Name _ _ _ unq) = unq---- | Variable name.-varName :: Var -> Name-varName (Var name _) = name---- | Null `MemAddr`.-null_addr :: MemAddr-null_addr = MemAddr 0---- | `MemAddr`'s `Int` value.-addrInt :: MemAddr -> Int-addrInt (MemAddr int) = int---- | Initial `Status`.-init_status :: Status-init_status = Status { status_id = 1-                     , status_parent = 0-                     , status_steps = 0 }---- | Increment `Status` steps.-incStatusSteps :: Status -> Status-incStatusSteps status = status { status_steps = (status_steps status) + 1 }---- | Update the `Status` id.-updateStatusId :: Int -> Status -> Status-updateStatusId new_id status = status { status_id = new_id-                                      , status_parent = status_id status }---- | Empty `Stack.-empty_stack :: Stack-empty_stack = Stack []---- | `Stack` pop.-popStack :: Stack -> Maybe (Frame, Stack)-popStack (Stack []) = Nothing-popStack (Stack (frame:frames)) = Just (frame, Stack frames)---- | `Stack` push.-pushStack :: Frame -> Stack -> Stack-pushStack frame (Stack frames) = Stack (frame : frames)---- | `Stack` as list of `Frame`s.-stackToList :: Stack -> [Frame]-stackToList (Stack frames) = frames---- | Empty `Locals`.-empty_locals :: Locals-empty_locals = Locals M.empty---- | `Locals` lookup.-lookupLocals :: Var -> Locals -> Maybe Value-lookupLocals var (Locals lmap) = M.lookup (varName var) lmap---- | `Locals` insertion.-insertLocals :: (Var, Value) -> Locals -> Locals-insertLocals (k, v) (Locals lmap) = Locals (M.insert (varName k) v lmap)---- | List insertion into `Locals`.-insertLocalsList :: [(Var, Value)] -> Locals -> Locals-insertLocalsList kvs locals = foldr insertLocals locals kvs---- | `Locals` to key value pairs.-localsToList :: Locals -> [(Name, Value)]-localsToList (Locals lmap) = M.toList lmap---- | Empty `Heap`.-empty_heap :: Heap-empty_heap = Heap M.empty null_addr---- | `Heap` lookup.-lookupHeap :: MemAddr -> Heap -> Maybe HeapObj-lookupHeap addr (Heap hmap prev) = case M.lookup addr hmap of-    Just (AddrObj redir) -> lookupHeap redir (Heap hmap prev)-    mb_hobj -> mb_hobj---- | `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 ((addrInt prev) + 1)-    hmap' = M.insert addr hobj hmap---- | 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'---- | `Heap` direct insertion at a specific `MemAddr`.-insertHeap :: (MemAddr, HeapObj) -> Heap -> Heap-insertHeap (k, v) (Heap hmap prev) = Heap (M.insert k v hmap) prev---- | Insert a list of `HeapObj` at specified `MemAddr` locations.-insertHeapList :: [(MemAddr, HeapObj)] -> Heap -> Heap-insertHeapList kvs heap = foldr insertHeap heap kvs---- | `Heap` to key value pairs.-heapToList :: Heap -> [(MemAddr, HeapObj)]-heapToList (Heap hmap _) = M.toList hmap---- | Empty `Globals`.-empty_globals :: Globals-empty_globals = Globals M.empty---- | `Globals` lookup.-lookupGlobals :: Var -> Globals -> Maybe Value-lookupGlobals var (Globals gmap) = M.lookup (varName var) gmap---- | `Globals` insertion.-insertGlobals :: (Var, Value) -> Globals -> Globals-insertGlobals (k, v) (Globals gmap) = Globals (M.insert (varName k) v gmap)---- | 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 kvs globals = foldr insertGlobals globals kvs---- | `Globals` to key value pairs.-globalsToList :: Globals -> [(Name, Value)]-globalsToList (Globals gmap) = M.toList gmap---- | Empty `PathCons`.-empty_pathcons :: PathCons-empty_pathcons = PathCons []---- | `PathCons` insertion.-insertPathCons :: Constraint -> PathCons -> PathCons-insertPathCons cons (PathCons conss) = PathCons (cons : conss)---- | Insert a list of `Constraint`s into a `PathCons`.-insertPathConsList :: [Constraint] -> PathCons -> PathCons-insertPathConsList conss pathcons = foldr insertPathCons pathcons conss---- | `PathCons` to list of `Constraint`s.-pathconsToList :: PathCons -> [Constraint]-pathconsToList (PathCons conss) = conss---- Complex functions that involve multiple data structures.---- | `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-    Just val -> Just val---- | `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-    case val of-        LitVal _ -> Nothing-        MemVal addr -> lookupHeap addr heap >>= \hobj -> Just (addr, hobj)---- | Type of `HeapObj` held at `MemAddr`, if found.-memAddrType :: MemAddr -> Heap -> Maybe Type-memAddrType addr heap = do-    hobj <- lookupHeap addr heap-    case hobj of-        AddrObj redir -> memAddrType redir heap-        LitObj lit -> Just (litType lit)-        SymObj (Symbol s _) -> Just (varType s)-        ConObj dcon _ -> Just (dataconType dcon)-        FunObj ps e _ -> Just (foldr FunTy (exprType e) (map varType ps))-        Blackhole -> Just Bottom-

@@ -6,7 +6,7 @@ -- | A `Program` is defined as a list of bindings. The @Name@ is an identifier -- that determines a unique binder to the @var@. In practice, these are defined -- to be `Name` and `Var` respectively.-newtype Program = Program [Bind] deriving (Show, Eq, Read)+newtype Program = Program [Binds] deriving (Show, Eq, Read)  -- | Variables, data constructors, type variables, and type constructors. data NameSpace = VarNSpace | DataNSpace | TvNSpace | TcClsNSpace@@ -24,9 +24,9 @@  -- | 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.+-- value deriviation, and `LitEval` to represent symbolic literal evaluation,+-- as literal manipulation functions are defined in the Haskell Prelude, and+-- thus outside of scope for us. data Lit = MachChar Char Type          | MachStr String Type          | MachInt Int Type@@ -37,13 +37,12 @@          | MachNullAddr Type          | BlankAddr          | AddrLit Int-         | SymLit Var-         | SymLitEval PrimFun [Lit]+         | LitEval PrimFun [Lit]          deriving (Show, Eq, Read)  -- | Atomic objects. `VarAtom` may be used for variable lookups, while -- `LitAtom` is used to denote literals.-data Atom = LitAtom (Lit)+data Atom = LitAtom Lit           | VarAtom Var           deriving (Show, Eq, Read) @@ -55,7 +54,7 @@           | PrimApp PrimFun [Atom]           | ConApp DataCon [Atom]           | FunApp Var [Atom]-          | Let Bind Expr+          | Let Binds Expr           | Case Expr Var [Alt]           deriving (Show, Eq, Read) @@ -69,8 +68,8 @@             | Default             deriving (Show, Eq, Read) --- | Bind-data Bind = Bind RecForm [(Var, BindRhs)] deriving (Show, Eq, Read)+-- | Bindings+data Binds = Binds RecForm [(Var, BindRhs)] deriving (Show, Eq, Read)  -- | Recursive? data RecForm = Rec | NonRec deriving (Show, Eq, Read)@@ -88,7 +87,7 @@ -- | 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 Type = TyVarTy Name Type+data Type = TyVarTy Var           | AppTy Type Type           | ForAllTy TyBinder Type           | CastTy Type Coercion

@@ -21,8 +21,7 @@ litType (MachNullAddr ty) = ty litType (BlankAddr) = Bottom litType (AddrLit _) = Bottom-litType (SymLit var) = varType var-litType (SymLitEval pf args) = foldl AppTy (primfunType pf) (map litType args)+litType (LitEval pf args) = foldl AppTy (primFunType pf) (map litType args)  -- | Atom type. atomType :: Atom -> Type@@ -30,12 +29,12 @@ atomType (VarAtom var) = varType var  -- | Primitive function type.-primfunType :: PrimFun -> Type-primfunType (PrimFun _ ty) = ty+primFunType :: PrimFun -> Type+primFunType (PrimFun _ ty) = ty  -- | Data constructor type denoted as a function.-dataconType :: DataCon -> Type-dataconType (DataCon _ ty tys) = foldr FunTy ty tys+dataConType :: DataCon -> Type+dataConType (DataCon _ ty tys) = foldr FunTy ty tys  -- | Alt type altType :: Alt -> Type@@ -44,8 +43,8 @@ -- | 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 dc args) = foldl AppTy (dataconType dc) (map atomType args)+exprType (PrimApp pf args) = foldl AppTy (primFunType pf) (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

@@ -2,7 +2,7 @@ module SSTG.Core.Translation.Haskell     ( CompileClosure     , mkCompileClosure-    , mkTargetBinds+    , mkTargetBindsList     , mkIOString     ) where @@ -37,9 +37,9 @@     return (showPpr dflags obj)  -- | Given the project directory and the source file path, compiles the--- `ModuleGraph` and translates it into a SSTG `Bind`s.-mkTargetBinds :: FilePath -> FilePath -> IO [SL.Bind]-mkTargetBinds proj src = do+-- `ModuleGraph` and translates it into a SSTG `Binds`s.+mkTargetBindsList :: FilePath -> FilePath -> IO [SL.Binds]+mkTargetBindsList proj src = do     (sums_gutss, dflags, env) <- mkCompileClosure proj src     let (sums, gutss) = (map fst sums_gutss, map snd sums_gutss)     let mod_lcs = map (\s -> (ms_mod s, ms_location s)) sums@@ -51,7 +51,7 @@     let zipd2 = zip (map fst mod_lcs) preps     stg_bindss <- mapM (\(m, p) -> coreToStg dflags m p) zipd2     -- Create the binds.-    return (map mkBind (concat stg_bindss))+    return (map mkBinds (concat stg_bindss))  -- | Compilation closure type. type CompileClosure = ([(ModSummary, ModGuts)], DynFlags, HscEnv)@@ -83,12 +83,12 @@ mkExpr (StgApp occ args) = SL.FunApp (mkVar occ) (map mkAtom args) mkExpr (StgConApp dcon args) = SL.ConApp (mkData dcon) (map mkAtom args) mkExpr (StgOpApp op args _) = SL.PrimApp (mkPrimOp op) (map mkAtom args)-mkExpr (StgTick _ expr)= mkExpr expr+mkExpr (StgTick _ expr) = mkExpr expr mkExpr (StgLam _ _) = error "mkExpr: StgLam detected"-mkExpr (StgLet bind expr) = SL.Let (mkBind bind) (mkExpr expr)-mkExpr (StgLetNoEscape _ _ bind expr) = mkExpr (StgLet bind expr)-mkExpr (StgCase mxpr _ _ cvar _ _ alts) = SL.Case (mkExpr mxpr) (mkVar cvar)-                                                  (map mkAlt alts)+mkExpr (StgLet binds expr) = SL.Let (mkBinds binds) (mkExpr expr)+mkExpr (StgLetNoEscape _ _ binds expr) = mkExpr (StgLet binds expr)+mkExpr (StgCase mexpr _ _ cvar _ _ alts) = SL.Case (mkExpr mexpr) (mkVar cvar)+                                                   (map mkAlt alts)  -- | Make SSTG `Atom`. mkAtom :: StgArg -> SL.Atom@@ -103,8 +103,8 @@     ns = (mkNameSpace . occNameSpace . nameOccName) name     unq = (getKey . nameUnique) name     mdl = case nameModule_maybe name of-              Nothing -> Nothing               Just md -> Just ((moduleNameString . moduleName) md)+              Nothing -> Nothing  -- | Make SSTG `NameSpace`. mkNameSpace :: NameSpace -> SL.NameSpace@@ -122,9 +122,10 @@     vtype = (mkType . varType) var  -- | Make SSTG `Bind`.-mkBind :: StgBinding -> SL.Bind-mkBind (StgNonRec bind r) = SL.Bind SL.NonRec [(mkVar bind, mkRhs r)]-mkBind (StgRec bind) = SL.Bind SL.Rec (map (\(b,r) -> (mkVar b, mkRhs r)) bind)+mkBinds :: StgBinding -> SL.Binds+mkBinds (StgNonRec var rhs) = SL.Binds SL.NonRec [(mkVar var, mkRhs rhs)]+mkBinds (StgRec binds) = SL.Binds SL.Rec+                                  (map (\(v, r) -> (mkVar v, mkRhs r)) binds)  -- | Make SSTG `BindRhs`. mkRhs :: StgRhs -> SL.BindRhs@@ -181,10 +182,10 @@  -- | Make SSTG `Type`. mkType :: Type -> SL.Type-mkType (TyVarTy v) = SL.TyVarTy (mkName (V.varName v)) (mkType (varType v))+mkType (TyVarTy var) = SL.TyVarTy (mkVar var) mkType (AppTy t1 t2) = SL.AppTy (mkType t1) (mkType t2) mkType (TyConApp tc ts) = SL.TyConApp (mkTyCon tc) (map mkType ts)-mkType (ForAllTy b ty) = SL.ForAllTy (mkTyBinder b) (mkType ty)+mkType (ForAllTy tb ty) = SL.ForAllTy (mkTyBinder tb) (mkType ty) mkType (LitTy tlit) = SL.LitTy (mkTyLit tlit) mkType (CastTy ty cor) = SL.CastTy (mkType ty) (mkCoercion cor) mkType (CoercionTy cor) = SL.CoercionTy (mkCoercion cor)@@ -215,7 +216,7 @@ -- | make SSTG `TyBinder`. mkTyBinder :: TyBinder -> SL.TyBinder mkTyBinder (Anon _) = SL.AnonTyBndr-mkTyBinder (Named v _) = SL.NamedTyBndr (mkName (V.varName v))+mkTyBinder (Named var _) = SL.NamedTyBndr (mkName (V.varName var))  -- | Make SSTG `Type` literals. mkTyLit :: TyLit -> SL.TyLit

@@ -2,7 +2,7 @@ module SSTG.Utils.Printing     ( pprStateStr     , pprLivesDeadsStr-    , pprBindStr+    , pprBindsStr     ) where  import SSTG.Core@@ -104,7 +104,7 @@  -- | Print `MemAddr`. pprMemAddrStr :: MemAddr -> String-pprMemAddrStr addr = show (addrInt addr)+pprMemAddrStr addr = show (memAddrInt addr)  -- | Print `Name`. pprNameStr :: Name -> String@@ -156,44 +156,56 @@     locs_str = pprLocalsStr locals     acc_strs = [header, injIntoList [expr_str, locs_str]] --- | Print `HeapObj`.-pprHeapObjStr :: HeapObj -> String-pprHeapObjStr (Blackhole) = "Blackhole!!!"-pprHeapObjStr (AddrObj addr) = pprMemAddrStr addr-pprHeapObjStr (LitObj lit) = injSpace acc_strs+-- | Print `Heap`'s redirection.+pprMemRedirStr :: (MemAddr, MemAddr) -> String+pprMemRedirStr (addr, redir) = sub (addr_str ++ ", " ++ redir_str)   where+    addr_str = pprMemAddrStr addr+    redir_str = pprMemAddrStr redir++-- | Print `Heap`'s`HeapObj`.+pprMemHeapObjStr :: (MemAddr, HeapObj) -> String+pprMemHeapObjStr (addr, Blackhole) = sub (pprMemAddrStr addr ++ ", Blackhole")+pprMemHeapObjStr (addr, LitObj lit) = acc_str+  where     header = "LitObj"+    addr_str = pprMemAddrStr addr     lit_str = pprLitStr lit-    acc_strs = [header, lit_str]-pprHeapObjStr (SymObj (Symbol sym mb_scls)) = injSpace acc_strs+    acc_str = sub (addr_str ++ ", " ++ injSpace [header, lit_str])+pprMemHeapObjStr (addr, SymObj (Symbol sym mb_scls)) = acc_str   where     header = "SymObj"+    addr_str = pprMemAddrStr addr     var_str = pprVarStr sym     scls_str = (sub . pprSymClosureStr) mb_scls-    acc_strs = [header, var_str, scls_str]-pprHeapObjStr (ConObj dcon vals) = injSpace acc_strs+    acc_str = sub (addr_str ++ ", " ++ injSpace [header, var_str, scls_str])+pprMemHeapObjStr (addr, ConObj dcon vals) = acc_str   where     header = "ConObj"+    addr_str = pprMemAddrStr addr     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+    acc_str = sub (addr_str ++ ", " ++ injSpace [header, dcon_str, vals_str])+pprMemHeapObjStr (addr, FunObj params expr locals) = acc_str   where     header = "FunObj"+    addr_str = pprMemAddrStr addr     prms_str = injIntoList (map pprVarStr params)     expr_str = pprExprStr expr     locs_str = pprLocalsStr locals-    acc_strs = [header, prms_str, expr_str, locs_str]+    funobj_str = injSpace [header, prms_str, expr_str, locs_str]+    acc_str = sub (addr_str ++ ", " ++ funobj_str)  -- | Print `Heap`. pprHeapStr :: Heap -> String pprHeapStr heap = injNewLine acc_strs   where     hlist = heapToList heap-    addr_strs = map (pprMemAddrStr . fst) hlist-    hobj_strs = map (pprHeapObjStr . snd) hlist-    zipd_strs = zip addr_strs hobj_strs-    acc_strs = map (\(m, o) -> sub (m ++ ", " ++ o)) zipd_strs+    addr_redirs = [(addr, r) | (addr, Left r) <- hlist]+    addr_hobjs = [(addr, o) | (addr, Right o) <- hlist]+    addr_redir_strs = map pprMemRedirStr addr_redirs+    addr_hobj_strs = map pprMemHeapObjStr addr_hobjs+    acc_strs = addr_redir_strs ++ addr_hobj_strs  -- | Print `Globals`. pprGlobalsStr :: Globals -> String@@ -314,19 +326,19 @@  -- | Print @(Var, BindRhs)@. pprBindKVStr :: (Var, BindRhs) -> String-pprBindKVStr (var, lamf) = (sub . injComma) acc_strs+pprBindKVStr (var, rhs) = (sub . injComma) acc_strs   where     var_str = pprVarStr var-    lamf_str = pprBindRhsStr lamf-    acc_strs = [var_str, lamf_str]+    rhs_str = pprBindRhsStr rhs+    acc_strs = [var_str, rhs_str] --- | Print `Bind`.-pprBindStr :: Bind -> String-pprBindStr (Bind rec bnd) = injSpace acc_strs+-- | Print `Binds`.+pprBindsStr :: Binds -> String+pprBindsStr (Binds rec kvs) = injSpace acc_strs   where     header = case rec of { Rec -> "Rec"; NonRec -> "NonRec" }-    bnds_str = injIntoList (map pprBindKVStr bnd)-    acc_strs = [header, bnds_str]+    kvs_str = injIntoList (map pprBindKVStr kvs)+    acc_strs = [header, kvs_str]  -- | Print `Expr`. pprExprStr :: Expr -> String@@ -360,17 +372,17 @@     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+pprExprStr (Let binds expr) = injSpace acc_strs   where     header = "Let"-    bnd_str = (sub . pprBindStr) bnd+    binds_str = (sub . pprBindsStr) binds     expr_str = (sub . pprExprStr) expr-    acc_strs = [header, bnd_str, expr_str]+    acc_strs = [header, binds_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 = snd ("__Type__", show ty)+pprTypeStr ty = fst ("__Type__", show ty)  -- | Print `Code`. pprCodeStr :: Code -> String@@ -404,6 +416,6 @@     prms_str = injIntoList (map pprVarStr ps)     expr_str = pprExprStr expr     locs_str = pprLocalsStr locals-    hold_str = case hold of { True -> "Positive"; False -> "Negative" }+    hold_str = if hold then "Positive" else "Negative"     acc_strs = [acon_str, prms_str, expr_str, locs_str, hold_str]