Merge pull request #995 from GaloisInc/call-stack

Call stacks

CHANGES.md

@@ -1,3 +1,14 @@
+# NEXT
+
+## New features
+
+* By default, the interpreter will now track source locations of
+  expressions being evaluated, and retain call stack information.
+  This information is incorporated into error messages arising from
+  runtime errors. This additional bookkeeping incurs significant
+  runtime overhead, but may be disabled using the `--no-call-stacks`
+  command-line option.
+
 # 2.10.0
 
 ## Language changes

cryptol-remote-api/src/CryptolServer.hs

@@ -6,7 +6,7 @@ import Control.Lens
 import Control.Monad.IO.Class
 
 import Cryptol.Backend.Monad (EvalOpts(..), PPOpts(..), PPFloatFormat(..), PPFloatExp(..))
-import Cryptol.ModuleSystem (ModuleCmd, ModuleEnv)
+import Cryptol.ModuleSystem (ModuleCmd, ModuleEnv, ModuleInput(..))
 import Cryptol.ModuleSystem.Env
   (getLoadedModules, lmFilePath, lmFingerprint, meLoadedModules,
    initialModuleEnv, meSearchPath, ModulePath(..))
@@ -21,7 +21,13 @@ runModuleCmd :: ModuleCmd a -> Method ServerState a
 runModuleCmd cmd =
     do s <- getState
        reader <- getFileReader
-       out <- liftIO $ cmd (theEvalOpts, reader, view moduleEnv s)
+       let minp = ModuleInput
+                  { minpCallStacks = True -- TODO, where should we get this option from?
+                  , minpEvalOpts   = theEvalOpts
+                  , minpByteReader = reader
+                  , minpModuleEnv  = view moduleEnv s
+                  }
+       out <- liftIO $ cmd minp
        case out of
          (Left x, warns) ->
            raise (cryptolError x warns)

cryptol-remote-api/src/CryptolServer/Data/Expression.hs

@@ -348,6 +348,8 @@ readBack :: PrimMap -> TC.Type -> Value -> Eval Expression
 readBack prims ty val =
   let tbl = primTable theEvalOpts in
   let ?evalPrim = \i -> Right <$> Map.lookup i tbl in
+  let ?range = emptyRange in -- TODO?
+  let ?callStacks = False in -- TODO?
   case TC.tNoUser ty of
     TC.TRec tfs ->
       Record . HM.fromList <$>
@@ -399,7 +401,7 @@ readBack prims ty val =
 
 
 observe :: Eval a -> Method ServerState a
-observe e = liftIO (runEval e)
+observe e = liftIO (runEval mempty e)
 
 mkEApp :: Expr PName -> [Expr PName] -> Expr PName
 mkEApp f args = foldl EApp f args

cryptol.cabal

@@ -171,6 +171,7 @@ library
                        Cryptol.Eval.Concrete,
                        Cryptol.Eval.Env,
                        Cryptol.Eval.Generic,
+                       Cryptol.Eval.Prims,
                        Cryptol.Eval.Reference,
                        Cryptol.Eval.SBV,
                        Cryptol.Eval.Type,

cryptol/Main.hs

@@ -48,6 +48,7 @@ data Options = Options
   , optVersion         :: Bool
   , optHelp            :: Bool
   , optBatch           :: Maybe FilePath
+  , optCallStacks      :: Bool
   , optCommands        :: [String]
   , optColorMode       :: ColorMode
   , optCryptolrc       :: Cryptolrc
@@ -62,6 +63,7 @@ defaultOptions  = Options
   , optVersion         = False
   , optHelp            = False
   , optBatch           = Nothing
+  , optCallStacks      = True
   , optCommands        = []
   , optColorMode       = AutoColor
   , optCryptolrc       = CryrcDefault
@@ -95,6 +97,9 @@ options  =
   , Option "h" ["help"] (NoArg setHelp)
     "display this message"
 
+  , Option "" ["no-call-stacks"] (NoArg setNoCallStacks)
+    "Disable tracking of call stack information, which reduces interpreter overhead"
+
   , Option "" ["no-unicode-logo"] (NoArg setNoUnicodeLogo)
     "Don't use unicode characters in the REPL logo"
 
@@ -149,6 +154,10 @@ setHelp  = modify $ \ opts -> opts { optHelp = True }
 setCryrcDisabled :: OptParser Options
 setCryrcDisabled  = modify $ \ opts -> opts { optCryptolrc = CryrcDisabled }
 
+-- | Disable call stack tracking
+setNoCallStacks :: OptParser Options
+setNoCallStacks = modify $ \opts -> opts { optCallStacks = False }
+
 -- | Add another file to read as a @.cryptolrc@ file, unless @.cryptolrc@
 -- files have been disabled
 addCryrc :: String -> OptParser Options
