fix inconsistent navigation state after making choice

src/Pate/TraceTree.hs

@@ -150,7 +150,7 @@
 import qualified Prettyprinter.Render.String as PP
 
 import qualified Data.Aeson as JSON
 import qualified Compat.Aeson as JSON
 import           Data.Parameterized.Classes
 import           Data.Parameterized.Some
 import           Data.Parameterized.SymbolRepr ( knownSymbol, symbolRepr, SomeSym(..), SymbolRepr )
@@ -161,7 +161,7 @@
 import Data.Set (Set)
 import GHC.IO (unsafePerformIO)
 import qualified Control.Concurrent as IO
 import qualified System.IO as IO
 import Data.Maybe (catMaybes)
 import Control.Concurrent (threadDelay)
 import Control.Monad.State.Strict (StateT (..), MonadState (..))
@@ -884,9 +884,6 @@
          , choicePick :: IO ()
          -- ^ executed by some interactive client to indicate
          -- this is the desired choice
-         -- FIXME: this needs to coordinate with the 'ChoiceHeader' to ensure
-         -- that 'choiceReady' will necessarily return 'True' once 
-         -- this function unblocks
          , choiceChosen :: IO Bool
          -- ^ returns True if this is the desired choice
          }

tools/pate-repl/Repl.hs

@@ -155,7 +155,22 @@ data ReplIOStore =
 data LoadOpts = LoadOpts { loadJSONMode :: Bool }
 
 newtype ReplM_ sym arch a = ReplM_ { unReplM :: (StateT (ReplState sym arch) IO a) }
-  deriving ( Functor, Applicative, Monad, MonadState (ReplState sym arch), IO.MonadIO )
+  deriving ( Functor, Applicative, Monad, MonadState (ReplState sym arch), IO.MonadIO)
+
+-- | Same as 'IO.liftIO' but ensures that the global 'ref' representing
+--   the current state is consistent with the state of 'ReplM'
+liftIO_State :: IO a -> ReplM sym arch a
+liftIO_State f = ReplM_ $ do
+    st <- get
+    ValidSymArchRepr{} <- return $ replValidRepr st
+    (IO.liftIO $ IO.readIORef ref) >>= \case
+      NoTreeLoaded -> fail "Inconsistent verifier state: no initial state"
+      SomeReplState tid _ ->  do
+        IO.liftIO $ IO.writeIORef ref (SomeReplState tid st)
+        a <- IO.liftIO f
+        (IO.liftIO $ IO.readIORef ref) >>= \case
+          SomeReplState _ st' -> put (unsafeCoerce st') >> return a
+          NoTreeLoaded -> fail "Inconsistent verifier state: lost state"
 
 type ReplM sym arch a = (PA.ValidArch arch, PS.ValidSym sym) => ReplM_ sym arch a
 
@@ -696,16 +711,9 @@ goto' idx = do
       Just (SomeChoice c) -> do
         IO.liftIO $ choicePick c
         (IO.liftIO $ IO.threadDelay 100)
-        let untilReady = do
-              headerReady <- choiceReady $ choiceHeader c
-              choiceReady <- choiceChosen c
-              if headerReady && choiceReady then
-                return ()
-              else IO.threadDelay 100 >> untilReady
-        IO.liftIO $ untilReady
         Some curNode <- currentNode
         top'
-        IO.liftIO $ wait
+        liftIO_State $ wait
         (Just <$> currentNode)
       Nothing -> do
         goto_node' nextNode
@@ -812,7 +820,7 @@ input' s = withCurrentNode $ \tr -> asInput tr >>= \case
     Nothing -> do
       IO.liftIO $ IO.threadDelay 100
       top'
-      IO.liftIO $ wait
+      liftIO_State $ wait
       return Nothing
     Just err -> return $ Just err
   Nothing -> return $ Just (InputChoiceError "Not an input prompt" [])