SSTG 0.1.1.0 → 0.1.1.1

raw patch · 16 files changed

+330/−338 lines, 16 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• SSTG.cabal +4/−4
• app/Main.hs +4/−4
• src/SSTG/Core.hs +2/−2
• src/SSTG/Core/Execution/Engine.hs +10/−9
• src/SSTG/Core/Execution/Naming.hs +18/−25
• src/SSTG/Core/Execution/Rules.hs +15/−15
• src/SSTG/Core/Execution/Stepping.hs +26/−10
• src/SSTG/Core/Execution/Support.hs +35/−44
• src/SSTG/Core/Language.hs +9/−0
• src/SSTG/Core/Language/Syntax.hs +153/−0
• src/SSTG/Core/Language/Typing.hs +53/−0
• src/SSTG/Core/Syntax.hs +0/−9
• src/SSTG/Core/Syntax/Language.hs +0/−153
• src/SSTG/Core/Syntax/Typing.hs +0/−53
• src/SSTG/Core/Translation/Haskell.hs +1/−1
• src/SSTG/Utils/Printing.hs +0/−9

@@ -1,5 +1,5 @@ name:                SSTG-version:             0.1.1.0+version:             0.1.1.1 synopsis:            STG Symbolic Execution description:         Prototype of STG-based Symbolic Execution for Haskell. homepage:            https://github.com/AntonXue/SSTG#readme@@ -19,9 +19,9 @@                      , SSTG.Core                      , SSTG.Core.Translation                      , SSTG.Core.Translation.Haskell-                     , SSTG.Core.Syntax-                     , SSTG.Core.Syntax.Language-                     , SSTG.Core.Syntax.Typing+                     , SSTG.Core.Language+                     , SSTG.Core.Language.Syntax+                     , SSTG.Core.Language.Typing                      , SSTG.Core.Execution                      , SSTG.Core.Execution.Engine                      , SSTG.Core.Execution.Naming

@@ -45,9 +45,9 @@                     ok -> Just ok  parseFlags :: [String] -> RunFlags-parseFlags args = RunFlags { step_count = parseStepCount args-                           , step_type  = parseStepType  args-                           , dump_dir   = parseDumpDir   args }+parseFlags args = RunFlags { flag_step_count = parseStepCount args+                           , flag_step_type  = parseStepType  args+                           , flag_dump_dir   = parseDumpDir   args }  injDumpLocs :: String -> Int -> FilePath -> [FilePath] injDumpLocs entry n dir = map (\i -> start ++ (show i) ++ ".txt") [1..n]@@ -77,7 +77,7 @@     putStrLn $ show flags     -- Execution!     let ldss  = execute flags state-    case dump_dir flags of+    case flag_dump_dir flags of         -- Dump to terminal.         Nothing  -> mapM_ (putStrLn . pprLivesDeadsStr) ldss         -- Dump to file.

@@ -1,11 +1,11 @@ -- | Import Module for SSTG.Core module SSTG.Core     ( module SSTG.Core.Execution-    , module SSTG.Core.Syntax+    , module SSTG.Core.Language     , module SSTG.Core.Translation     ) where  import SSTG.Core.Execution-import SSTG.Core.Syntax+import SSTG.Core.Language import SSTG.Core.Translation 

