diff --git a/SSTG.cabal b/SSTG.cabal --- a/SSTG.cabal +++ b/SSTG.cabal @@ -1,5 +1,5 @@ name: SSTG -version: 0.1.0.2 +version: 0.1.0.3 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 @@ -144,7 +144,7 @@ names' = freshSeededNameList confs confs adjusted = map (\(n, t) -> Var n t) (zip names' (map varType actuals)) -- Throw the parameters on heap as symbolic objects - sym_objs = map (\p -> SymObj (Symbol p)) adjusted + sym_objs = map (\p -> SymObj (Symbol p Nothing)) adjusted (heap', addrs) = allocHeapList sym_objs heap -- make Atom representations for arguments and shove into locals. mem_vals = map (\a -> MemVal a) addrs diff --git a/src/SSTG/Core/Execution/Models.hs b/src/SSTG/Core/Execution/Models.hs --- a/src/SSTG/Core/Execution/Models.hs +++ b/src/SSTG/Core/Execution/Models.hs @@ -42,7 +42,7 @@ } deriving (Show, Eq, Read) -- | Symbolic -newtype Symbol = Symbol Var deriving (Show, Eq, Read) +data Symbol = Symbol Var (Maybe (Expr, Locals)) deriving (Show, Eq, Read) -- | Status data Status = Status { steps :: Int @@ -194,9 +194,9 @@ memAddrType addr heap = do hobj <- lookupHeap addr heap return $ case hobj of - Blackhole -> Bottom - LitObj lit -> litType lit - SymObj (Symbol sv) -> varType sv - ConObj dcon _ -> dataConType dcon - FunObj prms expr _ -> foldr FunTy (exprType expr) (map varType prms) + 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) diff --git a/src/SSTG/Core/Execution/Namer.hs b/src/SSTG/Core/Execution/Namer.hs --- a/src/SSTG/Core/Execution/Namer.hs +++ b/src/SSTG/Core/Execution/Namer.hs @@ -54,7 +54,7 @@ -- | Heap Object Names heapObjNames :: HeapObj -> [Name] -heapObjNames Blackhole = [] +heapObjNames (Blackhole) = [] heapObjNames (LitObj _) = [] heapObjNames (SymObj sym) = symbolNames sym heapObjNames (ConObj dcon _) = dataNames dcon @@ -63,7 +63,10 @@ -- | Symbol Names symbolNames :: Symbol -> [Name] -symbolNames (Symbol sym) = varNames sym +symbolNames (Symbol sym mb_scls) = varNames sym ++ scls_names + where scls_names = case mb_scls of + Nothing -> [] + Just (e, l) -> exprNames e ++ localsNames l -- | Lambda Form Names bindRhsNames :: BindRhs -> [Name] 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 @@ -87,7 +87,7 @@ liftUnInt (LiftAct var locals globals heap confs) = pass_out where sname = freshSeededName (varName var) confs svar = Var sname (varType var) - (heap', addr) = allocHeap (SymObj (Symbol svar)) heap + (heap', addr) = allocHeap (SymObj (Symbol svar Nothing)) heap globals' = insertGlobals var (MemVal addr) globals confs' = sname : confs pass_out = LiftAct addr locals globals' heap' confs' @@ -182,7 +182,7 @@ where (mvar, addr, cvar, Alt ac params expr) = args snames = freshSeededNameList (map varName params) confs svars = map (\(p, n) -> Var n (varType p)) (zip params snames) - hobjs = map (SymObj . Symbol) svars + hobjs = map (\s -> SymObj (Symbol s Nothing)) svars (heap', addrs) = allocHeapList hobjs heap mem_vals = map MemVal addrs llist = (cvar, MemVal addr) : zip params mem_vals @@ -297,11 +297,11 @@ -- Rule Fun App Symbolic | Evaluate (FunApp sfun args) locals <- code - , Just (_, hobj) <- vlookupHeap sfun locals globals heap - , SymObj (Symbol svar) <- hobj = do + , Just (_, hobj) <- vlookupHeap sfun locals globals heap + , SymObj (Symbol svar _) <- hobj = do let sname = freshSeededName (varName svar) confs let svar' = Var sname (foldl AppTy (varType svar) (map atomType args)) - let sym = Symbol svar' + let sym = Symbol svar' (Just (FunApp sfun args, locals)) let (heap', addr) = allocHeap (SymObj sym) heap return ( RuleFunAppSym , [state { state_heap = heap' @@ -501,8 +501,8 @@ -- Rule Apply Frame Delete ReturnPtr Sym | Stack (ApplyFrame args frm_locs : rest) <- stack , Return (MemVal addr) <- code - , Just hobj <- lookupHeap addr heap - , SymObj (Symbol sym) <- hobj = do + , Just hobj <- lookupHeap addr heap + , SymObj (Symbol sym _) <- hobj = do let sname = freshSeededName (varName sym) confs let svar = Var sname (varType sym) let frm_locs' = insertLocals svar (MemVal addr) frm_locs diff --git a/src/SSTG/Utils/PrettyPrint.hs b/src/SSTG/Utils/PrettyPrint.hs --- a/src/SSTG/Utils/PrettyPrint.hs +++ b/src/SSTG/Utils/PrettyPrint.hs @@ -128,16 +128,25 @@ addr_str = pprMemAddrStr addr acc_strs = [header, addr_str] +pprSymClosureStr :: Maybe (Expr, Locals) -> String +pprSymClosureStr (Nothing) = "SymClosure ()" +pprSymClosureStr (Just (expr, locals)) = injSpace acc_strs + where header = "SymClosure" + expr_str = pprExprStr expr + locs_str = pprLocalsStr locals + acc_strs = [header, injIntoList [expr_str, locs_str]] + pprHeapObjStr :: HeapObj -> String -pprHeapObjStr Blackhole = "Blackhole!!!" +pprHeapObjStr (Blackhole) = "Blackhole!!!" pprHeapObjStr (LitObj lit) = injSpace acc_strs where header = "LitObj" lit_str = pprLitStr lit acc_strs = [header, lit_str] -pprHeapObjStr (SymObj (Symbol sym)) = injSpace acc_strs +pprHeapObjStr (SymObj (Symbol sym mb_scls)) = injSpace acc_strs where header = "SymObj" var_str = pprVarStr sym - acc_strs = [header, var_str] + scls_str = (sub . pprSymClosureStr) mb_scls + acc_strs = [header, var_str, scls_str] pprHeapObjStr (ConObj dcon vals) = injSpace acc_strs where header = "ConObj" dcon_str = pprDataConStr dcon @@ -230,7 +239,7 @@ where header = "LitAlt" lit_str = (sub . pprLitStr) lit acc_strs = [header, lit_str] -pprAltConStr Default = "Default" +pprAltConStr (Default) = "Default" pprAltStr :: Alt -> String pprAltStr (Alt acon var expr) = injSpace acc_strs