diff --git a/SSTG.cabal b/SSTG.cabal --- a/SSTG.cabal +++ b/SSTG.cabal @@ -1,5 +1,5 @@ name: SSTG -version: 0.1.1.3 +version: 0.1.1.4 synopsis: STG Symbolic Execution description: Prototype of STG-based Symbolic Execution for Haskell. homepage: https://github.com/AntonXue/SSTG#readme @@ -19,7 +19,6 @@ , SSTG.Core , SSTG.Core.Language , SSTG.Core.Language.Naming - , SSTG.Core.Language.Support , SSTG.Core.Language.Syntax , SSTG.Core.Language.Typing , SSTG.Core.Preprocessing @@ -32,6 +31,7 @@ , SSTG.Core.Execution.Engine , SSTG.Core.Execution.Rules , SSTG.Core.Execution.Stepping + , SSTG.Core.Execution.Support , SSTG.Utils , SSTG.Utils.Printing , SSTG.Utils.FileIO diff --git a/app/Main.hs b/app/Main.hs --- a/app/Main.hs +++ b/app/Main.hs @@ -4,7 +4,7 @@ import qualified Data.Char as C import qualified Data.List as L -import qualified Data.Map as M +import qualified Data.Map as M import System.Environment import Text.Read @@ -14,17 +14,17 @@ trimSlash :: String -> String trimSlash str = case trim str of - "" -> "" + "" -> "" trimmed -> case last trimmed of '/' -> trimSlash (init trimmed) - _ -> trimmed + _ -> trimmed matchArg :: String -> [String] -> (String -> a) -> a -> a matchArg tgt args fun def = case L.elemIndex tgt args of + Just i -> if i >= length args + then error ("Invalid use of " ++ tgt) + else fun (args !! (i + 1)) -- fun (args !! (i + 1)) Nothing -> def - Just i -> if i >= length args - then error ("Invalid use of " ++ tgt) - else fun (args !! (i + 1)) -- fun (args !! (i + 1)) parseStepCount :: [String] -> Int parseStepCount args = matchArg "--n" args read 200 @@ -32,22 +32,22 @@ parseStepType :: [String] -> StepType parseStepType args = case matched of { Just t -> t; Nothing -> BFS } where matched = matchArg "--method" args (\a -> M.lookup a types) Nothing - types = M.fromList [ ("bfs", BFS) + types = M.fromList [ ("bfs", BFS) , ("bfs-log", BFSLogged) - , ("dfs", DFS) + , ("dfs", DFS) , ("dfs-log", DFSLogged) ] parseDumpDir :: [String] -> Maybe FilePath parseDumpDir args = case matchArg "--dump" args (readMaybe . show) Nothing of - Nothing -> Nothing Just raw -> case trimSlash raw of "" -> error ("Invalid use of " ++ raw) ok -> Just ok + Nothing -> Nothing parseFlags :: [String] -> RunFlags parseFlags args = RunFlags { flag_step_count = parseStepCount args - , flag_step_type = parseStepType args - , flag_dump_dir = parseDumpDir args } + , flag_step_type = parseStepType args + , flag_dump_dir = parseDumpDir args } injDumpLocs :: String -> Int -> FilePath -> [FilePath] injDumpLocs entry n dir = map (\i -> start ++ (show i) ++ ".txt") [1..n] @@ -58,31 +58,31 @@ -- Get command line arguments. (proj:src:tail_args) <- getArgs -- Make bindings. - binds <- mkTargetBinds proj src + bindss <- mkTargetBindsList proj src -- Configure entry. let entry = if length tail_args > 0 then tail_args !! 0 else "main" -- Get the flags. let flags = parseFlags tail_args -- Do the loading. - let load_result = loadStateEntry entry (Program binds) - putStrLn $ "binds: " ++ show (length binds) + let load_result = loadStateEntry entry (Program bindss) + putStrLn $ "binds: " ++ show (length bindss) -- Get the state from the loader. state <- case load_result of - LoadError str -> error str - LoadOkay state -> return state + LoadError str -> error str + LoadOkay state -> return state LoadGuess state cands -> do putStrLn "Other possible candidates:" putStrLn $ show cands return state putStrLn $ show flags -- Execution! - let ldss = execute flags state + let ldss = execute flags state case flag_dump_dir flags of - -- Dump to terminal. - Nothing -> mapM_ (putStrLn . pprLivesDeadsStr) ldss -- Dump to file. Just dir -> do let locs = injDumpLocs entry (length ldss) dir putStrLn $ show (length ldss) mapM_ (\(fp, lds) -> writePrettyState fp lds) (zip locs ldss) + -- Dump to terminal. + Nothing -> mapM_ (putStrLn . pprLivesDeadsStr) ldss 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 @@ -3,9 +3,11 @@ ( module SSTG.Core.Execution.Engine , module SSTG.Core.Execution.Rules , module SSTG.Core.Execution.Stepping + , module SSTG.Core.Execution.Support ) where import SSTG.Core.Execution.Engine import SSTG.Core.Execution.Rules import SSTG.Core.Execution.Stepping +import SSTG.Core.Execution.Support 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,11 +10,13 @@ ) where import SSTG.Core.Language + import SSTG.Core.Execution.Stepping +import SSTG.Core.Execution.Support -- | Load Result data LoadResult = LoadOkay State - | LoadGuess State [Bind] + | LoadGuess State [Binds] | LoadError String deriving (Show, Eq, Read) @@ -27,7 +29,7 @@ -- | Load from a specified entry point. loadStateEntry :: String -> Program -> LoadResult -loadStateEntry entry (Program bnds) = if length matches == 0 +loadStateEntry entry (Program bindss) = if length matches == 0 then LoadError ("No entry candidates found for: [" ++ entry ++ "]") else if length others == 0 then LoadOkay state @@ -39,14 +41,14 @@ stack = empty_stack -- Globals and Heap are loaded together. They are still beta forms now. heap0 = empty_heap - (glist, heap1, bnd_addrss) = initGlobals bnds heap0 + (glist, heap1, binds_addrss) = initGlobals bindss heap0 globals0 = insertGlobalsList glist empty_globals - (heap2, localss) = liftBinds bnd_addrss globals0 heap1 - bnd_locs = zip bnds localss + (heap2, localss) = liftBindsList binds_addrss globals0 heap1 + binds_locs = zip bindss localss -- Code loading. Completes heap and globals with symbolic injection. - matches = entryMatches entry bnd_locs - ((tgt_bnd, tgt_loc):others) = matches - ((tgt_var, tgt_rhs):_) = lhsMatches entry tgt_bnd + matches = entryMatches entry binds_locs + ((tgt_binds, tgt_loc):others) = matches + ((tgt_var, tgt_rhs):_) = lhsMatches entry tgt_binds (code, globals, heap) = loadCode tgt_var tgt_rhs tgt_loc globals0 heap2 -- Ready to fill the state. state0 = State { state_status = status @@ -58,44 +60,44 @@ , state_paths = empty_pathcons } -- Gather information on all variables. - state = state0 { state_names = allNames state0 } + state = state0 { state_names = allNames (Program bindss) } --- | Allocate Bind -allocBind :: Bind -> Heap -> (Heap, [MemAddr]) -allocBind (Bind _ pairs) heap = (heap', addrs) +-- | Allocate Binds +allocBinds :: Binds -> Heap -> (Heap, [MemAddr]) +allocBinds (Binds _ kvs) heap = (heap', addrs) where - hfakes = map (const Blackhole) pairs + hfakes = map (const Blackhole) kvs (heap', addrs) = allocHeapList hfakes heap --- | Allocate List of `Bind`s -allocBindList :: [Bind] -> Heap -> (Heap, [[MemAddr]]) -allocBindList [] heap = (heap, []) -allocBindList (b:bs) heap = (heapf, addrs : as) +-- | Allocate List of `Binds`s +allocBindsList :: [Binds] -> Heap -> (Heap, [[MemAddr]]) +allocBindsList [] heap = (heap, []) +allocBindsList (b:bs) heap = (heapf, addrs : as) where - (heap', addrs) = allocBind b heap - (heapf, as) = allocBindList bs heap' + (heap', addrs) = allocBinds b heap + (heapf, as) = allocBindsList bs heap' --- | Bind Address to Name Values -bndAddrsToVarVals :: (Bind, [MemAddr]) -> [(Var, Value)] -bndAddrsToVarVals (Bind _ rhss, addrs) = zip (map fst rhss) mem_vals +-- | Binds Address to Name Values +bindsAddrsToVarVals :: (Binds, [MemAddr]) -> [(Var, Value)] +bindsAddrsToVarVals (Binds _ kvs, addrs) = zip (map fst kvs) mem_vals where mem_vals = map (\a -> MemVal a) addrs -- | Initialize Globals -initGlobals :: [Bind] -> Heap -> ([(Var, Value)], Heap, [(Bind, [MemAddr])]) -initGlobals bnds heap = (var_vals, heap', bnd_addrss) +initGlobals :: [Binds] -> Heap -> ([(Var, Value)], Heap, [(Binds, [MemAddr])]) +initGlobals bindss heap = (var_vals, heap', binds_addrss) where - (heap', addrss) = allocBindList bnds heap - bnd_addrss = zip bnds addrss - var_vals = concatMap bndAddrsToVarVals bnd_addrss + (heap', addrss) = allocBindsList bindss heap + binds_addrss = zip bindss addrss + var_vals = concatMap bindsAddrsToVarVals binds_addrss -- | Force Atom Lookup forceLookupValue :: Atom -> Locals -> Globals -> Value forceLookupValue (LitAtom lit) _ _ = LitVal lit forceLookupValue (VarAtom var) locals globals = case lookupValue var locals globals of - Nothing -> LitVal BlankAddr -- An error, but I want to not crash. Just val -> val + Nothing -> LitVal BlankAddr -- An error, but I want to not crash. -- | Full Rhs Object forceRhsObj :: BindRhs -> Locals -> Globals -> HeapObj @@ -104,38 +106,38 @@ where arg_vals = map (\a -> forceLookupValue a locals globals) args --- | Lift `Bind`. -liftBind :: (Bind, [MemAddr]) -> Globals -> Heap -> (Heap, Locals) -liftBind (Bind rec pairs, addrs) globals heap = (heap', locals) +-- | Lift `Binds`. +liftBinds :: (Binds, [MemAddr]) -> Globals -> Heap -> (Heap, Locals) +liftBinds (Binds rec kvs, addrs) globals heap = (heap', locals) where - (vars, rhss) = unzip pairs + (vars, rhss) = unzip kvs mem_vals = map (\a -> MemVal a) addrs e_locs = empty_locals r_locs = insertLocalsList (zip vars mem_vals) e_locs locals = case rec of { Rec -> r_locs; NonRec -> e_locs } hobjs = map (\r -> forceRhsObj r locals globals) rhss - heap' = insertHeapList (zip addrs hobjs) heap + heap' = insertHeapObjList (zip addrs hobjs) heap --- | Lift Bind List -liftBinds :: [(Bind, [MemAddr])] -> Globals -> Heap -> (Heap, [Locals]) -liftBinds [] _ heap = (heap, []) -liftBinds (bm:bms) globals heap = (heapf, locals : ls) +-- | Lift Binds List +liftBindsList :: [(Binds, [MemAddr])] -> Globals -> Heap -> (Heap, [Locals]) +liftBindsList [] _ heap = (heap, []) +liftBindsList (bm:bms) globals heap = (heapf, locals : ls) where - (heap', locals) = liftBind bm globals heap - (heapf, ls) = liftBinds bms globals heap' + (heap', locals) = liftBinds bm globals heap + (heapf, ls) = liftBindsList bms globals heap' -- | Return a sub-list of binds in which the entry candidate appears. -entryMatches :: String -> [(Bind, Locals)] -> [(Bind, Locals)] -entryMatches entry bnd_locs = filter (bindFilter entry) bnd_locs +entryMatches :: String -> [(Binds, Locals)] -> [(Binds, Locals)] +entryMatches entry binds_locs = filter (isEntryBinds entry) binds_locs --- | Bind Filtering -bindFilter :: String -> (Bind, Locals) -> Bool -bindFilter entry (bnd, _) = lhsMatches entry bnd /= [] +-- | Binds Filtering +isEntryBinds :: String -> (Binds, Locals) -> Bool +isEntryBinds entry (binds, _) = lhsMatches entry binds /= [] --- | Sub-Binds String Match -lhsMatches :: String -> Bind -> [(Var, BindRhs)] -lhsMatches st (Bind _ pairs) = - filter (\(var, _) -> st == (nameOccStr . varName) var) pairs +-- | Sub-Bindss String Match +lhsMatches :: String -> Binds -> [(Var, BindRhs)] +lhsMatches st (Binds _ kvs) = + filter (\(var, _) -> st == (nameOccStr . varName) var) kvs -- | Load Code loadCode :: Var -> BindRhs -> Locals -> Globals -> Heap -> (Code,Globals,Heap) diff --git a/src/SSTG/Core/Execution/Rules.hs b/src/SSTG/Core/Execution/Rules.hs --- a/src/SSTG/Core/Execution/Rules.hs +++ b/src/SSTG/Core/Execution/Rules.hs @@ -7,6 +7,8 @@ import SSTG.Core.Language +import SSTG.Core.Execution.Support + -- | `Rule`s that are applied during STG reduction. data Rule = RuleAtomLit | RuleAtomLitPtr | RuleAtomValPtr | RuleAtomUnInt | RulePrimApp @@ -66,7 +68,7 @@ -- | `Value` to `Lit`. valueToLit :: Value -> Lit valueToLit (LitVal lit) = lit -valueToLit (MemVal addr) = AddrLit (addrInt addr) +valueToLit (MemVal addr) = AddrLit (memAddrInt addr) -- | Uneven `zip` of two `List`s, with the leftover stored. unevenZip :: [a] -> [b] -> ([(a, b)], Either [a] [b]) @@ -140,26 +142,26 @@ LiftAct hobj locals' globals' heap' confs' = liftBindRhs pass_in LiftAct hos localsf globalsf heapf confsf = liftBindRhsList pass_rest --- | Lift `Bind`. -liftBind :: LiftAct Bind -> LiftAct () -liftBind (LiftAct (Bind NonRec bnd) locals globals heap confs) = pass_out +-- | Lift `Binds`. +liftBinds :: LiftAct Binds -> LiftAct () +liftBinds (LiftAct (Binds NonRec kvs) locals globals heap confs) = pass_out where (heapf, addrs) = allocHeapList hobjs heap' mem_vals = map MemVal addrs - localsf = insertLocalsList (zip (map fst bnd) mem_vals) locals' - pass_in = LiftAct (map snd bnd) locals globals heap confs + localsf = insertLocalsList (zip (map fst kvs) mem_vals) locals' + pass_in = LiftAct (map snd kvs) locals globals heap confs pass_out = LiftAct () localsf globals' heapf confs' LiftAct hobjs locals' globals' heap' confs' = liftBindRhsList pass_in -liftBind (LiftAct (Bind Rec bnd) locals globals heap confs) = pass_out +liftBinds (LiftAct (Binds Rec kvs) locals globals heap confs) = pass_out where - hfakes = map (const Blackhole) bnd + hfakes = map (const Blackhole) kvs -- Allocate dummy BLACKHOLEs (heap', addrs) = allocHeapList hfakes heap mem_vals = map MemVal addrs -- Use the reigstered loca BLACKHOLEs to construct the locals closure. - locals' = insertLocalsList (zip (map fst bnd) mem_vals) locals - heapf = insertHeapList (zip addrs hobjs) heap'' - pass_in = LiftAct (map snd bnd) locals' globals heap' confs + locals' = insertLocalsList (zip (map fst kvs) mem_vals) locals + heapf = insertHeapObjList (zip addrs hobjs) heap'' + pass_in = LiftAct (map snd kvs) locals' globals heap' confs pass_out = LiftAct () localsf globals' heapf confs' LiftAct hobjs localsf globals' heap'' confs' = liftBindRhsList pass_in @@ -195,8 +197,8 @@ mem_vals = map MemVal addrs kvs = (cvar, MemVal addr) : zip params mem_vals locals' = insertLocalsList kvs locals - mxpr = Atom (VarAtom mvar) - conss = [Constraint (ac, params) mxpr locals' True] + mexpr = Atom (VarAtom mvar) + conss = [Constraint (ac, params) mexpr locals' True] confs' = snames ++ confs pass_out = LiftAct (expr, conss) locals' globals heap' confs' @@ -257,7 +259,7 @@ | Evaluate (PrimApp pfun args) locals <- code = let pass_in = LiftAct args locals globals heap confs LiftAct vals locals' globals' heap' confs' = liftAtomList pass_in - eval = SymLitEval pfun (map valueToLit vals) + eval = LitEval pfun (map valueToLit vals) in Just (RulePrimApp ,[state { state_heap = heap' , state_globals = globals' @@ -338,9 +340,9 @@ , state_names = confs' }]) -- Rule Let - | Evaluate (Let bnd expr) locals <- code = - let pass_in = LiftAct bnd locals globals heap confs - LiftAct _ locals' globals' heap' confs' = liftBind pass_in + | Evaluate (Let binds expr) locals <- code = + let pass_in = LiftAct binds locals globals heap confs + LiftAct _ locals' globals' heap' confs' = liftBinds pass_in in Just (RuleLet ,[state { state_heap = heap' , state_globals = globals' @@ -414,7 +416,7 @@ let frame = UpdateFrame addr in Just (RuleUpdateCThunk ,[state { state_stack = pushStack frame stack - , state_heap = insertHeap (addr, Blackhole) heap + , state_heap = insertHeapObj (addr, Blackhole) heap , state_code = Evaluate expr fun_locs }]) -- Rule Update Frame Delete Lit @@ -422,7 +424,7 @@ , Return (LitVal lit) <- code = Just (RuleUpdateDLit ,[state { state_stack = stack' - , state_heap = insertHeap (frm_addr, LitObj lit) heap + , state_heap = insertHeapObj (frm_addr, LitObj lit) heap , state_code = Return (LitVal lit) }]) -- Rule Update Frame Delete Val Pointer @@ -432,24 +434,24 @@ , isHeapValueForm hobj = Just (RuleUpdateDValPtr ,[state { state_stack = stack' - , state_heap = insertHeap (frm_addr, AddrObj addr) heap + , state_heap = insertHeapRedir (frm_addr, addr) heap , state_code = Return (MemVal addr) }]) -- Rule Case Frame Create Case Non LitVal or MemVal - | Evaluate (Case mxpr cvar alts) locals <- code - , not (isExprValueForm mxpr locals globals heap) = + | Evaluate (Case mexpr cvar alts) locals <- code + , not (isExprValueForm mexpr locals globals heap) = let frame = CaseFrame cvar alts locals in Just (RuleCaseCCaseNonVal ,[state { state_stack = pushStack frame stack - , state_code = Evaluate mxpr locals }]) + , state_code = Evaluate mexpr locals }]) -- Rule Case Frame Delete Lit | Just (CaseFrame cvar alts frm_locs, stack') <- popStack stack , Return (LitVal lit) <- code = - let mxpr = Atom (LitAtom lit) + let cexpr = Case (Atom (LitAtom lit)) cvar alts in Just (RuleCaseDLit ,[state { state_stack = stack' - , state_code = Evaluate (Case mxpr cvar alts) frm_locs }]) + , state_code = Evaluate cexpr frm_locs }]) -- Rule Case Frame Delete Heap Value | Just (CaseFrame cvar alts frm_locs, stack') <- popStack stack @@ -458,11 +460,11 @@ , isHeapValueForm hobj = let vname = freshSeededName (varName cvar) confs vvar = Var vname (varType cvar) - mxpr = Atom (VarAtom vvar) + cexpr = Case (Atom (VarAtom vvar)) cvar alts frm_locs' = insertLocals (vvar, MemVal addr) frm_locs in Just (RuleCaseDValPtr ,[state { state_stack = stack' - , state_code = Evaluate (Case mxpr cvar alts) frm_locs' + , state_code = Evaluate cexpr frm_locs' , state_names = vname : confs }]) -- Rule Apply Frame Create Function Thunk 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 @@ -37,20 +37,20 @@ where status = state_status state status' = case mb_id of + Just int -> incStatusSteps (updateStatusId int status) Nothing -> incStatusSteps status - Just id' -> incStatusSteps (updateStatusId id' status) -- | Given a list of `State` along with its list of past `Rule` reductions, -- apply STG reduction. If reduction yields `Nothing`, simply return itself. step :: ([Rule], State) -> [([Rule], State)] step (hist, start) = case reduce start of - Nothing -> [(hist, start)] Just (rule, results) -> let trace = hist ++ [rule] mb_id = if length results > 1 then Just (hash trace) else Nothing in map (\s -> (trace, incStatus mb_id s)) results + Nothing -> [(hist, start)] -- | This is what we use the `<*>` over. pass :: [LiveState] -> ([LiveState], [DeadState] -> [DeadState]) diff --git a/src/SSTG/Core/Execution/Support.hs b/src/SSTG/Core/Execution/Support.hs new file mode 100644 --- /dev/null +++ b/src/SSTG/Core/Execution/Support.hs @@ -0,0 +1,340 @@ +-- | Symbolic STG Execution Support Architecture +module SSTG.Core.Execution.Support + ( SymbolicT(..) + , fmap + , pure + , (<*>) + , return + , (>>=) + + , State(..) + , Symbol(..) + , Status(..) + , Stack + , Frame(..) + , MemAddr + , Value(..) + , Locals + , Heap + , HeapObj(..) + , Globals + , Code(..) + , PathCons + , Constraint(..) + + , null_addr + , memAddrInt + + , init_status + , incStatusSteps + , updateStatusId + + , empty_stack + , popStack + , pushStack + , stackToList + + , empty_locals + , lookupLocals + , insertLocals + , insertLocalsList + , localsToList + + , empty_heap + , lookupHeap + , insertHeapObj + , insertHeapObjList + , insertHeapRedir + , allocHeap + , allocHeapList + , heapToList + + , empty_globals + , lookupGlobals + , insertGlobals + , insertGlobalsList + , globalsToList + + , empty_pathcons + , insertPathCons + , insertPathConsList + , pathconsToList + + , lookupValue + , vlookupHeap + , memAddrType + ) where + +import SSTG.Core.Language + +import qualified Data.Map as M + +-- | Symbolic Transformation represents transformations applied to some +-- State`(s). This is useful in allowing us to transfer from different actions +-- within the engine. +newtype SymbolicT s a = SymbolicT { run :: s -> (s, a) } + +-- | Functor instance of Symbolic Transformation. +instance Functor (SymbolicT s) where + fmap f st = SymbolicT (\s0 -> let (s1, a1) = (run st) s0 in (s1, f a1)) + +-- | Applicative instance of Symbolic Transformation. +instance Applicative (SymbolicT s) where + pure a = SymbolicT (\s -> (s, a)) + + sf <*> st = SymbolicT (\s0 -> let (s1, a1) = (run st) s0 + (s2, f2) = (run sf) s1 in (s2, f2 a1)) + +-- | Monad instance of Symbolic Transformation. +instance Monad (SymbolicT s) where + return a = pure a + + st >>= fs = SymbolicT (\s0 -> let (s1, a1) = (run st) s0 + (s2, a2) = (run (fs a1)) s1 in (s2, a2)) + +-- | `State` contains the information necessary to perform symbolic execution. +-- Eval/Apply graph reduction semantics are used. +data State = State { state_status :: !Status + , state_stack :: !Stack + , state_heap :: !Heap + , state_globals :: !Globals + , state_code :: !Code + , state_names :: ![Name] + , state_paths :: !PathCons + } deriving (Show, Eq, Read) + +-- | Symbolic variables. The @Maybe (Expr, Locals)@ can be used to trace the +-- source from which the symbolic variable was generated. For instance, this is +-- useful during symbolic function application. +data Symbol = Symbol Var (Maybe (Expr, Locals)) deriving (Show, Eq, Read) + +-- | State status. +data Status = Status { status_id :: !Int + , status_parent :: !Int + , status_steps :: !Int + } deriving (Show, Eq, Read) + +-- | Execution stack used in graph reduction semnatics. +newtype Stack = Stack [Frame] deriving (Show, Eq, Read) + +-- | Frames of a stack. +data Frame = CaseFrame Var [Alt] Locals + | ApplyFrame [Atom] Locals + | UpdateFrame MemAddr + deriving (Show, Eq, Read) + +-- | Memory address for things on the `Heap`. +newtype MemAddr = MemAddr Int deriving (Show, Eq, Read, Ord) + +-- | A `Value` is something that we aim to reduce our current expression down +-- into. `MemAddr` is a pointer to an object on the heap, such as `FunObj` or +-- `ConObj`, which are "returned" from expression evaluation in this form. +data Value = LitVal Lit + | MemVal MemAddr + deriving (Show, Eq, Read) + +-- | Locals binds a `Var`'s `Name` to its some `Value`. +newtype Locals = Locals (M.Map Name Value) deriving (Show, Eq, Read) + +-- | Heaps map `MemAddr` to `HeapObj`, while keeping track of the last address +-- that was allocated. This allows us to consistently allocate fresh addresses +-- on the `Heap`. +data Heap = Heap (M.Map MemAddr (Either MemAddr HeapObj)) MemAddr + deriving (Show, Eq, Read) + +-- | Heap objects. +data HeapObj = LitObj Lit + | SymObj Symbol + | ConObj DataCon [Value] + | FunObj [Var] Expr Locals + | Blackhole + deriving (Show, Eq, Read) + +-- | Globals are statically loaded at the time when a `State` is loaded. +-- However, because uninterpreted / out-of-scope variables are made symbolic +-- at runtime, it can be modified during execution. +newtype Globals = Globals (M.Map Name Value) deriving (Show, Eq, Read) + +-- | Evaluation of the current expression. We are either evaluating, or ready +-- to return with some `Value`. +data Code = Evaluate Expr Locals + | Return Value + deriving (Show, Eq, Read) + +-- | Path constraints are the conjunctive normal form of `Constraint`s. +newtype PathCons = PathCons [Constraint] deriving (Show, Eq, Read) + +-- | Constraints denote logical paths taken in program execution thus far. +data Constraint = Constraint (AltCon, [Var]) Expr Locals Bool + deriving (Show, Eq, Read) + +-- Simple functions that require only the immediate data structure. + +-- | Null `MemAddr`. +null_addr :: MemAddr +null_addr = MemAddr 0 + +-- | `MemAddr`'s `Int` value. +memAddrInt :: MemAddr -> Int +memAddrInt (MemAddr int) = int + +-- | Initial `Status`. +init_status :: Status +init_status = Status { status_id = 1 + , status_parent = 0 + , status_steps = 0 } + +-- | Increment `Status` steps. +incStatusSteps :: Status -> Status +incStatusSteps status = status { status_steps = (status_steps status) + 1 } + +-- | Update the `Status` id. +updateStatusId :: Int -> Status -> Status +updateStatusId int status = status { status_id = int + , status_parent = status_id status } + +-- | Empty `Stack. +empty_stack :: Stack +empty_stack = Stack [] + +-- | `Stack` pop. +popStack :: Stack -> Maybe (Frame, Stack) +popStack (Stack []) = Nothing +popStack (Stack (frame:frames)) = Just (frame, Stack frames) + +-- | `Stack` push. +pushStack :: Frame -> Stack -> Stack +pushStack frame (Stack frames) = Stack (frame : frames) + +-- | `Stack` as list of `Frame`s. +stackToList :: Stack -> [Frame] +stackToList (Stack frames) = frames + +-- | Empty `Locals`. +empty_locals :: Locals +empty_locals = Locals M.empty + +-- | `Locals` lookup. +lookupLocals :: Var -> Locals -> Maybe Value +lookupLocals var (Locals lmap) = M.lookup (varName var) lmap + +-- | `Locals` insertion. +insertLocals :: (Var, Value) -> Locals -> Locals +insertLocals (k, v) (Locals lmap) = Locals (M.insert (varName k) v lmap) + +-- | List insertion into `Locals`. +insertLocalsList :: [(Var, Value)] -> Locals -> Locals +insertLocalsList kvs locals = foldr insertLocals locals kvs + +-- | `Locals` to key value pairs. +localsToList :: Locals -> [(Name, Value)] +localsToList (Locals lmap) = M.toList lmap + +-- | Empty `Heap`. +empty_heap :: Heap +empty_heap = Heap M.empty null_addr + +-- | `Heap` lookup. +lookupHeap :: MemAddr -> Heap -> Maybe HeapObj +lookupHeap addr (Heap hmap prev) = case M.lookup addr hmap of + Just (Left redir) -> lookupHeap redir (Heap hmap prev) + Just (Right hobj) -> Just hobj + Nothing -> Nothing + +-- | `Heap` direct insertion at a specific `MemAddr`. +insertHeapObj :: (MemAddr, HeapObj) -> Heap -> Heap +insertHeapObj (k, v) (Heap hmap prev) = Heap (M.insert k (Right v) hmap) prev + +-- | Insert a list of `HeapObj` at specified `MemAddr` locations. +insertHeapObjList :: [(MemAddr, HeapObj)] -> Heap -> Heap +insertHeapObjList kvs heap = foldr insertHeapObj heap kvs + +-- | Insert a redirection `MemAddr` into the `Heap`. +insertHeapRedir :: (MemAddr, MemAddr) -> Heap -> Heap +insertHeapRedir (a, r) (Heap hmap prev) = Heap (M.insert a (Left r) hmap) prev + +-- | `Heap` allocation. Updates the last `MemAddr` kept in the `Heap`. +allocHeap :: HeapObj -> Heap -> (Heap, MemAddr) +allocHeap hobj (Heap hmap prev) = (heap', addr) + where + addr = MemAddr ((memAddrInt prev) + 1) + heap' = insertHeapObj (addr, hobj) (Heap hmap addr) + +-- | Allocate a list of `HeapObj` in a `Heap`, returning in the same order the +-- `MemAddr` at which they have been allocated at. +allocHeapList :: [HeapObj] -> Heap -> (Heap, [MemAddr]) +allocHeapList [] heap = (heap, []) +allocHeapList (hobj:hobjs) heap = (heapf, addr : as) + where + (heap', addr) = allocHeap hobj heap + (heapf, as) = allocHeapList hobjs heap' + +-- | `Heap` to key value pairs. +heapToList :: Heap -> [(MemAddr, Either MemAddr HeapObj)] +heapToList (Heap hmap _) = M.toList hmap + +-- | Empty `Globals`. +empty_globals :: Globals +empty_globals = Globals M.empty + +-- | `Globals` lookup. +lookupGlobals :: Var -> Globals -> Maybe Value +lookupGlobals var (Globals gmap) = M.lookup (varName var) gmap + +-- | `Globals` insertion. +insertGlobals :: (Var, Value) -> Globals -> Globals +insertGlobals (k, v) (Globals gmap) = Globals (M.insert (varName k) v gmap) + +-- | Insert a list of `Var` and `Value` pairs into `Globals`. This would +-- typically occur for new symbolic variables created from uninterpreted / +-- out-of-scope variables during runtime. +insertGlobalsList :: [(Var, Value)] -> Globals -> Globals +insertGlobalsList kvs globals = foldr insertGlobals globals kvs + +-- | `Globals` to key value pairs. +globalsToList :: Globals -> [(Name, Value)] +globalsToList (Globals gmap) = M.toList gmap + +-- | Empty `PathCons`. +empty_pathcons :: PathCons +empty_pathcons = PathCons [] + +-- | `PathCons` insertion. +insertPathCons :: Constraint -> PathCons -> PathCons +insertPathCons cons (PathCons conss) = PathCons (cons : conss) + +-- | Insert a list of `Constraint`s into a `PathCons`. +insertPathConsList :: [Constraint] -> PathCons -> PathCons +insertPathConsList conss pathcons = foldr insertPathCons pathcons conss + +-- | `PathCons` to list of `Constraint`s. +pathconsToList :: PathCons -> [Constraint] +pathconsToList (PathCons conss) = conss + +-- Complex functions that involve multiple data structures. + +-- | `Value` lookup from the `Locals` first, then `Globals`. +lookupValue :: Var -> Locals -> Globals -> Maybe Value +lookupValue var locals globals = case lookupLocals var locals of + Just val -> Just val + Nothing -> lookupGlobals var globals + +-- | `Heap` lookup. Returns the corresponding `MemAddr` and `HeapObj` if found. +vlookupHeap :: Var -> Locals -> Globals -> Heap -> Maybe (MemAddr, HeapObj) +vlookupHeap var locals globals heap = do + val <- lookupValue var locals globals + case val of + LitVal _ -> Nothing + MemVal addr -> lookupHeap addr heap >>= \hobj -> Just (addr, hobj) + +-- | Type of `HeapObj` held at `MemAddr`, if found. +memAddrType :: MemAddr -> Heap -> Maybe Type +memAddrType addr heap = do + hobj <- lookupHeap addr heap + case hobj of + LitObj lit -> Just (litType lit) + SymObj (Symbol svar _) -> Just (varType svar) + ConObj dcon _ -> Just (dataConType dcon) + FunObj ps expr _ -> Just (foldr FunTy (exprType expr) (map varType ps)) + Blackhole -> Just Bottom + 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,13 +1,11 @@ -- | Export Module for SSTG.Syntax module SSTG.Core.Language ( module SSTG.Core.Language.Naming - , module SSTG.Core.Language.Support , module SSTG.Core.Language.Syntax , module SSTG.Core.Language.Typing ) where import SSTG.Core.Language.Naming -import SSTG.Core.Language.Support import SSTG.Core.Language.Syntax import SSTG.Core.Language.Typing diff --git a/src/SSTG/Core/Language/Naming.hs b/src/SSTG/Core/Language/Naming.hs --- a/src/SSTG/Core/Language/Naming.hs +++ b/src/SSTG/Core/Language/Naming.hs @@ -1,6 +1,9 @@ -- | Naming Module module SSTG.Core.Language.Naming ( allNames + , varName + , nameOccStr + , nameInt , freshString , freshName , freshSeededName @@ -8,156 +11,107 @@ , freshSeededNameList ) where -import SSTG.Core.Language.Support import SSTG.Core.Language.Syntax import qualified Data.List as L import qualified Data.Set as S -- | All `Name`s in a `State`. -allNames :: State -> [Name] -allNames state = L.nub acc_ns - where - stack_ns = stackNames (state_stack state) - heap_ns = heapNames (state_heap state) - glbls_ns = globalsNames (state_globals state) - expr_ns = codeNames (state_code state) - pcons_ns = pconsNames (state_paths state) - acc_ns = stack_ns ++ heap_ns ++ glbls_ns ++ expr_ns ++ pcons_ns - --- | `Name`s in a `Stack`. -stackNames :: Stack -> [Name] -stackNames stack = concatMap frameNames (stackToList stack) - --- | `Name`s in a `Frame`. -frameNames :: Frame -> [Name] -frameNames (UpdateFrame _) = [] -frameNames (ApplyFrame as ls) = localsNames ls ++ concatMap atomNames as -frameNames (CaseFrame var alts ls) = localsNames ls ++ concatMap altNames alts - ++ varNames var - --- | `Name`s in an `Alt`. -altNames :: Alt -> [Name] -altNames (Alt _ vars expr) = concatMap varNames vars ++ exprNames expr - --- | `Name`s in the `Locals` -localsNames :: Locals -> [Name] -localsNames locals = map fst (localsToList locals) +allNames :: Program -> [Name] +allNames (Program bindss) = concatMap bindsNames bindss --- | `Name`s in the `Heap`. -heapNames :: Heap -> [Name] -heapNames heap = concatMap (heapObjNames . snd) (heapToList heap) +-- | `Name`s in a `Binds`. +bindsNames :: Binds -> [Name] +bindsNames (Binds _ kvs) = lhs ++ rhs + where + lhs = concatMap (varNames . fst) kvs + rhs = concatMap (bindRhsNames . snd) kvs --- | `Name`s in a `HeapObj`. -heapObjNames :: HeapObj -> [Name] -heapObjNames (AddrObj _) = [] -heapObjNames (Blackhole) = [] -heapObjNames (LitObj _) = [] -heapObjNames (SymObj sym) = symbolNames sym -heapObjNames (ConObj dcon _) = dataNames dcon -heapObjNames (FunObj ps expr locs) = exprNames expr ++ localsNames locs - ++ concatMap varNames ps +-- | A `Var`'s `Name`. Not to be confused with the other function. +varName :: Var -> Name +varName (Var name _) = name --- | `Name`s in a `Symbol`. -symbolNames :: Symbol -> [Name] -symbolNames (Symbol sym mb_scls) = varNames sym ++ scls_ns - where - scls_ns = case mb_scls of - Nothing -> [] - Just (e, l) -> exprNames e ++ localsNames l +-- | `Name`s in a `Var`. +varNames :: Var -> [Name] +varNames (Var name ty) = name : typeNames ty -- | `Name`s in a `BindRhs`. bindRhsNames :: BindRhs -> [Name] bindRhsNames (FunForm prms expr) = concatMap varNames prms ++ exprNames expr bindRhsNames (ConForm dcon args) = concatMap atomNames args ++ dataNames dcon --- | `Name`s in a `Var`. -varNames :: Var -> [Name] -varNames (Var n t) = n : typeNames t - --- | `Name`s in an `Atom`. -atomNames :: Atom -> [Name] -atomNames (LitAtom _) = [] -atomNames (VarAtom var) = varNames var - --- | `Name`s in `Globals`. -globalsNames :: Globals -> [Name] -globalsNames globals = map fst (globalsToList globals) - --- | `Name`s in the current evaluation `Code`. -codeNames :: Code -> [Name] -codeNames (Return _) = [] -codeNames (Evaluate expr locals) = exprNames expr ++ localsNames locals - -- | `Name`s in an `Expr`. exprNames :: Expr -> [Name] exprNames (Atom atom) = atomNames atom -exprNames (Let bnd expr) = exprNames expr ++ bindNames bnd +exprNames (Let binds expr) = exprNames expr ++ bindsNames binds exprNames (FunApp fun args) = varNames fun ++ concatMap atomNames args exprNames (PrimApp prim args) = pfunNames prim ++ concatMap atomNames args exprNames (ConApp dcon args) = dataNames dcon ++ concatMap atomNames args exprNames (Case expr var alts) = exprNames expr ++ concatMap altNames alts ++ varNames var --- | `Name`s in a `Type`. -typeNames :: Type -> [Name] -typeNames (TyVarTy n ty) = n : typeNames ty -typeNames (CoercionTy coer) = coercionNames coer -typeNames (AppTy t1 t2) = typeNames t1 ++ typeNames t2 -typeNames (CastTy ty coer) = typeNames ty ++ coercionNames coer -typeNames (ForAllTy bnd ty) = typeNames ty ++ tyBinderNames bnd -typeNames (FunTy t1 t2) = typeNames t1 ++ typeNames t2 -typeNames (TyConApp tc ty) = tyConNames tc ++ concatMap typeNames ty -typeNames (LitTy _) = [] -typeNames (Bottom) = [] +-- | `Name`s in an `Atom`. +atomNames :: Atom -> [Name] +atomNames (LitAtom _) = [] +atomNames (VarAtom var) = varNames var + -- | `Name`s in a `PrimFun`. pfunNames :: PrimFun -> [Name] -pfunNames (PrimFun n ty) = n : typeNames ty +pfunNames (PrimFun name ty) = name : typeNames ty -- | `Name`s in a `DataCon`. dataNames :: DataCon -> [Name] -dataNames (DataCon n ty tys) = n : concatMap typeNames (ty : tys) +dataNames (DataCon name ty tys) = name : concatMap typeNames (ty : tys) +-- | `Name`s in an `Alt`. +altNames :: Alt -> [Name] +altNames (Alt _ vars expr) = concatMap varNames vars ++ exprNames expr + +-- | `Name`s in a `Type`. +typeNames :: Type -> [Name] +typeNames (TyVarTy var) = varNames var +typeNames (AppTy ty1 ty2) = typeNames ty1 ++ typeNames ty2 +typeNames (ForAllTy bndr ty) = typeNames ty ++ tyBinderNames bndr +typeNames (FunTy ty1 ty2) = typeNames ty1 ++ typeNames ty2 +typeNames (TyConApp tycon ty) = tyConNames tycon ++ concatMap typeNames ty +typeNames (CoercionTy coer) = coercionNames coer +typeNames (CastTy ty coer) = typeNames ty ++ coercionNames coer +typeNames (LitTy _) = [] +typeNames (Bottom) = [] + -- | `Name`s in a `TyBinder`. tyBinderNames :: TyBinder -> [Name] tyBinderNames (AnonTyBndr) = [] -tyBinderNames (NamedTyBndr n) = [n] +tyBinderNames (NamedTyBndr name) = [name] -- | `Name`s in a `TyCon`. tyConNames :: TyCon -> [Name] -tyConNames (FamilyTyCon n ns) = n : ns -tyConNames (SynonymTyCon n ns) = n : ns -tyConNames (AlgTyCon n ns r) = n : ns ++ algTyRhsNames r -tyConNames (FunTyCon n bs) = n : concatMap tyBinderNames bs -tyConNames (PrimTyCon n bs) = n : concatMap tyBinderNames bs -tyConNames (Promoted n bs dc) = n : concatMap tyBinderNames bs ++ dataNames dc +tyConNames (FamilyTyCon name params) = name : params +tyConNames (SynonymTyCon name params) = name : params +tyConNames (AlgTyCon name params rhs) = name : params ++ algTyRhsNames rhs +tyConNames (FunTyCon name bndrs) = name : concatMap tyBinderNames bndrs +tyConNames (PrimTyCon name bndrs) = name : concatMap tyBinderNames bndrs +tyConNames (Promoted name bndrs dcon) = name : concatMap tyBinderNames bndrs + ++ dataNames dcon -- | `Name`s in a `Coercion`. coercionNames :: Coercion -> [Name] -coercionNames (Coercion t1 t2) = typeNames t1 ++ typeNames t2 +coercionNames (Coercion ty1 ty2) = typeNames ty1 ++ typeNames ty2 -- | `Name`s in a `AlgTyRhs`. algTyRhsNames :: AlgTyRhs -> [Name] algTyRhsNames (AbstractTyCon _) = [] -algTyRhsNames (DataTyCon ns) = ns -algTyRhsNames (TupleTyCon n) = [n] -algTyRhsNames (NewTyCon n) = [n] - --- | `Name`s in a `Bind`. -bindNames :: Bind -> [Name] -bindNames (Bind _ bnd) = lhs ++ rhs - where - lhs = concatMap (varNames . fst) bnd - rhs = concatMap (bindRhsNames . snd) bnd +algTyRhsNames (DataTyCon names) = names +algTyRhsNames (TupleTyCon name) = [name] +algTyRhsNames (NewTyCon name) = [name] --- | `Name`s in a `PathCons`. -pconsNames :: PathCons -> [Name] -pconsNames pathcons = concatMap constraintNames (pathconsToList pathcons) +-- | A `Name`'s occurrence string. +nameOccStr :: Name -> String +nameOccStr (Name occ _ _ _) = occ --- | `Name`s in a `PathCons`. -constraintNames :: Constraint -> [Name] -constraintNames (Constraint (_, vs) e locs _) = exprNames e ++ localsNames locs - ++ map varName vs +-- | A `Name`'s unique int. +nameInt :: Name -> Int +nameInt (Name _ _ _ int) = int -- | Create a fresh seed given any `Int`, a `String` seed, and a `Set` of -- `String`s that we do not want our new `String` to conflict with. The sole @@ -196,7 +150,7 @@ occ' = freshString 1 occ (S.fromList alls) unq' = maxs + 1 alls = map nameOccStr confs - maxs = L.maximum (unq : map nameUnique confs) + maxs = L.maximum (unq : map nameInt confs) -- | Generate a list of `Name`s, each corresponding to the appropriate element -- of the `NameSpace` list. diff --git a/src/SSTG/Core/Language/Support.hs b/src/SSTG/Core/Language/Support.hs deleted file mode 100644 --- a/src/SSTG/Core/Language/Support.hs +++ /dev/null @@ -1,351 +0,0 @@ --- | Symbolic STG Execution Support Architecture -module SSTG.Core.Language.Support - ( SymbolicT(..) - , fmap - , pure - , (<*>) - , return - , (>>=) - - , State(..) - , Symbol(..) - , Status(..) - , Stack - , Frame(..) - , MemAddr - , Value(..) - , Locals - , Heap - , HeapObj(..) - , Globals - , Code(..) - , PathCons - , Constraint(..) - - , nameOccStr - , nameUnique - , varName - , null_addr - , addrInt - - , init_status - , incStatusSteps - , updateStatusId - - , empty_stack - , popStack - , pushStack - , stackToList - - , empty_locals - , lookupLocals - , insertLocals - , insertLocalsList - , localsToList - - , empty_heap - , lookupHeap - , allocHeap - , allocHeapList - , insertHeap - , insertHeapList - , heapToList - - , empty_globals - , lookupGlobals - , insertGlobals - , insertGlobalsList - , globalsToList - - , empty_pathcons - , insertPathCons - , insertPathConsList - , pathconsToList - - , lookupValue - , vlookupHeap - , memAddrType - ) where - -import SSTG.Core.Language.Syntax -import SSTG.Core.Language.Typing - -import qualified Data.Map as M - --- | Symbolic Transformation represents transformations applied to some --- State`(s). This is useful in allowing us to transfer from different actions --- within the engine. -newtype SymbolicT s a = SymbolicT { run :: s -> (s, a) } - --- | Functor instance of Symbolic Transformation. -instance Functor (SymbolicT s) where - fmap f st = SymbolicT (\s0 -> let (s1, a1) = (run st) s0 in (s1, f a1)) - --- | Applicative instance of Symbolic Transformation. -instance Applicative (SymbolicT s) where - pure a = SymbolicT (\s -> (s, a)) - - sf <*> st = SymbolicT (\s0 -> let (s1, a1) = (run st) s0 - (s2, f2) = (run sf) s1 in (s2, f2 a1)) - --- | Monad instance of Symbolic Transformation. -instance Monad (SymbolicT s) where - return a = pure a - - st >>= fs = SymbolicT (\s0 -> let (s1, a1) = (run st) s0 - (s2, a2) = (run (fs a1)) s1 in (s2, a2)) - --- | `State` contains the information necessary to perform symbolic execution. --- Eval/Apply graph reduction semantics are used. -data State = State { state_status :: !Status - , state_stack :: !Stack - , state_heap :: !Heap - , state_globals :: !Globals - , state_code :: !Code - , state_names :: ![Name] - , state_paths :: !PathCons - } deriving (Show, Eq, Read) - --- | Symbolic variables. The @Maybe (Expr, Locals)@ can be used to trace the --- source from which the symbolic variable was generated. For instance, this is --- useful during symbolic function application. -data Symbol = Symbol Var (Maybe (Expr, Locals)) deriving (Show, Eq, Read) - --- | State status. -data Status = Status { status_id :: !Int - , status_parent :: !Int - , status_steps :: !Int - } deriving (Show, Eq, Read) - --- | Execution stack used in graph reduction semnatics. -newtype Stack = Stack [Frame] deriving (Show, Eq, Read) - --- | Frames of a stack. -data Frame = CaseFrame Var [Alt] Locals - | ApplyFrame [Atom] Locals - | UpdateFrame MemAddr - deriving (Show, Eq, Read) - --- | Memory address for things on the `Heap`. -newtype MemAddr = MemAddr Int deriving (Show, Eq, Read, Ord) - --- | A `Value` is something that we aim to reduce our current expression down --- into. `MemAddr` is a pointer to an object on the heap, such as `FunObj` or --- `ConObj`, which are "returned" from expression evaluation in this form. -data Value = LitVal Lit - | MemVal MemAddr - deriving (Show, Eq, Read) - --- | Locals binds a `Var`'s `Name` to its some `Value`. -newtype Locals = Locals (M.Map Name Value) deriving (Show, Eq, Read) - --- | Heaps map `MemAddr` to `HeapObj`, while keeping track of the last address --- that was allocated. This allows us to consistently allocate fresh addresses --- on the `Heap`. -data Heap = Heap (M.Map MemAddr HeapObj) MemAddr deriving (Show, Eq, Read) - --- | Heap objects. -data HeapObj = LitObj Lit - | SymObj Symbol - | ConObj DataCon [Value] - | FunObj [Var] Expr Locals - | AddrObj MemAddr - | Blackhole - deriving (Show, Eq, Read) - --- | Globals are statically loaded at the time when a `State` is loaded. --- However, because uninterpreted / out-of-scope variables are made symbolic --- at runtime, it can be modified during execution. -newtype Globals = Globals (M.Map Name Value) deriving (Show, Eq, Read) - --- | Evaluation of the current expression. We are either evaluating, or ready --- to return with some `Value`. -data Code = Evaluate Expr Locals - | Return Value - deriving (Show, Eq, Read) - --- | Path constraints are the conjunctive normal form of `Constraint`s. -newtype PathCons = PathCons [Constraint] deriving (Show, Eq, Read) - --- | Constraints denote logical paths taken in program execution thus far. -data Constraint = Constraint (AltCon, [Var]) Expr Locals Bool - deriving (Show, Eq, Read) - --- Simple functions that require only the immediate data structure. - --- | A `Name`'s occurrence string. -nameOccStr :: Name -> String -nameOccStr (Name occ _ _ _) = occ - --- | `Name` imique `Int`. -nameUnique :: Name -> Int -nameUnique (Name _ _ _ unq) = unq - --- | Variable name. -varName :: Var -> Name -varName (Var name _) = name - --- | Null `MemAddr`. -null_addr :: MemAddr -null_addr = MemAddr 0 - --- | `MemAddr`'s `Int` value. -addrInt :: MemAddr -> Int -addrInt (MemAddr int) = int - --- | Initial `Status`. -init_status :: Status -init_status = Status { status_id = 1 - , status_parent = 0 - , status_steps = 0 } - --- | Increment `Status` steps. -incStatusSteps :: Status -> Status -incStatusSteps status = status { status_steps = (status_steps status) + 1 } - --- | Update the `Status` id. -updateStatusId :: Int -> Status -> Status -updateStatusId new_id status = status { status_id = new_id - , status_parent = status_id status } - --- | Empty `Stack. -empty_stack :: Stack -empty_stack = Stack [] - --- | `Stack` pop. -popStack :: Stack -> Maybe (Frame, Stack) -popStack (Stack []) = Nothing -popStack (Stack (frame:frames)) = Just (frame, Stack frames) - --- | `Stack` push. -pushStack :: Frame -> Stack -> Stack -pushStack frame (Stack frames) = Stack (frame : frames) - --- | `Stack` as list of `Frame`s. -stackToList :: Stack -> [Frame] -stackToList (Stack frames) = frames - --- | Empty `Locals`. -empty_locals :: Locals -empty_locals = Locals M.empty - --- | `Locals` lookup. -lookupLocals :: Var -> Locals -> Maybe Value -lookupLocals var (Locals lmap) = M.lookup (varName var) lmap - --- | `Locals` insertion. -insertLocals :: (Var, Value) -> Locals -> Locals -insertLocals (k, v) (Locals lmap) = Locals (M.insert (varName k) v lmap) - --- | List insertion into `Locals`. -insertLocalsList :: [(Var, Value)] -> Locals -> Locals -insertLocalsList kvs locals = foldr insertLocals locals kvs - --- | `Locals` to key value pairs. -localsToList :: Locals -> [(Name, Value)] -localsToList (Locals lmap) = M.toList lmap - --- | Empty `Heap`. -empty_heap :: Heap -empty_heap = Heap M.empty null_addr - --- | `Heap` lookup. -lookupHeap :: MemAddr -> Heap -> Maybe HeapObj -lookupHeap addr (Heap hmap prev) = case M.lookup addr hmap of - Just (AddrObj redir) -> lookupHeap redir (Heap hmap prev) - mb_hobj -> mb_hobj - --- | `Heap` allocation. Updates the last `MemAddr` kept in the `Heap`. -allocHeap :: HeapObj -> Heap -> (Heap, MemAddr) -allocHeap hobj (Heap hmap prev) = (Heap hmap' addr, addr) - where - addr = MemAddr ((addrInt prev) + 1) - hmap' = M.insert addr hobj hmap - --- | Allocate a list of `HeapObj` in a `Heap`, returning in the same order the --- `MemAddr` at which they have been allocated at. -allocHeapList :: [HeapObj] -> Heap -> (Heap, [MemAddr]) -allocHeapList [] heap = (heap, []) -allocHeapList (hobj:hobjs) heap = (heapf, addr : as) - where - (heap', addr) = allocHeap hobj heap - (heapf, as) = allocHeapList hobjs heap' - --- | `Heap` direct insertion at a specific `MemAddr`. -insertHeap :: (MemAddr, HeapObj) -> Heap -> Heap -insertHeap (k, v) (Heap hmap prev) = Heap (M.insert k v hmap) prev - --- | Insert a list of `HeapObj` at specified `MemAddr` locations. -insertHeapList :: [(MemAddr, HeapObj)] -> Heap -> Heap -insertHeapList kvs heap = foldr insertHeap heap kvs - --- | `Heap` to key value pairs. -heapToList :: Heap -> [(MemAddr, HeapObj)] -heapToList (Heap hmap _) = M.toList hmap - --- | Empty `Globals`. -empty_globals :: Globals -empty_globals = Globals M.empty - --- | `Globals` lookup. -lookupGlobals :: Var -> Globals -> Maybe Value -lookupGlobals var (Globals gmap) = M.lookup (varName var) gmap - --- | `Globals` insertion. -insertGlobals :: (Var, Value) -> Globals -> Globals -insertGlobals (k, v) (Globals gmap) = Globals (M.insert (varName k) v gmap) - --- | Insert a list of `Var` and `Value` pairs into `Globals`. This would --- typically occur for new symbolic variables created from uninterpreted / --- out-of-scope variables during runtime. -insertGlobalsList :: [(Var, Value)] -> Globals -> Globals -insertGlobalsList kvs globals = foldr insertGlobals globals kvs - --- | `Globals` to key value pairs. -globalsToList :: Globals -> [(Name, Value)] -globalsToList (Globals gmap) = M.toList gmap - --- | Empty `PathCons`. -empty_pathcons :: PathCons -empty_pathcons = PathCons [] - --- | `PathCons` insertion. -insertPathCons :: Constraint -> PathCons -> PathCons -insertPathCons cons (PathCons conss) = PathCons (cons : conss) - --- | Insert a list of `Constraint`s into a `PathCons`. -insertPathConsList :: [Constraint] -> PathCons -> PathCons -insertPathConsList conss pathcons = foldr insertPathCons pathcons conss - --- | `PathCons` to list of `Constraint`s. -pathconsToList :: PathCons -> [Constraint] -pathconsToList (PathCons conss) = conss - --- Complex functions that involve multiple data structures. - --- | `Value` lookup from the `Locals` first, then `Globals`. -lookupValue :: Var -> Locals -> Globals -> Maybe Value -lookupValue var locals globals = case lookupLocals var locals of - Nothing -> lookupGlobals var globals - Just val -> Just val - --- | `Heap` lookup. Returns the corresponding `MemAddr` and `HeapObj` if found. -vlookupHeap :: Var -> Locals -> Globals -> Heap -> Maybe (MemAddr, HeapObj) -vlookupHeap var locals globals heap = do - val <- lookupValue var locals globals - case val of - LitVal _ -> Nothing - MemVal addr -> lookupHeap addr heap >>= \hobj -> Just (addr, hobj) - --- | Type of `HeapObj` held at `MemAddr`, if found. -memAddrType :: MemAddr -> Heap -> Maybe Type -memAddrType addr heap = do - hobj <- lookupHeap addr heap - case hobj of - AddrObj redir -> memAddrType redir heap - LitObj lit -> Just (litType lit) - SymObj (Symbol s _) -> Just (varType s) - ConObj dcon _ -> Just (dataconType dcon) - FunObj ps e _ -> Just (foldr FunTy (exprType e) (map varType ps)) - Blackhole -> Just Bottom - 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 @@ -6,7 +6,7 @@ -- | A `Program` is defined as a list of bindings. The @Name@ is an identifier -- that determines a unique binder to the @var@. In practice, these are defined -- to be `Name` and `Var` respectively. -newtype Program = Program [Bind] deriving (Show, Eq, Read) +newtype Program = Program [Binds] deriving (Show, Eq, Read) -- | Variables, data constructors, type variables, and type constructors. data NameSpace = VarNSpace | DataNSpace | TvNSpace | TcClsNSpace @@ -24,9 +24,9 @@ -- | Literals are largely augmented from the original GHC implementation, with -- additional annotations to denote `BlankAddr` for lifting, `AddrLit` for --- value deriviation, `SymLit` for symbolic literals, and `SymLitEval` to --- represent symbolic literal evaluation, as literal manipulation functions --- are defined in the Haskell Prelude, and thus outside of scope for us. +-- value deriviation, and `LitEval` to represent symbolic literal evaluation, +-- as literal manipulation functions are defined in the Haskell Prelude, and +-- thus outside of scope for us. data Lit = MachChar Char Type | MachStr String Type | MachInt Int Type @@ -37,13 +37,12 @@ | MachNullAddr Type | BlankAddr | AddrLit Int - | SymLit Var - | SymLitEval PrimFun [Lit] + | LitEval PrimFun [Lit] deriving (Show, Eq, Read) -- | Atomic objects. `VarAtom` may be used for variable lookups, while -- `LitAtom` is used to denote literals. -data Atom = LitAtom (Lit) +data Atom = LitAtom Lit | VarAtom Var deriving (Show, Eq, Read) @@ -55,7 +54,7 @@ | PrimApp PrimFun [Atom] | ConApp DataCon [Atom] | FunApp Var [Atom] - | Let Bind Expr + | Let Binds Expr | Case Expr Var [Alt] deriving (Show, Eq, Read) @@ -69,8 +68,8 @@ | Default deriving (Show, Eq, Read) --- | Bind -data Bind = Bind RecForm [(Var, BindRhs)] deriving (Show, Eq, Read) +-- | Bindings +data Binds = Binds RecForm [(Var, BindRhs)] deriving (Show, Eq, Read) -- | Recursive? data RecForm = Rec | NonRec deriving (Show, Eq, Read) @@ -88,7 +87,7 @@ -- | Types are information that are useful to keep during symbolic execution -- in order to generate correct feeds into the SMT solver. Overapproxmation is -- currently performed, and is likely to be cut back in the future. -data Type = TyVarTy Name Type +data Type = TyVarTy Var | AppTy Type Type | ForAllTy TyBinder Type | CastTy Type Coercion 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 @@ -21,8 +21,7 @@ litType (MachNullAddr ty) = ty litType (BlankAddr) = Bottom litType (AddrLit _) = Bottom -litType (SymLit var) = varType var -litType (SymLitEval pf args) = foldl AppTy (primfunType pf) (map litType args) +litType (LitEval pf args) = foldl AppTy (primFunType pf) (map litType args) -- | Atom type. atomType :: Atom -> Type @@ -30,12 +29,12 @@ atomType (VarAtom var) = varType var -- | Primitive function type. -primfunType :: PrimFun -> Type -primfunType (PrimFun _ ty) = ty +primFunType :: PrimFun -> Type +primFunType (PrimFun _ ty) = ty -- | Data constructor type denoted as a function. -dataconType :: DataCon -> Type -dataconType (DataCon _ ty tys) = foldr FunTy ty tys +dataConType :: DataCon -> Type +dataConType (DataCon _ ty tys) = foldr FunTy ty tys -- | Alt type altType :: Alt -> Type @@ -44,8 +43,8 @@ -- | I wonder what this could possibly be? exprType :: Expr -> Type exprType (Atom atom) = atomType atom -exprType (PrimApp pf args) = foldl AppTy (primfunType pf) (map atomType args) -exprType (ConApp dc args) = foldl AppTy (dataconType dc) (map atomType args) +exprType (PrimApp pf args) = foldl AppTy (primFunType pf) (map atomType args) +exprType (ConApp dc args) = foldl AppTy (dataConType dc) (map atomType args) exprType (FunApp fun args) = foldl AppTy (varType fun) (map atomType args) exprType (Let _ expr) = exprType expr exprType (Case _ _ (a:_)) = altType a 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 @@ -2,7 +2,7 @@ module SSTG.Core.Translation.Haskell ( CompileClosure , mkCompileClosure - , mkTargetBinds + , mkTargetBindsList , mkIOString ) where @@ -37,9 +37,9 @@ return (showPpr dflags obj) -- | Given the project directory and the source file path, compiles the --- `ModuleGraph` and translates it into a SSTG `Bind`s. -mkTargetBinds :: FilePath -> FilePath -> IO [SL.Bind] -mkTargetBinds proj src = do +-- `ModuleGraph` and translates it into a SSTG `Binds`s. +mkTargetBindsList :: FilePath -> FilePath -> IO [SL.Binds] +mkTargetBindsList proj src = do (sums_gutss, dflags, env) <- mkCompileClosure proj src let (sums, gutss) = (map fst sums_gutss, map snd sums_gutss) let mod_lcs = map (\s -> (ms_mod s, ms_location s)) sums @@ -51,7 +51,7 @@ let zipd2 = zip (map fst mod_lcs) preps stg_bindss <- mapM (\(m, p) -> coreToStg dflags m p) zipd2 -- Create the binds. - return (map mkBind (concat stg_bindss)) + return (map mkBinds (concat stg_bindss)) -- | Compilation closure type. type CompileClosure = ([(ModSummary, ModGuts)], DynFlags, HscEnv) @@ -83,12 +83,12 @@ mkExpr (StgApp occ args) = SL.FunApp (mkVar occ) (map mkAtom args) mkExpr (StgConApp dcon args) = SL.ConApp (mkData dcon) (map mkAtom args) mkExpr (StgOpApp op args _) = SL.PrimApp (mkPrimOp op) (map mkAtom args) -mkExpr (StgTick _ expr)= mkExpr expr +mkExpr (StgTick _ expr) = mkExpr expr mkExpr (StgLam _ _) = error "mkExpr: StgLam detected" -mkExpr (StgLet bind expr) = SL.Let (mkBind bind) (mkExpr expr) -mkExpr (StgLetNoEscape _ _ bind expr) = mkExpr (StgLet bind expr) -mkExpr (StgCase mxpr _ _ cvar _ _ alts) = SL.Case (mkExpr mxpr) (mkVar cvar) - (map mkAlt alts) +mkExpr (StgLet binds expr) = SL.Let (mkBinds binds) (mkExpr expr) +mkExpr (StgLetNoEscape _ _ binds expr) = mkExpr (StgLet binds expr) +mkExpr (StgCase mexpr _ _ cvar _ _ alts) = SL.Case (mkExpr mexpr) (mkVar cvar) + (map mkAlt alts) -- | Make SSTG `Atom`. mkAtom :: StgArg -> SL.Atom @@ -103,8 +103,8 @@ ns = (mkNameSpace . occNameSpace . nameOccName) name unq = (getKey . nameUnique) name mdl = case nameModule_maybe name of - Nothing -> Nothing Just md -> Just ((moduleNameString . moduleName) md) + Nothing -> Nothing -- | Make SSTG `NameSpace`. mkNameSpace :: NameSpace -> SL.NameSpace @@ -122,9 +122,10 @@ vtype = (mkType . varType) var -- | Make SSTG `Bind`. -mkBind :: StgBinding -> SL.Bind -mkBind (StgNonRec bind r) = SL.Bind SL.NonRec [(mkVar bind, mkRhs r)] -mkBind (StgRec bind) = SL.Bind SL.Rec (map (\(b,r) -> (mkVar b, mkRhs r)) bind) +mkBinds :: StgBinding -> SL.Binds +mkBinds (StgNonRec var rhs) = SL.Binds SL.NonRec [(mkVar var, mkRhs rhs)] +mkBinds (StgRec binds) = SL.Binds SL.Rec + (map (\(v, r) -> (mkVar v, mkRhs r)) binds) -- | Make SSTG `BindRhs`. mkRhs :: StgRhs -> SL.BindRhs @@ -181,10 +182,10 @@ -- | Make SSTG `Type`. mkType :: Type -> SL.Type -mkType (TyVarTy v) = SL.TyVarTy (mkName (V.varName v)) (mkType (varType v)) +mkType (TyVarTy var) = SL.TyVarTy (mkVar var) mkType (AppTy t1 t2) = SL.AppTy (mkType t1) (mkType t2) mkType (TyConApp tc ts) = SL.TyConApp (mkTyCon tc) (map mkType ts) -mkType (ForAllTy b ty) = SL.ForAllTy (mkTyBinder b) (mkType ty) +mkType (ForAllTy tb ty) = SL.ForAllTy (mkTyBinder tb) (mkType ty) mkType (LitTy tlit) = SL.LitTy (mkTyLit tlit) mkType (CastTy ty cor) = SL.CastTy (mkType ty) (mkCoercion cor) mkType (CoercionTy cor) = SL.CoercionTy (mkCoercion cor) @@ -215,7 +216,7 @@ -- | make SSTG `TyBinder`. mkTyBinder :: TyBinder -> SL.TyBinder mkTyBinder (Anon _) = SL.AnonTyBndr -mkTyBinder (Named v _) = SL.NamedTyBndr (mkName (V.varName v)) +mkTyBinder (Named var _) = SL.NamedTyBndr (mkName (V.varName var)) -- | Make SSTG `Type` literals. mkTyLit :: TyLit -> SL.TyLit 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 @@ -2,7 +2,7 @@ module SSTG.Utils.Printing ( pprStateStr , pprLivesDeadsStr - , pprBindStr + , pprBindsStr ) where import SSTG.Core @@ -104,7 +104,7 @@ -- | Print `MemAddr`. pprMemAddrStr :: MemAddr -> String -pprMemAddrStr addr = show (addrInt addr) +pprMemAddrStr addr = show (memAddrInt addr) -- | Print `Name`. pprNameStr :: Name -> String @@ -156,44 +156,56 @@ locs_str = pprLocalsStr locals acc_strs = [header, injIntoList [expr_str, locs_str]] --- | Print `HeapObj`. -pprHeapObjStr :: HeapObj -> String -pprHeapObjStr (Blackhole) = "Blackhole!!!" -pprHeapObjStr (AddrObj addr) = pprMemAddrStr addr -pprHeapObjStr (LitObj lit) = injSpace acc_strs +-- | Print `Heap`'s redirection. +pprMemRedirStr :: (MemAddr, MemAddr) -> String +pprMemRedirStr (addr, redir) = sub (addr_str ++ ", " ++ redir_str) where + addr_str = pprMemAddrStr addr + redir_str = pprMemAddrStr redir + +-- | Print `Heap`'s`HeapObj`. +pprMemHeapObjStr :: (MemAddr, HeapObj) -> String +pprMemHeapObjStr (addr, Blackhole) = sub (pprMemAddrStr addr ++ ", Blackhole") +pprMemHeapObjStr (addr, LitObj lit) = acc_str + where header = "LitObj" + addr_str = pprMemAddrStr addr lit_str = pprLitStr lit - acc_strs = [header, lit_str] -pprHeapObjStr (SymObj (Symbol sym mb_scls)) = injSpace acc_strs + acc_str = sub (addr_str ++ ", " ++ injSpace [header, lit_str]) +pprMemHeapObjStr (addr, SymObj (Symbol sym mb_scls)) = acc_str where header = "SymObj" + addr_str = pprMemAddrStr addr var_str = pprVarStr sym scls_str = (sub . pprSymClosureStr) mb_scls - acc_strs = [header, var_str, scls_str] -pprHeapObjStr (ConObj dcon vals) = injSpace acc_strs + acc_str = sub (addr_str ++ ", " ++ injSpace [header, var_str, scls_str]) +pprMemHeapObjStr (addr, ConObj dcon vals) = acc_str where header = "ConObj" + addr_str = pprMemAddrStr addr dcon_str = pprDataConStr dcon vals_str = injIntoList (map pprValueStr vals) - acc_strs = [header, dcon_str, vals_str] -pprHeapObjStr (FunObj params expr locals) = injSpace acc_strs + acc_str = sub (addr_str ++ ", " ++ injSpace [header, dcon_str, vals_str]) +pprMemHeapObjStr (addr, FunObj params expr locals) = acc_str where header = "FunObj" + addr_str = pprMemAddrStr addr prms_str = injIntoList (map pprVarStr params) expr_str = pprExprStr expr locs_str = pprLocalsStr locals - acc_strs = [header, prms_str, expr_str, locs_str] + funobj_str = injSpace [header, prms_str, expr_str, locs_str] + acc_str = sub (addr_str ++ ", " ++ funobj_str) -- | Print `Heap`. pprHeapStr :: Heap -> String pprHeapStr heap = injNewLine acc_strs where hlist = heapToList heap - addr_strs = map (pprMemAddrStr . fst) hlist - hobj_strs = map (pprHeapObjStr . snd) hlist - zipd_strs = zip addr_strs hobj_strs - acc_strs = map (\(m, o) -> sub (m ++ ", " ++ o)) zipd_strs + addr_redirs = [(addr, r) | (addr, Left r) <- hlist] + addr_hobjs = [(addr, o) | (addr, Right o) <- hlist] + addr_redir_strs = map pprMemRedirStr addr_redirs + addr_hobj_strs = map pprMemHeapObjStr addr_hobjs + acc_strs = addr_redir_strs ++ addr_hobj_strs -- | Print `Globals`. pprGlobalsStr :: Globals -> String @@ -314,19 +326,19 @@ -- | Print @(Var, BindRhs)@. pprBindKVStr :: (Var, BindRhs) -> String -pprBindKVStr (var, lamf) = (sub . injComma) acc_strs +pprBindKVStr (var, rhs) = (sub . injComma) acc_strs where var_str = pprVarStr var - lamf_str = pprBindRhsStr lamf - acc_strs = [var_str, lamf_str] + rhs_str = pprBindRhsStr rhs + acc_strs = [var_str, rhs_str] --- | Print `Bind`. -pprBindStr :: Bind -> String -pprBindStr (Bind rec bnd) = injSpace acc_strs +-- | Print `Binds`. +pprBindsStr :: Binds -> String +pprBindsStr (Binds rec kvs) = injSpace acc_strs where header = case rec of { Rec -> "Rec"; NonRec -> "NonRec" } - bnds_str = injIntoList (map pprBindKVStr bnd) - acc_strs = [header, bnds_str] + kvs_str = injIntoList (map pprBindKVStr kvs) + acc_strs = [header, kvs_str] -- | Print `Expr`. pprExprStr :: Expr -> String @@ -360,17 +372,17 @@ var_str = (sub . pprVarStr) var alts_str = pprAltsStr alts acc_strs = [header, expr_str, var_str, alts_str] -pprExprStr (Let bnd expr) = injSpace acc_strs +pprExprStr (Let binds expr) = injSpace acc_strs where header = "Let" - bnd_str = (sub . pprBindStr) bnd + binds_str = (sub . pprBindsStr) binds expr_str = (sub . pprExprStr) expr - acc_strs = [header, bnd_str, expr_str] + acc_strs = [header, binds_str, expr_str] -- | Print `Type`. NOTE: currently only prints @"__TyPE__"@ because there is -- a lot of `Type` information which makes analysis of dumps hard otherwise. pprTypeStr :: Type -> String -pprTypeStr ty = snd ("__Type__", show ty) +pprTypeStr ty = fst ("__Type__", show ty) -- | Print `Code`. pprCodeStr :: Code -> String @@ -404,6 +416,6 @@ prms_str = injIntoList (map pprVarStr ps) expr_str = pprExprStr expr locs_str = pprLocalsStr locals - hold_str = case hold of { True -> "Positive"; False -> "Negative" } + hold_str = if hold then "Positive" else "Negative" acc_strs = [acon_str, prms_str, expr_str, locs_str, hold_str]