diff --git a/SSTG.cabal b/SSTG.cabal --- a/SSTG.cabal +++ b/SSTG.cabal @@ -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 diff --git a/app/Main.hs b/app/Main.hs --- a/app/Main.hs +++ b/app/Main.hs @@ -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. diff --git a/src/SSTG/Core.hs b/src/SSTG/Core.hs --- a/src/SSTG/Core.hs +++ b/src/SSTG/Core.hs @@ -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 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 @@ -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] 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 @@ -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 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 @@ -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' diff --git a/src/SSTG/Core/Execution/Stepping.hs b/src/SSTG/Core/Execution/Stepping.hs --- a/src/SSTG/Core/Execution/Stepping.hs +++ b/src/SSTG/Core/Execution/Stepping.hs @@ -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]) 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 @@ -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. diff --git a/src/SSTG/Core/Language.hs b/src/SSTG/Core/Language.hs new file mode 100644 --- /dev/null +++ b/src/SSTG/Core/Language.hs @@ -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 + diff --git a/src/SSTG/Core/Language/Syntax.hs b/src/SSTG/Core/Language/Syntax.hs new file mode 100644 --- /dev/null +++ b/src/SSTG/Core/Language/Syntax.hs @@ -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) + diff --git a/src/SSTG/Core/Language/Typing.hs b/src/SSTG/Core/Language/Typing.hs new file mode 100644 --- /dev/null +++ b/src/SSTG/Core/Language/Typing.hs @@ -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 + diff --git a/src/SSTG/Core/Syntax.hs b/src/SSTG/Core/Syntax.hs deleted file mode 100644 --- a/src/SSTG/Core/Syntax.hs +++ /dev/null @@ -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 - diff --git a/src/SSTG/Core/Syntax/Language.hs b/src/SSTG/Core/Syntax/Language.hs deleted file mode 100644 --- a/src/SSTG/Core/Syntax/Language.hs +++ /dev/null @@ -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) - diff --git a/src/SSTG/Core/Syntax/Typing.hs b/src/SSTG/Core/Syntax/Typing.hs deleted file mode 100644 --- a/src/SSTG/Core/Syntax/Typing.hs +++ /dev/null @@ -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 - 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 @@ -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 diff --git a/src/SSTG/Utils/Printing.hs b/src/SSTG/Utils/Printing.hs --- a/src/SSTG/Utils/Printing.hs +++ b/src/SSTG/Utils/Printing.hs @@ -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