Merge pull request #1626 from GaloisInc/T1623

`cryptol-remote-api`: Check for valid evaluation contexts

cryptol-remote-api/CHANGELOG.md

@@ -1,5 +1,13 @@
 # Revision history for `cryptol-remote-api` and `cryptol-eval-server`
 
+## next -- TBA
+
+* Fix a bug in which the `check`, `prove or satisfy`, and `evaluate expression`
+  commands would fail to check the validity of the expression supplied as an
+  argument. Among other issues, this could cause the remote API to panic when
+  attempting to check an expression that depends on definitions from a
+  parameterized module.
+
 ## 3.1.0 -- 2024-02-05
 
 * The v3.1.0 release is made in tandem with the Cryptol 3.1.0 release. See the

cryptol-remote-api/docs/Errors.rst

@@ -129,7 +129,7 @@ Evaluation errors (``20200``–``20499``)
    where the JSON object for ``type`` is a
    :ref:`JSON Cryptol type <cryptol-json-type>`.
 -  ``20220``: “Can’t evaluate Cryptol in a parameterized module”
-   ``{ modules: [String] }``
+   ``{ "type parameters": [String], "definitions": [String] }``
 -  ``20230``: “Prover error” ``{ error: String }``
 
 Module errors (``20500``–``20699``)

cryptol-remote-api/python/tests/cryptol/test_cryptol_api.py

@@ -9,6 +9,7 @@
 from shutil import which
 import cryptol
 import argo_client.connection as argo
+from argo_client.interaction import ArgoException
 import cryptol.cryptoltypes
 from cryptol.single_connection import *
 from cryptol import solver
@@ -286,5 +287,27 @@ def test_tls_connection(self):
             x_val2 = cry_eval("Id::id x")
             self.assertEqual(x_val1, x_val2)
 
+
+class CryptolParamModTests(unittest.TestCase):
+
+    @classmethod
+    def setUpClass(self):
+        connect(verify=False)
+        load_file(str(Path('tests','cryptol','test-files', 'Param.cry')))
+
+    def test_param_mod(self):
+        with self.assertRaises(ArgoException) as res:
+            check('foo')
+        e = res.exception
+        self.assertEqual(e.data['type parameters'], [])
+        self.assertEqual(e.data['definitions'], ['Param::foo'])
+
+        with self.assertRaises(ArgoException) as res:
+            check('`(w)')
+        e = res.exception
+        self.assertEqual(e.data['type parameters'], ['Param::`parameter` interface of Param::w'])
+        self.assertEqual(e.data['definitions'], [])
+
+
 if __name__ == "__main__":
     unittest.main()

cryptol-remote-api/src/CryptolServer.hs

@@ -6,16 +6,19 @@
 module CryptolServer (module CryptolServer) where
 
 import Control.Lens
+import Control.Monad (unless)
 import Control.Monad.IO.Class
 import Control.Monad.Reader (ReaderT(ReaderT))
 import qualified Data.Aeson as JSON
 import Data.Containers.ListUtils (nubOrd)
+import qualified Data.Set as Set
 import Data.Text (Text)
 
 import Cryptol.Eval (EvalOpts(..))
+import Cryptol.IR.FreeVars (FreeVars)
 import Cryptol.ModuleSystem (ModuleCmd, ModuleEnv(..), ModuleInput(..))
 import Cryptol.ModuleSystem.Env
