SSTG 0.1.0.3 → 0.1.0.4
raw patch · 6 files changed
+146/−150 lines, 6 files
Files
- SSTG.cabal +1/−1
- app/Main.hs +3/−3
- src/SSTG/Core/Execution/Models.hs +5/−5
- src/SSTG/Core/Execution/Namer.hs +4/−4
- src/SSTG/Core/Execution/Rules.hs +131/−135
- src/SSTG/Utils/PrettyPrint.hs +2/−2
SSTG.cabal view
@@ -1,5 +1,5 @@ name: SSTG-version: 0.1.0.3+version: 0.1.0.4 synopsis: STG Symbolic Execution description: Prototype of STG-based Symbolic Execution for Haskell. homepage: https://github.com/AntonXue/SSTG#readme
app/Main.hs view
@@ -24,10 +24,10 @@ error str LoadOkay state -> do putStrLn" **************** INIT ***************"- -- putStrLn "Initial state:"- -- putStrLn $ pprStateStr state- let lds = execute1 200 state+ putStrLn "Initial state:"+ putStrLn $ pprStateStr state putStrLn "*************** BEGIN ***************"+ let lds = execute1 40 state putStrLn $ pprLivesDeadsStr lds LoadGuess state cands -> do putStrLn $ pprStateStr state
src/SSTG/Core/Execution/Models.hs view
@@ -52,7 +52,7 @@ newtype Stack = Stack [Frame] deriving (Show, Eq, Read) -- | Stack Frame-data Frame = AltFrame Var [Alt] Locals+data Frame = CaseFrame Var [Alt] Locals | ApplyFrame [Atom] Locals | UpdateFrame MemAddr deriving (Show, Eq, Read)@@ -178,8 +178,8 @@ -- | Lookup Value lookupValue :: Var -> Locals -> Globals -> Maybe Value lookupValue var locals globals = case lookupLocals var locals of- Nothing -> lookupGlobals var globals- mb_value -> mb_value+ Nothing -> lookupGlobals var globals+ mb_val -> mb_val -- | Lookup Heap by Variable vlookupHeap :: Var -> Locals -> Globals -> Heap -> Maybe (MemAddr, HeapObj)@@ -187,13 +187,13 @@ val <- lookupValue var locals globals case val of LitVal _ -> Nothing- MemVal addr -> lookupHeap addr heap >>= \hobj -> return (addr, hobj)+ MemVal addr -> lookupHeap addr heap >>= \hobj -> Just (addr, hobj) -- | MemAddr Type memAddrType :: MemAddr -> Heap -> Maybe Type memAddrType addr heap = do hobj <- lookupHeap addr heap- return $ case hobj of+ Just $ case hobj of Blackhole -> Bottom LitObj lit -> litType lit SymObj (Symbol s _) -> varType s
src/SSTG/Core/Execution/Namer.hs view
@@ -34,10 +34,10 @@ -- | Frame Names frameNames :: Frame -> [Name]-frameNames (UpdateFrame _) = []-frameNames (ApplyFrame as lcs) = concatMap atomNames as ++ localsNames lcs-frameNames (AltFrame var alts lcs) = varNames var ++ (concatMap altNames alts)- ++ localsNames lcs+frameNames (UpdateFrame _) = []+frameNames (ApplyFrame as lcs) = concatMap atomNames as ++ localsNames lcs+frameNames (CaseFrame var alts lcs) = varNames var ++ (concatMap altNames alts)+ ++ localsNames lcs -- | Alt Names altNames :: Alt -> [Name]
src/SSTG/Core/Execution/Rules.hs view
@@ -22,8 +22,8 @@ | RuleUpdateCThunk | RuleUpdateDLit | RuleUpdateDValPtr - | RuleAltCCaseNonVal- | RuleAltDLit | RuleAltDValPtr+ | RuleCaseCCaseNonVal+ | RuleCaseDLit | RuleCaseDValPtr | RuleApplyCFunThunk | RuleApplyCFunAppOver | RuleApplyDReturnFun | RuleApplyDReturnSym@@ -213,53 +213,53 @@ -- Stack Independent Rules -- Atom Lit- | Evaluate (Atom (LitAtom lit)) _ <- code = do- return ( RuleAtomLit- , [state { state_code = Return (LitVal lit) }])+ | Evaluate (Atom (LitAtom lit)) _ <- code =+ Just (RuleAtomLit+ ,[state { state_code = Return (LitVal lit) }]) -- Atom Lit Pointer | Evaluate (Atom (VarAtom var)) locals <- code , Just (_, hobj) <- vlookupHeap var locals globals heap- , LitObj lit <- hobj = do- return ( RuleAtomLitPtr- , [state { state_code = Evaluate (Atom (LitAtom lit)) locals }])+ , LitObj lit <- hobj =+ Just (RuleAtomLitPtr+ ,[state { state_code = Evaluate (Atom (LitAtom lit)) locals }]) -- Rule Atom Val Pointer | Evaluate (Atom (VarAtom var)) locals <- code , Just (addr, hobj) <- vlookupHeap var locals globals heap- , isHeapValueForm hobj = do- return ( RuleAtomValPtr- , [state { state_code = Return (MemVal addr) }])+ , isHeapValueForm hobj =+ Just (RuleAtomValPtr+ ,[state { state_code = Return (MemVal addr) }]) -- Rule Atom Uninterpreted | Evaluate (Atom (VarAtom uvar)) locals <- code- , Nothing <- vlookupHeap uvar locals globals heap = do+ , Nothing <- vlookupHeap uvar locals globals heap = let pass_in = LiftAct uvar locals globals heap confs- let LiftAct _ locals' globals' heap' confs' = liftUnInt pass_in- return ( RuleAtomUnInt- , [state { state_heap = heap'+ LiftAct _ locals' globals' heap' confs' = liftUnInt pass_in+ in Just (RuleAtomUnInt+ ,[state { state_heap = heap' , state_globals = globals' , state_code = Evaluate (Atom (VarAtom uvar)) locals' , state_names = confs' }]) -- Prim Function App- | Evaluate (PrimApp pfun args) locals <- code = do+ | Evaluate (PrimApp pfun args) locals <- code = 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_heap = heap'+ LiftAct vals locals' globals' heap' confs' = liftAtomList pass_in+ eval = SymLitEval pfun (map valueToLit vals)+ in Just (RulePrimApp+ ,[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+ | Evaluate (ConApp dcon args) locals <- code = 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 = heapf+ LiftAct vals _ globals' heap' confs' = liftAtomList pass_in+ (heapf, addr) = allocHeap (ConObj dcon vals) heap'+ in Just (RuleConApp+ ,[state { state_heap = heapf , state_globals = globals' , state_code = Return (MemVal addr) , state_names = confs' }])@@ -268,12 +268,12 @@ | Evaluate (FunApp fun args) locals <- code , Just (_, hobj) <- vlookupHeap fun locals globals heap , FunObj params expr fun_locs <- hobj- , length params == length args = do+ , length params == length args = 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_heap = heap'+ LiftAct vals _ globals' heap' confs' = liftAtomList pass_in+ fun_locs' = insertLocalsList (zip params vals) fun_locs+ in Just (RuleFunAppExact+ ,[state { state_heap = heap' , state_globals = globals' , state_code = Evaluate expr fun_locs' , state_names = confs' }])@@ -282,15 +282,15 @@ | Evaluate (FunApp fun args) locals <- code , Just (_, hobj) <- vlookupHeap fun locals globals heap , FunObj params expr fun_locs <- hobj- , (_, Left ex_ps) <- unevenZip params args = do+ , (_, Left ex_ps) <- unevenZip params args = 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 pobj = FunObj ex_ps expr fun_locs'- let (heapf, paddr) = allocHeap pobj heap'- return ( RuleFunAppUnder- , [state { state_heap = heapf+ LiftAct vals _ globals' heap' confs' = liftAtomList pass_in+ fun_locs' = insertLocalsList (zip params vals) fun_locs+ -- New Fun Object.+ pobj = FunObj ex_ps expr fun_locs'+ (heapf, paddr) = allocHeap pobj heap'+ in Just (RuleFunAppUnder+ ,[state { state_heap = heapf , state_globals = globals' , state_code = Return (MemVal paddr) , state_names = confs' }])@@ -298,106 +298,102 @@ -- Rule Fun App Symbolic | Evaluate (FunApp sfun args) locals <- code , Just (_, hobj) <- vlookupHeap sfun locals globals heap- , SymObj (Symbol svar _) <- hobj = do+ , SymObj (Symbol svar _) <- hobj = let sname = freshSeededName (varName svar) confs- let svar' = Var sname (foldl AppTy (varType svar) (map atomType args))- let sym = Symbol svar' (Just (FunApp sfun args, locals))- let (heap', addr) = allocHeap (SymObj sym) heap- return ( RuleFunAppSym- , [state { state_heap = heap'+ svar' = Var sname (foldl AppTy (varType svar) (map atomType args))+ sym = Symbol svar' (Just (FunApp sfun args, locals))+ (heap', addr) = allocHeap (SymObj sym) heap+ in Just (RuleFunAppSym+ ,[state { state_heap = heap' , 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) }])+ , ConObj _ _ <- hobj =+ Just (RuleFunAppConPtr+ ,[state { state_code = Return (MemVal addr) }]) -- Rule Fun App Uninterpreted | Evaluate (FunApp ufun args) locals <- code- , Nothing <- vlookupHeap ufun locals globals heap = do+ , Nothing <- vlookupHeap ufun locals globals heap = 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 = confs' }])+ LiftAct _ locals' globals' heap' confs' = liftUnInt pass_in+ in Just (RuleFunAppUnInt+ ,[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+ | Evaluate (Let bnd expr) locals <- code = let pass_in = LiftAct bnd locals globals heap confs- let LiftAct _ locals' globals' heap' confs' = liftBinding pass_in- return ( RuleLet- , [state { state_heap = heap'+ LiftAct _ locals' globals' heap' confs' = liftBinding pass_in+ in Just (RuleLet+ ,[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- , (Alt _ _ expr):_ <- matchLitAlts lit alts = do- -- Account for cvar.+ , (Alt _ _ expr):_ <- matchLitAlts lit alts = let locals' = insertLocals cvar (LitVal lit) locals- return ( RuleCaseLit- , [state { state_code = Evaluate expr locals' }])+ in Just (RuleCaseLit+ ,[state { state_code = Evaluate expr locals' }]) -- Rule Case Con Pointer | Evaluate (Case (Atom (VarAtom mvar)) cvar alts) locals <- code , Just (addr, hobj) <- vlookupHeap mvar locals globals heap , ConObj dcon vals <- hobj , (Alt _ params expr):_ <- matchDataAlts dcon alts- , length params == length vals = do- -- Account for cvar.+ , length params == length vals = let llist = (cvar, MemVal addr) : zip params vals- let locals' = insertLocalsList llist locals- return ( RuleCaseConPtr- , [state { state_code = Evaluate expr locals' }])+ locals' = insertLocalsList llist locals+ in Just (RuleCaseConPtr+ ,[state { state_code = Evaluate expr locals' }]) -- Rule Case Any Lit | Evaluate (Case (Atom (LitAtom lit)) cvar alts) locals <- code , [] <- matchLitAlts lit alts- , (Alt _ _ expr):_ <- defaultAlts alts = do- -- Account for cvar.+ , (Alt _ _ expr):_ <- defaultAlts alts = let locals' = insertLocals cvar (LitVal lit) locals- return ( RuleCaseAnyLit- , [state { state_code = Evaluate expr locals' }])+ in Just (RuleCaseAnyLit+ ,[state { state_code = Evaluate expr locals' }]) -- Rule Case Any Con Pointer | Evaluate (Case (Atom (VarAtom mvar)) cvar alts) locals <- code , Just (addr, hobj) <- vlookupHeap mvar locals globals heap , ConObj dcon _ <- hobj , [] <- matchDataAlts dcon alts- , (Alt _ _ expr):_ <- defaultAlts alts = do- -- Account for cvar.+ , (Alt _ _ expr):_ <- defaultAlts alts = let llist = (cvar, (MemVal addr)) : []- let locals' = insertLocalsList llist locals- return ( RuleCaseAnyConPtr- , [state { state_code = Evaluate expr locals' }])+ locals' = insertLocalsList llist locals+ in Just (RuleCaseAnyConPtr+ ,[state { state_code = Evaluate expr locals' }]) -- Rule Case Sym | Evaluate (Case (Atom (VarAtom mvar)) cvar alts) locals <- code , Just (addr, hobj) <- vlookupHeap mvar locals globals heap , SymObj _ <- hobj , (acon_alts, def_alts) <- (altConAlts alts, defaultAlts alts)- , length (acon_alts ++ def_alts) > 0 = do+ , length (acon_alts ++ def_alts) > 0 = 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)+ acon_lifts = map liftSymAlt acon_ins+ 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 (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) ->+ def_lifts = map liftSymAlt def_ins+ -- Make AltCon states first.+ acon_sts = map (liftedAltToState state) acon_lifts+ -- Make DEFAULT states next.+ all_pcons = concatMap (\(LiftAct (_, pc) _ _ _ _) -> pc) acon_lifts+ negs = negatePathCons all_pcons+ 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)+ def_sts = map (liftedAltToState state) def_lifts'+ in Just (RuleCaseSym, acon_sts ++ def_sts) -- Stack Dependent Rules @@ -405,17 +401,17 @@ | Stack frames <- stack , Evaluate (Atom (VarAtom var)) locals <- code , Just (addr, hobj) <- vlookupHeap var locals globals heap- , FunObj [] expr fun_locs <- hobj = do -- Thunk form.- return ( RuleUpdateCThunk- , [state { state_stack = Stack (UpdateFrame addr : frames)+ , FunObj [] expr fun_locs <- hobj = -- Thunk form.+ Just (RuleUpdateCThunk+ ,[state { state_stack = Stack (UpdateFrame addr : frames) , state_heap = insertHeap addr Blackhole heap , state_code = Evaluate expr fun_locs }]) -- Rule Update Frame Delete Lit | Stack (UpdateFrame frm_addr : rest) <- stack- , Return (LitVal lit) <- code = do- return ( RuleUpdateDLit- , [state { state_stack = Stack rest+ , Return (LitVal lit) <- code =+ Just (RuleUpdateDLit+ ,[state { state_stack = Stack rest , state_heap = insertHeap frm_addr (LitObj lit) heap , state_code = Return (LitVal lit) }]) @@ -423,39 +419,39 @@ | Stack (UpdateFrame frm_addr : rest) <- stack , Return (MemVal addr) <- code , Just hobj <- lookupHeap addr heap- , isHeapValueForm hobj = do- return ( RuleUpdateDValPtr- , [state { state_stack = Stack rest+ , isHeapValueForm hobj =+ Just (RuleUpdateDValPtr+ ,[state { state_stack = Stack rest , state_heap = insertHeap frm_addr hobj heap , state_code = Return (MemVal addr) }]) - -- Rule Alt Frame Create Case Non LitVal or MemVal+ -- Rule Case Frame Create Case Non LitVal or MemVal | Stack frames <- stack , Evaluate (Case mxpr cvar alts) locals <- code- , not (isExprValueForm mxpr locals globals heap) = do- return ( RuleAltCCaseNonVal- , [state { state_stack = Stack (AltFrame cvar alts locals : frames)+ , not (isExprValueForm mxpr locals globals heap) =+ Just (RuleCaseCCaseNonVal+ ,[state { state_stack = Stack (CaseFrame cvar alts locals : frames) , state_code = Evaluate mxpr locals }]) - -- Rule Alt Frame Delete Lit- | Stack (AltFrame cvar alts frm_locs : rest) <- stack- , Return (LitVal lit) <- code = do+ -- Rule Case Frame Delete Lit+ | Stack (CaseFrame cvar alts frm_locs : rest) <- stack+ , Return (LitVal lit) <- code = let mxpr = Atom (LitAtom lit)- return ( RuleAltDLit- , [state { state_stack = Stack rest+ in Just (RuleCaseDLit+ ,[state { state_stack = Stack rest , state_code = Evaluate (Case mxpr cvar alts) frm_locs }]) - -- Rule Alt Frame Delete Heap Value- | Stack (AltFrame cvar alts frm_locs : rest) <- stack- , Return (MemVal addr) <- code+ -- Rule Case Frame Delete Heap Value+ | Stack (CaseFrame cvar alts frm_locs : rest) <- stack+ , Return (MemVal addr) <- code , Just hobj <- lookupHeap addr heap- , isHeapValueForm hobj = do+ , isHeapValueForm hobj = let vname = freshSeededName (varName cvar) confs- let vvar = Var vname (varType cvar)- let mxpr = Atom (VarAtom vvar)- let frm_locs' = insertLocals vvar (MemVal addr) frm_locs- return ( RuleAltDValPtr- , [state { state_stack = Stack rest+ vvar = Var vname (varType cvar)+ mxpr = Atom (VarAtom vvar)+ frm_locs' = insertLocals vvar (MemVal addr) frm_locs+ in Just (RuleCaseDValPtr+ ,[state { state_stack = Stack rest , state_code = Evaluate (Case mxpr cvar alts) frm_locs' , state_names = vname : confs }]) @@ -463,9 +459,9 @@ | Stack frames <- stack , Evaluate (FunApp fun args) locals <- code , Just (_, hobj) <- vlookupHeap fun locals globals heap- , FunObj [] expr fun_locs <- hobj = do- return ( RuleApplyCFunThunk- , [state { state_stack = Stack (ApplyFrame args locals : frames)+ , FunObj [] expr fun_locs <- hobj =+ Just (RuleApplyCFunThunk+ ,[state { state_stack = Stack (ApplyFrame args locals : frames) , state_code = Evaluate expr fun_locs }]) -- Rule Apply Frame Create Function Over Application@@ -473,12 +469,12 @@ , Evaluate (FunApp fun args) locals <- code , Just (_, hobj) <- vlookupHeap fun locals globals heap , FunObj params expr fun_locs <- hobj- , (_, Right ex_as) <- unevenZip params args = do+ , (_, Right ex_as) <- unevenZip params args = 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_as locals' : frames)+ LiftAct vals locals' globals' heap' confs' = liftAtomList pass_in+ fun_locs' = insertLocalsList (zip params vals) fun_locs+ in Just (RuleApplyCFunAppOver+ ,[state { state_stack = Stack (ApplyFrame ex_as locals' : frames) , state_heap = heap' , state_globals = globals' , state_code = Evaluate expr fun_locs'@@ -488,13 +484,13 @@ | Stack (ApplyFrame args frm_locs : rest) <- stack , Return (MemVal addr) <- code , Just hobj <- lookupHeap addr heap- , FunObj _ _ _ <- hobj = do- ftype <- memAddrType addr heap+ , FunObj _ _ _ <- hobj+ , Just ftype <- memAddrType addr heap = let fname = freshName VarNSpace confs- let fvar = Var fname ftype- let frm_locs' = insertLocals fvar (MemVal addr) frm_locs- return ( RuleApplyDReturnFun- , [state { state_stack = Stack rest+ fvar = Var fname ftype+ frm_locs' = insertLocals fvar (MemVal addr) frm_locs+ in Just (RuleApplyDReturnFun+ ,[state { state_stack = Stack rest , state_code = Evaluate (FunApp fvar args) frm_locs' , state_names = fname : confs }]) @@ -502,17 +498,17 @@ | Stack (ApplyFrame args frm_locs : rest) <- stack , Return (MemVal addr) <- code , Just hobj <- lookupHeap addr heap- , SymObj (Symbol sym _) <- hobj = do+ , SymObj (Symbol sym _) <- hobj = let sname = freshSeededName (varName sym) confs- let svar = Var sname (varType sym)- let frm_locs' = insertLocals svar (MemVal addr) frm_locs- return ( RuleApplyDReturnSym- , [state { state_stack = Stack rest+ svar = Var sname (varType sym)+ frm_locs' = insertLocals svar (MemVal addr) frm_locs+ in Just (RuleApplyDReturnSym+ ,[state { state_stack = Stack rest , state_code = Evaluate (FunApp svar args) frm_locs' , state_names = sname : confs }]) -- State is Value Form- | isStateValueForm state = return (RuleIdentity, [state])+ | isStateValueForm state = Just (RuleIdentity, [state]) -- Everything Broke!!! | otherwise = Nothing
src/SSTG/Utils/PrettyPrint.hs view
@@ -112,8 +112,8 @@ acc_strs = "Stack" : frame_strs pprFrameStr :: Frame -> String-pprFrameStr (AltFrame var alts locals) = injNewLine acc_strs- where header = "AltFrame"+pprFrameStr (CaseFrame var alts locals) = injNewLine acc_strs+ where header = "CaseFrame" var_str = pprVarStr var alts_str = pprAltsStr alts locs_str = pprLocalsStr locals