diff --git a/crux-mir-comp/src/Mir/Cryptol.hs b/crux-mir-comp/src/Mir/Cryptol.hs index d8bf55534..51dc44ce3 100644 --- a/crux-mir-comp/src/Mir/Cryptol.hs +++ b/crux-mir-comp/src/Mir/Cryptol.hs @@ -241,7 +241,7 @@ loadCryptolFunc col sig modulePath name = do ce' <- liftIO $ SAW.importModule sc ce (Right modName) Nothing SAW.PublicAndPrivate Nothing liftIO (writeIORef (mirCryEnv mirState) ce') -- (m, _ce') <- liftIO $ SAW.loadCryptolModule sc ce (Text.unpack modulePath) - -- tt <- liftIO $ SAW.lookupCryptolModule m (Text.unpack name) + -- tt <- liftIO $ SAW.extractDefFromCryptolModule m (Text.unpack name) tt <- liftIO $ SAW.parseTypedTerm sc ce' $ SAW.InputText name "" 1 1 diff --git a/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs b/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs index 9fd48cd65..09e113431 100644 --- a/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs +++ b/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs @@ -16,7 +16,7 @@ module CryptolSAWCore.CryptolEnv , initCryptolEnv , loadCryptolModule , bindCryptolModule - , lookupCryptolModule + , extractDefFromCryptolModule , combineCryptolEnv , importModule , bindTypedTerm @@ -51,6 +51,7 @@ import qualified Data.Set as Set import Data.Maybe (fromMaybe) import Data.Text (Text, pack, splitOn) import Control.Monad(when) +import GHC.Stack import System.Environment (lookupEnv) import System.Environment.Executable (splitExecutablePath) @@ -102,7 +103,6 @@ import CryptolSAWCore.TypedTerm import Cryptol.ModuleSystem.Env (ModContextParams(NoParams)) -- import SAWCentral.AST (Located(getVal, locatedPos), Import(..)) - -- | Parse input, together with information about where it came from. data InputText = InputText { inpText :: Text -- ^ Parse this @@ -115,20 +115,24 @@ 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. +-- | 'ImportVisibility' - Should a given import (see 'importModule') +-- 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. +-- +-- NOTE: this notion of public vs. private symbols is specific to +-- SAWScript and distinct from Cryptol's notion of private +-- definitions. +-- data ImportVisibility - = OnlyPublic - | PublicAndPrivate + = OnlyPublic -- ^ behaves like a normal Cryptol "import" + | PublicAndPrivate -- ^ allows viewing of both "private" sections and (arbitrarily nested) submodules. + deriving (Eq, Show) + -- | The environment for capturing the Cryptol interpreter state as well as the -- SAWCore translations and associated state. -- --- FIXME[D]: The differences in function between this and the similar --- C.Env? - data CryptolEnv = CryptolEnv { eImports :: [(ImportVisibility, P.Import)] -- ^ Declarations of imported Cryptol modules @@ -181,12 +185,13 @@ nameMatcher xs = -- Initialize ------------------------------------------------------------------ --- FIXME: Code duplication, these three functions are relatively similar (and last 2 are 85% similar): --- - initCryptolEnv --- - loadCryptolModule --- - importModule ---- TODO: common up the common code. - +-- | initCryptolEnv - Create initial CryptolEnv, this involves loading +-- the built-in modules (preludeName, arrayName, +-- preludeReferenceName) and translating them into SAWCore, and +-- putting them into scope. +-- +-- NOTE: submodules in these built-in modules are supported in this code. +-- initCryptolEnv :: (?fileReader :: FilePath -> IO ByteString) => SharedContext -> IO CryptolEnv @@ -218,7 +223,7 @@ initCryptolEnv sc = do return () -- Load Cryptol reference implementations - ((_,refTop), modEnv) <- + ((_,refTop), modEnv3) <- liftModuleM modEnv2 $ MB.loadModuleFrom False (MM.FromModule preludeReferenceName) let refMod = T.tcTopEntityToModule refTop @@ -226,13 +231,14 @@ initCryptolEnv sc = do -- Set up reference implementation redirections let refDecls = T.mDecls refMod let nms = Set.toList (MI.ifsPublic (TIface.genIfaceNames refMod)) + let refPrims = Map.fromList [ (prelPrim (identText (MN.nameIdent nm)), T.EWhere (T.EVar nm) refDecls) | nm <- nms ] let cryEnv0 = C.emptyEnv{ C.envRefPrims = refPrims } -- Generate SAWCore translations for all values in scope - termEnv <- genTermEnv sc modEnv cryEnv0 + termEnv <- genTermEnv sc modEnv3 cryEnv0 -- The module names in P.Import are now Located, so give them an empty position. let preludeName' = P.Located P.emptyRange preludeName @@ -244,7 +250,7 @@ initCryptolEnv sc = do , (OnlyPublic, P.Import preludeReferenceName' (Just preludeReferenceName) Nothing Nothing Nothing) , (OnlyPublic, P.Import arrayName' Nothing Nothing Nothing Nothing) ] - , eModuleEnv = modEnv + , eModuleEnv = modEnv3 , eExtraNames = mempty , eExtraTypes = Map.empty , eExtraTSyns = Map.empty @@ -254,6 +260,20 @@ initCryptolEnv sc = do , eFFITypes = Map.empty } +-- | Translate all declarations in all loaded modules to SAWCore terms +-- NOTE: used only for initialization code. + +genTermEnv :: SharedContext -> ME.ModuleEnv -> C.Env -> IO (Map T.Name Term) +genTermEnv sc modEnv cryEnv0 = do + let declGroups = concatMap T.mDecls + $ filter (not . T.isParametrizedModule) + $ ME.loadedModules modEnv + nominals = ME.loadedNominalTypes modEnv + cryEnv1 <- C.genCodeForNominalTypes sc nominals cryEnv0 + cryEnv2 <- C.importTopLevelDeclGroups sc C.defaultPrimitiveOptions cryEnv1 declGroups + return (C.envE cryEnv2) + + -- Parse ----------------------------------------------------------------------- ioParseExpr :: InputText -> IO (P.Expr P.PName) @@ -281,24 +301,50 @@ ioParseResult res = case res of Right a -> return a Left e -> fail $ "Cryptol parse error:\n" ++ show (P.ppError e) -- X.throwIO (ParseError e) --- Rename ---------------------------------------------------------------------- + +-- NamingEnv and Related ------------------------------------------------------- + +-- | @'getNamingEnv' env@ - get the full 'MR.NamingEnv' based on all the 'eImports' getNamingEnv :: CryptolEnv -> MR.NamingEnv -getNamingEnv env = eExtraNames env `MR.shadowing` nameEnv +getNamingEnv env = + eExtraNames env + `MR.shadowing` + (mconcat $ map + (importToNamingEnv (eModuleEnv env)) + (eImports env) + ) + +importToNamingEnv :: ME.ModuleEnv + -> (ImportVisibility, T.Import) + -> MR.NamingEnv +importToNamingEnv modEnv (vis,imprt) = + MN.interpImportEnv imprt -- adjust for qualified imports + $ adjustVisible -- adjust if OnlyPublic names + $ ME.mctxNames mctx -- namingEnv for PublicAndPrivate + where - nameEnv = mconcat $ fromMaybe [] $ traverse loadImport (eImports env) - loadImport (vis, i) = do - lm <- ME.lookupModule (P.thing $ T.iModule i) (eModuleEnv env) - let ifc = MI.ifNames (ME.lmInterface lm) - syms = MN.namingEnvFromNames $ - case vis of - OnlyPublic -> MI.ifsPublic ifc - PublicAndPrivate -> MI.ifsDefines ifc - return $ MN.interpImportEnv i syms + mctx = modContextOf' (P.ImpTop $ P.thing $ T.iModule imprt) + + adjustVisible = case vis of + PublicAndPrivate -> id + OnlyPublic -> + \env' -> MN.filterUNames (`Set.member` ME.mctxExported mctx) env' + + modContextOf' fm = + case ME.modContextOf fm modEnv of + Just c -> c + Nothing -> panic "getNamingEnv" + ["expecting module to be loaded: " + <> Text.pack (show (pp fm))] + getAllIfaceDecls :: ME.ModuleEnv -> M.IfaceDecls -getAllIfaceDecls me = mconcat (map (both . ME.lmInterface) (ME.getLoadedModules (ME.meLoadedModules me))) - where both = MI.ifDefines +getAllIfaceDecls me = + mconcat + (map (MI.ifDefines . ME.lmInterface) + (ME.getLoadedModules (ME.meLoadedModules me))) + -- Typecheck ------------------------------------------------------------------- @@ -368,17 +414,6 @@ translateDeclGroups sc env dgs = , eTermEnv = C.envE cryEnv' } --- | Translate all declarations in all loaded modules to SAWCore terms -genTermEnv :: SharedContext -> ME.ModuleEnv -> C.Env -> IO (Map T.Name Term) -genTermEnv sc modEnv cryEnv0 = do - let declGroups = concatMap T.mDecls - $ filter (not . T.isParametrizedModule) - $ ME.loadedModules modEnv - nominals = ME.loadedNominalTypes modEnv - cryEnv1 <- C.genCodeForNominalTypes sc nominals cryEnv0 - cryEnv2 <- C.importTopLevelDeclGroups sc C.defaultPrimitiveOptions cryEnv1 declGroups - return (C.envE cryEnv2) - -------------------------------------------------------------------------------- @@ -397,78 +432,138 @@ checkNotParameterized m = , "Either use a ` import, or make a module instantiation." ] +-- FIXME: Code duplication, these two functions are highly similar: +-- - loadCryptolModule +-- - importModule +-- - TODO: "common up" the common code per #2569. + +-- | loadCryptolModule - load a cryptol module and return a handle to +-- the `CryptolModule`. The contents of the module are not imported. +-- +-- This is used to implement the "cryptol_load" primitive in which a +-- handle to the module is returned and can be bound to a SAWScript +-- variable. loadCryptolModule :: (?fileReader :: FilePath -> IO ByteString) => SharedContext -> - C.ImportPrimitiveOptions -> CryptolEnv -> FilePath -> IO (CryptolModule, CryptolEnv) -loadCryptolModule sc primOpts env path = do - +loadCryptolModule sc env path = do let modEnv = eModuleEnv env - (mtop, modEnv') <- liftModuleM modEnv (MB.loadModuleByPath True path) + (mtop, modEnv') <- liftModuleM modEnv $ + MB.loadModuleByPath True path m <- case mtop of - T.TCTopModule mo -> pure mo + T.TCTopModule mod' -> pure mod' T.TCTopSignature {} -> - fail $ "Expected a module, but " ++ show path ++ " is an interface." + fail $ + "Expected a module, but " ++ show path ++ " is an interface." + checkNotParameterized m + -- NOTE: unclear what's happening here! + -- - FIXME: understand and doc. + -- - `m` not used (directly) but translating the modEnv' + -- - this behavior is not in `importModule` + let ifaceDecls = getAllIfaceDecls modEnv' (types, modEnv'') <- liftModuleM modEnv' $ do - prims <- MB.getPrimMap - TM.inpVars `fmap` MB.genInferInput P.emptyRange prims NoParams ifaceDecls + do prims <- MB.getPrimMap + -- generate the primitive map; a monad reader + TM.inpVars `fmap` + MB.genInferInput P.emptyRange prims NoParams ifaceDecls + + -- NOTE: inpVars are the variables that are in scope. + -- FIXME: we are possibly doing unnecessary computation here (see + -- source code for MB.getPrimMap and MB.genInferInput.) + + -- FIXME: it appears (need to verify) that modEnv'' == modEnv' + -- if this true, we can simplify and move this section + -- into `mkCryptolModule`. - -- Regenerate SharedTerm environment. - oldCryEnv <- mkCryEnv env + -- Regenerate SharedTerm environment: let oldModNames = map ME.lmName $ ME.lmLoadedModules $ ME.meLoadedModules modEnv - - let isNew m' = T.mName m' `notElem` oldModNames - let newModules = filter isNew + isNew m' = T.mName m' `notElem` oldModNames + newModules = filter isNew $ map ME.lmModule $ ME.lmLoadedModules $ ME.meLoadedModules modEnv'' - - let newDeclGroups = concatMap T.mDecls newModules - let newNominal = Map.difference (ME.loadedNominalTypes modEnv') + newDeclGroups = concatMap T.mDecls newModules + newNominal = Map.difference (ME.loadedNominalTypes modEnv') (ME.loadedNominalTypes modEnv) newTermEnv <- - do cEnv <- C.genCodeForNominalTypes sc newNominal oldCryEnv - newCryEnv <- C.importTopLevelDeclGroups sc primOpts cEnv newDeclGroups + do oldCryEnv <- mkCryEnv env + cEnv <- C.genCodeForNominalTypes sc newNominal oldCryEnv + newCryEnv <- C.importTopLevelDeclGroups + sc C.defaultPrimitiveOptions cEnv newDeclGroups return (C.envE newCryEnv) + cryptolModule <- mkCryptolModule m types newTermEnv + + -- NOTE: Bringing the module-handle into {{-}} scope is not handled + -- here; it is done rather in `bindCryptolModule`, ONLY if the + -- user binds the `cryptolModule` returned here at the saw + -- command line. + + return ( cryptolModule + , env { eModuleEnv = modEnv'' + , eTermEnv = newTermEnv + , eFFITypes = updateFFITypes m newTermEnv (eFFITypes env) + } + -- NOTE here the difference between this function and + -- `importModule`: + -- 1. the `eImports` field is not updated, as + -- this module (as a whole) is not being + -- brought into scope inside {{ }} constructs. + -- 2. modEnv'' vs modEnv' (which may not be different, see + -- notes above). + ) + +-- | mkCryptolModule +-- +-- FIXME: +-- - This incorrectly excludes both submodules and their contents from +-- the NamingEnvs in `CryptolModule` + +-- - Regarding the CLI API: the `CryptolModule` type is exposed to +-- the SAWScript CLI, is this necessary? + +mkCryptolModule :: T.Module + -> Map MN.Name T.Schema + -> Map MN.Name Term + -> IO CryptolModule +mkCryptolModule m types newTermEnv = + do let names = MEx.exported C.NSValue (T.mExports m) -- :: Set T.Name - - let tm' = Map.filterWithKey (\k _ -> Set.member k names) $ - Map.intersectionWith - (\t x -> TypedTerm (TypedTermSchema t) x) - types - newTermEnv - - let env' = updateFFITypes m - env { eModuleEnv = modEnv'' - , eTermEnv = newTermEnv - } - - let sm' = Map.filterWithKey - (\k _ -> Set.member k (MEx.exported C.NSType (T.mExports m))) - (T.mTySyns m) - - return (CryptolModule sm' tm', env') - -updateFFITypes :: T.Module -> CryptolEnv -> CryptolEnv -updateFFITypes m env = env { eFFITypes = eFFITypes' } + return $ + CryptolModule + -- create type synonym Map, keep only the exports: + (Map.filterWithKey + (\k _ -> Set.member k (MEx.exported C.NSType (T.mExports m))) + (T.mTySyns m) + ) + -- FIXME: TODO: ensure type synonym in submodule is included. + + -- create the map of symbols: + ( Map.filterWithKey (\k _ -> Set.member k names) + $ Map.intersectionWith + (\t x -> TypedTerm (TypedTermSchema t) x) + types -- NOTE: only use of this variable. + newTermEnv + ) + +updateFFITypes :: T.Module -> Map MN.Name Term -> Map NameInfo T.FFI -> Map NameInfo T.FFI +updateFFITypes m eTermEnv' eFFITypes' = + foldr (\(nm, ty) -> Map.insert (getNameInfo nm) ty) + eFFITypes' + (T.findForeignDecls m) where - eFFITypes' = foldr - (\(nm, ty) -> Map.insert (getNameInfo nm) ty) - (eFFITypes env) - (T.findForeignDecls m) getNameInfo nm = - case Map.lookup nm (eTermEnv env) of + case Map.lookup nm eTermEnv' of Just tm -> case asConstant tm of Just n -> nameInfo n @@ -483,31 +578,61 @@ updateFFITypes m env = env { eFFITypes = eFFITypes' } "Cannot find foreign function in term environment: " <> Text.pack (show nm) ] +-- | bindCryptolModule - ad hoc function called when `D <-cryptol_load` is seen +-- on the command line. +-- +-- FIXME: +-- - submodules are not handled correctly below. +-- - the code is duplicating functionality that we have with `importModule` +-- TODO: +-- - new design in PR #2593 (addressing issue #2569) should replace +-- this function so that the fundamental work is done via `importModule`. + bindCryptolModule :: (P.ModName, CryptolModule) -> CryptolEnv -> CryptolEnv bindCryptolModule (modName, CryptolModule sm tm) env = env { eExtraNames = flip (foldr addName) (Map.keys tm') $ - flip (foldr addTSyn) (Map.keys sm) $ eExtraNames env + flip (foldr addTSyn) (Map.keys sm) $ + flip (foldr addSubModule) (Map.keys tm') $ + eExtraNames env , eExtraTSyns = Map.union sm (eExtraTSyns env) , eExtraTypes = Map.union (fmap fst tm') (eExtraTypes env) , eTermEnv = Map.union (fmap snd tm') (eTermEnv env) } where - -- select out those typed terms that have Cryptol schemas + -- | `tm'` is the typed terms from `tm` that have Cryptol schemas tm' = Map.mapMaybe f tm - f (TypedTerm (TypedTermSchema s) x) = Just (s,x) - f _ = Nothing + where + f (TypedTerm (TypedTermSchema s) x) = Just (s,x) + f _ = Nothing addName name = MN.shadowing (MN.singletonNS C.NSValue (P.mkQual modName (MN.nameIdent name)) name) + + addSubModule name = MN.shadowing (MN.singletonNS C.NSModule (P.mkQual modName (MN.nameIdent name)) name) + addTSyn name = MN.shadowing (MN.singletonNS C.NSType (P.mkQual modName (MN.nameIdent name)) name) -lookupCryptolModule :: CryptolModule -> Text -> IO TypedTerm -lookupCryptolModule (CryptolModule _ tm) name = +-- | NOTE: this is only used in the "cryptol_extract" primitive. +extractDefFromCryptolModule :: CryptolModule -> Text -> IO TypedTerm +extractDefFromCryptolModule (CryptolModule _ tm) name = case Map.lookup (mkIdent name) (Map.mapKeys MN.nameIdent tm) of + Just t -> return t Nothing -> fail $ Text.unpack $ "Binding not found: " <> name - Just t -> return t + -- FIXME: unfortunate we have lost the name of the module. + + -- FIXME: bug: we can't access definitions in submodules. + -- FIXME: this is ad hoc, somehow invoke parse for name, or the like? + -------------------------------------------------------------------------------- +-- | @'importModule' sc env src as vis imps@ - extend the Cryptol +-- environment with a module. Closely mirrors the sawscript command "import". +-- +-- NOTE: +-- - the module can be qualified or not (per 'as' argument). per +-- - 'vis' we can import public definitions or *all* (i.e., internal +-- and public) definitions. + importModule :: (?fileReader :: FilePath -> IO ByteString) => SharedContext {- ^ Shared context for creating terms -} -> @@ -519,62 +644,73 @@ importModule :: IO CryptolEnv importModule sc env src as vis imps = do let modEnv = eModuleEnv env - (mtop, modEnv') <- - liftModuleM modEnv $ + (mtop, modEnv') <- liftModuleM modEnv $ case src of Left path -> MB.loadModuleByPath True path - Right mn -> snd <$> MB.loadModuleFrom True (MM.FromModule mn) + Right mn -> snd <$> MB.loadModuleFrom True (MM.FromModule mn) m <- case mtop of - T.TCTopModule m -> pure m + T.TCTopModule mod' -> pure mod' T.TCTopSignature {} -> - fail "Expected a module but found an interface." + fail "Expected a module but found an interface." + checkNotParameterized m - -- Regenerate SharedTerm environment. - oldCryEnv <- mkCryEnv env + -- Regenerate SharedTerm environment: let oldModNames = map ME.lmName $ ME.lmLoadedModules $ ME.meLoadedModules modEnv - let isNew m' = T.mName m' `notElem` oldModNames - let newModules = filter isNew + isNew m' = T.mName m' `notElem` oldModNames + newModules = filter isNew $ map ME.lmModule $ ME.lmLoadedModules $ ME.meLoadedModules modEnv' - let newDeclGroups = concatMap T.mDecls newModules - let newNominal = Map.difference (ME.loadedNominalTypes modEnv') + newDeclGroups = concatMap T.mDecls newModules + newNominal = Map.difference (ME.loadedNominalTypes modEnv') (ME.loadedNominalTypes modEnv) newTermEnv <- - do cEnv <- C.genCodeForNominalTypes sc newNominal oldCryEnv - newCryEnv <- C.importTopLevelDeclGroups sc C.defaultPrimitiveOptions - cEnv newDeclGroups + do oldCryEnv <- mkCryEnv env + cEnv <- C.genCodeForNominalTypes sc newNominal oldCryEnv + newCryEnv <- C.importTopLevelDeclGroups + sc C.defaultPrimitiveOptions cEnv newDeclGroups return (C.envE newCryEnv) - return $ - updateFFITypes m - env { eImports = (vis, P.Import (locate $ T.mName m) as imps Nothing Nothing) - : eImports env - , eModuleEnv = modEnv' - , eTermEnv = newTermEnv - } - where + let newImport = (vis, P.Import { T.iModule= locate $ T.mName m + , T.iAs = as + , T.iSpec = imps + , T.iInst = Nothing + , T.iDoc = Nothing + } + ) -- XXX: it would be better to have the real position, but it -- seems to have been thrown away on the Cryptol side. locate x = P.Located P.emptyRange x + return $ + env{ eModuleEnv = modEnv' + , eTermEnv = newTermEnv + , eFFITypes = updateFFITypes m newTermEnv (eFFITypes env) + , eImports = newImport : eImports env + } + bindIdent :: Ident -> CryptolEnv -> (T.Name, CryptolEnv) bindIdent ident env = (name, env') where modEnv = eModuleEnv env supply = ME.meSupply modEnv fixity = Nothing - (name, supply') = MN.mkDeclared C.NSValue (C.TopModule interactiveName) MN.UserName ident fixity P.emptyRange supply + (name, supply') = MN.mkDeclared + C.NSValue + (C.TopModule interactiveName) + MN.UserName + ident fixity P.emptyRange supply modEnv' = modEnv { ME.meSupply = supply' } env' = env { eModuleEnv = modEnv' } bindTypedTerm :: (Ident, TypedTerm) -> CryptolEnv -> CryptolEnv bindTypedTerm (ident, TypedTerm (TypedTermSchema schema) trm) env = - env' { eExtraNames = MR.shadowing (MN.singletonNS C.NSValue pname name) (eExtraNames env) + env' { eExtraNames = MR.shadowing (MN.singletonNS C.NSValue pname name) + (eExtraNames env) , eExtraTypes = Map.insert name schema (eExtraTypes env) , eTermEnv = Map.insert name trm (eTermEnv env) } @@ -613,14 +749,17 @@ meSolverConfig :: ME.ModuleEnv -> TM.SolverConfig meSolverConfig env = TM.defaultSolverConfig (ME.meSearchPath env) resolveIdentifier :: - (?fileReader :: FilePath -> IO ByteString) => + (HasCallStack, ?fileReader :: FilePath -> IO ByteString) => CryptolEnv -> Text -> IO (Maybe T.Name) resolveIdentifier env nm = case splitOn (pack "::") nm of [] -> pure Nothing + -- FIXME: shouldn't this be error? [i] -> doResolve (P.UnQual (C.mkIdent i)) xs -> let (qs,i) = (init xs, last xs) - in doResolve (P.Qual (C.packModName qs) (C.mkIdent i)) + in doResolve (P.Qual (C.packModName qs) (C.mkIdent i)) + -- FIXME: Is there no function that parses Text into PName? + where modEnv = eModuleEnv env nameEnv = getNamingEnv env @@ -643,12 +782,12 @@ resolveIdentifier env nm = parseTypedTerm :: - (?fileReader :: FilePath -> IO ByteString) => + (HasCallStack, ?fileReader :: FilePath -> IO ByteString) => SharedContext -> CryptolEnv -> InputText -> IO TypedTerm parseTypedTerm sc env input = do - -- Parse + -- Parse: pexpr <- ioParseExpr input - + -- Translate: pExprToTypedTerm sc env pexpr pExprToTypedTerm :: @@ -659,13 +798,13 @@ pExprToTypedTerm sc env pexpr = do ((expr, schema), modEnv') <- liftModuleM modEnv $ do - -- Eliminate patterns + -- Eliminate patterns: npe <- MM.interactive (MB.noPat pexpr) - -- Resolve names let nameEnv = getNamingEnv env - - re <- MM.interactive (MB.rename interactiveName nameEnv (MR.rename npe)) + let npe' = MR.rename npe + re <- MM.interactive (MB.rename interactiveName nameEnv npe') + -- NOTE: if a name is not in scope, it is reported here. -- Infer types let ifDecls = getAllIfaceDecls modEnv diff --git a/cryptol-saw-core/src/CryptolSAWCore/TypedTerm.hs b/cryptol-saw-core/src/CryptolSAWCore/TypedTerm.hs index 8095b74a3..d3d00db16 100644 --- a/cryptol-saw-core/src/CryptolSAWCore/TypedTerm.hs +++ b/cryptol-saw-core/src/CryptolSAWCore/TypedTerm.hs @@ -234,7 +234,9 @@ abstractTypedExts sc tecs (TypedTerm (TypedTermOther _tp) trm) = -- terms. data CryptolModule = - CryptolModule (Map C.Name C.TySyn) (Map C.Name TypedTerm) + CryptolModule + (Map C.Name C.TySyn) -- type synonyms + (Map C.Name TypedTerm) -- symbols (mapping to SawCore things). showCryptolModule :: CryptolModule -> String showCryptolModule (CryptolModule sm tm) = diff --git a/deps/cryptol b/deps/cryptol index 0412ebf96..e9827790c 160000 --- a/deps/cryptol +++ b/deps/cryptol @@ -1 +1 @@ -Subproject commit 0412ebf96c00361dd67e20718eac6a9f13b4c6f1 +Subproject commit e9827790c59cb40381932f66df4b91df89a4fac1 diff --git a/intTests/.gitignore b/intTests/.gitignore index 370368720..c8e5db37d 100644 --- a/intTests/.gitignore +++ b/intTests/.gitignore @@ -1,4 +1,5 @@ .cache +*.cache .local .saw logs diff --git a/intTests/test_saw_submodule_access1/A.cry b/intTests/test_saw_submodule_access1/A.cry new file mode 100644 index 000000000..719d08d80 --- /dev/null +++ b/intTests/test_saw_submodule_access1/A.cry @@ -0,0 +1,4 @@ +module A where + +a : [32] +a = 2 diff --git a/intTests/test_saw_submodule_access1/B.cry b/intTests/test_saw_submodule_access1/B.cry new file mode 100644 index 000000000..581383565 --- /dev/null +++ b/intTests/test_saw_submodule_access1/B.cry @@ -0,0 +1,4 @@ +module B where +import A + +b = a + 10 diff --git a/intTests/test_saw_submodule_access1/C.cry b/intTests/test_saw_submodule_access1/C.cry new file mode 100644 index 000000000..b3a58cd5f --- /dev/null +++ b/intTests/test_saw_submodule_access1/C.cry @@ -0,0 +1,4 @@ +module C where +import A as A' +c = A'::a + 100 +a = A'::a diff --git a/intTests/test_saw_submodule_access1/D.cry b/intTests/test_saw_submodule_access1/D.cry new file mode 100644 index 000000000..62fd960cb --- /dev/null +++ b/intTests/test_saw_submodule_access1/D.cry @@ -0,0 +1,19 @@ +module D where +import B +import C + +d00 = 2000 + b + c +d01 = 5 + D2::d2 + +type DTySy = [32] + +submodule D2 where + d2 = d00 + 10000 + + type D2TySy = [32] + + submodule D3 where + d3 = d00 + d2 + 1 + + type D3TySy = [32] + diff --git a/intTests/test_saw_submodule_access1/E.cry b/intTests/test_saw_submodule_access1/E.cry new file mode 100644 index 000000000..98478a5c2 --- /dev/null +++ b/intTests/test_saw_submodule_access1/E.cry @@ -0,0 +1,11 @@ +module E where +import D + +e = 5 +e2 = d00 + +// NOT legal: D2::d2 +// But this works: + +import submodule D2 +e3 = d2 diff --git a/intTests/test_saw_submodule_access1/F.cry b/intTests/test_saw_submodule_access1/F.cry new file mode 100644 index 000000000..67da35189 --- /dev/null +++ b/intTests/test_saw_submodule_access1/F.cry @@ -0,0 +1,21 @@ +module F where +import B +import C + +top0 = 2000 + b + c +topd2 = 5 + D3::d2 +topd3 = 10 + D3::D4::d3 + +d00 : [32] +d00 = 1 // let's conflict with D.cry + +submodule D3 where + d2 = 10000 + top0 + d3D2 = 1 + D4::d3 + d2' = 1 + d3P + + private + d3P = 1 + d2 + + submodule D4 where + d3 = 20000 + top0 + d2 diff --git a/intTests/test_saw_submodule_access1/IgnoredImportErrors.cry b/intTests/test_saw_submodule_access1/IgnoredImportErrors.cry new file mode 100644 index 000000000..7446b6d8e --- /dev/null +++ b/intTests/test_saw_submodule_access1/IgnoredImportErrors.cry @@ -0,0 +1,12 @@ +module IgnoredImportErrors where + +// NOTE: none of the foobar* variables are in the code. +// - but this error is not caught by saw or cryptol. + +import D as D1 (foobar1) +import D as D2 hiding (foobar2) + +import D (foobar3) +import D hiding (foobar4) + +x = 5 diff --git a/intTests/test_saw_submodule_access1/UseFunctors.cry b/intTests/test_saw_submodule_access1/UseFunctors.cry new file mode 100644 index 000000000..e090fb033 --- /dev/null +++ b/intTests/test_saw_submodule_access1/UseFunctors.cry @@ -0,0 +1,26 @@ +module UseFunctors where + +submodule M where + x = 0x02 + + submodule M1 where + x = 0x03 + +ex1 = M::x + M::M1::x // This is OK because of implicit imports of M and M1 + +// This is a functor +submodule F where + parameter + p: [8] + + submodule FM where + z = 0x03 + p + + f = 2 * p + +submodule I = submodule F where + p = 11 + +ex2 = I::f + 2 // This is OK because of implicit import of I + +// ex3 = I::FM::z This is not OK, becase FM is not syntactically visible in I, so we can't add an implicit import \ No newline at end of file diff --git a/intTests/test_saw_submodule_access1/test.sh b/intTests/test_saw_submodule_access1/test.sh new file mode 100755 index 000000000..c6c01a2e6 --- /dev/null +++ b/intTests/test_saw_submodule_access1/test.sh @@ -0,0 +1,14 @@ +set -e + # all must pass. + +$SAW test_import_errors.saw + +$SAW test_import_D.saw + +! $SAW test_load_D.saw + + # finishing https://github.com/GaloisInc/saw-script/pull/2593 + # should allow test_load_D.saw to succeed. (as it should) + # TODO: remove the ! above when that PR is done. + +$SAW test_UseFunctors.saw diff --git a/intTests/test_saw_submodule_access1/test_UseFunctors.saw b/intTests/test_saw_submodule_access1/test_UseFunctors.saw new file mode 100644 index 000000000..cc25631ce --- /dev/null +++ b/intTests/test_saw_submodule_access1/test_UseFunctors.saw @@ -0,0 +1,10 @@ +import "UseFunctors.cry"; + +print (eval_int {{ex1}}); // should succeed. +print (eval_int {{ex2}}); // should succeed. + +// confirming fails of things that shouldn't be in scope: +fails (do {return {{ I::FM::z }};}); + // see comments in .cry file. + +print "done"; diff --git a/intTests/test_saw_submodule_access1/test_import_D.saw b/intTests/test_saw_submodule_access1/test_import_D.saw new file mode 100644 index 000000000..db5c28135 --- /dev/null +++ b/intTests/test_saw_submodule_access1/test_import_D.saw @@ -0,0 +1,11 @@ +import "D.cry"; + +print (eval_int {{D2::d2}}); // should succeed. +print (eval_int {{D2::D3::d3}}); // should succeed. + +// confirming fails of things that shouldn't be in scope: +fails (do {return {{ d2 }};}); +fails (do {return {{ D2::d3 }};}); +fails (do {return {{ D::D2::d2 }};}); + +print "done"; diff --git a/intTests/test_saw_submodule_access1/test_import_errors.saw b/intTests/test_saw_submodule_access1/test_import_errors.saw new file mode 100644 index 000000000..b9171108c --- /dev/null +++ b/intTests/test_saw_submodule_access1/test_import_errors.saw @@ -0,0 +1,3 @@ +import "IgnoredImportErrors.cry"; + +print "done"; diff --git a/intTests/test_saw_submodule_access1/test_load_D.saw b/intTests/test_saw_submodule_access1/test_load_D.saw new file mode 100644 index 000000000..09c0a0df1 --- /dev/null +++ b/intTests/test_saw_submodule_access1/test_load_D.saw @@ -0,0 +1,9 @@ +D <- cryptol_load "D.cry"; + +print (eval_int {{D::D2::d2}}); // should succeed + +// confirming fails of things that shouldn't be in scope: +fails (do {return {{ d2 }};}); +fails (do {return {{ D::d2 }};}); + +print "done"; \ No newline at end of file diff --git a/intTests/test_saw_submodule_access2/.gitignore b/intTests/test_saw_submodule_access2/.gitignore new file mode 100644 index 000000000..4619758de --- /dev/null +++ b/intTests/test_saw_submodule_access2/.gitignore @@ -0,0 +1,3 @@ +*.rawlog +*.log +*.diff diff --git a/intTests/test_saw_submodule_access2/Makefile b/intTests/test_saw_submodule_access2/Makefile new file mode 100644 index 000000000..c9e12c62a --- /dev/null +++ b/intTests/test_saw_submodule_access2/Makefile @@ -0,0 +1,5 @@ +all: ; +clean: + sh ./test.sh clean + +.PHONY: all clean diff --git a/intTests/test_saw_submodule_access2/test.sh b/intTests/test_saw_submodule_access2/test.sh new file mode 100644 index 000000000..5fcd79d0a --- /dev/null +++ b/intTests/test_saw_submodule_access2/test.sh @@ -0,0 +1 @@ +exec ${TEST_SHELL:-bash} ../support/test-and-diff.sh "$@" diff --git a/intTests/test_saw_submodule_access2/testDups.log.good b/intTests/test_saw_submodule_access2/testDups.log.good new file mode 100644 index 000000000..6628bfc61 --- /dev/null +++ b/intTests/test_saw_submodule_access2/testDups.log.good @@ -0,0 +1,14 @@ + Loading file "testDups.saw" + 2114 +== Anticipated failure message == +Stack trace: + (builtin) in (callback) + (builtin) in fails + testDups.saw:7:1-7:44 (at top level) +Cryptol error: +[error] at testDups.saw:7:33--7:36 + Multiple definitions for symbol: d00 + (at ../test_saw_submodule_access1/D.cry:5:1--5:4, D::d00) + (at ../test_saw_submodule_access1/F.cry:10:1--10:4, F::d00) + + done diff --git a/intTests/test_saw_submodule_access2/testDups.saw b/intTests/test_saw_submodule_access2/testDups.saw new file mode 100644 index 000000000..44e4acb0c --- /dev/null +++ b/intTests/test_saw_submodule_access2/testDups.saw @@ -0,0 +1,10 @@ +import "../test_saw_submodule_access1/D.cry"; +import "../test_saw_submodule_access1/F.cry"; + +print (eval_int {{top0}}); // no problem! + +// expected failures: +fails (do { return (eval_int {{ d00 }}); } ); + // should fail with "Multiple Definitions" + +print "done"; diff --git a/intTests/test_saw_submodule_access2/testQualifiedImports.log.good b/intTests/test_saw_submodule_access2/testQualifiedImports.log.good new file mode 100644 index 000000000..d149a6713 --- /dev/null +++ b/intTests/test_saw_submodule_access2/testQualifiedImports.log.good @@ -0,0 +1,33 @@ + Loading file "testQualifiedImports.saw" + 2114 + 12114 + 14229 + 2 +== Anticipated failure message == +Stack trace: + (builtin) in (callback) + (builtin) in fails + testQualifiedImports.saw:13:1-13:30 (at top level) +Cryptol error: +[error] at testQualifiedImports.saw:13:22--13:25 + Value not in scope: d00 + +== Anticipated failure message == +Stack trace: + (builtin) in (callback) + (builtin) in fails + testQualifiedImports.saw:14:1-14:34 (at top level) +Cryptol error: +[error] at testQualifiedImports.saw:14:22--14:29 + Value not in scope: MyD::d2 + +== Anticipated failure message == +Stack trace: + (builtin) in (callback) + (builtin) in fails + testQualifiedImports.saw:15:1-15:40 (at top level) +Cryptol error: +[error] at testQualifiedImports.saw:15:22--15:35 + Value not in scope: NOTINSCOPEVar + + done diff --git a/intTests/test_saw_submodule_access2/testQualifiedImports.saw b/intTests/test_saw_submodule_access2/testQualifiedImports.saw new file mode 100644 index 000000000..4d40ff9fa --- /dev/null +++ b/intTests/test_saw_submodule_access2/testQualifiedImports.saw @@ -0,0 +1,17 @@ +import "../test_saw_submodule_access1/D.cry" as MyD; + +// testing visible exports: + +print (eval_int {{MyD::d00}}); +print (eval_int {{MyD::D2::d2}}); +print (eval_int {{MyD::D2::D3::d3}}); + +// testing visible in MyD variables: +print (eval_int {{MyD::a}}); + +// confirming fails of things that shouldn't be in scope: +fails (do {return {{ d00 }};}); +fails (do {return {{ MyD::d2 }};}); +fails (do {return {{ NOTINSCOPEVar }};}); + +print "done"; diff --git a/saw-central/src/SAWCentral/Builtins.hs b/saw-central/src/SAWCentral/Builtins.hs index 4cda29a19..b5908d6f9 100644 --- a/saw-central/src/SAWCentral/Builtins.hs +++ b/saw-central/src/SAWCentral/Builtins.hs @@ -2146,7 +2146,7 @@ cryptol_load fileReader path = do rw <- getTopLevelRW let ce = rwCryptol rw let ?fileReader = fileReader - (m, ce') <- io $ CEnv.loadCryptolModule sc CEnv.defaultPrimitiveOptions ce path + (m, ce') <- io $ CEnv.loadCryptolModule sc ce path putTopLevelRW $ rw { rwCryptol = ce' } return m diff --git a/saw-central/src/SAWCentral/Prover/Exporter.hs b/saw-central/src/SAWCentral/Prover/Exporter.hs index 80e346d0d..45c67f283 100644 --- a/saw-central/src/SAWCentral/Prover/Exporter.hs +++ b/saw-central/src/SAWCentral/Prover/Exporter.hs @@ -71,8 +71,7 @@ import Prettyprinter.Render.Text import Lang.JVM.ProcessUtils (readProcessExitIfFailure) -import CryptolSAWCore.CryptolEnv (initCryptolEnv, loadCryptolModule, - ImportPrimitiveOptions(..), mkCryEnv) +import CryptolSAWCore.CryptolEnv (initCryptolEnv, loadCryptolModule, mkCryEnv) import CryptolSAWCore.Prelude (cryptolModule, scLoadPreludeModule, scLoadCryptolModule) import CryptolSAWCore.PreludeM (cryptolMModule, specMModule, scLoadSpecMModule, scLoadCryptolMModule) @@ -530,8 +529,9 @@ writeCoqCryptolModule mon inputFile outputFile notations skips = io $ do let ?fileReader = BS.readFile env <- initCryptolEnv sc cryptolPrimitivesForSAWCoreModule <- scFindModule sc nameOfCryptolPrimitivesForSAWCoreModule - let primOpts = ImportPrimitiveOptions{ allowUnknownPrimitives = True } - (cm, _) <- loadCryptolModule sc primOpts env inputFile + (cm, _) <- loadCryptolModule sc env inputFile + -- NOTE: implementation of loadCryptolModule, now uses this default: + -- defaultPrimitiveOptions = ImportPrimitiveOptions{allowUnknownPrimitives=True} cry_env <- mkCryEnv env mm <- scGetModuleMap sc let ?mm = mm diff --git a/saw-central/src/SAWCentral/Value.hs b/saw-central/src/SAWCentral/Value.hs index 866df58af..c7698c377 100644 --- a/saw-central/src/SAWCentral/Value.hs +++ b/saw-central/src/SAWCentral/Value.hs @@ -1197,7 +1197,7 @@ maybeInsert k (Just x) m = M.insert k x m extendEnv :: SharedContext -> SS.LName -> SS.Schema -> Maybe String -> Value -> TopLevelRW -> IO TopLevelRW -extendEnv sc x ty md v rw = +extendEnv sc name ty md v rw = do ce' <- case v of VTerm t -> @@ -1222,10 +1222,9 @@ extendEnv sc x ty md v rw = , rwCryptol = ce' } where - name = x -- XXX why is this using getOrig? - ident = T.mkIdent (SS.getOrig x) - modname = T.packModName [SS.getOrig x] + ident = T.mkIdent (SS.getOrig name) + modname = T.packModName [SS.getOrig name] ce = rwCryptol rw typedTermOfString :: SharedContext -> String -> IO TypedTerm diff --git a/saw-central/src/SAWCentral/X86.hs b/saw-central/src/SAWCentral/X86.hs index 10efb99e9..aa2154f11 100644 --- a/saw-central/src/SAWCentral/X86.hs +++ b/saw-central/src/SAWCentral/X86.hs @@ -133,7 +133,7 @@ import SAWCore.Recognizer(asBool) import SAWCoreWhat4.ReturnTrip (sawRegisterSymFunInterp, toSC, saw_ctx) -- Cryptol Verifier -import CryptolSAWCore.CryptolEnv(CryptolEnv,initCryptolEnv,loadCryptolModule,defaultPrimitiveOptions) +import CryptolSAWCore.CryptolEnv(CryptolEnv,initCryptolEnv,loadCryptolModule) import CryptolSAWCore.Prelude(scLoadPreludeModule,scLoadCryptolModule) -- SAWCentral @@ -387,7 +387,7 @@ loadCry sym mb = env <- initCryptolEnv sc case mb of Nothing -> return env - Just file -> snd <$> loadCryptolModule sc defaultPrimitiveOptions env file + Just file -> snd <$> loadCryptolModule sc env file -------------------------------------------------------------------------------- diff --git a/saw-script/src/SAWScript/Interpreter.hs b/saw-script/src/SAWScript/Interpreter.hs index 4f00aeef4..4f07f86fb 100644 --- a/saw-script/src/SAWScript/Interpreter.hs +++ b/saw-script/src/SAWScript/Interpreter.hs @@ -1597,7 +1597,7 @@ instance IsValue CryptolModule where instance FromValue CryptolModule where fromValue _ (VCryptolModule m) = m - fromValue _ _ = error "fromValue ModuleEnv" + fromValue _ _ = error "fromValue CryptolModule" instance IsValue JSS.Class where toValue _name c = VJavaClass c @@ -2688,7 +2688,7 @@ primitives = Map.fromList Experimental [ "Disable checking of safety obligations encountered during symbolic" , "execution. This is unsound! However, it can be useful during" - , "initial proof construction to focus only on the stated correcness" + , "initial proof construction to focus only on the stated correctness" , "specifications." ] @@ -4199,7 +4199,7 @@ primitives = Map.fromList [ "Load the given file as a Cryptol module." ] , prim "cryptol_extract" "CryptolModule -> String -> TopLevel Term" - (pureVal CEnv.lookupCryptolModule) + (pureVal CEnv.extractDefFromCryptolModule) Current [ "Load a single definition from a Cryptol module and translate it into" , "a 'Term'."