diff --git a/SSTG.cabal b/SSTG.cabal --- a/SSTG.cabal +++ b/SSTG.cabal @@ -1,5 +1,5 @@ name: SSTG -version: 0.1.0.7 +version: 0.1.0.8 synopsis: STG Symbolic Execution description: Prototype of STG-based Symbolic Execution for Haskell. homepage: https://github.com/AntonXue/SSTG#readme 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 @@ -14,8 +14,6 @@ import SSTG.Core.Execution.Stepping import SSTG.Core.Execution.Support -import qualified Data.Map as M - -- | Load Result data LoadResult = LoadOkay State | LoadGuess State [Binding] @@ -38,11 +36,11 @@ where -- Status or something. status = Status { steps = 0 } -- Stack initialized to empty. - stack = Stack [] + stack = emptyStack -- Globals and Heap are loaded together. They are still beta forms now. - heap0 = Heap M.empty (MemAddr 0) + heap0 = emptyHeap (glist, heap1, bnd_addrss) = initGlobals bnds heap0 - globals0 = Globals (M.fromList glist) + globals0 = insertGlobalsList glist emptyGlobals (heap2, localss) = liftBindings bnd_addrss globals0 heap1 bnd_locs = zip bnds localss -- Code loading. Completes heap and globals with symbolic injection. @@ -57,8 +55,8 @@ , state_globals = globals , state_code = code , state_names = [] - , state_paths = [] - , state_links = SymLinks M.empty } + , state_paths = emptyPathCons + , state_links = emptySymLinks } -- Gather information on all variables. state = state0 { state_names = allNames state0 } @@ -72,23 +70,22 @@ -- | Allocate List of Bindings allocBindingList :: [Binding] -> Heap -> (Heap, [[MemAddr]]) allocBindingList [] heap = (heap, []) -allocBindingList (b:bs) heap = (res_heap, addrs : as) +allocBindingList (b:bs) heap = (heapf, addrs : as) where (heap', addrs) = allocBinding b heap - (res_heap, as) = allocBindingList bs heap' + (heapf, as) = allocBindingList bs heap' -- | Binding Address to Name Values -bndAddrsToNameVals :: (Binding, [MemAddr]) -> [(Name, Value)] -bndAddrsToNameVals (Binding _ rhss, addrs) = zip names pointers - where names = map (varName . fst) rhss - pointers = map (\a -> MemVal a) addrs +bndAddrsToVarVals :: (Binding, [MemAddr]) -> [(Var, Value)] +bndAddrsToVarVals (Binding _ rhss, addrs) = zip (map fst rhss) mem_vals + where mem_vals = map (\a -> MemVal a) addrs -- | Initialize Globals initGlobals :: [Binding] -> Heap -> - ([(Name, Value)], Heap, [(Binding, [MemAddr])]) -initGlobals bnds heap = (name_vals, heap', bnd_addrss) + ([(Var, Value)], Heap, [(Binding, [MemAddr])]) +initGlobals bnds heap = (var_vals, heap', bnd_addrss) where (heap', addrss) = allocBindingList bnds heap bnd_addrss = zip bnds addrss - name_vals = concatMap bndAddrsToNameVals bnd_addrss + var_vals = concatMap bndAddrsToVarVals bnd_addrss -- | Force Atom Lookup forceLookupValue :: Atom -> Locals -> Globals -> Value @@ -109,7 +106,7 @@ liftBinding (Binding rec pairs, addrs) globals heap = (heap', locals) where (vars, rhss) = unzip pairs mem_vals = map (\a -> MemVal a) addrs - e_locs = Locals M.empty + e_locs = emptyLocals r_locs = insertLocalsList (zip vars mem_vals) e_locs locals = case rec of { Rec -> r_locs; NonRec -> e_locs } hobjs = map (\r -> forceRhsObj r locals globals) rhss @@ -118,9 +115,9 @@ -- | Lift Binding List liftBindings :: [(Binding, [MemAddr])] -> Globals -> Heap -> (Heap, [Locals]) liftBindings [] _ heap = (heap, []) -liftBindings (bm:bms) globals heap = (res_heap, locals : ls) +liftBindings (bm:bms) globals heap = (heapf, locals : ls) where (heap', locals) = liftBinding bm globals heap - (res_heap, ls) = liftBindings bms globals heap' + (heapf, ls) = liftBindings bms globals heap' -- | Return a sub-list of bindings in which the entry candidate appears. entryMatches :: String -> [(Binding, Locals)] -> [(Binding, Locals)] @@ -188,5 +185,4 @@ execute1 :: Int -> State -> ([LiveState], [DeadState]) execute1 n state | n < 1 = ([([], state)], []) | otherwise = runBoundedBFS n state - diff --git a/src/SSTG/Core/Execution/Naming.hs b/src/SSTG/Core/Execution/Naming.hs --- a/src/SSTG/Core/Execution/Naming.hs +++ b/src/SSTG/Core/Execution/Naming.hs @@ -12,7 +12,6 @@ import SSTG.Core.Execution.Support import qualified Data.List as L -import qualified Data.Map as M import qualified Data.Set as S -- | All `Name`s in a `State`. @@ -29,8 +28,7 @@ -- | `Name`s in a `Stack`. stackNames :: Stack -> [Name] -stackNames (Stack []) = [] -stackNames (Stack (f:fs)) = frameNames f ++ stackNames (Stack fs) +stackNames stack = concatMap frameNames (stackToList stack) -- | `Name`s in a `Frame`. frameNames :: Frame -> [Name] @@ -45,15 +43,15 @@ -- | `Name`s in the `Locals` localsNames :: Locals -> [Name] -localsNames (Locals lmap) = M.keys lmap +localsNames locals = map fst (localsToList locals) -- | `Name`s in the `Heap`. heapNames :: Heap -> [Name] -heapNames (Heap heap _) = concatMap (heapObjNames . snd) hlist - where hlist = M.toList heap +heapNames heap = concatMap (heapObjNames . snd) (heapToList heap) -- | `Name`s in a `HeapObj`. heapObjNames :: HeapObj -> [Name] +heapObjNames (AddrObj _) = [] heapObjNames (Blackhole) = [] heapObjNames (LitObj _) = [] heapObjNames (SymObj sym) = symbolNames sym @@ -84,7 +82,7 @@ -- | `Name`s in `Globals`. globalsNames :: Globals -> [Name] -globalsNames (Globals gmap) = M.keys gmap +globalsNames globals = map fst (globalsToList globals) -- | `Name`s in the current evaluation `Code`. codeNames :: Code -> [Name] @@ -116,13 +114,9 @@ pfunNames :: PrimFun -> [Name] pfunNames (PrimFun n ty) = n : typeNames ty --- | `Name`s in a `ConTag`. -conTagName :: ConTag -> Name -conTagName (ConTag n _) = n - -- | `Name`s in a `DataCon`. dataNames :: DataCon -> [Name] -dataNames (DataCon tg ty tys) = conTagName tg : concatMap typeNames (ty : tys) +dataNames (DataCon name ty tys) = name : concatMap typeNames (ty : tys) -- | `Name`s in a `TyBinder`. tyBinderNames :: TyBinder -> [Name] @@ -146,9 +140,9 @@ -- | `Name`s in a `AlgTyRhs`. algTyRhsNames :: AlgTyRhs -> [Name] algTyRhsNames (AbstractTyCon _) = [] -algTyRhsNames (DataTyCon tags) = map conTagName tags -algTyRhsNames (TupleTyCon tag) = [conTagName tag] -algTyRhsNames (NewTyCon tag) = [conTagName tag] +algTyRhsNames (DataTyCon names) = names +algTyRhsNames (TupleTyCon name) = [name] +algTyRhsNames (NewTyCon name) = [name] -- | `Name`s in a `Binding`. bindingNames :: Binding -> [Name] @@ -158,19 +152,16 @@ -- | `Name`s in a `PathCons`. pconsNames :: PathCons -> [Name] -pconsNames [] = [] -pconsNames (c:cs) = pcondNames c ++ pconsNames cs - --- | `Name`s in a `PathCond`. -pcondNames :: PathCond -> [Name] -pcondNames (PathCond (_, vars) expr locals _) = map varName vars ++ - exprNames expr ++ - localsNames locals +pconsNames pathcons = concatMap constraintNames (pathconsToList pathcons) +-- | `Name`s in a `PathCons`. +constraintNames :: Constraint -> [Name] +constraintNames (Constraint (_, vars) expr locals _) = exprNames expr ++ + localsNames locals ++ + map varName vars -- | `Name`s in a `SymLinks`. linksNames :: SymLinks -> [Name] -linksNames (SymLinks links) = concatMap (\(a, b) -> [a, b]) slist - where slist = M.toList links +linksNames symlinks = concatMap (\(a, b) -> [a, b]) (symlinksToList symlinks) -- | Create a fresh seed given any `Int`, a `String` seed, and a `Set` of -- `String`s that we do not want our new `String` to conflict with. The sole 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 @@ -57,10 +57,10 @@ isStateValueForm State { state_stack = stack , state_heap = heap , state_code = code } - | Stack [] <- stack + | Nothing <- popStack stack , Return (LitVal _) <- code = True - | Stack [] <- stack + | Nothing <- popStack stack , Return (MemVal addr) <- code , Just hobj <- lookupHeap addr heap , isHeapValueForm hobj = True @@ -70,7 +70,7 @@ -- | `Value` to `Lit`. valueToLit :: Value -> Lit valueToLit (LitVal lit) = lit -valueToLit (MemVal addr) = AddrLit (memAddrInt addr) +valueToLit (MemVal addr) = AddrLit (addrInt addr) -- | Uneven `zip` of two `List`s, with the leftover stored. unevenZip :: [a] -> [b] -> ([(a, b)], Either [a] [b]) @@ -80,7 +80,7 @@ where (acc, excess) = unevenZip as bs -- | Lift action wrapper type. -data LiftAct a = LiftAct a Locals Globals Heap [Name] +data LiftAct a = LiftAct a Locals Globals Heap [Name] -- | Lift uninterpreted `Var`s into `Globals`. liftUnInt :: LiftAct Var -> LiftAct MemAddr @@ -172,12 +172,12 @@ matchDataAlts :: DataCon -> [Alt] -> [Alt] matchDataAlts dc alts = [a | a @ (Alt (DataAlt adc) _ _) <- alts, dc == adc] --- | Negate `PathCons`. -negatePathCons :: PathCons -> PathCons -negatePathCons pcs = map (\(PathCond a e l b) -> (PathCond a e l (not b))) pcs +-- | Negate `Constraint`. +negateConstraint :: Constraint -> Constraint +negateConstraint (Constraint a e l b) = Constraint a e l (not b) -- | Lift `Alt`s during branching caused by symbolics. -liftSymAlt :: LiftAct (Var, MemAddr, Var, Alt) -> LiftAct (Expr, PathCons) +liftSymAlt :: LiftAct (Var, MemAddr, Var, Alt) -> LiftAct (Expr, [Constraint]) liftSymAlt (LiftAct args locals globals heap confs) = pass_out where (mvar, addr, cvar, Alt ac params expr) = args snames = freshSeededNameList (map varName params) confs @@ -188,19 +188,20 @@ llist = (cvar, MemVal addr) : zip params mem_vals locals' = insertLocalsList llist locals mxpr = Atom (VarAtom mvar) - pcons = [PathCond (ac, params) mxpr locals' True] + conss = [Constraint (ac, params) mxpr locals' True] confs' = snames ++ confs - pass_out = LiftAct (expr, pcons) locals' globals heap' confs' + pass_out = LiftAct (expr, conss) locals' globals heap' confs' -- | `Alt` closure to `State`. -liftedAltToState :: State -> LiftAct (Expr, PathCons) -> State +liftedAltToState :: State -> LiftAct (Expr, [Constraint]) -> State liftedAltToState state (LiftAct args locals globals heap confs) = state' - where (expr, pcons) = args + where (expr, conss) = args + pathcons = state_paths state state' = state { state_heap = heap , state_globals = globals , state_code = Evaluate expr locals , state_names = confs - , state_paths = pcons ++ state_paths state } + , state_paths = insertPathConsList conss pathcons } -- | Reduce the state if it matches some type of reduction `Rule`. Return -- `Nothing` to denote that rule application has completely failed. @@ -283,12 +284,12 @@ | Evaluate (FunApp fun args) locals <- code , Just (_, hobj) <- vlookupHeap fun locals globals heap , FunObj params expr fun_locs <- hobj - , (_, Left ex_ps) <- unevenZip params args = + , (_, Left ex_params) <- unevenZip params args = let pass_in = LiftAct args locals globals heap confs LiftAct vals _ globals' heap' confs' = liftAtomList pass_in fun_locs' = insertLocalsList (zip params vals) fun_locs -- New Fun Object. - pobj = FunObj ex_ps expr fun_locs' + pobj = FunObj ex_params expr fun_locs' (heapf, paddr) = allocHeap pobj heap' in Just (RuleFunAppUnder ,[state { state_heap = heapf @@ -388,8 +389,8 @@ -- Make AltCon states first. acon_sts = map (liftedAltToState state) acon_lifts -- Make DEFAULT states next. - all_pcons = concatMap (\(LiftAct (_, pc) _ _ _ _) -> pc) acon_lifts - negs = negatePathCons all_pcons + all_conss = concatMap (\(LiftAct (_, c) _ _ _ _) -> c) acon_lifts + negs = map negateConstraint all_conss def_lifts' = map (\(LiftAct (e, _) l g h c) -> (LiftAct (e, negs) l g h c)) def_lifts def_sts = map (liftedAltToState state) def_lifts' @@ -398,51 +399,51 @@ -- Stack Dependent Rules -- Rule Update Frame Create Thunk - | Stack frames <- stack - , Evaluate (Atom (VarAtom var)) locals <- code + | Evaluate (Atom (VarAtom var)) locals <- code , Just (addr, hobj) <- vlookupHeap var locals globals heap , FunObj [] expr fun_locs <- hobj = -- Thunk form. - Just (RuleUpdateCThunk - ,[state { state_stack = Stack (UpdateFrame addr : frames) + let frame = UpdateFrame addr + in Just (RuleUpdateCThunk + ,[state { state_stack = pushStack frame stack , state_heap = insertHeap addr Blackhole heap , state_code = Evaluate expr fun_locs }]) -- Rule Update Frame Delete Lit - | Stack (UpdateFrame frm_addr : rest) <- stack + | Just (UpdateFrame frm_addr, stack') <- popStack stack , Return (LitVal lit) <- code = Just (RuleUpdateDLit - ,[state { state_stack = Stack rest + ,[state { state_stack = stack' , state_heap = insertHeap frm_addr (LitObj lit) heap , state_code = Return (LitVal lit) }]) -- Rule Update Frame Delete Val Pointer - | Stack (UpdateFrame frm_addr : rest) <- stack + | Just (UpdateFrame frm_addr, stack') <- popStack stack , Return (MemVal addr) <- code , Just hobj <- lookupHeap addr heap , isHeapValueForm hobj = Just (RuleUpdateDValPtr - ,[state { state_stack = Stack rest - , state_heap = insertHeap frm_addr hobj heap + ,[state { state_stack = stack' + , state_heap = insertHeap frm_addr (AddrObj addr) heap , state_code = Return (MemVal addr) }]) -- Rule Case Frame Create Case Non LitVal or MemVal - | Stack frames <- stack - , Evaluate (Case mxpr cvar alts) locals <- code + | Evaluate (Case mxpr cvar alts) locals <- code , not (isExprValueForm mxpr locals globals heap) = - Just (RuleCaseCCaseNonVal - ,[state { state_stack = Stack (CaseFrame cvar alts locals : frames) + let frame = CaseFrame cvar alts locals + in Just (RuleCaseCCaseNonVal + ,[state { state_stack = pushStack frame stack , state_code = Evaluate mxpr locals }]) -- Rule Case Frame Delete Lit - | Stack (CaseFrame cvar alts frm_locs : rest) <- stack + | Just (CaseFrame cvar alts frm_locs, stack') <- popStack stack , Return (LitVal lit) <- code = let mxpr = Atom (LitAtom lit) in Just (RuleCaseDLit - ,[state { state_stack = Stack rest + ,[state { state_stack = stack' , state_code = Evaluate (Case mxpr cvar alts) frm_locs }]) -- Rule Case Frame Delete Heap Value - | Stack (CaseFrame cvar alts frm_locs : rest) <- stack + | Just (CaseFrame cvar alts frm_locs, stack') <- popStack stack , Return (MemVal addr) <- code , Just hobj <- lookupHeap addr heap , isHeapValueForm hobj = @@ -451,37 +452,37 @@ mxpr = Atom (VarAtom vvar) frm_locs' = insertLocals vvar (MemVal addr) frm_locs in Just (RuleCaseDValPtr - ,[state { state_stack = Stack rest + ,[state { state_stack = stack' , state_code = Evaluate (Case mxpr cvar alts) frm_locs' , state_names = vname : confs }]) -- Rule Apply Frame Create Function Thunk - | Stack frames <- stack - , Evaluate (FunApp fun args) locals <- code + | Evaluate (FunApp fun args) locals <- code , Just (_, hobj) <- vlookupHeap fun locals globals heap , FunObj [] expr fun_locs <- hobj = - Just (RuleApplyCFunThunk - ,[state { state_stack = Stack (ApplyFrame args locals : frames) + let frame = ApplyFrame args locals + in Just (RuleApplyCFunThunk + ,[state { state_stack = pushStack frame stack , state_code = Evaluate expr fun_locs }]) -- Rule Apply Frame Create Function Over Application - | Stack frames <- stack - , Evaluate (FunApp fun args) locals <- code + | Evaluate (FunApp fun args) locals <- code , Just (_, hobj) <- vlookupHeap fun locals globals heap , FunObj params expr fun_locs <- hobj - , (_, Right ex_as) <- unevenZip params args = + , (_, Right ex_args) <- unevenZip params args = let pass_in = LiftAct args locals globals heap confs LiftAct vals locals' globals' heap' confs' = liftAtomList pass_in fun_locs' = insertLocalsList (zip params vals) fun_locs + frame = ApplyFrame ex_args locals' in Just (RuleApplyCFunAppOver - ,[state { state_stack = Stack (ApplyFrame ex_as locals' : frames) + ,[state { state_stack = pushStack frame stack , state_heap = heap' , state_globals = globals' , state_code = Evaluate expr fun_locs' , state_names = confs' }]) -- Rule Apply Frame Delete ReturnPtr Function - | Stack (ApplyFrame args frm_locs : rest) <- stack + | Just (ApplyFrame args frm_locs, stack') <- popStack stack , Return (MemVal addr) <- code , Just hobj <- lookupHeap addr heap , FunObj _ _ _ <- hobj @@ -490,12 +491,12 @@ fvar = Var fname ftype frm_locs' = insertLocals fvar (MemVal addr) frm_locs in Just (RuleApplyDReturnFun - ,[state { state_stack = Stack rest + ,[state { state_stack = stack' , state_code = Evaluate (FunApp fvar args) frm_locs' , state_names = fname : confs }]) -- Rule Apply Frame Delete ReturnPtr Sym - | Stack (ApplyFrame args frm_locs : rest) <- stack + | Just (ApplyFrame args frm_locs, stack') <- popStack stack , Return (MemVal addr) <- code , Just hobj <- lookupHeap addr heap , SymObj (Symbol sym _) <- hobj = @@ -503,7 +504,7 @@ svar = Var sname (varType sym) frm_locs' = insertLocals svar (MemVal addr) frm_locs in Just (RuleApplyDReturnSym - ,[state { state_stack = Stack rest + ,[state { state_stack = stack' , state_code = Evaluate (FunApp svar args) frm_locs' , state_names = sname : confs }]) diff --git a/src/SSTG/Core/Execution/Support.hs b/src/SSTG/Core/Execution/Support.hs --- a/src/SSTG/Core/Execution/Support.hs +++ b/src/SSTG/Core/Execution/Support.hs @@ -1,6 +1,71 @@ -- | Symbolic STG Execution Support Architecture module SSTG.Core.Execution.Support - ( module SSTG.Core.Execution.Support + ( SymbolicT(..) + , fmap + , pure + , (<*>) + , return + , (>>=) + + , State(..) + , Symbol(..) + , Status(..) + , Stack + , Frame(..) + , MemAddr + , Value(..) + , Locals + , Heap + , HeapObj(..) + , Globals + , Code(..) + , PathCons + , Constraint(..) + , SymLinks + + , nameOccStr + , nameUnique + , varName + , nullAddr + , addrInt + + , emptyStack + , popStack + , pushStack + , stackToList + + , emptyLocals + , lookupLocals + , insertLocals + , insertLocalsList + , localsToList + + , emptyHeap + , lookupHeap + , allocHeap + , allocHeapList + , insertHeap + , insertHeapList + , heapToList + + , emptyGlobals + , lookupGlobals + , insertGlobals + , insertGlobalsList + , globalsToList + + , emptyPathCons + , insertPathCons + , insertPathConsList + , pathconsToList + + , emptySymLinks + , insertSymLinks + , symlinksToList + + , lookupValue + , vlookupHeap + , memAddrType ) where import SSTG.Core.Syntax @@ -54,7 +119,7 @@ -- | Frames of a stack. data Frame = CaseFrame Var [Alt] Locals - | ApplyFrame [Atom] Locals + | ApplyFrame [Atom] Locals | UpdateFrame MemAddr deriving (Show, Eq, Read) @@ -77,10 +142,11 @@ data Heap = Heap (M.Map MemAddr HeapObj) MemAddr deriving (Show, Eq, Read) -- | Heap objects. -data HeapObj = LitObj Lit - | SymObj Symbol - | ConObj DataCon [Value] - | FunObj [Var] Expr Locals +data HeapObj = LitObj Lit + | SymObj Symbol + | ConObj DataCon [Value] + | FunObj [Var] Expr Locals + | AddrObj MemAddr | Blackhole deriving (Show, Eq, Read) @@ -95,12 +161,12 @@ | Return Value deriving (Show, Eq, Read) --- | Path constraints. -type PathCons = [PathCond] +-- | Path constraints are the conjunctive normal form of `Constraint`s. +newtype PathCons = PathCons [Constraint] deriving (Show, Eq, Read) --- | Path conditions denote logical paths taken in program execution thus far. -data PathCond = PathCond (AltCon, [Var]) Expr Locals Bool - deriving (Show, Eq, Read) +-- | Constraints denote logical paths taken in program execution thus far. +data Constraint = Constraint (AltCon, [Var]) Expr Locals Bool + deriving (Show, Eq, Read) -- | Symbolic link tables helps keep track of what names went to what, what? newtype SymLinks = SymLinks (M.Map Name Name) deriving (Show, Eq, Read) @@ -111,7 +177,7 @@ nameOccStr :: Name -> String nameOccStr (Name occ _ _ _) = occ --- | Name's unique `Int` key. +-- | `Name` imique `Int`. nameUnique :: Name -> Int nameUnique (Name _ _ _ unq) = unq @@ -119,10 +185,35 @@ varName :: Var -> Name varName (Var name _) = name +-- | Null `MemAddr`. +nullAddr :: MemAddr +nullAddr = MemAddr 0 + -- | `MemAddr`'s `Int` value. -memAddrInt :: MemAddr -> Int -memAddrInt (MemAddr int) = int +addrInt :: MemAddr -> Int +addrInt (MemAddr int) = int +-- | Empty `Stack. +emptyStack :: Stack +emptyStack = Stack [] + +-- | `Stack` pop. +popStack :: Stack -> Maybe (Frame, Stack) +popStack (Stack []) = Nothing +popStack (Stack (f:fs)) = Just (f, Stack fs) + +-- | `Stack` push. +pushStack :: Frame -> Stack -> Stack +pushStack frame (Stack frames) = Stack (frame : frames) + +-- | `Stack` as list of `Frame`s. +stackToList :: Stack -> [Frame] +stackToList (Stack frames) = frames + +-- | Empty `Locals`. +emptyLocals :: Locals +emptyLocals = Locals M.empty + -- | `Locals` lookup. lookupLocals :: Var -> Locals -> Maybe Value lookupLocals var (Locals lmap) = M.lookup (varName var) lmap @@ -138,14 +229,24 @@ insertLocalsList ((var, val):vvs) locals = insertLocalsList vvs locals' where locals' = insertLocals var val locals +-- | `Locals` to key value pairs. +localsToList :: Locals -> [(Name, Value)] +localsToList (Locals lmap) = M.toList lmap + +-- | Empty `Heap`. +emptyHeap :: Heap +emptyHeap = Heap M.empty (MemAddr 0) + -- | `Heap` lookup. lookupHeap :: MemAddr -> Heap -> Maybe HeapObj -lookupHeap addr (Heap hmap _) = M.lookup addr hmap +lookupHeap addr (Heap hmap prev) = case M.lookup addr hmap of + Just (AddrObj redir) -> lookupHeap redir (Heap hmap prev) + mb_hobj -> mb_hobj -- | `Heap` allocation. Updates the last `MemAddr` kept in the `Heap`. allocHeap :: HeapObj -> Heap -> (Heap, MemAddr) allocHeap hobj (Heap hmap prev) = (Heap hmap' addr, addr) - where addr = MemAddr ((memAddrInt prev) + 1) + where addr = MemAddr ((addrInt prev) + 1) hmap' = M.insert addr hobj hmap -- | Allocate a list of `HeapObj` in a `Heap`, returning in the same order the @@ -167,6 +268,14 @@ insertHeapList ((addr, hobj):ahs) heap = insertHeapList ahs heap' where heap' = insertHeap addr hobj heap +-- | `Heap` to key value pairs. +heapToList :: Heap -> [(MemAddr, HeapObj)] +heapToList (Heap hmap _) = M.toList hmap + +-- | Empty `Globals`. +emptyGlobals :: Globals +emptyGlobals = Globals M.empty + -- | `Globals` lookup. lookupGlobals :: Var -> Globals -> Maybe Value lookupGlobals var (Globals gmap) = M.lookup (varName var) gmap @@ -184,13 +293,45 @@ insertGlobalsList ((var, val):vvs) globals = insertGlobalsList vvs globals' where globals' = insertGlobals var val globals +-- | `Globals` to key value pairs. +globalsToList :: Globals -> [(Name, Value)] +globalsToList (Globals gmap) = M.toList gmap + +-- | Empty `PathCons`. +emptyPathCons :: PathCons +emptyPathCons = PathCons [] + +-- | `PathCons` insertion. +insertPathCons :: Constraint -> PathCons -> PathCons +insertPathCons cons (PathCons pcs) = PathCons (cons : pcs) + +-- | Insert a list of `Constraint`s into a `PathCons`. +insertPathConsList :: [Constraint] -> PathCons -> PathCons +insertPathConsList conss pathcons = foldr insertPathCons pathcons conss + +-- | `PathCons` to list of `Constraint`s. +pathconsToList :: PathCons -> [Constraint] +pathconsToList (PathCons conss) = conss + +-- | Empty `SymLinks`. +emptySymLinks :: SymLinks +emptySymLinks = SymLinks M.empty + +-- | `SymLinks` insertion. +insertSymLinks :: Name -> Name -> SymLinks -> SymLinks +insertSymLinks old new (SymLinks smap) = SymLinks (M.insert old new smap) + +-- | `SymLinks` to list of key value pairs. +symlinksToList :: SymLinks -> [(Name, Name)] +symlinksToList (SymLinks smap) = M.toList smap + -- Complex functions that involve multiple data structures. -- | `Value` lookup from the `Locals` first, then `Globals`. lookupValue :: Var -> Locals -> Globals -> Maybe Value lookupValue var locals globals = case lookupLocals var locals of - Nothing -> lookupGlobals var globals - mb_val -> mb_val + Nothing -> lookupGlobals var globals + Just val -> Just val -- | `Heap` lookup. Returns the corresponding `MemAddr` and `HeapObj` if found. vlookupHeap :: Var -> Locals -> Globals -> Heap -> Maybe (MemAddr, HeapObj) @@ -204,10 +345,11 @@ memAddrType :: MemAddr -> Heap -> Maybe Type memAddrType addr heap = do hobj <- lookupHeap addr heap - Just $ case hobj of - Blackhole -> Bottom - LitObj lit -> litType lit - SymObj (Symbol s _) -> varType s - ConObj dcon _ -> dataConType dcon - FunObj prms expr _ -> foldr FunTy (exprType expr) (map varType prms) + case hobj of + AddrObj redir -> memAddrType redir heap + LitObj lit -> Just (litType lit) + SymObj (Symbol s _) -> Just (varType s) + ConObj dcon _ -> Just (dataConType dcon) + FunObj ps e _ -> Just (foldr FunTy (exprType e) (map varType ps)) + Blackhole -> Just Bottom diff --git a/src/SSTG/Core/Syntax/Language.hs b/src/SSTG/Core/Syntax/Language.hs --- a/src/SSTG/Core/Syntax/Language.hs +++ b/src/SSTG/Core/Syntax/Language.hs @@ -14,7 +14,6 @@ type Binding = GenBinding Name Var type BindRhs = GenBindRhs Name Var -type ConTag = GenConTag Name type DataCon = GenDataCon Name type Type = GenType Name type TyBinder = GenTyBinder Name @@ -47,18 +46,18 @@ -- value deriviation, `SymLit` for symbolic literals, and `SymLitEval` to -- represent symbolic literal evaluation, as literal manipulation functions -- are defined in the Haskell Prelude, and thus outside of scope for us. -data GenLit bnd var = MachChar Char (GenType bnd) - | MachStr String (GenType bnd) - | MachInt Int (GenType bnd) - | MachWord Int (GenType bnd) - | MachFloat Rational (GenType bnd) - | MachDouble Rational (GenType bnd) - | MachNullAddr (GenType bnd) - | MachLabel String (Maybe Int) (GenType bnd) +data GenLit bnd var = MachChar Char (GenType bnd) + | MachStr String (GenType bnd) + | MachInt Int (GenType bnd) + | MachWord Int (GenType bnd) + | MachFloat Rational (GenType bnd) + | MachDouble Rational (GenType bnd) + | MachNullAddr (GenType bnd) + | MachLabel String (Maybe Int) (GenType bnd) | BlankAddr - | AddrLit Int - | SymLit var - | SymLitEval (GenPrimFun bnd var) [GenLit bnd var] + | AddrLit Int + | SymLit var + | SymLitEval (GenPrimFun bnd var) [GenLit bnd var] deriving (Show, Eq, Read) -- | Atomic objects. `VarAtom` may be used for variable lookups, while @@ -72,10 +71,10 @@ -- | Expressions closely correspond to their representation in GHC. data GenExpr bnd var = Atom (GenAtom bnd var) - | PrimApp (GenPrimFun bnd var) [GenAtom bnd var] - | ConApp (GenDataCon bnd) [GenAtom bnd var] - | FunApp var [GenAtom bnd var] - | Let (GenBinding bnd var) (GenExpr bnd var) + | PrimApp (GenPrimFun bnd var) [GenAtom bnd var] + | ConApp (GenDataCon bnd) [GenAtom bnd var] + | FunApp var [GenAtom bnd var] + | Let (GenBinding bnd var) (GenExpr bnd var) | Case (GenExpr bnd var) var [GenAlt bnd var] deriving (Show, Eq, Read) @@ -100,34 +99,31 @@ -- | `BindRhs` taken straight from STG can be either in constructor form, or -- function form. Empty parameter list denotes a thunk. data GenBindRhs bnd var = ConForm (GenDataCon bnd) [GenAtom bnd var] - | FunForm [var] (GenExpr bnd var) + | FunForm [var] (GenExpr bnd var) deriving (Show, Eq, Read) --- | Data Constructor tag that uniquely identifiers data constructors. -data GenConTag bnd = ConTag bnd Int deriving (Show, Eq, Read) - -- | Data Constructor consists of its tag, the type that corresponds to its -- ADT, and a list of paramters it takes. -data GenDataCon bnd = DataCon (GenConTag bnd) (GenType bnd) [GenType bnd] +data GenDataCon bnd = DataCon bnd (GenType bnd) [GenType bnd] deriving (Show, Eq, Read) -- | Types are information that are useful to keep during symbolic execution -- in order to generate correct feeds into the SMT solver. Overapproxmation is -- currently performed, and is likely to be cut back in the future. -data GenType bnd = TyVarTy bnd (GenType bnd) - | AppTy (GenType bnd) (GenType bnd) +data GenType bnd = TyVarTy bnd (GenType bnd) + | AppTy (GenType bnd) (GenType bnd) | ForAllTy (GenTyBinder bnd) (GenType bnd) - | CastTy (GenType bnd) (GenCoercion bnd) - | TyConApp (GenTyCon bnd) [GenType bnd] + | CastTy (GenType bnd) (GenCoercion bnd) + | TyConApp (GenTyCon bnd) [GenType bnd] | CoercionTy (GenCoercion bnd) | LitTy TyLit - | FunTy (GenType bnd) (GenType bnd) + | FunTy (GenType bnd) (GenType bnd) | Bottom deriving (Show, Eq, Read) -- | Type binder for `ForAllTy`. data GenTyBinder bnd = NamedTyBndr bnd (GenType bnd) - | AnonTyBndr (GenType bnd) + | AnonTyBndr (GenType bnd) deriving (Show, Eq, Read) -- | `Type` literal. @@ -151,8 +147,8 @@ -- | ADT RHS. data GenAlgTyRhs bnd = AbstractTyCon Bool - | DataTyCon [GenConTag bnd] - | TupleTyCon (GenConTag bnd) - | NewTyCon (GenConTag bnd) + | DataTyCon [bnd] + | NewTyCon bnd + | TupleTyCon bnd deriving (Show, Eq, Read) 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 @@ -146,16 +146,14 @@ MachNullAddr -> SL.MachNullAddr ((mkType . literalType) lit) (MachLabel f m _) -> SL.MachLabel (unpackFS f) m ((mkType . literalType) lit) --- | Make SSTG `ConTag`. -mkDataTag :: DataCon -> SL.ConTag -mkDataTag datacon = SL.ConTag name tag - where name = (mkName . dataConName) datacon - tag = dataConTag datacon +-- | `DataCon`'s `Name`. +mkDataName :: DataCon -> SL.Name +mkDataName datacon = (mkName. dataConName) datacon -- | Make SSTG `DataCon`. mkData :: DataCon -> SL.DataCon -mkData datacon = SL.DataCon dcid ty args - where dcid = mkDataTag datacon +mkData datacon = SL.DataCon name ty args + where name = mkDataName datacon ty = (mkType . dataConRepType) datacon args = map mkType (dataConOrigArgTys datacon) @@ -205,10 +203,10 @@ -- | Make SSTG `AlgTyRhs`. mkAlgTyConRhs :: AlgTyConRhs -> SL.AlgTyRhs -mkAlgTyConRhs (AbstractTyCon b) = SL.AbstractTyCon b -mkAlgTyConRhs (DataTyCon {data_cons = dcs}) = SL.DataTyCon (map mkDataTag dcs) -mkAlgTyConRhs (TupleTyCon {data_con = dc}) = SL.TupleTyCon (mkDataTag dc) -mkAlgTyConRhs (NewTyCon {data_con = dc}) = SL.NewTyCon (mkDataTag dc) +mkAlgTyConRhs (AbstractTyCon b) = SL.AbstractTyCon b +mkAlgTyConRhs (DataTyCon {data_cons = ds}) = SL.DataTyCon (map mkDataName ds) +mkAlgTyConRhs (TupleTyCon {data_con = d}) = SL.TupleTyCon (mkDataName d) +mkAlgTyConRhs (NewTyCon {data_con = d}) = SL.NewTyCon (mkDataName d) -- | make SSTG `TyBinder`. mkTyBndr :: TyBinder -> SL.TyBinder 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 @@ -7,7 +7,6 @@ import SSTG.Core -import qualified Data.Map as M import qualified Data.List as L -- | Print `LiveState` and `DeadState` that yield from execution snapshots. @@ -50,8 +49,8 @@ globals_str = (pprGlobalsStr . state_globals) state expr_str = (pprCodeStr . state_code) state names_str = (pprNamesStr . state_names) state - pcons_str = (pprPConsStr . state_paths) state - links_str = (pprLinksStr . state_links) state + pcons_str = (pprPathConsStr . state_paths) state + links_str = (pprSymLinksStr . state_links) state acc_strs = [ ">>>>> [State] >>>>>>>>>>>>>>>" , status_str , "----- [Stack] ---------------" @@ -102,7 +101,7 @@ -- | Print `MemAddr`. pprMemAddrStr :: MemAddr -> String -pprMemAddrStr (MemAddr int) = show int +pprMemAddrStr addr = show (addrInt addr) -- | Print `Name`. pprNameStr :: Name -> String @@ -118,8 +117,8 @@ -- | Print `Stack`. pprStackStr :: Stack -> String -pprStackStr (Stack stack) = injNewLineSeps10 acc_strs - where frame_strs = map pprFrameStr stack +pprStackStr stack = injNewLineSeps10 acc_strs + where frame_strs = map pprFrameStr (stackToList stack) acc_strs = "Stack" : frame_strs -- | Print `Frame`. @@ -152,6 +151,7 @@ -- | Print `HeapObj`. pprHeapObjStr :: HeapObj -> String pprHeapObjStr (Blackhole) = "Blackhole!!!" +pprHeapObjStr (AddrObj addr) = pprMemAddrStr addr pprHeapObjStr (LitObj lit) = injSpace acc_strs where header = "LitObj" lit_str = pprLitStr lit @@ -175,32 +175,30 @@ -- | Print `Heap`. pprHeapStr :: Heap -> String -pprHeapStr (Heap hmap addr) = injNewLine (map (\k -> ">" ++ k) acc_strs) - where kvs = M.toList hmap - addr_strs = map (pprMemAddrStr . fst) kvs - hobj_strs = map (pprHeapObjStr . snd) kvs +pprHeapStr heap = injNewLine acc_strs + where hlist = heapToList heap + addr_strs = map (pprMemAddrStr . fst) hlist + hobj_strs = map (pprHeapObjStr . snd) hlist zipd_strs = zip addr_strs hobj_strs - addr_str = pprMemAddrStr addr - kvs_strs = map (\(m, o) -> sub (m ++ "," ++ o)) zipd_strs - acc_strs = addr_str : kvs_strs + acc_strs = map (\(m, o) -> sub (m ++ ", " ++ o)) zipd_strs -- | Print `Globals`. pprGlobalsStr :: Globals -> String -pprGlobalsStr (Globals gmap) = injNewLine (map (\k -> ">" ++ k) acc_strs) - where kvs = M.toList gmap - name_strs = map (pprNameStr . fst) kvs - val_strs = map (pprValueStr . snd) kvs +pprGlobalsStr globals = injNewLine acc_strs + where glist = globalsToList globals + name_strs = map (pprNameStr . fst) glist + val_strs = map (pprValueStr . snd) glist zipd_strs = zip name_strs val_strs - acc_strs = map (\(n, v) -> sub (n ++ "," ++ v)) zipd_strs + acc_strs = map (\(n, v) -> sub (n ++ ", " ++ v)) zipd_strs -- | Print `Locals`. pprLocalsStr :: Locals -> String -pprLocalsStr (Locals lmap) = injIntoList acc_strs - where kvs = M.toList lmap - name_strs = map (pprNameStr . fst) kvs - val_strs = map (pprValueStr . snd) kvs +pprLocalsStr locals = injIntoList acc_strs + where llist = localsToList locals + name_strs = map (pprNameStr . fst) llist + val_strs = map (pprValueStr . snd) llist zipd_strs = zip name_strs val_strs - acc_strs = map (\(n, v) -> sub (n ++ "," ++ v)) zipd_strs + acc_strs = map (\(n, v) -> sub (n ++ ", " ++ v)) zipd_strs -- | Print `Value`. pprValueStr :: Value -> String @@ -232,15 +230,11 @@ lit_str = (sub . pprLitStr) lit acc_strs = [header, lit_str] --- | Print `ConTag`. -pprConTagStr :: ConTag -> String -pprConTagStr (ConTag name _) = pprNameStr name - -- | Print `DataCon`. pprDataConStr :: DataCon -> String -pprDataConStr (DataCon tag ty tys) = injSpace acc_strs +pprDataConStr (DataCon name ty tys) = injSpace acc_strs where header = "DataCon" - tag_str = (sub . pprConTagStr) tag + tag_str = (sub . pprNameStr) name ty_str = (sub . pprTypeStr) ty tys_str = injIntoList (map pprTypeStr tys) acc_strs = [header, tag_str, ty_str, tys_str] @@ -360,23 +354,23 @@ pprNamesStr names = injIntoList (map pprNameStr names) -- | Print `PathCons`. -pprPConsStr :: PathCons -> String -pprPConsStr pathcons = injNewLineSeps5 strs - where strs = map pprPCondStr pathcons +pprPathConsStr :: PathCons -> String +pprPathConsStr pathcons = injNewLineSeps5 strs + where strs = map pprConstraintStr (pathconsToList pathcons) -- | Print `PathCond`. -pprPCondStr :: PathCond -> String -pprPCondStr (PathCond (acon, params) expr locals hold) = injIntoList acc_strs - where acon_str = pprAltConStr acon - prms_str = injIntoList (map pprVarStr params) +pprConstraintStr :: Constraint -> String +pprConstraintStr (Constraint (ac, ps) expr locals hold) = injIntoList acc_strs + where acon_str = pprAltConStr ac + prms_str = injIntoList (map pprVarStr ps) expr_str = pprExprStr expr locs_str = pprLocalsStr locals hold_str = case hold of { True -> "Positive"; False -> "Negative" } acc_strs = [acon_str, prms_str, expr_str, locs_str, hold_str] -- | Print `SymLinks`. -pprLinksStr :: SymLinks -> String -pprLinksStr (SymLinks links) = injNewLineSeps5 acc_strs - where kvs = M.toList links - acc_strs = map (\(k, v) -> pprNameStr k ++ " -> " ++ pprNameStr v) kvs +pprSymLinksStr :: SymLinks -> String +pprSymLinksStr symlinks = injNewLineSeps5 acc_strs + where slist = symlinksToList symlinks + acc_strs = map (\(k, v) -> pprNameStr k ++ ", " ++ pprNameStr v) slist