Better printing of Cryptol errors in saw-remote-api

This improves the output of Cryptol-related errors in `saw-remote-api` slightly, which fixes #1128. There are still some remaining infelicities in how these errors are displayed, but this is a Cryptol-specific problem. The remaining work is being tracked at GaloisInc/cryptol#1106.
GaloisInc · Mar 15, 2021 · 06be727 · 06be727
1 parent 0e93b7a
commit 06be727
Show file tree

Hide file tree

Showing 4 changed files with 39 additions and 30 deletions.
diff --git a/saw-remote-api/src/SAWServer/CryptolExpression.hs b/saw-remote-api/src/SAWServer/CryptolExpression.hs
@@ -6,16 +6,18 @@ module SAWServer.CryptolExpression
  ( getCryptolExpr
  , getTypedTerm
  , getTypedTermOfCExp
+ , CryptolModuleException(..)
  ) where
 
+import Control.Exception (Exception)
 import Control.Lens ( view )
 import Control.Monad.IO.Class ( MonadIO(liftIO) )
 import qualified Data.ByteString as B
 import qualified Data.Map as Map
 import Data.Maybe (fromMaybe)
 
 import Cryptol.Eval (EvalOpts(..))
-import Cryptol.ModuleSystem (ModuleRes, ModuleInput(..))
+import Cryptol.ModuleSystem (ModuleError, ModuleInput(..), ModuleRes, ModuleWarning)
 import Cryptol.ModuleSystem.Base (genInferInput, getPrimMap, noPat, rename)
 import Cryptol.ModuleSystem.Env (ModuleEnv, meSolverConfig)
 import Cryptol.ModuleSystem.Interface (noIfaceParams)
@@ -108,3 +110,10 @@ runInferOutput out =
     InferFailed nm warns errs ->
       do typeCheckWarnings nm warns
          typeCheckingFailed nm errs
+
+data CryptolModuleException = CryptolModuleException
+  { cmeError    :: ModuleError
+  , cmeWarnings :: [ModuleWarning]
+  } deriving Show
+
+instance Exception CryptolModuleException
diff --git a/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs b/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs
@@ -13,6 +13,7 @@ module SAWServer.JVMCrucibleSetup
   , compileJVMContract
   ) where
 
+import Control.Exception (throw)
 import Control.Lens ( view )
 import Control.Monad.IO.Class ( MonadIO(liftIO) )
 import Control.Monad.State
@@ -66,7 +67,7 @@ import SAWServer.Data.Contract
                argumentVals, postVars, postConds, postAllocated, postPointsTos,
                returnVal) )
 import SAWServer.Data.SetupValue ()
-import SAWServer.CryptolExpression (getTypedTermOfCExp)
+import SAWServer.CryptolExpression (CryptolModuleException(..), getTypedTermOfCExp)
 import SAWServer.Exceptions ( notAtTopLevel )
 import SAWServer.OK ( OK, ok )
 import SAWServer.TopLevel ( tl )
@@ -178,24 +179,20 @@ interpretJVMSetup fileReader bic cenv0 ss = evalStateT (traverse_ go ss) (mempty
         Val x -> return x -- TODO add cases for the server values that
                           -- are not coming from the setup monad
                           -- (e.g. surrounding context)
-    getSetupVal (_, cenv) (CryptolExpr expr) = JVMSetupM $
-      do res <- liftIO $ getTypedTermOfCExp fileReader (biSharedContext bic) cenv expr
-         -- TODO: add warnings (snd res)
-         case fst res of
-           Right (t, _) -> return (MS.SetupTerm t)
-           Left err -> error $ "Cryptol error: " ++ show err -- TODO: report properly
+    getSetupVal env (CryptolExpr expr) =
+      do t <- getTypedTerm env expr
+         return (MS.SetupTerm t)
     getSetupVal _ _sv = error $ "unrecognized setup value" -- ++ show sv
 
     getTypedTerm ::
       (Map ServerName ServerSetupVal, CryptolEnv) ->
       P.Expr P.PName ->
       JVMSetupM TypedTerm
-    getTypedTerm (_, cenv) expr = JVMSetupM $
-      do res <- liftIO $ getTypedTermOfCExp fileReader (biSharedContext bic) cenv expr
-         -- TODO: add warnings (snd res)
-         case fst res of
-           Right (t, _) -> return t
-           Left err -> error $ "Cryptol error: " ++ show err -- TODO: report properly
+    getTypedTerm (_, cenv) expr = JVMSetupM $ liftIO $
+      do (res, warnings) <- getTypedTermOfCExp fileReader (biSharedContext bic) cenv expr
+         case res of
+           Right (t, _) -> return t -- TODO: Report warnings
+           Left err -> throw $ CryptolModuleException err warnings
 
     resolve env name =
        case Map.lookup name env of

diff --git a/saw-remote-api/src/SAWServer/LLVMCrucibleSetup.hs b/saw-remote-api/src/SAWServer/LLVMCrucibleSetup.hs
@@ -18,6 +18,7 @@ module SAWServer.LLVMCrucibleSetup
   , compileLLVMContract
   ) where
 