-  (getLoadedModules, lmFilePath, lmFileInfo, fiFingerprint,
+  (getLoadedModules, loadedParamModDeps, lmFilePath, lmFileInfo, fiFingerprint,
    initialModuleEnv, ModulePath(..))
 import Cryptol.ModuleSystem.Name (FreshM(..))
 import Cryptol.ModuleSystem.Fingerprint ( fingerprintFile )
@@ -25,7 +28,7 @@ import qualified Cryptol.TypeCheck.Solver.SMT as SMT
 
 import qualified Argo
 import qualified Argo.Doc as Doc
-import CryptolServer.Exceptions ( cryptolError )
+import CryptolServer.Exceptions ( cryptolError, evalInParamMod )
 import CryptolServer.Options
     ( WithOptions(WithOptions), Options(Options, optEvalOpts) )
 
@@ -110,6 +113,18 @@ liftModuleCmd cmd =
            do setModuleEnv newEnv
               return x
 
+-- | Is evaluation enabled? If the currently focused module is parameterized,
+-- then we cannot evaluate.
+--
+-- See also the 'validEvalContext' function in @Cryptol.REPL.Monad@, on which
+-- this function is based.
+validEvalContext :: FreeVars a => a -> CryptolCommand ()
+validEvalContext a =
+  do me <- getModuleEnv
+     let (badTs, bad) = loadedParamModDeps (meLoadedModules me) a
+     unless (Set.null bad && Set.null badTs) $
+       raise (evalInParamMod (Set.toList badTs) (Set.toList bad))
+
 data LoadedModule = LoadedModule
   { _loadedName :: Maybe ModName   -- ^ Working on this module.
   , _loadedPath :: FilePath        -- ^ Working on this file.

cryptol-remote-api/src/CryptolServer/Check.hs

@@ -37,6 +37,7 @@ import CryptolServer
     ( getTCSolver,
       getModuleEnv,
       liftModuleCmd,
+      validEvalContext,
       CryptolMethod(raise),
       CryptolCommand )
 import CryptolServer.AesonCompat (KeyCompat)
@@ -56,7 +57,8 @@ check :: CheckParams -> CryptolCommand CheckResult
 check (CheckParams jsonExpr cMode) =
   do e <- getExpr jsonExpr
      (_expr, ty, schema) <- liftModuleCmd (CM.checkExpr e)
-     -- TODO? validEvalContext expr, ty, schema
+     validEvalContext ty
+     validEvalContext schema
      s <- getTCSolver
      perhapsDef <- liftIO (defaultReplExpr s ty schema)
      case perhapsDef of

cryptol-remote-api/src/CryptolServer/EvalExpr.hs

@@ -42,9 +42,8 @@ evalExpression (EvalExprParams jsonExpr) =
 evalExpression' :: P.Expr P.PName -> CryptolCommand JSON.Value
 evalExpression' e = do
   (_expr, ty, schema) <- liftModuleCmd (checkExpr e)
-  -- TODO: see Cryptol REPL for how to check whether we
-  -- can actually evaluate things, which we can't do in
-  -- a parameterized module
+  validEvalContext ty
+  validEvalContext schema
   s <- getTCSolver
   perhapsDef <- liftIO (defaultReplExpr s ty schema)
   case perhapsDef of

cryptol-remote-api/src/CryptolServer/Exceptions.hs

@@ -81,11 +81,11 @@ cryptolError modErr warns =
         (20710, [ ("source", jsonPretty src)
                 , ("errors", jsonList (map jsonPretty errs))
                 ])
-      ExpandPropGuardsError src err ->
+      ExpandPropGuardsError src err' ->
         (20711, [ ("source", jsonPretty src)
-                , ("errors", jsonPretty err)
+                , ("errors", jsonPretty err')
                 ])
-        
+
       NoIncludeErrors src errs ->
         -- TODO: structured error here
         (20720, [ ("source", jsonPretty src)
@@ -171,11 +171,12 @@ unwantedDefaults defs =
       [ jsonTypeAndString ty <> fromListKM ["parameter" .= pretty param]
       | (param, ty) <- defs ] ]))
 
-evalInParamMod :: [CM.Name] -> JSONRPCException
-evalInParamMod mods =
+evalInParamMod :: [TC.TParam] -> [CM.Name] -> JSONRPCException
+evalInParamMod tyParams defs =
   makeJSONRPCException
     20220 "Can't evaluate Cryptol in a parameterized module."
-    (Just (JSON.object ["modules" .= map pretty mods]))
+    (Just (JSON.object ["type parameters" .= map pretty tyParams
+                       , "definitions" .= map pretty defs ]))
 
 evalPolyErr ::
   TC.Schema {- ^ the type that was too polymorphic -} ->

cryptol-remote-api/src/CryptolServer/Sat.hs

@@ -55,7 +55,8 @@ proveSat :: ProveSatParams -> CryptolCommand ProveSatResult
 proveSat (ProveSatParams queryType (ProverName proverName) jsonExpr hConsing) = do
   e <- getExpr jsonExpr
   (_expr, ty, schema) <- liftModuleCmd (checkExpr e)
-  -- TODO validEvalContext expr, ty, schema
+  validEvalContext ty
+  validEvalContext schema
   decls <- deDecls . meDynEnv <$> getModuleEnv
   s <- getTCSolver
   perhapsDef <- liftIO (defaultReplExpr s ty schema)

src/Cryptol/ModuleSystem/Env.hs

@@ -22,14 +22,16 @@ import Paths_cryptol (getDataDir)
 
 import Cryptol.Backend.FFI (ForeignSrc, unloadForeignSrc, getForeignSrcPath)
 import Cryptol.Eval (EvalEnv)
+import qualified Cryptol.IR.FreeVars as T
 import Cryptol.ModuleSystem.Fingerprint
 import Cryptol.ModuleSystem.Interface
-import Cryptol.ModuleSystem.Name (Name,Supply,emptySupply)
+import Cryptol.ModuleSystem.Name (Name,NameInfo(..),Supply,emptySupply,nameInfo)
 import qualified Cryptol.ModuleSystem.NamingEnv as R
 import Cryptol.Parser.AST
 import qualified Cryptol.TypeCheck as T
 import qualified Cryptol.TypeCheck.Interface as T
 import qualified Cryptol.TypeCheck.AST as T
+import qualified Cryptol.Utils.Ident as I
 import Cryptol.Utils.PP (PP(..),text,parens,NameDisp)
 
 import Data.ByteString(ByteString)
@@ -478,6 +480,30 @@ isLoadedParamMod mn ln = any ((mn ==) . lmName) (lmLoadedParamModules ln)
 isLoadedInterface :: ModName -> LoadedModules -> Bool
 isLoadedInterface mn ln = any ((mn ==) . lmName) (lmLoadedSignatures ln)
 
+-- | Return the set of type parameters (@'Set' 'T.TParam'@) and definitions
+-- (@'Set' 'Name'@) from the supplied 'LoadedModules' value that another
+-- definition (of type @a@) depends on.
+loadedParamModDeps ::
+  T.FreeVars a =>
+  LoadedModules ->
+  a ->
+  (Set T.TParam, Set Name)
+loadedParamModDeps lm a = (badTs, bad)
+  where
+    ds      = T.freeVars a
+    badVals = foldr badName Set.empty (T.valDeps ds)
+    bad     = foldr badName badVals (T.tyDeps ds)
+    badTs   = T.tyParams ds
+
+    badName nm bs =
+      case nameInfo nm of
+
+        -- XXX: Changes if focusing on nested modules
+        GlobalName _ I.OrigName { ogModule = I.TopModule m }
+          | isLoadedParamMod m lm -> Set.insert nm bs
+          | isLoadedInterface m lm -> Set.insert nm bs
+
+        _ -> bs
 
 
 lookupTCEntity :: ModName -> ModuleEnv -> Maybe (LoadedModuleG T.TCTopEntity)

src/Cryptol/REPL/Monad.hs

@@ -560,26 +560,12 @@ asBatch body = do
   modifyRW_ $ (\ rw -> rw { eIsBatch = wasBatch })
   return a
 
--- | Is evaluation enabled.  If the currently focused module is
--- parameterized, then we cannot evalute.
+-- | Is evaluation enabled? If the currently focused module is parameterized,
+-- then we cannot evaluate.
 validEvalContext :: T.FreeVars a => a -> REPL ()
 validEvalContext a =
   do me <- eModuleEnv <$> getRW
-     let ds      = T.freeVars a
-         badVals = foldr badName Set.empty (T.valDeps ds)
-         bad     = foldr badName badVals (T.tyDeps ds)
-         badTs   = T.tyParams ds
-
-         badName nm bs =
-           case M.nameInfo nm of
-
-             -- XXX: Changes if focusing on nested modules
-             M.GlobalName _ I.OrigName { ogModule = I.TopModule m }
-               | M.isLoadedParamMod m (M.meLoadedModules me) -> Set.insert nm bs
-               | M.isLoadedInterface m (M.meLoadedModules me) -> Set.insert nm bs
-
-             _ -> bs
-
+     let (badTs, bad) = M.loadedParamModDeps (M.meLoadedModules me) a
      unless (Set.null bad && Set.null badTs) $
        raise (EvalInParamModule (Set.toList badTs) (Set.toList bad))