SSTG 0.1.1.5 → 0.1.1.6

raw patch · 8 files changed

+46/−42 lines, 8 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• SSTG.cabal +1/−1
• src/SSTG/Core/Execution/Rules.hs +22/−21
• src/SSTG/Core/Execution/Support.hs +1/−2
• src/SSTG/Core/Language/Naming.hs +6/−1
• src/SSTG/Core/Language/Syntax.hs +2/−2
• src/SSTG/Core/Language/Typing.hs +1/−1
• src/SSTG/Core/Translation/Haskell.hs +5/−5
• src/SSTG/Utils/Printing.hs +8/−9

@@ -1,5 +1,5 @@ name:                SSTG-version:             0.1.1.5+version:             0.1.1.6 synopsis:            STG Symbolic Execution description:         Prototype of STG-based Symbolic Execution for Haskell. homepage:            https://github.com/AntonXue/SSTG#readme

@@ -138,9 +138,9 @@   where     pass_in = LiftAct rhs locals globals heap confs     pass_rest = LiftAct rs locals' globals' heap' confs'-    pass_out = LiftAct (hobj : hos) localsf globalsf heapf confsf+    pass_out = LiftAct (hobj : hs) localsf globalsf heapf confsf     LiftAct hobj locals' globals' heap' confs' = liftBindRhs pass_in-    LiftAct hos localsf globalsf heapf confsf = liftBindRhss pass_rest+    LiftAct hs localsf globalsf heapf confsf = liftBindRhss pass_rest  -- | Lift `Binds`. liftBinds :: LiftAct Binds -> LiftAct ()@@ -167,19 +167,19 @@  -- | `Default` `Alt` branches in a `Case`. defaultAlts :: [Alt] -> [Alt]-defaultAlts alts = [a | a @ (Alt Default _ _) <- alts]+defaultAlts alts = [a | a @ (Alt Default _) <- alts]  -- | `AltCon` `Alt` branches in a `Case`.-altConAlts :: [Alt] -> [Alt]-altConAlts alts = [a | a @ (Alt acon _ _) <- alts, acon /= Default]+nonDefaultAlts :: [Alt] -> [Alt]+nonDefaultAlts alts = [a | a @ (Alt acon _) <- alts, acon /= Default]  -- | Match `LitAlt` `Alt` branches. matchLitAlts :: Lit -> [Alt] -> [Alt]-matchLitAlts lit alts = [a | a @ (Alt (LitAlt alit) _ _) <- alts, lit == alit]+matchLitAlts lit alts = [a | a @ (Alt (LitAlt alit) _) <- alts, lit == alit]  -- | Match `DataCon` `Alt` branches. matchDataAlts :: DataCon -> [Alt] -> [Alt]-matchDataAlts dc alts = [a | a @ (Alt (DataAlt adc) _ _) <- alts, dc == adc]+matchDataAlts dc alts = [a | a @ (Alt (DataAlt adc _) _) <- alts, dc == adc]  -- | Negate `Constraint`. negateConstraint :: Constraint -> Constraint@@ -189,7 +189,8 @@ 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+    (mvar, addr, cvar, Alt acon expr) = args+    params = case acon of { DataAlt _ ps -> ps ; _ -> [] }     snames = freshSeededNames (map varName params) confs     svars = map (\(p, n) -> Var n (varType p)) (zip params snames)     hobjs = map (\s -> SymObj (Symbol s Nothing)) svars@@ -198,7 +199,7 @@     kvs = (cvar, MemVal addr) : zip params mem_vals     locals' = insertLocalsVals kvs locals     mexpr = Atom (VarAtom mvar)-    conss = [Constraint (ac, params) mexpr locals' True]+    conss = [Constraint acon mexpr locals' True]     confs' = snames ++ confs     pass_out = LiftAct (expr, conss) locals' globals heap' confs' @@ -351,7 +352,7 @@    -- Rule Case Lit   | Evaluate (Case (Atom (LitAtom lit)) cvar alts) locals <- code-  , (Alt _ _ expr):_ <- matchLitAlts lit alts =+  , (Alt _ expr):_ <- matchLitAlts lit alts =     let locals' = insertLocalsVal (cvar, LitVal lit) locals     in Just (RuleCaseLit             ,[state { state_code = Evaluate expr locals' }])@@ -360,7 +361,7 @@   | Evaluate (Case (Atom (VarAtom mvar)) cvar alts) locals <- code   , Just (addr, hobj) <- vlookupHeap mvar locals globals heap   , ConObj dcon vals <- hobj-  , (Alt _ params expr):_ <- matchDataAlts dcon alts+  , (Alt (DataAlt _ params) expr):_ <- matchDataAlts dcon alts   , length params == length vals =     let kvs = (cvar, MemVal addr) : zip params vals         locals' = insertLocalsVals kvs locals@@ -370,7 +371,7 @@   -- Rule Case Any Lit   | Evaluate (Case (Atom (LitAtom lit)) cvar alts) locals <- code   , [] <- matchLitAlts lit alts-  , (Alt _ _ expr):_ <- defaultAlts alts =+  , (Alt _ expr):_ <- defaultAlts alts =     let locals' = insertLocalsVal (cvar, LitVal lit) locals     in Just (RuleCaseAnyLit             ,[state { state_code = Evaluate expr locals' }])@@ -380,7 +381,7 @@   , Just (addr, hobj) <- vlookupHeap mvar locals globals heap   , ConObj dcon _ <- hobj   , [] <- matchDataAlts dcon alts-  , (Alt _ _ expr):_ <- defaultAlts alts =+  , (Alt _ expr):_ <- defaultAlts alts =     let locals' = insertLocalsVal (cvar, MemVal addr) locals     in Just (RuleCaseAnyConPtr             ,[state { state_code = Evaluate expr locals' }])@@ -389,23 +390,23 @@   | Evaluate (Case (Atom (VarAtom mvar)) cvar alts) locals <- code   , Just (addr, hobj) <- vlookupHeap mvar locals globals heap   , SymObj _ <- hobj-  , (acon_alts, def_alts) <- (altConAlts alts, defaultAlts alts)-  , length (acon_alts ++ def_alts) > 0 =-    let acon_ins = map (\a -> LiftAct (mvar, addr, cvar, a)-                                      locals globals heap confs) acon_alts-        acon_lifts = map liftSymAlt acon_ins+  , (ndef_alts, def_alts) <- (nonDefaultAlts alts, defaultAlts alts)+  , length (ndef_alts ++ def_alts) > 0 =+    let ndef_ins = map (\a -> LiftAct (mvar, addr, cvar, a)+                                      locals globals heap confs) ndef_alts+        ndef_lifts = map liftSymAlt ndef_ins         def_ins = map (\a -> LiftAct (mvar, addr, cvar, a)                                      locals globals heap confs) def_alts         def_lifts = map liftSymAlt def_ins         -- Make AltCon states first.-        acon_sts = map (liftedAltToState state) acon_lifts+        ndef_sts = map (liftedAltToState state) ndef_lifts         -- Make DEFAULT states next.-        all_conss = concatMap (\(LiftAct (_, c) _ _ _ _) -> c) acon_lifts+        all_conss = concatMap (\(LiftAct (_, c) _ _ _ _) -> c) ndef_lifts         negatives = map negateConstraint all_conss         def_lifts' = map (\(LiftAct (e, _) l g h c) ->                            (LiftAct (e, negatives) l g h c)) def_lifts         def_sts = map (liftedAltToState state) def_lifts'-    in Just (RuleCaseSym, acon_sts ++ def_sts)+    in Just (RuleCaseSym, ndef_sts ++ def_sts)  -- Stack Dependent Rules 

