From 03ac6374691e192b236604f889a2aec1567cbb49 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Mon, 18 Jan 2021 10:07:16 -0800 Subject: [PATCH 1/3] Type check in context of private symbols Include both public and private symbols from imported modules when type checking. This addresses saw-script#971. --- cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs b/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs index ea1cfa91eb..dde0698c5a 100644 --- a/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs +++ b/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs @@ -238,7 +238,8 @@ getNamingEnv env = eExtraNames env `MR.shadowing` nameEnv nameEnv = mconcat $ fromMaybe [] $ traverse loadImport (eImports env) loadImport i = do lm <- ME.lookupModule (T.iModule i) (eModuleEnv env) - return $ MN.interpImport i (MI.ifPublic (ME.lmInterface lm)) + let ifc = ME.lmInterface lm + return $ MN.interpImport i (MI.ifPublic ifc `mappend` M.ifPrivate ifc) getAllIfaceDecls :: ME.ModuleEnv -> M.IfaceDecls getAllIfaceDecls me = mconcat (map (both . ME.lmInterface) (ME.getLoadedModules (ME.meLoadedModules me))) From 96318034fe5fa837d8a046fe860cd73a7f397331 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Tue, 19 Jan 2021 14:34:36 -0800 Subject: [PATCH 2/3] Make visibility of Cryptol symbols configurable --- .../src/Verifier/SAW/CryptolEnv.hs | 29 ++++++++++++++----- cryptol-saw-core/test/CryptolVerifierTC.hs | 4 +-- 2 files changed, 23 insertions(+), 10 deletions(-) diff --git a/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs b/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs index dde0698c5a..a3e18cb873 100644 --- 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,10 +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) let ifc = ME.lmInterface lm - return $ MN.interpImport i (MI.ifPublic ifc `mappend` M.ifPrivate ifc) + 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))) @@ -385,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 $ @@ -405,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 index 8270df0a7d..73b1e58052 100644 --- 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 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 OnlyPublic Nothing putStrLn "Translated Array.cry!" cenv3 <- CEnv.parseDecls sc cenv2 (CEnv.InputText superclassContents "superclass.cry" 1 1) putStrLn "Translated superclass.cry!" From 2ac0378392d2e7b4fad49af7078dd5d74be952cc Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Tue, 19 Jan 2021 14:36:49 -0800 Subject: [PATCH 3/3] Fix cryptol-saw-core tests --- cryptol-saw-core/test/CryptolVerifierTC.hs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/cryptol-saw-core/test/CryptolVerifierTC.hs b/cryptol-saw-core/test/CryptolVerifierTC.hs index 73b1e58052..e5bffe455b 100644 --- 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 OnlyPublic 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 OnlyPublic 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!"