interpreter: add chewing gum for stack traces of do-blocks

This restores the stack trace compromised in the previous commit, at
the cost of making a small mess. This is its own commit in order to be
able to revert it easily later.

This works by stuffing a Maybe String into VDo, populating it from the
stack trace goop, and feeding it to a wrapper around interpretStmts.
As an instance of chewing gum, it could be worse...

Author: sauclovian-g

intTests/test_sawscript_builtins/fail2.log.good

@@ -1,5 +1,6 @@
  Loading file "fail2.saw"
  Stack trace:
+"f" (fail2.saw:5:1-5:2)
 "fail" (fail2.saw:4:17-4:21)
 requested failure
 

saw-central/src/SAWCentral/Value.hs

@@ -301,7 +301,11 @@ data Value
     -- | Returned value in unspecified monad
   | VReturn Value
     -- | Not-yet-executed do-block in unspecified monad
-  | VDo SS.Pos LocalEnv [SS.Stmt]
+    --
+    --   The string is a hack hook for the current implementation of
+    --   stack traces. See the commit message that added it for further
+    --   information. XXX: to be removed along with the stack trace code
+  | VDo SS.Pos (Maybe String) LocalEnv [SS.Stmt]
     -- | Single monadic bind in unspecified monad.
     --   This exists only to support the "for" builtin; see notes there
     --   for why this is so. XXX: remove it once that's no longer needed
@@ -476,7 +480,7 @@ showsPrecValue opts nenv p v =
     VTerm t -> showString (SAWCorePP.showTermWithNames opts nenv (ttTerm t))
     VType sig -> showString (pretty sig)
     VReturn v' -> showString "return " . showsPrecValue opts nenv (p + 1) v'
-    VDo pos _env stmts ->
+    VDo pos _name _env stmts ->
       let e = SS.Block pos stmts in
       shows (PP.pretty e)
     VBindOnce v1 v2 ->

saw-script/src/SAWScript/Interpreter.hs

@@ -425,10 +425,8 @@ withStackTraceFrame str val =
             withStackTraceFrame str `fmap` doProofScript m
       in
       VProofScript m'
-    VDo _pos _env _stmts ->
-      -- Blah. Let's just ignore it for now... XXX.
-      -- (but with luck we'll be able to throw this code out before anyone cares)
-      val
+    VDo pos _ env stmts ->
+      VDo pos (Just str) env stmts
     VBindOnce v1 v2 ->
       let v1' = withStackTraceFrame str v1
           v2' = withStackTraceFrame str v2
@@ -515,7 +513,7 @@ interpretExpr expr =
           VArray <$> traverse interpretExpr es
       SS.Block pos stmts -> do
           env <- getLocalEnv
-          return $ VDo pos env stmts
+          return $ VDo pos Nothing env stmts
       SS.Tuple _ es ->
           VTuple <$> traverse interpretExpr es
       SS.Record _ bs ->
@@ -622,8 +620,8 @@ interpretStmts stmts =
             -- (or whichever value for whichever monad)
             let v'' :: m Value = return v'
             return $ mkValue v''
-          VDo _blkpos env stmts' ->
-            withLocalEnvAny env (interpretStmts stmts')
+          VDo _blkpos mname env stmts' ->
+            withLocalEnvAny env (interpretStmts' mname stmts')              
           VBindOnce m1 v2 -> do
             v1 <- actionFromValue m1
             m2 <- liftTopLevel $ applyValue "Value in a VBindOnce, via force" v2 v1
@@ -689,6 +687,20 @@ interpretStmts stmts =
             let env' = LocalTypedef (getVal name) ty : env
             withLocalEnv env' (interpretStmts ss)
 
+-- Wrapper around interpretStmts for inserting a stack trace frame, in the
+-- old style. XXX remove along with the old stack trace code...
+interpretStmts' :: InterpreterMonad m => Maybe String -> [SS.Stmt] -> m Value
+interpretStmts' mname stmts = do
+  trace <- liftTopLevel $ gets rwStackTrace
+  case mname of
+    Nothing -> pure ()
+    Just name -> liftTopLevel $ modify (\rw -> rw { rwStackTrace = name : trace })
+  v <- interpretStmts stmts
+  case mname of
+    Nothing -> pure ()
+    Just _ -> liftTopLevel $ modify (\rw -> rw { rwStackTrace = trace })
+  return v
+
 -- Execute a top-level bind.
 processStmtBind ::
   InterpreterMonad m =>
@@ -1025,8 +1037,8 @@ instance IsValue a => IsValue (TopLevel a) where
 instance FromValue a => FromValue (TopLevel a) where
     fromValue (VTopLevel action) = fmap fromValue action
     fromValue (VReturn v) = return (fromValue v)
-    fromValue (VDo _pos env stmts) = do
-      v <- withLocalEnv env (interpretStmts stmts)
+    fromValue (VDo _pos mname env stmts) = do
+      v <- withLocalEnv env (interpretStmts' mname stmts)
       fromValue v
     fromValue (VBindOnce m1 v2) = do
       v1 <- fromValue m1
@@ -1044,8 +1056,8 @@ instance FromValue a => FromValue (ProofScript a) where
     --  the type system should keep this from happening.
     fromValue (VTopLevel m) = ProofScript (lift (lift (fmap fromValue m)))
     fromValue (VReturn v) = return (fromValue v)
-    fromValue (VDo _pos env stmts) = do
-      v <- withLocalEnvProof env (interpretStmts stmts)
+    fromValue (VDo _pos mname env stmts) = do
+      v <- withLocalEnvProof env (interpretStmts' mname stmts)
       fromValue v
     fromValue (VBindOnce m1 v2) = ProofScript $ do
       v1 <- unProofScript (fromValue m1)
@@ -1059,8 +1071,8 @@ instance IsValue a => IsValue (LLVMCrucibleSetupM a) where
 instance FromValue a => FromValue (LLVMCrucibleSetupM a) where
     fromValue (VLLVMCrucibleSetup m) = fmap fromValue m
     fromValue (VReturn v) = return (fromValue v)
-    fromValue (VDo _pos env stmts) = do
-      v <- withLocalEnvLLVM env (interpretStmts stmts)
+    fromValue (VDo _pos mname env stmts) = do
+      v <- withLocalEnvLLVM env (interpretStmts' mname stmts)
       fromValue v
     fromValue (VBindOnce m1 v2) = LLVMCrucibleSetupM $ do
       v1 <- runLLVMCrucibleSetupM (fromValue m1)
@@ -1074,8 +1086,8 @@ instance IsValue a => IsValue (JVMSetupM a) where
 instance FromValue a => FromValue (JVMSetupM a) where
     fromValue (VJVMSetup m) = fmap fromValue m
     fromValue (VReturn v) = return (fromValue v)
-    fromValue (VDo _pos env stmts) = do
-      v <- withLocalEnvJVM env (interpretStmts stmts)
+    fromValue (VDo _pos mname env stmts) = do
+      v <- withLocalEnvJVM env (interpretStmts' mname stmts)
       fromValue v
     fromValue (VBindOnce m1 v2) = JVMSetupM $ do
       v1 <- runJVMSetupM (fromValue m1)
@@ -1089,8 +1101,8 @@ instance IsValue a => IsValue (MIRSetupM a) where
 instance FromValue a => FromValue (MIRSetupM a) where
     fromValue (VMIRSetup m) = fmap fromValue m
     fromValue (VReturn v) = return (fromValue v)
-    fromValue (VDo _pos env stmts) = do
-      v <- withLocalEnvMIR env (interpretStmts stmts)
+    fromValue (VDo _pos mname env stmts) = do
+      v <- withLocalEnvMIR env (interpretStmts' mname stmts)
       fromValue v
     fromValue (VBindOnce m1 v2) = MIRSetupM $ do
       v1 <- runMIRSetupM (fromValue m1)