@@ -165,8 +165,7 @@ 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)+data Constraint = Constraint AltCon Expr Locals Bool deriving (Show, Eq, Read)  -- Simple functions that require only the immediate data structure. 

@@ -65,7 +65,12 @@  -- | `Name`s in an `Alt`. altNames :: Alt -> [Name]-altNames (Alt _ vars expr) = concatMap varNames vars ++ exprNames expr+altNames (Alt acon expr) = altConNames acon ++ exprNames expr++-- | `Name`s in an `AltCon`.+altConNames :: AltCon -> [Name]+altConNames (DataAlt dcon ps) = dataConNames dcon ++ concatMap varNames ps+altConNames _ = []  -- | `Name`s in a `Type`. typeNames :: Type -> [Name]

@@ -60,10 +60,10 @@  -- | Alternatives utilize an `AltCon`, a list of parameters of that match to -- the appropriate `DataAlt` as applicable, and an expression for the result.-data Alt = Alt AltCon [Var] Expr deriving (Show, Eq, Read)+data Alt = Alt AltCon Expr deriving (Show, Eq, Read)  -- | Alt Constructor-data AltCon = DataAlt DataCon+data AltCon = DataAlt DataCon [Var]             | LitAlt Lit             | Default             deriving (Show, Eq, Read)

