SSTG 0.1.0.8 → 0.1.0.9

raw patch · 9 files changed

+89/−91 lines, 9 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• README.md +1/−1
• SSTG.cabal +1/−1
• app/Main.hs +2/−2
• src/SSTG/Core/Execution/Engine.hs +6/−6
• src/SSTG/Core/Execution/Naming.hs +16/−17
• src/SSTG/Core/Execution/Rules.hs +6/−6
• src/SSTG/Core/Execution/Support.hs +21/−21
• src/SSTG/Core/Syntax/Language.hs +8/−9
• src/SSTG/Core/Translation/Haskell.hs +28/−28

@@ -51,7 +51,7 @@ ```  #### Defunctionalization-HEY KIDS YA EVER WANNA REASON ABOUT HIGHER-ORDER FUNCTIONS BUT YOUR SMT SOLVER AIN'T SMAHT ENOUGH??? CHECK OUT THIS [COOL WIKIPEDIA ARTICLE RIGHT HERE!!!][defunctionalization]+[Defunctionalization Wikipedia article][defunctionalization]  [defunctionalization]: https://en.wikipedia.org/wiki/Defunctionalization 

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

@@ -39,9 +39,9 @@  parseDumpDir :: [String] -> Maybe FilePath parseDumpDir args = case matchArg "--dump" args (readMaybe . show) Nothing of-    Nothing  -> error "part1"+    Nothing  -> Nothing     Just raw -> case trimSlash raw of-                    "" -> error "part2"+                    "" -> error ("Invalid use of " ++ raw)                     ok -> Just ok  parseFlags :: [String] -> RunFlags

@@ -36,11 +36,11 @@   where -- Status or something.         status   = Status { steps = 0 }         -- Stack initialized to empty.-        stack    = emptyStack+        stack    = empty_stack         -- Globals and Heap are loaded together. They are still beta forms now.-        heap0    = emptyHeap+        heap0    = empty_heap         (glist, heap1, bnd_addrss) = initGlobals bnds heap0-        globals0 = insertGlobalsList glist emptyGlobals+        globals0 = insertGlobalsList glist empty_globals         (heap2, localss) = liftBindings bnd_addrss globals0 heap1         bnd_locs = zip bnds localss         -- Code loading. Completes heap and globals with symbolic injection.@@ -55,8 +55,8 @@                          , state_globals = globals                          , state_code    = code                          , state_names   = []-                         , state_paths   = emptyPathCons-                         , state_links   = emptySymLinks }+                         , state_paths   = empty_pathcons+                         , state_links   = empty_symlinks }          -- Gather information on all variables.         state    = state0 { state_names = allNames state0 }@@ -106,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   = emptyLocals+        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

@@ -61,10 +61,10 @@  -- | `Name`s in a `Symbol`. symbolNames :: Symbol -> [Name]-symbolNames (Symbol sym mb_scls) = varNames sym ++ scls_names-  where scls_names = case mb_scls of-                         Nothing     -> []-                         Just (e, l) -> exprNames e ++ localsNames l+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 `BindRhs`. bindRhsNames :: BindRhs -> [Name]@@ -116,22 +116,21 @@  -- | `Name`s in a `DataCon`. dataNames :: DataCon -> [Name]-dataNames (DataCon name ty tys) = name : concatMap typeNames (ty : tys)+dataNames (DataCon n ty tys) = n : concatMap typeNames (ty : tys)  -- | `Name`s in a `TyBinder`. tyBinderNames :: TyBinder -> [Name]-tyBinderNames (NamedTyBndr n ty) = n : typeNames ty-tyBinderNames (AnonTyBndr ty)    = typeNames ty+tyBinderNames (AnonTyBndr)    = []+tyBinderNames (NamedTyBndr n) = [n]  -- | `Name`s in a `TyCon`. tyConNames :: TyCon -> [Name]-tyConNames (FunTyCon n)      = [n]-tyConNames (AlgTyCon n r)    = n : algTyRhsNames r-tyConNames (SynonymTyCon n)  = [n]-tyConNames (FamilyTyCon n)   = [n]-tyConNames (PrimTyCon n)     = [n]-tyConNames (TcTyCon n)       = [n]-tyConNames (Promoted n dcon) = n : dataNames dcon+tyConNames (FunTyCon n bs)     = n : concatMap tyBinderNames bs+tyConNames (AlgTyCon n ns r)   = n : ns ++ algTyRhsNames r+tyConNames (SynonymTyCon n ns) = n : ns+tyConNames (FamilyTyCon n ns)  = n : ns+tyConNames (PrimTyCon n bs)    = n : concatMap tyBinderNames bs+tyConNames (Promoted n bs dc)  = n : concatMap tyBinderNames bs ++ dataNames dc  -- | `Name`s in a `Coercion`. coercionNames :: Coercion -> [Name]@@ -140,9 +139,9 @@ -- | `Name`s in a `AlgTyRhs`. algTyRhsNames :: AlgTyRhs -> [Name] algTyRhsNames (AbstractTyCon _) = []-algTyRhsNames (DataTyCon names) = names-algTyRhsNames (TupleTyCon name) = [name]-algTyRhsNames (NewTyCon name)   = [name]+algTyRhsNames (DataTyCon ns)    = ns+algTyRhsNames (TupleTyCon n)    = [n]+algTyRhsNames (NewTyCon n)      = [n]  -- | `Name`s in a `Binding`. bindingNames :: Binding -> [Name]

@@ -196,12 +196,12 @@ liftedAltToState :: State -> LiftAct (Expr, [Constraint]) -> State liftedAltToState state (LiftAct args locals globals heap confs) = state'   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   = insertPathConsList conss pathcons }+        pathcons = state_paths state+        state'   = state { state_heap    = heap+                         , state_globals = globals+                         , state_code    = Evaluate expr locals+                         , state_names   = confs+                         , 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.

@@ -26,21 +26,21 @@     , nameOccStr     , nameUnique     , varName-    , nullAddr+    , null_addr     , addrInt -    , emptyStack+    , empty_stack     , popStack     , pushStack     , stackToList -    , emptyLocals+    , empty_locals     , lookupLocals     , insertLocals     , insertLocalsList     , localsToList -    , emptyHeap+    , empty_heap     , lookupHeap     , allocHeap     , allocHeapList@@ -48,18 +48,18 @@     , insertHeapList     , heapToList -    , emptyGlobals+    , empty_globals     , lookupGlobals     , insertGlobals     , insertGlobalsList     , globalsToList -    , emptyPathCons+    , empty_pathcons     , insertPathCons     , insertPathConsList     , pathconsToList -    , emptySymLinks+    , empty_symlinks     , insertSymLinks     , symlinksToList @@ -186,16 +186,16 @@ varName (Var name _) = name  -- | Null `MemAddr`.-nullAddr :: MemAddr-nullAddr = MemAddr 0+null_addr :: MemAddr+null_addr = MemAddr 0  -- | `MemAddr`'s `Int` value. addrInt :: MemAddr -> Int addrInt (MemAddr int) = int  -- | Empty `Stack.-emptyStack :: Stack-emptyStack = Stack []+empty_stack :: Stack+empty_stack = Stack []  -- | `Stack` pop. popStack :: Stack -> Maybe (Frame, Stack)@@ -211,8 +211,8 @@ stackToList (Stack frames) = frames  -- | Empty `Locals`.-emptyLocals :: Locals-emptyLocals = Locals M.empty+empty_locals :: Locals+empty_locals = Locals M.empty  -- | `Locals` lookup. lookupLocals :: Var -> Locals -> Maybe Value@@ -234,8 +234,8 @@ localsToList (Locals lmap) = M.toList lmap  -- | Empty `Heap`.-emptyHeap :: Heap-emptyHeap = Heap M.empty (MemAddr 0)+empty_heap :: Heap+empty_heap = Heap M.empty null_addr  -- | `Heap` lookup. lookupHeap :: MemAddr -> Heap -> Maybe HeapObj@@ -273,8 +273,8 @@ heapToList (Heap hmap _) = M.toList hmap  -- | Empty `Globals`.-emptyGlobals :: Globals-emptyGlobals = Globals M.empty+empty_globals :: Globals+empty_globals = Globals M.empty  -- | `Globals` lookup. lookupGlobals :: Var -> Globals -> Maybe Value@@ -298,8 +298,8 @@ globalsToList (Globals gmap) = M.toList gmap  -- | Empty `PathCons`.-emptyPathCons :: PathCons-emptyPathCons = PathCons []+empty_pathcons :: PathCons+empty_pathcons = PathCons []  -- | `PathCons` insertion. insertPathCons :: Constraint -> PathCons -> PathCons@@ -314,8 +314,8 @@ pathconsToList (PathCons conss) = conss  -- | Empty `SymLinks`.-emptySymLinks :: SymLinks-emptySymLinks = SymLinks M.empty+empty_symlinks :: SymLinks+empty_symlinks = SymLinks M.empty  -- | `SymLinks` insertion. insertSymLinks :: Name -> Name -> SymLinks -> SymLinks

