Step execution from suspended state

surveyor-brick/src/Surveyor/Brick/Handlers.hs

@@ -138,6 +138,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

surveyor-core/src/Surveyor/Core.hs

@@ -181,6 +181,7 @@ module Surveyor.Core (
   HC.handleContextEvent,
   HI.handleInfoEvent,
   HL.handleLoggingEvent,
+  HD.handleDebuggingEvent,
   -- * Keymap
   K.Keymap,
   K.Key(..),
@@ -224,6 +225,7 @@ import qualified Surveyor.Core.Events as CE
 import qualified Surveyor.Core.Handlers.Context as HC
 import qualified Surveyor.Core.Handlers.Info as HI
 import qualified Surveyor.Core.Handlers.Logging as HL
+import qualified Surveyor.Core.Handlers.Debugging as HD
 import qualified Surveyor.Core.IRRepr as IR
 import qualified Surveyor.Core.Keymap as K
 import qualified Surveyor.Core.Loader as CL

surveyor-core/src/Surveyor/Core/Commands.hs

@@ -71,6 +71,7 @@ allCommands =
   , C.SomeCommand resetInstructionSelectionC
   , C.SomeCommand contextBackC
   , C.SomeCommand contextForwardC
+  , C.SomeCommand stepExecutionC
   , C.SomeCommand initializeSymbolicExecutionC
   , C.SomeCommand beginSymbolicExecutionSetupC
   , C.SomeCommand startSymbolicExecutionC
@@ -204,6 +205,16 @@ contextForwardC =
     callback = \customEventChan _ PL.Nil ->
       SCE.emitEvent customEventChan SCE.ContextForward
 
+stepExecutionC :: forall s st . Command s st '[]
+stepExecutionC =
+  C.Command "step-execution" doc PL.Nil PL.Nil callback (const True)
+  where
+    doc = "Step execution from the current breakpoint"
+    callback :: Callback s st '[]
+    callback = \customEventChan _ PL.Nil ->
+      SCE.emitEvent customEventChan SCE.StepExecution
+
+
 setLogFileC :: forall s st . Command s st '[AR.FilePathType]
 setLogFileC =
   C.Command "set-log-file" doc names rep callback (const True)

surveyor-core/src/Surveyor/Core/Events.hs

@@ -13,6 +13,7 @@ module Surveyor.Core.Events (
   InfoEvent(..),
   SymbolicExecutionEvent(..),
   ContextEvent(..),
+  DebuggingEvent(..),
   ToEvent(..),
   emitEvent
   ) where
@@ -131,6 +132,10 @@ data ContextEvent s st where
   SelectPreviousOperand :: PN.Nonce s (arch :: Type) -> ContextEvent s st
   ResetInstructionSelection :: PN.Nonce s (arch :: Type) -> ContextEvent s st
 
+-- | Events relating to the debugger
+data DebuggingEvent s st where
+  StepExecution :: DebuggingEvent s st
+
 type family EventExtension (st :: Type -> Type -> Type) :: Type -> (Type -> Type -> Type) -> Type
 
 -- | All of the events supported by Surveyor (with extensions for UI-specific events)
@@ -140,6 +145,7 @@ data Events s st where
   SymbolicExecutionEvent :: SymbolicExecutionEvent s st -> Events s st
   InfoEvent :: InfoEvent s st -> Events s st
   ContextEvent :: ContextEvent s st -> Events s st
+  DebuggingEvent :: DebuggingEvent s st -> Events s st
 
   -- | Apply an arbitrary state update based on some value that has been computed
   -- asynchronously (to avoid blocking the event loop with an expensive
@@ -163,6 +169,9 @@ instance ToEvent s st Events where
 instance ToEvent s st ContextEvent where
   toEvent = ContextEvent
 
+instance ToEvent s st DebuggingEvent where
+  toEvent = DebuggingEvent
+
 instance ToEvent s st LoggingEvent where
   toEvent = LoggingEvent
 

surveyor-core/src/Surveyor/Core/Handlers/Debugging.hs

@@ -0,0 +1,101 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+module Surveyor.Core.Handlers.Debugging ( handleDebuggingEvent ) where
+
+import           Control.Lens ( (^.), (^?), _Just, (&), (%~) )
+import           Control.Monad.IO.Class ( MonadIO, liftIO )
+import           Control.Monad.Reader ( runReaderT )
+import           Data.Parameterized.Some ( Some(..) )
+import qualified Data.BitVector.Sized as BV
+
+import qualified Lang.Crucible.Simulator.ExecutionTree as CSET
+import qualified Lang.Crucible.Simulator.EvalStmt as CSE
+import qualified Lang.Crucible.Simulator.RegMap as CSRM
+import qualified Lang.Crucible.Simulator.Operations as CSO
+import qualified Lang.Crucible.Simulator.CallFrame as CSCF
+import qualified Lang.Crucible.Types as CT
+import qualified Lang.Crucible.LLVM.MemModel as CLT
+import qualified What4.Interface as WI
+
+import qualified Surveyor.Core.Architecture as SCA
+import qualified Surveyor.Core.Events as SCE
+import qualified Surveyor.Core.State as SCS
+import qualified Surveyor.Core.Context as CCX
+import qualified Surveyor.Core.SymbolicExecution as SymEx
+
+handleDebuggingEvent :: (SCA.Architecture arch s, MonadIO m)
+                     => SCS.S e u arch s
+                     -> SCE.DebuggingEvent s (SCS.S e u)
+                     -> m (SCS.State e u s)
+handleDebuggingEvent s0 evt =
+  case evt of
+    SCE.StepExecution
+      | Just sessionID <- s0 ^? SCS.lArchState . _Just . SCS.contextL . CCX.currentContext . CCX.symExecSessionIDL
+      , Just symExSt <- s0 ^? SCS.lArchState . _Just . SCS.symExStateL
+      , Just (Some (SymEx.Suspended symNonce suspSt)) <- SymEx.lookupSessionState symExSt sessionID -> do
+          let st = SymEx.suspendedSymState suspSt
+          let sym = SymEx.symbolicBackend st
+          liftIO $! do
+              let simState0 = SymEx.suspendedSimState suspSt
+              let vff = simState0 ^. CSET.stateTree . CSET.actContext
+
+              case vff of
+                CSET.VFFEnd vfv@(CSET.VFVCall _ (CSCF.MF frm) (CSET.ReturnToCrucible rtp _)) -> do
+                  case rtp of
+                    CT.UnitRepr -> do
+                      let ret = CSRM.RegEntry CT.UnitRepr ()
+                      let cont = CSO.performReturn "debug_assert" vfv ret
+                      exst <- runReaderT cont simState0
+                      res <- CSE.singleStepCrucible 0 exst
+
+                      case CSET.execStateSimState res of
+                        Nothing -> error "Failed to execute crucible step"
+                        Just (CSET.SomeSimState simState1) -> do
+                          let topFrame = simState1 ^. CSET.stateTree . CSET.actFrame
+                          case topFrame ^. CSET.gpValue of
+                            CSCF.MF cf -> do
+                              let st' = SymEx.Suspended symNonce (suspSt { SymEx.suspendedSimState = simState1
+                                                                         , SymEx.suspendedCallFrame = cf })
+                              return $! SCS.State (s0 & SCS.lArchState . _Just . SCS.symExStateL
+                                                      %~ SymEx.mergeSessionState (SymEx.singleSessionState st'))
+
+                            _ -> error "Unexpected frame after stepping execution"
+
+                    CLT.LLVMPointerRepr w -> do
+                      blk0 <- WI.natLit sym 0
+                      bv0 <- WI.bvLit sym w (BV.mkBV w 32)
+                      let ptr = CLT.LLVMPointer blk0 bv0
+                      let ret = CSRM.RegEntry rtp ptr
+                      let cont = CSO.performReturn "debug_assert" vfv ret
+                      exst <- runReaderT cont simState0
+                      res <- CSE.singleStepCrucible 0 exst
+
+                      case CSET.execStateSimState res of
+                        Nothing -> error "Failed to execute crucible step"
+                        Just (CSET.SomeSimState simState1) -> do
+                          let topFrame = simState1 ^. CSET.stateTree . CSET.actFrame
+                          case topFrame ^. CSET.gpValue of
+                            CSCF.MF cf -> do
+                              let st' = SymEx.Suspended symNonce (suspSt { SymEx.suspendedSimState = simState1
+                                                                         , SymEx.suspendedCallFrame = cf })
+                              return $! SCS.State (s0 & SCS.lArchState . _Just . SCS.symExStateL
+                                                      %~ SymEx.mergeSessionState (SymEx.singleSessionState st'))
+
+                            _ -> error "Unexpected frame after stepping execution"
+
+                    _ ->
+                      case CSCF.frameHandle frm of
+                        CSCF.SomeHandle fh ->
+                          error $! "Unexpected frame: " ++ show fh ++ " return type: " ++ show rtp
+
+                CSET.VFFBranch {} ->
+                  error "Unexpected active frame: VFFBranch"
+                CSET.VFFPartial {} ->
+                  error "Unexpected active frame: VFFPartial"
+                CSET.VFFEnd {} ->
+                  error "Unexpected active frame: VFFEnd"
+
+      | otherwise -> return $! SCS.State s0

surveyor-core/src/Surveyor/Core/SymbolicExecution.hs

@@ -55,7 +55,8 @@ module Surveyor.Core.SymbolicExecution (
   -- * Simulation data
   SimulationData(..),
   breakpointP,
-  modelViewP
+  modelViewP,
+  setupProfiling
   ) where
 
 import           Control.DeepSeq ( NFData(..), deepseq )

surveyor-core/surveyor-core.cabal

@@ -35,6 +35,7 @@ library
                        Surveyor.Core.Handlers.Info
                        Surveyor.Core.Handlers.Logging
                        Surveyor.Core.Handlers.Context
+                       Surveyor.Core.Handlers.Debugging
                        Surveyor.Core.SymbolicExecution
                        Surveyor.Core.SymbolicExecution.Config
                        Surveyor.Core.SymbolicExecution.Session