diff --git a/saw-remote-api/python/README.md b/saw-remote-api/python/README.md index 2722590bcc..268403adb3 100644 --- a/saw-remote-api/python/README.md +++ b/saw-remote-api/python/README.md @@ -28,7 +28,7 @@ cd saw-remote-api/python E.g., here is how the docker image of the server might be used: ``` $ docker run --name=saw-remote-api -d \ - -v $PWD/tests/saw/test-files:/home/saw/tests/test-files \ + -v $PWD/tests/saw/test-files:/home/saw/tests/saw/test-files \ -p 8080:8080 \ galoisinc/saw-remote-api:nightly $ export SAW_SERVER_URL="http://localhost:8080/" diff --git a/saw-remote-api/src/SAWServer/CryptolExpression.hs b/saw-remote-api/src/SAWServer/CryptolExpression.hs index 5af4d95c19..b52b8e5f57 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 e3e20389fe..629a989b9c 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 @@ -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 index 37ad666367..b66bb8ac83 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, @@ -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 index 8121edd6f7..4d314abd29 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 res