Add infrastructure for letting users specify names for values

Add the ability for users to name sub-terms in the `ValueViewer` widget. Users can select sub-terms and use a new contextual command to provide a name.  The TUI prompts the user via the minibuffer for the requested name.  The `ValueViewer` has been updated to render names next to relevant terms.

Currently, only terms with nonces can be named.

Fixes #59.  Begins addressing #57.

surveyor-brick/src/Brick/Widget/Minibuffer.hs

@@ -16,6 +16,7 @@ module Brick.Widget.Minibuffer (
   minibuffer,
   activeCompletionTarget,
   setCompletions,
+  invokeCommand,
   MinibufferStatus(..),
   handleMinibufferEvent,
   renderMinibuffer
@@ -184,16 +185,7 @@ handleMinibufferEvent evt customEventChan s mb@(Minibuffer { parseArgument = par
           -- the command immediately
           case FL.selectedItem (commandList mb) of
             Nothing -> return (Completed mb)
-            Just (C.SomeCommand (C.Command _ _ argNames argTypes callback _)) ->
-              case (argNames, argTypes) of
-                (PL.Nil, PL.Nil) -> do
-                  liftIO (callback customEventChan s PL.Nil)
-                  return (Executed (resetMinibuffer mb))
-                _ ->
-                  return $ Completed mb { state = CollectingArguments argNames argTypes PL.Nil PL.Nil argTypes callback
-                                        , commandList = FL.resetList (commandList mb)
-                                        , argumentList = FL.resetList (argumentList mb)
-                                        }
+            Just someCmd -> liftIO $ invokeCommand customEventChan s mb someCmd
         CollectingArguments expectedArgNames expectedArgTypes collectedArgTypes collectedArgValues callbackType callback ->
           case (expectedArgNames, expectedArgTypes) of
             (PL.Nil, PL.Nil) ->
@@ -265,6 +257,32 @@ handleMinibufferEvent evt customEventChan s mb@(Minibuffer { parseArgument = par
                                              , outstandingCompletion = Just (completionTarget, ac)
                                              }
 
+-- | Invoke a command in the minibuffer to let it prompt the user for arguments
+--
+-- This function is intended to allow non-minibuffer code to set the minibuffer
+-- into a state that will prompt users for command argument values.  This lets
+-- other code us the minibuffer as their UI.
+invokeCommand :: ( C.CommandLike b
+                 , ZG.GenericTextZipper t
+                 )
+              => C.Chan (C.EventType b)
+              -> C.StateType b
+              -> Minibuffer b t n
+              -> C.SomeCommand b
+              -> IO (MinibufferStatus b t n)
+invokeCommand customEventChan s mb (C.SomeCommand (C.Command _ _ argNames argTypes callback p))
+  | not (p s) = return (Canceled mb)
+  | otherwise =
+    case (argNames, argTypes) of
+      (PL.Nil, PL.Nil) -> do
+        callback customEventChan s PL.Nil
+        return (Executed (resetMinibuffer mb))
+      _ ->
+        return $ Completed mb { state = CollectingArguments argNames argTypes PL.Nil PL.Nil argTypes callback
+                              , commandList = FL.resetList (commandList mb)
+                              , argumentList = FL.resetList (argumentList mb)
+                              }
+
 setCompletions :: V.Vector t -> Minibuffer b t n -> Minibuffer b t n
 setCompletions comps mb =
   mb { argumentList = FL.updateList (const comps) (argumentList mb) }

surveyor-brick/src/Surveyor/Brick.hs

@@ -205,7 +205,9 @@ drawUIMode binFileName archState s uim =
     C.SemanticsViewer ->
       drawAppShell s (ISV.renderInstructionSemanticsViewer binfo (archState ^. C.contextG) ISV.instructionSemanticsViewer)
     C.SymbolicExecutionManager -> do
-      drawAppShell s (SEM.renderSymbolicExecutionManager (archState ^. BH.symbolicExecutionManagerG))
+      let valNames = s ^. C.lValueNames
+      let sem = archState ^. BH.symbolicExecutionManagerG
+      drawAppShell s (SEM.renderSymbolicExecutionManager sem valNames)
   where
     binfo = C.sAnalysisResult archState
 
@@ -293,6 +295,7 @@ emptyState mfp mloader ng customEventChan = do
              , C.sAppState = maybe C.AwaitingFile (const C.Loading) mfp
              , C.sEventChannel = customEventChan
              , C.sNonceGenerator = ng
+             , C.sValueNames = C.emptyValueNameMap
              , C.sKeymap = SBK.defaultKeymap Nothing
              , C.sUIExtension = uiExt
              , C.sArchState = Nothing
@@ -359,7 +362,7 @@ stateFromContext ng mkAnalysisResult chan simState bp = do
                                   }
       ctxStk <- contextStackFromState ng tc0 ares sesID simState fcfg
       -- NOTE: This can throw an exception, but that is fine: the TUI is not yet up
-      symbolicExecutionState <- C.suspendedState symSt simState (Just bp)
+      symbolicExecutionState <- C.suspendedState ng symSt simState (Just bp)
       let uiState = SBE.BrickUIState { SBE.sBlockSelector = BS.emptyBlockSelector
                                      , SBE.sBlockViewers = MapF.fromList blockViewers
                                      , SBE.sFunctionViewer = MapF.fromList funcViewers
@@ -390,6 +393,7 @@ stateFromContext ng mkAnalysisResult chan simState bp = do
                  , C.sArchNonce = n0
                  , C.sEventChannel = chan
                  , C.sUIExtension = uiExt
+                 , C.sValueNames = C.emptyValueNameMap
                  , C.sArchState = Just archState
                  , C.sUIMode = C.SomeUIMode C.SymbolicExecutionManager
                  }

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

@@ -20,13 +20,17 @@ module Surveyor.Brick.Command (
   extraCommands,
   findBlockC,
   listFunctionsC,
+  promptValueNameC,
   mkExtension
   ) where
 
+import           Control.Lens ( (^.), (^?), _Just )
 import qualified Data.Functor.Const as C
 import           Data.Kind ( Type )
+import           Data.Maybe ( isJust )
 import qualified Data.Parameterized.List as PL
 import qualified Data.Parameterized.Nonce as PN
+import           Data.Parameterized.Some ( Some(..) )
 import           Data.Proxy ( Proxy(..) )
 import qualified Data.Text as T
 
@@ -64,8 +68,24 @@ extraCommands = [ C.SomeCommand showMacawBlockC
                 , C.SomeCommand minibufferC
                 , C.SomeCommand findBlockC
                 , C.SomeCommand listFunctionsC
+                , C.SomeCommand promptValueNameC
                 ]
 
+promptValueNameC :: forall s st . (st ~ C.S SBE.BrickUIExtension SBE.BrickUIState) => Command s st '[]
+promptValueNameC =
+  C.Command "name-selected-value" doc PL.Nil PL.Nil callback hasCurrentValue
+  where
+    doc = "Prompt the user for the name to assign to the currently-selected value"
+    callback :: Callback s st '[]
+    callback = \customEventChan (C.getNonce -> C.SomeNonce archNonce) PL.Nil ->
+      C.emitEvent customEventChan (SBE.PromptValueName archNonce)
+    hasCurrentValue :: C.SomeState (C.S e u) s -> Bool
+    hasCurrentValue (C.SomeState st)
+      | Just sessionID <- st ^? C.lArchState . _Just . C.contextL . C.currentContext . C.symExecSessionIDL
+      , Just symExSt <- st ^? C.lArchState . _Just . C.symExStateL
+      , Just (Some (C.Suspended _symNonce suspSt)) <- C.lookupSessionState symExSt sessionID =
+          isJust (C.suspendedCurrentValue suspSt)
+      | otherwise = False
 
 
 listFunctionsC :: forall s st . (C.HasNonce st, st ~ C.S SBE.BrickUIExtension SBE.BrickUIState) => Command s st '[]

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

@@ -104,6 +104,8 @@ data BrickUIEvent s (st :: Type -> Type -> Type) where
   FindFunctionsContaining :: PN.Nonce s arch -> Maybe (C.Address arch s) -> BrickUIEvent s st
   FindBlockContaining :: PN.Nonce s arch -> C.Address arch s -> BrickUIEvent s st
 
+  PromptValueName :: PN.Nonce s arch -> BrickUIEvent s st
+
 instance C.ToEvent s (C.S BrickUIExtension BrickUIState) BrickUIEvent where
   toEvent = C.ExtensionEvent
 

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

@@ -117,7 +117,7 @@ handleVtyEvent s0@(C.State s) evt
           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 %~ (<> viewSome C.singleSessionState st1)
+                     & C.lArchState . _Just . C.symExStateL %~ (viewSome C.singleSessionState st1 <>)
           B.continue $! C.State s'
     C.SomeUIMode _m -> B.continue s0
 

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

@@ -14,6 +14,7 @@ import           Surveyor.Brick.Attributes ( focusedListAttr )
 import qualified Surveyor.Brick.Extension as SBE
 import qualified Surveyor.Brick.Widget.BlockSelector as BS
 import qualified Surveyor.Brick.Widget.FunctionSelector as FS
+import qualified Surveyor.Brick.Widget.Minibuffer as MB
 
 handleExtensionEvent :: (C.Architecture arch s)
                      => C.S SBE.BrickUIExtension SBE.BrickUIState arch s
@@ -93,3 +94,22 @@ handleExtensionEvent s0 evt =
                       & C.lArchState . _Just . C.lUIState . SBE.functionSelectorL .~ FS.functionSelector callback focusedListAttr funcs
           B.continue (C.State s1)
       | otherwise -> B.continue (C.State s0)
+
+    SBE.PromptValueName archNonce
+      | Just PC.Refl <- PC.testEquality archNonce (s0 ^. C.lNonce)
+      , C.SomeUIMode curMode <- s0 ^. C.lUIMode
+      , mb <- s0 ^. C.lUIExtension . SBE.minibufferG -> do
+          let chan = s0 ^. C.lEventChannel
+          mbs <- liftIO $ MB.invokeCommand chan (C.SomeState s0) mb (C.SomeCommand C.nameCurrentValueC)
+          case mbs of
+            MB.Canceled mb' -> do
+              let s1 = s0 & C.lUIExtension . SBE.minibufferL .~ mb'
+              B.continue $! C.State s1
+            MB.Completed mb' -> do
+              let s1 = s0 & C.lUIExtension . SBE.minibufferL .~ mb'
+                          & C.lUIMode .~ C.SomeMiniBuffer (C.MiniBuffer curMode)
+              B.continue $! C.State s1
+            MB.Executed mb' -> do
+              let s1 = s0 & C.lUIExtension . SBE.minibufferL .~ mb'
+              B.continue $! C.State s1
+      | otherwise -> B.continue (C.State s0)

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

@@ -150,6 +150,7 @@ stateFromAnalysisResult s0 ares newDiags state uiMode = do
              , C.sLoader = C.sLoader s0
              , C.sKeymap = keymap
              , C.sUIExtension = uiExt
+             , C.sValueNames = C.emptyValueNameMap
              , C.sArchNonce = C.archNonce ares
              , C.sArchState =
                case () of

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

@@ -8,8 +8,12 @@ import           Control.Monad.IO.Class ( liftIO )
 import qualified Control.NF as NF
 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           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
@@ -75,3 +79,28 @@ handleSymbolicExecutionEvent s0 evt =
     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)
+
+    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)

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

@@ -46,10 +46,11 @@ addModeKeys modeKeymap (mode, keys) =
   F.foldl' (\km (k, C.SomeCommand cmd) -> C.addModeKey mode k cmd km) modeKeymap keys
 
 -- | Mode-specific keys that do not have any dependency on the architecture
-modeKeys :: [(C.SomeUIMode s, [(C.Key, C.SomeCommand (C.SurveyorCommand s (C.S e u)))])]
+modeKeys :: [(C.SomeUIMode s, [(C.Key, C.SomeCommand (C.SurveyorCommand s (C.S SBE.BrickUIExtension SBE.BrickUIState)))])]
 modeKeys = [ (C.SomeUIMode C.SymbolicExecutionManager,
                   [ (C.Key (V.KChar 'c') [], C.SomeCommand C.beginSymbolicExecutionSetupC)
                   , (C.Key (V.KChar 's') [], C.SomeCommand C.startSymbolicExecutionC)
+                  , (C.Key (V.KChar 'n') [], C.SomeCommand SBC.promptValueNameC)
                   ])
            ]
 

surveyor-brick/src/Surveyor/Brick/Widget/Minibuffer.hs

@@ -3,6 +3,7 @@
 module Surveyor.Brick.Widget.Minibuffer (
   MB.Minibuffer,
   minibuffer,
+  MB.invokeCommand,
   MB.MinibufferStatus(..),
   MB.handleMinibufferEvent,
   MB.renderMinibuffer,
@@ -41,6 +42,7 @@ completeArgument cmds =
             let matches = V.filter (SW.matches matcher) cmdNames
             let toGeneric txt = mconcat (map Z.singleton (T.unpack txt))
             return (fmap toGeneric matches)
+      C.ValueNonceTypeRepr -> return V.empty
 
 completeFilename :: (Z.GenericTextZipper a) => a -> IO [FilePath]
 completeFilename t =

surveyor-brick/src/Surveyor/Brick/Widget/SymbolicExecution.hs

@@ -55,14 +55,15 @@ symbolicExecutionManager (Some state) =
     C.Suspended {} -> Suspended state (SEE.stateExplorer state)
 
 renderSymbolicExecutionManager :: SymbolicExecutionManager e arch s
+                               -> C.ValueNameMap s
                                -> B.Widget Names
-renderSymbolicExecutionManager sem =
+renderSymbolicExecutionManager sem valNames =
   case sem of
     Configuring _ form -> SEC.renderSymbolicExecutionConfigurator form
     Initializing st -> SES.renderSymbolicExecutionSetup st
     Executing st -> SEM.renderSymbolicExecutionMonitor st
     Inspecting st -> SEI.renderSymbolicExecutionInspector st
-    Suspended st form -> SEE.renderSymbolicExecutionStateExplorer (st, form)
+    Suspended st form -> SEE.renderSymbolicExecutionStateExplorer (st, form) valNames
 
 handleSymbolicExecutionManagerEvent :: B.BrickEvent Names e
                                     -> SymbolicExecutionManager e arch s