+import Control.Exception (throw)
 import Control.Lens ( view )
 import Control.Monad.State
     ( evalStateT,
@@ -71,7 +72,7 @@ import SAWServer.Data.Contract
     ( PointsTo(..), Allocated(..), ContractVar(..), Contract(..) )
 import SAWServer.Data.LLVMType (JSONLLVMType, llvmType)
 import SAWServer.Data.SetupValue ()
-import SAWServer.CryptolExpression (getTypedTermOfCExp)
+import SAWServer.CryptolExpression (CryptolModuleException(..), getTypedTermOfCExp)
 import SAWServer.Exceptions ( notAtTopLevel, cantLoadLLVMModule )
 import SAWServer.OK ( OK, ok )
 import SAWServer.TrackFile ( trackFile )
@@ -181,23 +182,19 @@ interpretLLVMSetup fileReader bic cenv0 ss =
         Val x -> return x -- TODO add cases for the named server values that
                           -- are not coming from the setup monad
                           -- (e.g. surrounding context)
-    getSetupVal (_, cenv) (CryptolExpr expr) = LLVMCrucibleSetupM $
-      do res <- liftIO $ getTypedTermOfCExp fileReader (biSharedContext bic) cenv expr
-         -- TODO: add warnings (snd res)
-         case fst res of
-           Right (t, _) -> return (CMS.anySetupTerm t)
-           Left err -> error $ "Cryptol error: " ++ show err -- TODO: report properly
+    getSetupVal env (CryptolExpr expr) =
+      do t <- getTypedTerm env expr
+         return (CMS.anySetupTerm t)
 
     getTypedTerm ::
       (Map ServerName ServerSetupVal, CryptolEnv) ->
       P.Expr P.PName ->
       LLVMCrucibleSetupM TypedTerm
-    getTypedTerm (_, cenv) expr = LLVMCrucibleSetupM $
-      do res <- liftIO $ getTypedTermOfCExp fileReader (biSharedContext bic) cenv expr
-         -- TODO: add warnings (snd res)
-         case fst res of
-           Right (t, _) -> return t
-           Left err -> error $ "Cryptol error: " ++ show err -- TODO: report properly
+    getTypedTerm (_, cenv) expr = LLVMCrucibleSetupM $ liftIO $
+      do (res, warnings) <- getTypedTermOfCExp fileReader (biSharedContext bic) cenv expr
+         case res of
+           Right (t, _) -> return t -- TODO: report warnings
+           Left err -> throw $ CryptolModuleException err warnings
 
     resolve env name =
        case Map.lookup name env of

diff --git a/saw-remote-api/src/SAWServer/TopLevel.hs b/saw-remote-api/src/SAWServer/TopLevel.hs
@@ -2,14 +2,17 @@
 {-# LANGUAGE ScopedTypeVariables #-}
 module SAWServer.TopLevel (tl) where
 
-import Control.Exception ( try, SomeException )
+import Control.Exception ( try, SomeException(..) )
 import Control.Lens ( view, set )
 import Control.Monad.State ( MonadIO(liftIO) )
+import Data.Typeable (cast)
 
 import SAWScript.Value ( TopLevel, runTopLevel )
 
 import qualified Argo
+import CryptolServer.Exceptions (cryptolError)
 import SAWServer ( SAWState, sawTopLevelRO, sawTopLevelRW )
+import SAWServer.CryptolExpression (CryptolModuleException(..))
 import SAWServer.Exceptions ( verificationException )
 
 tl :: TopLevel a -> Argo.Command SAWState a
@@ -19,8 +22,11 @@ tl act =
          rw = view sawTopLevelRW st
      liftIO (try (runTopLevel act ro rw)) >>=
        \case
-         Left (e :: SomeException) ->
-           Argo.raise (verificationException e)
+         Left e@(SomeException e')
+           |  Just (CryptolModuleException err warnings) <- cast e'
+           -> Argo.raise (cryptolError err warnings)
+           |  otherwise
+           -> Argo.raise (verificationException e)
          Right (res, rw') ->
            do Argo.modifyState $ set sawTopLevelRW rw'
               return res