SSTG 0.1.0.7 → 0.1.0.8

raw patch · 8 files changed

+315/−197 lines, 8 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• SSTG.cabal +1/−1
• src/SSTG/Core/Execution/Engine.hs +16/−20
• src/SSTG/Core/Execution/Naming.hs +16/−25
• src/SSTG/Core/Execution/Rules.hs +47/−46
• src/SSTG/Core/Execution/Support.hs +166/−24
• src/SSTG/Core/Syntax/Language.hs +26/−30
• src/SSTG/Core/Translation/Haskell.hs +9/−11
• src/SSTG/Utils/Printing.hs +34/−40

@@ -1,5 +1,5 @@ name:                SSTG-version:             0.1.0.7+version:             0.1.0.8 synopsis:            STG Symbolic Execution description:         Prototype of STG-based Symbolic Execution for Haskell. homepage:            https://github.com/AntonXue/SSTG#readme

@@ -14,8 +14,6 @@ import SSTG.Core.Execution.Stepping import SSTG.Core.Execution.Support -import qualified Data.Map as M- -- | Load Result data LoadResult = LoadOkay  State                 | LoadGuess State [Binding]@@ -38,11 +36,11 @@   where -- Status or something.         status   = Status { steps = 0 }         -- Stack initialized to empty.-        stack    = Stack []+        stack    = emptyStack         -- Globals and Heap are loaded together. They are still beta forms now.-        heap0    = Heap M.empty (MemAddr 0)+        heap0    = emptyHeap         (glist, heap1, bnd_addrss) = initGlobals bnds heap0-        globals0 = Globals (M.fromList glist)+        globals0 = insertGlobalsList glist emptyGlobals         (heap2, localss) = liftBindings bnd_addrss globals0 heap1         bnd_locs = zip bnds localss         -- Code loading. Completes heap and globals with symbolic injection.@@ -57,8 +55,8 @@                          , state_globals = globals                          , state_code    = code                          , state_names   = []-                         , state_paths   = []-                         , state_links   = SymLinks M.empty }+                         , state_paths   = emptyPathCons+                         , state_links   = emptySymLinks }          -- Gather information on all variables.         state    = state0 { state_names = allNames state0 }@@ -72,23 +70,22 @@ -- | Allocate List of Bindings allocBindingList :: [Binding] -> Heap -> (Heap, [[MemAddr]]) allocBindingList []     heap = (heap, [])-allocBindingList (b:bs) heap = (res_heap, addrs : as)+allocBindingList (b:bs) heap = (heapf, addrs : as)   where (heap', addrs) = allocBinding b heap-        (res_heap, as) = allocBindingList bs heap'+        (heapf, as)    = allocBindingList bs heap'  -- | Binding Address to Name Values-bndAddrsToNameVals :: (Binding, [MemAddr]) -> [(Name, Value)]-bndAddrsToNameVals (Binding _ rhss, addrs) = zip names pointers-  where names    = map (varName . fst) rhss-        pointers = map (\a -> MemVal a) addrs+bndAddrsToVarVals :: (Binding, [MemAddr]) -> [(Var, Value)]+bndAddrsToVarVals (Binding _ rhss, addrs) = zip (map fst rhss) mem_vals+  where mem_vals = map (\a -> MemVal a) addrs  -- | Initialize Globals initGlobals :: [Binding] -> Heap ->-               ([(Name, Value)], Heap, [(Binding, [MemAddr])])-initGlobals bnds heap = (name_vals, heap', bnd_addrss)+               ([(Var, Value)], Heap, [(Binding, [MemAddr])])+initGlobals bnds heap = (var_vals, heap', bnd_addrss)   where (heap', addrss) = allocBindingList bnds heap         bnd_addrss = zip bnds addrss-        name_vals  = concatMap bndAddrsToNameVals bnd_addrss+        var_vals   = concatMap bndAddrsToVarVals bnd_addrss  -- | Force Atom Lookup forceLookupValue :: Atom -> Locals -> Globals -> Value@@ -109,7 +106,7 @@ liftBinding (Binding rec pairs, addrs) globals heap = (heap', locals)   where (vars, rhss) = unzip pairs         mem_vals = map (\a -> MemVal a) addrs-        e_locs   = Locals M.empty+        e_locs   = emptyLocals         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@@ -118,9 +115,9 @@ -- | Lift Binding List liftBindings :: [(Binding, [MemAddr])] -> Globals -> Heap -> (Heap, [Locals]) liftBindings []       _       heap = (heap, [])-liftBindings (bm:bms) globals heap = (res_heap, locals : ls)+liftBindings (bm:bms) globals heap = (heapf, locals : ls)   where (heap', locals) = liftBinding bm globals heap-        (res_heap, ls)  = liftBindings bms globals heap'+        (heapf, ls)     = liftBindings bms globals heap'  -- | Return a sub-list of bindings in which the entry candidate appears. entryMatches :: String -> [(Binding, Locals)] -> [(Binding, Locals)]@@ -188,5 +185,4 @@ execute1 :: Int -> State -> ([LiveState], [DeadState]) execute1 n state | n < 1     = ([([], state)], [])                  | otherwise = runBoundedBFS n state- 