@@ -9,7 +9,7 @@     , execute1     ) where -import SSTG.Core.Syntax+import SSTG.Core.Language import SSTG.Core.Execution.Naming import SSTG.Core.Execution.Stepping import SSTG.Core.Execution.Support@@ -34,7 +34,9 @@         then LoadOkay  state         else LoadGuess state (map fst others)   where -- Status or something.-        status   = Status { steps = 0 }+        status   = Status { status_id = 1+                          , status_parent_id = 0+                          , status_steps = 0 }         -- Stack initialized to empty.         stack    = empty_stack         -- Globals and Heap are loaded together. They are still beta forms now.@@ -55,8 +57,7 @@                          , state_globals = globals                          , state_code    = code                          , state_names   = []-                         , state_paths   = empty_pathcons-                         , state_links   = empty_symlinks }+                         , state_paths   = empty_pathcons }          -- Gather information on all variables.         state    = state0 { state_names = allNames state0 }@@ -163,9 +164,9 @@   | otherwise = base  -- | Run flags.-data RunFlags = RunFlags { step_count :: Int-                         , step_type  :: StepType-                         , dump_dir   :: Maybe FilePath+data RunFlags = RunFlags { flag_step_count :: Int+                         , flag_step_type  :: StepType+                         , flag_dump_dir   :: Maybe FilePath                          } deriving (Show, Eq, Read)  -- | Step execution type.@@ -173,9 +174,9 @@  -- | Perform execution on a `State` given the run flags. execute :: RunFlags -> State -> [([LiveState], [DeadState])]-execute flags state = step (step_count flags) state+execute flags state = step (flag_step_count flags) state   where step :: Int -> State -> [([LiveState], [DeadState])]-        step = case step_type flags of+        step = case flag_step_type flags of                    BFS       -> \k s -> [runBoundedBFS k s]                    BFSLogged -> runBoundedBFSLogged                    DFS       -> \k s -> [runBoundedDFS k s]

@@ -8,7 +8,7 @@     , freshSeededNameList     ) where -import SSTG.Core.Syntax+import SSTG.Core.Language import SSTG.Core.Execution.Support  import qualified Data.List as L@@ -22,9 +22,7 @@         glbls_ns = globalsNames (state_globals state)         expr_ns  = codeNames    (state_code    state)         pcons_ns = pconsNames   (state_paths   state)-        links_ns = linksNames   (state_links   state)-        acc_ns   = stack_ns ++ heap_ns  ++ glbls_ns ++-                   expr_ns  ++ pcons_ns ++ links_ns+        acc_ns   = stack_ns ++ heap_ns ++ glbls_ns ++ expr_ns  ++ pcons_ns  -- | `Name`s in a `Stack`. stackNames :: Stack -> [Name]@@ -32,10 +30,10 @@  -- | `Name`s in a `Frame`. frameNames :: Frame -> [Name]-frameNames (UpdateFrame _)          = []-frameNames (ApplyFrame as lcs)      = concatMap atomNames as ++ localsNames lcs-frameNames (CaseFrame var alts lcs) = varNames var ++ (concatMap altNames alts)-                                                   ++ localsNames lcs+frameNames (UpdateFrame _)         = []+frameNames (ApplyFrame as ls)      = localsNames ls ++ concatMap atomNames as+frameNames (CaseFrame var alts ls) = localsNames ls ++ concatMap altNames alts+                                                    ++ varNames var  -- | `Name`s in an `Alt`. altNames :: Alt -> [Name]@@ -68,8 +66,8 @@  -- | `Name`s in a `BindRhs`. bindRhsNames :: BindRhs -> [Name]-bindRhsNames (FunForm prms expr) = (concatMap varNames prms) ++ exprNames expr-bindRhsNames (ConForm dcon args) = dataNames dcon ++ concatMap atomNames args+bindRhsNames (FunForm prms expr) = concatMap varNames prms  ++ exprNames expr+bindRhsNames (ConForm dcon args) = concatMap atomNames args ++ dataNames dcon  -- | `Name`s in a `Var`. varNames :: Var -> [Name]@@ -77,8 +75,8 @@  -- | `Name`s in an `Atom`. atomNames :: Atom -> [Name]-atomNames (VarAtom var) = varNames var atomNames (LitAtom _)   = []+atomNames (VarAtom var) = varNames var  -- | `Name`s in `Globals`. globalsNames :: Globals -> [Name]@@ -95,19 +93,19 @@ exprNames (FunApp fun args)    = varNames  fun  ++ concatMap atomNames args exprNames (PrimApp prim args)  = pfunNames prim ++ concatMap atomNames args exprNames (ConApp dcon args)   = dataNames dcon ++ concatMap atomNames args-exprNames (Let binds expr)     = bindingNames binds ++ exprNames expr-exprNames (Case expr var alts) = varNames var ++ exprNames expr-                                              ++ concatMap altNames alts+exprNames (Let bnd expr)       = exprNames expr ++ bindingNames bnd+exprNames (Case expr var alts) = exprNames expr ++ varNames var+                                                ++ concatMap altNames alts -- | `Name`s in a `Type`. typeNames :: Type -> [Name] typeNames (TyVarTy n ty)    = n : typeNames ty+typeNames (CoercionTy coer) = coercionNames coer typeNames (AppTy t1 t2)     = typeNames t1  ++ typeNames t2-typeNames (ForAllTy bnd ty) = tyBinderNames bnd ++ typeNames ty typeNames (CastTy ty coer)  = typeNames ty  ++ coercionNames coer typeNames (TyConApp tc ty)  = tyConNames tc ++ concatMap typeNames ty-typeNames (CoercionTy coer) = coercionNames coer+typeNames (ForAllTy bnd ty) = typeNames ty  ++ tyBinderNames bnd+typeNames (FunTy t1 t2)     = typeNames t1  ++ typeNames t2 typeNames (LitTy _)         = []-typeNames (FunTy t1 t2)     = typeNames t1 ++ typeNames t2 typeNames (Bottom)          = []  -- | `Name`s in a `PrimFun`.@@ -155,12 +153,8 @@  -- | `Name`s in a `PathCons`. constraintNames :: Constraint -> [Name]-constraintNames (Constraint (_, vars) expr locals _) = exprNames expr     ++-                                                       localsNames locals ++-                                                       map varName vars--- | `Name`s in a `SymLinks`.-linksNames :: SymLinks -> [Name]-linksNames symlinks = concatMap (\(a, b) -> [a, b]) (symlinksToList symlinks)+constraintNames (Constraint (_, vs) e locs _) = exprNames e ++ localsNames locs+                                                            ++ map varName vs  -- | Create a fresh seed given any `Int`, a `String` seed, and a `Set` of -- `String`s that we do not want our new `String` to conflict with. The sole@@ -168,8 +162,7 @@ -- prime number to "orbit" an index around a fixed list of acceptable `Char`s. freshString :: Int -> String -> S.Set String -> String freshString rand seed confs = if S.member seed confs-    then freshString (rand + 1) (seed ++ [pick]) confs-    else seed+    then freshString (rand + 1) (seed ++ [pick]) confs else seed   where pick  = bank !! index         index = raw_i `mod` (length bank)         raw_i = (abs rand) * prime