@@ -38,7 +38,7 @@  -- | Alt type altType :: Alt -> Type-altType (Alt _ _ expr) = exprType expr+altType (Alt _ expr) = exprType expr  -- | I wonder what this could possibly be? exprType :: Expr -> Type

@@ -172,13 +172,13 @@  -- | Make SSTG `Alt`. mkAlt :: StgAlt -> SL.Alt-mkAlt (a, b, _, e) = SL.Alt (mkAltCon a) (map mkVar b) (mkExpr e)+mkAlt (a, ps, _, e) = SL.Alt (mkAltCon a ps) (mkExpr e)  -- | Make SSTG `AltCon`.-mkAltCon :: AltCon -> SL.AltCon-mkAltCon (DataAlt dc) = SL.DataAlt (mkData dc)-mkAltCon (LitAlt lit) = SL.LitAlt (mkLit lit)-mkAltCon (DEFAULT) = SL.Default+mkAltCon :: AltCon -> [Var] -> SL.AltCon+mkAltCon (DataAlt dcon) params = SL.DataAlt (mkData dcon) (map mkVar params)+mkAltCon (LitAlt lit) _ = SL.LitAlt (mkLit lit)+mkAltCon (DEFAULT) _ = SL.Default  -- | Make SSTG `Type`. mkType :: Type -> SL.Type

@@ -283,11 +283,12 @@  -- | Print `AltCon`. pprAltConStr :: AltCon -> String-pprAltConStr (DataAlt dcon) = injSpace acc_strs+pprAltConStr (DataAlt dcon params) = injSpace acc_strs   where     header = "DataAlt"     dcon_str = (sub . pprDataConStr) dcon-    acc_strs = [header, dcon_str]+    ps_str = injIntoList (map pprVarStr params)+    acc_strs = [header, dcon_str, ps_str] pprAltConStr (LitAlt lit) = injSpace acc_strs   where     header = "LitAlt"@@ -297,13 +298,12 @@  -- | Print `Alt`. pprAltStr :: Alt -> String-pprAltStr (Alt acon var expr) = injSpace acc_strs+pprAltStr (Alt acon expr) = injSpace acc_strs   where     header = "Alt"     acon_str = (sub . pprAltConStr) acon-    vars_str = injIntoList (map pprVarStr var)     expr_str = (sub . pprExprStr) expr-    acc_strs = [header, acon_str, vars_str, expr_str]+    acc_strs = [header, acon_str, expr_str]  -- | Print a list of `Alt`s. pprAltsStr :: [Alt] -> String@@ -410,12 +410,11 @@  -- | Print `PathCond`. pprConstraintStr :: Constraint -> String-pprConstraintStr (Constraint (ac, ps) expr locals hold) = injIntoList acc_strs+pprConstraintStr (Constraint acon expr locals hold) = injIntoList acc_strs   where-    acon_str = pprAltConStr ac-    prms_str = injIntoList (map pprVarStr ps)+    acon_str = pprAltConStr acon     expr_str = pprExprStr expr     locs_str = pprLocalsStr locals     hold_str = if hold then "Positive" else "Negative"-    acc_strs = [acon_str, prms_str, expr_str, locs_str, hold_str]+    acc_strs = [acon_str, expr_str, locs_str, hold_str]