diff --git a/SSTG.cabal b/SSTG.cabal --- a/SSTG.cabal +++ b/SSTG.cabal @@ -1,5 +1,5 @@ name: SSTG -version: 0.1.1.2 +version: 0.1.1.3 synopsis: STG Symbolic Execution description: Prototype of STG-based Symbolic Execution for Haskell. homepage: https://github.com/AntonXue/SSTG#readme @@ -17,17 +17,21 @@ hs-source-dirs: src exposed-modules: SSTG , SSTG.Core - , SSTG.Core.Translation - , SSTG.Core.Translation.Haskell , SSTG.Core.Language + , SSTG.Core.Language.Naming + , SSTG.Core.Language.Support , SSTG.Core.Language.Syntax , SSTG.Core.Language.Typing + , SSTG.Core.Preprocessing + , SSTG.Core.Preprocessing.Defunctionalization + , SSTG.Core.SMT + , SSTG.Core.SMT.Syntax + , SSTG.Core.Translation + , SSTG.Core.Translation.Haskell , SSTG.Core.Execution , SSTG.Core.Execution.Engine - , SSTG.Core.Execution.Naming , SSTG.Core.Execution.Rules , SSTG.Core.Execution.Stepping - , SSTG.Core.Execution.Support , SSTG.Utils , SSTG.Utils.Printing , SSTG.Utils.FileIO diff --git a/src/SSTG/Core.hs b/src/SSTG/Core.hs --- a/src/SSTG/Core.hs +++ b/src/SSTG/Core.hs @@ -2,10 +2,14 @@ module SSTG.Core ( module SSTG.Core.Execution , module SSTG.Core.Language + , module SSTG.Core.Preprocessing + , module SSTG.Core.SMT , module SSTG.Core.Translation ) where import SSTG.Core.Execution import SSTG.Core.Language +import SSTG.Core.Preprocessing +import SSTG.Core.SMT import SSTG.Core.Translation diff --git a/src/SSTG/Core/Execution.hs b/src/SSTG/Core/Execution.hs --- a/src/SSTG/Core/Execution.hs +++ b/src/SSTG/Core/Execution.hs @@ -1,15 +1,11 @@ -- | Export Module for SSTG.Core.Execution module SSTG.Core.Execution ( module SSTG.Core.Execution.Engine - , module SSTG.Core.Execution.Naming , 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.Naming import SSTG.Core.Execution.Rules import SSTG.Core.Execution.Stepping -import SSTG.Core.Execution.Support diff --git a/src/SSTG/Core/Execution/Engine.hs b/src/SSTG/Core/Execution/Engine.hs --- a/src/SSTG/Core/Execution/Engine.hs +++ b/src/SSTG/Core/Execution/Engine.hs @@ -10,12 +10,10 @@ ) where import SSTG.Core.Language -import SSTG.Core.Execution.Naming import SSTG.Core.Execution.Stepping -import SSTG.Core.Execution.Support -- | Load Result -data LoadResult = LoadOkay State +data LoadResult = LoadOkay State | LoadGuess State [Bind] | LoadError String deriving (Show, Eq, Read) @@ -24,100 +22,107 @@ -- experimental results. loadState :: Program -> LoadResult loadState prog = loadStateEntry main_occ_name prog - where main_occ_name = "main" -- Based on a few experimental programs. + where + main_occ_name = "main" -- Based on a few experimental programs. -- | Load from a specified entry point. loadStateEntry :: String -> Program -> LoadResult loadStateEntry entry (Program bnds) = if length matches == 0 then LoadError ("No entry candidates found for: [" ++ entry ++ "]") else if length others == 0 - then LoadOkay state + then LoadOkay state else LoadGuess state (map fst others) - where -- Status or something. - status = Status { status_id = 1 - , status_parent_id = 0 - , status_steps = 0 } - -- Stack initialized to empty. - 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 - globals0 = insertGlobalsList glist empty_globals - (heap2, localss) = liftBinds bnd_addrss globals0 heap1 - bnd_locs = zip bnds 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 - (code, globals, heap) = loadCode tgt_var tgt_rhs tgt_loc globals0 heap2 - -- Ready to fill the state. - state0 = State { state_status = status - , state_stack = stack - , state_heap = heap - , state_globals = globals - , state_code = code - , state_names = [] - , state_paths = empty_pathcons } + where + -- Status or something. + status = init_status + -- Stack initialized to empty. + 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 + globals0 = insertGlobalsList glist empty_globals + (heap2, localss) = liftBinds bnd_addrss globals0 heap1 + bnd_locs = zip bnds 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 + (code, globals, heap) = loadCode tgt_var tgt_rhs tgt_loc globals0 heap2 + -- Ready to fill the state. + state0 = State { state_status = status + , state_stack = stack + , state_heap = heap + , state_globals = globals + , state_code = code + , state_names = [] + , state_paths = empty_pathcons } - -- Gather information on all variables. - state = state0 { state_names = allNames state0 } + -- Gather information on all variables. + state = state0 { state_names = allNames state0 } -- | Allocate Bind allocBind :: Bind -> Heap -> (Heap, [MemAddr]) allocBind (Bind _ pairs) heap = (heap', addrs) - where hfakes = map (const Blackhole) pairs - (heap', addrs) = allocHeapList hfakes heap + where + hfakes = map (const Blackhole) pairs + (heap', addrs) = allocHeapList hfakes heap -- | Allocate List of `Bind`s allocBindList :: [Bind] -> Heap -> (Heap, [[MemAddr]]) -allocBindList [] heap = (heap, []) +allocBindList [] heap = (heap, []) allocBindList (b:bs) heap = (heapf, addrs : as) - where (heap', addrs) = allocBind b heap - (heapf, as) = allocBindList bs heap' + where + (heap', addrs) = allocBind b heap + (heapf, as) = allocBindList bs heap' -- | Bind Address to Name Values bndAddrsToVarVals :: (Bind, [MemAddr]) -> [(Var, Value)] bndAddrsToVarVals (Bind _ rhss, addrs) = zip (map fst rhss) mem_vals - where mem_vals = map (\a -> MemVal a) addrs + 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) - where (heap', addrss) = allocBindList bnds heap - bnd_addrss = zip bnds addrss - var_vals = concatMap bndAddrsToVarVals bnd_addrss + where + (heap', addrss) = allocBindList bnds heap + bnd_addrss = zip bnds addrss + var_vals = concatMap bndAddrsToVarVals bnd_addrss -- | Force Atom Lookup forceLookupValue :: Atom -> Locals -> Globals -> Value -forceLookupValue (LitAtom lit) _ _ = LitVal lit +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. + Nothing -> LitVal BlankAddr -- An error, but I want to not crash. Just val -> val -- | Full Rhs Object forceRhsObj :: BindRhs -> Locals -> Globals -> HeapObj -forceRhsObj (FunForm prms expr) locals _ = FunObj prms expr locals +forceRhsObj (FunForm prms expr) locals _ = FunObj prms expr locals forceRhsObj (ConForm dcon args) locals globals = ConObj dcon arg_vals - where arg_vals = map (\a -> forceLookupValue a locals globals) args + 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) - where (vars, rhss) = unzip pairs - 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 + where + (vars, rhss) = unzip pairs + 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 -- | Lift Bind List liftBinds :: [(Bind, [MemAddr])] -> Globals -> Heap -> (Heap, [Locals]) -liftBinds [] _ heap = (heap, []) +liftBinds [] _ heap = (heap, []) liftBinds (bm:bms) globals heap = (heapf, locals : ls) - where (heap', locals) = liftBind bm globals heap - (heapf, ls) = liftBinds bms globals heap' + where + (heap', locals) = liftBind bm globals heap + (heapf, ls) = liftBinds bms globals heap' -- | Return a sub-list of binds in which the entry candidate appears. entryMatches :: String -> [(Bind, Locals)] -> [(Bind, Locals)] @@ -134,28 +139,30 @@ -- | Load Code loadCode :: Var -> BindRhs -> Locals -> Globals -> Heap -> (Code,Globals,Heap) -loadCode ent (ConForm _ _) locals globals heap = (code, globals, heap) - where code = Evaluate (Atom (VarAtom ent)) locals +loadCode ent (ConForm _ _) locals globals heap = (code, globals, heap) + where + code = Evaluate (Atom (VarAtom ent)) locals loadCode ent (FunForm params expr) locals globals heap = (code, globals, heap') - where actuals = traceArgs params expr locals globals heap - confs = map varName actuals - names' = freshSeededNameList confs confs - adjusted = map (\(n, t) -> Var n t) (zip names' (map varType actuals)) - -- Throw the parameters on heap as symbolic objects - sym_objs = map (\p -> SymObj (Symbol p Nothing)) adjusted - (heap', addrs) = allocHeapList sym_objs heap - -- make Atom representations for arguments and shove into locals. - mem_vals = map (\a -> MemVal a) addrs - locals' = insertLocalsList (zip adjusted mem_vals) locals - args = map (\p -> VarAtom p) adjusted - -- Set up code - code = Evaluate (FunApp ent args) locals' + where + actuals = traceArgs params expr locals globals heap + confs = map varName actuals + names' = freshSeededNameList confs confs + adjusted = map (\(n, t) -> Var n t) (zip names' (map varType actuals)) + -- Throw the parameters on heap as symbolic objects + sym_objs = map (\p -> SymObj (Symbol p Nothing)) adjusted + (heap', addrs) = allocHeapList sym_objs heap + -- make Atom representations for arguments and shove into locals. + mem_vals = map (\a -> MemVal a) addrs + locals' = insertLocalsList (zip adjusted mem_vals) locals + args = map (\p -> VarAtom p) adjusted + -- Set up code + code = Evaluate (FunApp ent args) locals' -- | We need to do stupid tracing if it's THUNK'D by default >:( traceArgs :: [Var] -> Expr -> Locals -> Globals -> Heap -> [Var] traceArgs base expr locals globals heap - | FunApp var [] <- expr - , Just (_, hobj) <- vlookupHeap var locals globals heap + | FunApp var [] <- expr + , Just (_, hobj) <- vlookupHeap var locals globals heap , FunObj params _ _ <- hobj , length params > 0 , length base == 0 = params @@ -164,8 +171,8 @@ -- | Run flags. data RunFlags = RunFlags { flag_step_count :: Int - , flag_step_type :: StepType - , flag_dump_dir :: Maybe FilePath + , flag_step_type :: StepType + , flag_dump_dir :: Maybe FilePath } deriving (Show, Eq, Read) -- | Step execution type. @@ -174,15 +181,16 @@ -- | Perform execution on a `State` given the run flags. execute :: RunFlags -> State -> [([LiveState], [DeadState])] execute flags state = step (flag_step_count flags) state - where step :: Int -> State -> [([LiveState], [DeadState])] - step = case flag_step_type flags of - BFS -> \k s -> [runBoundedBFS k s] - BFSLogged -> runBoundedBFSLogged - DFS -> \k s -> [runBoundedDFS k s] - DFSLogged -> runBoundedDFSLogged + where + step :: Int -> State -> [([LiveState], [DeadState])] + step = case flag_step_type flags of + BFS -> \k s -> [runBoundedBFS k s] + BFSLogged -> runBoundedBFSLogged + DFS -> \k s -> [runBoundedDFS k s] + DFSLogged -> runBoundedDFSLogged -- | Simple `BFS` based execution on a state. execute1 :: Int -> State -> ([LiveState], [DeadState]) -execute1 n state | n < 1 = ([([], state)], []) +execute1 n state | n < 1 = ([([], state)], []) | otherwise = runBoundedBFS n state diff --git a/src/SSTG/Core/Execution/Naming.hs b/src/SSTG/Core/Execution/Naming.hs deleted file mode 100644 --- a/src/SSTG/Core/Execution/Naming.hs +++ /dev/null @@ -1,209 +0,0 @@ --- | Naming Module -module SSTG.Core.Execution.Naming - ( allNames - , freshString - , freshName - , freshSeededName - , freshNameList - , freshSeededNameList - ) where - -import SSTG.Core.Language -import SSTG.Core.Execution.Support - -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) - --- | `Name`s in the `Heap`. -heapNames :: Heap -> [Name] -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 -heapObjNames (ConObj dcon _) = dataNames dcon -heapObjNames (FunObj ps expr locs) = exprNames expr ++ localsNames locs - ++ concatMap varNames ps - --- | `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 `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 (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 a `PrimFun`. -pfunNames :: PrimFun -> [Name] -pfunNames (PrimFun n ty) = n : typeNames ty - --- | `Name`s in a `DataCon`. -dataNames :: DataCon -> [Name] -dataNames (DataCon n ty tys) = n : concatMap typeNames (ty : tys) - --- | `Name`s in a `TyBinder`. -tyBinderNames :: TyBinder -> [Name] -tyBinderNames (AnonTyBndr) = [] -tyBinderNames (NamedTyBndr n) = [n] - --- | `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 - --- | `Name`s in a `Coercion`. -coercionNames :: Coercion -> [Name] -coercionNames (Coercion t1 t2) = typeNames t1 ++ typeNames t2 - --- | `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 - --- | `Name`s in a `PathCons`. -pconsNames :: PathCons -> [Name] -pconsNames pathcons = concatMap constraintNames (pathconsToList pathcons) - --- | `Name`s in a `PathCons`. -constraintNames :: Constraint -> [Name] -constraintNames (Constraint (_, vs) e locs _) = exprNames e ++ localsNames locs - ++ map varName vs - --- | Create a fresh seed given any `Int`, a `String` seed, and a `Set` of --- `String`s that we do not want our new `String` to conflict with. The sole --- purpose of the `Int` seed is to allow us tell us how much to multiply some --- prime number to "orbit" an index around a fixed list of acceptable `Char`s. -freshString :: Int -> String -> S.Set String -> String -freshString rand seed confs = if S.member seed confs - then freshString (rand + 1) (seed ++ [pick]) confs else seed - where pick = bank !! index - index = raw_i `mod` (length bank) - raw_i = (abs rand) * prime - prime = 151 -- The original? :) - bank = lower ++ upper ++ nums - lower = "abcdefghijlkmnopqrstuvwxyz" - upper = "ABCDEFGHIJKLMNOPQRSTUVWXYZ" - nums = "1234567890" - --- | Fresh `Name` given a list of `Name`s that acts as conflicts. The fresh --- `Name`s generated in this manner are prefixed with @"fs?"@, which is not a --- valid identifier in Haskell, but okay in SSTG. we also specify the --- `NameSpace` under which the `Name` will be generated. This will generally --- be `VarNSpace` in actual usage. -freshName :: NameSpace -> [Name] -> Name -freshName nspace confs = freshSeededName seed confs - where seed = Name "fs?" Nothing nspace 0 - --- | A fresh `Name` generated from a seed `Name`, which will act as the prefix --- of the new `Name`. We ues the same `NameSpace` as the seed `Name` when --- generating this way. -freshSeededName :: Name -> [Name] -> Name -freshSeededName seed confs = Name occ' mdl ns unq' - where Name occ mdl ns unq = seed - occ' = freshString 1 occ (S.fromList alls) - unq' = maxs + 1 - alls = map nameOccStr confs - maxs = L.maximum (unq : map nameUnique confs) - --- | Generate a list of `Name`s, each corresponding to the appropriate element --- of the `NameSpace` list. -freshNameList :: [NameSpace] -> [Name] -> [Name] -freshNameList [] _ = [] -freshNameList (nspace:nss) confs = name' : freshNameList nss confs' - where name' = freshName nspace confs - confs' = name' : confs - --- | List of seeded fresh `Name`s. -freshSeededNameList :: [Name] -> [Name] -> [Name] -freshSeededNameList [] _ = [] -freshSeededNameList (n:ns) confs = name' : freshSeededNameList ns confs' - where name' = freshSeededName n confs - confs' = name' : confs - diff --git a/src/SSTG/Core/Execution/Rules.hs b/src/SSTG/Core/Execution/Rules.hs --- a/src/SSTG/Core/Execution/Rules.hs +++ b/src/SSTG/Core/Execution/Rules.hs @@ -6,14 +6,12 @@ ) where import SSTG.Core.Language -import SSTG.Core.Execution.Naming -import SSTG.Core.Execution.Support -- | `Rule`s that are applied during STG reduction. data Rule = RuleAtomLit | RuleAtomLitPtr | RuleAtomValPtr | RuleAtomUnInt | RulePrimApp | RuleConApp - | RuleFunAppExact | RuleFunAppUnder | RuleFunAppSym + | RuleFunAppExact | RuleFunAppUnder | RuleFunAppSym | RuleFunAppConPtr | RuleFunAppUnInt | RuleLet | RuleCaseLit | RuleCaseConPtr | RuleCaseAnyLit | RuleCaseAnyConPtr @@ -25,59 +23,58 @@ | RuleCaseCCaseNonVal | RuleCaseDLit | RuleCaseDValPtr - | RuleApplyCFunThunk | RuleApplyCFunAppOver + | RuleApplyCFunThunk | RuleApplyCFunAppOver | RuleApplyDReturnFun | RuleApplyDReturnSym | RuleIdentity deriving (Show, Eq, Read, Ord) --- Stack Independent Rules +-- Stack Independent Rules -- | Does not include `LitObj`. i.e. if something points to this, we have -- nothing to do in terms of reducitons. isHeapValueForm :: HeapObj -> Bool -isHeapValueForm (SymObj _) = True -isHeapValueForm (ConObj _ _) = True +isHeapValueForm (SymObj _) = True +isHeapValueForm (ConObj _ _) = True isHeapValueForm (FunObj (_:_) _ _) = True -isHeapValueForm _ = False +isHeapValueForm _ = False -- | Either a `Lit` or points to a `Heap` value (not LitObj!). If we find -- nothing in the `Heap`, then this means we can still upcast the var to a -- symbolic that we create additional mappings to in the `Globals`. isExprValueForm :: Expr -> Locals -> Globals -> Heap -> Bool -isExprValueForm (Atom (LitAtom _)) _ _ _ = True +isExprValueForm (Atom (LitAtom _)) _ _ _ = True isExprValueForm (Atom (VarAtom var)) locals globals heap = case vlookupHeap var locals globals heap of Just (_, hobj) -> isHeapValueForm hobj - Nothing -> False -isExprValueForm _ _ _ _ = False + Nothing -> False +isExprValueForm _ _ _ _ = False -- | Is the `State` in a normal form that cannot be reduced further? isStateValueForm :: State -> Bool -isStateValueForm State { state_stack = stack - , state_heap = heap - , state_code = code } - | Nothing <- popStack stack - , Return (LitVal _) <- code = True +isStateValueForm state + | Nothing <- popStack (state_stack state) + , Return (LitVal _) <- (state_code state) = True - | Nothing <- popStack stack - , Return (MemVal addr) <- code - , Just hobj <- lookupHeap addr heap + | Nothing <- popStack (state_stack state) + , Return (MemVal addr) <- (state_code state) + , Just hobj <- lookupHeap addr (state_heap state) , isHeapValueForm hobj = True | otherwise = False -- | `Value` to `Lit`. valueToLit :: Value -> Lit -valueToLit (LitVal lit) = lit +valueToLit (LitVal lit) = lit valueToLit (MemVal addr) = AddrLit (addrInt addr) -- | Uneven `zip` of two `List`s, with the leftover stored. unevenZip :: [a] -> [b] -> ([(a, b)], Either [a] [b]) -unevenZip as [] = ([], Left as) -unevenZip [] bs = ([], Right bs) +unevenZip as [] = ([], Left as) +unevenZip [] bs = ([], Right bs) unevenZip (a:as) (b:bs) = ((a, b) : acc, excess) - where (acc, excess) = unevenZip as bs + where + (acc, excess) = unevenZip as bs -- | Lift action wrapper type. data LiftAct a = LiftAct a Locals Globals Heap [Name] @@ -85,76 +82,86 @@ -- | Lift uninterpreted `Var`s into `Globals`. liftUnInt :: LiftAct Var -> LiftAct MemAddr liftUnInt (LiftAct var locals globals heap confs) = pass_out - where sname = freshSeededName (varName var) confs - svar = Var sname (varType var) - (heap', addr) = allocHeap (SymObj (Symbol svar Nothing)) heap - globals' = insertGlobals (var, MemVal addr) globals - confs' = sname : confs - pass_out = LiftAct addr locals globals' heap' confs' + where + sname = freshSeededName (varName var) confs + svar = Var sname (varType var) + (heap', addr) = allocHeap (SymObj (Symbol svar Nothing)) heap + globals' = insertGlobals (var, MemVal addr) globals + confs' = sname : confs + pass_out = LiftAct addr locals globals' heap' confs' -- | Lift `Atom` if necessary (i.e. uinterpreted / out-of-scope). liftAtom :: LiftAct Atom -> LiftAct Value liftAtom (LiftAct atom locals globals heap confs) = pass_out - where pass_out = LiftAct aval locals globals' heap' confs' - (aval, globals', heap', confs') = case atom of - LitAtom lit -> (LitVal lit, globals, heap, confs) - VarAtom var -> case lookupValue var locals globals of - Just val -> (val, globals, heap, confs) - Nothing -> let pass_in = LiftAct var locals globals heap confs - LiftAct addr _ g' h' c' = liftUnInt pass_in - in (MemVal addr, g', h', c') + where + pass_out = LiftAct aval locals globals' heap' confs' + (aval, globals', heap', confs') = case atom of + LitAtom lit -> (LitVal lit, globals, heap, confs) + VarAtom var -> case lookupValue var locals globals of + Just val -> (val, globals, heap, confs) + Nothing -> let pass_in = LiftAct var locals globals heap confs + LiftAct addr _ g' h' c' = liftUnInt pass_in + in (MemVal addr, g', h', c') -- | Lift a list of `Atom`s. liftAtomList :: LiftAct [Atom] -> LiftAct [Value] -liftAtomList (LiftAct [] locals globals heap confs) = pass_out - where pass_out = LiftAct [] locals globals heap confs +liftAtomList (LiftAct [] locals globals heap confs) = pass_out + where + pass_out = LiftAct [] locals globals heap confs liftAtomList (LiftAct (atom:as) locals globals heap confs) = pass_out - where pass_in = LiftAct atom locals globals heap confs - pass_rest = LiftAct as locals' globals' heap' confs' - pass_out = LiftAct (val : vs) localsf globalsf heapf confsf - LiftAct val locals' globals' heap' confs' = liftAtom pass_in - LiftAct vs localsf globalsf heapf confsf = liftAtomList pass_rest + where + pass_in = LiftAct atom locals globals heap confs + pass_rest = LiftAct as locals' globals' heap' confs' + pass_out = LiftAct (val : vs) localsf globalsf heapf confsf + LiftAct val locals' globals' heap' confs' = liftAtom pass_in + LiftAct vs localsf globalsf heapf confsf = liftAtomList pass_rest -- | Lift `BindRhs`. liftBindRhs :: LiftAct BindRhs -> LiftAct HeapObj liftBindRhs (LiftAct (FunForm prms expr) locals globals heap confs) = pass_out - where pass_out = LiftAct (FunObj prms expr locals) locals globals heap confs + where + pass_out = LiftAct (FunObj prms expr locals) locals globals heap confs liftBindRhs (LiftAct (ConForm dcon args) locals globals heap confs) = pass_out - where pass_in = LiftAct args locals globals heap confs - pass_out = LiftAct (ConObj dcon vals) locals' globals' heap' confs' - LiftAct vals locals' globals' heap' confs' = liftAtomList pass_in + where + pass_in = LiftAct args locals globals heap confs + pass_out = LiftAct (ConObj dcon vals) locals' globals' heap' confs' + LiftAct vals locals' globals' heap' confs' = liftAtomList pass_in -- | Lift `BindRhs` list. liftBindRhsList :: LiftAct [BindRhs] -> LiftAct [HeapObj] -liftBindRhsList (LiftAct [] locals globals heap confs) = pass_out - where pass_out = LiftAct [] locals globals heap confs +liftBindRhsList (LiftAct [] locals globals heap confs) = pass_out + where + pass_out = LiftAct [] locals globals heap confs liftBindRhsList (LiftAct (rhs:rs) locals globals heap confs) = pass_out - where pass_in = LiftAct rhs locals globals heap confs - pass_rest = LiftAct rs locals' globals' heap' confs' - pass_out = LiftAct (hobj : hos) localsf globalsf heapf confsf - LiftAct hobj locals' globals' heap' confs' = liftBindRhs pass_in - LiftAct hos localsf globalsf heapf confsf = liftBindRhsList pass_rest + where + pass_in = LiftAct rhs locals globals heap confs + pass_rest = LiftAct rs locals' globals' heap' confs' + pass_out = LiftAct (hobj : hos) localsf globalsf heapf confsf + 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 - 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 - 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 - where hfakes = map (const Blackhole) bnd - -- 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 - pass_out = LiftAct () localsf globals' heapf confs' - LiftAct hobjs localsf globals' heap'' confs' = liftBindRhsList pass_in + 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 + 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 + where + hfakes = map (const Blackhole) bnd + -- 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 + pass_out = LiftAct () localsf globals' heapf confs' + LiftAct hobjs localsf globals' heap'' confs' = liftBindRhsList pass_in -- | `Default` `Alt` branches in a `Case`. defaultAlts :: [Alt] -> [Alt] @@ -179,59 +186,61 @@ -- | Lift `Alt`s during branching caused by symbolics. 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 - svars = map (\(p, n) -> Var n (varType p)) (zip params snames) - hobjs = map (\s -> SymObj (Symbol s Nothing)) svars - (heap', addrs) = allocHeapList hobjs heap - 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] - confs' = snames ++ confs - pass_out = LiftAct (expr, conss) locals' globals heap' confs' + where + (mvar, addr, cvar, Alt ac params expr) = args + snames = freshSeededNameList (map varName params) confs + svars = map (\(p, n) -> Var n (varType p)) (zip params snames) + hobjs = map (\s -> SymObj (Symbol s Nothing)) svars + (heap', addrs) = allocHeapList hobjs heap + 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] + confs' = snames ++ confs + pass_out = LiftAct (expr, conss) locals' globals heap' confs' -- | `Alt` closure to `State`. liftedAltToState :: State -> LiftAct (Expr, [Constraint]) -> State liftedAltToState state (LiftAct args locals globals heap confs) = state' - 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 = insertPathConsList conss pathcons } + where + (expr, conss) = args + pcons = state_paths state + state' = state { state_heap = heap + , state_globals = globals + , state_code = Evaluate expr locals + , state_names = confs + , state_paths = insertPathConsList conss pcons } -- | Reduce the state if it matches some type of reduction `Rule`. Return -- `Nothing` to denote that rule application has completely failed. reduce :: State -> Maybe (Rule, [State]) -reduce state @ State { state_stack = stack - , state_heap = heap +reduce state @ State { state_stack = stack + , state_heap = heap , state_globals = globals - , state_code = code - , state_names = confs } + , state_code = code + , state_names = confs } - -- Stack Independent Rules +-- Stack Independent Rules -- Atom Lit | Evaluate (Atom (LitAtom lit)) _ <- code = - Just (RuleAtomLit - ,[state { state_code = Return (LitVal lit) }]) + Just (RuleAtomLit + ,[state { state_code = Return (LitVal lit) }]) -- Atom Lit Pointer | Evaluate (Atom (VarAtom var)) locals <- code , Just (_, hobj) <- vlookupHeap var locals globals heap - , LitObj lit <- hobj = - Just (RuleAtomLitPtr - ,[state { state_code = Evaluate (Atom (LitAtom lit)) locals }]) + , LitObj lit <- hobj = + Just (RuleAtomLitPtr + ,[state { state_code = Evaluate (Atom (LitAtom lit)) locals }]) -- Rule Atom Val Pointer | Evaluate (Atom (VarAtom var)) locals <- code , Just (addr, hobj) <- vlookupHeap var locals globals heap , isHeapValueForm hobj = - Just (RuleAtomValPtr - ,[state { state_code = Return (MemVal addr) }]) + Just (RuleAtomValPtr + ,[state { state_code = Return (MemVal addr) }]) -- Rule Atom Uninterpreted | Evaluate (Atom (VarAtom uvar)) locals <- code @@ -239,21 +248,21 @@ let pass_in = LiftAct uvar locals globals heap confs LiftAct _ locals' globals' heap' confs' = liftUnInt pass_in in Just (RuleAtomUnInt - ,[state { state_heap = heap' + ,[state { state_heap = heap' , state_globals = globals' - , state_code = Evaluate (Atom (VarAtom uvar)) locals' - , state_names = confs' }]) + , state_code = Evaluate (Atom (VarAtom uvar)) locals' + , state_names = confs' }]) -- Prim Function App | 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 = SymLitEval pfun (map valueToLit vals) in Just (RulePrimApp - ,[state { state_heap = heap' + ,[state { state_heap = heap' , state_globals = globals' - , state_code = Evaluate (Atom (LitAtom eval)) locals' - , state_names = confs' }]) + , state_code = Evaluate (Atom (LitAtom eval)) locals' + , state_names = confs' }]) -- Rule Con App | Evaluate (ConApp dcon args) locals <- code = @@ -261,61 +270,61 @@ LiftAct vals _ globals' heap' confs' = liftAtomList pass_in (heapf, addr) = allocHeap (ConObj dcon vals) heap' in Just (RuleConApp - ,[state { state_heap = heapf + ,[state { state_heap = heapf , state_globals = globals' - , state_code = Return (MemVal addr) - , state_names = confs' }]) + , state_code = Return (MemVal addr) + , state_names = confs' }]) -- Rule Fun App Exact | Evaluate (FunApp fun args) locals <- code - , Just (_, hobj) <- vlookupHeap fun locals globals heap + , Just (_, hobj) <- vlookupHeap fun locals globals heap , FunObj params expr fun_locs <- hobj , length params == length args = - let pass_in = LiftAct args locals globals heap confs + 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 in Just (RuleFunAppExact - ,[state { state_heap = heap' + ,[state { state_heap = heap' , state_globals = globals' - , state_code = Evaluate expr fun_locs' - , state_names = confs' }]) + , state_code = Evaluate expr fun_locs' + , state_names = confs' }]) -- Rule Fun App Under | Evaluate (FunApp fun args) locals <- code - , Just (_, hobj) <- vlookupHeap fun locals globals heap + , Just (_, hobj) <- vlookupHeap fun locals globals heap , FunObj params expr fun_locs <- hobj - , (_, Left ex_params) <- unevenZip params args = - let pass_in = LiftAct args locals globals heap confs + , (_, 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_params expr fun_locs' + pobj = FunObj ex_params expr fun_locs' (heapf, paddr) = allocHeap pobj heap' in Just (RuleFunAppUnder - ,[state { state_heap = heapf + ,[state { state_heap = heapf , state_globals = globals' - , state_code = Return (MemVal paddr) - , state_names = confs' }]) + , state_code = Return (MemVal paddr) + , state_names = confs' }]) -- Rule Fun App Symbolic | Evaluate (FunApp sfun args) locals <- code - , Just (_, hobj) <- vlookupHeap sfun locals globals heap + , Just (_, hobj) <- vlookupHeap sfun locals globals heap , SymObj (Symbol svar _) <- hobj = let sname = freshSeededName (varName svar) confs svar' = Var sname (foldl AppTy (varType svar) (map atomType args)) - sym = Symbol svar' (Just (FunApp sfun args, locals)) + sym = Symbol svar' (Just (FunApp sfun args, locals)) (heap', addr) = allocHeap (SymObj sym) heap in Just (RuleFunAppSym - ,[state { state_heap = heap' - , state_code = Return (MemVal addr) + ,[state { state_heap = heap' + , state_code = Return (MemVal addr) , state_names = sname : confs }]) -- Rule Fun App ConObj | Evaluate (FunApp cvar []) locals <- code , Just (addr, hobj) <- vlookupHeap cvar locals globals heap - , ConObj _ _ <- hobj = - Just (RuleFunAppConPtr - ,[state { state_code = Return (MemVal addr) }]) + , ConObj _ _ <- hobj = + Just (RuleFunAppConPtr + ,[state { state_code = Return (MemVal addr) }]) -- Rule Fun App Uninterpreted | Evaluate (FunApp ufun args) locals <- code @@ -323,20 +332,20 @@ let pass_in = LiftAct ufun locals globals heap confs LiftAct _ locals' globals' heap' confs' = liftUnInt pass_in in Just (RuleFunAppUnInt - ,[state { state_heap = heap' + ,[state { state_heap = heap' , state_globals = globals' - , state_code = Evaluate (FunApp ufun args) locals' - , state_names = confs' }]) + , state_code = Evaluate (FunApp ufun args) locals' + , 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 in Just (RuleLet - ,[state { state_heap = heap' + ,[state { state_heap = heap' , state_globals = globals' - , state_code = Evaluate expr locals' - , state_names = confs' }]) + , state_code = Evaluate expr locals' + , state_names = confs' }]) -- Rule Case Lit | Evaluate (Case (Atom (LitAtom lit)) cvar alts) locals <- code @@ -347,18 +356,18 @@ -- Rule Case Con Pointer | Evaluate (Case (Atom (VarAtom mvar)) cvar alts) locals <- code - , Just (addr, hobj) <- vlookupHeap mvar locals globals heap - , ConObj dcon vals <- hobj + , Just (addr, hobj) <- vlookupHeap mvar locals globals heap + , ConObj dcon vals <- hobj , (Alt _ params expr):_ <- matchDataAlts dcon alts , length params == length vals = - let kvs = (cvar, MemVal addr) : zip params vals + let kvs = (cvar, MemVal addr) : zip params vals locals' = insertLocalsList kvs locals in Just (RuleCaseConPtr ,[state { state_code = Evaluate expr locals' }]) -- Rule Case Any Lit | Evaluate (Case (Atom (LitAtom lit)) cvar alts) locals <- code - , [] <- matchLitAlts lit alts + , [] <- matchLitAlts lit alts , (Alt _ _ expr):_ <- defaultAlts alts = let locals' = insertLocals (cvar, LitVal lit) locals in Just (RuleCaseAnyLit @@ -367,64 +376,64 @@ -- Rule Case Any Con Pointer | Evaluate (Case (Atom (VarAtom mvar)) cvar alts) locals <- code , Just (addr, hobj) <- vlookupHeap mvar locals globals heap - , ConObj dcon _ <- hobj - , [] <- matchDataAlts dcon alts - , (Alt _ _ expr):_ <- defaultAlts alts = + , ConObj dcon _ <- hobj + , [] <- matchDataAlts dcon alts + , (Alt _ _ expr):_ <- defaultAlts alts = let locals' = insertLocals (cvar, MemVal addr) locals in Just (RuleCaseAnyConPtr ,[state { state_code = Evaluate expr locals' }]) -- Rule Case Sym | Evaluate (Case (Atom (VarAtom mvar)) cvar alts) locals <- code - , Just (addr, hobj) <- vlookupHeap mvar locals globals heap - , SymObj _ <- hobj + , Just (addr, hobj) <- vlookupHeap mvar locals globals heap + , SymObj _ <- hobj , (acon_alts, def_alts) <- (altConAlts alts, defaultAlts alts) , length (acon_alts ++ def_alts) > 0 = - let acon_ins = map (\a -> LiftAct (mvar, addr, cvar, a) - locals globals heap confs) acon_alts + let acon_ins = map (\a -> LiftAct (mvar, addr, cvar, a) + locals globals heap confs) acon_alts acon_lifts = map liftSymAlt acon_ins - def_ins = map (\a -> LiftAct (mvar, addr, cvar, a) - locals globals heap confs) def_alts - def_lifts = map liftSymAlt def_ins + def_ins = map (\a -> LiftAct (mvar, addr, cvar, a) + locals globals heap confs) def_alts + def_lifts = map liftSymAlt def_ins -- Make AltCon states first. - acon_sts = map (liftedAltToState state) acon_lifts + acon_sts = map (liftedAltToState state) acon_lifts -- Make DEFAULT states next. - all_conss = concatMap (\(LiftAct (_, c) _ _ _ _) -> c) acon_lifts - negatives = map negateConstraint all_conss + all_conss = concatMap (\(LiftAct (_, c) _ _ _ _) -> c) acon_lifts + negatives = map negateConstraint all_conss def_lifts' = map (\(LiftAct (e, _) l g h c) -> (LiftAct (e, negatives) l g h c)) def_lifts - def_sts = map (liftedAltToState state) def_lifts' + def_sts = map (liftedAltToState state) def_lifts' in Just (RuleCaseSym, acon_sts ++ def_sts) - -- Stack Dependent Rules +-- Stack Dependent Rules -- Rule Update Frame Create Thunk | Evaluate (Atom (VarAtom var)) locals <- code - , Just (addr, hobj) <- vlookupHeap var locals globals heap - , FunObj [] expr fun_locs <- hobj = -- Thunk form. + , Just (addr, hobj) <- vlookupHeap var locals globals heap + , FunObj [] expr fun_locs <- hobj = -- Thunk form. 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 }]) + , state_heap = insertHeap (addr, Blackhole) heap + , state_code = Evaluate expr fun_locs }]) -- Rule Update Frame Delete Lit | Just (UpdateFrame frm_addr, stack') <- popStack stack - , Return (LitVal lit) <- code = - Just (RuleUpdateDLit - ,[state { state_stack = stack' - , state_heap = insertHeap (frm_addr, LitObj lit) heap - , state_code = Return (LitVal lit) }]) + , Return (LitVal lit) <- code = + Just (RuleUpdateDLit + ,[state { state_stack = stack' + , state_heap = insertHeap (frm_addr, LitObj lit) heap + , state_code = Return (LitVal lit) }]) -- Rule Update Frame Delete Val Pointer | Just (UpdateFrame frm_addr, stack') <- popStack stack - , Return (MemVal addr) <- code + , Return (MemVal addr) <- code , Just hobj <- lookupHeap addr heap , isHeapValueForm hobj = - Just (RuleUpdateDValPtr - ,[state { state_stack = stack' - , state_heap = insertHeap (frm_addr, AddrObj addr) heap - , state_code = Return (MemVal addr) }]) + Just (RuleUpdateDValPtr + ,[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 | Evaluate (Case mxpr cvar alts) locals <- code @@ -432,80 +441,80 @@ let frame = CaseFrame cvar alts locals in Just (RuleCaseCCaseNonVal ,[state { state_stack = pushStack frame stack - , state_code = Evaluate mxpr locals }]) + , state_code = Evaluate mxpr locals }]) -- Rule Case Frame Delete Lit | Just (CaseFrame cvar alts frm_locs, stack') <- popStack stack - , Return (LitVal lit) <- code = + , Return (LitVal lit) <- code = let mxpr = Atom (LitAtom lit) in Just (RuleCaseDLit ,[state { state_stack = stack' - , state_code = Evaluate (Case mxpr cvar alts) frm_locs }]) + , state_code = Evaluate (Case mxpr cvar alts) frm_locs }]) -- Rule Case Frame Delete Heap Value | Just (CaseFrame cvar alts frm_locs, stack') <- popStack stack - , Return (MemVal addr) <- code + , Return (MemVal addr) <- code , Just hobj <- lookupHeap addr heap , isHeapValueForm hobj = - let vname = freshSeededName (varName cvar) confs - vvar = Var vname (varType cvar) - mxpr = Atom (VarAtom vvar) + let vname = freshSeededName (varName cvar) confs + vvar = Var vname (varType cvar) + mxpr = Atom (VarAtom vvar) 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 (Case mxpr cvar alts) frm_locs' , state_names = vname : confs }]) -- Rule Apply Frame Create Function Thunk | Evaluate (FunApp fun args) locals <- code , Just (_, hobj) <- vlookupHeap fun locals globals heap - , FunObj [] _ _ <- hobj = + , FunObj [] _ _ <- hobj = let frame = ApplyFrame args locals in Just (RuleApplyCFunThunk ,[state { state_stack = pushStack frame stack - , state_code = Evaluate (Atom (VarAtom fun)) locals }]) + , state_code = Evaluate (Atom (VarAtom fun)) locals }]) -- Rule Apply Frame Create Function Over Application | Evaluate (FunApp fun args) locals <- code - , Just (_, hobj) <- vlookupHeap fun locals globals heap + , Just (_, hobj) <- vlookupHeap fun locals globals heap , FunObj params expr fun_locs <- hobj - , (_, Right ex_args) <- unevenZip params args = - let pass_in = LiftAct args locals globals heap confs + , (_, 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' + frame = ApplyFrame ex_args locals' in Just (RuleApplyCFunAppOver - ,[state { state_stack = pushStack frame stack - , state_heap = heap' + ,[state { state_stack = pushStack frame stack + , state_heap = heap' , state_globals = globals' - , state_code = Evaluate expr fun_locs' - , state_names = confs' }]) + , state_code = Evaluate expr fun_locs' + , state_names = confs' }]) -- Rule Apply Frame Delete ReturnPtr Function | Just (ApplyFrame args frm_locs, stack') <- popStack stack - , Return (MemVal addr) <- code - , Just hobj <- lookupHeap addr heap + , Return (MemVal addr) <- code + , Just hobj <- lookupHeap addr heap , FunObj _ _ _ <- hobj - , Just ftype <- memAddrType addr heap = - let fname = freshName VarNSpace confs - fvar = Var fname ftype + , Just ftype <- memAddrType addr heap = + let fname = freshName VarNSpace confs + fvar = Var fname ftype frm_locs' = insertLocals (fvar, MemVal addr) frm_locs in Just (RuleApplyDReturnFun ,[state { state_stack = stack' - , state_code = Evaluate (FunApp fvar args) frm_locs' + , state_code = Evaluate (FunApp fvar args) frm_locs' , state_names = fname : confs }]) -- Rule Apply Frame Delete ReturnPtr Sym | Just (ApplyFrame args frm_locs, stack') <- popStack stack - , Return (MemVal addr) <- code - , Just hobj <- lookupHeap addr heap + , Return (MemVal addr) <- code + , Just hobj <- lookupHeap addr heap , SymObj (Symbol svar _) <- hobj = - let sname = freshSeededName (varName svar) confs - svar' = Var sname (varType svar) + let sname = freshSeededName (varName svar) confs + svar' = Var sname (varType svar) frm_locs' = insertLocals (svar', MemVal addr) frm_locs in Just (RuleApplyDReturnSym ,[state { state_stack = stack' - , state_code = Evaluate (FunApp svar' args) frm_locs' + , state_code = Evaluate (FunApp svar' args) frm_locs' , state_names = sname : confs }]) -- State is Value Form diff --git a/src/SSTG/Core/Execution/Stepping.hs b/src/SSTG/Core/Execution/Stepping.hs --- a/src/SSTG/Core/Execution/Stepping.hs +++ b/src/SSTG/Core/Execution/Stepping.hs @@ -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 @@ -17,10 +17,11 @@ -- | Custom hash function. hash :: [Rule] -> Int hash rules = L.foldl' (\acc c -> (acc + p2 * C.ord c)`mod` p3) p1 str - where str = concatMap show rules - p1 = 5381 - p2 = 1009 - p3 = 433494437 + where + str = concatMap show rules + p1 = 5381 + p2 = 1009 + p3 = 433494437 -- | A `State` that is not in value form yet, capable of being evaluated. A -- list of `Rule`s is kept to denote reduction history. @@ -33,16 +34,17 @@ -- | Increment Status conditions, and shift the current / parent id as needed. incStatus :: Maybe Int -> State -> State incStatus mb_id state = state { state_status = status' } - where status = state_status state - status' = case mb_id of - Nothing -> incStatusSteps status - Just id' -> incStatusSteps (updateStatusId id' status) + where + status = state_status state + status' = case mb_id of + 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)] + Nothing -> [(hist, start)] Just (rule, results) -> let trace = hist ++ [rule] mb_id = if length results > 1 @@ -53,17 +55,19 @@ -- | This is what we use the `<*>` over. pass :: [LiveState] -> ([LiveState], [DeadState] -> [DeadState]) pass rule_states = (lives, \prev -> prev ++ deads) - where stepped = concatMap step rule_states - lives = filter (not . isStateValueForm . snd) stepped - deads = filter (isStateValueForm . snd) stepped + where + stepped = concatMap step rule_states + lives = filter (not . isStateValueForm . snd) stepped + deads = filter (isStateValueForm . snd) stepped -- | Run bounded breadth-first-search of the execution space with an `Int` to -- denote the maximum number of steps to take. runBoundedBFS :: Int -> State -> ([LiveState], [DeadState]) runBoundedBFS n state = (run execution) [([], state)] - where passes = take n (repeat (SymbolicT { run = pass })) - start = SymbolicT { run = (\lives -> (lives, [])) } - execution = foldl (\acc s -> s <*> acc) start passes + where + passes = take n (repeat (SymbolicT { run = pass })) + start = SymbolicT { run = (\lives -> (lives, [])) } + execution = foldl (\acc s -> s <*> acc) start passes -- | Run bounded breadth-first-search of the execution state with an `Int` to -- denote the maximum number of steps to take. We keep track of a list to track diff --git a/src/SSTG/Core/Execution/Support.hs b/src/SSTG/Core/Execution/Support.hs deleted file mode 100644 --- a/src/SSTG/Core/Execution/Support.hs +++ /dev/null @@ -1,348 +0,0 @@ --- | 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(..) - - , 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 - -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_id :: 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_id = 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_id = 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 - diff --git a/src/SSTG/Core/Language.hs b/src/SSTG/Core/Language.hs --- a/src/SSTG/Core/Language.hs +++ b/src/SSTG/Core/Language.hs @@ -1,9 +1,13 @@ -- | Export Module for SSTG.Syntax module SSTG.Core.Language - ( module SSTG.Core.Language.Syntax + ( 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 diff --git a/src/SSTG/Core/Language/Naming.hs b/src/SSTG/Core/Language/Naming.hs new file mode 100644 --- /dev/null +++ b/src/SSTG/Core/Language/Naming.hs @@ -0,0 +1,217 @@ +-- | Naming Module +module SSTG.Core.Language.Naming + ( allNames + , freshString + , freshName + , freshSeededName + , freshNameList + , 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) + +-- | `Name`s in the `Heap`. +heapNames :: Heap -> [Name] +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 +heapObjNames (ConObj dcon _) = dataNames dcon +heapObjNames (FunObj ps expr locs) = exprNames expr ++ localsNames locs + ++ concatMap varNames ps + +-- | `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 `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 (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 a `PrimFun`. +pfunNames :: PrimFun -> [Name] +pfunNames (PrimFun n ty) = n : typeNames ty + +-- | `Name`s in a `DataCon`. +dataNames :: DataCon -> [Name] +dataNames (DataCon n ty tys) = n : concatMap typeNames (ty : tys) + +-- | `Name`s in a `TyBinder`. +tyBinderNames :: TyBinder -> [Name] +tyBinderNames (AnonTyBndr) = [] +tyBinderNames (NamedTyBndr n) = [n] + +-- | `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 + +-- | `Name`s in a `Coercion`. +coercionNames :: Coercion -> [Name] +coercionNames (Coercion t1 t2) = typeNames t1 ++ typeNames t2 + +-- | `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 + +-- | `Name`s in a `PathCons`. +pconsNames :: PathCons -> [Name] +pconsNames pathcons = concatMap constraintNames (pathconsToList pathcons) + +-- | `Name`s in a `PathCons`. +constraintNames :: Constraint -> [Name] +constraintNames (Constraint (_, vs) e locs _) = exprNames e ++ localsNames locs + ++ map varName vs + +-- | Create a fresh seed given any `Int`, a `String` seed, and a `Set` of +-- `String`s that we do not want our new `String` to conflict with. The sole +-- purpose of the `Int` seed is to allow us tell us how much to multiply some +-- prime number to "orbit" an index around a fixed list of acceptable `Char`s. +freshString :: Int -> String -> S.Set String -> String +freshString rand seed confs = if S.member seed confs + then freshString (rand + 1) (seed ++ [pick]) confs else seed + where + pick = bank !! index + index = raw_i `mod` (length bank) + raw_i = (abs rand) * prime + prime = 151 -- The original? :) + bank = lower ++ upper ++ nums + lower = "abcdefghijlkmnopqrstuvwxyz" + upper = "ABCDEFGHIJKLMNOPQRSTUVWXYZ" + nums = "1234567890" + +-- | Fresh `Name` given a list of `Name`s that acts as conflicts. The fresh +-- `Name`s generated in this manner are prefixed with @"fs?"@, which is not a +-- valid identifier in Haskell, but okay in SSTG. we also specify the +-- `NameSpace` under which the `Name` will be generated. This will generally +-- be `VarNSpace` in actual usage. +freshName :: NameSpace -> [Name] -> Name +freshName nspace confs = freshSeededName seed confs + where + seed = Name "fs?" Nothing nspace 0 + +-- | A fresh `Name` generated from a seed `Name`, which will act as the prefix +-- of the new `Name`. We ues the same `NameSpace` as the seed `Name` when +-- generating this way. +freshSeededName :: Name -> [Name] -> Name +freshSeededName seed confs = Name occ' mdl ns unq' + where + Name occ mdl ns unq = seed + occ' = freshString 1 occ (S.fromList alls) + unq' = maxs + 1 + alls = map nameOccStr confs + maxs = L.maximum (unq : map nameUnique confs) + +-- | Generate a list of `Name`s, each corresponding to the appropriate element +-- of the `NameSpace` list. +freshNameList :: [NameSpace] -> [Name] -> [Name] +freshNameList [] _ = [] +freshNameList (nspace:nss) confs = name' : freshNameList nss confs' + where + name' = freshName nspace confs + confs' = name' : confs + +-- | List of seeded fresh `Name`s. +freshSeededNameList :: [Name] -> [Name] -> [Name] +freshSeededNameList [] _ = [] +freshSeededNameList (n:ns) confs = name' : freshSeededNameList ns confs' + where + name' = freshSeededName n confs + confs' = name' : confs + diff --git a/src/SSTG/Core/Language/Support.hs b/src/SSTG/Core/Language/Support.hs new file mode 100644 --- /dev/null +++ b/src/SSTG/Core/Language/Support.hs @@ -0,0 +1,351 @@ +-- | 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 + diff --git a/src/SSTG/Core/Language/Syntax.hs b/src/SSTG/Core/Language/Syntax.hs --- a/src/SSTG/Core/Language/Syntax.hs +++ b/src/SSTG/Core/Language/Syntax.hs @@ -3,29 +3,10 @@ ( module SSTG.Core.Language.Syntax ) where -type Program = GenProgram Name Var - -type Lit = GenLit Name Var -type Atom = GenAtom Name Var -type PrimFun = GenPrimFun Name Var -type Expr = GenExpr Name Var -type Alt = GenAlt Name Var -type AltCon = GenAltCon Name Var -type Bind = GenBind Name Var -type BindRhs = GenBindRhs Name Var - -type DataCon = GenDataCon Name -type Type = GenType Name -type TyBinder = GenTyBinder Name -type Coercion = GenCoercion Name -type TyCon = GenTyCon Name -type AlgTyRhs = GenAlgTyRhs Name - --- | A `Program` is defined as a list of bindings. The @bnd@ is an identifier +-- | 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 GenProgram bnd var = Program [GenBind bnd var] - deriving (Show, Eq, Read) +newtype Program = Program [Bind] deriving (Show, Eq, Read) -- | Variables, data constructors, type variables, and type constructors. data NameSpace = VarNSpace | DataNSpace | TvNSpace | TcClsNSpace @@ -39,92 +20,89 @@ deriving (Show, Eq, Read, Ord) -- | Variables consist of a `Name` and a `Type`. -data Var = Var Name (GenType Name) deriving (Show, Eq, Read) +data Var = Var Name Type deriving (Show, Eq, Read) -- | Literals are largely augmented from the original GHC implementation, with -- additional annotations to denote `BlankAddr` for lifting, `AddrLit` for -- value deriviation, `SymLit` for symbolic literals, and `SymLitEval` to -- represent symbolic literal evaluation, as literal manipulation functions -- are defined in the Haskell Prelude, and thus outside of scope for us. -data GenLit bnd var = MachChar Char (GenType bnd) - | MachStr String (GenType bnd) - | MachInt Int (GenType bnd) - | 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] - deriving (Show, Eq, Read) +data Lit = MachChar Char Type + | MachStr String Type + | MachInt Int Type + | MachWord Int Type + | MachFloat Rational Type + | MachDouble Rational Type + | MachLabel String (Maybe Int) Type + | MachNullAddr Type + | BlankAddr + | AddrLit Int + | SymLit Var + | SymLitEval PrimFun [Lit] + deriving (Show, Eq, Read) -- | Atomic objects. `VarAtom` may be used for variable lookups, while -- `LitAtom` is used to denote literals. -data GenAtom bnd var = LitAtom (GenLit bnd var) - | VarAtom var - deriving (Show, Eq, Read) +data Atom = LitAtom (Lit) + | VarAtom Var + deriving (Show, Eq, Read) -- | Primitive functions. -data GenPrimFun bnd var = PrimFun bnd (GenType bnd) deriving (Show, Eq, Read) +data PrimFun = PrimFun Name Type deriving (Show, Eq, Read) -- | 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 (GenBind bnd var) (GenExpr bnd var) - | Case (GenExpr bnd var) var [GenAlt bnd var] - deriving (Show, Eq, Read) +data Expr = Atom Atom + | PrimApp PrimFun [Atom] + | ConApp DataCon [Atom] + | FunApp Var [Atom] + | Let Bind Expr + | Case Expr Var [Alt] + deriving (Show, Eq, Read) -- | Alternatives utilize an `AltCon`, a list of parameters of that match to -- the appropriate `DataAlt` as applicable, and an expression for the result. -data GenAlt bnd var = Alt (GenAltCon bnd var) [var] (GenExpr bnd var) - deriving (Show, Eq, Read) +data Alt = Alt AltCon [Var] Expr deriving (Show, Eq, Read) -- | Alt Constructor -data GenAltCon bnd var = DataAlt (GenDataCon bnd) - | LitAlt (GenLit bnd var) - | Default - deriving (Show, Eq, Read) +data AltCon = DataAlt DataCon + | LitAlt Lit + | Default + deriving (Show, Eq, Read) -- | Bind -data GenBind bnd var = Bind RecForm [(var, GenBindRhs bnd var)] - deriving (Show, Eq, Read) +data Bind = Bind RecForm [(Var, BindRhs)] deriving (Show, Eq, Read) -- | Recursive? data RecForm = Rec | NonRec deriving (Show, Eq, Read) -- | `BindRhs` taken straight from STG can be either in constructor form, or -- function form. Empty parameter list denotes a thunk. -data GenBindRhs bnd var = ConForm (GenDataCon bnd) [GenAtom bnd var] - | FunForm [var] (GenExpr bnd var) - deriving (Show, Eq, Read) +data BindRhs = ConForm DataCon [Atom] + | FunForm [Var] Expr + 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 bnd (GenType bnd) [GenType bnd] - deriving (Show, Eq, Read) +data DataCon = DataCon Name Type [Type] 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) - | ForAllTy (GenTyBinder bnd) (GenType bnd) - | CastTy (GenType bnd) (GenCoercion bnd) - | TyConApp (GenTyCon bnd) [GenType bnd] - | CoercionTy (GenCoercion bnd) - | LitTy TyLit - | FunTy (GenType bnd) (GenType bnd) - | Bottom - deriving (Show, Eq, Read) +data Type = TyVarTy Name Type + | AppTy Type Type + | ForAllTy TyBinder Type + | CastTy Type Coercion + | TyConApp TyCon [Type] + | CoercionTy Coercion + | LitTy TyLit + | FunTy Type Type + | Bottom + deriving (Show, Eq, Read) -- | Type binder for `ForAllTy`. -data GenTyBinder bnd = NamedTyBndr bnd - | AnonTyBndr - deriving (Show, Eq, Read) +data TyBinder = NamedTyBndr Name + | AnonTyBndr + deriving (Show, Eq, Read) -- | `Type` literal. data TyLit = NumTyLit Int @@ -132,22 +110,21 @@ deriving (Show, Eq, Read) -- | Coercion. I have no idea what this does :) -data GenCoercion bnd = Coercion (GenType bnd) (GenType bnd) - deriving (Show, Eq, Read) +data Coercion = Coercion Type Type deriving (Show, Eq, Read) -- | Type constructor. -data GenTyCon bnd = FunTyCon bnd [GenTyBinder bnd] - | AlgTyCon bnd [bnd] (GenAlgTyRhs bnd) - | SynonymTyCon bnd [bnd] - | FamilyTyCon bnd [bnd] - | PrimTyCon bnd [GenTyBinder bnd] - | Promoted bnd [GenTyBinder bnd] (GenDataCon bnd) - deriving (Show, Eq, Read) +data TyCon = FunTyCon Name [TyBinder] + | AlgTyCon Name [Name] AlgTyRhs + | SynonymTyCon Name [Name] + | FamilyTyCon Name [Name] + | PrimTyCon Name [TyBinder] + | Promoted Name [TyBinder] DataCon + deriving (Show, Eq, Read) -- | ADT RHS. -data GenAlgTyRhs bnd = AbstractTyCon Bool - | DataTyCon [bnd] - | NewTyCon bnd - | TupleTyCon bnd - deriving (Show, Eq, Read) +data AlgTyRhs = AbstractTyCon Bool + | DataTyCon [Name] + | NewTyCon Name + | TupleTyCon Name + deriving (Show, Eq, Read) diff --git a/src/SSTG/Core/Language/Typing.hs b/src/SSTG/Core/Language/Typing.hs --- a/src/SSTG/Core/Language/Typing.hs +++ b/src/SSTG/Core/Language/Typing.hs @@ -11,17 +11,17 @@ -- | Literal type. litType :: Lit -> Type -litType (MachChar _ ty) = ty -litType (MachStr _ ty) = ty -litType (MachInt _ ty) = ty -litType (MachWord _ ty) = ty -litType (MachFloat _ ty) = ty -litType (MachDouble _ ty) = ty -litType (MachNullAddr ty) = ty -litType (MachLabel _ _ ty) = ty -litType (BlankAddr) = Bottom -litType (AddrLit _) = Bottom -litType (SymLit var) = varType var +litType (MachChar _ ty) = ty +litType (MachStr _ ty) = ty +litType (MachInt _ ty) = ty +litType (MachWord _ ty) = ty +litType (MachFloat _ ty) = ty +litType (MachDouble _ ty) = ty +litType (MachLabel _ _ ty) = ty +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) -- | Atom type. @@ -43,11 +43,11 @@ -- | I wonder what this could possibly be? exprType :: Expr -> Type -exprType (Atom atom) = atomType atom +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 (FunApp fun args) = foldl AppTy (varType fun) (map atomType args) -exprType (Let _ expr) = exprType expr -exprType (Case _ _ (a:_)) = altType a -exprType _ = Bottom +exprType (ConApp dc args) = foldl AppTy (dataconType dc) (map atomType args) +exprType (FunApp fun args) = foldl AppTy (varType fun) (map atomType args) +exprType (Let _ expr) = exprType expr +exprType (Case _ _ (a:_)) = altType a +exprType _ = Bottom diff --git a/src/SSTG/Core/Preprocessing.hs b/src/SSTG/Core/Preprocessing.hs new file mode 100644 --- /dev/null +++ b/src/SSTG/Core/Preprocessing.hs @@ -0,0 +1,7 @@ +-- | Export Module for SSTG.Core.Preprocessing +module SSTG.Core.Preprocessing + ( module SSTG.Core.Preprocessing.Defunctionalization + ) where + +import SSTG.Core.Preprocessing.Defunctionalization + diff --git a/src/SSTG/Core/Preprocessing/Defunctionalization.hs b/src/SSTG/Core/Preprocessing/Defunctionalization.hs new file mode 100644 --- /dev/null +++ b/src/SSTG/Core/Preprocessing/Defunctionalization.hs @@ -0,0 +1,8 @@ +-- | Defunctionalization +module SSTG.Core.Preprocessing.Defunctionalization + ( defunctionalize + ) where + +defunctionalize :: a +defunctionalize = undefined + diff --git a/src/SSTG/Core/SMT.hs b/src/SSTG/Core/SMT.hs new file mode 100644 --- /dev/null +++ b/src/SSTG/Core/SMT.hs @@ -0,0 +1,7 @@ +-- | Export Module for SSTG.Core.SMT +module SSTG.Core.SMT + ( module SSTG.Core.SMT.Syntax + ) where + +import SSTG.Core.SMT.Syntax + diff --git a/src/SSTG/Core/SMT/Syntax.hs b/src/SSTG/Core/SMT/Syntax.hs new file mode 100644 --- /dev/null +++ b/src/SSTG/Core/SMT/Syntax.hs @@ -0,0 +1,7 @@ +-- | SMT2-Lib Syntax +module SSTG.Core.SMT.Syntax + ( SMTExpr(..) + ) where + +data SMTExpr = SMTEXPR + diff --git a/src/SSTG/Core/Translation/Haskell.hs b/src/SSTG/Core/Translation/Haskell.hs --- a/src/SSTG/Core/Translation/Haskell.hs +++ b/src/SSTG/Core/Translation/Haskell.hs @@ -34,8 +34,7 @@ mkIOString :: (Outputable a) => a -> IO String mkIOString obj = runGhc (Just libdir) $ do dflags <- getSessionDynFlags - let ppr_str = showPpr dflags obj - return ppr_str + return (showPpr dflags obj) -- | Given the project directory and the source file path, compiles the -- `ModuleGraph` and translates it into a SSTG `Bind`s. @@ -44,16 +43,15 @@ (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 - let m_bndss = map mg_binds gutss - let m_tcss = map mg_tcs gutss + let mod_bindss = map mg_binds gutss + let mod_tycss = map mg_tcs gutss -- Zip in preparation for STG transformation. - let z1 = zip3 mod_lcs m_bndss m_tcss - preps <- mapM (\((m, l), b, t) -> corePrepPgm env m l b t) z1 - let z2 = zip (map fst mod_lcs) preps - s_bndss <- mapM (\(m, p) -> coreToStg dflags m p) z2 + let zipd1 = zip3 mod_lcs mod_bindss mod_tycss + preps <- mapM (\((m, l), b, t) -> corePrepPgm env m l b t) zipd1 + let zipd2 = zip (map fst mod_lcs) preps + stg_bindss <- mapM (\(m, p) -> coreToStg dflags m p) zipd2 -- Create the binds. - let sl_bnds = map mkBind (concat s_bndss) - return sl_bnds + return (map mkBind (concat stg_bindss)) -- | Compilation closure type. type CompileClosure = ([(ModSummary, ModGuts)], DynFlags, HscEnv) @@ -66,32 +64,31 @@ mkCompileClosure proj src = runGhc (Just libdir) $ do beta_flags <- getSessionDynFlags let dflags = beta_flags { importPaths = [proj] } - _ <- setSessionDynFlags dflags - env <- getSession - target <- guessTarget src Nothing - _ <- setTargets [target] - _ <- load LoadAllTargets + _ <- setSessionDynFlags dflags + env <- getSession + target <- guessTarget src Nothing + _ <- setTargets [target] + _ <- load LoadAllTargets -- Now that things are loaded, make the compilation closure. - mod_graph <- getModuleGraph - pmods <- mapM parseModule mod_graph - tmods <- mapM typecheckModule pmods - dmods <- mapM desugarModule tmods - let m_gtss = map coreModule dmods - let zipd = (zip mod_graph m_gtss, dflags, env) - return zipd + mod_graph <- getModuleGraph + pmods <- mapM parseModule mod_graph + tmods <- mapM typecheckModule pmods + dmods <- mapM desugarModule tmods + let mod_gutss = map coreModule dmods + return (zip mod_graph mod_gutss, dflags, env) -- | Make SSTG `Expr`. mkExpr :: StgExpr -> SL.Expr -mkExpr (StgLit lit) = SL.Atom (SL.LitAtom (mkLit lit)) -mkExpr (StgApp occ args) = SL.FunApp (mkVar occ) (map mkAtom args) -mkExpr (StgConApp dc args) = SL.ConApp (mkData dc) (map mkAtom args) +mkExpr (StgLit lit) = SL.Atom (SL.LitAtom (mkLit lit)) +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 (StgLam _ _) = error "mkExpr: StgLam detected" -mkExpr (StgLet bnd expr) = SL.Let (mkBind bnd) (mkExpr expr) -mkExpr (StgLetNoEscape _ _ bnd expr) = mkExpr (StgLet bnd expr) -mkExpr (StgCase mexpr _ _ bndr _ _ alts) = SL.Case (mkExpr mexpr) (mkVar bndr) - (map mkAlt alts) +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) -- | Make SSTG `Atom`. mkAtom :: StgArg -> SL.Atom @@ -101,51 +98,52 @@ -- | Make SSTG `Name`. mkName :: Name -> SL.Name mkName name = SL.Name occ mdl ns unq - where occ = (occNameString . nameOccName) name - ns = (mkNameSpace . occNameSpace . nameOccName) name - unq = (getKey . nameUnique) name - mdl = case nameModule_maybe name of - Nothing -> Nothing - Just md -> Just ((moduleNameString . moduleName) md) + where + occ = (occNameString . nameOccName) name + ns = (mkNameSpace . occNameSpace . nameOccName) name + unq = (getKey . nameUnique) name + mdl = case nameModule_maybe name of + Nothing -> Nothing + Just md -> Just ((moduleNameString . moduleName) md) -- | Make SSTG `NameSpace`. mkNameSpace :: NameSpace -> SL.NameSpace -mkNameSpace ns | isVarNameSpace ns = SL.VarNSpace - | isTvNameSpace ns = SL.TvNSpace +mkNameSpace ns | isVarNameSpace ns = SL.VarNSpace + | isTvNameSpace ns = SL.TvNSpace | isDataConNameSpace ns = SL.DataNSpace - | isTcClsNameSpace ns = SL.TcClsNSpace - | otherwise = error "mkNameSpace: unrecognized" + | isTcClsNameSpace ns = SL.TcClsNSpace + | otherwise = error "mkNameSpace: unrecognized" -- | Make SSTG Var mkVar :: Var -> SL.Var mkVar var = SL.Var vname vtype - where vname = (mkName . V.varName) var - vtype = (mkType . varType) var + where + vname = (mkName . V.varName) var + vtype = (mkType . varType) var -- | Make SSTG `Bind`. mkBind :: StgBinding -> SL.Bind -mkBind (StgNonRec bnd r) = SL.Bind SL.NonRec [(mkVar bnd, mkRhs r)] -mkBind (StgRec bnd) = SL.Bind SL.Rec (map (\(b, r) -> - (mkVar b, mkRhs r)) bnd) +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) -- | Make SSTG `BindRhs`. mkRhs :: StgRhs -> SL.BindRhs -mkRhs (StgRhsCon _ dc args) = SL.ConForm (mkData dc) (map mkAtom args) +mkRhs (StgRhsCon _ dcon args) = SL.ConForm (mkData dcon) (map mkAtom args) mkRhs (StgRhsClosure _ _ _ _ _ ps e) = SL.FunForm (map mkVar ps) (mkExpr e) -- | Make SSTG `Lit`. mkLit :: Literal -> SL.Lit mkLit lit = case lit of - (MachChar chr) -> SL.MachChar chr ((mkType . literalType) lit) - (MachStr bstr) -> SL.MachStr (show bstr) ((mkType . literalType) lit) - (MachInt i) -> SL.MachInt (fromInteger i) ((mkType . literalType) lit) - (MachInt64 i) -> SL.MachInt (fromInteger i) ((mkType . literalType) lit) - (MachWord i) -> SL.MachWord (fromInteger i) ((mkType . literalType) lit) - (MachWord64 i) -> SL.MachWord (fromInteger i) ((mkType . literalType) lit) - (MachFloat rat) -> SL.MachFloat rat ((mkType . literalType) lit) - (MachDouble rat) -> SL.MachDouble rat ((mkType . literalType) lit) - (LitInteger i _) -> SL.MachInt (fromInteger i) ((mkType . literalType) lit) - (MachNullAddr) -> SL.MachNullAddr ((mkType . literalType) lit) + (MachChar chr) -> SL.MachChar chr ((mkType . literalType) lit) + (MachStr bstr) -> SL.MachStr (show bstr) ((mkType . literalType) lit) + (MachInt i) -> SL.MachInt (fromInteger i) ((mkType . literalType) lit) + (MachInt64 i) -> SL.MachInt (fromInteger i) ((mkType . literalType) lit) + (MachWord i) -> SL.MachWord (fromInteger i) ((mkType . literalType) lit) + (MachWord64 i) -> SL.MachWord (fromInteger i) ((mkType . literalType) lit) + (MachFloat rat) -> SL.MachFloat rat ((mkType . literalType) lit) + (MachDouble rat) -> SL.MachDouble rat ((mkType . literalType) lit) + (LitInteger i _) -> SL.MachInt (fromInteger i) ((mkType . literalType) lit) + (MachNullAddr) -> SL.MachNullAddr ((mkType . literalType) lit) (MachLabel f m _) -> SL.MachLabel (unpackFS f) m ((mkType . literalType) lit) -- | `DataCon`'s `Name`. @@ -155,19 +153,21 @@ -- | Make SSTG `DataCon`. mkData :: DataCon -> SL.DataCon mkData datacon = SL.DataCon name ty args - where name = mkDataName datacon - ty = (mkType . dataConRepType) datacon - args = map mkType (dataConOrigArgTys datacon) + where + name = mkDataName datacon + ty = (mkType . dataConRepType) datacon + args = map mkType (dataConOrigArgTys datacon) -- | Make SSTG `PrimFun`. mkPrimOp :: StgOp -> SL.PrimFun mkPrimOp (StgPrimOp op) = SL.PrimFun (SL.Name occ Nothing ns unq) ty - where occname = primOpOcc op - occ = occNameString occname - ns = (mkNameSpace . occNameSpace) occname - unq = primOpTag op - ty = (mkType . primOpType) op -mkPrimOp _ = error "mkPrimOp: got StgPrimCallOp or StgFCallOp" + where + occname = primOpOcc op + occ = occNameString occname + ns = (mkNameSpace . occNameSpace) occname + unq = primOpTag op + ty = (mkType . primOpType) op +mkPrimOp _ = error "mkPrimOp: got StgPrimCallOp or StgFCallOp" -- | Make SSTG `Alt`. mkAlt :: StgAlt -> SL.Alt @@ -176,54 +176,55 @@ -- | Make SSTG `AltCon`. mkAltCon :: AltCon -> SL.AltCon mkAltCon (DataAlt dc) = SL.DataAlt (mkData dc) -mkAltCon (LitAlt lit) = SL.LitAlt (mkLit lit) -mkAltCon (DEFAULT) = SL.Default +mkAltCon (LitAlt lit) = SL.LitAlt (mkLit lit) +mkAltCon (DEFAULT) = SL.Default -- | Make SSTG `Type`. mkType :: Type -> SL.Type -mkType (AppTy t1 t2) = SL.AppTy (mkType t1) (mkType t2) +mkType (TyVarTy v) = SL.TyVarTy (mkName (V.varName v)) (mkType (varType v)) +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 (LitTy tlit) = SL.LitTy (mkTyLit tlit) -mkType (CastTy ty cor) = SL.CastTy (mkType ty) (mkCoercion cor) +mkType (ForAllTy b ty) = SL.ForAllTy (mkTyBinder b) (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) -mkType (TyVarTy v) = SL.TyVarTy (mkName (V.varName v)) - (mkType (varType v)) -- | Make SSTG `TyCon`. mkTyCon :: TyCon -> SL.TyCon -mkTyCon tc | isFunTyCon tc = SL.FunTyCon name tcbndrs - | isAlgTyCon tc = SL.AlgTyCon name tvnames algrhs - | isFamilyTyCon tc = SL.FamilyTyCon name tvnames - | isPrimTyCon tc = SL.PrimTyCon name tcbndrs +mkTyCon tc | isFunTyCon tc = SL.FunTyCon name tcbindrs + | isAlgTyCon tc = SL.AlgTyCon name tvnames algrhs + | isFamilyTyCon tc = SL.FamilyTyCon name tvnames + | isPrimTyCon tc = SL.PrimTyCon name tcbindrs | isTypeSynonymTyCon tc = SL.SynonymTyCon name tvnames - | isPromotedDataCon tc = SL.Promoted name tcbndrs dcon - | otherwise = error "mkTyCon: unrecognized TyCon" - where name = (mkName . tyConName) tc - algrhs = (mkAlgTyConRhs . algTyConRhs) tc - tcbndrs = map mkTyBinder (tyConBinders tc) - tvnames = map (mkName. V.varName) (tyConTyVars tc) - dcon = (mkData . MB.fromJust . isPromotedDataCon_maybe) tc + | isPromotedDataCon tc = SL.Promoted name tcbindrs dcon + | otherwise = error "mkTyCon: unrecognized TyCon" + where + name = (mkName . tyConName) tc + algrhs = (mkAlgTyConRhs . algTyConRhs) tc + tcbindrs = map mkTyBinder (tyConBinders tc) + tvnames = map (mkName. V.varName) (tyConTyVars tc) + dcon = (mkData . MB.fromJust . isPromotedDataCon_maybe) tc -- | Make SSTG `AlgTyRhs`. mkAlgTyConRhs :: AlgTyConRhs -> SL.AlgTyRhs -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) +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`. mkTyBinder :: TyBinder -> SL.TyBinder -mkTyBinder (Anon _) = SL.AnonTyBndr +mkTyBinder (Anon _) = SL.AnonTyBndr mkTyBinder (Named v _) = SL.NamedTyBndr (mkName (V.varName v)) -- | Make SSTG `Type` literals. mkTyLit :: TyLit -> SL.TyLit -mkTyLit (NumTyLit i) = SL.NumTyLit (fromInteger i) +mkTyLit (NumTyLit i) = SL.NumTyLit (fromInteger i) mkTyLit (StrTyLit fs) = SL.StrTyLit (unpackFS fs) -- | Make SSTG `Coercion`. mkCoercion :: Coercion -> SL.Coercion mkCoercion coer = SL.Coercion (mkType a) (mkType b) - where (a, b) = (unPair . coercionKind) coer + where + (a, b) = (unPair . coercionKind) coer diff --git a/src/SSTG/Utils/FileIO.hs b/src/SSTG/Utils/FileIO.hs --- a/src/SSTG/Utils/FileIO.hs +++ b/src/SSTG/Utils/FileIO.hs @@ -5,8 +5,7 @@ , writePrettyState ) where -import SSTG.Core.Execution.Stepping -import SSTG.Core.Execution.Support +import SSTG.Core import SSTG.Utils.Printing import Text.Read diff --git a/src/SSTG/Utils/Printing.hs b/src/SSTG/Utils/Printing.hs --- a/src/SSTG/Utils/Printing.hs +++ b/src/SSTG/Utils/Printing.hs @@ -12,26 +12,29 @@ -- | Print `LiveState` and `DeadState` that yield from execution snapshots. pprLivesDeadsStr :: ([LiveState], [DeadState]) -> String pprLivesDeadsStr (lives, deads) = injNewLineSeps10 acc_strs - where header = "(Lives, Deads)" - lv_str = (injNewLineSeps5 . map pprLiveStr) lives - dd_str = (injNewLineSeps5 . map pprDeadStr) deads - acc_strs = [header, lv_str, dd_str] + where + header = "(Lives, Deads)" + lv_str = (injNewLineSeps5 . map pprLiveStr) lives + dd_str = (injNewLineSeps5 . map pprDeadStr) deads + acc_strs = [header, lv_str, dd_str] -- | Print `LiveState`. pprLiveStr :: LiveState -> String pprLiveStr (rules, state) = injNewLine acc_strs - where header = "Live" - rule_str = pprRulesStr rules - st_str = pprStateStr state - acc_strs = [header, rule_str, st_str] + where + header = "Live" + rule_str = pprRulesStr rules + st_str = pprStateStr state + acc_strs = [header, rule_str, st_str] -- | Print `DeadState`. pprDeadStr :: LiveState -> String pprDeadStr (rules, state) = injNewLine acc_strs - where header = "Dead" - rule_str = pprRulesStr rules - st_str = pprStateStr state - acc_strs = [header, rule_str, st_str] + where + header = "Dead" + rule_str = pprRulesStr rules + st_str = pprStateStr state + acc_strs = [header, rule_str, st_str] -- | Print `Rule`. pprRuleStr :: Rule -> String @@ -42,29 +45,30 @@ -- | Print `State`. pprStateStr :: State -> String -pprStateStr state = injNewLine acc_strs - where status_str = (pprStatusStr . state_status) state - stack_str = (pprStackStr . state_stack) state - heap_str = (pprHeapStr . state_heap) state - globals_str = (pprGlobalsStr . state_globals) state - expr_str = (pprCodeStr . state_code) state - names_str = (pprNamesStr . state_names) state - pcons_str = (pprPathConsStr . state_paths) state - acc_strs = [ ">>>>> [State] >>>>>>>>>>>>>>>" - , status_str - , "----- [Stack] ---------------" - , stack_str - , "----- [Heap] ----------------" - , heap_str - , "----- [Globals] -------------" - , globals_str - , "----- [Expression] ----------" - , expr_str - , "----- [All Names] -------" - , fst ("", names_str) -- names_str - , "----- [Path Constraint] -----" - , pcons_str - , "<<<<<<<<<<<<<<<<<<<<<<<<<<<<<" ] +pprStateStr state = injNewLine acc_strs + where + status_str= (pprStatusStr . state_status) state + stack_str = (pprStackStr . state_stack) state + heap_str = (pprHeapStr . state_heap) state + globals_str = (pprGlobalsStr . state_globals) state + expr_str = (pprCodeStr . state_code) state + names_str = (pprNamesStr . state_names) state + pcons_str = (pprPathConsStr . state_paths) state + acc_strs = [ ">>>>> [State] >>>>>>>>>>>>>>>" + , status_str + , "----- [Stack] ---------------" + , stack_str + , "----- [Heap] ----------------" + , heap_str + , "----- [Globals] -------------" + , globals_str + , "----- [Expression] ----------" + , expr_str + , "----- [All Names] -------" + , fst ("", names_str) -- names_str + , "----- [Path Constraint] -----" + , pcons_str + , "<<<<<<<<<<<<<<<<<<<<<<<<<<<<<" ] -- | Inject `String` into parantheses. sub :: String -> String @@ -89,12 +93,14 @@ -- | Inject a list of `String`s with newline separators of dashes length 5. injNewLineSeps5 :: [String] -> String injNewLineSeps5 strs = L.intercalate seps strs - where seps = "\n-----\n" + where + seps = "\n-----\n" -- | Inject a list of `String`s wit hnewline separators of dashes length 10. injNewLineSeps10 :: [String] -> String injNewLineSeps10 strs = L.intercalate seps strs - where seps = "\n----------\n" + where + seps = "\n----------\n" -- | Print `MemAddr`. pprMemAddrStr :: MemAddr -> String @@ -115,155 +121,177 @@ -- | Print `Stack`. pprStackStr :: Stack -> String pprStackStr stack = injNewLineSeps10 acc_strs - where frame_strs = map pprFrameStr (stackToList stack) - acc_strs = "Stack" : frame_strs + where + frame_strs = map pprFrameStr (stackToList stack) + acc_strs = "Stack" : frame_strs -- | Print `Frame`. pprFrameStr :: Frame -> String pprFrameStr (CaseFrame var alts locals) = injNewLine acc_strs - where header = "CaseFrame" - var_str = pprVarStr var - alts_str = pprAltsStr alts - locs_str = pprLocalsStr locals - acc_strs = [header, var_str, alts_str, locs_str] + where + header = "CaseFrame" + var_str = pprVarStr var + alts_str = pprAltsStr alts + locs_str = pprLocalsStr locals + acc_strs = [header, var_str, alts_str, locs_str] pprFrameStr (ApplyFrame args locals) = injNewLine acc_strs - where header = "ApplyFrame" - args_str = injIntoList (map pprAtomStr args) - locs_str = pprLocalsStr locals - acc_strs = [header, args_str, locs_str] + where + header = "ApplyFrame" + args_str = injIntoList (map pprAtomStr args) + locs_str = pprLocalsStr locals + acc_strs = [header, args_str, locs_str] pprFrameStr (UpdateFrame addr) = injNewLine acc_strs - where header = "UpdateFrame" - addr_str = pprMemAddrStr addr - acc_strs = [header, addr_str] + where + header = "UpdateFrame" + addr_str = pprMemAddrStr addr + acc_strs = [header, addr_str] -- | Print the @Maybe (Expr, Locals)@. pprSymClosureStr :: Maybe (Expr, Locals) -> String -pprSymClosureStr (Nothing) = "SymClosure ()" +pprSymClosureStr (Nothing) = "SymClosure ()" pprSymClosureStr (Just (expr, locals)) = injSpace acc_strs - where header = "SymClosure" - expr_str = pprExprStr expr - locs_str = pprLocalsStr locals - acc_strs = [header, injIntoList [expr_str, locs_str]] + where + header = "SymClosure" + expr_str = pprExprStr expr + 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 - where header = "LitObj" - lit_str = pprLitStr lit - acc_strs = [header, lit_str] + where + header = "LitObj" + lit_str = pprLitStr lit + acc_strs = [header, lit_str] pprHeapObjStr (SymObj (Symbol sym mb_scls)) = injSpace acc_strs - where header = "SymObj" - var_str = pprVarStr sym - scls_str = (sub . pprSymClosureStr) mb_scls - acc_strs = [header, var_str, scls_str] + where + header = "SymObj" + var_str = pprVarStr sym + scls_str = (sub . pprSymClosureStr) mb_scls + acc_strs = [header, var_str, scls_str] pprHeapObjStr (ConObj dcon vals) = injSpace acc_strs - where header = "ConObj" - dcon_str = pprDataConStr dcon - vals_str = injIntoList (map pprValueStr vals) - acc_strs = [header, dcon_str, vals_str] + where + header = "ConObj" + dcon_str = pprDataConStr dcon + vals_str = injIntoList (map pprValueStr vals) + acc_strs = [header, dcon_str, vals_str] pprHeapObjStr (FunObj params expr locals) = injSpace acc_strs - where header = "FunObj" - prms_str = injIntoList (map pprVarStr params) - expr_str = pprExprStr expr - locs_str = pprLocalsStr locals - acc_strs = [header, prms_str, expr_str, locs_str] + where + header = "FunObj" + prms_str = injIntoList (map pprVarStr params) + expr_str = pprExprStr expr + locs_str = pprLocalsStr locals + acc_strs = [header, prms_str, expr_str, locs_str] -- | 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 + 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 -- | Print `Globals`. pprGlobalsStr :: Globals -> String 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 + 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 -- | Print `Locals`. pprLocalsStr :: Locals -> String 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 + 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 -- | Print `Value`. pprValueStr :: Value -> String pprValueStr (LitVal lit) = injSpace acc_strs - where header = "LitVal" - lit_str = pprLitStr lit - acc_strs = [header, lit_str] + where + header = "LitVal" + lit_str = pprLitStr lit + acc_strs = [header, lit_str] pprValueStr (MemVal addr) = injSpace acc_strs - where header = "MemVal" - ptr_str = pprMemAddrStr addr - acc_strs = [header, ptr_str] + where + header = "MemVal" + ptr_str = pprMemAddrStr addr + acc_strs = [header, ptr_str] -- | Print `Var`. pprVarStr :: Var -> String pprVarStr (Var name ty) = injSpace acc_strs - where header = "Var" - name_str = (sub . pprNameStr) name - type_str = (sub . pprTypeStr) ty - acc_strs = [header, name_str, type_str] + where + header = "Var" + name_str = (sub . pprNameStr) name + type_str = (sub . pprTypeStr) ty + acc_strs = [header, name_str, type_str] -- | Print `Atom`. pprAtomStr :: Atom -> String pprAtomStr (VarAtom var) = injSpace acc_strs - where header = "VarAtom" - var_str = (sub . pprVarStr) var - acc_strs = [header, var_str] + where + header = "VarAtom" + var_str = (sub . pprVarStr) var + acc_strs = [header, var_str] pprAtomStr (LitAtom lit) = injSpace acc_strs - where header = "LitAtom" - lit_str = (sub . pprLitStr) lit - acc_strs = [header, lit_str] + where + header = "LitAtom" + lit_str = (sub . pprLitStr) lit + acc_strs = [header, lit_str] -- | Print `DataCon`. pprDataConStr :: DataCon -> String pprDataConStr (DataCon name ty tys) = injSpace acc_strs - where header = "DataCon" - 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] + where + header = "DataCon" + 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] -- | Print `PrimFun`. pprPrimFunStr :: PrimFun -> String pprPrimFunStr (PrimFun name ty) = injSpace acc_strs - where header = "PrimFun" - name_str = (sub . pprNameStr) name - type_str = (sub . pprTypeStr) ty - acc_strs = [header, name_str, type_str] + where + header = "PrimFun" + name_str = (sub . pprNameStr) name + type_str = (sub . pprTypeStr) ty + acc_strs = [header, name_str, type_str] -- | Print `AltCon`. pprAltConStr :: AltCon -> String pprAltConStr (DataAlt dcon) = injSpace acc_strs - where header = "DataAlt" - dcon_str = (sub . pprDataConStr) dcon - acc_strs = [header, dcon_str] + where + header = "DataAlt" + dcon_str = (sub . pprDataConStr) dcon + acc_strs = [header, dcon_str] pprAltConStr (LitAlt lit) = injSpace acc_strs - where header = "LitAlt" - lit_str = (sub . pprLitStr) lit - acc_strs = [header, lit_str] + where + header = "LitAlt" + lit_str = (sub . pprLitStr) lit + acc_strs = [header, lit_str] pprAltConStr (Default) = "Default" -- | Print `Alt`. pprAltStr :: Alt -> String pprAltStr (Alt acon var expr) = injSpace acc_strs - where header = "Alt" - acon_str = (sub . pprAltConStr) acon - vars_str = injIntoList (map pprVarStr var) - expr_str = (sub . pprExprStr) expr - acc_strs = [header, acon_str, vars_str, expr_str] + where + header = "Alt" + acon_str = (sub . pprAltConStr) acon + vars_str = injIntoList (map pprVarStr var) + expr_str = (sub . pprExprStr) expr + acc_strs = [header, acon_str, vars_str, expr_str] -- | Print a list of `Alt`s. pprAltsStr :: [Alt] -> String @@ -272,79 +300,91 @@ -- | Print `BindRhs`. pprBindRhsStr :: BindRhs -> String pprBindRhsStr (FunForm params expr) = injSpace acc_strs - where header = "FunForm" - prms_str = injIntoList (map pprVarStr params) - expr_str = (sub . pprExprStr) expr - acc_strs = [header, prms_str, expr_str] + where + header = "FunForm" + prms_str = injIntoList (map pprVarStr params) + expr_str = (sub . pprExprStr) expr + acc_strs = [header, prms_str, expr_str] pprBindRhsStr (ConForm dcon args) = injSpace acc_strs - where header = "ConForm" - dcon_str = (sub . pprDataConStr) dcon - args_str = injIntoList (map pprAtomStr args) - acc_strs = [header, dcon_str, args_str] + where + header = "ConForm" + dcon_str = (sub . pprDataConStr) dcon + args_str = injIntoList (map pprAtomStr args) + acc_strs = [header, dcon_str, args_str] -- | Print @(Var, BindRhs)@. pprBindKVStr :: (Var, BindRhs) -> String pprBindKVStr (var, lamf) = (sub . injComma) acc_strs - where var_str = pprVarStr var - lamf_str = pprBindRhsStr lamf - acc_strs = [var_str, lamf_str] + where + var_str = pprVarStr var + lamf_str = pprBindRhsStr lamf + acc_strs = [var_str, lamf_str] -- | Print `Bind`. pprBindStr :: Bind -> String pprBindStr (Bind rec bnd) = injSpace acc_strs - where header = case rec of { Rec -> "Rec"; NonRec -> "NonRec" } - bnds_str = injIntoList (map pprBindKVStr bnd) - acc_strs = [header, bnds_str] + where + header = case rec of { Rec -> "Rec"; NonRec -> "NonRec" } + bnds_str = injIntoList (map pprBindKVStr bnd) + acc_strs = [header, bnds_str] -- | Print `Expr`. pprExprStr :: Expr -> String pprExprStr (Atom atom) = injSpace acc_strs - where header = "Atom" - atom_str = (sub . pprAtomStr) atom - acc_strs = [header, atom_str] + where + header = "Atom" + atom_str = (sub . pprAtomStr) atom + acc_strs = [header, atom_str] pprExprStr (FunApp var args) = injSpace acc_strs - where header = "FunApp" - var_str = (sub . pprVarStr) var - args_str = injIntoList (map pprAtomStr args) - acc_strs = [header, var_str, args_str] + where + header = "FunApp" + var_str = (sub . pprVarStr) var + args_str = injIntoList (map pprAtomStr args) + acc_strs = [header, var_str, args_str] pprExprStr (PrimApp pfun args) = injSpace acc_strs - where header = "PrimApp" - pfun_str = (sub . pprPrimFunStr) pfun - args_str = injIntoList (map pprAtomStr args) - acc_strs = [header, pfun_str, args_str] + where + header = "PrimApp" + pfun_str = (sub . pprPrimFunStr) pfun + args_str = injIntoList (map pprAtomStr args) + acc_strs = [header, pfun_str, args_str] pprExprStr (ConApp dcon args) = injSpace acc_strs - where header = "ConApp" - dcon_str = (sub . pprDataConStr) dcon - args_str = injIntoList (map pprAtomStr args) - acc_strs = [header, dcon_str, args_str] + where + header = "ConApp" + dcon_str = (sub . pprDataConStr) dcon + args_str = injIntoList (map pprAtomStr args) + acc_strs = [header, dcon_str, args_str] pprExprStr (Case expr var alts) = injSpace acc_strs - where header = "Case" - expr_str = (sub . pprExprStr) expr - var_str = (sub . pprVarStr) var - alts_str = pprAltsStr alts - acc_strs = [header, expr_str, var_str, alts_str] + where + header = "Case" + expr_str = (sub . pprExprStr) expr + var_str = (sub . pprVarStr) var + alts_str = pprAltsStr alts + acc_strs = [header, expr_str, var_str, alts_str] pprExprStr (Let bnd expr) = injSpace acc_strs - where header = "Let" - bnd_str = (sub . pprBindStr) bnd - expr_str = (sub . pprExprStr) expr - acc_strs = [header, bnd_str, expr_str] + where + header = "Let" + bnd_str = (sub . pprBindStr) bnd + expr_str = (sub . pprExprStr) expr + acc_strs = [header, bnd_str, expr_str] -- | Print `Type`. NOTE: currently only prints @"__TyPE__"@ because there is -- a lot of `Type` information which makes analysis of dumps hard otherwise. pprTypeStr :: Type -> String -pprTypeStr ty = fst ("__Type__", ty) +pprTypeStr ty = snd ("__Type__", show ty) -- | Print `Code`. pprCodeStr :: Code -> String pprCodeStr (Evaluate expr locals) = injSpace acc_strs - where header = "Evaluate" - expr_str = (sub . pprExprStr) expr - loc_str = (sub . pprLocalsStr) locals - acc_strs = [header, expr_str, loc_str] + where + header = "Evaluate" + expr_str = (sub . pprExprStr) expr + loc_str = (sub . pprLocalsStr) locals + acc_strs = [header, expr_str, loc_str] pprCodeStr (Return val) = injSpace acc_strs - where header = "Return" - val_str = pprValueStr val - acc_strs = [header, val_str] + where + header = "Return" + val_str = pprValueStr val + acc_strs = [header, val_str] -- | Print a list of `Name`s. pprNamesStr :: [Name] -> String @@ -353,15 +393,17 @@ -- | Print `PathCons`. pprPathConsStr :: PathCons -> String pprPathConsStr pathcons = injNewLineSeps5 strs - where strs = map pprConstraintStr (pathconsToList pathcons) + where + strs = map pprConstraintStr (pathconsToList pathcons) -- | Print `PathCond`. 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] + 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]