Poorly formatted VerificationError when cryptol("...") mentions an unbound variable #1128
Labels
subsystem: saw-remote-api
Issues related to the SAW server and its RPC bindings
Comments
|
Some further digging reveals that this is at least partially 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 |
|
After some experimentation, the following diff --git a/saw-remote-api/src/SAWServer/CryptolExpression.hs b/saw-remote-api/src/SAWServer/CryptolExpression.hs
index 5af4d95c..b52b8e5f 100644
--- a/saw-remote-api/src/SAWServer/CryptolExpression.hs
+++ b/saw-remote-api/src/SAWServer/CryptolExpression.hs
@@ -6,8 +6,10 @@ 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
@@ -15,7 +17,7 @@ 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
index 16e3121c..a71241dc 100644
--- 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
@@ -67,7 +68,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 )
@@ -179,24 +180,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
index 2d76b992..ced0f238 100644
--- 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,
@@ -72,7 +73,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 )
@@ -182,23 +183,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
index 8121edd6..4d314abd 100644
--- 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 resWith that patch, the error becomes: Perhaps there's a more elegant way to propagate the Cryptol module errors up to the top level, but I couldn't think of one. |
pnwamk
added
the
subsystem: saw-remote-api
mergify bot
added a commit
that referenced
this issue
May 19, 2021
Adapt to cryptol PR #1128 "persist-solver2"
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
I recently made a mistake when using the
cryptol()function in the following setup:The commented-out
# self.points_to(p, cryptol("{x} # {x}".format(x=x.name())), check_target_type = None)line is what I should have written, but I accidentally used the line above it instead. Unfortunately, the error message thatgalois-py-toolkitgives here doesn't make the mistake as obvious as it could be. To reproduce, run the following commands:Notice that a raw
VerificationErroris dumped to the screen unformatted. Compare this to the error that you'd experience in a similar SAWScript program:The text was updated successfully, but these errors were encountered: