diff --git a/.github/ci.sh b/.github/ci.sh index 0763894e..27647dc3 100755 --- a/.github/ci.sh +++ b/.github/ci.sh @@ -145,7 +145,7 @@ check_docs() { } test_rpc() { - cabal v2-test cryptol-remote-api + ./cry rpc-test } bundle_files() { diff --git a/.gitmodules b/.gitmodules index cbf4e6ef..6dc16ede 100644 --- a/.gitmodules +++ b/.gitmodules @@ -4,3 +4,6 @@ [submodule "deps/argo"] path = deps/argo url = https://github.com/galoisinc/argo +[submodule "cryptol-remote-api/test/galois-py-toolkit"] + path = cryptol-remote-api/test/galois-py-toolkit + url = https://github.com/GaloisInc/galois-py-toolkit.git diff --git a/cabal.project b/cabal.project index 996adafa..d8665fc9 100644 --- a/cabal.project +++ b/cabal.project @@ -3,5 +3,3 @@ packages: cryptol-remote-api tests deps/argo/argo - deps/argo/python - deps/argo/tasty-script-exitcode diff --git a/cry b/cry index 3fdcdb67..c5f410e7 100755 --- a/cry +++ b/cry @@ -20,6 +20,7 @@ Available commands: haddock Generate Haddock documentation test Run some tests (may take a while) quick-test Like "test" but run fewer tests by default + rpc-test Run RPC server tests exe-path Print the location of the local executable EOM } @@ -83,6 +84,16 @@ case $COMMAND in $TESTS ;; + rpc-test) + echo Running RPC server tests + DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )" + if [ ! -d "$DIR/cryptol-remote-api/test/galois-py-toolkit/tests" ]; then + git submodule update --init $DIR/cryptol-remote-api + fi + $DIR/cryptol-remote-api/test/run_rpc_tests.sh + ;; + + help) show_usage && exit 0 ;; exe-path) cabal v2-exec which cryptol ;; diff --git a/cryptol-remote-api/cryptol-eval-server/Main.hs b/cryptol-remote-api/cryptol-eval-server/Main.hs index f872996f..f53bb1c5 100644 --- a/cryptol-remote-api/cryptol-eval-server/Main.hs +++ b/cryptol-remote-api/cryptol-eval-server/Main.hs @@ -4,12 +4,19 @@ {-# LANGUAGE TypeApplications #-} module Main (main) where -import Control.Lens hiding (argument) +import Control.Lens ( view, set ) import System.Environment (lookupEnv) import System.Exit (exitFailure) import System.FilePath (splitSearchPath) import System.IO (hPutStrLn, stderr) import Options.Applicative + ( Parser, + Alternative((<|>)), + help, + long, + metavar, + strOption, + value ) import Cryptol.Eval (EvalOpts(..), defaultPPOpts) import Cryptol.ModuleSystem (ModuleInput(..), loadModuleByPath, loadModuleByName, meSolverConfig) @@ -19,24 +26,32 @@ import qualified Cryptol.TypeCheck.Solver.SMT as SMT import Cryptol.Utils.Ident (ModName, modNameToText, textToModName, preludeName) import Cryptol.Utils.Logger (quietLogger) -import Argo (MethodType(..), AppMethod, mkDefaultApp) -import Argo.DefaultMain +import Argo (AppMethod, mkApp, defaultAppOpts, StateMutability(PureState)) +import Argo.DefaultMain ( customMain, userOptions ) import qualified Argo.Doc as Doc import CryptolServer -import CryptolServer.Call + ( ServerState, moduleEnv, initialState, setSearchPath, command ) +import CryptolServer.Call ( call ) import CryptolServer.EvalExpr + ( evalExpressionDescr, evalExpression ) import CryptolServer.FocusedModule -import CryptolServer.Names -import CryptolServer.TypeCheck -import CryptolServer.Sat + ( focusedModuleDescr, focusedModule ) +import CryptolServer.Names ( visibleNamesDescr, visibleNames ) +import CryptolServer.TypeCheck ( checkType ) +import CryptolServer.Sat ( proveSatDescr, proveSat ) main :: IO () main = customMain initMod initMod initMod initMod description buildApp where buildApp opts = - mkDefaultApp "Cryptol RPC Server" evalServerDocs (startingState (userOptions opts)) cryptolEvalMethods + mkApp + "Cryptol RPC Server" + evalServerDocs + (defaultAppOpts PureState) + (startingState (userOptions opts)) + cryptolEvalMethods startingState (StartingFile file) reader = do paths <- getSearchPaths @@ -100,34 +115,28 @@ initMod = StartingFile <$> (Left <$> filename <|> Right . textToModName <$> modu cryptolEvalMethods :: [AppMethod ServerState] cryptolEvalMethods = - [ method + [ command "focused module" - Query focusedModuleDescr focusedModule - , method + , command "evaluate expression" - Query evalExpressionDescr evalExpression - , method + , command "call" - Query (Doc.Paragraph [Doc.Text "Evaluate the result of calling a Cryptol function on one or more parameters."]) call - , method + , command "visible names" - Query visibleNamesDescr visibleNames - , method + , command "check type" - Query (Doc.Paragraph [Doc.Text "Check and return the type of the given expression."]) checkType - , method + , command "prove or satisfy" - Query proveSatDescr proveSat ] diff --git a/cryptol-remote-api/cryptol-remote-api.cabal b/cryptol-remote-api/cryptol-remote-api.cabal index 3280b3cf..b18ef8d2 100644 --- a/cryptol-remote-api/cryptol-remote-api.cabal +++ b/cryptol-remote-api/cryptol-remote-api.cabal @@ -7,8 +7,7 @@ author: David Thrane Christiansen maintainer: dtc@galois.com category: Language extra-source-files: CHANGELOG.md -data-files: test-scripts/**/*.py - test-scripts/**/*.cry + common warnings ghc-options: diff --git a/cryptol-remote-api/cryptol-remote-api/Main.hs b/cryptol-remote-api/cryptol-remote-api/Main.hs index 12c4d2ec..69a54cd4 100644 --- a/cryptol-remote-api/cryptol-remote-api/Main.hs +++ b/cryptol-remote-api/cryptol-remote-api/Main.hs @@ -7,26 +7,35 @@ module Main (main) where import System.Environment (lookupEnv) import System.FilePath (splitSearchPath) -import Argo (MethodType(..), AppMethod, mkDefaultApp) -import Argo.DefaultMain +import Argo (AppMethod, mkApp, defaultAppOpts, StateMutability( PureState )) +import Argo.DefaultMain (defaultMain) import qualified Argo.Doc as Doc import CryptolServer -import CryptolServer.Call -import CryptolServer.ChangeDir + ( command, initialState, setSearchPath, ServerState ) +import CryptolServer.Call ( call, callDescr ) +import CryptolServer.ChangeDir ( cd, cdDescr ) import CryptolServer.EvalExpr + ( evalExpression, evalExpressionDescr ) import CryptolServer.FocusedModule + ( focusedModule, focusedModuleDescr ) import CryptolServer.LoadModule -import CryptolServer.Names -import CryptolServer.Sat -import CryptolServer.TypeCheck + ( loadFile, loadFileDescr, loadModule, loadModuleDescr ) +import CryptolServer.Names ( visibleNames, visibleNamesDescr ) +import CryptolServer.Sat ( proveSat, proveSatDescr ) +import CryptolServer.TypeCheck ( checkType, checkTypeDescr ) main :: IO () main = do paths <- getSearchPaths initSt <- setSearchPath paths <$> initialState - theApp <- mkDefaultApp "Cryptol RPC Server" serverDocs (const (pure initSt)) cryptolMethods + theApp <- mkApp + "Cryptol RPC Server" + serverDocs + (defaultAppOpts PureState) + (const (pure initSt)) + cryptolMethods defaultMain description theApp serverDocs :: [Doc.Block] @@ -46,49 +55,40 @@ getSearchPaths = cryptolMethods :: [AppMethod ServerState] cryptolMethods = - [ method + [ command "change directory" - Command cdDescr cd - , method + , command "load module" - Command loadModuleDescr loadModule - , method + , command "load file" - Command loadFileDescr loadFile - , method + , command "focused module" - Query focusedModuleDescr focusedModule - , method + , command "evaluate expression" - Query evalExpressionDescr evalExpression - , method + , command "call" - Query callDescr call - , method + , command "visible names" - Query visibleNamesDescr visibleNames - , method + , command "check type" - Query checkTypeDescr checkType - , method + , command "prove or satisfy" - Query proveSatDescr proveSat ] diff --git a/cryptol-remote-api/src/CryptolServer.hs b/cryptol-remote-api/src/CryptolServer.hs index 7e568ead..5113eb74 100644 --- a/cryptol-remote-api/src/CryptolServer.hs +++ b/cryptol-remote-api/src/CryptolServer.hs @@ -22,53 +22,72 @@ import qualified Cryptol.TypeCheck.Solver.SMT as SMT import qualified Argo import qualified Argo.Doc as Doc -import CryptolServer.Exceptions +import CryptolServer.Exceptions ( cryptolError ) import CryptolServer.Options + ( WithOptions(WithOptions), Options(Options, optEvalOpts) ) -newtype CryptolMethod a = CryptolMethod { runCryptolMethod :: Options -> Argo.Method ServerState a } - deriving (Functor, Applicative, Monad, MonadIO) via ReaderT Options (Argo.Method ServerState) +newtype CryptolCommand a = CryptolCommand { runCryptolCommand :: Options -> Argo.Command ServerState a } + deriving (Functor, Applicative, Monad, MonadIO) via ReaderT Options (Argo.Command ServerState) -method :: +newtype CryptolNotification a = CryptolNotification { runCryptolNotification :: Options -> Argo.Notification a } + deriving (Functor, Applicative, Monad, MonadIO) via ReaderT Options Argo.Notification + +command :: forall params result. (JSON.FromJSON params, JSON.ToJSON result, Doc.DescribedParams params) => Text -> - Argo.MethodType -> Doc.Block -> - (params -> CryptolMethod result) -> + (params -> CryptolCommand result) -> Argo.AppMethod ServerState -method name ty doc f = Argo.method name ty doc f' - where f' (WithOptions opts params) = runCryptolMethod (f params) opts +command name doc f = Argo.command name doc f' + where f' (WithOptions opts params) = runCryptolCommand (f params) opts -getOptions :: CryptolMethod Options -getOptions = CryptolMethod pure +notification :: + forall params. + (JSON.FromJSON params, Doc.DescribedParams params) => + Text -> + Doc.Block -> + (params -> CryptolNotification ()) -> + Argo.AppMethod ServerState +notification name doc f = Argo.notification name doc f' + where f' (WithOptions opts params) = runCryptolNotification (f params) opts -getEvalOpts :: CryptolMethod EvalOpts -getEvalOpts = optEvalOpts <$> getOptions +class CryptolMethod m where + getOptions :: m Options + getEvalOpts :: m EvalOpts + raise :: Argo.JSONRPCException -> m a -raise :: Argo.JSONRPCException -> CryptolMethod a -raise = CryptolMethod . const . Argo.raise +instance CryptolMethod CryptolCommand where + getOptions = CryptolCommand pure + getEvalOpts = optEvalOpts <$> getOptions + raise = CryptolCommand . const . Argo.raise -getModuleEnv :: CryptolMethod ModuleEnv -getModuleEnv = - CryptolMethod $ const $ view moduleEnv <$> Argo.getState +instance CryptolMethod CryptolNotification where + getOptions = CryptolNotification pure + getEvalOpts = optEvalOpts <$> getOptions + raise = CryptolNotification . const . Argo.raise -setModuleEnv :: ModuleEnv -> CryptolMethod () +getModuleEnv :: CryptolCommand ModuleEnv +getModuleEnv = CryptolCommand $ const $ view moduleEnv <$> Argo.getState + + +setModuleEnv :: ModuleEnv -> CryptolCommand () setModuleEnv me = - CryptolMethod $ const $ Argo.getState >>= \s -> Argo.setState (set moduleEnv me s) + CryptolCommand $ const $ Argo.getState >>= \s -> Argo.setState (set moduleEnv me s) -runModuleCmd :: ModuleCmd a -> CryptolMethod a +runModuleCmd :: ModuleCmd a -> CryptolCommand a runModuleCmd cmd = do Options callStacks evOpts <- getOptions - s <- CryptolMethod $ const Argo.getState - reader <- CryptolMethod $ const Argo.getFileReader + s <- CryptolCommand $ const Argo.getState + reader <- CryptolCommand $ const Argo.getFileReader let minp solver = ModuleInput - { minpCallStacks = callStacks - , minpEvalOpts = pure evOpts - , minpByteReader = reader - , minpModuleEnv = view moduleEnv s - , minpTCSolver = solver - } + { minpCallStacks = callStacks + , minpEvalOpts = pure evOpts + , minpByteReader = reader + , minpModuleEnv = view moduleEnv s + , minpTCSolver = solver + } let solverCfg = meSolverConfig (view moduleEnv s) out <- liftIO $ SMT.withSolver solverCfg (cmd . minp) case out of diff --git a/cryptol-remote-api/src/CryptolServer/Call.hs b/cryptol-remote-api/src/CryptolServer/Call.hs index b2d200ea..05826968 100644 --- a/cryptol-remote-api/src/CryptolServer/Call.hs +++ b/cryptol-remote-api/src/CryptolServer/Call.hs @@ -26,7 +26,7 @@ callDescr = Doc.Paragraph [Doc.Text "Evaluate the result of calling a Cryptol function on one or more parameters."] -call :: CallParams -> CryptolMethod JSON.Value +call :: CallParams -> CryptolCommand JSON.Value call (CallParams rawFun rawArgs) = do fun <- getExpr rawFun args <- traverse getExpr rawArgs diff --git a/cryptol-remote-api/src/CryptolServer/ChangeDir.hs b/cryptol-remote-api/src/CryptolServer/ChangeDir.hs index 6ff9adc8..1202f86f 100644 --- a/cryptol-remote-api/src/CryptolServer/ChangeDir.hs +++ b/cryptol-remote-api/src/CryptolServer/ChangeDir.hs @@ -18,7 +18,7 @@ cdDescr :: Doc.Block cdDescr = Doc.Paragraph [Doc.Text "Changes the server's working directory to the given path."] -cd :: ChangeDirectoryParams -> CryptolMethod () +cd :: ChangeDirectoryParams -> CryptolCommand () cd (ChangeDirectoryParams newDir) = do exists <- liftIO $ doesDirectoryExist newDir if exists diff --git a/cryptol-remote-api/src/CryptolServer/Data/Expression.hs b/cryptol-remote-api/src/CryptolServer/Data/Expression.hs index 8b9b2ba8..dc49f746 100644 --- a/cryptol-remote-api/src/CryptolServer/Data/Expression.hs +++ b/cryptol-remote-api/src/CryptolServer/Data/Expression.hs @@ -43,7 +43,7 @@ import Cryptol.Parser.Selector import Cryptol.Utils.Ident import Cryptol.Utils.RecordMap (recordFromFields, canonicalFields) - +import Argo import CryptolServer import CryptolServer.Exceptions import CryptolServer.Data.Type @@ -231,20 +231,20 @@ instance JSON.ToJSON Expression where toJSON gen -decode :: Encoding -> Text -> CryptolMethod Integer +decode :: (Argo.Method m, Monad m) => Encoding -> Text -> m Integer decode Base64 txt = let bytes = encodeUtf8 txt in case Base64.decode bytes of Left err -> - raise (invalidBase64 bytes err) + Argo.raise (invalidBase64 bytes err) Right decoded -> return $ bytesToInt decoded decode Hex txt = squish <$> traverse hexDigit (T.unpack txt) where squish = foldl (\acc i -> (acc * 16) + i) 0 -hexDigit :: Num a => Char -> CryptolMethod a +hexDigit :: (Argo.Method m, Monad m) => Num a => Char -> m a hexDigit '0' = pure 0 hexDigit '1' = pure 1 hexDigit '2' = pure 2 @@ -267,50 +267,54 @@ hexDigit 'e' = pure 14 hexDigit 'E' = pure 14 hexDigit 'f' = pure 15 hexDigit 'F' = pure 15 -hexDigit c = raise (invalidHex c) +hexDigit c = Argo.raise (invalidHex c) -getExpr :: Expression -> CryptolMethod (Expr PName) -getExpr Unit = +getExpr :: Expression -> CryptolCommand (Expr PName) +getExpr = CryptolCommand . const . getCryptolExpr + +-- N.B., used in SAWServer as well, hence the more generic monad +getCryptolExpr :: (Argo.Method m, Monad m) => Expression -> m (Expr PName) +getCryptolExpr Unit = return $ ETyped (ETuple []) (TTuple []) -getExpr (Bit b) = +getCryptolExpr (Bit b) = return $ ETyped (EVar (UnQual (mkIdent $ if b then "True" else "False"))) TBit -getExpr (Integer i) = +getCryptolExpr (Integer i) = return $ ETyped (ELit (ECNum i (DecLit (pack (show i))))) (TUser (UnQual (mkIdent "Integer")) []) -getExpr (IntegerModulo i n) = +getCryptolExpr (IntegerModulo i n) = return $ ETyped (ELit (ECNum i (DecLit (pack (show i))))) (TUser (UnQual (mkIdent "Z")) [TNum n]) -getExpr (Num enc txt w) = +getCryptolExpr (Num enc txt w) = do d <- decode enc txt return $ ETyped (ELit (ECNum d (DecLit txt))) (TSeq (TNum w) TBit) -getExpr (Record fields) = +getCryptolExpr (Record fields) = fmap (ERecord . recordFromFields) $ for (HM.toList fields) $ \(recName, spec) -> - (mkIdent recName,) . (emptyRange,) <$> getExpr spec -getExpr (Sequence elts) = - EList <$> traverse getExpr elts -getExpr (Tuple projs) = - ETuple <$> traverse getExpr projs -getExpr (Concrete syntax) = + (mkIdent recName,) . (emptyRange,) <$> getCryptolExpr spec +getCryptolExpr (Sequence elts) = + EList <$> traverse getCryptolExpr elts +getCryptolExpr (Tuple projs) = + ETuple <$> traverse getCryptolExpr projs +getCryptolExpr (Concrete syntax) = case parseExpr syntax of Left err -> - raise (cryptolParseErr syntax err) + Argo.raise (cryptolParseErr syntax err) Right e -> pure e -getExpr (Let binds body) = - EWhere <$> getExpr body <*> traverse mkBind binds +getCryptolExpr (Let binds body) = + EWhere <$> getCryptolExpr body <*> traverse mkBind binds where mkBind (LetBinding x rhs) = DBind . @@ -318,15 +322,15 @@ getExpr (Let binds body) = Bind (fakeLoc (UnQual (mkIdent x))) [] bindBody Nothing False Nothing [] True Nothing) . fakeLoc . DExpr <$> - getExpr rhs + getCryptolExpr rhs fakeLoc = Located emptyRange -getExpr (Application fun (arg :| [])) = - EApp <$> getExpr fun <*> getExpr arg -getExpr (Application fun (arg1 :| (arg : args))) = - getExpr (Application (Application fun (arg1 :| [])) (arg :| args)) -getExpr (TypeApplication gen (TypeArguments args)) = - EAppT <$> getExpr gen <*> pure (map inst (Map.toList args)) +getCryptolExpr (Application fun (arg :| [])) = + EApp <$> getCryptolExpr fun <*> getCryptolExpr arg +getCryptolExpr (Application fun (arg1 :| (arg : args))) = + getCryptolExpr (Application (Application fun (arg1 :| [])) (arg :| args)) +getCryptolExpr (TypeApplication gen (TypeArguments args)) = + EAppT <$> getCryptolExpr gen <*> pure (map inst (Map.toList args)) where inst (n, t) = NamedInst (Named (Located emptyRange n) (unJSONPType t)) @@ -391,7 +395,7 @@ readBack ty val = "'" -observe :: Eval a -> CryptolMethod a +observe :: Eval a -> CryptolCommand a observe e = liftIO (runEval mempty e) mkEApp :: Expr PName -> [Expr PName] -> Expr PName diff --git a/cryptol-remote-api/src/CryptolServer/EvalExpr.hs b/cryptol-remote-api/src/CryptolServer/EvalExpr.hs index e267a143..547c7aa4 100644 --- a/cryptol-remote-api/src/CryptolServer/EvalExpr.hs +++ b/cryptol-remote-api/src/CryptolServer/EvalExpr.hs @@ -32,12 +32,12 @@ evalExpressionDescr :: Doc.Block evalExpressionDescr = Doc.Paragraph [Doc.Text "Evaluate the Cryptol expression to a value."] -evalExpression :: EvalExprParams -> CryptolMethod JSON.Value +evalExpression :: EvalExprParams -> CryptolCommand JSON.Value evalExpression (EvalExprParams jsonExpr) = do e <- getExpr jsonExpr evalExpression' e -evalExpression' :: P.Expr PName -> CryptolMethod JSON.Value +evalExpression' :: P.Expr PName -> CryptolCommand JSON.Value evalExpression' e = do (_expr, ty, schema) <- runModuleCmd (checkExpr e) -- TODO: see Cryptol REPL for how to check whether we diff --git a/cryptol-remote-api/src/CryptolServer/FocusedModule.hs b/cryptol-remote-api/src/CryptolServer/FocusedModule.hs index 97d99a08..318468c7 100644 --- a/cryptol-remote-api/src/CryptolServer/FocusedModule.hs +++ b/cryptol-remote-api/src/CryptolServer/FocusedModule.hs @@ -19,7 +19,7 @@ focusedModuleDescr = Doc.Paragraph [Doc.Text "The 'current' module. Used to decide how to print names, for example."] -focusedModule :: FocusedModParams -> CryptolMethod JSON.Value +focusedModule :: FocusedModParams -> CryptolCommand JSON.Value focusedModule _ = do me <- getModuleEnv case meFocusedModule me of diff --git a/cryptol-remote-api/src/CryptolServer/LoadModule.hs b/cryptol-remote-api/src/CryptolServer/LoadModule.hs index a4d7c29c..7f924e59 100644 --- a/cryptol-remote-api/src/CryptolServer/LoadModule.hs +++ b/cryptol-remote-api/src/CryptolServer/LoadModule.hs @@ -23,7 +23,7 @@ import CryptolServer loadFileDescr :: Doc.Block loadFileDescr = Doc.Paragraph [Doc.Text "Load the specified module (by file path)."] -loadFile :: LoadFileParams -> CryptolMethod () +loadFile :: LoadFileParams -> CryptolCommand () loadFile (LoadFileParams fn) = void $ runModuleCmd (loadModuleByPath fn) @@ -47,7 +47,7 @@ instance Doc.DescribedParams LoadFileParams where loadModuleDescr :: Doc.Block loadModuleDescr = Doc.Paragraph [Doc.Text "Load the specified module (by name)."] -loadModule :: LoadModuleParams -> CryptolMethod () +loadModule :: LoadModuleParams -> CryptolCommand () loadModule (LoadModuleParams mn) = void $ runModuleCmd (loadModuleByName mn) diff --git a/cryptol-remote-api/src/CryptolServer/Names.hs b/cryptol-remote-api/src/CryptolServer/Names.hs index 1e640bc4..85b3aefe 100644 --- a/cryptol-remote-api/src/CryptolServer/Names.hs +++ b/cryptol-remote-api/src/CryptolServer/Names.hs @@ -36,7 +36,7 @@ visibleNamesDescr :: Doc.Block visibleNamesDescr = Doc.Paragraph [Doc.Text "List the currently visible (i.e., in scope) names."] -visibleNames :: VisibleNamesParams -> CryptolMethod [NameInfo] +visibleNames :: VisibleNamesParams -> CryptolCommand [NameInfo] visibleNames _ = do me <- getModuleEnv let DEnv { deNames = dyNames } = meDynEnv me diff --git a/cryptol-remote-api/src/CryptolServer/Sat.hs b/cryptol-remote-api/src/CryptolServer/Sat.hs index 9501ac95..c353cf3a 100644 --- a/cryptol-remote-api/src/CryptolServer/Sat.hs +++ b/cryptol-remote-api/src/CryptolServer/Sat.hs @@ -42,7 +42,7 @@ proveSatDescr = [ Doc.Text "Find a value which satisfies the given predicate, or show that it is valid." , Doc.Text "(i.e., find a value which when passed as the argument produces true or show that for all possible arguments the predicate will produce true)."] -proveSat :: ProveSatParams -> CryptolMethod ProveSatResult +proveSat :: ProveSatParams -> CryptolCommand ProveSatResult proveSat (ProveSatParams queryType (Prover name) jsonExpr) = do e <- getExpr jsonExpr (_expr, ty, schema) <- runModuleCmd (checkExpr e) @@ -83,7 +83,7 @@ proveSat (ProveSatParams queryType (Prover name) jsonExpr) = Satisfied <$> traverse satResult results where - satResult :: [(TValue, Expr, Value)] -> CryptolMethod [(JSONType, Expression)] + satResult :: [(TValue, Expr, Value)] -> CryptolCommand [(JSONType, Expression)] satResult es = traverse result es result (t, _, v) = diff --git a/cryptol-remote-api/src/CryptolServer/TypeCheck.hs b/cryptol-remote-api/src/CryptolServer/TypeCheck.hs index 9732011a..646d7c75 100644 --- a/cryptol-remote-api/src/CryptolServer/TypeCheck.hs +++ b/cryptol-remote-api/src/CryptolServer/TypeCheck.hs @@ -22,7 +22,7 @@ checkTypeDescr :: Doc.Block checkTypeDescr = Doc.Paragraph [Doc.Text "Check and return the type of the given expression."] -checkType :: TypeCheckParams -> CryptolMethod JSON.Value +checkType :: TypeCheckParams -> CryptolCommand JSON.Value checkType (TypeCheckParams e) = do e' <- getExpr e (_expr, _ty, schema) <- runModuleCmd (checkExpr e') diff --git a/cryptol-remote-api/test-scripts/Foo.cry b/cryptol-remote-api/test-scripts/Foo.cry deleted file mode 100644 index 2b047c45..00000000 --- a/cryptol-remote-api/test-scripts/Foo.cry +++ /dev/null @@ -1,54 +0,0 @@ -module Foo where - -import Id as Id - -id : {a} a -> a -id x = x - -x : [8] -x = 255 - -add : {a} (fin a) => [a] -> [a] -> [a] -add = (+) - -foo : {foo : [32], bar : [32]} -foo = {foo = 23, bar = 99} - -getFoo : {foo : [32], bar : [32]} -> [32] -getFoo x = x.foo - -op1 : {n} (fin n) => [n] -> [n + 1] -op1 a = 0 - -op2 : {n} (fin n) => [n] -> [n - n] -op2 a = 0 - -op3 : {n} (fin n) => [n] -> [n * 1] -op3 a = 0 - -op4 : {n} (fin n) => [n] -> [n / 1] -op4 a = 0 - -op5 : {n} (fin n) => [n] -> [n % 1] -op5 a = 0 - -op6 : {n} (fin n) => [n] -> [n ^^ 1] -op6 a = 0 - -op7 : {n} (fin n) => [n] -> [n /^ 1] -op7 a = 0 - -op8 : {n} (fin n) => [n] -> [width n] -op8 a = 0 - -op9 : {n} (fin n) => [n] -> [max n 1] -op9 a = 0 - -op10 : {n} (fin n) => [n] -> [min 1 n] -op10 a = 0 - -op11 : {n} (fin n) => [n] -> [lg2 n] -op11 a = 0 - -isSqrtOf9 : [8] -> Bit -isSqrtOf9 x = x*x == 9 \ No newline at end of file diff --git a/cryptol-remote-api/test-scripts/Id.cry b/cryptol-remote-api/test-scripts/Id.cry deleted file mode 100644 index 81bf39ea..00000000 --- a/cryptol-remote-api/test-scripts/Id.cry +++ /dev/null @@ -1,4 +0,0 @@ -module Id where - -id : {n} (fin n) => [n] -> [n] -id a = a diff --git a/cryptol-remote-api/test-scripts/Inst.cry b/cryptol-remote-api/test-scripts/Inst.cry deleted file mode 100644 index 3e726480..00000000 --- a/cryptol-remote-api/test-scripts/Inst.cry +++ /dev/null @@ -1,4 +0,0 @@ -module Inst = - Param where - type w = 8 - diff --git a/cryptol-remote-api/test-scripts/Param.cry b/cryptol-remote-api/test-scripts/Param.cry deleted file mode 100644 index 84619d7f..00000000 --- a/cryptol-remote-api/test-scripts/Param.cry +++ /dev/null @@ -1,8 +0,0 @@ -module Param where -parameter - type w : # - type constraint (fin w) - -foo : [w] -> [2 * w] -foo x = x # x - diff --git a/cryptol-remote-api/test-scripts/cryptol-api_test.py b/cryptol-remote-api/test-scripts/cryptol-api_test.py deleted file mode 100644 index 9b99e0a9..00000000 --- a/cryptol-remote-api/test-scripts/cryptol-api_test.py +++ /dev/null @@ -1,70 +0,0 @@ -import os -import unittest -from cryptol import CryptolConnection, CryptolContext, cry -import cryptol -import cryptol.cryptoltypes -from cryptol import solver -from cryptol.bitvector import BV -from BitVector import * - -dir_path = os.path.dirname(os.path.realpath(__file__)) - -c = cryptol.connect("cryptol-remote-api socket") - -c.change_directory(dir_path) - -c.load_file("Foo.cry") - -class CryptolTests(unittest.TestCase): - - def test_low_level(self): - x_val = c.evaluate_expression("x").result() - - self.assertEqual(c.evaluate_expression("Id::id x").result(), x_val) - self.assertEqual(c.call('Id::id', bytes.fromhex('ff')).result(), BV(8,255)) - - self.assertEqual(c.call('add', b'\0', b'\1').result(), BV(8,1)) - self.assertEqual(c.call('add', bytes.fromhex('ff'), bytes.fromhex('03')).result(), BV(8,2)) - - def test_module_import(self): - cryptol.add_cryptol_module('Foo', c) - from Foo import add - self.assertEqual(add(b'\2', 2), BV(8,4)) - - self.assertEqual(add(BitVector( intVal = 0, size = 8 ), BitVector( intVal = 1, size = 8 )), BV(8,1)) - self.assertEqual(add(BitVector( intVal = 1, size = 8 ), BitVector( intVal = 2, size = 8 )), BV(8,3)) - self.assertEqual(add(BitVector( intVal = 255, size = 8 ), BitVector( intVal = 1, size = 8 )), BV(8,0)) - self.assertEqual(add(BV(8,0), BV(8,1)), BV(8,1)) - self.assertEqual(add(BV(8,1), BV(8,2)), BV(8,3)) - self.assertEqual(add(BV(8,255), BV(8,1)), BV(8,0)) - - def test_sat(self): - # test a single sat model can be returned - rootsOf9 = c.sat('isSqrtOf9').result() - self.assertEqual(len(rootsOf9), 1) - self.assertTrue(int(rootsOf9[0]) ** 2 % 256, 9) - - # check we can specify the solver - rootsOf9 = c.sat('isSqrtOf9', solver = solver.ANY).result() - self.assertEqual(len(rootsOf9), 1) - self.assertTrue(int(rootsOf9[0]) ** 2 % 256, 9) - - # check we can ask for a specific number of results - rootsOf9 = c.sat('isSqrtOf9', count = 3).result() - self.assertEqual(len(rootsOf9), 3) - self.assertEqual([int(root) ** 2 % 256 for root in rootsOf9], [9,9,9]) - - # check we can ask for all results - rootsOf9 = c.sat('isSqrtOf9', count = None).result() - self.assertEqual(len(rootsOf9), 4) - self.assertEqual([int(root) ** 2 % 256 for root in rootsOf9], [9,9,9,9]) - - # check for an unsat condition - self.assertFalse(c.sat('\\x -> isSqrtOf9 x && ~(elem x [3,131,125,253])').result()) - - # check for a valid condition - self.assertTrue(c.prove('\\x -> isSqrtOf9 x ==> elem x [3,131,125,253]').result()) - - - -unittest.main() diff --git a/cryptol-remote-api/test-scripts/cryptol-tests.py b/cryptol-remote-api/test-scripts/cryptol-tests.py deleted file mode 100644 index 262cedb6..00000000 --- a/cryptol-remote-api/test-scripts/cryptol-tests.py +++ /dev/null @@ -1,245 +0,0 @@ -import os -from pathlib import Path -import signal -import subprocess -import sys -import time - -import argo.connection as argo -import cryptol -from cryptol import CryptolConnection, CryptolContext, cry - -dir_path = Path(os.path.dirname(os.path.realpath(__file__))) - -cryptol_path = dir_path.joinpath('test-data') - - - -def low_level_api_test(c): - - id_1 = c.send_command("load module", {"module name": "M", "state": None}) - reply_1 = c.wait_for_reply_to(id_1) - assert('result' in reply_1) - assert('state' in reply_1['result']) - assert('answer' in reply_1['result']) - state_1 = reply_1['result']['state'] - - id_2 = c.send_query("evaluate expression", {"expression": {"expression":"call","function":"f","arguments":[{"expression":"bits","encoding":"hex","data":"ff","width":8}]}, "state": state_1}) - reply_2 = c.wait_for_reply_to(id_2) - assert('result' in reply_2) - assert('answer' in reply_2['result']) - assert('value' in reply_2['result']['answer']) - assert(reply_2['result']['answer']['value'] == - {'data': [{'data': 'ff', 'width': 8, 'expression': 'bits', 'encoding': 'hex'}, - {'data': 'ff', 'width': 8, 'expression': 'bits', 'encoding': 'hex'}], - 'expression': 'sequence'}) - - id_3 = c.send_query("evaluate expression", {"expression": {"expression":"call","function":"g","arguments":[{"expression":"bits","encoding":"hex","data":"ff","width":8}]}, "state": state_1}) - reply_3 = c.wait_for_reply_to(id_3) - assert('result' in reply_3) - assert('answer' in reply_3['result']) - assert('value' in reply_3['result']['answer']) - assert(reply_3['result']['answer']['value'] == - {'data': [{'data': 'ff', 'width': 8, 'expression': 'bits', 'encoding': 'hex'}, - {'data': 'ff', 'width': 8, 'expression': 'bits', 'encoding': 'hex'}], - 'expression': 'sequence'}) - - id_4 = c.send_query("evaluate expression", {"expression":{"expression":"call","function":"h","arguments":[{"expression":"sequence","data":[{"expression":"bits","encoding":"hex","data":"ff","width":8},{"expression":"bits","encoding":"hex","data":"ff","width":8}]}]}, "state": state_1}) - reply_4 = c.wait_for_reply_to(id_4) - assert('result' in reply_4) - assert('answer' in reply_4['result']) - assert('value' in reply_4['result']['answer']) - assert(reply_4['result']['answer']['value'] == - {'data': [{'data': 'ff', 'width': 8, 'expression': 'bits', 'encoding': 'hex'}, - {'data': 'ff', 'width': 8, 'expression': 'bits', 'encoding': 'hex'}], - 'expression': 'sequence'}) - - a_record = {"expression": "record", - "data": {"unit": "()", - "fifteen": {"expression": "bits", - "encoding": "hex", - "width": 4, - "data": "f"}}} - - id_5 = c.send_query("evaluate expression", {"state": state_1, "expression": a_record}) - reply_5 = c.wait_for_reply_to(id_5) - assert('result' in reply_5) - assert('answer' in reply_5['result']) - assert('value' in reply_5['result']['answer']) - assert(reply_5['result']['answer']['value'] == - {'expression': 'record', - 'data': {'fifteen': - {'data': 'f', - 'width': 4, - 'expression': 'bits', - 'encoding': 'hex'}, - 'unit': - {'expression': 'unit'}}}) - - id_6 = c.send_query("evaluate expression", - {"state": state_1, - "expression": {"expression": "let", - "binders": [{"name": "theRecord", "definition": a_record}], - "body": {"expression": "tuple", - "data": [a_record, "theRecord"]}}}) - reply_6 = c.wait_for_reply_to(id_6) - assert('result' in reply_6) - assert('answer' in reply_6['result']) - assert('value' in reply_6['result']['answer']) - assert(reply_6['result']['answer']['value'] == - {'expression': 'tuple', - 'data': [{'data': {'fifteen': {'data': 'f', 'width': 4, 'expression': 'bits', 'encoding': 'hex'}, - 'unit': {'expression': 'unit'}}, - 'expression': 'record'}, - {'data': {'fifteen': {'data': 'f', 'width': 4, 'expression': 'bits', 'encoding': 'hex'}, - 'unit': {'expression': 'unit'}}, - 'expression': 'record'}]}) - - id_7 = c.send_query("evaluate expression", - {"state": state_1, - "expression": {"expression": "sequence", - "data": [a_record, a_record]}}) - reply_7 = c.wait_for_reply_to(id_7) - assert('result' in reply_7) - assert('answer' in reply_7['result']) - assert('value' in reply_7['result']['answer']) - assert(reply_7['result']['answer']['value'] == - {'expression': 'sequence', - 'data': [{'data': {'fifteen': {'data': 'f', 'width': 4, 'expression': 'bits', 'encoding': 'hex'}, - 'unit': {'expression': 'unit'}}, - 'expression': 'record'}, - {'data': {'fifteen': {'data': 'f', 'width': 4, 'expression': 'bits', 'encoding': 'hex'}, - 'unit': {'expression': 'unit'}}, - 'expression': 'record'}]}) - - id_8 = c.send_query("evaluate expression", - {"state": state_1, - "expression": {"expression": "integer modulo", - "integer": 14, - "modulus": 42}}) - reply_8 = c.wait_for_reply_to(id_8) - assert('result' in reply_8) - assert('answer' in reply_8['result']) - assert('value' in reply_8['result']['answer']) - assert(reply_8['result']['answer']['value'] == - {"expression": "integer modulo", - "integer": 14, - "modulus": 42}) - - id_9 = c.send_query("evaluate expression", - {"state": state_1, - "expression": "m `{a=60}"}) - reply_9 = c.wait_for_reply_to(id_9) - assert('result' in reply_9) - assert('answer' in reply_9['result']) - assert('value' in reply_9['result']['answer']) - assert(reply_9['result']['answer']['value'] == - {"expression": "integer modulo", - "integer": 42, - "modulus": 60}) - - - id_10 = c.send_query("evaluate expression", {"state": state_1, "expression": "two"}) - reply_10 = c.wait_for_reply_to(id_10) - assert('result' in reply_10) - assert('answer' in reply_10['result']) - assert('value' in reply_10['result']['answer']) - assert(reply_10['result']['answer']['value'] == {'data': '0002', 'width': 15, 'expression': 'bits', 'encoding': 'hex'}) - - id_11 = c.send_query("evaluate expression", {"state": state_1, "expression": "three"}) - reply_11 = c.wait_for_reply_to(id_11) - assert('result' in reply_11) - assert('answer' in reply_11['result']) - assert('value' in reply_11['result']['answer']) - assert(reply_11['result']['answer']['value'] == {'data': '0003', 'width': 16, 'expression': 'bits', 'encoding': 'hex'}) - - id_12 = c.send_query("evaluate expression", {"state": state_1, "expression": "four"}) - reply_12 = c.wait_for_reply_to(id_12) - assert('result' in reply_12) - assert('answer' in reply_12['result']) - assert('value' in reply_12['result']['answer']) - assert(reply_12['result']['answer']['value'] == {'data': '00004', 'width': 17, 'expression': 'bits', 'encoding': 'hex'}) - - # Test empty options - def test_options(options): - id_opt = c.send_query("evaluate expression", {"state": state_1, "expression": "four", "options": options}) - reply_opt = c.wait_for_reply_to(id_opt) - assert('result' in reply_opt) - assert('answer' in reply_opt['result']) - assert('value' in reply_opt['result']['answer']) - assert(reply_opt['result']['answer']['value'] == {'data': '00004', 'width': 17, 'expression': 'bits', 'encoding': 'hex'}) - - test_options(dict()) - test_options({"call stacks": True}) - test_options({"call stacks": False}) - test_options({"call stacks": False, "output": dict()}) - test_options({"call stacks": False, "output": {"ASCII": True}}) - test_options({"call stacks": False, "output": {"base": 16}}) - test_options({"call stacks": False, "output": {"prefix of infinite lengths": 3}}) - - def test_instantiation(t, expected=None): - if expected is None: expected = t - id_t = c.send_query("check type", {"state": state_1, "expression": {"expression": "instantiate", "generic": "id", "arguments": {"a": t}}}) - reply_t = c.wait_for_reply_to(id_t) - assert('result' in reply_t) - assert('answer' in reply_t['result']) - assert('type schema' in reply_t['result']['answer']) - assert(reply_t['result']['answer']['type schema']['type']['domain'] == expected) - - # These test both the type instantiation form and the serialization/deserialization of the types involved - test_instantiation({"type": "Integer"}) - test_instantiation({"type": "record", - "fields": {'a': {'type': 'Integer'}, - 'b': {'type': 'sequence', 'length': {'type': 'inf'}, 'contents': {'type': 'unit'}}}}) - test_instantiation({'type': 'sequence', - 'length': {'type': 'number', 'value': 42}, - 'contents': {'type': 'Rational'}}) - test_instantiation({'type': 'bitvector', - 'width': {'type': 'number', 'value': 432}}) - test_instantiation({'type': 'variable', - 'name': 'Word8'}, - {'type': 'bitvector', - 'width': {'type': 'number', 'value': 8}}) - test_instantiation({'type': 'variable', - 'name': 'Twenty', - 'arguments': [{'type': 'Z', 'modulus': {'type': 'number', 'value': 5}}]}, - { 'type': 'sequence', - 'length': {'value': 20, 'type': 'number'}, - 'contents': {'type': 'Z', 'modulus': {'value': 5, 'type': 'number'}}}) - - -# Test with both sockets and stdio - -c1 = argo.ServerConnection( - cryptol.CryptolDynamicSocketProcess( - "cryptol-remote-api socket", - cryptol_path=cryptol_path)) -c2 = argo.ServerConnection( - cryptol.CryptolStdIOProcess( - "cryptol-remote-api stdio", - cryptol_path=cryptol_path)) - -low_level_api_test(c1) -low_level_api_test(c2) - -env = os.environ.copy() -env['CRYPTOLPATH'] = cryptol_path - -p = subprocess.Popen( - ["cryptol-remote-api", "socket", "--port", "50005"], - stdout=subprocess.DEVNULL, - stdin=subprocess.DEVNULL, - stderr=subprocess.DEVNULL, - start_new_session=True, - env=env) - -time.sleep(5) -assert(p is not None) -assert(p.poll() is None) - -c3 = argo.ServerConnection( - argo.RemoteSocketProcess('localhost', 50005, ipv6=True)) - -low_level_api_test(c3) - -os.killpg(os.getpgid(p.pid), signal.SIGKILL) diff --git a/cryptol-remote-api/test-scripts/eval-server-test.py b/cryptol-remote-api/test-scripts/eval-server-test.py deleted file mode 100644 index 91911be0..00000000 --- a/cryptol-remote-api/test-scripts/eval-server-test.py +++ /dev/null @@ -1,47 +0,0 @@ -import os -from pathlib import Path -import signal -import subprocess -import time - -import argo.connection as argo -import cryptol - -dir_path = Path(os.path.dirname(os.path.realpath(__file__))) - -cryptol_path = dir_path.joinpath('test-data') - - -env = os.environ.copy() -env['CRYPTOLPATH'] = cryptol_path - -p = subprocess.Popen( - ["cabal", "v2-exec", "cryptol-eval-server", "--verbose=0", "--", "http", "/", "--port", "50005", "--module", "M"], - stdout=subprocess.PIPE, - stdin=subprocess.DEVNULL, - stderr=subprocess.PIPE, - start_new_session=True, - env=env) -time.sleep(5) -assert(p is not None) -poll_result = p.poll() -if poll_result is not None: - print(poll_result) - print(p.stdout.read()) - print(p.stderr.read()) -assert(poll_result is None) - -c = argo.ServerConnection(argo.HttpProcess('http://localhost:50005/')) - - -mid = c.send_query("evaluate expression", {"expression": {"expression":"call","function":"f","arguments":[{"expression":"bits","encoding":"hex","data":"ff","width":8}]}, "state": None}) -reply = c.wait_for_reply_to(mid) -assert('result' in reply) -assert('answer' in reply['result']) -assert('value' in reply['result']['answer']) -assert(reply['result']['answer']['value'] == - {'data': [{'data': 'ff', 'width': 8, 'expression': 'bits', 'encoding': 'hex'}, - {'data': 'ff', 'width': 8, 'expression': 'bits', 'encoding': 'hex'}], - 'expression': 'sequence'}) - -os.killpg(os.getpgid(p.pid), signal.SIGKILL) diff --git a/cryptol-remote-api/test-scripts/test-data/M.cry b/cryptol-remote-api/test-scripts/test-data/M.cry deleted file mode 100644 index fa72c30c..00000000 --- a/cryptol-remote-api/test-scripts/test-data/M.cry +++ /dev/null @@ -1,28 +0,0 @@ -module M where -f : [8] -> [2][8] -f x = repeat x - -g : [8] -> [2][8] -g x = [x, x] - -h : [2][8] -> [2][8] -h x = x - -m : {a} (fin a, a > 42) => Z a -m = 42 - - -two : [15] -two = 2 - -three : [16] -three = 3 - -four : [17] -four = 4 - -id : {a} a -> a -id x = x - -type Word8 = [8] -type Twenty a = [20]a diff --git a/cryptol-remote-api/test/Dockerfile b/cryptol-remote-api/test/Dockerfile deleted file mode 100644 index 91e385c6..00000000 --- a/cryptol-remote-api/test/Dockerfile +++ /dev/null @@ -1,8 +0,0 @@ -FROM python:3.7 -# Intended to be built from the root of the cryptol git repository - -COPY deps/argo argo -RUN pip3 install -r argo/python/requirements.txt -RUN pip3 install -e argo/python -COPY cryptol-remote-api/test/test-cryptol-remote-api.py /entrypoint.py -ENTRYPOINT ["python3", "/entrypoint.py"] diff --git a/cryptol-remote-api/test/Test.hs b/cryptol-remote-api/test/Test.hs deleted file mode 100644 index fac2a3d3..00000000 --- a/cryptol-remote-api/test/Test.hs +++ /dev/null @@ -1,87 +0,0 @@ -{-# LANGUAGE OverloadedStrings #-} -{-# LANGUAGE LambdaCase #-} -{-# LANGUAGE TypeApplications #-} -{-# LANGUAGE ScopedTypeVariables #-} -module Main (main) where - -import Data.Aeson as JSON (fromJSON, toJSON, Result(..)) - -import qualified Data.HashMap.Strict as HM -import Data.List.NonEmpty(NonEmpty(..)) -import System.Directory (findExecutable) - -import Test.QuickCheck.Instances.Text() -import Test.Tasty -import Test.Tasty.HUnit.ScriptExit -import Test.Tasty.HUnit -import Test.Tasty.QuickCheck - -import CryptolServer.Call - -import Argo.PythonBindings -import Paths_cryptol_remote_api - -exeExists :: FilePath -> IO FilePath -exeExists e = findExecutable e >>= - maybe (assertFailure $ e <> " executable not found") pure - -main :: IO () -main = - do reqs <- getArgoPythonFile "requirements.txt" - sequence_ [exeExists "z3", exeExists "cryptol-remote-api", exeExists "cryptol-eval-server"] - withPython3venv (Just reqs) $ \pip python -> - do pySrc <- getArgoPythonFile "." - testScriptsDir <- getDataFileName "test-scripts/" - pip ["install", pySrc] - putStrLn "pipped" - - scriptTests <- makeScriptTests testScriptsDir [python] - - defaultMain $ - testGroup "Tests for saw-remote-api" - [ testGroup "Scripting API tests" scriptTests - , callMsgProps - ] - -instance Arbitrary Encoding where - arbitrary = oneof [pure Hex, pure Base64] - -instance Arbitrary Expression where - arbitrary = sized spec - where - spec n - | n <= 0 = - oneof [ Bit <$> arbitrary - , pure Unit - , Num <$> arbitrary <*> arbitrary <*> arbitrary - , Integer <$> arbitrary - -- NB: The following case will not generate - -- syntactically valid Cryptol. But for testing - -- round-tripping of the JSON, and coverage of various - -- functions, it's better than nothing. - , Concrete <$> arbitrary - ] - | otherwise = - choose (2, n) >>= - \len -> - let sub = n `div` len - in - oneof [ Record . HM.fromList <$> vectorOf len ((,) <$> arbitrary <*> spec sub) - , Sequence <$> vectorOf len (spec sub) - , Tuple <$> vectorOf len (spec sub) - -- NB: Will not make valid identifiers, so if we - -- ever insert validation, then this will need to - -- change. - , Let <$> vectorOf len (LetBinding <$> arbitrary <*> spec sub) <*> spec sub - , Application <$> spec sub <*> ((:|) <$> spec sub <*> vectorOf len (spec sub)) - ] - -callMsgProps :: TestTree -callMsgProps = - testGroup "QuickCheck properties for the \"call\" message" - [ testProperty "encoding and decoding arg specs is the identity" $ - \(spec :: Expression) -> - case fromJSON (toJSON spec) of - JSON.Success v -> spec == v - JSON.Error _ -> False - ] diff --git a/cryptol-remote-api/test/galois-py-toolkit b/cryptol-remote-api/test/galois-py-toolkit new file mode 160000 index 00000000..08413dbd --- /dev/null +++ b/cryptol-remote-api/test/galois-py-toolkit @@ -0,0 +1 @@ +Subproject commit 08413dbd48fb601b45b398de73218b9de2b95985 diff --git a/cryptol-remote-api/test/run_rpc_tests.sh b/cryptol-remote-api/test/run_rpc_tests.sh new file mode 100755 index 00000000..54cbb802 --- /dev/null +++ b/cryptol-remote-api/test/run_rpc_tests.sh @@ -0,0 +1,44 @@ +#!/bin/bash + +DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )" + +if [ ! -d "$DIR/galois-py-toolkit/tests" ]; then + echo "ERROR: could not find the python test directory -- is the galois-py-toolkit submodule initialzed?" + exit 1 +fi + +pushd $DIR/galois-py-toolkit + +NUM_FAILS=0 + +echo "Setting up python environment for remote server clients..." +python3 -m venv virtenv +. virtenv/bin/activate +pip install -r requirements.txt + +export CRYPTOL_SERVER=$(cabal v2-exec which cryptol-remote-api) +echo "Running cryptol-remote-api tests..." +echo "Using server $CRYPTOL_SERVER" +python3 -m unittest discover tests/cryptol +if [ $? -ne 0 ]; then + NUM_FAILS=$(($NUM_FAILS+1)) +fi + +echo "Running cryptol-eval-server tests..." +export CRYPTOL_SERVER=$(cabal v2-exec which cryptol-eval-server) +echo "Using server $CRYPTOL_SERVER" +python3 -m unittest discover tests/cryptol_eval +if [ $? -ne 0 ]; then + NUM_FAILS=$(($NUM_FAILS+1)) +fi + +popd + +if [ $NUM_FAILS -eq 0 ] +then + echo "All RPC tests passed" + exit 0 +else + echo "Some RPC tests failed" + exit 1 +fi diff --git a/cryptol-remote-api/test/test-cryptol-remote-api.py b/cryptol-remote-api/test/test-cryptol-remote-api.py deleted file mode 100644 index 14972a7b..00000000 --- a/cryptol-remote-api/test/test-cryptol-remote-api.py +++ /dev/null @@ -1,17 +0,0 @@ -import sys -import argo.connection as argo -import cryptol - -connType = sys.argv[1] -host = sys.argv[2] -port = int(sys.argv[3]) - -if connType == 'socket': - c = cryptol.connect(argo.RemoteSocketProcess(host, port=port, ipv6=False)) -elif connType == 'http': - c = cryptol.CryptolConnection(argo.ServerConnection(argo.HttpProcess(url="http://%s:%d/" % (host,port)))) -else: - raise Exception('specify socket or http for connection type') - -c.load_module('Cryptol') -assert c.evaluate_expression("1+1").result()['value'] == 2 diff --git a/deps/argo b/deps/argo index a1766950..371fb3ff 160000 --- a/deps/argo +++ b/deps/argo @@ -1 +1 @@ -Subproject commit a1766950a3ddbb23e4a8d4c6eedecaa385959347 +Subproject commit 371fb3ff98da581ea2a20d80b454ab62e98e5a45