@@ -206,6 +215,7 @@ main  = do
           (opts', mCleanup) <- setupCmdScript opts
           status <- repl (optCryptolrc opts')
                          (optBatch opts')
+                         (optCallStacks opts')
                          (optStopOnError opts')
                          (setupREPL opts')
           case mCleanup of

cryptol/REPL/Haskeline.hs

@@ -48,38 +48,38 @@ import           Prelude.Compat
 crySession :: Maybe FilePath -> Bool -> REPL CommandExitCode
 crySession mbBatch stopOnError =
   do settings <- io (setHistoryFile (replSettings isBatch))
-     let act = runInputTBehavior behavior settings (withInterrupt loop)
+     let act = runInputTBehavior behavior settings (withInterrupt (loop 1))
      if isBatch then asBatch act else act
   where
   (isBatch,behavior) = case mbBatch of
     Nothing   -> (False,defaultBehavior)
     Just path -> (True,useFile path)
 
-  loop :: InputT REPL CommandExitCode
-  loop =
+  loop :: Int -> InputT REPL CommandExitCode
+  loop lineNum =
     do ln <- getInputLines =<< MTL.lift getPrompt
        case ln of
          NoMoreLines -> return CommandOk
          Interrupted
            | isBatch && stopOnError -> return CommandError
-           | otherwise -> loop
-         NextLine line
-           | all isSpace line -> loop
-           | otherwise        -> doCommand line
-
-  doCommand txt =
-    case parseCommand findCommandExact txt of
-      Nothing | isBatch && stopOnError  -> return CommandError
-              | otherwise -> loop -- say somtething?
+           | otherwise -> loop lineNum
+         NextLine ls
+           | all (all isSpace) ls -> loop (lineNum + length ls)
+           | otherwise            -> doCommand lineNum ls
+
+  doCommand lineNum txt =
+    case parseCommand findCommandExact (unlines txt) of
+      Nothing | isBatch && stopOnError -> return CommandError
+              | otherwise -> loop (lineNum + length txt)  -- say somtething?
       Just cmd -> join $ MTL.lift $
-        do status <- handleInterrupt (handleCtrlC CommandError) (runCommand cmd)
+        do status <- handleInterrupt (handleCtrlC CommandError) (runCommand lineNum mbBatch cmd)
            case status of
              CommandError | isBatch && stopOnError -> return (return status)
              _ -> do goOn <- shouldContinue
-                     return (if goOn then loop else return status)
+                     return (if goOn then loop (lineNum + length txt) else return status)
 
 
-data NextLine = NextLine String | NoMoreLines | Interrupted
+data NextLine = NextLine [String] | NoMoreLines | Interrupted
 
 getInputLines :: String -> InputT REPL NextLine
 getInputLines = handleInterrupt (MTL.lift (handleCtrlC Interrupted)) . loop []
@@ -91,7 +91,7 @@ getInputLines = handleInterrupt (MTL.lift (handleCtrlC Interrupted)) . loop []
          Nothing -> return NoMoreLines
          Just l
            | not (null l) && last l == '\\' -> loop (init l : ls) newPropmpt
-           | otherwise -> return $ NextLine $ unlines $ reverse $ l : ls
+           | otherwise -> return $ NextLine $ reverse $ l : ls
 
 loadCryRC :: Cryptolrc -> REPL CommandExitCode
 loadCryRC cryrc =
@@ -116,9 +116,9 @@ loadCryRC cryrc =
                            _         -> return status
 
 -- | Haskeline-specific repl implementation.
-repl :: Cryptolrc -> Maybe FilePath -> Bool -> REPL () -> IO CommandExitCode
-repl cryrc mbBatch stopOnError begin =
-  runREPL (isJust mbBatch) stdoutLogger $
+repl :: Cryptolrc -> Maybe FilePath -> Bool -> Bool -> REPL () -> IO CommandExitCode
+repl cryrc mbBatch callStacks stopOnError begin =
+  runREPL (isJust mbBatch) callStacks stdoutLogger $
   do status <- loadCryRC cryrc
      case status of
        CommandOk -> begin >> crySession mbBatch stopOnError
@@ -201,7 +201,7 @@ canDisplayColor = io (hSupportsANSI stdout)
 cryptolCommand :: CompletionFunc REPL
 cryptolCommand cursor@(l,r)
   | ":" `isPrefixOf` l'
-  , Just (cmd,rest) <- splitCommand l' = case nub (findCommand cmd) of
+  , Just (_,cmd,rest) <- splitCommand l' = case nub (findCommand cmd) of
 
       [c] | null rest && not (any isSpace l') -> do
             return (l, cmdComp cmd c)

src/Cryptol/Backend.hs

@@ -35,31 +35,28 @@ import Data.Kind (Type)
 import Data.Ratio ( (%), numerator, denominator )
 
 import Cryptol.Backend.FloatHelpers (BF)
-import Cryptol.Backend.Monad ( PPOpts(..), EvalError(..) )
-import Cryptol.TypeCheck.AST(Name)
+import Cryptol.Backend.Monad
+  ( PPOpts(..), EvalError(..), CallStack, pushCallFrame )
+import Cryptol.ModuleSystem.Name(Name)
+import Cryptol.Parser.Position
 import Cryptol.Utils.PP
 
 
 invalidIndex :: Backend sym => sym -> Integer -> SEval sym a
-invalidIndex sym = raiseError sym . InvalidIndex . Just
+invalidIndex sym i = raiseError sym (InvalidIndex (Just i))
 
 cryUserError :: Backend sym => sym -> String -> SEval sym a
-cryUserError sym = raiseError sym . UserError
+cryUserError sym msg = raiseError sym (UserError msg)
 
 cryNoPrimError :: Backend sym => sym -> Name -> SEval sym a
-cryNoPrimError sym = raiseError sym . NoPrim
-
+cryNoPrimError sym nm = raiseError sym (NoPrim nm)
 
 {-# INLINE sDelay #-}
 -- | Delay the given evaluation computation, returning a thunk
 --   which will run the computation when forced.  Raise a loop
 --   error if the resulting thunk is forced during its own evaluation.
-sDelay :: Backend sym => sym -> Maybe String -> SEval sym a -> SEval sym (SEval sym a)
-sDelay sym msg m =
-  let msg'  = maybe "" ("while evaluating "++) msg
-      retry = raiseError sym (LoopError msg')
-   in sDelayFill sym m retry
-
+sDelay :: Backend sym => sym -> SEval sym a -> SEval sym (SEval sym a)
+sDelay sym m = sDelayFill sym m Nothing ""
 
 -- | Representation of rational numbers.
 --     Invariant: denominator is not 0
@@ -234,13 +231,27 @@ class MonadIO (SEval sym) => Backend sym where
   --   which will run the computation when forced.  Run the 'retry'
   --   computation instead if the resulting thunk is forced during
   --   its own evaluation.
-  sDelayFill :: sym -> SEval sym a -> SEval sym a -> SEval sym (SEval sym a)
+  sDelayFill :: sym -> SEval sym a -> Maybe (SEval sym a) -> String -> SEval sym (SEval sym a)
 
   -- | Begin evaluating the given computation eagerly in a separate thread
   --   and return a thunk which will await the completion of the given computation
   --   when forced.
   sSpark :: sym -> SEval sym a -> SEval sym (SEval sym a)
 
+  -- | Push a call frame on to the current call stack while evaluating the given action
+  sPushFrame :: sym -> Name -> Range -> SEval sym a -> SEval sym a
+  sPushFrame sym nm rng m = sModifyCallStack sym (pushCallFrame nm rng) m
+
+  -- | Use the given call stack while evaluating the given action
+  sWithCallStack :: sym -> CallStack -> SEval sym a -> SEval sym a
+  sWithCallStack sym stk m = sModifyCallStack sym (\_ -> stk) m
+
+  -- | Apply the given function to the current call stack while evaluating the given action
+  sModifyCallStack :: sym -> (CallStack -> CallStack) -> SEval sym a -> SEval sym a
+
+  -- | Retrieve the current evaluation call stack
+  sGetCallStack :: sym -> SEval sym CallStack
+
   -- | Merge the two given computations according to the predicate.
   mergeEval ::
      sym ->
@@ -257,7 +268,6 @@ class MonadIO (SEval sym) => Backend sym where
   -- | Indiciate that an error condition exists
   raiseError :: sym -> EvalError -> SEval sym a
 
-
   -- ==== Pretty printing  ====
   -- | Pretty-print an individual bit
   ppBit :: sym -> SBit sym -> Doc
@@ -674,7 +684,7 @@ class MonadIO (SEval sym) => Backend sym where
     SInteger sym ->
     SEval sym (SBit sym)
 
-  -- | Multiplicitive inverse in (Z n).
+  -- | Multiplicative inverse in (Z n).
   --   PRECONDITION: the modulus is a prime
   znRecip ::
     sym ->

src/Cryptol/Backend/Concrete.hs

@@ -136,10 +136,12 @@ instance Backend Concrete where
   type SFloat Concrete = FP.BF
   type SEval Concrete = Eval
 
-  raiseError _ err = io (X.throwIO err)
+  raiseError _ err =
+    do stk <- getCallStack
+       io (X.throwIO (EvalErrorEx stk err))
 
   assertSideCondition _ True _ = return ()
-  assertSideCondition _ False err = io (X.throwIO err)
+  assertSideCondition sym False err = raiseError sym err
 
   wordLen _ (BV w _) = w
   wordAsChar _ (BV _ x) = Just $! integerToChar x
@@ -160,6 +162,8 @@ instance Backend Concrete where
   sDeclareHole _ = blackhole
   sDelayFill _ = delayFill
   sSpark _ = evalSpark
+  sModifyCallStack _ f m = modifyCallStack f m
+  sGetCallStack _ = getCallStack
 
   ppBit _ b | b         = text "True"
             | otherwise = text "False"
@@ -393,6 +397,3 @@ fpRoundMode sym w =
     Right a  -> pure a
 
 
-
-
-