Merge pull request #120 from GaloisInc/at-private-imports

Check types in context of private symbols
GaloisInc · Jan 19, 2021 · 30f26cd · 30f26cd
2 parents 13995d8 + 2ac0378
commit 30f26cd
Show file tree

Hide file tree

Showing 2 changed files with 24 additions and 10 deletions.
diff --git a/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs b/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs
@@ -10,7 +10,8 @@ Stability   : provisional
 {-# LANGUAGE ScopedTypeVariables #-}
 
 module Verifier.SAW.CryptolEnv
-  ( CryptolEnv(..)
+  ( ImportVisibility(..)
+  , CryptolEnv(..)
   , initCryptolEnv
   , loadCryptolModule
   , bindCryptolModule
@@ -105,8 +106,16 @@ data InputText = InputText
 
 --------------------------------------------------------------------------------
 
+-- | Should a given import result in all symbols being visible (as they
+-- are for focused modules in the Cryptol REPL) or only public symbols?
+-- Making all symbols visible is useful for verification and code
+-- generation.
+data ImportVisibility
+  = OnlyPublic
+  | PublicAndPrivate
+
 data CryptolEnv = CryptolEnv
-  { eImports    :: [P.Import]           -- ^ Declarations of imported Cryptol modules
+  { eImports    :: [(ImportVisibility, P.Import)]           -- ^ Declarations of imported Cryptol modules
   , eModuleEnv  :: ME.ModuleEnv         -- ^ Imported modules, and state for the ModuleM monad
   , eExtraNames :: MR.NamingEnv         -- ^ Context for the Cryptol renamer
   , eExtraTypes :: Map T.Name T.Schema  -- ^ Cryptol types for extra names in scope
@@ -195,8 +204,8 @@ initCryptolEnv sc = do
   termEnv <- genTermEnv sc modEnv cryEnv0
 
   return CryptolEnv
-    { eImports    = [P.Import preludeName Nothing Nothing
-                    ,P.Import preludeReferenceName (Just preludeReferenceName) Nothing
+    { eImports    = [ (OnlyPublic, P.Import preludeName Nothing Nothing)
+                    , (OnlyPublic, P.Import preludeReferenceName (Just preludeReferenceName) Nothing)
                     ]
     , eModuleEnv  = modEnv
     , eExtraNames = mempty
@@ -236,9 +245,13 @@ getNamingEnv :: CryptolEnv -> MR.NamingEnv
 getNamingEnv env = eExtraNames env `MR.shadowing` nameEnv
   where
     nameEnv = mconcat $ fromMaybe [] $ traverse loadImport (eImports env)
-    loadImport i = do
+    loadImport (vis, i) = do
       lm <- ME.lookupModule (T.iModule i) (eModuleEnv env)
-      return $ MN.interpImport i (MI.ifPublic (ME.lmInterface lm))
+      let ifc = ME.lmInterface lm
+          syms = case vis of
+                   OnlyPublic       -> MI.ifPublic ifc
+                   PublicAndPrivate -> MI.ifPublic ifc `mappend` M.ifPrivate ifc
+      return $ MN.interpImport i syms
 
 getAllIfaceDecls :: ME.ModuleEnv -> M.IfaceDecls
 getAllIfaceDecls me = mconcat (map (both . ME.lmInterface) (ME.getLoadedModules (ME.meLoadedModules me)))
@@ -384,9 +397,10 @@ importModule ::
   CryptolEnv                {- ^ Extend this environment -} ->
   Either FilePath P.ModName {- ^ Where to find the module -} ->
   Maybe P.ModName           {- ^ Name qualifier -} ->
+  ImportVisibility          {- ^ What visibility to give symbols from this module -} ->
   Maybe P.ImportSpec        {- ^ What to import -} ->
   IO CryptolEnv
-importModule sc env src as imps = do
+importModule sc env src as vis imps = do
   let modEnv = eModuleEnv env
   (m, modEnv') <-
     liftModuleM modEnv $
@@ -404,7 +418,7 @@ importModule sc env src as imps = do
   newCryEnv <- C.importTopLevelDeclGroups sc oldCryEnv newDeclGroups
   newTermEnv <- traverse (\(t, j) -> incVars sc 0 j t) (C.envE newCryEnv)
 
-  return env { eImports = P.Import (T.mName m) as imps : eImports env
+  return env { eImports = (vis, P.Import (T.mName m) as imps) : eImports env
              , eModuleEnv = modEnv'
              , eTermEnv = newTermEnv }
 

diff --git a/cryptol-saw-core/test/CryptolVerifierTC.hs b/cryptol-saw-core/test/CryptolVerifierTC.hs
@@ -27,9 +27,9 @@ main =
      let ?fileReader = BS.readFile
      cenv0 <- CEnv.initCryptolEnv sc
      putStrLn "Translated Cryptol.cry!"
-     cenv1 <- CEnv.importModule sc cenv0 (Right N.floatName) Nothing Nothing
+     cenv1 <- CEnv.importModule sc cenv0 (Right N.floatName) Nothing CEnv.OnlyPublic Nothing
      putStrLn "Translated Float.cry!"
-     cenv2 <- CEnv.importModule sc cenv1 (Right N.arrayName) Nothing Nothing
+     cenv2 <- CEnv.importModule sc cenv1 (Right N.arrayName) Nothing CEnv.OnlyPublic Nothing
      putStrLn "Translated Array.cry!"
      cenv3 <- CEnv.parseDecls sc cenv2 (CEnv.InputText superclassContents "superclass.cry" 1 1)
      putStrLn "Translated superclass.cry!"