@@ -5,7 +5,7 @@     , isStateValueForm     ) where -import SSTG.Core.Syntax+import SSTG.Core.Language import SSTG.Core.Execution.Naming import SSTG.Core.Execution.Support @@ -88,7 +88,7 @@   where sname    = freshSeededName (varName var) confs         svar     = Var sname (varType var)         (heap', addr) = allocHeap (SymObj (Symbol svar Nothing)) heap-        globals' = insertGlobals var (MemVal addr) globals+        globals' = insertGlobals (var, MemVal addr) globals         confs'   = sname : confs         pass_out = LiftAct addr locals globals' heap' confs' @@ -185,8 +185,8 @@         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-        locals'  = insertLocalsList llist locals+        kvs      = (cvar, MemVal addr) : zip params mem_vals+        locals'  = insertLocalsList kvs locals         mxpr     = Atom (VarAtom mvar)         conss    = [Constraint (ac, params) mxpr locals' True]         confs'   = snames ++ confs@@ -341,7 +341,7 @@   -- Rule Case Lit   | Evaluate (Case (Atom (LitAtom lit)) cvar alts) locals <- code   , (Alt _ _ expr):_ <- matchLitAlts lit alts =-    let locals' = insertLocals cvar (LitVal lit) locals+    let locals' = insertLocals (cvar, LitVal lit) locals     in Just (RuleCaseLit             ,[state { state_code = Evaluate expr locals' }]) @@ -351,8 +351,8 @@   , ConObj dcon vals      <- hobj   , (Alt _ params expr):_ <- matchDataAlts dcon alts   , length params == length vals =-    let llist   = (cvar, MemVal addr) : zip params vals-        locals' = insertLocalsList llist locals+    let kvs     = (cvar, MemVal addr) : zip params vals+        locals' = insertLocalsList kvs locals     in Just (RuleCaseConPtr             ,[state { state_code = Evaluate expr locals' }]) @@ -360,7 +360,7 @@   | Evaluate (Case (Atom (LitAtom lit)) cvar alts) locals <- code   , []               <- matchLitAlts lit alts   , (Alt _ _ expr):_ <- defaultAlts alts =-    let locals' = insertLocals cvar (LitVal lit) locals+    let locals' = insertLocals (cvar, LitVal lit) locals     in Just (RuleCaseAnyLit             ,[state { state_code = Evaluate expr locals' }]) @@ -370,7 +370,7 @@   , ConObj dcon _     <- hobj   , []                <- matchDataAlts dcon alts   , (Alt _ _ expr):_  <- defaultAlts alts =-    let locals' = insertLocals cvar (MemVal addr) locals+    let locals' = insertLocals (cvar, MemVal addr) locals     in Just (RuleCaseAnyConPtr             ,[state { state_code = Evaluate expr locals' }]) @@ -405,7 +405,7 @@     let frame = UpdateFrame addr     in Just (RuleUpdateCThunk             ,[state { state_stack = pushStack frame stack-                    , state_heap  = insertHeap addr Blackhole heap+                    , state_heap  = insertHeap (addr, Blackhole) heap                     , state_code  = Evaluate expr fun_locs }])    -- Rule Update Frame Delete Lit@@ -413,7 +413,7 @@   , Return (LitVal lit)                 <- code =        Just (RuleUpdateDLit             ,[state { state_stack = stack'-                    , state_heap  = insertHeap frm_addr (LitObj lit) heap+                    , state_heap  = insertHeap (frm_addr, LitObj lit) heap                     , state_code  = Return (LitVal lit) }])    -- Rule Update Frame Delete Val Pointer@@ -423,7 +423,7 @@   , isHeapValueForm hobj =        Just (RuleUpdateDValPtr             ,[state { state_stack = stack'-                    , state_heap  = insertHeap frm_addr (AddrObj addr) heap+                    , state_heap  = insertHeap (frm_addr, AddrObj addr) heap                     , state_code  = Return (MemVal addr) }])    -- Rule Case Frame Create Case Non LitVal or MemVal@@ -450,7 +450,7 @@     let vname     = freshSeededName (varName cvar) confs         vvar      = Var vname (varType cvar)         mxpr      = Atom (VarAtom vvar)-        frm_locs' = insertLocals vvar (MemVal addr) frm_locs+        frm_locs' = insertLocals (vvar, MemVal addr) frm_locs     in Just (RuleCaseDValPtr             ,[state { state_stack = stack'                     , state_code  = Evaluate (Case mxpr cvar alts) frm_locs'@@ -489,7 +489,7 @@   , Just ftype   <- memAddrType addr heap =     let fname     = freshName VarNSpace confs         fvar      = Var fname ftype-        frm_locs' = insertLocals fvar (MemVal addr) frm_locs+        frm_locs' = insertLocals (fvar, MemVal addr) frm_locs     in Just (RuleApplyDReturnFun             ,[state { state_stack = stack'                     , state_code  = Evaluate (FunApp fvar args) frm_locs'@@ -502,7 +502,7 @@   , SymObj (Symbol sym _) <- hobj =     let sname     = freshSeededName (varName sym) confs         svar      = Var sname (varType sym)-        frm_locs' = insertLocals svar (MemVal addr) frm_locs+        frm_locs' = insertLocals (svar, MemVal addr) frm_locs     in Just (RuleApplyDReturnSym             ,[state { state_stack = stack'                     , state_code  = Evaluate (FunApp svar args) frm_locs'

@@ -11,6 +11,17 @@ import SSTG.Core.Execution.Rules import SSTG.Core.Execution.Support +import qualified Data.Char as C+import qualified Data.List as L++-- | Custom hash function.+hash :: [Rule] -> Int+hash rules = L.foldl' (\acc c -> (acc + p2 * C.ord c)`mod` p3) p1 str+  where str = concatMap show rules+        p1  = 5381+        p2  = 1009+        p3  = 433494437+ -- | A `State` that is not in value form yet, capable of being evaluated. A -- list of `Rule`s is kept to denote reduction history. type LiveState = ([Rule], State)@@ -19,20 +30,25 @@ -- reduction history. type DeadState = ([Rule], State) --- | Increment the `steps` counter of a `Status`.-incStatus :: Status -> Status-incStatus status = status { steps = (steps status) + 1 }---- | Increment the `steps` counter inside the `state_status`.-incState :: State -> State-incState state = state { state_status = incStatus (state_status state) }+-- | Increment Status conditions, and shift the current / parent id as needed.+incStatus :: Maybe Int -> State -> State+incStatus mb_id state = state { state_status = status' }+  where status  = state_status state+        status' = case mb_id of+                      Nothing  -> incStatusSteps status+                      Just id' -> incStatusSteps (updateStatusId id' status)  -- | Given a list of `State` along with its list of past `Rule` reductions, -- apply STG reduction. If reduction yields `Nothing`, simply return itself. step :: ([Rule], State) -> [([Rule], State)]-step (hist, state) = case reduce state of-    Nothing             -> [(hist, state)]-    Just (rule, states) -> map (\s -> (hist ++ [rule], incState s)) states+step (hist, start) = case reduce start of+    Nothing              -> [(hist, start)]+    Just (rule, results) ->+        let trace = hist ++ [rule]+            mb_id = if length results > 1+                        then Just (hash trace)+                        else Nothing+        in map (\s -> (trace, incStatus mb_id s)) results  -- | This is what we use the `<*>` over. pass :: [LiveState] -> ([LiveState], [DeadState] -> [DeadState])

@@ -21,7 +21,6 @@     , Code(..)     , PathCons     , Constraint(..)-    , SymLinks      , nameOccStr     , nameUnique@@ -29,6 +28,10 @@     , null_addr     , addrInt +    , init_status+    , incStatusSteps+    , updateStatusId+     , empty_stack     , popStack     , pushStack@@ -59,16 +62,12 @@     , insertPathConsList     , pathconsToList -    , empty_symlinks-    , insertSymLinks-    , symlinksToList-     , lookupValue     , vlookupHeap     , memAddrType     ) where -import SSTG.Core.Syntax+import SSTG.Core.Language  import qualified Data.Map as M @@ -102,7 +101,6 @@                    , state_code    :: Code                    , state_names   :: [Name]                    , state_paths   :: PathCons-                   , state_links   :: SymLinks                    } deriving (Show, Eq, Read)  -- | Symbolic variables. The @Maybe (Expr, Locals)@ can be used to trace the@@ -111,7 +109,9 @@ data Symbol = Symbol Var (Maybe (Expr, Locals)) deriving (Show, Eq, Read)  -- | State status.-data Status = Status { steps :: Int+data Status = Status { status_id        :: Int+                     , status_parent_id :: Int+                     , status_steps     :: Int                      } deriving (Show, Eq, Read)  -- | Execution stack used in graph reduction semnatics.@@ -168,9 +168,6 @@ data Constraint = Constraint (AltCon, [Var]) Expr Locals Bool                 deriving (Show, Eq, Read) --- | Symbolic link tables helps keep track of what names went to what, what?-newtype SymLinks = SymLinks (M.Map Name Name) deriving (Show, Eq, Read)- --   Simple functions that require only the immediate data structure.  -- | A `Name`'s occurrence string.@@ -193,14 +190,29 @@ addrInt :: MemAddr -> Int addrInt (MemAddr int) = int +-- | Initial `Status`.+init_status :: Status+init_status = Status { status_id        = 1+                     , status_parent_id = 0+                     , status_steps     = 0 }++-- | Increment `Status` steps.+incStatusSteps :: Status -> Status+incStatusSteps status = status { status_steps = (status_steps status) + 1 }++-- | Update the `Status` id.+updateStatusId :: Int -> Status -> Status+updateStatusId new_id status = status { status_id        = new_id+                                      , status_parent_id = status_id status }+ -- | Empty `Stack. empty_stack :: Stack empty_stack = Stack []  -- | `Stack` pop. popStack :: Stack -> Maybe (Frame, Stack)-popStack (Stack [])     = Nothing-popStack (Stack (f:fs)) = Just (f, Stack fs)+popStack (Stack [])             = Nothing+popStack (Stack (frame:frames)) = Just (frame, Stack frames)  -- | `Stack` push. pushStack :: Frame -> Stack -> Stack@@ -219,15 +231,12 @@ lookupLocals var (Locals lmap) = M.lookup (varName var) lmap  -- | `Locals` insertion.-insertLocals :: Var -> Value -> Locals -> Locals-insertLocals var val (Locals lmap) = Locals lmap'-  where lmap' = M.insert (varName var) val lmap+insertLocals :: (Var, Value) -> Locals -> Locals+insertLocals (k, v) (Locals lmap) = Locals (M.insert (varName k) v lmap)  -- | List insertion into `Locals`. insertLocalsList :: [(Var, Value)] -> Locals -> Locals-insertLocalsList []               locals = locals-insertLocalsList ((var, val):vvs) locals = insertLocalsList vvs locals'-  where locals' = insertLocals var val locals+insertLocalsList kvs locals = foldr insertLocals locals kvs  -- | `Locals` to key value pairs. localsToList :: Locals -> [(Name, Value)]@@ -258,15 +267,12 @@         (heapf, as)   = allocHeapList hobjs heap'  -- | `Heap` direct insertion at a specific `MemAddr`.-insertHeap :: MemAddr -> HeapObj -> Heap -> Heap-insertHeap addr hobj (Heap hmap prev) = Heap hmap' prev-  where hmap' = M.insert addr hobj hmap+insertHeap :: (MemAddr, HeapObj) -> Heap -> Heap+insertHeap (k, v) (Heap hmap prev) = Heap (M.insert k v hmap) prev  -- | Insert a list of `HeapObj` at specified `MemAddr` locations. insertHeapList :: [(MemAddr, HeapObj)] -> Heap -> Heap-insertHeapList []                 heap = heap-insertHeapList ((addr, hobj):ahs) heap = insertHeapList ahs heap'-  where heap' = insertHeap addr hobj heap+insertHeapList kvs heap = foldr insertHeap heap kvs  -- | `Heap` to key value pairs. heapToList :: Heap -> [(MemAddr, HeapObj)]@@ -281,17 +287,14 @@ lookupGlobals var (Globals gmap) = M.lookup (varName var) gmap  -- | `Globals` insertion.-insertGlobals :: Var -> Value -> Globals -> Globals-insertGlobals var val (Globals gmap) = Globals gmap'-  where gmap' = M.insert (varName var) val gmap+insertGlobals :: (Var, Value) -> Globals -> Globals+insertGlobals (k, v) (Globals gmap) = Globals (M.insert (varName k) v gmap)  -- | Insert a list of `Var` and `Value` pairs into `Globals`. This would -- typically occur for new symbolic variables created from uninterpreted / -- out-of-scope variables during runtime. insertGlobalsList :: [(Var, Value)] -> Globals -> Globals-insertGlobalsList []               globals = globals-insertGlobalsList ((var, val):vvs) globals = insertGlobalsList vvs globals'-  where globals' = insertGlobals var val globals+insertGlobalsList kvs globals = foldr insertGlobals globals kvs  -- | `Globals` to key value pairs. globalsToList :: Globals -> [(Name, Value)]@@ -303,7 +306,7 @@  -- | `PathCons` insertion. insertPathCons :: Constraint -> PathCons -> PathCons-insertPathCons cons (PathCons pcs) = PathCons (cons : pcs)+insertPathCons cons (PathCons conss) = PathCons (cons : conss)  -- | Insert a list of `Constraint`s into a `PathCons`. insertPathConsList :: [Constraint] -> PathCons -> PathCons@@ -312,18 +315,6 @@ -- | `PathCons` to list of `Constraint`s. pathconsToList :: PathCons -> [Constraint] pathconsToList (PathCons conss) = conss---- | Empty `SymLinks`.-empty_symlinks :: SymLinks-empty_symlinks = SymLinks M.empty---- | `SymLinks` insertion.-insertSymLinks :: Name -> Name -> SymLinks -> SymLinks-insertSymLinks old new (SymLinks smap) = SymLinks (M.insert old new smap)---- | `SymLinks` to list of key value pairs.-symlinksToList :: SymLinks -> [(Name, Name)]-symlinksToList (SymLinks smap) = M.toList smap  --   Complex functions that involve multiple data structures. 

@@ -0,0 +1,9 @@+-- | Export Module for SSTG.Syntax+module SSTG.Core.Language+    ( module SSTG.Core.Language.Syntax+    , module SSTG.Core.Language.Typing+    ) where++import SSTG.Core.Language.Syntax+import SSTG.Core.Language.Typing+

@@ -0,0 +1,153 @@+-- | SSTG Syntax Definitions+module SSTG.Core.Language.Syntax+    ( module SSTG.Core.Language.Syntax+    ) where++type Program  = GenProgram  Name Var++type Lit      = GenLit      Name Var+type Atom     = GenAtom     Name Var+type PrimFun  = GenPrimFun  Name Var+type Expr     = GenExpr     Name Var+type Alt      = GenAlt      Name Var+type AltCon   = GenAltCon   Name Var+type Binding  = GenBinding  Name Var+type BindRhs  = GenBindRhs  Name Var++type DataCon  = GenDataCon  Name+type Type     = GenType     Name+type TyBinder = GenTyBinder Name+type Coercion = GenCoercion Name+type TyCon    = GenTyCon    Name+type AlgTyRhs = GenAlgTyRhs Name++-- | A `Program` is defined as a list of bindings. The @bnd@ is an identifier+-- that determines a unique binder to the @var@. In practice, these are defined+-- to be `Name` and `Var` respectively.+newtype GenProgram bnd var = Program [GenBinding bnd var]+                           deriving (Show, Eq, Read)++-- | Variables, data constructors, type variables, and type constructors.+data NameSpace = VarNSpace | DataNSpace | TvNSpace | TcClsNSpace+               deriving (Show, Eq, Read, Ord)++-- | The occurrence name is defined as a string, with a `Maybe` module name+-- appearing. The `Int` denotes a `Unique` translated from GHC. For instance,+-- in the case of @Map.empty@, the occurrence name is @"empty"@, while the+-- module name is some variant of @Just \"Data.Map\"@.+data Name = Name String (Maybe String) NameSpace Int+          deriving (Show, Eq, Read, Ord)++-- | Variables consist of a `Name` and a `Type`.+data Var = Var Name (GenType Name) deriving (Show, Eq, Read)++-- | Literals are largely augmented from the original GHC implementation, with+-- additional annotations to denote `BlankAddr` for lifting, `AddrLit` for+-- value deriviation, `SymLit` for symbolic literals, and `SymLitEval` to+-- represent symbolic literal evaluation, as literal manipulation functions+-- are defined in the Haskell Prelude, and thus outside of scope for us.+data GenLit bnd var = MachChar     Char (GenType bnd)+                    | MachStr      String (GenType bnd)+                    | MachInt      Int (GenType bnd)+                    | MachWord     Int (GenType bnd)+                    | MachFloat    Rational (GenType bnd)+                    | MachDouble   Rational (GenType bnd)+                    | MachNullAddr (GenType bnd)+                    | MachLabel    String (Maybe Int) (GenType bnd)+                    | BlankAddr+                    | AddrLit      Int+                    | SymLit       var+                    | SymLitEval   (GenPrimFun bnd var) [GenLit bnd var]+                    deriving (Show, Eq, Read)++-- | Atomic objects. `VarAtom` may be used for variable lookups, while+-- `LitAtom` is used to denote literals.+data GenAtom bnd var = LitAtom (GenLit bnd var)+                     | VarAtom var+                     deriving (Show, Eq, Read)++-- | Primitive functions.+data GenPrimFun bnd var = PrimFun bnd (GenType bnd) deriving (Show, Eq, Read)++-- | Expressions closely correspond to their representation in GHC.+data GenExpr bnd var = Atom    (GenAtom bnd var)+                     | PrimApp (GenPrimFun bnd var) [GenAtom bnd var]+                     | ConApp  (GenDataCon bnd) [GenAtom bnd var]+                     | FunApp  var [GenAtom bnd var]+                     | Let     (GenBinding bnd var) (GenExpr bnd var)+                     | Case    (GenExpr bnd var) var [GenAlt bnd var]+                     deriving (Show, Eq, Read)++-- | Alternatives utilize an `AltCon`, a list of parameters of that match to+-- the appropriate `DataAlt` as applicable, and an expression for the result.+data GenAlt bnd var = Alt (GenAltCon bnd var) [var] (GenExpr bnd var)+                    deriving (Show, Eq, Read)++-- | Alt Constructor+data GenAltCon bnd var = DataAlt (GenDataCon bnd)+                       | LitAlt  (GenLit bnd var)+                       | Default+                       deriving (Show, Eq, Read)++-- | Binding+data GenBinding bnd var = Binding RecForm [(var, GenBindRhs bnd var)]+                        deriving (Show, Eq, Read)++-- | Recursive?+data RecForm = Rec | NonRec deriving (Show, Eq, Read)++-- | `BindRhs` taken straight from STG can be either in constructor form, or+-- function form. Empty parameter list denotes a thunk.+data GenBindRhs bnd var = ConForm (GenDataCon bnd) [GenAtom bnd var]+                        | FunForm [var] (GenExpr bnd var)+                        deriving (Show, Eq, Read)++-- | Data Constructor consists of its tag, the type that corresponds to its+-- ADT, and a list of paramters it takes.+data GenDataCon bnd = DataCon bnd (GenType bnd) [GenType bnd]+                    deriving (Show, Eq, Read)++-- | Types are information that are useful to keep during symbolic execution+-- in order to generate correct feeds into the SMT solver. Overapproxmation is+-- currently performed, and is likely to be cut back in the future.+data GenType bnd = TyVarTy    bnd (GenType bnd)+                 | AppTy      (GenType bnd) (GenType bnd)+                 | ForAllTy   (GenTyBinder bnd) (GenType bnd)+                 | CastTy     (GenType bnd) (GenCoercion bnd)+                 | TyConApp   (GenTyCon bnd) [GenType bnd]+                 | CoercionTy (GenCoercion bnd)+                 | LitTy      TyLit+                 | FunTy      (GenType bnd) (GenType bnd)+                 | Bottom+                 deriving (Show, Eq, Read)++-- | Type binder for `ForAllTy`.+data GenTyBinder bnd = NamedTyBndr bnd+                     | AnonTyBndr+                     deriving (Show, Eq, Read)++-- | `Type` literal.+data TyLit = NumTyLit Int+           | StrTyLit String+           deriving (Show, Eq, Read)++-- | Coercion. I have no idea what this does :)+data GenCoercion bnd = Coercion (GenType bnd) (GenType bnd)+                     deriving (Show, Eq, Read)++-- | Type constructor.+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.+data GenAlgTyRhs bnd = AbstractTyCon Bool+                     | DataTyCon     [bnd]+                     | NewTyCon      bnd+                     | TupleTyCon    bnd+                     deriving (Show, Eq, Read)+

@@ -0,0 +1,53 @@+-- | Typing Module+module SSTG.Core.Language.Typing+    ( module SSTG.Core.Language.Typing+    ) where++import SSTG.Core.Language.Syntax++-- | Variable type.+varType :: Var -> Type+varType (Var _ ty) = ty++-- | Literal type.+litType :: Lit -> Type+litType (MachChar _ ty)      = ty+litType (MachStr _ ty)       = ty+litType (MachInt _ ty)       = ty+litType (MachWord _ ty)      = ty+litType (MachFloat _ ty)     = ty+litType (MachDouble _ ty)    = ty+litType (MachNullAddr ty)    = ty+litType (MachLabel _ _ ty)   = ty+litType (BlankAddr)          = Bottom+litType (AddrLit _)          = Bottom+litType (SymLit var)         = varType var+litType (SymLitEval pf args) = foldl AppTy (primFunType pf) (map litType args)++-- | Atom type.+atomType :: Atom -> Type+atomType (VarAtom var) = varType var+atomType (LitAtom lit) = litType lit++-- | Primitive function type.+primFunType :: PrimFun -> Type+primFunType (PrimFun _ ty) = ty++-- | Data constructor type denoted as a function.+dataConType :: DataCon -> Type+dataConType (DataCon _ ty tys) = foldr FunTy ty tys++-- | Alt type+altType :: Alt -> Type+altType (Alt _ _ expr) = exprType expr++-- | I wonder what this could possibly be?+exprType :: Expr -> Type+exprType (Atom atom)       = atomType atom+exprType (PrimApp pf args) = foldl AppTy (primFunType pf) (map atomType args)+exprType (ConApp dc args)  = foldl AppTy (dataConType dc) (map atomType args)+exprType (FunApp fun args) = foldl AppTy (varType fun)    (map atomType args)+exprType (Let _ expr)      = exprType expr+exprType (Case _ _ (a:_))  = altType a+exprType _                 = Bottom+

@@ -1,9 +0,0 @@--- | Export Module for SSTG.Syntax-module SSTG.Core.Syntax-    ( module SSTG.Core.Syntax.Language-    , module SSTG.Core.Syntax.Typing-    ) where--import SSTG.Core.Syntax.Language-import SSTG.Core.Syntax.Typing-

@@ -1,153 +0,0 @@--- | SSTG Syntax Definitions-module SSTG.Core.Syntax.Language-    ( module SSTG.Core.Syntax.Language-    ) where--type Program  = GenProgram  Name Var--type Lit      = GenLit      Name Var-type Atom     = GenAtom     Name Var-type PrimFun  = GenPrimFun  Name Var-type Expr     = GenExpr     Name Var-type Alt      = GenAlt      Name Var-type AltCon   = GenAltCon   Name Var-type Binding  = GenBinding  Name Var-type BindRhs  = GenBindRhs  Name Var--type DataCon  = GenDataCon  Name-type Type     = GenType     Name-type TyBinder = GenTyBinder Name-type Coercion = GenCoercion Name-type TyCon    = GenTyCon    Name-type AlgTyRhs = GenAlgTyRhs Name---- | A `Program` is defined as a list of bindings. The @bnd@ is an identifier--- that determines a unique binder to the @var@. In practice, these are defined--- to be `Name` and `Var` respectively.-newtype GenProgram bnd var = Program [GenBinding bnd var]-                           deriving (Show, Eq, Read)---- | Variables, data constructors, type variables, and type constructors.-data NameSpace = VarNSpace | DataNSpace | TvNSpace | TcClsNSpace-               deriving (Show, Eq, Read, Ord)---- | The occurrence name is defined as a string, with a `Maybe` module name--- appearing. The `Int` denotes a `Unique` translated from GHC. For instance,--- in the case of @Map.empty@, the occurrence name is @"empty"@, while the--- module name is some variant of @Just \"Data.Map\"@.-data Name = Name String (Maybe String) NameSpace Int-          deriving (Show, Eq, Read, Ord)---- | Variables consist of a `Name` and a `Type`.-data Var = Var Name (GenType Name) deriving (Show, Eq, Read)---- | Literals are largely augmented from the original GHC implementation, with--- additional annotations to denote `BlankAddr` for lifting, `AddrLit` for--- value deriviation, `SymLit` for symbolic literals, and `SymLitEval` to--- represent symbolic literal evaluation, as literal manipulation functions--- are defined in the Haskell Prelude, and thus outside of scope for us.-data GenLit bnd var = MachChar     Char (GenType bnd)-                    | MachStr      String (GenType bnd)-                    | MachInt      Int (GenType bnd)-                    | MachWord     Int (GenType bnd)-                    | MachFloat    Rational (GenType bnd)-                    | MachDouble   Rational (GenType bnd)-                    | MachNullAddr (GenType bnd)-                    | MachLabel    String (Maybe Int) (GenType bnd)-                    | BlankAddr-                    | AddrLit      Int-                    | SymLit       var-                    | SymLitEval   (GenPrimFun bnd var) [GenLit bnd var]-                    deriving (Show, Eq, Read)---- | Atomic objects. `VarAtom` may be used for variable lookups, while--- `LitAtom` is used to denote literals.-data GenAtom bnd var = VarAtom var-                     | LitAtom (GenLit bnd var)-                     deriving (Show, Eq, Read)---- | Primitive functions.-data GenPrimFun bnd var = PrimFun bnd (GenType bnd) deriving (Show, Eq, Read)---- | Expressions closely correspond to their representation in GHC.-data GenExpr bnd var = Atom    (GenAtom bnd var)-                     | PrimApp (GenPrimFun bnd var) [GenAtom bnd var]-                     | ConApp  (GenDataCon bnd) [GenAtom bnd var]-                     | FunApp  var [GenAtom bnd var]-                     | Let     (GenBinding bnd var) (GenExpr bnd var)-                     | Case    (GenExpr bnd var) var [GenAlt bnd var]-                     deriving (Show, Eq, Read)---- | Alternatives utilize an `AltCon`, a list of parameters of that match to--- the appropriate `DataAlt` as applicable, and an expression for the result.-data GenAlt bnd var = Alt (GenAltCon bnd var) [var] (GenExpr bnd var)-                    deriving (Show, Eq, Read)---- | Alt Constructor-data GenAltCon bnd var = DataAlt (GenDataCon bnd)-                       | LitAlt  (GenLit bnd var)-                       | Default-                       deriving (Show, Eq, Read)---- | Binding-data GenBinding bnd var = Binding RecForm [(var, GenBindRhs bnd var)]-                        deriving (Show, Eq, Read)---- | Recursive?-data RecForm = Rec | NonRec deriving (Show, Eq, Read)---- | `BindRhs` taken straight from STG can be either in constructor form, or--- function form. Empty parameter list denotes a thunk.-data GenBindRhs bnd var = ConForm (GenDataCon bnd) [GenAtom bnd var]-                        | FunForm [var] (GenExpr bnd var)-                        deriving (Show, Eq, Read)---- | Data Constructor consists of its tag, the type that corresponds to its--- ADT, and a list of paramters it takes.-data GenDataCon bnd = DataCon bnd (GenType bnd) [GenType bnd]-                    deriving (Show, Eq, Read)---- | Types are information that are useful to keep during symbolic execution--- in order to generate correct feeds into the SMT solver. Overapproxmation is--- currently performed, and is likely to be cut back in the future.-data GenType bnd = TyVarTy    bnd (GenType bnd)-                 | AppTy      (GenType bnd) (GenType bnd)-                 | ForAllTy   (GenTyBinder bnd) (GenType bnd)-                 | CastTy     (GenType bnd) (GenCoercion bnd)-                 | TyConApp   (GenTyCon bnd) [GenType bnd]-                 | CoercionTy (GenCoercion bnd)-                 | LitTy      TyLit-                 | FunTy      (GenType bnd) (GenType bnd)-                 | Bottom-                 deriving (Show, Eq, Read)---- | Type binder for `ForAllTy`.-data GenTyBinder bnd = NamedTyBndr bnd-                     | AnonTyBndr-                     deriving (Show, Eq, Read)---- | `Type` literal.-data TyLit = NumTyLit Int-           | StrTyLit String-           deriving (Show, Eq, Read)---- | Coercion. I have no idea what this does :)-data GenCoercion bnd = Coercion (GenType bnd) (GenType bnd)-                     deriving (Show, Eq, Read)---- | Type constructor.-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.-data GenAlgTyRhs bnd = AbstractTyCon Bool-                     | DataTyCon     [bnd]-                     | NewTyCon      bnd-                     | TupleTyCon    bnd-                     deriving (Show, Eq, Read)-

@@ -1,53 +0,0 @@--- | Typing Module-module SSTG.Core.Syntax.Typing-    ( module SSTG.Core.Syntax.Typing-    ) where--import SSTG.Core.Syntax.Language---- | Variable type.-varType :: Var -> Type-varType (Var _ ty) = ty---- | Literal type.-litType :: Lit -> Type-litType (MachChar _ ty)      = ty-litType (MachStr _ ty)       = ty-litType (MachInt _ ty)       = ty-litType (MachWord _ ty)      = ty-litType (MachFloat _ ty)     = ty-litType (MachDouble _ ty)    = ty-litType (MachNullAddr ty)    = ty-litType (MachLabel _ _ ty)   = ty-litType (BlankAddr)          = Bottom-litType (AddrLit _)          = Bottom-litType (SymLit var)         = varType var-litType (SymLitEval pf args) = foldl AppTy (primFunType pf) (map litType args)---- | Atom type.-atomType :: Atom -> Type-atomType (VarAtom var) = varType var-atomType (LitAtom lit) = litType lit---- | Primitive function type.-primFunType :: PrimFun -> Type-primFunType (PrimFun _ ty) = ty---- | Data constructor type denoted as a function.-dataConType :: DataCon -> Type-dataConType (DataCon _ ty tys) = foldr FunTy ty tys---- | Alt type-altType :: Alt -> Type-altType (Alt _ _ expr) = exprType expr---- | I wonder what this could possibly be?-exprType :: Expr -> Type-exprType (Atom atom)       = atomType atom-exprType (PrimApp pf args) = foldl AppTy (primFunType pf) (map atomType args)-exprType (ConApp dc args)  = foldl AppTy (dataConType dc) (map atomType args)-exprType (FunApp fun args) = foldl AppTy (varType fun)    (map atomType args)-exprType (Let _ expr)      = exprType expr-exprType (Case _ _ (a:_))  = altType a-exprType _                 = Bottom-

@@ -5,7 +5,7 @@     , mkIOStr     ) where -import qualified SSTG.Core.Syntax.Language as SL+import qualified SSTG.Core.Language as SL  import Coercion import CorePrep

@@ -50,7 +50,6 @@         expr_str    = (pprCodeStr     . state_code)    state         names_str   = (pprNamesStr    . state_names)   state         pcons_str   = (pprPathConsStr . state_paths)   state-        links_str   = (pprSymLinksStr . state_links)   state         acc_strs    = [ ">>>>> [State] >>>>>>>>>>>>>>>"                       , status_str                       , "----- [Stack] ---------------"@@ -65,8 +64,6 @@                       , fst ("", names_str)  -- names_str                       , "----- [Path Constraint] -----"                       , pcons_str-                      , "----- [Symbolic Links] ------"-                      , links_str                       , "<<<<<<<<<<<<<<<<<<<<<<<<<<<<<" ]  -- | Inject `String` into parantheses.@@ -367,10 +364,4 @@         locs_str = pprLocalsStr locals         hold_str = case hold of { True -> "Positive"; False -> "Negative" }         acc_strs = [acon_str, prms_str, expr_str, locs_str, hold_str]---- | Print `SymLinks`.-pprSymLinksStr :: SymLinks -> String-pprSymLinksStr symlinks = injNewLineSeps5 acc_strs-  where slist    = symlinksToList symlinks-        acc_strs = map (\(k, v) -> pprNameStr k ++ ", " ++  pprNameStr v) slist