-
Notifications
You must be signed in to change notification settings - Fork 1
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Implement stepping out of functions from a paused symbolic execution …
…frame This change completes Vikraman's sketch of the functionality. It: - Removes the error calls (replacing them with logging) - Simplifies the single stepping implementation - Redesigns the symbolic execution state management and rendering The issue with the state management was that symbolic execution state was duplicated between the core and the brick UI in a way that allowed them to get out of sync. This mean that changes to the core state (e.g., as users advance the suspended state via commands) were not reflected in the UI (as the UI state was stale). To fix this, all updates to the symbolic execution state now go through a new distinguished message (the handler for which applies the update). This allows the frontends to apply additional processing to observe all of these updates and regenerate the UI state whenever there is a relevant update. This also simplifies the symbolic execution widget, which now only returns its own updated state (and handles any state updates via message passing). Some other changes included with this change: - There is an option for adding calling context information for generated log entries - Extracts the core symbolic execution state handlers and puts them back into the core where they belong - Make symbolic execution session state updates safer (remove mergeSessionState) Closes #74 (integrated with these changes)
- Loading branch information
Showing
23 changed files
with
577 additions
and
337 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
117 changes: 31 additions & 86 deletions
117
surveyor-brick/src/Surveyor/Brick/Handlers/SymbolicExecution.hs
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,108 +1,53 @@ | ||
| {-# LANGUAGE GADTs #-} | ||
| -- | Brick-level handlers for symbolic execution events | ||
| module Surveyor.Brick.Handlers.SymbolicExecution ( handleSymbolicExecutionEvent ) where | ||
|
|
||
| import qualified Brick as B | ||
| import qualified Control.Concurrent.Async as A | ||
| import Control.Lens ( (&), (^.), (.~), (%~), _Just, (^?) ) | ||
| import Control.Lens ( (&), (^.), (%~), _Just ) | ||
| import Control.Monad.IO.Class ( liftIO ) | ||
| import qualified Control.NF as NF | ||
| import qualified Data.Map.Strict as Map | ||
| import qualified Data.Parameterized.Classes as PC | ||
| import Data.Parameterized.Some ( Some(..) ) | ||
| import qualified Data.Text as T | ||
| import qualified Lang.Crucible.Simulator.RegMap as CSR | ||
| import qualified Lang.Crucible.Types as LCT | ||
| import GHC.Stack ( HasCallStack ) | ||
| import Surveyor.Brick.Names ( Names(..) ) | ||
| import qualified Surveyor.Core as C | ||
| import qualified What4.Expr.Builder as WEB | ||
|
|
||
| import qualified Surveyor.Brick.Extension as SBE | ||
| import qualified Surveyor.Brick.Widget.SymbolicExecution as SEM | ||
|
|
||
| handleSymbolicExecutionEvent :: (C.Architecture arch s) | ||
| -- | This handler provides brick UI-specific handling for symbolic execution events | ||
| -- | ||
| -- This handler is intended to run after the core-provided handlers, providing | ||
| -- hooks to update UI state when needed. | ||
| -- | ||
| -- We really only need to do one thing: capture any updates to the symbolic | ||
| -- execution state so that we can rebuild the relevant UI elements | ||
| handleSymbolicExecutionEvent :: (C.Architecture arch s, HasCallStack) | ||
| => C.S SBE.BrickUIExtension SBE.BrickUIState arch s | ||
| -> C.SymbolicExecutionEvent s (C.S SBE.BrickUIExtension SBE.BrickUIState) | ||
| -> B.EventM Names (B.Next (C.State SBE.BrickUIExtension SBE.BrickUIState s)) | ||
| handleSymbolicExecutionEvent s0 evt = | ||
| case evt of | ||
| C.InitializeSymbolicExecution archNonce mConfig mFuncHandle | ||
| | Just PC.Refl <- PC.testEquality archNonce (s0 ^. C.lNonce) | ||
| , Just sessionID <- s0 ^? C.lArchState . _Just . C.contextL . C.currentContext . C.symExecSessionIDL | ||
| , Just symExSt <- s0 ^? C.lArchState . _Just . C.symExStateL -> do | ||
| -- FIXME: Instead of the default, we could scan the context stack for | ||
| -- the most recent configuration | ||
| let ng = C.sNonceGenerator s0 | ||
| conf <- liftIO $ maybe (C.defaultSymbolicExecutionConfig ng) return mConfig | ||
| case C.lookupSessionState symExSt sessionID of | ||
| Just (Some oldState) -> liftIO $ C.cleanupSymbolicExecutionState oldState | ||
| Nothing -> return () | ||
| let newState = C.configuringSymbolicExecution conf | ||
| let manager = SEM.symbolicExecutionManager (Some newState) | ||
| let s1 = s0 & C.lUIMode .~ C.SomeUIMode C.SymbolicExecutionManager | ||
| & C.lArchState . _Just . C.lUIState . SBE.symbolicExecutionManagerL .~ manager | ||
| & C.lArchState . _Just . C.symExStateL %~ C.mergeSessionState (C.singleSessionState newState) | ||
| & C.lArchState . _Just . C.contextL . C.currentContext . C.symExecSessionIDL .~ C.symbolicSessionID newState | ||
| B.continue (C.State s1) | ||
| | otherwise -> B.continue (C.State s0) | ||
|
|
||
| C.BeginSymbolicExecutionSetup archNonce symExConfig cfg | ||
| C.InitializeSymbolicExecution {} -> B.continue (C.State s0) | ||
| C.BeginSymbolicExecutionSetup {} -> B.continue (C.State s0) | ||
| C.StartSymbolicExecution {} -> B.continue (C.State s0) | ||
| C.ReportSymbolicExecutionMetrics {} -> B.continue (C.State s0) | ||
| C.NameValue {} -> B.continue (C.State s0) | ||
| C.InitializeValueNamePrompt {} -> B.continue (C.State s0) | ||
| C.SetCurrentSymbolicExecutionValue {} -> B.continue (C.State s0) | ||
| C.UpdateSymbolicExecutionState archNonce newState | ||
| | Just PC.Refl <- PC.testEquality archNonce (s0 ^. C.lNonce) -> do | ||
| let ng = C.sNonceGenerator s0 | ||
| symExSt <- liftIO $ C.initializingSymbolicExecution ng symExConfig cfg | ||
| let manager = SEM.symbolicExecutionManager (Some symExSt) | ||
| let s1 = s0 & C.lUIMode .~ C.SomeUIMode C.SymbolicExecutionManager | ||
| & C.lArchState . _Just . C.lUIState . SBE.symbolicExecutionManagerL .~ manager | ||
| & C.lArchState . _Just . C.symExStateL %~ C.mergeSessionState (C.singleSessionState symExSt) | ||
| B.continue (C.State s1) | ||
| | otherwise -> B.continue (C.State s0) | ||
| -- Whenever the symbolic execution state changes, we need to rebuild | ||
| -- the UI for the corresponding session ID | ||
| let sessionID = C.symbolicSessionID newState | ||
|
|
||
| C.StartSymbolicExecution archNonce ares symState | ||
| | Just PC.Refl <- PC.testEquality archNonce (s0 ^. C.lNonce) -> do | ||
| let eventChan = s0 ^. C.lEventChannel | ||
| (newState, executionLoop) <- liftIO $ C.startSymbolicExecution eventChan ares symState | ||
| task <- liftIO $ A.async $ do | ||
| inspectState <- executionLoop | ||
| let updateSymExecState _ st = | ||
| let manager = SEM.symbolicExecutionManager (Some inspectState) | ||
| in st & C.lUIMode .~ C.SomeUIMode C.SymbolicExecutionManager | ||
| & C.lArchState . _Just . C.lUIState . SBE.symbolicExecutionManagerL .~ manager | ||
| & C.lArchState . _Just . C.symExStateL %~ C.mergeSessionState (C.singleSessionState newState) | ||
| -- We pass () as the value of the update state and capture the real | ||
| -- value (the new state) because there isn't an easy way to get an | ||
| -- NFData instance for states. That is okay, though, because they are | ||
| -- evaluated enough. | ||
| C.writeChan eventChan (C.AsyncStateUpdate archNonce (NF.nf ()) updateSymExecState) | ||
| let manager = SEM.symbolicExecutionManager (Some newState) | ||
| let s1 = s0 & C.lUIMode .~ C.SomeUIMode C.SymbolicExecutionManager | ||
| & C.lArchState . _Just . C.lUIState . SBE.symbolicExecutionManagerL .~ manager | ||
| & C.lArchState . _Just . C.symExStateL %~ C.mergeSessionState (C.singleSessionState newState) | ||
| B.continue (C.State s1) | ||
| | otherwise -> B.continue (C.State s0) | ||
|
|
||
| C.ReportSymbolicExecutionMetrics sid metrics -> do | ||
| let s1 = s0 & C.lArchState . _Just . C.symExStateL %~ C.updateSessionMetrics sid metrics | ||
| B.continue (C.State s1) | ||
|
|
||
| C.NameValue valueNonce name -> do | ||
| let s1 = s0 & C.lValueNames %~ C.addValueName valueNonce name | ||
| B.continue (C.State s1) | ||
| let msg = C.msgWithContext { C.logLevel = C.Debug | ||
| , C.logText = [ T.pack ("Updating widget for session " ++ show sessionID) ] | ||
| } | ||
| liftIO $ C.logMessage s0 msg | ||
|
|
||
| C.InitializeValueNamePrompt archNonce name | ||
| | Just PC.Refl <- PC.testEquality archNonce (s0 ^. C.lNonce) | ||
| , Just sessionID <- s0 ^? C.lArchState . _Just . C.contextL . C.currentContext . C.symExecSessionIDL | ||
| , Just symExSt <- s0 ^? C.lArchState . _Just . C.symExStateL | ||
| , Just (Some (C.Suspended _symNonce suspSt)) <- C.lookupSessionState symExSt sessionID | ||
| , Just (Some curVal) <- C.suspendedCurrentValue suspSt -> do | ||
| case LCT.asBaseType (CSR.regType curVal) of | ||
| LCT.AsBaseType _btr -> | ||
| case CSR.regValue curVal of | ||
| WEB.AppExpr ae -> liftIO $ C.sEmitEvent s0 (C.NameValue (WEB.appExprId ae) name) | ||
| WEB.NonceAppExpr nae -> liftIO $ C.sEmitEvent s0 (C.NameValue (WEB.nonceExprId nae) name) | ||
| _ -> return () | ||
| LCT.NotBaseType -> return () | ||
| B.continue (C.State s0) | ||
| | otherwise -> do | ||
| liftIO $ C.logMessage s0 (C.msgWith { C.logLevel = C.Debug | ||
| , C.logSource = C.EventHandler (T.pack "InitializeValueNamePrompt") | ||
| , C.logText = [T.pack "Pattern matches failed"] | ||
| }) | ||
| B.continue (C.State s0) | ||
| let manager = SEM.symbolicExecutionManager (Some newState) | ||
| let s1 = s0 & C.lArchState . _Just . C.lUIState . SBE.symbolicExecutionStateL %~ Map.insert sessionID manager | ||
| B.continue (C.State s1) | ||
| | otherwise -> B.continue (C.State s0) |
Oops, something went wrong.