@@ -12,7 +12,6 @@ import SSTG.Core.Execution.Support  import qualified Data.List as L-import qualified Data.Map  as M import qualified Data.Set  as S  -- | All `Name`s in a `State`.@@ -29,8 +28,7 @@  -- | `Name`s in a `Stack`. stackNames :: Stack -> [Name]-stackNames (Stack [])     = []-stackNames (Stack (f:fs)) = frameNames f ++ stackNames (Stack fs)+stackNames stack = concatMap frameNames (stackToList stack)  -- | `Name`s in a `Frame`. frameNames :: Frame -> [Name]@@ -45,15 +43,15 @@  -- | `Name`s in the `Locals` localsNames :: Locals -> [Name]-localsNames (Locals lmap) = M.keys lmap+localsNames locals = map fst (localsToList locals)  -- | `Name`s in the `Heap`. heapNames :: Heap -> [Name]-heapNames (Heap heap _) = concatMap (heapObjNames . snd) hlist-  where hlist = M.toList heap+heapNames heap = concatMap (heapObjNames . snd) (heapToList heap)  -- | `Name`s in a `HeapObj`. heapObjNames :: HeapObj -> [Name]+heapObjNames (AddrObj _)           = [] heapObjNames (Blackhole)           = [] heapObjNames (LitObj _)            = [] heapObjNames (SymObj sym)          = symbolNames sym@@ -84,7 +82,7 @@  -- | `Name`s in `Globals`. globalsNames :: Globals -> [Name]-globalsNames (Globals gmap) = M.keys gmap+globalsNames globals = map fst (globalsToList globals)  -- | `Name`s in the current evaluation `Code`. codeNames :: Code -> [Name]@@ -116,13 +114,9 @@ pfunNames :: PrimFun -> [Name] pfunNames (PrimFun n ty) = n : typeNames ty --- | `Name`s in a `ConTag`.-conTagName :: ConTag -> Name-conTagName (ConTag n _) = n- -- | `Name`s in a `DataCon`. dataNames :: DataCon -> [Name]-dataNames (DataCon tg ty tys) = conTagName tg : concatMap typeNames (ty : tys)+dataNames (DataCon name ty tys) = name : concatMap typeNames (ty : tys)  -- | `Name`s in a `TyBinder`. tyBinderNames :: TyBinder -> [Name]@@ -146,9 +140,9 @@ -- | `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]+algTyRhsNames (DataTyCon names) = names+algTyRhsNames (TupleTyCon name) = [name]+algTyRhsNames (NewTyCon name)   = [name]  -- | `Name`s in a `Binding`. bindingNames :: Binding -> [Name]@@ -158,19 +152,16 @@  -- | `Name`s in a `PathCons`. pconsNames :: PathCons -> [Name]-pconsNames []     = []-pconsNames (c:cs) = pcondNames c ++ pconsNames cs---- | `Name`s in a `PathCond`.-pcondNames :: PathCond -> [Name]-pcondNames (PathCond (_, vars) expr locals _) = map varName vars ++-                                                exprNames expr   ++-                                                localsNames locals+pconsNames pathcons = concatMap constraintNames (pathconsToList pathcons) +-- | `Name`s in a `PathCons`.+constraintNames :: Constraint -> [Name]+constraintNames (Constraint (_, vars) expr locals _) = exprNames expr     +++                                                       localsNames locals +++                                                       map varName vars -- | `Name`s in a `SymLinks`. linksNames :: SymLinks -> [Name]-linksNames (SymLinks links) = concatMap (\(a, b) -> [a, b]) slist-  where slist = M.toList links+linksNames symlinks = concatMap (\(a, b) -> [a, b]) (symlinksToList symlinks)  -- | 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

@@ -57,10 +57,10 @@ isStateValueForm State { state_stack = stack                        , state_heap  = heap                        , state_code  = code }-  | Stack []          <- stack+  | Nothing           <- popStack stack   , Return (LitVal _) <- code = True -  | Stack []             <- stack+  | Nothing              <- popStack stack   , Return (MemVal addr) <- code   , Just hobj            <- lookupHeap addr heap   , isHeapValueForm hobj = True@@ -70,7 +70,7 @@ -- | `Value` to `Lit`. valueToLit :: Value -> Lit valueToLit (LitVal lit)  = lit-valueToLit (MemVal addr) = AddrLit (memAddrInt addr)+valueToLit (MemVal addr) = AddrLit (addrInt addr)  -- | Uneven `zip` of two `List`s, with the leftover stored. unevenZip :: [a] -> [b] -> ([(a, b)], Either [a] [b])@@ -80,7 +80,7 @@   where (acc, excess) = unevenZip as bs  -- | Lift action wrapper type.-data LiftAct a = LiftAct  a Locals Globals Heap [Name]+data LiftAct a = LiftAct a Locals Globals Heap [Name]  -- | Lift uninterpreted `Var`s into `Globals`. liftUnInt :: LiftAct Var -> LiftAct MemAddr@@ -172,12 +172,12 @@ matchDataAlts :: DataCon -> [Alt] -> [Alt] matchDataAlts dc alts = [a | a @ (Alt (DataAlt adc) _ _) <- alts, dc == adc] --- | Negate `PathCons`.-negatePathCons :: PathCons -> PathCons-negatePathCons pcs = map (\(PathCond a e l b) -> (PathCond a e l (not b))) pcs+-- | Negate `Constraint`.+negateConstraint :: Constraint -> Constraint+negateConstraint (Constraint a e l b) = Constraint a e l (not b)  -- | Lift `Alt`s during branching caused by symbolics.-liftSymAlt :: LiftAct (Var, MemAddr, Var, Alt) -> LiftAct (Expr, PathCons)+liftSymAlt :: LiftAct (Var, MemAddr, Var, Alt) -> LiftAct (Expr, [Constraint]) liftSymAlt (LiftAct args locals globals heap confs) = pass_out   where (mvar, addr, cvar, Alt ac params expr) = args         snames   = freshSeededNameList (map varName params) confs@@ -188,19 +188,20 @@         llist    = (cvar, MemVal addr) : zip params mem_vals         locals'  = insertLocalsList llist locals         mxpr     = Atom (VarAtom mvar)-        pcons    = [PathCond (ac, params) mxpr locals' True]+        conss    = [Constraint (ac, params) mxpr locals' True]         confs'   = snames ++ confs-        pass_out = LiftAct (expr, pcons) locals' globals heap' confs'+        pass_out = LiftAct (expr, conss) locals' globals heap' confs'  -- | `Alt` closure to `State`.-liftedAltToState :: State -> LiftAct (Expr, PathCons) -> State+liftedAltToState :: State -> LiftAct (Expr, [Constraint]) -> State liftedAltToState state (LiftAct args locals globals heap confs) = state'-  where (expr, pcons) = args+  where (expr, conss) = args+        pathcons      = state_paths state         state' = state { state_heap    = heap                        , state_globals = globals                        , state_code    = Evaluate expr locals                        , state_names   = confs-                       , state_paths   = pcons ++ state_paths state }+                       , state_paths   = insertPathConsList conss pathcons }  -- | Reduce the state if it matches some type of reduction `Rule`. Return -- `Nothing` to denote that rule application has completely failed.@@ -283,12 +284,12 @@   | Evaluate (FunApp fun args) locals <- code   , Just (_, hobj)              <- vlookupHeap fun locals globals heap   , FunObj params expr fun_locs <- hobj-  , (_, Left ex_ps)             <- unevenZip params args =+  , (_, Left ex_params)         <- unevenZip params args =     let pass_in   = LiftAct args locals globals heap confs         LiftAct vals _ globals' heap' confs' = liftAtomList pass_in         fun_locs' = insertLocalsList (zip params vals) fun_locs         -- New Fun Object.-        pobj      = FunObj ex_ps expr fun_locs'+        pobj      = FunObj ex_params expr fun_locs'         (heapf, paddr) = allocHeap pobj heap'     in Just (RuleFunAppUnder             ,[state { state_heap    = heapf@@ -388,8 +389,8 @@         -- Make AltCon states first.         acon_sts   = map (liftedAltToState state) acon_lifts         -- Make DEFAULT states next.-        all_pcons  = concatMap (\(LiftAct (_, pc) _ _ _ _) -> pc) acon_lifts-        negs       = negatePathCons all_pcons+        all_conss  = concatMap (\(LiftAct (_, c) _ _ _ _) -> c) acon_lifts+        negs       = map negateConstraint all_conss         def_lifts' = map (\(LiftAct (e, _) l g h c) ->                            (LiftAct (e, negs) l g h c)) def_lifts         def_sts    = map (liftedAltToState state) def_lifts'@@ -398,51 +399,51 @@   -- Stack Dependent Rules    -- Rule Update Frame Create Thunk-  | Stack frames                         <- stack-  , Evaluate (Atom (VarAtom var)) locals <- code+  | Evaluate (Atom (VarAtom var)) locals <- code   , Just (addr, hobj)       <- vlookupHeap var locals globals heap   , FunObj [] expr fun_locs <- hobj = -- Thunk form.-       Just (RuleUpdateCThunk-            ,[state { state_stack = Stack (UpdateFrame addr : frames)+    let frame = UpdateFrame addr+    in Just (RuleUpdateCThunk+            ,[state { state_stack = pushStack frame stack                     , state_heap  = insertHeap addr Blackhole heap                     , state_code  = Evaluate expr fun_locs }])    -- Rule Update Frame Delete Lit-  | Stack (UpdateFrame frm_addr : rest) <- stack+  | Just (UpdateFrame frm_addr, stack') <- popStack stack   , Return (LitVal lit)                 <- code =        Just (RuleUpdateDLit-            ,[state { state_stack = Stack rest+            ,[state { state_stack = stack'                     , state_heap  = insertHeap frm_addr (LitObj lit) heap                     , state_code  = Return (LitVal lit) }])    -- Rule Update Frame Delete Val Pointer-  | Stack (UpdateFrame frm_addr : rest) <- stack+  | Just (UpdateFrame frm_addr, stack') <- popStack stack   , Return (MemVal addr)                <- code   , Just hobj <- lookupHeap addr heap   , isHeapValueForm hobj =        Just (RuleUpdateDValPtr-            ,[state { state_stack = Stack rest-                    , state_heap  = insertHeap frm_addr hobj heap+            ,[state { state_stack = stack'+                    , state_heap  = insertHeap frm_addr (AddrObj addr) heap                     , state_code  = Return (MemVal addr) }])    -- Rule Case Frame Create Case Non LitVal or MemVal-  | Stack frames                          <- stack-  , Evaluate (Case mxpr cvar alts) locals <- code+  | Evaluate (Case mxpr cvar alts) locals <- code   , not (isExprValueForm mxpr locals globals heap) =-       Just (RuleCaseCCaseNonVal-            ,[state { state_stack = Stack (CaseFrame cvar alts locals : frames)+    let frame = CaseFrame cvar alts locals+    in Just (RuleCaseCCaseNonVal+            ,[state { state_stack = pushStack frame stack                     , state_code  = Evaluate mxpr locals }])      -- Rule Case Frame Delete Lit-  | Stack (CaseFrame cvar alts frm_locs : rest) <- stack+  | Just (CaseFrame cvar alts frm_locs, stack') <- popStack stack   , Return (LitVal lit)                         <- code =     let mxpr = Atom (LitAtom lit)     in Just (RuleCaseDLit-            ,[state { state_stack = Stack rest+            ,[state { state_stack = stack'                     , state_code  = Evaluate (Case mxpr cvar alts) frm_locs }])    -- Rule Case Frame Delete Heap Value-  | Stack (CaseFrame cvar alts frm_locs : rest) <- stack+  | Just (CaseFrame cvar alts frm_locs, stack') <- popStack stack   , Return (MemVal addr)                        <- code   , Just hobj <- lookupHeap addr heap   , isHeapValueForm hobj =@@ -451,37 +452,37 @@         mxpr      = Atom (VarAtom vvar)         frm_locs' = insertLocals vvar (MemVal addr) frm_locs     in Just (RuleCaseDValPtr-            ,[state { state_stack = Stack rest+            ,[state { state_stack = stack'                     , state_code  = Evaluate (Case mxpr cvar alts) frm_locs'                     , state_names = vname : confs }])    -- Rule Apply Frame Create Function Thunk-  | Stack frames                      <- stack-  , Evaluate (FunApp fun args) locals <- code+  | Evaluate (FunApp fun args) locals <- code   , Just (_, hobj)          <- vlookupHeap fun locals globals heap   , FunObj [] expr fun_locs <- hobj =-       Just (RuleApplyCFunThunk-            ,[state { state_stack = Stack (ApplyFrame args locals : frames)+    let frame = ApplyFrame args locals+    in Just (RuleApplyCFunThunk+            ,[state { state_stack = pushStack frame stack                     , state_code  = Evaluate expr fun_locs }])    -- Rule Apply Frame Create Function Over Application-  | Stack frames                      <- stack-  , Evaluate (FunApp fun args) locals <- code+  | Evaluate (FunApp fun args) locals <- code   , Just (_, hobj)              <- vlookupHeap fun locals globals heap   , FunObj params expr fun_locs <- hobj-  , (_, Right ex_as)            <- unevenZip params args =+  , (_, Right ex_args)          <- unevenZip params args =     let pass_in   = LiftAct args locals globals heap confs         LiftAct vals locals' globals' heap' confs' = liftAtomList pass_in         fun_locs' = insertLocalsList (zip params vals) fun_locs+        frame     = ApplyFrame ex_args locals'     in Just (RuleApplyCFunAppOver-            ,[state { state_stack   = Stack (ApplyFrame ex_as locals' : frames)+            ,[state { state_stack   = pushStack frame stack                     , state_heap    = heap'                     , state_globals = globals'                     , state_code    = Evaluate expr fun_locs'                     , state_names   = confs' }])    -- Rule Apply Frame Delete ReturnPtr Function-  | Stack (ApplyFrame args frm_locs : rest) <- stack+  | Just (ApplyFrame args frm_locs, stack') <- popStack stack   , Return (MemVal addr)                    <- code   , Just hobj    <- lookupHeap addr heap   , FunObj _ _ _ <- hobj@@ -490,12 +491,12 @@         fvar      = Var fname ftype         frm_locs' = insertLocals fvar (MemVal addr) frm_locs     in Just (RuleApplyDReturnFun-            ,[state { state_stack = Stack rest+            ,[state { state_stack = stack'                     , state_code  = Evaluate (FunApp fvar args) frm_locs'                     , state_names = fname : confs }])    -- Rule Apply Frame Delete ReturnPtr Sym-  | Stack (ApplyFrame args frm_locs : rest) <- stack+  | Just (ApplyFrame args frm_locs, stack') <- popStack stack   , Return (MemVal addr)                    <- code   , Just hobj             <- lookupHeap addr heap   , SymObj (Symbol sym _) <- hobj =@@ -503,7 +504,7 @@         svar      = Var sname (varType sym)         frm_locs' = insertLocals svar (MemVal addr) frm_locs     in Just (RuleApplyDReturnSym-            ,[state { state_stack = Stack rest+            ,[state { state_stack = stack'                     , state_code  = Evaluate (FunApp svar args) frm_locs'                     , state_names = sname : confs }]) 

@@ -1,6 +1,71 @@ -- | Symbolic STG Execution Support Architecture module SSTG.Core.Execution.Support-    ( module SSTG.Core.Execution.Support+    ( SymbolicT(..)+    , fmap+    , pure+    , (<*>)+    , return+    , (>>=)++    , State(..)+    , Symbol(..)+    , Status(..)+    , Stack+    , Frame(..)+    , MemAddr+    , Value(..)+    , Locals+    , Heap+    , HeapObj(..)+    , Globals+    , Code(..)+    , PathCons+    , Constraint(..)+    , SymLinks++    , nameOccStr+    , nameUnique+    , varName+    , nullAddr+    , addrInt++    , emptyStack+    , popStack+    , pushStack+    , stackToList++    , emptyLocals+    , lookupLocals+    , insertLocals+    , insertLocalsList+    , localsToList++    , emptyHeap+    , lookupHeap+    , allocHeap+    , allocHeapList+    , insertHeap+    , insertHeapList+    , heapToList++    , emptyGlobals+    , lookupGlobals+    , insertGlobals+    , insertGlobalsList+    , globalsToList++    , emptyPathCons+    , insertPathCons+    , insertPathConsList+    , pathconsToList++    , emptySymLinks+    , insertSymLinks+    , symlinksToList++    , lookupValue+    , vlookupHeap+    , memAddrType     ) where  import SSTG.Core.Syntax@@ -54,7 +119,7 @@  -- | Frames of a stack. data Frame = CaseFrame   Var [Alt] Locals-           | ApplyFrame  [Atom]    Locals+           | ApplyFrame  [Atom] Locals            | UpdateFrame MemAddr            deriving (Show, Eq, Read) @@ -77,10 +142,11 @@ 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+data HeapObj = LitObj  Lit+             | SymObj  Symbol+             | ConObj  DataCon [Value]+             | FunObj  [Var] Expr Locals+             | AddrObj MemAddr              | Blackhole              deriving (Show, Eq, Read) @@ -95,12 +161,12 @@           | Return   Value           deriving (Show, Eq, Read) --- | Path constraints.-type PathCons = [PathCond]+-- | Path constraints are the conjunctive normal form of `Constraint`s.+newtype PathCons = PathCons [Constraint] deriving (Show, Eq, Read) --- | Path conditions denote logical paths taken in program execution thus far.-data PathCond = PathCond (AltCon, [Var]) Expr Locals Bool-              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)  -- | Symbolic link tables helps keep track of what names went to what, what? newtype SymLinks = SymLinks (M.Map Name Name) deriving (Show, Eq, Read)@@ -111,7 +177,7 @@ nameOccStr :: Name -> String nameOccStr (Name occ _ _ _) = occ --- | Name's unique `Int` key.+-- | `Name` imique `Int`. nameUnique :: Name -> Int nameUnique (Name _ _ _ unq) = unq @@ -119,10 +185,35 @@ varName :: Var -> Name varName (Var name _) = name +-- | Null `MemAddr`.+nullAddr :: MemAddr+nullAddr = MemAddr 0+ -- | `MemAddr`'s `Int` value.-memAddrInt :: MemAddr -> Int-memAddrInt (MemAddr int) = int+addrInt :: MemAddr -> Int+addrInt (MemAddr int) = int +-- | Empty `Stack.+emptyStack :: Stack+emptyStack = Stack []++-- | `Stack` pop.+popStack :: Stack -> Maybe (Frame, Stack)+popStack (Stack [])     = Nothing+popStack (Stack (f:fs)) = Just (f, Stack fs)++-- | `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`.+emptyLocals :: Locals+emptyLocals = Locals M.empty+ -- | `Locals` lookup. lookupLocals :: Var -> Locals -> Maybe Value lookupLocals var (Locals lmap) = M.lookup (varName var) lmap@@ -138,14 +229,24 @@ insertLocalsList ((var, val):vvs) locals = insertLocalsList vvs locals'   where locals' = insertLocals var val locals +-- | `Locals` to key value pairs.+localsToList :: Locals -> [(Name, Value)]+localsToList (Locals lmap) = M.toList lmap++-- | Empty `Heap`.+emptyHeap :: Heap+emptyHeap = Heap M.empty (MemAddr 0)+ -- | `Heap` lookup. lookupHeap :: MemAddr -> Heap -> Maybe HeapObj-lookupHeap addr (Heap hmap _) = M.lookup addr hmap+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 ((memAddrInt prev) + 1)+  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@@ -167,6 +268,14 @@ insertHeapList ((addr, hobj):ahs) heap = insertHeapList ahs heap'   where heap' = insertHeap addr hobj heap +-- | `Heap` to key value pairs.+heapToList :: Heap -> [(MemAddr, HeapObj)]+heapToList (Heap hmap _) = M.toList hmap++-- | Empty `Globals`.+emptyGlobals :: Globals+emptyGlobals = Globals M.empty+ -- | `Globals` lookup. lookupGlobals :: Var -> Globals -> Maybe Value lookupGlobals var (Globals gmap) = M.lookup (varName var) gmap@@ -184,13 +293,45 @@ insertGlobalsList ((var, val):vvs) globals = insertGlobalsList vvs globals'   where globals' = insertGlobals var val globals +-- | `Globals` to key value pairs.+globalsToList :: Globals -> [(Name, Value)]+globalsToList (Globals gmap) = M.toList gmap++-- | Empty `PathCons`.+emptyPathCons :: PathCons+emptyPathCons = PathCons []++-- | `PathCons` insertion.+insertPathCons :: Constraint -> PathCons -> PathCons+insertPathCons cons (PathCons pcs) = PathCons (cons : pcs)++-- | 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++-- | Empty `SymLinks`.+emptySymLinks :: SymLinks+emptySymLinks = SymLinks M.empty++-- | `SymLinks` insertion.+insertSymLinks :: Name -> Name -> SymLinks -> SymLinks+insertSymLinks old new (SymLinks smap) = SymLinks (M.insert old new smap)++-- | `SymLinks` to list of key value pairs.+symlinksToList :: SymLinks -> [(Name, Name)]+symlinksToList (SymLinks smap) = M.toList smap+ --   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-    mb_val  -> mb_val+    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)@@ -204,10 +345,11 @@ memAddrType :: MemAddr -> Heap -> Maybe Type memAddrType addr heap = do     hobj <- lookupHeap addr heap-    Just $ case hobj of-        Blackhole           -> Bottom-        LitObj lit          -> litType lit-        SymObj (Symbol s _) -> varType s-        ConObj dcon _       -> dataConType dcon-        FunObj prms expr _  -> foldr FunTy (exprType expr) (map varType prms)+    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 

