diff --git a/SSTG.cabal b/SSTG.cabal --- a/SSTG.cabal +++ b/SSTG.cabal @@ -1,5 +1,5 @@ name: SSTG -version: 0.1.0.1 +version: 0.1.0.2 synopsis: STG Symbolic Execution description: Prototype of STG-based Symbolic Execution for Haskell. homepage: https://github.com/AntonXue/SSTG#readme @@ -30,6 +30,7 @@ , SSTG.Core.Execution.Stepper , SSTG.Utils , SSTG.Utils.PrettyPrint + ghc-options: -Wall -fmax-pmcheck-iterations=2000000 build-depends: base >= 4.7 && < 5 , ghc , ghc-paths diff --git a/app/Main.hs b/app/Main.hs --- a/app/Main.hs +++ b/app/Main.hs @@ -2,8 +2,6 @@ import SSTG -import qualified Data.Map as M - import System.Environment main :: IO () @@ -18,16 +16,17 @@ -- Do the loading. let load_result = loadStateEntry entry (Program binds) putStrLn $ "binds: " ++ show (length binds) + -- putStrLn "Bindings" + -- mapM_ (putStrLn . pprBindingStr) binds + case load_result of LoadError str -> do error str LoadOkay state -> do - -- putStrLn "Bindings" - -- mapM_ (putStrLn . pprBindingStr) binds putStrLn" **************** INIT ***************" - putStrLn "Initial state:" - putStrLn $ pprStateStr state - let lds = execute1 100 state + -- putStrLn "Initial state:" + -- putStrLn $ pprStateStr state + let lds = execute1 200 state putStrLn "*************** BEGIN ***************" putStrLn $ pprLivesDeadsStr lds LoadGuess state cands -> do 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 @@ -11,8 +11,7 @@ import SSTG.Core.Execution.Namer import SSTG.Core.Execution.Stepper -import qualified Data.List as L -import qualified Data.Map as M +import qualified Data.Map as M -- | Load Result data LoadResult = LoadOkay State @@ -59,7 +58,6 @@ , state_links = SymLinks M.empty } -- Gather information on all variables. - names = allNames state0 state = state0 { state_names = allNames state0 } -- | Allocate Binding @@ -89,12 +87,6 @@ bnd_addrss = zip bnds addrss name_vals = concatMap bndAddrsToNameVals bnd_addrss --- | Force Get Address -forceLookupAddr :: Var -> Globals -> MemAddr -forceLookupAddr var globals = case lookupGlobals var globals of - Just (MemVal addr) -> addr - otherwise -> MemAddr (-1) - -- | Force Atom Lookup forceLookupValue :: Atom -> Locals -> Globals -> Value forceLookupValue (LitAtom lit) _ _ = LitVal lit @@ -134,7 +126,7 @@ -- | Bind Filtering bindFilter :: String -> (Binding, Locals) -> Bool -bindFilter entry (bnd, loc) = lhsMatches entry bnd /= [] +bindFilter entry (bnd, _) = lhsMatches entry bnd /= [] -- | Sub-Bindings String Match lhsMatches :: String -> Binding -> [(Var, BindRhs)] diff --git a/src/SSTG/Core/Execution/Models.hs b/src/SSTG/Core/Execution/Models.hs --- a/src/SSTG/Core/Execution/Models.hs +++ b/src/SSTG/Core/Execution/Models.hs @@ -28,7 +28,7 @@ instance Monad (SymbolicT s) where return a = pure a st >>= fs = SymbolicT (\s0 -> let (s1, a1) = (run st) s0 - (s2, a2) = (run (fs a1)) s2 in (s2, a2)) + (s2, a2) = (run (fs a1)) s1 in (s2, a2)) -- | State data State = State { state_status :: Status @@ -91,7 +91,8 @@ type PathCons = [PathCond] -- | Path Condition -data PathCond = PathCond Alt Expr Locals Bool deriving (Show, Eq, Read) +data PathCond = PathCond (AltCon, [Var]) Expr Locals Bool + deriving (Show, Eq, Read) -- | Symbolic Link Table newtype SymLinks = SymLinks (M.Map Name Name) deriving (Show, Eq, Read) @@ -142,9 +143,9 @@ -- | Allocate Heap List allocHeapList :: [HeapObj] -> Heap -> (Heap, [MemAddr]) allocHeapList [] heap = (heap, []) -allocHeapList (hobj:hobjs) heap = (res_heap, addr : as) - where (heap', addr) = allocHeap hobj heap - (res_heap, as) = allocHeapList hobjs heap' +allocHeapList (hobj:hobjs) heap = (heapf, addr : as) + where (heap', addr) = allocHeap hobj heap + (heapf, as) = allocHeapList hobjs heap' -- | Insert Heap insertHeap :: MemAddr -> HeapObj -> Heap -> Heap @@ -180,17 +181,12 @@ Nothing -> lookupGlobals var globals mb_value -> mb_value --- | Look Up Value by Atom -alookupValue :: Atom -> Locals -> Globals -> Maybe Value -alookupValue (LitAtom lit) _ _ = Just (LitVal lit) -alookupValue (VarAtom var) locals globals = lookupValue var locals globals - -- | Lookup Heap by Variable vlookupHeap :: Var -> Locals -> Globals -> Heap -> Maybe (MemAddr, HeapObj) vlookupHeap var locals globals heap = do val <- lookupValue var locals globals case val of - LitVal lit -> Nothing + LitVal _ -> Nothing MemVal addr -> lookupHeap addr heap >>= \hobj -> return (addr, hobj) -- | MemAddr Type @@ -198,9 +194,9 @@ memAddrType addr heap = do hobj <- lookupHeap addr heap return $ case hobj of - Blackhole -> Bottom - LitObj lit -> litType lit - SymObj (Symbol svar) -> varType svar - ConObj dcon _ -> dataConType dcon - FunObj params expr _ -> FunTy (map varType params ++ [exprType expr]) + Blackhole -> Bottom + LitObj lit -> litType lit + SymObj (Symbol sv) -> varType sv + ConObj dcon _ -> dataConType dcon + FunObj prms expr _ -> foldr FunTy (exprType expr) (map varType prms) diff --git a/src/SSTG/Core/Execution/Namer.hs b/src/SSTG/Core/Execution/Namer.hs --- a/src/SSTG/Core/Execution/Namer.hs +++ b/src/SSTG/Core/Execution/Namer.hs @@ -11,11 +11,9 @@ import SSTG.Core.Syntax import SSTG.Core.Execution.Models -import qualified Data.Char as C -import qualified Data.IntMap as IM -import qualified Data.List as L -import qualified Data.Map as M -import qualified Data.Set as S +import qualified Data.List as L +import qualified Data.Map as M +import qualified Data.Set as S -- | All Names in State allNames :: State -> [Name] @@ -56,12 +54,12 @@ -- | Heap Object Names heapObjNames :: HeapObj -> [Name] -heapObjNames Blackhole = [] -heapObjNames (LitObj _) = [] -heapObjNames (SymObj sym) = symbolNames sym -heapObjNames (ConObj dcon _) = dataNames dcon -heapObjNames (FunObj prms expr locals) = - concatMap varNames prms ++ exprNames expr ++ localsNames locals +heapObjNames Blackhole = [] +heapObjNames (LitObj _) = [] +heapObjNames (SymObj sym) = symbolNames sym +heapObjNames (ConObj dcon _) = dataNames dcon +heapObjNames (FunObj ps expr locs) = exprNames expr ++ localsNames locs + ++ concatMap varNames ps -- | Symbol Names symbolNames :: Symbol -> [Name] @@ -97,8 +95,8 @@ 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 (Case expr var alts) = varNames var ++ exprNames expr + ++ concatMap altNames alts -- | Type Names typeNames :: Type -> [Name] typeNames (TyVarTy n ty) = n : typeNames ty @@ -108,8 +106,7 @@ typeNames (TyConApp tc ty) = tyConNames tc ++ concatMap typeNames ty typeNames (CoercionTy coer) = coercionNames coer typeNames (LitTy _) = [] -typeNames (FunTy tys) = concatMap typeNames tys -typeNames (TyClosure ty ts) = concatMap typeNames (ty : ts) +typeNames (FunTy t1 t2) = typeNames t1 ++ typeNames t2 typeNames (Bottom) = [] -- | Prim Fun Names @@ -122,7 +119,7 @@ -- | Data Constructor Names dataNames :: DataCon -> [Name] -dataNames (DataCon id ty tys) = conTagName id : concatMap typeNames (ty : tys) +dataNames (DataCon tg ty tys) = conTagName tg : concatMap typeNames (ty : tys) -- | Type Binder Names tyBinderNames :: TyBinder -> [Name] @@ -131,13 +128,13 @@ -- | Type Constructor Names 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 (PromotedDataCon n dcon) = n : dataNames dcon +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 -- | Coercion Names coercionNames :: Coercion -> [Name] @@ -152,9 +149,9 @@ -- | Binding Names bindingNames :: Binding -> [Name] -bindingNames (Binding _ bnds) = lhs ++ rhs - where lhs = concatMap (varNames . fst) bnds - rhs = concatMap (bindRhsNames . snd) bnds +bindingNames (Binding _ bnd) = lhs ++ rhs + where lhs = concatMap (varNames . fst) bnd + rhs = concatMap (bindRhsNames . snd) bnd -- | Path Constraint Names pconsNames :: PathCons -> [Name] @@ -163,12 +160,13 @@ -- | Path Condition Names pcondNames :: PathCond -> [Name] -pcondNames (PathCond alt expr locals _) = altNames alt ++ exprNames expr - ++ localsNames locals +pcondNames (PathCond (_, vars) expr locals _) = map varName vars ++ + exprNames expr ++ + localsNames locals -- | Symbolic Link Names linksNames :: SymLinks -> [Name] -linksNames (SymLinks links) = [] -- map (\(a, b) -> [a, b]) kvs +linksNames (SymLinks links) = concatMap (\(a, b) -> [a, b]) kvs where kvs = M.toList links -- | Fresh String from Int Rand Seed @@ -192,8 +190,8 @@ -- | Seeded Fresh Name from Conflict List freshSeededName :: Name -> [Name] -> Name -freshSeededName seed confs = Name occ' mod ns unq' - where Name occ mod ns unq = seed +freshSeededName seed confs = Name occ' mdl ns unq' + where Name occ mdl ns unq = seed occ' = freshString 1 occ (S.fromList alls) unq' = maxs + 1 alls = map nameOccStr confs 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 @@ -9,13 +9,12 @@ import SSTG.Core.Execution.Models import SSTG.Core.Execution.Namer -import qualified Data.Map as M - -- | Rules data Rule = RuleAtomLit | RuleAtomLitPtr | RuleAtomValPtr | RuleAtomUnInt | RulePrimApp | RuleConApp - | RuleFunAppExact | RuleFunAppUnder | RuleFunAppSym | RuleFunAppUnInt + | RuleFunAppExact | RuleFunAppUnder | RuleFunAppSym + | RuleFunAppConPtr | RuleFunAppUnInt | RuleLet | RuleCaseLit | RuleCaseConPtr | RuleCaseAnyLit | RuleCaseAnyConPtr | RuleCaseSym @@ -43,14 +42,15 @@ isHeapValueForm _ = False -- | Is Value Form --- Either a lit or points to a heap value (not LitObj!) +-- Either a lit or points to a heap value (not LitObj!). If we find nothing +-- in the heap, then this means we can still upcast the var to a symbolic. isExprValueForm :: Expr -> Locals -> Globals -> Heap -> Bool isExprValueForm (Atom (LitAtom _)) _ _ _ = True isExprValueForm (Atom (VarAtom var)) locals globals heap = case vlookupHeap var locals globals heap of Just (_, hobj) -> isHeapValueForm hobj Nothing -> False -isExprValueForm _ _ _ _ = False +isExprValueForm _ _ _ _ = False -- | Is State Value? isStateValueForm :: State -> Bool @@ -76,39 +76,86 @@ unevenZip :: [a] -> [b] -> ([(a, b)], Either [a] [b]) unevenZip as [] = ([], Left as) unevenZip [] bs = ([], Right bs) -unevenZip (a:as) (b:bs) = ((a, b) : acc, rem) - where (acc, rem) = unevenZip as bs +unevenZip (a:as) (b:bs) = ((a, b) : acc, excess) + where (acc, excess) = unevenZip as bs --- | Inject Type Closure -injTyClosure :: Type -> [Atom] -> Type -injTyClosure ty args = TyClosure ty (map atomType args) +-- | Lift Action Wrap Type +data LiftAct a = LiftAct a Locals Globals Heap [Name] --- | Bind Rhs to Heap Object -rhsToObj :: BindRhs -> Locals -> Globals -> Maybe HeapObj -rhsToObj (FunForm prms expr) locals _ = Just (FunObj prms expr locals) -rhsToObj (ConForm dcon args) locals globals = do - arg_vals <- mapM (\a -> alookupValue a locals globals) args - return (ConObj dcon arg_vals) +-- | Lift Uninterpreted Variable +liftUnInt :: LiftAct Var -> LiftAct MemAddr +liftUnInt (LiftAct var locals globals heap confs) = pass_out + where sname = freshSeededName (varName var) confs + svar = Var sname (varType var) + (heap', addr) = allocHeap (SymObj (Symbol svar)) heap + globals' = insertGlobals var (MemVal addr) globals + confs' = sname : confs + pass_out = LiftAct addr locals globals' heap' confs' --- | Lift Let Binding -liftBinding :: Binding -> Locals -> Globals -> Heap -> Maybe (Heap, Locals) -liftBinding (Binding NonRec bnd) locals globals heap = do - hobjs <- mapM (\r -> rhsToObj r locals globals) (map snd bnd) - let (heap', addrs) = allocHeapList hobjs heap - return (heap', locals) -liftBinding (Binding Rec bnd) (Locals lmap) globals heap = do - let names = map (varName . fst) bnd - let hfakes = map (const Blackhole) bnd - -- Allocate dummy BlackholeS - let (heap', addrs) = allocHeapList hfakes heap - let mem_vals = map (\a -> MemVal a) addrs - -- Use the allocated BlackholeS to construct the locals closure. - let lmap' = M.fromList (zip names mem_vals) - let locals' = Locals (M.union lmap' lmap) - hobjs <- mapM (\r -> rhsToObj r locals' globals) (map snd bnd) - let injects = zip addrs hobjs - return (insertHeapList injects heap', locals') +-- | Lift Atom +liftAtom :: LiftAct Atom -> LiftAct Value +liftAtom (LiftAct atom locals globals heap confs) = pass_out + where pass_out = LiftAct aval locals globals' heap' confs' + (aval, globals', heap', confs') = case atom of + LitAtom lit -> (LitVal lit, globals, heap, confs) + VarAtom var -> case lookupValue var locals globals of + Just val -> (val, globals, heap, confs) + Nothing -> let pass_in = LiftAct var locals globals heap confs + LiftAct addr _ g' h' c' = liftUnInt pass_in + in (MemVal addr, g', h', c') +-- | Lift Atom List +liftAtomList :: LiftAct [Atom] -> LiftAct [Value] +liftAtomList (LiftAct [] locals globals heap confs) = pass_out + where pass_out = LiftAct [] locals globals heap confs +liftAtomList (LiftAct (atom:as) locals globals heap confs) = pass_out + where pass_in = LiftAct atom locals globals heap confs + LiftAct val locals' globals' heap' confs' = liftAtom pass_in + pass_rest = LiftAct as locals' globals' heap' confs' + LiftAct vs localsf globalsf heapf confsf = liftAtomList pass_rest + pass_out = LiftAct (val : vs) localsf globalsf heapf confsf + +-- | Lift Bind Rhs +liftBindRhs :: LiftAct BindRhs -> LiftAct HeapObj +liftBindRhs (LiftAct (FunForm prms expr) locals globals heap confs) = pass_out + where pass_out = LiftAct (FunObj prms expr locals) locals globals heap confs +liftBindRhs (LiftAct (ConForm dcon args) locals globals heap confs) = pass_out + where pass_in = LiftAct args locals globals heap confs + LiftAct vals locals' globals' heap' confs' = liftAtomList pass_in + pass_out = LiftAct (ConObj dcon vals) locals' globals' heap' confs' + +-- | Lift Bind Rhs List +liftBindRhsList :: LiftAct [BindRhs] -> LiftAct [HeapObj] +liftBindRhsList (LiftAct [] locals globals heap confs) = pass_out + where pass_out = LiftAct [] locals globals heap confs +liftBindRhsList (LiftAct (rhs:rs) locals globals heap confs) = pass_out + where pass_in = LiftAct rhs locals globals heap confs + LiftAct hobj locals' globals' heap' confs' = liftBindRhs pass_in + pass_rest = LiftAct rs locals' globals' heap' confs' + LiftAct hos localsf globalsf heapf confsf = liftBindRhsList pass_rest + pass_out = LiftAct (hobj : hos) localsf globalsf heapf confsf + +-- | Lift Binding +liftBinding :: LiftAct Binding -> LiftAct () +liftBinding (LiftAct (Binding NonRec bnd) locals globals heap confs) = pass_out + where pass_in = LiftAct (map snd bnd) locals globals heap confs + LiftAct hobjs locals' globals' heap' confs' = liftBindRhsList pass_in + (heapf, addrs) = allocHeapList hobjs heap' + mem_vals = map MemVal addrs + localsf = insertLocalsList (zip (map fst bnd) mem_vals) locals' + pass_out = LiftAct () localsf globals' heapf confs' +liftBinding (LiftAct (Binding Rec bnd) locals globals heap confs) = pass_out + where hfakes = map (const Blackhole) bnd + -- Allocate dummy BLACKHOLEs + (heap', addrs) = allocHeapList hfakes heap + mem_vals = map MemVal addrs + -- Use the reigstered loca BLACKHOLEs to construct the locals closure. + locals' = insertLocalsList (zip (map fst bnd) mem_vals) locals + pass_in = LiftAct (map snd bnd) locals' globals heap' confs + LiftAct hobjs localsf globals' heap'' confs' = liftBindRhsList pass_in + heapf = insertHeapList (zip addrs hobjs) heap'' + pass_out = LiftAct () localsf globals' heapf confs' + -- | Default Alts defaultAlts :: [Alt] -> [Alt] defaultAlts alts = [a | a @ (Alt Default _ _) <- alts] @@ -130,28 +177,30 @@ negatePathCons pcs = map (\(PathCond a e l b) -> (PathCond a e l (not b))) pcs -- | Lift Sym Alt -liftSymAlt :: Var -> MemAddr -> Var -> Locals -> Heap -> [Name] -> Alt -> - (Expr, Locals, Heap, PathCons, [Name]) -liftSymAlt mvar addr cvar locals heap confs (Alt ac params expr) = - (expr, locals', heap', pcons, confs') - where pre_names = freshSeededNameList (map varName params) confs - sym_vars = map (\(p, n) -> Var n (varType p)) (zip params pre_names) - sym_objs = map (\v -> SymObj (Symbol v)) sym_vars - (heap', addrs) = allocHeapList sym_objs heap - mem_vals = map (\a -> MemVal a) addrs - llist = (cvar, MemVal addr) : zip params mem_vals - locals' = insertLocalsList llist locals - mxpr = Atom (VarAtom mvar) - pcons = [PathCond (Alt ac params expr) mxpr locals' True] - confs' = pre_names ++ confs +liftSymAlt :: LiftAct (Var, MemAddr, Var, Alt) -> LiftAct (Expr, PathCons) +liftSymAlt (LiftAct args locals globals heap confs) = pass_out + where (mvar, addr, cvar, Alt ac params expr) = args + snames = freshSeededNameList (map varName params) confs + svars = map (\(p, n) -> Var n (varType p)) (zip params snames) + hobjs = map (SymObj . Symbol) svars + (heap', addrs) = allocHeapList hobjs heap + mem_vals = map MemVal addrs + llist = (cvar, MemVal addr) : zip params mem_vals + locals' = insertLocalsList llist locals + mxpr = Atom (VarAtom mvar) + pcons = [PathCond (ac, params) mxpr locals' True] + confs' = snames ++ confs + pass_out = LiftAct (expr, pcons) locals' globals heap' confs' -- | Alt Closure to State -altClosureToState :: State -> (Expr, Locals, Heap, PathCons, [Name]) -> State -altClosureToState state (expr, locals, heap, pcons, confs) = state' - where state' = state { state_heap = heap - , state_code = Evaluate expr locals - , state_names = confs ++ state_names state - , state_paths = pcons ++ state_paths state } +liftedAltToState :: State -> LiftAct (Expr, PathCons) -> State +liftedAltToState state (LiftAct args locals globals heap confs) = state' + where (expr, pcons) = args + state' = state { state_heap = heap + , state_globals = globals + , state_code = Evaluate expr locals + , state_names = confs + , state_paths = pcons ++ state_paths state } -- | Reduce reduce :: State -> Maybe (Rule, [State]) @@ -159,8 +208,7 @@ , state_heap = heap , state_globals = globals , state_code = code - , state_names = confs - , state_paths = paths } + , state_names = confs } -- Stack Independent Rules @@ -186,63 +234,73 @@ -- Rule Atom Uninterpreted | Evaluate (Atom (VarAtom uvar)) locals <- code , Nothing <- vlookupHeap uvar locals globals heap = do - let sname = freshSeededName (varName uvar) confs - let svar = Var sname (varType uvar) - let sym = Symbol svar - let (heap', addr) = allocHeap (SymObj sym) heap - let globals' = insertGlobals uvar (MemVal addr) globals + let pass_in = LiftAct uvar locals globals heap confs + let LiftAct _ locals' globals' heap' confs' = liftUnInt pass_in return ( RuleAtomUnInt , [state { state_heap = heap' , state_globals = globals' - , state_code = Evaluate (Atom (VarAtom uvar)) locals - , state_names = sname : confs }]) + , state_code = Evaluate (Atom (VarAtom uvar)) locals' + , state_names = confs' }]) -- Prim Function App | Evaluate (PrimApp pfun args) locals <- code = do - arg_vals <- mapM (\a -> alookupValue a locals globals) args - let eval = SymLitEval pfun (map valueToLit arg_vals) + let pass_in = LiftAct args locals globals heap confs + let LiftAct vals locals' globals' heap' confs' = liftAtomList pass_in + let eval = SymLitEval pfun (map valueToLit vals) return ( RulePrimApp - , [state { state_code = Evaluate (Atom (LitAtom eval)) locals }]) + , [state { state_heap = heap' + , state_globals = globals' + , state_code = Evaluate (Atom (LitAtom eval)) locals' + , state_names = confs' }]) -- | Rule Con App | Evaluate (ConApp dcon args) locals <- code = do - arg_vals <- mapM (\a -> alookupValue a locals globals) args - let (heap', addr) = allocHeap (ConObj dcon arg_vals) heap + let pass_in = LiftAct args locals globals heap confs + let LiftAct vals _ globals' heap' confs' = liftAtomList pass_in + let (heapf, addr) = allocHeap (ConObj dcon vals) heap' return ( RuleConApp - , [state { state_heap = heap' - , state_code = Return (MemVal addr) }]) + , [state { state_heap = heapf + , state_globals = globals' + , state_code = Return (MemVal addr) + , state_names = confs' }]) -- | Rule Fun App Exact | Evaluate (FunApp fun args) locals <- code , Just (_, hobj) <- vlookupHeap fun locals globals heap , FunObj params expr fun_locs <- hobj , length params == length args = do - arg_vals <- mapM (\a -> alookupValue a locals globals) args - let fun_locs' = insertLocalsList (zip params arg_vals) fun_locs + let pass_in = LiftAct args locals globals heap confs + let LiftAct vals _ globals' heap' confs' = liftAtomList pass_in + let fun_locs' = insertLocalsList (zip params vals) fun_locs return ( RuleFunAppExact - , [state { state_code = Evaluate expr fun_locs' }]) + , [state { state_heap = heap' + , state_globals = globals' + , state_code = Evaluate expr fun_locs' + , state_names = confs' }]) -- Rule Fun App Under | Evaluate (FunApp fun args) locals <- code , Just (_, hobj) <- vlookupHeap fun locals globals heap , FunObj params expr fun_locs <- hobj - , (_, Left ex_prms) <- unevenZip params args = do - -- Set up existing closure first. - arg_vals <- mapM (\a -> alookupValue a locals globals) args - let fun_locs' = insertLocalsList (zip params arg_vals) fun_locs + , (_, Left ex_ps) <- unevenZip params args = do + let pass_in = LiftAct args locals globals heap confs + let LiftAct vals _ globals' heap' confs' = liftAtomList pass_in + let fun_locs' = insertLocalsList (zip params vals) fun_locs -- New Fun Object. - let pfobj = FunObj ex_prms expr fun_locs' - let (heap', pfaddr) = allocHeap pfobj heap + let pobj = FunObj ex_ps expr fun_locs' + let (heapf, paddr) = allocHeap pobj heap' return ( RuleFunAppUnder - , [state { state_heap = heap' - , state_code = Return (MemVal pfaddr) }]) + , [state { state_heap = heapf + , state_globals = globals' + , state_code = Return (MemVal paddr) + , state_names = confs' }]) -- Rule Fun App Symbolic | Evaluate (FunApp sfun args) locals <- code , Just (_, hobj) <- vlookupHeap sfun locals globals heap , SymObj (Symbol svar) <- hobj = do let sname = freshSeededName (varName svar) confs - let svar' = Var sname (injTyClosure (varType svar) args) + let svar' = Var sname (foldl AppTy (varType svar) (map atomType args)) let sym = Symbol svar' let (heap', addr) = allocHeap (SymObj sym) heap return ( RuleFunAppSym @@ -250,26 +308,33 @@ , state_code = Return (MemVal addr) , state_names = sname : confs }]) + -- Rule Fun App ConObj + | Evaluate (FunApp cvar []) locals <- code + , Just (addr, hobj) <- vlookupHeap cvar locals globals heap + , ConObj _ _ <- hobj = do + return ( RuleFunAppConPtr + , [state { state_code = Return (MemVal addr) }]) + -- Rule Fun App Uninterpreted | Evaluate (FunApp ufun args) locals <- code , Nothing <- vlookupHeap ufun locals globals heap = do - let sname = freshSeededName (varName ufun) confs - let svar = Var sname (varType ufun) - let sym = Symbol svar - let (heap', addr) = allocHeap (SymObj sym) heap - let globals' = insertGlobals ufun (MemVal addr) globals + let pass_in = LiftAct ufun locals globals heap confs + let LiftAct _ locals' globals' heap' confs' = liftUnInt pass_in return ( RuleFunAppUnInt - , [state { state_heap = heap' - , state_globals = globals' - , state_code = Evaluate (FunApp ufun args) locals - , state_names = sname : confs }]) + , [ state { state_heap = heap' + , state_globals = globals' + , state_code = Evaluate (FunApp ufun args) locals' + , state_names = confs' }]) -- Rule Let | Evaluate (Let bnd expr) locals <- code = do - (heap', locals') <- liftBinding bnd locals globals heap + let pass_in = LiftAct bnd locals globals heap confs + let LiftAct _ locals' globals' heap' confs' = liftBinding pass_in return ( RuleLet - , [state { state_heap = heap' - , state_code = Evaluate expr locals' }]) + , [state { state_heap = heap' + , state_globals = globals' + , state_code = Evaluate expr locals' + , state_names = confs' }]) -- Rule Case Lit | Evaluate (Case (Atom (LitAtom lit)) cvar alts) locals <- code @@ -318,16 +383,20 @@ , SymObj _ <- hobj , (acon_alts, def_alts) <- (altConAlts alts, defaultAlts alts) , length (acon_alts ++ def_alts) > 0 = do - -- Remember to account for cvar. - let acon_clss = map (liftSymAlt mvar addr cvar locals heap confs) acon_alts - let def_clss = map (liftSymAlt mvar addr cvar locals heap confs) def_alts + let acon_ins = map (\a -> LiftAct (mvar, addr, cvar, a) + locals globals heap confs) acon_alts + let acon_lifts = map liftSymAlt acon_ins + let def_ins = map (\a -> LiftAct (mvar, addr, cvar, a) + locals globals heap confs) def_alts + let def_lifts = map liftSymAlt def_ins -- Make AltCon states first. - let acon_sts = map (altClosureToState state) acon_clss - -- Make Default states next. - let all_pcons = concatMap (\(_, _, _, pc, _) -> pc) acon_clss - let neg_pcons = negatePathCons all_pcons - let def_clss' = map (\(e, l, h, p, c) -> (e, l, h, neg_pcons, c)) def_clss - let def_sts = map (altClosureToState state) def_clss' + let acon_sts = map (liftedAltToState state) acon_lifts + -- Make DEFAULT states next. + let all_pcons = concatMap (\(LiftAct (_, pc) _ _ _ _) -> pc) acon_lifts + let negs = negatePathCons all_pcons + let def_lifts' = map (\(LiftAct (e, _) l g h c) -> + (LiftAct (e, negs) l g h c)) def_lifts + let def_sts = map (liftedAltToState state) def_lifts' return (RuleCaseSym, acon_sts ++ def_sts) -- Stack Dependent Rules @@ -404,12 +473,16 @@ , Evaluate (FunApp fun args) locals <- code , Just (_, hobj) <- vlookupHeap fun locals globals heap , FunObj params expr fun_locs <- hobj - , (_, Right ex_args) <- unevenZip params args = do - arg_vals <- mapM (\a -> alookupValue a locals globals) args - let fun_locs' = insertLocalsList (zip params arg_vals) fun_locs + , (_, Right ex_as) <- unevenZip params args = do + let pass_in = LiftAct args locals globals heap confs + let LiftAct vals locals' globals' heap' confs' = liftAtomList pass_in + let fun_locs' = insertLocalsList (zip params vals) fun_locs return ( RuleApplyCFunAppOver - , [state { state_stack = Stack (ApplyFrame ex_args locals : frames) - , state_code = Evaluate expr fun_locs' }]) + , [state { state_stack = Stack (ApplyFrame ex_as locals' : frames) + , state_heap = heap' + , state_globals = globals' + , state_code = Evaluate expr fun_locs' + , state_names = confs' }]) -- Rule Apply Frame Delete ReturnPtr Function | Stack (ApplyFrame args frm_locs : rest) <- stack diff --git a/src/SSTG/Core/Execution/Stepper.hs b/src/SSTG/Core/Execution/Stepper.hs --- a/src/SSTG/Core/Execution/Stepper.hs +++ b/src/SSTG/Core/Execution/Stepper.hs @@ -5,12 +5,9 @@ , runBoundedDFS ) where -import SSTG.Core.Syntax import SSTG.Core.Execution.Models import SSTG.Core.Execution.Rules -import qualified Data.Map as M - type LiveState = ([Rule], State) type DeadState = ([Rule], State) @@ -38,5 +35,6 @@ start = SymbolicT { run = (\lives -> (lives, [])) } execution = foldl (\acc s -> s <*> acc) start passes +runBoundedDFS :: a runBoundedDFS = undefined 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 @@ -105,8 +105,7 @@ | TyConApp (GenTyCon bnd) [GenType bnd] | CoercionTy (GenCoercion bnd) | LitTy TyLit - | FunTy [GenType bnd] - | TyClosure (GenType bnd) [GenType bnd] + | FunTy (GenType bnd) (GenType bnd) | Bottom deriving (Show, Eq, Read) @@ -125,13 +124,13 @@ deriving (Show, Eq, Read) -- | TyCon -data GenTyCon bnd = FunTyCon bnd - | AlgTyCon bnd (GenAlgTyRhs bnd) - | SynonymTyCon bnd - | FamilyTyCon bnd - | PrimTyCon bnd - | PromotedDataCon bnd (GenDataCon bnd) - | TcTyCon bnd +data GenTyCon bnd = FunTyCon bnd + | AlgTyCon bnd (GenAlgTyRhs bnd) + | SynonymTyCon bnd + | FamilyTyCon bnd + | PrimTyCon bnd + | Promoted bnd (GenDataCon bnd) + | TcTyCon bnd deriving (Show, Eq, Read) -- | Algebraic Type Constructor RHS diff --git a/src/SSTG/Core/Syntax/Typer.hs b/src/SSTG/Core/Syntax/Typer.hs --- a/src/SSTG/Core/Syntax/Typer.hs +++ b/src/SSTG/Core/Syntax/Typer.hs @@ -16,10 +16,11 @@ litType (MachFloat _ ty) = ty litType (MachDouble _ ty) = ty litType (MachNullAddr ty) = ty +litType (MachLabel _ _ ty) = ty litType (BlankAddr) = Bottom -litType (AddrLit addr) = Bottom +litType (AddrLit _) = Bottom litType (SymLit var) = varType var -litType (SymLitEval pf args) = TyClosure (primFunType pf) (map litType args) +litType (SymLitEval pf args) = foldl AppTy (primFunType pf) (map litType args) atomType :: Atom -> Type atomType (VarAtom var) = varType var @@ -36,9 +37,9 @@ exprType :: Expr -> Type exprType (Atom atom) = atomType atom -exprType (PrimApp pf args) = TyClosure (primFunType pf) (map atomType args) +exprType (PrimApp pf args) = foldl AppTy (primFunType pf) (map atomType args) exprType (ConApp dcon _) = dataConType dcon -exprType (FunApp fun args) = TyClosure (varType fun) (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 @@ -1,43 +1,33 @@ -- | Haskell Translation -- Extracts SSTG from Haskell source. module SSTG.Core.Translation.Haskell - ( mkTargetBindings + ( mkCompileClosure + , mkTargetBindings , mkIOStr ) where import qualified SSTG.Core.Syntax.Language as SL -import BasicTypes import Coercion import CorePrep import CoreSyn import CoreToStg -import CostCentre import DataCon import FastString -import ForeignCall import GHC import GHC.Paths -import GhcMonad import HscTypes import Literal -import Module import Name import Outputable import Pair import PrimOp -import SrcLoc import StgSyn import TyCon import TyCoRep -import Type -import UniqSet import Unique import Var as V -import System.IO - -import qualified Data.IntMap as IM import qualified Data.Maybe as MB -- | Make IO String from Outputable @@ -56,14 +46,13 @@ let mod_lcs = map (\s -> (ms_mod s, ms_location s)) sums let m_bndss = map mg_binds gutss let m_tcss = map mg_tcs gutss - - let z1 = zip3 mod_lcs m_bndss m_tcss - preps <- sequence $ map (\((m, l), b, t) -> corePrepPgm env m l b t) z1 - - let z2 = zip (map fst mod_lcs) preps - stg_bndss <- sequence $ map (\(m, p) -> coreToStg dflags m p) z2 - - let sl_bnds = map mkBinding (concat stg_bndss) + -- Zip in preparation for STG transformation. + let z1 = zip3 mod_lcs m_bndss m_tcss + preps <- mapM (\((m, l), b, t) -> corePrepPgm env m l b t) z1 + let z2 = zip (map fst mod_lcs) preps + s_bndss <- mapM (\(m, p) -> coreToStg dflags m p) z2 + -- Create the bindings. + let sl_bnds = map mkBinding (concat s_bndss) return sl_bnds -- | Make Compilation Closure @@ -76,19 +65,18 @@ mkCompileClosure proj src = runGhc (Just libdir) $ do beta_flags <- getSessionDynFlags let dflags = beta_flags { importPaths = [proj] } - setSessionDynFlags dflags - env <- getSession - target <- guessTarget src Nothing - setTargets [target] - load LoadAllTargets - - mod_graph <- getModuleGraph - pmods <- (sequence . map parseModule) mod_graph - tmods <- (sequence . map typecheckModule) pmods - dmods <- (sequence . map desugarModule) tmods - let mod_gutss = map coreModule dmods - - let zipd = (zip mod_graph mod_gutss, dflags, env) + _ <- setSessionDynFlags dflags + env <- getSession + target <- guessTarget src Nothing + _ <- setTargets [target] + _ <- load LoadAllTargets + -- Now that things are loaded, make the compilation closure. + mod_graph <- getModuleGraph + pmods <- mapM parseModule mod_graph + tmods <- mapM typecheckModule pmods + dmods <- mapM desugarModule tmods + let m_gtss = map coreModule dmods + let zipd = (zip mod_graph m_gtss, dflags, env) return zipd -- | Make SSTG Expr @@ -111,11 +99,11 @@ -- | Make SSTG Name mkName :: Name -> SL.Name -mkName name = SL.Name occ mod ns unq +mkName name = SL.Name occ mdl ns unq where occ = (occNameString . nameOccName) name ns = (mkNameSpace . occNameSpace . nameOccName) name unq = (getKey . nameUnique) name - mod = case nameModule_maybe name of + mdl = case nameModule_maybe name of Nothing -> Nothing Just md -> Just ((moduleNameString . moduleName) md) @@ -136,8 +124,8 @@ -- | Make SSTG Binding mkBinding :: StgBinding -> SL.Binding mkBinding (StgNonRec bnd rhs) = SL.Binding SL.NonRec [(mkVar bnd, mkRhs rhs)] -mkBinding (StgRec bnds) = SL.Binding SL.Rec - (map (\(b, r) -> (mkVar b, mkRhs r)) bnds) +mkBinding (StgRec bnd) = SL.Binding SL.Rec + (map (\(b, r) -> (mkVar b, mkRhs r)) bnd) -- | Make SSTG Rhs mkRhs :: StgRhs -> SL.BindRhs @@ -148,7 +136,7 @@ -- | Make SSTG Lit mkLit :: Literal -> SL.Lit mkLit lit = case lit of - (MachChar char) -> SL.MachChar char ((mkType . literalType) lit) + (MachChar chr) -> SL.MachChar chr ((mkType . literalType) lit) (MachStr bstr) -> SL.MachStr (show bstr) ((mkType . literalType) lit) (MachInt i) -> SL.MachInt (fromInteger i) ((mkType . literalType) lit) (MachInt64 i) -> SL.MachInt (fromInteger i) ((mkType . literalType) lit) @@ -161,15 +149,15 @@ (MachLabel f m _) -> SL.MachLabel (unpackFS f) m ((mkType . literalType) lit) -- | Make SSTG Data Constructor ID -mkDataId :: DataCon -> SL.ConTag -mkDataId datacon = SL.ConTag name tag +mkDataTag :: DataCon -> SL.ConTag +mkDataTag datacon = SL.ConTag name tag where name = (mkName . dataConName) datacon tag = dataConTag datacon -- | Make SSTG Data Constructor mkData :: DataCon -> SL.DataCon mkData datacon = SL.DataCon dcid ty args - where dcid = mkDataId datacon + where dcid = mkDataTag datacon ty = (mkType . dataConRepType) datacon args = map mkType (dataConOrigArgTys datacon) @@ -177,11 +165,11 @@ mkPrimOp :: StgOp -> SL.PrimFun mkPrimOp (StgPrimOp op) = SL.PrimFun (SL.Name occ Nothing ns unq) ty where occname = primOpOcc op - occ = occNameString occname - ns = (mkNameSpace . occNameSpace) occname - unq = primOpTag op - ty = (mkType . primOpType) op -mkPrimOp otherwise = error "mkPrimOp: got StgPrimCallOp or StgFCallOp" + occ = occNameString occname + ns = (mkNameSpace . occNameSpace) occname + unq = primOpTag op + ty = (mkType . primOpType) op +mkPrimOp _ = error "mkPrimOp: got StgPrimCallOp or StgFCallOp" -- | Make SSTG Alt mkAlt :: StgAlt -> SL.Alt @@ -191,7 +179,7 @@ mkAltCon :: AltCon -> SL.AltCon mkAltCon (DataAlt dc) = SL.DataAlt (mkData dc) mkAltCon (LitAlt lit) = SL.LitAlt (mkLit lit) -mkAltCon DEFAULT = SL.Default +mkAltCon (DEFAULT) = SL.Default -- | Make SSTG Type mkType :: Type -> SL.Type @@ -203,42 +191,37 @@ mkType (CastTy ty cor) = SL.CastTy (mkType ty) (mkCoercion cor) mkType (CoercionTy cor) = SL.CoercionTy (mkCoercion cor) --- | Make SSTG Kind -mkKind :: Kind -> SL.Type -mkKind = mkType - -- | Make SSTG Type Constructor 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 +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.PromotedDataCon name dcon + | isPromotedDataCon tc = SL.Promoted name dcon | otherwise = error "mkTyCon: unrecognized TyCon" where name = (mkName . tyConName) tc - kind = (mkKind . tyConKind) tc algrhs = (mkAlgTyConRhs . algTyConRhs) tc dcon = (mkData . MB.fromJust . isPromotedDataCon_maybe) tc -- | Make SSTG Algebraic Type Constructor RHS mkAlgTyConRhs :: AlgTyConRhs -> SL.AlgTyRhs mkAlgTyConRhs (AbstractTyCon b) = SL.AbstractTyCon b -mkAlgTyConRhs (DataTyCon {data_cons = dcs}) = SL.DataTyCon (map mkDataId dcs) -mkAlgTyConRhs (TupleTyCon {data_con = dc}) = SL.TupleTyCon (mkDataId dc) -mkAlgTyConRhs (NewTyCon {data_con = dc}) = SL.NewTyCon (mkDataId dc) +mkAlgTyConRhs (DataTyCon {data_cons = dcs}) = SL.DataTyCon (map mkDataTag dcs) +mkAlgTyConRhs (TupleTyCon {data_con = dc}) = SL.TupleTyCon (mkDataTag dc) +mkAlgTyConRhs (NewTyCon {data_con = dc}) = SL.NewTyCon (mkDataTag dc) -- | make SSTG Type Binder mkTyBndr :: TyBinder -> SL.TyBinder mkTyBndr (Anon ty) = SL.AnonTyBndr (mkType ty) -mkTyBndr (Named v f) = SL.NamedTyBndr (mkName (V.varName v)) +mkTyBndr (Named v _) = SL.NamedTyBndr (mkName (V.varName v)) (mkType (varType v)) -- | Make SSTG Type Literal mkTyLit :: TyLit -> SL.TyLit -mkTyLit (NumTyLit int) = SL.NumTyLit (fromInteger int) -mkTyLit (StrTyLit fs) = SL.StrTyLit (unpackFS fs) +mkTyLit (NumTyLit i) = SL.NumTyLit (fromInteger i) +mkTyLit (StrTyLit fs) = SL.StrTyLit (unpackFS fs) -- | Make SSTG Coercion mkCoercion :: Coercion -> SL.Coercion diff --git a/src/SSTG/Utils/PrettyPrint.hs b/src/SSTG/Utils/PrettyPrint.hs --- a/src/SSTG/Utils/PrettyPrint.hs +++ b/src/SSTG/Utils/PrettyPrint.hs @@ -58,7 +58,7 @@ , "----- [Expression] ----------" , expr_str , "----- [All Names] -------" - , "" -- names_str + , fst ("", names_str) -- names_str , "----- [Path Constraint] -----" , pcons_str , "----- [Symbolic Links] ------" @@ -126,7 +126,7 @@ pprFrameStr (UpdateFrame addr) = injNewLine acc_strs where header = "UpdateFrame" addr_str = pprMemAddrStr addr - acc_strs = [addr_str] + acc_strs = [header, addr_str] pprHeapObjStr :: HeapObj -> String pprHeapObjStr Blackhole = "Blackhole!!!" @@ -156,7 +156,9 @@ addr_strs = map (pprMemAddrStr . fst) kvs hobj_strs = map (pprHeapObjStr . snd) kvs zipd_strs = zip addr_strs hobj_strs - acc_strs = map (\(m, o) -> sub (m ++ "," ++ o)) zipd_strs + addr_str = pprMemAddrStr addr + kvs_strs = map (\(m, o) -> sub (m ++ "," ++ o)) zipd_strs + acc_strs = addr_str : kvs_strs pprGlobalsStr :: Globals -> String pprGlobalsStr (Globals gmap) = injNewLine (map (\k -> ">" ++ k) acc_strs) @@ -202,15 +204,15 @@ acc_strs = [header, lit_str] pprConTagStr :: ConTag -> String -pprConTagStr (ConTag name int) = pprNameStr name +pprConTagStr (ConTag name _) = pprNameStr name pprDataConStr :: DataCon -> String -pprDataConStr (DataCon id ty tys) = injSpace acc_strs +pprDataConStr (DataCon tag ty tys) = injSpace acc_strs where header = "DataCon" - id_str = (sub . pprConTagStr) id + tag_str = (sub . pprConTagStr) tag ty_str = (sub . pprTypeStr) ty tys_str = injIntoList (map pprTypeStr tys) - acc_strs = [header, id_str, ty_str, tys_str] + acc_strs = [header, tag_str, ty_str, tys_str] pprPrimFunStr :: PrimFun -> String pprPrimFunStr (PrimFun name ty) = injSpace acc_strs @@ -219,21 +221,21 @@ type_str = (sub . pprTypeStr) ty acc_strs = [header, name_str, type_str] -pprAltCon :: AltCon -> String -pprAltCon (DataAlt dcon) = injSpace acc_strs +pprAltConStr :: AltCon -> String +pprAltConStr (DataAlt dcon) = injSpace acc_strs where header = "DataAlt" dcon_str = (sub . pprDataConStr) dcon acc_strs = [header, dcon_str] -pprAltCon (LitAlt lit) = injSpace acc_strs +pprAltConStr (LitAlt lit) = injSpace acc_strs where header = "LitAlt" lit_str = (sub . pprLitStr) lit acc_strs = [header, lit_str] -pprAltCon Default = "Default" +pprAltConStr Default = "Default" pprAltStr :: Alt -> String pprAltStr (Alt acon var expr) = injSpace acc_strs where header = "Alt" - acon_str = (sub . pprAltCon) acon + acon_str = (sub . pprAltConStr) acon vars_str = injIntoList (map pprVarStr var) expr_str = (sub . pprExprStr) expr acc_strs = [header, acon_str, vars_str, expr_str] @@ -260,9 +262,9 @@ acc_strs = [var_str, lamf_str] pprBindingStr :: Binding -> String -pprBindingStr (Binding rec bnds) = injSpace acc_strs - where header = case rec of { Rec -> "Rec-Bind"; NonRec -> "NonRec-Bind" } - bnds_str = injIntoList (map bindStr bnds) +pprBindingStr (Binding rec bnd) = injSpace acc_strs + where header = case rec of { Rec -> "Rec"; NonRec -> "NonRec" } + bnds_str = injIntoList (map bindStr bnd) acc_strs = [header, bnds_str] pprExprStr :: Expr -> String @@ -298,7 +300,7 @@ acc_strs = [header, bnd_str, expr_str] pprTypeStr :: Type -> String -pprTypeStr ty = "__Type__" +pprTypeStr ty = fst ("__Type__", ty) -- | State Code String pprCodeStr :: Code -> String @@ -323,12 +325,13 @@ -- | Path Condition String pprPCondStr :: PathCond -> String -pprPCondStr (PathCond alt expr locals hold) = injIntoList acc_strs - where alt_str = pprAltStr alt +pprPCondStr (PathCond (acon, params) expr locals hold) = injIntoList acc_strs + where acon_str = pprAltConStr acon + prms_str = injIntoList (map pprVarStr params) expr_str = pprExprStr expr locs_str = pprLocalsStr locals hold_str = case hold of { True -> "Positive"; False -> "Negative" } - acc_strs = [alt_str, expr_str, locs_str, hold_str] + acc_strs = [acon_str, prms_str, expr_str, locs_str, hold_str] -- | Symbolic Links String pprLinksStr :: SymLinks -> String