Vikraman feat/step (#77)

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) Revises the handling of the breakpoint override Instead of having the debug execution feature identify breakpoints, implement a body for the breakpoint override that starts the debugger. This makes handling of breakpoints and debug assertions the same. Co-authored-by: Vikraman Choudhury <[email protected]>
GaloisInc · Dec 30, 2020 · 81992dd · 81992dd
1 parent f3cbb14
commit 81992dd
Show file tree

Hide file tree

Showing 25 changed files with 667 additions and 282 deletions.
diff --git a/crux-dbg/src/Crux/Debug/LLVM.hs b/crux-dbg/src/Crux/Debug/LLVM.hs
@@ -30,6 +30,9 @@ import           Data.Parameterized.Some ( Some(..) )
 import           Data.Proxy ( Proxy(..) )
 import           Data.String ( fromString )
 import qualified Data.Text as T
+import qualified Data.Text.Encoding as TE
+import qualified Data.Text.Encoding.Error as TE
+import           GHC.TypeLits ( type (<=) )
 import qualified System.Exit as SE
 import qualified System.IO as IO
 import qualified Text.LLVM as TL
@@ -81,7 +84,7 @@ breakpointOverrides :: ( LCB.IsSymInterface sym
                     -> [CLI.OverrideTemplate (SC.LLVMPersonality sym) sym arch rtp l a]
 breakpointOverrides cruxOpts sconf =
   [ CLI.basic_llvm_override $ [LCLQ.llvmOvr| void @crucible_breakpoint(i8*, ...) |]
-      do_breakpoint
+      (do_breakpoint sconf)
 
   , CLI.basic_llvm_override $ [LCLQ.llvmOvr| void @crucible_debug_assert( i8, i8*, i32 ) |]
       (do_debug_assert (parseSolverOffline cruxOpts) sconf)
@@ -155,22 +158,44 @@ simulateLLVMWithDebug cruxOpts dbgOpts bcFilePath = C.SimulatorCallback $ \sym _
                 case SC.llvmAnalysisResultFromModule ng nonce hdlAlloc llvmModule (Some translation) of
                   SC.SomeResult ares -> return ares
           let debuggerConfig = SB.DebuggerConfig (Proxy @SC.LLVM) (Proxy @(SC.CrucibleExt SC.LLVM)) llvmCon
-          let debugger = SB.debuggerFeature debuggerConfig (WEB.exprCounter sym)
           let initSt = LCS.InitialState simCtx globSt LCS.defaultAbortHandler LCT.UnitRepr $
                 LCS.runOverrideSim LCT.UnitRepr $ do
                   registerFunctions cruxOpts debuggerConfig llvmModule translation
                   checkEntryPoint (fromMaybe "main" (CDC.entryPoint dbgOpts)) (CLT.cfgMap translation)
           -- FIXME: We can use this callback to collect live explanations in terms of solver state
           let handleExplanation = \_ _ -> return mempty
-          return (C.RunnableStateWithExtensions initSt [debugger], handleExplanation)
+          let executionFeatures = []
+          return (C.RunnableStateWithExtensions initSt executionFeatures, handleExplanation)
         | otherwise -> CMC.throwM (UnsupportedX86BitWidth rep)
 
-do_breakpoint :: (wptr ~ CLE.ArchWidth arch)
-              => LCS.GlobalVar CLM.Mem
+do_breakpoint :: ( wptr ~ CLE.ArchWidth arch
+                 , ext ~ CLI.LLVM arch
+                 , sym ~ WEB.ExprBuilder t st fs
+                 , SC.SymbolicArchitecture arch' t
+                 , LCB.IsSymInterface sym
+                 , 1 <= wptr
+                 , 16 <= wptr
+                 )
+              => SB.DebuggerConfig t ext arch'
+              -> LCS.GlobalVar CLM.Mem
               -> sym
               -> Ctx.Assignment (LCS.RegEntry sym) (Ctx.EmptyCtx Ctx.::> CLT.LLVMPointerType wptr Ctx.::> LCT.VectorType LCT.AnyType)
               -> LCS.OverrideSim (SC.LLVMPersonality sym) sym (CLI.LLVM arch) r args ret ()
-do_breakpoint _gv _sym _ = return ()
+do_breakpoint sconf memVar sym (Ctx.Empty Ctx.:> breakpointNamePtr Ctx.:> breakpointValues) = do
+  let ?ptrWidth = CLM.ptrWidth (LCS.regValue breakpointNamePtr)
+  let ?recordLLVMAnnotation = \_ _ -> return ()
+  let ng = WEB.exprCounter sym
+  simState <- CMS.get
+  bpName <- case LCSG.lookupGlobal memVar (simState ^. LCSET.stateGlobals) of
+              Nothing -> return "<Unnamed Breakpoint>"
+              Just memImpl -> do
+                chars <- liftIO $ CLM.loadString sym memImpl (LCS.regValue breakpointNamePtr) Nothing
+                return (TE.decodeUtf8With TE.lenientDecode (BS.pack chars))
+  let bp = SC.Breakpoint { SC.breakpointType = SC.UnconditionalBreakpoint
+                         , SC.breakpointName = Just bpName
+                         , SC.breakpointArguments = LCS.regValue breakpointValues
+                         }
+  void $ liftIO $ SB.surveyorState sconf ng simState (SC.SimBreakpoint bp)
 
 -- TODO: export in crux
 lookupString :: (LCB.IsSymInterface sym, CLM.HasLLVMAnn sym, CLO.ArchOk arch)

diff --git a/surveyor-brick/src/Surveyor/Brick.hs b/surveyor-brick/src/Surveyor/Brick.hs
@@ -25,6 +25,7 @@ import           Control.Lens ( (&), (^.), (^?), (.~) )
 import qualified Control.Lens as L
 import           Control.Monad ( join )
 import qualified Data.Foldable as F
+import qualified Data.Map.Strict as Map
 import           Data.Maybe ( fromMaybe, mapMaybe, isJust )
 import qualified Data.Parameterized.Classes as PC
 import qualified Data.Parameterized.Map as MapF
@@ -99,8 +100,8 @@ drawDiagnostics diags = B.viewport DiagnosticView B.Vertical body
       case comp of
         C.Unspecified -> ""
         C.Loader -> "Loader" @? "log-component"
-        C.EventHandler nm -> PPT.renderStrict (PP.layoutCompact ("Event[" PP.<+> PP.pretty nm PP.<+> "]")) @? "log-component"
-        C.CommandCallback nm -> PPT.renderStrict (PP.layoutCompact ("Command[" PP.<+> PP.pretty nm PP.<+> "]")) @? "log-component"
+        C.EventHandler nm -> PPT.renderStrict (PP.layoutCompact ("Event[" <> PP.pretty nm <> "]")) @? "log-component"
+        C.CommandCallback nm -> PPT.renderStrict (PP.layoutCompact ("Command[" <> PP.pretty nm <> "]")) @? "log-component"
         C.EchoAreaUpdate -> ""
 
     renderTime tm = PPT.renderStrict (PP.layoutCompact (PP.pretty tm)) @? "log-time"
@@ -204,10 +205,14 @@ drawUIMode binFileName archState s uim =
       | otherwise -> drawAppShell s (B.txt (T.pack ("Missing function view for IR: " ++ show repr)))
     C.SemanticsViewer ->
       drawAppShell s (ISV.renderInstructionSemanticsViewer binfo (archState ^. C.contextG) ISV.instructionSemanticsViewer)
-    C.SymbolicExecutionManager -> do
-      let valNames = s ^. C.lValueNames
-      let sem = archState ^. BH.symbolicExecutionManagerG
-      drawAppShell s (SEM.renderSymbolicExecutionManager sem valNames)
+    C.SymbolicExecutionManager
+      | Just sessionID <- archState ^? C.contextL . C.currentContext . C.symExecSessionIDL
+      , Just sessions <- archState ^? C.symExStateL
+      , Just (Some symExState) <- C.lookupSessionState sessions sessionID
+      , Just manager <- archState ^. BH.symbolicExecutionStateG . L.at sessionID -> do
+          let valNames = s ^. C.lValueNames
+          drawAppShell s (SEM.renderSymbolicExecutionManager manager symExState valNames)
+      | otherwise -> drawAppShell s (B.txt (T.pack "No symbolic execution state"))
   where
     binfo = C.sAnalysisResult archState
 
@@ -346,8 +351,8 @@ stateFromContext ng mkAnalysisResult chan simState simData = do
                                        , SBE.sBlockViewers = MapF.fromList blockViewers
                                        , SBE.sFunctionViewer = MapF.fromList (funcViewers ares)
                                        , SBE.sFunctionSelector = FS.functionSelector (const (return ())) focusedListAttr []
-                                       , SBE.sSymbolicExecutionManager =
-                                         SEM.symbolicExecutionManager (Some symbolicExecutionState)
+                                       , SBE.sSymbolicExecutionState =
+                                         Map.singleton sesID (SEM.symbolicExecutionManager (Some symbolicExecutionState))
                                        }
         tc0 <- C.newTranslationCache
         ctxStk <- contextStackFromState ng tc0 ares sesID simState pfcfg
@@ -408,8 +413,8 @@ stateFromContext ng mkAnalysisResult chan simState simData = do
                                      , SBE.sBlockViewers = MapF.fromList blockViewers
                                      , SBE.sFunctionViewer = MapF.fromList (funcViewers ares)
                                      , SBE.sFunctionSelector = FS.functionSelector (const (return ())) focusedListAttr []
-                                     , SBE.sSymbolicExecutionManager =
-                                       SEM.symbolicExecutionManager (Some symbolicExecutionState)
+                                     , SBE.sSymbolicExecutionState =
+                                       Map.singleton sesID (SEM.symbolicExecutionManager (Some symbolicExecutionState))
                                      }
       let archState = C.ArchState { C.sAnalysisResult = ares
                                   -- FIXME: Pick a context based on the stack in the simulator

diff --git a/surveyor-brick/src/Surveyor/Brick/Extension.hs b/surveyor-brick/src/Surveyor/Brick/Extension.hs
@@ -25,14 +25,15 @@ module Surveyor.Brick.Extension (
   blockViewerG,
   functionViewersL,
   functionViewerG,
-  symbolicExecutionManagerL,
-  symbolicExecutionManagerG
+  symbolicExecutionStateL,
+  symbolicExecutionStateG
   ) where
 
 import           Control.Lens ( (^.), (&), (%~) )
 import qualified Control.Lens as L
 import qualified Control.NF as NF
 import           Data.Kind ( Type )
+import qualified Data.Map.Strict as Map
 import qualified Data.Parameterized.Map as MapF
 import qualified Data.Parameterized.Nonce as PN
 import qualified Data.Text as T
@@ -71,7 +72,7 @@ data BrickUIState arch s =
                , sBlockSelector :: !(BS.BlockSelector arch s)
                , sBlockViewers :: !(MapF.MapF (C.IRRepr arch) (BV.BlockViewer arch s))
                , sFunctionViewer :: !(MapF.MapF (C.IRRepr arch) (FV.FunctionViewer arch s))
-               , sSymbolicExecutionManager :: !(SEM.SymbolicExecutionManager (C.Events s (C.S BrickUIExtension BrickUIState)) arch s)
+               , sSymbolicExecutionState :: !(Map.Map (C.SessionID s) (SEM.SymbolicExecutionManager (C.Events s (C.S BrickUIExtension BrickUIState)) arch s))
                }
   deriving (Generic)
 
