Merge pull request #1473 from GaloisInc/file-deps

File deps

CHANGES.md

@@ -34,6 +34,10 @@
   These affect random test generation,
   and help write reproducable Cryptol scripts.
 
+* Add `:file-deps` commnads ro the REPL and Python API.
+  It shows information about the source files and dependencies of
+  loaded modules.
+
 ## Bug fixes
 
 * Fix a bug in the What4 backend that could cause applications of `(@)` with

cryptol-remote-api/cryptol-remote-api.cabal

@@ -13,8 +13,8 @@ flag static
   description: Create a statically-linked binary
 
 flag NotThreaded
-  default: false
-  manual: true
+  default: False
+  manual: True
   description: Omit the -threaded ghc flag
 
 common warnings
@@ -80,6 +80,7 @@ library
     CryptolServer.Names
     CryptolServer.Sat
     CryptolServer.TypeCheck
+    CryptolServer.FileDeps
 
   other-modules:
     CryptolServer.AesonCompat

cryptol-remote-api/cryptol-remote-api/Main.hs

@@ -33,6 +33,7 @@ import CryptolServer.LoadModule
 import CryptolServer.Names ( visibleNames, visibleNamesDescr )
 import CryptolServer.Sat ( proveSat, proveSatDescr )
 import CryptolServer.TypeCheck ( checkType, checkTypeDescr )
+import CryptolServer.FileDeps( fileDeps, fileDepsDescr )
 
 main :: IO ()
 main =
@@ -91,6 +92,10 @@ cryptolMethods =
      "load file"
      loadFileDescr
      loadFile
+  , command
+     "file-deps"
+     fileDepsDescr
+     fileDeps
   , command
      "focused module"
      focusedModuleDescr

cryptol-remote-api/docs/Cryptol.rst

@@ -388,6 +388,50 @@ No return fields
 
 
 
+file-deps (command)
+~~~~~~~~~~~~~~~~~~~
+
+Get information about the dependencies of a loaded top-level module. The dependencies include the dependencies of modules nested in this one.
+
+Parameter fields
+++++++++++++++++
+
+
+``module name``
+  Get information about this loaded module.
+
+
+
+Return fields
++++++++++++++
+
+
+``source``
+  File containing the module. For internal modules this is an object { internal: "LABEL" }.
+
+
+
+``fingerprint``
+  A hash of the module content.
+
+
+
+``includes``
+  Files included in this module.
+
+
+
+``imports``
+  Modules imported by this module.
+
+
+
+``foreign``
+  Foreign libraries loaded by this module.
+
+
+
+
 focused module (command)
 ~~~~~~~~~~~~~~~~~~~~~~~~
 

cryptol-remote-api/python/GettingStarted.md