@@ -122,8 +122,8 @@                  deriving (Show, Eq, Read)  -- | Type binder for `ForAllTy`.-data GenTyBinder bnd = NamedTyBndr bnd (GenType bnd)-                     | AnonTyBndr  (GenType bnd)+data GenTyBinder bnd = NamedTyBndr bnd+                     | AnonTyBndr                      deriving (Show, Eq, Read)  -- | `Type` literal.@@ -136,13 +136,12 @@                      deriving (Show, Eq, Read)  -- | Type constructor.-data GenTyCon bnd = FunTyCon     bnd-                  | AlgTyCon     bnd (GenAlgTyRhs bnd)-                  | SynonymTyCon bnd-                  | FamilyTyCon  bnd-                  | PrimTyCon    bnd-                  | Promoted     bnd (GenDataCon bnd)-                  | TcTyCon      bnd+data GenTyCon bnd = FunTyCon     bnd [GenTyBinder bnd]+                  | AlgTyCon     bnd [bnd] (GenAlgTyRhs bnd)+                  | SynonymTyCon bnd [bnd]+                  | FamilyTyCon  bnd [bnd]+                  | PrimTyCon    bnd [GenTyBinder bnd]+                  | Promoted     bnd [GenTyBinder bnd] (GenDataCon bnd)                   deriving (Show, Eq, Read)  -- | ADT RHS.

