diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -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 diff --git a/SSTG.cabal b/SSTG.cabal --- a/SSTG.cabal +++ b/SSTG.cabal @@ -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 diff --git a/app/Main.hs b/app/Main.hs --- a/app/Main.hs +++ b/app/Main.hs @@ -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 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 @@ -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 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 @@ -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] 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 @@ -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. 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 @@ -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 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 @@ -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. 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 @@ -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