@@ -14,7 +14,6 @@ type Binding  = GenBinding  Name Var type BindRhs  = GenBindRhs  Name Var -type ConTag   = GenConTag   Name type DataCon  = GenDataCon  Name type Type     = GenType     Name type TyBinder = GenTyBinder Name@@ -47,18 +46,18 @@ -- 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)-                    | MachWord   Int      (GenType bnd)-                    | MachFloat  Rational (GenType bnd)-                    | MachDouble Rational (GenType bnd)-                    | MachNullAddr        (GenType bnd)-                    | MachLabel  String   (Maybe Int) (GenType bnd)+data GenLit bnd var = MachChar     Char (GenType bnd)+                    | MachStr      String (GenType bnd)+                    | MachInt      Int (GenType bnd)+                    | MachWord     Int (GenType bnd)+                    | MachFloat    Rational (GenType bnd)+                    | MachDouble   Rational (GenType bnd)+                    | MachNullAddr (GenType bnd)+                    | MachLabel    String (Maybe Int) (GenType bnd)                     | BlankAddr-                    | AddrLit    Int-                    | SymLit     var-                    | SymLitEval (GenPrimFun bnd var) [GenLit bnd var]+                    | AddrLit      Int+                    | SymLit       var+                    | SymLitEval   (GenPrimFun bnd var) [GenLit bnd var]                     deriving (Show, Eq, Read)  -- | Atomic objects. `VarAtom` may be used for variable lookups, while@@ -72,10 +71,10 @@  -- | 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]-                     | FunApp  var                   [GenAtom bnd var]-                     | Let     (GenBinding bnd var)  (GenExpr bnd var)+                     | PrimApp (GenPrimFun bnd var) [GenAtom bnd var]+                     | ConApp  (GenDataCon bnd) [GenAtom bnd var]+                     | FunApp  var [GenAtom bnd var]+                     | Let     (GenBinding bnd var) (GenExpr bnd var)                      | Case    (GenExpr bnd var) var [GenAlt bnd var]                      deriving (Show, Eq, Read) @@ -100,34 +99,31 @@ -- | `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)+                        | FunForm [var] (GenExpr bnd var)                         deriving (Show, Eq, Read) --- | Data Constructor tag that uniquely identifiers data constructors.-data GenConTag bnd = ConTag bnd Int deriving (Show, Eq, Read)- -- | 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]+data GenDataCon bnd = DataCon bnd (GenType bnd) [GenType bnd]                     deriving (Show, Eq, Read)  -- | 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)+data GenType bnd = TyVarTy    bnd (GenType bnd)+                 | AppTy      (GenType bnd) (GenType bnd)                  | ForAllTy   (GenTyBinder bnd) (GenType bnd)-                 | CastTy     (GenType bnd)     (GenCoercion bnd)-                 | TyConApp   (GenTyCon bnd)    [GenType bnd]+                 | CastTy     (GenType bnd) (GenCoercion bnd)+                 | TyConApp   (GenTyCon bnd) [GenType bnd]                  | CoercionTy (GenCoercion bnd)                  | LitTy      TyLit-                 | FunTy      (GenType bnd)     (GenType bnd)+                 | FunTy      (GenType bnd) (GenType bnd)                  | Bottom                  deriving (Show, Eq, Read)  -- | Type binder for `ForAllTy`. data GenTyBinder bnd = NamedTyBndr bnd (GenType bnd)-                     | AnonTyBndr      (GenType bnd)+                     | AnonTyBndr  (GenType bnd)                      deriving (Show, Eq, Read)  -- | `Type` literal.@@ -151,8 +147,8 @@  -- | ADT RHS. data GenAlgTyRhs bnd = AbstractTyCon Bool-                     | DataTyCon     [GenConTag bnd]-                     | TupleTyCon    (GenConTag bnd)-                     | NewTyCon      (GenConTag bnd)+                     | DataTyCon     [bnd]+                     | NewTyCon      bnd+                     | TupleTyCon    bnd                      deriving (Show, Eq, Read) 

@@ -146,16 +146,14 @@   MachNullAddr      -> SL.MachNullAddr ((mkType . literalType) lit)   (MachLabel f m _) -> SL.MachLabel (unpackFS f) m ((mkType . literalType) lit) --- | Make SSTG `ConTag`.-mkDataTag :: DataCon -> SL.ConTag-mkDataTag datacon = SL.ConTag name tag-  where name = (mkName . dataConName) datacon-        tag  = dataConTag datacon+-- | `DataCon`'s `Name`.+mkDataName :: DataCon -> SL.Name+mkDataName datacon = (mkName. dataConName) datacon  -- | Make SSTG `DataCon`. mkData :: DataCon -> SL.DataCon-mkData datacon = SL.DataCon dcid ty args-  where dcid = mkDataTag datacon+mkData datacon = SL.DataCon name ty args+  where name = mkDataName datacon         ty   = (mkType . dataConRepType) datacon         args = map mkType (dataConOrigArgTys datacon) @@ -205,10 +203,10 @@  -- | 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)+mkAlgTyConRhs (AbstractTyCon b)            = SL.AbstractTyCon b+mkAlgTyConRhs (DataTyCon {data_cons = ds}) = SL.DataTyCon  (map mkDataName ds)+mkAlgTyConRhs (TupleTyCon {data_con = d})  = SL.TupleTyCon (mkDataName d)+mkAlgTyConRhs (NewTyCon {data_con = d})    = SL.NewTyCon   (mkDataName d)  -- | make SSTG `TyBinder`. mkTyBndr :: TyBinder -> SL.TyBinder

@@ -7,7 +7,6 @@  import SSTG.Core -import qualified Data.Map  as M import qualified Data.List as L  -- | Print `LiveState` and `DeadState` that yield from execution snapshots.@@ -50,8 +49,8 @@         globals_str = (pprGlobalsStr  . state_globals) state         expr_str    = (pprCodeStr     . state_code)    state         names_str   = (pprNamesStr    . state_names)   state-        pcons_str   = (pprPConsStr    . state_paths)   state-        links_str   = (pprLinksStr    . state_links)   state+        pcons_str   = (pprPathConsStr . state_paths)   state+        links_str   = (pprSymLinksStr . state_links)   state         acc_strs    = [ ">>>>> [State] >>>>>>>>>>>>>>>"                       , status_str                       , "----- [Stack] ---------------"@@ -102,7 +101,7 @@  -- | Print `MemAddr`. pprMemAddrStr :: MemAddr -> String-pprMemAddrStr (MemAddr int) = show int+pprMemAddrStr addr = show (addrInt addr)  -- | Print `Name`. pprNameStr :: Name -> String@@ -118,8 +117,8 @@  -- | Print `Stack`. pprStackStr :: Stack -> String-pprStackStr (Stack stack) = injNewLineSeps10 acc_strs-  where frame_strs = map pprFrameStr stack+pprStackStr stack = injNewLineSeps10 acc_strs+  where frame_strs = map pprFrameStr (stackToList stack)         acc_strs   = "Stack" : frame_strs  -- | Print `Frame`.@@ -152,6 +151,7 @@ -- | Print `HeapObj`. pprHeapObjStr :: HeapObj -> String pprHeapObjStr (Blackhole) = "Blackhole!!!"+pprHeapObjStr (AddrObj addr) = pprMemAddrStr addr pprHeapObjStr (LitObj lit) = injSpace acc_strs   where header   = "LitObj"         lit_str  = pprLitStr lit@@ -175,32 +175,30 @@  -- | Print `Heap`. pprHeapStr :: Heap -> String-pprHeapStr (Heap hmap addr) = injNewLine (map (\k -> ">" ++ k) acc_strs)-  where kvs  = M.toList hmap-        addr_strs = map (pprMemAddrStr . fst) kvs-        hobj_strs = map (pprHeapObjStr . snd) kvs+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-        addr_str  = pprMemAddrStr addr-        kvs_strs  = map (\(m, o) -> sub (m ++ "," ++ o)) zipd_strs-        acc_strs  = addr_str : kvs_strs+        acc_strs  = map (\(m, o) -> sub (m ++ ", " ++ o)) zipd_strs  -- | Print `Globals`. pprGlobalsStr :: Globals -> String-pprGlobalsStr (Globals gmap) = injNewLine (map (\k -> ">" ++ k) acc_strs)-  where kvs  = M.toList gmap-        name_strs = map (pprNameStr . fst) kvs-        val_strs  = map (pprValueStr . snd) kvs+pprGlobalsStr globals = injNewLine acc_strs+  where glist     = globalsToList globals+        name_strs = map (pprNameStr . fst) glist+        val_strs  = map (pprValueStr . snd) glist         zipd_strs = zip name_strs val_strs-        acc_strs  = map (\(n, v) -> sub (n ++ "," ++ v)) zipd_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-        name_strs = map (pprNameStr . fst) kvs-        val_strs  = map (pprValueStr . snd) kvs+pprLocalsStr locals = injIntoList acc_strs+  where llist     = localsToList locals+        name_strs = map (pprNameStr . fst) llist+        val_strs  = map (pprValueStr . snd) llist         zipd_strs = zip name_strs val_strs-        acc_strs  = map (\(n, v) -> sub (n ++ "," ++ v)) zipd_strs+        acc_strs  = map (\(n, v) -> sub (n ++ ", " ++ v)) zipd_strs  -- | Print `Value`. pprValueStr :: Value -> String@@ -232,15 +230,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+pprDataConStr (DataCon name ty tys) = injSpace acc_strs   where header   = "DataCon"-        tag_str  = (sub . pprConTagStr) tag+        tag_str  = (sub . pprNameStr) name         ty_str   = (sub . pprTypeStr) ty         tys_str  = injIntoList (map pprTypeStr tys)         acc_strs = [header, tag_str, ty_str, tys_str]@@ -360,23 +354,23 @@ pprNamesStr names = injIntoList (map pprNameStr names)  -- | Print `PathCons`.-pprPConsStr :: PathCons -> String-pprPConsStr pathcons = injNewLineSeps5 strs-  where strs = map pprPCondStr pathcons+pprPathConsStr :: PathCons -> String+pprPathConsStr pathcons = injNewLineSeps5 strs+  where strs = map pprConstraintStr (pathconsToList pathcons)  -- | Print `PathCond`.-pprPCondStr :: PathCond -> String-pprPCondStr (PathCond (acon, params) expr locals hold) = injIntoList acc_strs-  where acon_str = pprAltConStr acon-        prms_str = injIntoList (map pprVarStr params)+pprConstraintStr :: Constraint -> String+pprConstraintStr (Constraint (ac, ps) expr locals hold) = injIntoList acc_strs+  where acon_str = pprAltConStr ac+        prms_str = injIntoList (map pprVarStr ps)         expr_str = pprExprStr expr         locs_str = pprLocalsStr locals         hold_str = case hold of { True -> "Positive"; False -> "Negative" }         acc_strs = [acon_str, prms_str, expr_str, locs_str, hold_str]  -- | 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+pprSymLinksStr :: SymLinks -> String+pprSymLinksStr symlinks = injNewLineSeps5 acc_strs+  where slist    = symlinksToList symlinks+        acc_strs = map (\(k, v) -> pprNameStr k ++ ", " ++  pprNameStr v) slist