SSTG 0.1.0.2 → 0.1.0.3

raw patch · 6 files changed

+33/−21 lines, 6 files

Files

• SSTG.cabal +1/−1
• src/SSTG/Core/Execution/Engine.hs +1/−1
• src/SSTG/Core/Execution/Models.hs +6/−6
• src/SSTG/Core/Execution/Namer.hs +5/−2
• src/SSTG/Core/Execution/Rules.hs +7/−7
• src/SSTG/Utils/PrettyPrint.hs +13/−4

@@ -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

@@ -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

@@ -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) 

@@ -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]

@@ -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

@@ -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