@@ -84,7 +85,7 @@ L.makeLensesFor
   , ("sBlockSelector", "blockSelectorL")
   , ("sBlockViewers", "blockViewersL")
   , ("sFunctionViewer", "functionViewersL")
-  , ("sSymbolicExecutionManager", "symbolicExecutionManagerL") ]
+  , ("sSymbolicExecutionState", "symbolicExecutionStateL") ]
   ''BrickUIState
 
 type instance C.EventExtension (C.S BrickUIExtension BrickUIState) = BrickUIEvent
@@ -135,5 +136,5 @@ blockViewerG rep = L.to (\as -> MapF.lookup rep (as ^. C.lUIState . blockViewers
 functionViewerG :: C.IRRepr arch ir -> L.Getter (C.ArchState BrickUIState arch s) (Maybe (FV.FunctionViewer arch s ir))
 functionViewerG rep = L.to (\as -> MapF.lookup rep (as ^. C.lUIState . functionViewersL))
 
-symbolicExecutionManagerG :: L.Getter (C.ArchState BrickUIState arch s) (SEM.SymbolicExecutionManager (C.Events s (C.S BrickUIExtension BrickUIState)) arch s)
-symbolicExecutionManagerG = L.to (^. C.lUIState . symbolicExecutionManagerL)
+symbolicExecutionStateG :: L.Getter (C.ArchState BrickUIState arch s) (Map.Map (C.SessionID s) (SEM.SymbolicExecutionManager (C.Events s (C.S BrickUIExtension BrickUIState)) arch s))
+symbolicExecutionStateG = L.to (^. C.lUIState . symbolicExecutionStateL)
diff --git a/surveyor-brick/src/Surveyor/Brick/Handlers.hs b/surveyor-brick/src/Surveyor/Brick/Handlers.hs
@@ -23,17 +23,19 @@ module Surveyor.Brick.Handlers (
   SBE.functionSelectorG,
   SBE.functionViewerG,
   SBE.minibufferG,
-  SBE.symbolicExecutionManagerG
+  SBE.symbolicExecutionStateG
   ) where
 
 import qualified Brick as B
 import           Control.Lens ( (&), (^.), (.~), (%~), (^?), _Just )
+import qualified Control.Lens as L
 import           Control.Monad.IO.Class ( liftIO )
 import qualified Control.NF as NF
 import qualified Data.Foldable as F
+import qualified Data.Map.Strict as Map
 import           Data.Parameterized.Classes
 import qualified Data.Parameterized.List as PL
-import           Data.Parameterized.Some ( viewSome )
+import           Data.Parameterized.Some ( Some(..) )
 import qualified Graphics.Vty as V
 
 import           Prelude
@@ -111,12 +113,13 @@ handleVtyEvent s0@(C.State s) evt
           let s' = s & C.lArchState . _Just . C.contextL .~ cstk'
           B.continue $! C.State s'
     C.SomeUIMode C.SymbolicExecutionManager
-      | Just archState <- s ^. C.lArchState -> do
-          let manager0 = archState ^. C.lUIState . SBE.symbolicExecutionManagerL
-          manager1 <- SEM.handleSymbolicExecutionManagerEvent (B.VtyEvent evt) manager0
-          let st1 = SEM.symbolicExecutionManagerState manager1
-          let s' = s & C.lArchState . _Just . C.lUIState . SBE.symbolicExecutionManagerL .~ manager1
-                     & C.lArchState . _Just . C.symExStateL %~ C.mergeSessionState (viewSome C.singleSessionState st1)
+      | Just archState <- s ^. C.lArchState
+      , Just sessionID <- archState ^? C.contextL . C.currentContext . C.symExecSessionIDL
+      , Just sessions <- archState ^? C.symExStateL
+      , Just (Some symExState) <- C.lookupSessionState sessions sessionID
+      , Just manager0 <- archState ^. C.lUIState . SBE.symbolicExecutionStateL . L.at sessionID -> do
+          manager1 <- SEM.handleSymbolicExecutionManagerEvent s (B.VtyEvent evt) manager0 symExState
+          let s' = s & C.lArchState . _Just . C.lUIState . SBE.symbolicExecutionStateL %~ Map.insert sessionID manager1
           B.continue $! C.State s'
     C.SomeUIMode _m -> B.continue s0
 
@@ -128,7 +131,12 @@ handleCustomEvent :: (C.Architecture arch s)
 handleCustomEvent s0 evt =
   case evt of
     C.LoadEvent le -> handleLoadEvent s0 le
-    C.SymbolicExecutionEvent se -> handleSymbolicExecutionEvent s0 se
+    C.SymbolicExecutionEvent se -> do
+      -- Delegate to the core handler, then add a hook to do any special
+      -- handling required to keep the UI in sync (using the brick UI specific
+      -- handler)
+      C.State s1 <- C.handleSymbolicExecutionEvent s0 se
+      handleSymbolicExecutionEvent s1 se
     C.LoggingEvent le -> do
       s1 <- C.handleLoggingEvent s0 le
       B.continue s1
@@ -138,6 +146,9 @@ handleCustomEvent s0 evt =
     C.ContextEvent ce -> do
       s1 <- C.handleContextEvent s0 ce
       B.continue s1
+    C.DebuggingEvent de -> do
+      s1 <- C.handleDebuggingEvent s0 de
+      B.continue s1
     C.ExtensionEvent ee -> handleExtensionEvent s0 ee
 
     -- We discard async state updates if the type of the state has changed in

diff --git a/surveyor-brick/src/Surveyor/Brick/Handlers/Load.hs b/surveyor-brick/src/Surveyor/Brick/Handlers/Load.hs
@@ -10,6 +10,7 @@ import qualified Brick as B
 import           Control.Lens ( (&), (^.), (.~), (%~), _Just )
 import           Control.Monad.IO.Class ( liftIO )
 import qualified Data.Foldable as F
+import qualified Data.Map.Strict as Map
 import qualified Data.Parameterized.Classes as PC
 import qualified Data.Parameterized.Map as MapF
 import           Data.Parameterized.Some ( Some(..) )
@@ -123,7 +124,7 @@ stateFromAnalysisResult s0 ares newDiags state uiMode = do
              defFunc : _ -> do
                let pushContext (newContext, sessState) oldState =
                      oldState & C.lArchState . _Just . C.contextL %~ C.pushContext newContext
-                              & C.lArchState . _Just . C.symExStateL %~ C.mergeSessionState sessState
+                              & C.lArchState . _Just . C.symExStateL %~ C.updateSessionState sessState
                C.asynchronously (C.archNonce ares) (C.sEmitEvent s0) pushContext $ do
                  case C.functionBlocks ares defFunc of
                    b0 : _ -> do
@@ -178,8 +179,8 @@ stateFromAnalysisResult s0 ares newDiags state uiMode = do
                                                        , SBE.sBlockViewers = MapF.fromList blockViewers
                                                        , SBE.sFunctionViewer = MapF.fromList funcViewers
                                                        , SBE.sFunctionSelector = FS.functionSelector (const (return ())) focusedListAttr []
-                                                       , SBE.sSymbolicExecutionManager =
-                                                         SEM.symbolicExecutionManager (Some (C.Configuring ses))
+                                                       , SBE.sSymbolicExecutionState =
+                                                         Map.singleton (ses ^. C.sessionID) (SEM.symbolicExecutionManager (Some (C.Configuring ses)))
                                                        }
                         return C.ArchState { C.sAnalysisResult = ares
                                            , C.sUIState = uiState