@@ -0,0 +1,66 @@
+1. Run the Cryptol remote API server:
+
+       > cryptol-remote-api http /cryptol
+
+   This starts an HTTP server with the default settings, which means that
+   the server can be accessed at `http://localhost:8080/cryptol`
+
+
+2. Start a Python shell:
+
+       > poetry run python
+
+   This runs a Python shell within an environment set up by
+   [poetry](https://python-poetry.org/)
+
+
+3. Load the `cryptol` library:
+
+       >>> import cryptol
+
+4. Connect to the remote server:
+
+       >>> cry = cryptol.connect(url="http://localhost:8080/cryptol", reset_server=True)
+
+   The URL is the one where we started the server in step 1.
+   The second parameter resets the state of the server.
+   See `help("cryptol.connect")` for other options.
+   At this point, `cry` is an object that we can use to interact with Cryptol.
+
+5. Load the standard library:
+
+       >>> cry.load_module("Cryptol")
+
+   The `load_module` method is similar to the `:module` command of the
+   Cryptol REPL---it loads a module to the server's state.
+   The module `Cryptol` is the standard library for Cryptol.
+
+6. Evaluate an expression:
+
+       >>> it = cry.evaluate_expression("1+1")
+
+   This command sends the expression `1 + 1` to the server,
+   and the value `it` contains the response.   Use the `result` method
+   to get the result, if the expression was evaluated successfully:
+
+       >>> it.result()
+       2
+
+7. Get information about the functions and values loaded in the serer:
+
+       >>> names = cry.names().result()
+
+   The result is a list of all loaded names.  Here is an example of getting
+   information about the first name that was returned:
+
+       >>> first = names[0]
+       >>> first["name"]
+       '(!)'
+       >>> first["type string"]
+       '{n, a, ix} (fin n, Integral ix) => [n]a -> ix -> a'
+       >>> print(first["documentation"])
+       Reverse index operator.  The first argument is a finite sequence.  The second
+       argument is the zero-based index of the element to select, starting from the
+       end of the sequence.
+
+

cryptol-remote-api/python/README.md

@@ -180,7 +180,7 @@ Or a server URL can be specified directly in the script, e.g.:
 cryptol.connect(url=URL)
 ```
 
-where `URL` is a URL for a running Cryptol server in HTTP mode.
+There is a step-by-step example [here](GettingStarted.md).
 
 ## Running Cryptol Scripts from a clean server state
 

cryptol-remote-api/python/cryptol/commands.py

@@ -75,6 +75,13 @@ def __init__(self, connection : HasProtocolState, filename : str, timeout: Optio
     def process_result(self, res : Any) -> Any:
         return res
 
+class CryptolFileDeps(argo.Command):
+  def __init__(self, connection : HasProtocolState, mod_name : str, timeout: Optional[float]) -> None:
+    super(CryptolFileDeps, self).__init__('file-deps', {'module name': mod_name}, connection, timeout=timeout)
+
+  def process_result(self, res : Any) -> Any:
+      return res
+
 class CryptolExtendSearchPath(argo.Command):
     def __init__(self, connection : HasProtocolState, dirs : List[str], timeout: Optional[float]) -> None:
         super(CryptolExtendSearchPath, self).__init__('extend search path', {'paths': dirs}, connection, timeout=timeout)
@@ -83,6 +90,8 @@ def process_result(self, res : Any) -> Any:
         return res
 
 
+
+
 class CryptolEvalExprRaw(argo.Command):
     def __init__(self, connection : HasProtocolState, expr : Any, timeout: Optional[float]) -> None:
         super(CryptolEvalExprRaw, self).__init__(

cryptol-remote-api/python/cryptol/connection.py

@@ -213,6 +213,15 @@ def load_module(self, module_name : str, *, timeout:Optional[float] = None) -> a
         self.most_recent_result = CryptolLoadModule(self, module_name, timeout)
         return self.most_recent_result
 
+    def file_deps(self, module_name : str, *, timeout:Optional[float] = None) -> argo.Command:
+        """Get information about a loaded module.
+
+        :param timeout: Optional timeout for this request (in seconds).
+        """
+        timeout = timeout if timeout is not None else self.timeout
+        self.most_recent_result = CryptolFileDeps(self, module_name, timeout)
+        return self.most_recent_result
+
     def eval_raw(self, expression : Any, *, timeout:Optional[float] = None) -> argo.Command:
         """Like the member method ``eval``, but does not call
         ``from_cryptol_arg`` on the ``.result()``.

cryptol-remote-api/python/cryptol/single_connection.py

@@ -242,3 +242,9 @@ def interrupt() -> None:
 def logging(on : bool, *, dest : TextIO = sys.stderr) -> None:
     """Whether to log received and transmitted JSON."""
     __get_designated_connection().logging(on=on,dest=dest)
+
+def file_deps(m : str, timeout:Optional[float] = None) -> Any:
+    """Get information about a loaded module."""
+    return __get_designated_connection().file_deps(m,timeout=timeout)
+
+

cryptol-remote-api/python/cryptol/synchronous.py

@@ -379,3 +379,7 @@ def interrupt(self) -> None:
     def logging(self, on : bool, *, dest : TextIO = sys.stderr) -> None:
         """Whether to log received and transmitted JSON."""
         self.connection.server_connection.logging(on=on,dest=dest)
+
+    def file_deps(self, m : str, timeout:Optional[float] = None) -> Any:
+        """Get information about a loaded module."""
+        return self.connection.file_deps(m,timeout=timeout).result()

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

@@ -0,0 +1,19 @@
+import unittest
+from pathlib import Path
+import unittest
+import cryptol
+from cryptol.single_connection import *
+
+class TestFileDeps(unittest.TestCase):
+    def test_FileDeps(self):
+        connect(verify=False)
+        load_file(str(Path('tests','cryptol','test-files','Id.cry')))
+        result = file_deps('Id')
+        self.assertEqual(result['fingerprint'],"8A49C6A461AF276DF56C4FE4279BCFC51D891214")
+        self.assertEqual(result['foreign'],[])
+        self.assertEqual(result['imports'],['Cryptol'])
+        self.assertEqual(result['includes'],[])
+        # we don't check source because it is system dependent
+
+if __name__ == "__main__":
+    unittest.main()

cryptol-remote-api/src/CryptolServer.hs

@@ -15,7 +15,7 @@ import Data.Text (Text)
 import Cryptol.Eval (EvalOpts(..))
 import Cryptol.ModuleSystem (ModuleCmd, ModuleEnv(..), ModuleInput(..))
 import Cryptol.ModuleSystem.Env
-  (getLoadedModules, lmFilePath, lmFingerprint,
+  (getLoadedModules, lmFilePath, lmFileInfo, fiFingerprint,
    initialModuleEnv, ModulePath(..))
 import Cryptol.ModuleSystem.Name (FreshM(..))
 import Cryptol.ModuleSystem.Fingerprint ( fingerprintFile )
@@ -180,6 +180,6 @@ validateServerState =
         InMem{} -> continue
         InFile file ->
           do fp <- fingerprintFile file
-             if fp == Just (lmFingerprint lm)
+             if fp == Just (fiFingerprint (lmFileInfo lm))
                then continue
                else return False

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

@@ -10,12 +10,14 @@ module CryptolServer.Exceptions
   , proverError
   , cryptolParseErr
   , cryptolError
+  , moduleNotLoaded
   ) where
 
 import qualified Data.Aeson as JSON
 import qualified Data.Text as Text
 import qualified Data.Vector as Vector
 
+import Cryptol.Parser.AST(ModName)
 import Cryptol.ModuleSystem (ModuleError(..), ModuleWarning(..))
 import Cryptol.ModuleSystem.Name as CM
 import Cryptol.Utils.PP (pretty, PP)
@@ -206,3 +208,10 @@ jsonTypeAndString ty =
   fromListKM
     [ "type" .= JSONSchema (TC.Forall [] [] ty)
     , "type string" .= pretty ty ]
+
+moduleNotLoaded :: ModName -> JSONRPCException
+moduleNotLoaded m =
+  makeJSONRPCException
+    20100 "Module not loaded"
+    (Just (JSON.object ["error" .= show (pretty m)]))
+

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

@@ -0,0 +1,99 @@
+{-# Language BlockArguments #-}
+{-# Language OverloadedStrings #-}
+{-# Language MultiParamTypeClasses #-}
+module CryptolServer.FileDeps
+  ( fileDeps
+  , fileDepsDescr
+  ) where
+
+import Data.Text (Text)
+import qualified Data.Text as Text
+import qualified Data.Set as Set
+import Control.Monad.IO.Class(liftIO)
+import System.Directory(canonicalizePath)
+
+import qualified Data.Aeson as JSON
+import Data.Aeson (FromJSON(..),ToJSON(..),(.=),(.:))
+import qualified Argo.Doc as Doc
+
+import Cryptol.Parser.AST (ModName)
+import Cryptol.Parser (parseModName)
+import Cryptol.ModuleSystem.Env
+  (LoadedModuleG(..), FileInfo(..), lookupTCEntity, ModulePath(..))
+import Cryptol.ModuleSystem.Fingerprint(fingerprintHexString)
+import Cryptol.Utils.PP(pp)
+
+import CryptolServer
+import CryptolServer.Exceptions(moduleNotLoaded)
+
+data FileDepsParams = FileDepsOfModule ModName
+
+data FileDeps = FileDeps
+  { fdSource :: ModulePath
+  , fdInfo   :: FileInfo
+  }
+
+fileDeps :: FileDepsParams -> CryptolCommand FileDeps
+fileDeps (FileDepsOfModule m) =
+  do env <- getModuleEnv
+     case lookupTCEntity m env of
+       Nothing -> raise (moduleNotLoaded m)
+       Just lm ->
+         do src <- case lmFilePath lm of
+                     InFile f' -> InFile <$> liftIO (canonicalizePath f')
+                     InMem l x -> pure (InMem l x)
+            pure FileDeps { fdSource = src, fdInfo = lmFileInfo lm }
+
+
+fileDepsDescr :: Doc.Block
+fileDepsDescr =
+  txt [ "Get information about the dependencies of a loaded top-level module."
+      , " The dependencies include the dependencies of modules nested in this one."
+      ]
+
+txt :: [Text] -> Doc.Block
+txt xs = Doc.Paragraph (map Doc.Text xs)
+
+instance FromJSON FileDepsParams where
+  parseJSON =
+    JSON.withObject "params for \"file deps\"" $
+    \o -> do val <- o .: "module name"
+             JSON.withText
+                "module name"
+                (\str ->
+                    case parseModName (Text.unpack str) of
+                      Nothing -> mempty
+                      Just n  -> return (FileDepsOfModule n))
+                val
+
+instance ToJSON FileDeps where
+  toJSON fd =
+    JSON.object
+      [ "source"      .= case fdSource fd of
+                           InFile f  -> toJSON f
+                           InMem l _ -> JSON.object [ "internal" .= l ]
+      , "fingerprint" .= fingerprintHexString (fiFingerprint fi)
+      , "includes"    .= Set.toList (fiForeignDeps fi)
+      , "imports"     .= map (show . pp) (Set.toList (fiImportDeps fi))
+      , "foreign"     .= Set.toList (fiForeignDeps fi)
+      ]
+    where
+    fi = fdInfo fd
+
+
+instance Doc.DescribedMethod FileDepsParams FileDeps where
+  parameterFieldDescription =
+    [ ("module name", txt ["Get information about this loaded module."])
+    ]
+
+  resultFieldDescription =
+    [ ("source",      txt [ "File containing the module."
+                          , " For internal modules this is an object { internal: \"LABEL\" }."
+                          ])
+    , ("fingerprint", txt ["A hash of the module content."])
+    , ("includes",    txt ["Files included in this module."])
+    , ("imports",     txt ["Modules imported by this module."])
+    , ("foreign",     txt ["Foreign libraries loaded by this module."])
+    ]
+
+