@@ -27,7 +27,7 @@ import Unique import Var as V -import qualified Data.Maybe  as MB+import qualified Data.Maybe as MB  -- | Make IO String from Outputable. mkIOStr :: (Outputable a) => a -> IO String@@ -79,7 +79,7 @@  -- | Make SSTG `Expr`. mkExpr :: StgExpr -> SL.Expr-mkExpr (StgLit lit) = SL.Atom (SL.LitAtom (mkLit lit))+mkExpr (StgLit lit)         = SL.Atom (SL.LitAtom (mkLit lit)) mkExpr (StgApp occ args)    = SL.FunApp (mkVar occ) (map mkAtom args) mkExpr (StgConApp dc args)  = SL.ConApp (mkData dc) (map mkAtom args) mkExpr (StgOpApp op args _) = SL.PrimApp (mkPrimOp op) (map mkAtom args)@@ -87,8 +87,8 @@ mkExpr (StgLam _ _)         = error "mkExpr: StgLam detected" mkExpr (StgLet bnd expr)    = SL.Let (mkBinding bnd) (mkExpr expr) mkExpr (StgLetNoEscape _ _ bnd expr)     = mkExpr (StgLet bnd expr)-mkExpr (StgCase mexpr _ _ bndr _ _ alts) =-    SL.Case (mkExpr mexpr) (mkVar bndr) (map mkAlt alts)+mkExpr (StgCase mexpr _ _ bndr _ _ alts) = SL.Case (mkExpr mexpr) (mkVar bndr)+                                                   (map mkAlt alts)  -- | Make SSTG `Atom`. mkAtom :: StgArg -> SL.Atom@@ -102,8 +102,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+                  Just md -> Just ((moduleNameString . moduleName) md)  -- | Make SSTG `NameSpace`. mkNameSpace :: NameSpace -> SL.NameSpace@@ -111,7 +111,7 @@                | isTvNameSpace  ns     = SL.TvNSpace                | isDataConNameSpace ns = SL.DataNSpace                | isTcClsNameSpace ns   = SL.TcClsNSpace-               | otherwise = error "mkNameSpace: unrecognized namespace"+               | otherwise             = error "mkNameSpace: unrecognized"  -- | Make SSTG Var mkVar :: Var -> SL.Var@@ -121,15 +121,14 @@  -- | Make SSTG Binding mkBinding :: StgBinding -> SL.Binding-mkBinding (StgNonRec bnd rhs) = SL.Binding SL.NonRec [(mkVar bnd, mkRhs rhs)]-mkBinding (StgRec bnd) = SL.Binding SL.Rec-                                    (map (\(b, r) -> (mkVar b, mkRhs r)) bnd)+mkBinding (StgNonRec bnd r) = SL.Binding SL.NonRec [(mkVar bnd, mkRhs r)]+mkBinding (StgRec bnd)      = SL.Binding SL.Rec (map (\(b, r) ->+                                                      (mkVar b, mkRhs r)) bnd)  -- | Make SSTG `BindRhs`. mkRhs :: StgRhs -> SL.BindRhs-mkRhs (StgRhsCon _ dc args) = SL.ConForm (mkData dc) (map mkAtom args)-mkRhs (StgRhsClosure _ _ _ _ _ params expr) =-    SL.FunForm (map mkVar params) (mkExpr expr)+mkRhs (StgRhsCon _ dc args)          = SL.ConForm (mkData dc) (map mkAtom args)+mkRhs (StgRhsClosure _ _ _ _ _ ps e) = SL.FunForm (map mkVar ps) (mkExpr e)  -- | Make SSTG `Lit`. mkLit :: Literal -> SL.Lit@@ -143,7 +142,7 @@   (MachFloat rat)   -> SL.MachFloat rat ((mkType . literalType) lit)   (MachDouble rat)  -> SL.MachDouble rat ((mkType . literalType) lit)   (LitInteger i _)  -> SL.MachInt (fromInteger i) ((mkType . literalType) lit)-  MachNullAddr      -> SL.MachNullAddr ((mkType . literalType) lit)+  (MachNullAddr)    -> SL.MachNullAddr ((mkType . literalType) lit)   (MachLabel f m _) -> SL.MachLabel (unpackFS f) m ((mkType . literalType) lit)  -- | `DataCon`'s `Name`.@@ -179,27 +178,29 @@  -- | Make SSTG `Type`. mkType :: Type -> SL.Type-mkType (TyVarTy v) = SL.TyVarTy (mkName (V.varName v)) (mkType (varType v)) 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 (mkTyBndr b) (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)+mkType (TyVarTy v)      = SL.TyVarTy (mkName (V.varName v))+                                     (mkType (varType v))  -- | Make SSTG `TyCon`. mkTyCon :: TyCon -> SL.TyCon-mkTyCon tc | isFunTyCon         tc = SL.FunTyCon     name-           | isAlgTyCon         tc = SL.AlgTyCon     name algrhs-           | isFamilyTyCon      tc = SL.FamilyTyCon  name-           | isPrimTyCon        tc = SL.PrimTyCon    name-           | isTcTyCon          tc = SL.TcTyCon      name-           | isTypeSynonymTyCon tc = SL.SynonymTyCon name-           | isPromotedDataCon  tc = SL.Promoted     name dcon-           | otherwise = error "mkTyCon: unrecognized TyCon"-  where name   = (mkName . tyConName) tc-        algrhs = (mkAlgTyConRhs . algTyConRhs) tc-        dcon   = (mkData . MB.fromJust . isPromotedDataCon_maybe) tc+mkTyCon tc | isFunTyCon         tc = SL.FunTyCon     name tcbndrs+           | isAlgTyCon         tc = SL.AlgTyCon     name tvnames algrhs+           | isFamilyTyCon      tc = SL.FamilyTyCon  name tvnames+           | isPrimTyCon        tc = SL.PrimTyCon    name tcbndrs+           | isTypeSynonymTyCon tc = SL.SynonymTyCon name tvnames+           | isPromotedDataCon  tc = SL.Promoted     name tcbndrs dcon+           | otherwise             = error "mkTyCon: unrecognized TyCon"+  where name    = (mkName . tyConName) tc+        algrhs  = (mkAlgTyConRhs . algTyConRhs) tc+        tcbndrs = map mkTyBndr (tyConBinders tc)+        tvnames = map (mkName. V.varName) (tyConTyVars tc)+        dcon    = (mkData . MB.fromJust . isPromotedDataCon_maybe) tc  -- | Make SSTG `AlgTyRhs`. mkAlgTyConRhs :: AlgTyConRhs -> SL.AlgTyRhs@@ -210,9 +211,8 @@  -- | make SSTG `TyBinder`. mkTyBndr :: TyBinder -> SL.TyBinder-mkTyBndr (Anon ty)   = SL.AnonTyBndr  (mkType ty)+mkTyBndr (Anon _)    = SL.AnonTyBndr mkTyBndr (Named v _) = SL.NamedTyBndr (mkName (V.varName v))-                                      (mkType (varType v))  -- | Make SSTG `Type` literals. mkTyLit :: TyLit -> SL.TyLit