From c2e1117b4307a631d2f99f8e03b5bbf9c7026f50 Mon Sep 17 00:00:00 2001 From: David Holland Date: Fri, 10 Oct 2025 21:49:33 -0400 Subject: [PATCH 01/13] REPL: Internal naming reform. - The members of the Refs record should have the prefix "r", not "e". - Also they should all have a prefix, not some of them. - Don't call the TopLevelRW the "environment"; that is already plenty confusing and will be growing more so shortly. NFCI --- saw-script/src/SAWScript/REPL/Command.hs | 10 +-- saw-script/src/SAWScript/REPL/Haskeline.hs | 4 +- saw-script/src/SAWScript/REPL/Monad.hs | 94 +++++++++++----------- 3 files changed, 54 insertions(+), 54 deletions(-) diff --git a/saw-script/src/SAWScript/REPL/Command.hs b/saw-script/src/SAWScript/REPL/Command.hs index 4fb23b57fd..01aad94c18 100644 --- a/saw-script/src/SAWScript/REPL/Command.hs +++ b/saw-script/src/SAWScript/REPL/Command.hs @@ -199,7 +199,7 @@ typeOfCmd str Right expr -> return expr let pos = getPos expr decl = SS.Decl pos (SS.PWild pos Nothing) Nothing expr - rw <- getValueEnvironment + rw <- getTopLevelRWForValues decl' <- do let primsAvail = rwPrimsAvail rw valueInfo = rwValueInfo rw @@ -223,7 +223,7 @@ searchCmd str pat <- case SAWScript.Parser.parseSchemaPattern tokens of Left err -> fail (show err) Right pat -> return pat - rw <- getValueEnvironment + rw <- getTopLevelRWForValues -- Always search the entire environment and recognize all type -- names in the user's pattern, regardless of whether @@ -339,7 +339,7 @@ quitCmd = stop envCmd :: REPL () envCmd = do - rw <- getValueEnvironment + rw <- getTopLevelRWForValues let avail = rwPrimsAvail rw valueInfo = rwValueInfo rw keep (_pos, lc, _rb, _ty, _v, _doc) = Set.member lc avail @@ -350,7 +350,7 @@ envCmd = do tenvCmd :: REPL () tenvCmd = do - rw <- getValueEnvironment + rw <- getTopLevelRWForValues let avail = rwPrimsAvail rw typeInfo = rwTypeInfo rw typeInfo' = Map.filter (\(lc, _ty) -> Set.member lc avail) typeInfo @@ -362,7 +362,7 @@ helpCmd :: String -> REPL () helpCmd cmd | null cmd = io (mapM_ putStrLn (genHelp commandList)) | otherwise = - do env <- getEnvironment + do env <- getTopLevelRW case Map.lookup (Text.pack cmd) (rwValueInfo env) of Just (_pos, _lc, _rb, _ty, _v, Just doc) -> io $ mapM_ TextIO.putStrLn doc diff --git a/saw-script/src/SAWScript/REPL/Haskeline.hs b/saw-script/src/SAWScript/REPL/Haskeline.hs index 853f10558a..ede53f9a06 100644 --- a/saw-script/src/SAWScript/REPL/Haskeline.hs +++ b/saw-script/src/SAWScript/REPL/Haskeline.hs @@ -57,8 +57,8 @@ replBody mbBatch begin = enableSubshell m = REPL $ \refs -> - do let ro' = (eTopLevelRO refs){ roSubshell = subshell (runInputT replSettings (withInterrupt loop)) } - unREPL m refs{ eTopLevelRO = ro' } + do let ro' = (rTopLevelRO refs){ roSubshell = subshell (runInputT replSettings (withInterrupt loop)) } + unREPL m refs{ rTopLevelRO = ro' } loop = do prompt <- MTL.lift getPrompt diff --git a/saw-script/src/SAWScript/REPL/Monad.hs b/saw-script/src/SAWScript/REPL/Monad.hs index 4640170295..378cb3247b 100644 --- a/saw-script/src/SAWScript/REPL/Monad.hs +++ b/saw-script/src/SAWScript/REPL/Monad.hs @@ -49,9 +49,9 @@ module SAWScript.REPL.Monad ( -- ** SAWScript stuff , getSharedContext , getTopLevelRO - , getValueEnvironment - , getEnvironment, modifyEnvironment, putEnvironment - , getEnvironmentRef + , getTopLevelRWForValues + , getTopLevelRW, modifyTopLevelRW, putTopLevelRW + , getTopLevelRWRef , getProofStateRef , getSAWScriptValueNames , getSAWScriptTypeNames @@ -113,11 +113,11 @@ deriving instance Typeable AIG.Proxy -- REPL Environment. data Refs = Refs - { eContinue :: IORef Bool - , eIsBatch :: Bool - , eTopLevelRO :: TopLevelRO - , environment :: IORef TopLevelRW - , proofState :: Maybe (IORef ProofState) + { rContinue :: IORef Bool + , rIsBatch :: Bool + , rTopLevelRO :: TopLevelRO + , rTopLevelRW :: IORef TopLevelRW + , rProofState :: Maybe (IORef ProofState) } -- | Initial, empty environment. @@ -127,11 +127,11 @@ defaultRefs isBatch opts = contRef <- newIORef True rwRef <- newIORef rw return Refs - { eContinue = contRef - , eIsBatch = isBatch - , eTopLevelRO = ro - , environment = rwRef - , proofState = Nothing + { rContinue = contRef + , rIsBatch = isBatch + , rTopLevelRO = ro + , rTopLevelRW = rwRef + , rProofState = Nothing } @@ -158,11 +158,11 @@ subshell (REPL m) = TopLevel_ $ do contRef <- newIORef True rwRef <- newIORef rw let refs = Refs - { eContinue = contRef - , eIsBatch = False - , eTopLevelRO = ro - , environment = rwRef - , proofState = Nothing + { rContinue = contRef + , rIsBatch = False + , rTopLevelRO = ro + , rTopLevelRW = rwRef + , rProofState = Nothing } m refs readIORef rwRef @@ -178,11 +178,11 @@ proof_subshell (REPL m) = rwRef <- newIORef rw proofRef <- newIORef proofSt let refs = Refs - { eContinue = contRef - , eIsBatch = False - , eTopLevelRO = ro - , environment = rwRef - , proofState = Just proofRef + { rContinue = contRef + , rIsBatch = False + , rTopLevelRO = ro + , rTopLevelRW = rwRef + , rProofState = Just proofRef } m refs (,) <$> readIORef rwRef <*> readIORef proofRef @@ -291,7 +291,7 @@ rethrowEvalError m = run `X.catch` rethrow exceptionProtect :: REPL () -> REPL () exceptionProtect cmd = - do chk <- io . makeCheckpoint =<< getEnvironment + do chk <- io . makeCheckpoint =<< getTopLevelRW cmd `catch` (handlerPP chk) `catchFail` (handlerFail chk) `catchOther` (handlerPrint chk) @@ -312,7 +312,7 @@ exceptionProtect cmd = liftTopLevel :: TopLevel a -> REPL a liftTopLevel m = do ro <- getTopLevelRO - ref <- getEnvironmentRef + ref <- getTopLevelRWRef io $ do rw <- readIORef ref (a, rw') <- runTopLevel m ro rw writeIORef ref rw' @@ -347,7 +347,7 @@ modifyRef r f = REPL (\refs -> modifyIORef (r refs) f) -- | Construct the prompt for the current environment. getPrompt :: REPL String getPrompt = - do batch <- REPL (return . eIsBatch) + do batch <- REPL (return . rIsBatch) if batch then return "" else getProofStateRef >>= \case @@ -357,14 +357,14 @@ getPrompt = return ("proof ("++show (length (psGoals ps))++")> ") shouldContinue :: REPL Bool -shouldContinue = readRef eContinue +shouldContinue = readRef rContinue stop :: REPL () -stop = modifyRef eContinue (const False) +stop = modifyRef rContinue (const False) unlessBatch :: REPL () -> REPL () unlessBatch body = - do batch <- REPL (return . eIsBatch) + do batch <- REPL (return . rIsBatch) unless batch body setREPLTitle :: REPL () @@ -456,44 +456,44 @@ setModuleEnv :: M.ModuleEnv -> REPL () setModuleEnv me = modifyCryptolEnv (\ce -> ce { eModuleEnv = me }) getCryptolEnv :: REPL CryptolEnv -getCryptolEnv = rwCryptol `fmap` getEnvironment +getCryptolEnv = rwCryptol `fmap` getTopLevelRW modifyCryptolEnv :: (CryptolEnv -> CryptolEnv) -> REPL () -modifyCryptolEnv f = modifyEnvironment (\rw -> rw { rwCryptol = f (rwCryptol rw) }) +modifyCryptolEnv f = modifyTopLevelRW (\rw -> rw { rwCryptol = f (rwCryptol rw) }) setCryptolEnv :: CryptolEnv -> REPL () setCryptolEnv x = modifyCryptolEnv (const x) getSharedContext :: REPL SharedContext -getSharedContext = rwSharedContext <$> getEnvironment +getSharedContext = rwSharedContext <$> getTopLevelRW getTopLevelRO :: REPL TopLevelRO -getTopLevelRO = REPL (return . eTopLevelRO) +getTopLevelRO = REPL (return . rTopLevelRO) -getEnvironmentRef :: REPL (IORef TopLevelRW) -getEnvironmentRef = environment <$> getRefs +getTopLevelRWRef :: REPL (IORef TopLevelRW) +getTopLevelRWRef = rTopLevelRW <$> getRefs getProofStateRef :: REPL (Maybe (IORef ProofState)) -getProofStateRef = proofState <$> getRefs +getProofStateRef = rProofState <$> getRefs -getEnvironment :: REPL TopLevelRW -getEnvironment = readRef environment +getTopLevelRW :: REPL TopLevelRW +getTopLevelRW = readRef rTopLevelRW -getValueEnvironment :: REPL TopLevelRW -getValueEnvironment = - do rw <- getEnvironment +getTopLevelRWForValues :: REPL TopLevelRW +getTopLevelRWForValues = + do rw <- getTopLevelRW io (mergeLocalEnv (rwSharedContext rw) (rwLocalEnv rw) rw) -putEnvironment :: TopLevelRW -> REPL () -putEnvironment = modifyEnvironment . const +putTopLevelRW :: TopLevelRW -> REPL () +putTopLevelRW = modifyTopLevelRW . const -modifyEnvironment :: (TopLevelRW -> TopLevelRW) -> REPL () -modifyEnvironment = modifyRef environment +modifyTopLevelRW :: (TopLevelRW -> TopLevelRW) -> REPL () +modifyTopLevelRW = modifyRef rTopLevelRW -- | Get visible variable names for Haskeline completion. getSAWScriptValueNames :: REPL [String] getSAWScriptValueNames = do - env <- getEnvironment + env <- getTopLevelRW let avail = rwPrimsAvail env visible (_, lc, _, _, _, _) = Set.member lc avail let rnames = Map.keys $ Map.filter visible $ rwValueInfo env @@ -502,7 +502,7 @@ getSAWScriptValueNames = do -- | Get visible type names for Haskeline completion. getSAWScriptTypeNames :: REPL [String] getSAWScriptTypeNames = do - env <- getEnvironment + env <- getTopLevelRW let avail = rwPrimsAvail env visible (lc, _) = Set.member lc avail let rnames = Map.keys $ Map.filter visible $ rwTypeInfo env From cf38a8083fffc2708f916e931fd6d1cc2b6dd7c9 Mon Sep 17 00:00:00 2001 From: David Holland Date: Fri, 10 Oct 2025 21:58:04 -0400 Subject: [PATCH 02/13] support: Add a ScopedMap type. This is like Data.Map except it's a chain of maps that function as scopes; keys in inner (more recent) scopes override matching keys in outer (older) scopes, as one wants for scoped variable lookup. You can also push and pop the scope entries as you carry the map in and out of scoping constructs. Also add SAWSupport.Panic because there isn't one yet and ScopedMap has a panic case: trying to pop the last scope. --- saw-support/src/SAWSupport/Panic.hs | 19 +++ saw-support/src/SAWSupport/ScopedMap.hs | 160 ++++++++++++++++++++++++ saw.cabal | 3 + 3 files changed, 182 insertions(+) create mode 100644 saw-support/src/SAWSupport/Panic.hs create mode 100644 saw-support/src/SAWSupport/ScopedMap.hs diff --git a/saw-support/src/SAWSupport/Panic.hs b/saw-support/src/SAWSupport/Panic.hs new file mode 100644 index 0000000000..ab25d2e0c4 --- /dev/null +++ b/saw-support/src/SAWSupport/Panic.hs @@ -0,0 +1,19 @@ +{-# LANGUAGE OverloadedStrings #-} +{- | +Module : SAWSupport.Panic +License : BSD3 +Maintainer : saw@galois.com +Stability : provisional +-} + +module SAWSupport.Panic (panic) where + +import Data.Text (Text) + +import SAWSupport.PanicSupport + +-- | Raise a fatal error. See commentary in PanicSupport. +-- Arguments are "location" (one string) and "description" (multiple +-- strings). +panic :: HasCallStack => Text -> [Text] -> a +panic loc descs = doPanic "saw-support" loc descs diff --git a/saw-support/src/SAWSupport/ScopedMap.hs b/saw-support/src/SAWSupport/ScopedMap.hs new file mode 100644 index 0000000000..6d314a94f2 --- /dev/null +++ b/saw-support/src/SAWSupport/ScopedMap.hs @@ -0,0 +1,160 @@ +{-# LANGUAGE OverloadedStrings #-} + +-- | +-- Module : SAWSupport.ScopedMap +-- Description : Scoped-aware finite map library +-- License : BSD3 +-- Maintainer : saw@galois.com +-- Stability : provisional +-- +-- Scope-aware map for use as an interpreter or typechecker +-- environment. +-- +-- The `ScopedMap` type is a stack of maps; each layer corresponds +-- to a scope as the client moves into and out of nested naming +-- environments. +-- +-- The current (innermost) scope is at the top of the stack / head of +-- the list. +-- +-- Update operations act on the current scope. Lookup operations +-- inspect the whole stack, starting at the innermost layer and +-- working out. +-- +-- The `push` and `pop` operations add and drop scopes respectively, +-- and should be used when the client enters and leaves a nested +-- naming environment. +-- +-- The `flatten` operation produces a single-layer Data.Map that +-- contains all the visible mappings. (That is, duplicate keys in +-- outer scopes are suppressed.) +-- +-- Other operations correspond to the ordinary operations on +-- Data.Map. Operations that generate collections (e.g. @keys@) come +-- in two versions: one that preserves the scope structure +-- (generally called @scoped@), and one that flattens it (generally +-- called @all@). +-- +-- In principle we should provide all the operations on Data.Map. +-- However, the implementation has been lazily evaluated and the +-- operations present are the ones that have been needed so far. +-- Add more as desired. + +module SAWSupport.ScopedMap ( + ScopedMap, -- opaque + push, + pop, + empty, + seed, + insert, + lookup, + filter, + scopedAssocs, + flatten, + allKeys, + allKeysSet + ) where + +import Prelude hiding (lookup, filter) + +import qualified Data.List.NonEmpty as N +import Data.List.NonEmpty (NonEmpty( (:|) )) +import Data.Foldable (toList) +--import qualified Data.Set as Set +import Data.Set (Set) +import qualified Data.Map as Map +import Data.Map (Map) + +import SAWSupport.Panic (panic) + + +-- | The type of scoped maps. +-- +-- The list of scopes is a `NonEmpty` to avoid unnecessary +-- degenerate cases. +newtype ScopedMap k v = ScopedMap (NonEmpty (Map k v)) + +-- | Push a new scope. +push :: Ord k => ScopedMap k v -> ScopedMap k v +push (ScopedMap scopes) = + ScopedMap $ N.cons Map.empty scopes + +-- | Pop and discard the most recent scope. +-- +-- Popping the last scope is an error and will panic. +pop :: Ord k => ScopedMap k v -> ScopedMap k v +pop (ScopedMap (_ :| more)) = case more of + [] -> + panic "pop" ["Popping topmost scope"] + s : more' -> + ScopedMap (s :| more') + +-- | An empty ScopedMap, with a single empty scope. +empty :: Ord k => ScopedMap k v +empty = + ScopedMap (Map.empty :| []) + +-- | Initialize a ScopedMap from a Map, which becomes the current (and +-- only) scope. +seed :: Ord k => Map k v -> ScopedMap k v +seed m = + ScopedMap (m :| []) + +-- | Insert into a ScopedMap. Always inserts in the innermost (most +-- recent) scope. +insert :: Ord k => k -> v -> ScopedMap k v -> ScopedMap k v +insert k v (ScopedMap (s :| more)) = + let s' = Map.insert k v s in + ScopedMap (s' :| more) + +-- | Look up a key in a ScopedMap. Checks all the scopes with the most +-- recent first. +lookup :: Ord k => k -> ScopedMap k v -> Maybe v +lookup k (ScopedMap (s0 :| more0)) = + let visit s more = case Map.lookup k s of + Just result -> Just result + Nothing -> case more of + [] -> Nothing + s' : more' -> visit s' more' + in + visit s0 more0 + +-- | Drop entries that don't match a predicate. +filter :: Ord k => (v -> Bool) -> ScopedMap k v -> ScopedMap k v +filter keep (ScopedMap (s :| more)) = + ScopedMap (Map.filter keep s :| map (Map.filter keep) more) + +-- | Return Map.assocs for each scope, preserving the scope boundaries. +-- The head of the returned list is the most recent scope. +scopedAssocs :: Ord k => ScopedMap k v -> [[(k, v)]] +scopedAssocs (ScopedMap scopes) = + map Map.assocs $ toList scopes + +-- FUTURE: add scopedKeys, scopedKeysSet + +-- | Convert to a plain map by folding the scopes together. Duplicate +-- bindings in more recent scopes take priority. +flatten :: Ord k => ScopedMap k v -> Map k v +flatten (ScopedMap (s0 :| more0)) = + let visit s more = + let result = case more of + [] -> Map.empty + s' : more' -> visit s' more' + in + -- Map.union gives its left argument priority given a + -- duplicate key. + Map.union s result + in + visit s0 more0 + +--FUTURE: add allAssocs + +-- | Return all keys, ignoring scope. +allKeys :: Ord k => ScopedMap k v -> [k] +allKeys m = + Map.keys $ flatten m + +-- | Return all keys as a set, ignoring scope. +allKeysSet :: Ord k => ScopedMap k v -> Set k +allKeysSet m = + Map.keysSet $ flatten m diff --git a/saw.cabal b/saw.cabal index 607c8ed4e7..8f9219de39 100644 --- a/saw.cabal +++ b/saw.cabal @@ -87,6 +87,9 @@ library saw-support exposed-modules: SAWSupport.PanicSupport SAWSupport.Pretty + SAWSupport.ScopedMap + other-modules: + SAWSupport.Panic ------------------------------------------------------------ From 3fcab1b692631101245fbed7cb8bed660621df85 Mon Sep 17 00:00:00 2001 From: David Holland Date: Wed, 15 Oct 2025 23:42:10 -0400 Subject: [PATCH 03/13] test_sawscript_builtins: Add two more cases of "undefined". These mysteriously behave differently; undefined9 crashes and undefined8 doesn't, even though they're almost identical and _should_, one would _think_, have the same eval behavior up to the point where "undefined" appears. Like undefined7, this is probably a function of the strange way the SAWScript interpreter handles its variable environments. I've been sitting on these for a while; not sure why I didn't merge them before. --- intTests/test_sawscript_builtins/undefined8.log.good | 4 ++++ intTests/test_sawscript_builtins/undefined8.saw | 7 +++++++ intTests/test_sawscript_builtins/undefined9.log.good | 5 +++++ intTests/test_sawscript_builtins/undefined9.saw | 5 +++++ 4 files changed, 21 insertions(+) create mode 100644 intTests/test_sawscript_builtins/undefined8.log.good create mode 100644 intTests/test_sawscript_builtins/undefined8.saw create mode 100644 intTests/test_sawscript_builtins/undefined9.log.good create mode 100644 intTests/test_sawscript_builtins/undefined9.saw diff --git a/intTests/test_sawscript_builtins/undefined8.log.good b/intTests/test_sawscript_builtins/undefined8.log.good new file mode 100644 index 0000000000..eb19d779bc --- /dev/null +++ b/intTests/test_sawscript_builtins/undefined8.log.good @@ -0,0 +1,4 @@ + Loading file "undefined8.saw" + oops didn't die + () + oops still didn't die diff --git a/intTests/test_sawscript_builtins/undefined8.saw b/intTests/test_sawscript_builtins/undefined8.saw new file mode 100644 index 0000000000..e3a3551c1f --- /dev/null +++ b/intTests/test_sawscript_builtins/undefined8.saw @@ -0,0 +1,7 @@ +// This does not crash, unlike undefined9. It isn't obvious +// what's different. + +let y = let x = undefined in (); +print "oops didn't die"; +print y; +print "oops still didn't die"; diff --git a/intTests/test_sawscript_builtins/undefined9.log.good b/intTests/test_sawscript_builtins/undefined9.log.good new file mode 100644 index 0000000000..536b0de089 --- /dev/null +++ b/intTests/test_sawscript_builtins/undefined9.log.good @@ -0,0 +1,5 @@ + Loading file "undefined9.saw" + interpret: undefined +CallStack (from HasCallStack): + error, called at saw-script/src/SAWScript/Interpreter.hs +FAILED diff --git a/intTests/test_sawscript_builtins/undefined9.saw b/intTests/test_sawscript_builtins/undefined9.saw new file mode 100644 index 0000000000..27d92c77cb --- /dev/null +++ b/intTests/test_sawscript_builtins/undefined9.saw @@ -0,0 +1,5 @@ +// This crashes immediately. + +let y = let x = undefined in return (); +print "oops didn't die"; + From abe229810d5eae634c3aba8509d05cc9c409bec6 Mon Sep 17 00:00:00 2001 From: David Holland Date: Thu, 16 Oct 2025 00:12:35 -0400 Subject: [PATCH 04/13] test1646: Renumber tests. There's about to be more than ten tests in here; insert zeros so things run in the expected order. For git safety this commit contains only renames; since the filenames appear in the reference outputs, they'll be updated next. --- intTests/test1646/{test1.log.good => test01.log.good} | 0 intTests/test1646/{test1.saw => test01.saw} | 0 intTests/test1646/{test2.log.good => test02.log.good} | 0 intTests/test1646/{test2.saw => test02.saw} | 0 intTests/test1646/{test3.log.good => test03.log.good} | 0 intTests/test1646/{test3.saw => test03.saw} | 0 intTests/test1646/{test4.log.good => test04.log.good} | 0 intTests/test1646/{test4.saw => test04.saw} | 0 intTests/test1646/{test5.log.good => test05.log.good} | 0 intTests/test1646/{test5.saw => test05.saw} | 0 intTests/test1646/{test6.log.good => test06.log.good} | 0 intTests/test1646/{test6.saw => test06.saw} | 0 intTests/test1646/{test7.log.good => test07.log.good} | 0 intTests/test1646/{test7.saw => test07.saw} | 0 intTests/test1646/{test8.log.good => test08.log.good} | 0 intTests/test1646/{test8.saw => test08.saw} | 0 16 files changed, 0 insertions(+), 0 deletions(-) rename intTests/test1646/{test1.log.good => test01.log.good} (100%) rename intTests/test1646/{test1.saw => test01.saw} (100%) rename intTests/test1646/{test2.log.good => test02.log.good} (100%) rename intTests/test1646/{test2.saw => test02.saw} (100%) rename intTests/test1646/{test3.log.good => test03.log.good} (100%) rename intTests/test1646/{test3.saw => test03.saw} (100%) rename intTests/test1646/{test4.log.good => test04.log.good} (100%) rename intTests/test1646/{test4.saw => test04.saw} (100%) rename intTests/test1646/{test5.log.good => test05.log.good} (100%) rename intTests/test1646/{test5.saw => test05.saw} (100%) rename intTests/test1646/{test6.log.good => test06.log.good} (100%) rename intTests/test1646/{test6.saw => test06.saw} (100%) rename intTests/test1646/{test7.log.good => test07.log.good} (100%) rename intTests/test1646/{test7.saw => test07.saw} (100%) rename intTests/test1646/{test8.log.good => test08.log.good} (100%) rename intTests/test1646/{test8.saw => test08.saw} (100%) diff --git a/intTests/test1646/test1.log.good b/intTests/test1646/test01.log.good similarity index 100% rename from intTests/test1646/test1.log.good rename to intTests/test1646/test01.log.good diff --git a/intTests/test1646/test1.saw b/intTests/test1646/test01.saw similarity index 100% rename from intTests/test1646/test1.saw rename to intTests/test1646/test01.saw diff --git a/intTests/test1646/test2.log.good b/intTests/test1646/test02.log.good similarity index 100% rename from intTests/test1646/test2.log.good rename to intTests/test1646/test02.log.good diff --git a/intTests/test1646/test2.saw b/intTests/test1646/test02.saw similarity index 100% rename from intTests/test1646/test2.saw rename to intTests/test1646/test02.saw diff --git a/intTests/test1646/test3.log.good b/intTests/test1646/test03.log.good similarity index 100% rename from intTests/test1646/test3.log.good rename to intTests/test1646/test03.log.good diff --git a/intTests/test1646/test3.saw b/intTests/test1646/test03.saw similarity index 100% rename from intTests/test1646/test3.saw rename to intTests/test1646/test03.saw diff --git a/intTests/test1646/test4.log.good b/intTests/test1646/test04.log.good similarity index 100% rename from intTests/test1646/test4.log.good rename to intTests/test1646/test04.log.good diff --git a/intTests/test1646/test4.saw b/intTests/test1646/test04.saw similarity index 100% rename from intTests/test1646/test4.saw rename to intTests/test1646/test04.saw diff --git a/intTests/test1646/test5.log.good b/intTests/test1646/test05.log.good similarity index 100% rename from intTests/test1646/test5.log.good rename to intTests/test1646/test05.log.good diff --git a/intTests/test1646/test5.saw b/intTests/test1646/test05.saw similarity index 100% rename from intTests/test1646/test5.saw rename to intTests/test1646/test05.saw diff --git a/intTests/test1646/test6.log.good b/intTests/test1646/test06.log.good similarity index 100% rename from intTests/test1646/test6.log.good rename to intTests/test1646/test06.log.good diff --git a/intTests/test1646/test6.saw b/intTests/test1646/test06.saw similarity index 100% rename from intTests/test1646/test6.saw rename to intTests/test1646/test06.saw diff --git a/intTests/test1646/test7.log.good b/intTests/test1646/test07.log.good similarity index 100% rename from intTests/test1646/test7.log.good rename to intTests/test1646/test07.log.good diff --git a/intTests/test1646/test7.saw b/intTests/test1646/test07.saw similarity index 100% rename from intTests/test1646/test7.saw rename to intTests/test1646/test07.saw diff --git a/intTests/test1646/test8.log.good b/intTests/test1646/test08.log.good similarity index 100% rename from intTests/test1646/test8.log.good rename to intTests/test1646/test08.log.good diff --git a/intTests/test1646/test8.saw b/intTests/test1646/test08.saw similarity index 100% rename from intTests/test1646/test8.saw rename to intTests/test1646/test08.saw From 088f94827e9ce5ec7b5d68c9574a9c8b614f2392 Mon Sep 17 00:00:00 2001 From: David Holland Date: Thu, 16 Oct 2025 00:24:02 -0400 Subject: [PATCH 05/13] test1646: Update reference outputs for previous. (mechanical changes only) --- intTests/test1646/test01.log.good | 6 +++--- intTests/test1646/test02.log.good | 6 +++--- intTests/test1646/test03.log.good | 6 +++--- intTests/test1646/test04.log.good | 6 +++--- intTests/test1646/test05.log.good | 2 +- intTests/test1646/test06.log.good | 10 +++++----- intTests/test1646/test07.log.good | 10 +++++----- intTests/test1646/test08.log.good | 10 +++++----- 8 files changed, 28 insertions(+), 28 deletions(-) diff --git a/intTests/test1646/test01.log.good b/intTests/test1646/test01.log.good index 94176e07f8..6c1406a55c 100644 --- a/intTests/test1646/test01.log.good +++ b/intTests/test1646/test01.log.good @@ -1,5 +1,5 @@ - Loading file "test1.saw" + Loading file "test01.saw" x=a - test1.saw:8:5-8:6: Warning: Redeclaration of x - test1.saw:3:5-3:6: Warning: Previous declaration was here + test01.saw:8:5-8:6: Warning: Redeclaration of x + test01.saw:3:5-3:6: Warning: Previous declaration was here x=b diff --git a/intTests/test1646/test02.log.good b/intTests/test1646/test02.log.good index 6b34e90901..f9427d0cef 100644 --- a/intTests/test1646/test02.log.good +++ b/intTests/test1646/test02.log.good @@ -1,7 +1,7 @@ - Loading file "test2.saw" + Loading file "test02.saw" x=a - test2.saw:8:5-8:6: Warning: Redeclaration of x - test2.saw:3:5-3:6: Warning: Previous declaration was here + test02.saw:8:5-8:6: Warning: Redeclaration of x + test02.saw:3:5-3:6: Warning: Previous declaration was here fromValue Text CallStack (from HasCallStack): error, called at saw-script/src/SAWScript/Interpreter.hs diff --git a/intTests/test1646/test03.log.good b/intTests/test1646/test03.log.good index 8d4035fdd6..ae4020811c 100644 --- a/intTests/test1646/test03.log.good +++ b/intTests/test1646/test03.log.good @@ -1,5 +1,5 @@ - Loading file "test3.saw" - test3.saw:9:8-9:9: Warning: Redeclaration of x - test3.saw:4:8-4:9: Warning: Previous declaration was here + Loading file "test03.saw" + test03.saw:9:8-9:9: Warning: Redeclaration of x + test03.saw:4:8-4:9: Warning: Previous declaration was here x=a x=a diff --git a/intTests/test1646/test04.log.good b/intTests/test1646/test04.log.good index a64bdf5c47..80b2647e97 100644 --- a/intTests/test1646/test04.log.good +++ b/intTests/test1646/test04.log.good @@ -1,5 +1,5 @@ - Loading file "test4.saw" - test4.saw:9:8-9:9: Warning: Redeclaration of x - test4.saw:4:8-4:9: Warning: Previous declaration was here + Loading file "test04.saw" + test04.saw:9:8-9:9: Warning: Redeclaration of x + test04.saw:4:8-4:9: Warning: Previous declaration was here x=a x=a diff --git a/intTests/test1646/test05.log.good b/intTests/test1646/test05.log.good index 2aa2944713..607fa10161 100644 --- a/intTests/test1646/test05.log.good +++ b/intTests/test1646/test05.log.good @@ -1,3 +1,3 @@ - Loading file "test5.saw" + Loading file "test05.saw" x=a x=b diff --git a/intTests/test1646/test06.log.good b/intTests/test1646/test06.log.good index e3d16fe2de..6e470ceed5 100644 --- a/intTests/test1646/test06.log.good +++ b/intTests/test1646/test06.log.good @@ -1,13 +1,13 @@ - Loading file "test6.saw" + Loading file "test06.saw" x=a - test6.saw:8:16-8:17: Type mismatch. + test06.saw:8:16-8:17: Type mismatch. Mismatch of type constructors. Expected: Int but got String - test6.saw:8:20-8:21: The type Int arises from the type of this term - test6.saw:3:20-3:23: The type String arises from the type of this term + test06.saw:8:20-8:21: The type Int arises from the type of this term + test06.saw:3:20-3:23: The type String arises from the type of this term Expected: Int Found: String - within "x" (test6.saw:8:16-8:17) + within "x" (test06.saw:8:16-8:17) FAILED diff --git a/intTests/test1646/test07.log.good b/intTests/test1646/test07.log.good index 8d094e0390..b541b3f4b9 100644 --- a/intTests/test1646/test07.log.good +++ b/intTests/test1646/test07.log.good @@ -1,8 +1,8 @@ - Loading file "test7.saw" + Loading file "test07.saw" Type errors: - test7.saw:4:4-4:26: Invalid use of 'rebindable' - test7.saw:4:4-4:26: It is only allowed at the syntactic top level - test7.saw:9:4-9:26: Invalid use of 'rebindable' - test7.saw:9:4-9:26: It is only allowed at the syntactic top level + test07.saw:4:4-4:26: Invalid use of 'rebindable' + test07.saw:4:4-4:26: It is only allowed at the syntactic top level + test07.saw:9:4-9:26: Invalid use of 'rebindable' + test07.saw:9:4-9:26: It is only allowed at the syntactic top level FAILED diff --git a/intTests/test1646/test08.log.good b/intTests/test1646/test08.log.good index 8cf4e9e85a..e7e24e874d 100644 --- a/intTests/test1646/test08.log.good +++ b/intTests/test1646/test08.log.good @@ -1,8 +1,8 @@ - Loading file "test8.saw" + Loading file "test08.saw" Type errors: - test8.saw:4:4-4:26: Invalid use of 'rebindable' - test8.saw:4:4-4:26: It is only allowed at the syntactic top level - test8.saw:9:4-9:26: Invalid use of 'rebindable' - test8.saw:9:4-9:26: It is only allowed at the syntactic top level + test08.saw:4:4-4:26: Invalid use of 'rebindable' + test08.saw:4:4-4:26: It is only allowed at the syntactic top level + test08.saw:9:4-9:26: Invalid use of 'rebindable' + test08.saw:9:4-9:26: It is only allowed at the syntactic top level FAILED From da25e63275b49af225151060234c2db0e79be3f2 Mon Sep 17 00:00:00 2001 From: David Holland Date: Wed, 15 Oct 2025 23:54:54 -0400 Subject: [PATCH 06/13] Add a bunch more "let rebindable" tests to intTests/test1646. They don't all work yet. --- intTests/test1646/test09.log.good | 4 + intTests/test1646/test09.saw | 11 + intTests/test1646/test10.log.good | 4 + intTests/test1646/test10.saw | 11 + intTests/test1646/test11.log.good | 5 + intTests/test1646/test11.saw | 12 ++ intTests/test1646/test12.log.good | 7 + intTests/test1646/test12.saw | 13 ++ intTests/test1646/test13.log.good | 9 + intTests/test1646/test13.saw | 16 ++ intTests/test1646/test14.log.good | 6 + intTests/test1646/test14.saw | 13 ++ intTests/test1646/test15.isaw | 4 + intTests/test1646/test15.log.good | 348 ++++++++++++++++++++++++++++++ 14 files changed, 463 insertions(+) create mode 100644 intTests/test1646/test09.log.good create mode 100644 intTests/test1646/test09.saw create mode 100644 intTests/test1646/test10.log.good create mode 100644 intTests/test1646/test10.saw create mode 100644 intTests/test1646/test11.log.good create mode 100644 intTests/test1646/test11.saw create mode 100644 intTests/test1646/test12.log.good create mode 100644 intTests/test1646/test12.saw create mode 100644 intTests/test1646/test13.log.good create mode 100644 intTests/test1646/test13.saw create mode 100644 intTests/test1646/test14.log.good create mode 100644 intTests/test1646/test14.saw create mode 100644 intTests/test1646/test15.isaw create mode 100644 intTests/test1646/test15.log.good diff --git a/intTests/test1646/test09.log.good b/intTests/test1646/test09.log.good new file mode 100644 index 0000000000..b3906ea246 --- /dev/null +++ b/intTests/test1646/test09.log.good @@ -0,0 +1,4 @@ + Loading file "test09.saw" + test09.saw:7:4-7:5: Warning: Redeclaration of x + test09.saw:4:16-4:17: Warning: Previous declaration was here + a diff --git a/intTests/test1646/test09.saw b/intTests/test1646/test09.saw new file mode 100644 index 0000000000..48b80a14b7 --- /dev/null +++ b/intTests/test1646/test09.saw @@ -0,0 +1,11 @@ +// This should print a. Binding x in a nested scope should have no +// effect. + +let rebindable x = "a"; + +do { + x <- return 3; + return (); +}; + +print x; diff --git a/intTests/test1646/test10.log.good b/intTests/test1646/test10.log.good new file mode 100644 index 0000000000..704f397d3c --- /dev/null +++ b/intTests/test1646/test10.log.good @@ -0,0 +1,4 @@ + Loading file "test10.saw" + test10.saw:7:8-7:9: Warning: Redeclaration of x + test10.saw:4:16-4:17: Warning: Previous declaration was here + a diff --git a/intTests/test1646/test10.saw b/intTests/test1646/test10.saw new file mode 100644 index 0000000000..28632b712c --- /dev/null +++ b/intTests/test1646/test10.saw @@ -0,0 +1,11 @@ +// This should print a. Binding x in a nested scope creates a new +// variable and should have no effect on the rebindable one. + +let rebindable x = "a"; + +do { + let x = 3; + return (); +}; + +print x; diff --git a/intTests/test1646/test11.log.good b/intTests/test1646/test11.log.good new file mode 100644 index 0000000000..8cd730fdca --- /dev/null +++ b/intTests/test1646/test11.log.good @@ -0,0 +1,5 @@ + Loading file "test11.saw" + test11.saw:6:8-6:9: Warning: Redeclaration of x + test11.saw:3:16-3:17: Warning: Previous declaration was here + 3 + b diff --git a/intTests/test1646/test11.saw b/intTests/test1646/test11.saw new file mode 100644 index 0000000000..9d7273fda5 --- /dev/null +++ b/intTests/test1646/test11.saw @@ -0,0 +1,12 @@ +// This should print 3 then b. + +let rebindable x = "a"; + +do { + let x = 3; + print x; + return (); +}; + +let rebindable x = "b"; +print x; diff --git a/intTests/test1646/test12.log.good b/intTests/test1646/test12.log.good new file mode 100644 index 0000000000..f7441a2570 --- /dev/null +++ b/intTests/test1646/test12.log.good @@ -0,0 +1,7 @@ + Loading file "test12.saw" + test12.saw:6:8-6:9: Warning: Redeclaration of x + test12.saw:3:16-3:17: Warning: Previous declaration was here + 3 + test12.saw:11:5-11:6: Warning: Redeclaration of x + test12.saw:3:16-3:17: Warning: Previous declaration was here + b diff --git a/intTests/test1646/test12.saw b/intTests/test1646/test12.saw new file mode 100644 index 0000000000..269f88b477 --- /dev/null +++ b/intTests/test1646/test12.saw @@ -0,0 +1,13 @@ +// This should print 3 then b. + +let rebindable x = "a"; + +do { + let x = 3; + print x; + return (); +}; + +let x = "b"; +print x; + diff --git a/intTests/test1646/test13.log.good b/intTests/test1646/test13.log.good new file mode 100644 index 0000000000..5537d3f2b8 --- /dev/null +++ b/intTests/test1646/test13.log.good @@ -0,0 +1,9 @@ + Loading file "test13.saw" + test13.saw:7:8-7:9: Warning: Redeclaration of x + test13.saw:4:16-4:17: Warning: Previous declaration was here + 3 + test13.saw:12:5-12:6: Warning: Redeclaration of x + test13.saw:4:16-4:17: Warning: Previous declaration was here + b + test13.saw:15:16-15:17: Cannot rebind x: Previous binding was not tagged 'rebindable' +FAILED diff --git a/intTests/test1646/test13.saw b/intTests/test1646/test13.saw new file mode 100644 index 0000000000..713e1eef4a --- /dev/null +++ b/intTests/test1646/test13.saw @@ -0,0 +1,16 @@ +// This is rejected; once the rebindable tag is dropped it can't be +// readded. + +let rebindable x = "a"; + +do { + let x = 3; + print x; + return (); +}; + +let x = "b"; +print x; + +let rebindable x = "c"; +print x; diff --git a/intTests/test1646/test14.log.good b/intTests/test1646/test14.log.good new file mode 100644 index 0000000000..01a52d821a --- /dev/null +++ b/intTests/test1646/test14.log.good @@ -0,0 +1,6 @@ + Loading file "test14.saw" + x=a + x=b + test14.saw:12:5-12:6: Warning: Redeclaration of x + test14.saw:9:16-9:17: Warning: Previous declaration was here + x=c diff --git a/intTests/test1646/test14.saw b/intTests/test1646/test14.saw new file mode 100644 index 0000000000..2a7c25fa43 --- /dev/null +++ b/intTests/test1646/test14.saw @@ -0,0 +1,13 @@ +// The second f call should print x=b. So should the third. +// XXX: currently the third prints x=c. + +let rebindable x = "a"; + +let f () = print (str_concat "x=" x); +f (); + +let rebindable x = "b"; +f (); + +let x = "c"; +f (); diff --git a/intTests/test1646/test15.isaw b/intTests/test1646/test15.isaw new file mode 100644 index 0000000000..8e96a0289d --- /dev/null +++ b/intTests/test1646/test15.isaw @@ -0,0 +1,4 @@ +let rebindable x = 3 +let rebindable y = 4 +let y = 5 +:env diff --git a/intTests/test1646/test15.log.good b/intTests/test1646/test15.log.good new file mode 100644 index 0000000000..4df51e0533 --- /dev/null +++ b/intTests/test1646/test15.log.good @@ -0,0 +1,348 @@ + :1:5-1:6: Warning: Redeclaration of y + :1:16-1:17: Warning: Previous declaration was here +abc : ProofScript () +abstract_symbolic : Term -> Term +add_cryptol_defs : [String] -> Simpset -> Simpset +add_cryptol_eqs : [String] -> Simpset -> Simpset +add_prelude_defs : [String] -> Simpset -> Simpset +add_prelude_eqs : [String] -> Simpset -> Simpset +add_x86_preserved_reg : String -> TopLevel () +addsimp : Theorem -> Simpset -> Simpset +addsimp_shallow : Theorem -> Simpset -> Simpset +addsimps : [Theorem] -> Simpset -> Simpset +admit : String -> ProofScript () +approxmc : Term -> TopLevel () +assume_unsat : ProofScript () +assume_valid : ProofScript () +auto_match : String -> String -> TopLevel () +basic_ss : Simpset +beta_reduce_goal : ProofScript () +beta_reduce_term : Term -> Term +bitblast : Term -> TopLevel AIG +bitwuzla : ProofScript () +boolector : ProofScript () +caseProofResult : {b} ProofResult -> (Theorem -> b) -> (Term -> b) -> b +caseSatResult : {b} SatResult -> b -> (Term -> b) -> b +check_convertible : Term -> Term -> TopLevel () +check_goal : ProofScript () +check_term : Term -> TopLevel () +clean_mismatched_versions_solver_cache : TopLevel () +codegen : String -> [String] -> String -> Term -> TopLevel () +concat : {a} [a] -> [a] -> [a] +core_axiom : String -> Theorem +core_thm : String -> Theorem +crucible_alloc : LLVMType -> LLVMSetup SetupValue +crucible_alloc_aligned : Int -> LLVMType -> LLVMSetup SetupValue +crucible_alloc_global : String -> LLVMSetup () +crucible_alloc_readonly : LLVMType -> LLVMSetup SetupValue +crucible_alloc_readonly_aligned : Int -> LLVMType -> LLVMSetup SetupValue +crucible_array : [SetupValue] -> SetupValue +crucible_conditional_points_to : Term -> SetupValue -> SetupValue -> LLVMSetup () +crucible_conditional_points_to_untyped : Term -> SetupValue -> SetupValue -> LLVMSetup () +crucible_declare_ghost_state : String -> TopLevel Ghost +crucible_elem : SetupValue -> Int -> SetupValue +crucible_equal : SetupValue -> SetupValue -> LLVMSetup () +crucible_execute_func : [SetupValue] -> LLVMSetup () +crucible_field : SetupValue -> String -> SetupValue +crucible_fresh_expanded_val : LLVMType -> LLVMSetup SetupValue +crucible_fresh_pointer : LLVMType -> LLVMSetup SetupValue +crucible_fresh_var : String -> LLVMType -> LLVMSetup Term +crucible_ghost_value : Ghost -> Term -> LLVMSetup () +crucible_global : String -> SetupValue +crucible_global_initializer : String -> SetupValue +crucible_java_extract : JavaClass -> String -> TopLevel Term +crucible_llvm_extract : LLVMModule -> String -> TopLevel Term +crucible_llvm_unsafe_assume_spec : LLVMModule -> String -> LLVMSetup () -> TopLevel LLVMSpec +crucible_llvm_verify : LLVMModule -> String -> [LLVMSpec] -> Bool -> LLVMSetup () -> ProofScript () -> TopLevel LLVMSpec +crucible_null : SetupValue +crucible_packed_struct : [SetupValue] -> SetupValue +crucible_points_to : SetupValue -> SetupValue -> LLVMSetup () +crucible_points_to_untyped : SetupValue -> SetupValue -> LLVMSetup () +crucible_postcond : Term -> LLVMSetup () +crucible_precond : Term -> LLVMSetup () +crucible_return : SetupValue -> LLVMSetup () +crucible_spec_size : LLVMSpec -> Int +crucible_spec_solvers : LLVMSpec -> [String] +crucible_struct : [SetupValue] -> SetupValue +crucible_symbolic_alloc : Bool -> Int -> Term -> LLVMSetup SetupValue +crucible_term : Term -> SetupValue +cryptol_add_path : String -> TopLevel () +cryptol_extract : CryptolModule -> String -> TopLevel Term +cryptol_load : String -> TopLevel CryptolModule +cryptol_prims : () -> CryptolModule +cryptol_ss : () -> Simpset +cvc4 : ProofScript () +cvc5 : ProofScript () +declare_ghost_state : String -> TopLevel Ghost +default_x86_preserved_reg : TopLevel () +define : String -> Term -> TopLevel Term +disable_alloc_sym_init_check : TopLevel () +disable_crucible_assert_then_assume : TopLevel () +disable_crucible_profiling : TopLevel () +disable_debug_intrinsics : TopLevel () +disable_lax_arithmetic : TopLevel () +disable_lax_loads_and_stores : TopLevel () +disable_lax_pointer_ordering : TopLevel () +disable_smt_array_memory_model : TopLevel () +disable_what4_eval : TopLevel () +disable_what4_hash_consing : TopLevel () +disable_x86_what4_hash_consing : TopLevel () +dsec_print : Term -> Term -> TopLevel () +dump_file_AST : String -> TopLevel () +empty_ss : Simpset +enable_crucible_assert_then_assume : TopLevel () +enable_crucible_profiling : String -> TopLevel () +enable_debug_intrinsics : TopLevel () +enable_deprecated : TopLevel () +enable_experimental : TopLevel () +enable_lax_arithmetic : TopLevel () +enable_lax_loads_and_stores : TopLevel () +enable_lax_pointer_ordering : TopLevel () +enable_smt_array_memory_model : TopLevel () +enable_what4_hash_consing : TopLevel () +env : TopLevel () +eval_bool : Term -> Bool +eval_int : Term -> Int +eval_list : Term -> [Term] +eval_size : Type -> Int +exec : String -> [String] -> String -> TopLevel String +exit : Int -> TopLevel () +external_aig_solver : String -> [String] -> ProofScript () +external_cnf_solver : String -> [String] -> ProofScript () +fail : {a} String -> TopLevel a +fails : {a} TopLevel a -> TopLevel () +false : Bool +for : {m, a, b} [a] -> (a -> m b) -> m [b] +fresh_symbolic : String -> Type -> TopLevel Term +get_env : String -> String +get_nopts : () -> Int +get_opt : Int -> String +goal_eval : ProofScript () +goal_eval_unint : [String] -> ProofScript () +goal_num : ProofScript Int +head : {a} [a] -> a +hoist_ifs : Term -> TopLevel Term +include : String -> TopLevel () +int_to_term : Int -> Term +is_convertible : Term -> Term -> TopLevel Bool +java_array : Int -> JavaType -> JavaType +java_bool : JavaType +java_byte : JavaType +java_char : JavaType +java_class : String -> JavaType +java_double : JavaType +java_float : JavaType +java_int : JavaType +java_load_class : String -> TopLevel JavaClass +java_long : JavaType +java_short : JavaType +jvm_alloc_array : Int -> JavaType -> JVMSetup JVMValue +jvm_alloc_object : String -> JVMSetup JVMValue +jvm_array_is : JVMValue -> Term -> JVMSetup () +jvm_assert : Term -> JVMSetup () +jvm_elem_is : JVMValue -> Int -> JVMValue -> JVMSetup () +jvm_equal : JVMValue -> JVMValue -> JVMSetup () +jvm_execute_func : [JVMValue] -> JVMSetup () +jvm_extract : JavaClass -> String -> TopLevel Term +jvm_field_is : JVMValue -> String -> JVMValue -> JVMSetup () +jvm_fresh_var : String -> JavaType -> JVMSetup Term +jvm_ghost_value : Ghost -> Term -> JVMSetup () +jvm_modifies_array : JVMValue -> JVMSetup () +jvm_modifies_elem : JVMValue -> Int -> JVMSetup () +jvm_modifies_field : JVMValue -> String -> JVMSetup () +jvm_modifies_static_field : String -> JVMSetup () +jvm_null : JVMValue +jvm_postcond : Term -> JVMSetup () +jvm_precond : Term -> JVMSetup () +jvm_return : JVMValue -> JVMSetup () +jvm_static_field_is : String -> JVMValue -> JVMSetup () +jvm_term : Term -> JVMValue +jvm_unint : [String] -> JVMSetup () +jvm_unsafe_assume_spec : JavaClass -> String -> JVMSetup () -> TopLevel JVMSpec +jvm_verify : JavaClass -> String -> [JVMSpec] -> Bool -> JVMSetup () -> ProofScript () -> TopLevel JVMSpec +lambda : Term -> Term -> Term +lambdas : [Term] -> Term -> Term +length : {a} [a] -> Int +list_term : [Term] -> Term +llvm_alias : String -> LLVMType +llvm_alloc : LLVMType -> LLVMSetup SetupValue +llvm_alloc_aligned : Int -> LLVMType -> LLVMSetup SetupValue +llvm_alloc_global : String -> LLVMSetup () +llvm_alloc_readonly : LLVMType -> LLVMSetup SetupValue +llvm_alloc_readonly_aligned : Int -> LLVMType -> LLVMSetup SetupValue +llvm_array : Int -> LLVMType -> LLVMType +llvm_array_value : [SetupValue] -> SetupValue +llvm_assert : Term -> LLVMSetup () +llvm_cast_pointer : SetupValue -> LLVMType -> SetupValue +llvm_cfg : LLVMModule -> String -> TopLevel CFG +llvm_conditional_points_to : Term -> SetupValue -> SetupValue -> LLVMSetup () +llvm_conditional_points_to_at_type : Term -> SetupValue -> LLVMType -> SetupValue -> LLVMSetup () +llvm_conditional_points_to_untyped : Term -> SetupValue -> SetupValue -> LLVMSetup () +llvm_declare_ghost_state : String -> TopLevel Ghost +llvm_double : LLVMType +llvm_elem : SetupValue -> Int -> SetupValue +llvm_equal : SetupValue -> SetupValue -> LLVMSetup () +llvm_execute_func : [SetupValue] -> LLVMSetup () +llvm_extract : LLVMModule -> String -> TopLevel Term +llvm_field : SetupValue -> String -> SetupValue +llvm_float : LLVMType +llvm_fresh_expanded_val : LLVMType -> LLVMSetup SetupValue +llvm_fresh_pointer : LLVMType -> LLVMSetup SetupValue +llvm_fresh_var : String -> LLVMType -> LLVMSetup Term +llvm_ghost_value : Ghost -> Term -> LLVMSetup () +llvm_global : String -> SetupValue +llvm_global_initializer : String -> SetupValue +llvm_int : Int -> LLVMType +llvm_load_module : String -> TopLevel LLVMModule +llvm_null : SetupValue +llvm_packed_struct_type : [LLVMType] -> LLVMType +llvm_packed_struct_value : [SetupValue] -> SetupValue +llvm_pointer : LLVMType -> LLVMType +llvm_points_to : SetupValue -> SetupValue -> LLVMSetup () +llvm_points_to_at_type : SetupValue -> LLVMType -> SetupValue -> LLVMSetup () +llvm_points_to_untyped : SetupValue -> SetupValue -> LLVMSetup () +llvm_postcond : Term -> LLVMSetup () +llvm_precond : Term -> LLVMSetup () +llvm_return : SetupValue -> LLVMSetup () +llvm_sizeof : LLVMModule -> LLVMType -> Int +llvm_spec_size : LLVMSpec -> Int +llvm_spec_solvers : LLVMSpec -> [String] +llvm_struct : String -> LLVMType +llvm_struct_type : [LLVMType] -> LLVMType +llvm_struct_value : [SetupValue] -> SetupValue +llvm_symbolic_alloc : Bool -> Int -> Term -> LLVMSetup SetupValue +llvm_term : Term -> SetupValue +llvm_type : String -> LLVMType +llvm_unint : [String] -> LLVMSetup () +llvm_union : SetupValue -> String -> SetupValue +llvm_unsafe_assume_spec : LLVMModule -> String -> LLVMSetup () -> TopLevel LLVMSpec +llvm_verify : LLVMModule -> String -> [LLVMSpec] -> Bool -> LLVMSetup () -> ProofScript () -> TopLevel LLVMSpec +load_aig : String -> TopLevel AIG +mathsat : ProofScript () +mir_unint : [String] -> MIRSetup () +nat_to_term : Int -> Term +nth : {a} [a] -> Int -> a +null : {a} [a] -> Bool +offline_aig : String -> ProofScript () +offline_aig_external : String -> ProofScript () +offline_cnf : String -> ProofScript () +offline_cnf_external : String -> ProofScript () +offline_extcore : String -> ProofScript () +offline_smtlib2 : String -> ProofScript () +offline_unint_smtlib2 : [String] -> String -> ProofScript () +offline_w4_unint_bitwuzla : [String] -> String -> ProofScript () +offline_w4_unint_cvc4 : [String] -> String -> ProofScript () +offline_w4_unint_cvc5 : [String] -> String -> ProofScript () +offline_w4_unint_yices : [String] -> String -> ProofScript () +offline_w4_unint_z3 : [String] -> String -> ProofScript () +parse_core : String -> Term +parse_core_mod : String -> String -> Term +parser_printer_roundtrip : String -> TopLevel () +print : {a} a -> TopLevel () +print_goal : ProofScript () +print_goal_consts : ProofScript () +print_goal_depth : Int -> ProofScript () +print_goal_inline : [Int] -> ProofScript () +print_goal_size : ProofScript () +print_goal_summary : ProofScript () +print_solver_cache : String -> TopLevel () +print_solver_cache_stats : TopLevel () +print_term : Term -> TopLevel () +print_term_depth : Int -> Term -> TopLevel () +print_type : Term -> TopLevel () +prove : ProofScript () -> Term -> TopLevel ProofResult +prove_core : ProofScript () -> String -> TopLevel Theorem +prove_extcore : ProofScript () -> Term -> TopLevel Theorem +prove_print : ProofScript () -> Term -> TopLevel Theorem +qc_print : Int -> Term -> TopLevel () +quickcheck : Int -> ProofScript () +read_aig : String -> TopLevel Term +read_bytes : String -> TopLevel Term +read_core : String -> TopLevel Term +replace : Term -> Term -> Term -> TopLevel Term +return : {m, a} a -> m a +rewrite : Simpset -> Term -> Term +rme : ProofScript () +run : {a} TopLevel a -> a +sat : ProofScript () -> Term -> TopLevel SatResult +sat_print : ProofScript () -> Term -> TopLevel () +save_aig : String -> AIG -> TopLevel () +save_aig_as_cnf : String -> AIG -> TopLevel () +sbv_abc : ProofScript () +sbv_bitwuzla : ProofScript () +sbv_boolector : ProofScript () +sbv_cvc4 : ProofScript () +sbv_cvc5 : ProofScript () +sbv_mathsat : ProofScript () +sbv_unint_bitwuzla : [String] -> ProofScript () +sbv_unint_cvc4 : [String] -> ProofScript () +sbv_unint_cvc5 : [String] -> ProofScript () +sbv_unint_yices : [String] -> ProofScript () +sbv_unint_z3 : [String] -> ProofScript () +sbv_yices : ProofScript () +sbv_z3 : ProofScript () +set_ascii : Bool -> TopLevel () +set_base : Int -> TopLevel () +set_color : Bool -> TopLevel () +set_memoization_hash : Int -> TopLevel () +set_memoization_hash_incremental : Int -> TopLevel () +set_memoization_incremental : TopLevel () +set_min_sharing : Int -> TopLevel () +set_solver_cache_path : String -> TopLevel () +set_solver_cache_timeout : Int -> TopLevel () +sharpSAT : Term -> TopLevel Integer +show : {a} a -> String +show_cfg : CFG -> String +show_term : Term -> String +simplify : Simpset -> ProofScript () +simplify_local : [Int] -> Simpset -> ProofScript () +size_to_term : Type -> Term +str_concat : String -> String -> String +str_concats : [String] -> String +tail : {a} [a] -> [a] +term_apply : Term -> [Term] -> Term +term_eval : Term -> Term +term_eval_unint : [String] -> Term -> Term +term_size : Term -> Int +term_tree_size : Term -> Int +test_solver_cache_stats : Int -> Int -> Int -> Int -> Int -> TopLevel () +time : {a} TopLevel a -> TopLevel a +trivial : ProofScript () +true : Bool +type : Term -> Type +undefined : {a} a +unfold_term : [String] -> Term -> Term +unfolding : [String] -> ProofScript () +unfolding_fix_once : [String] -> ProofScript () +unint_bitwuzla : [String] -> ProofScript () +unint_cvc4 : [String] -> ProofScript () +unint_cvc5 : [String] -> ProofScript () +unint_yices : [String] -> ProofScript () +unint_z3 : [String] -> ProofScript () +w4 : ProofScript () +w4_abc_aiger : ProofScript () +w4_abc_smtlib2 : ProofScript () +w4_abc_verilog : ProofScript () +w4_offline_smtlib2 : String -> ProofScript () +w4_unint_bitwuzla : [String] -> ProofScript () +w4_unint_cvc4 : [String] -> ProofScript () +w4_unint_cvc5 : [String] -> ProofScript () +w4_unint_rme : [String] -> ProofScript () +w4_unint_yices : [String] -> ProofScript () +w4_unint_z3 : [String] -> ProofScript () +w4_unint_z3_using : String -> [String] -> ProofScript () +with_time : {a} TopLevel a -> TopLevel (Int, a) +write_aig : String -> Term -> TopLevel () +write_aig_external : String -> Term -> TopLevel () +write_cnf : String -> Term -> TopLevel () +write_cnf_external : String -> Term -> TopLevel () +write_core : String -> Term -> TopLevel () +write_goal : String -> ProofScript () +write_saig : String -> Term -> TopLevel () +write_saig' : String -> Term -> Int -> TopLevel () +write_smtlib2 : String -> Term -> TopLevel () +write_smtlib2_w4 : String -> Term -> TopLevel () +x : Int +y : Int +yices : ProofScript () +z3 : ProofScript () From bf67874b9714275e54fc761a8f55d1125356f4fe Mon Sep 17 00:00:00 2001 From: David Holland Date: Fri, 17 Oct 2025 12:56:54 -0400 Subject: [PATCH 07/13] Add some tests for #2304 (Cryptol environment not scoped). The reference outputs here reflect the current behavior, not the desired behavior. --- intTests/test2304/.gitignore | 3 +++ intTests/test2304/Makefile | 5 +++++ intTests/test2304/test.sh | 1 + intTests/test2304/test01.log.good | 4 ++++ intTests/test2304/test01.saw | 8 ++++++++ intTests/test2304/test02.log.good | 11 +++++++++++ intTests/test2304/test02.saw | 8 ++++++++ intTests/test2304/test03.log.good | 11 +++++++++++ intTests/test2304/test03.saw | 12 ++++++++++++ intTests/test2304/test04.log.good | 7 +++++++ intTests/test2304/test04.saw | 12 ++++++++++++ intTests/test2304/test05.log.good | 7 +++++++ intTests/test2304/test05.saw | 12 ++++++++++++ 13 files changed, 101 insertions(+) create mode 100644 intTests/test2304/.gitignore create mode 100644 intTests/test2304/Makefile create mode 100644 intTests/test2304/test.sh create mode 100644 intTests/test2304/test01.log.good create mode 100644 intTests/test2304/test01.saw create mode 100644 intTests/test2304/test02.log.good create mode 100644 intTests/test2304/test02.saw create mode 100644 intTests/test2304/test03.log.good create mode 100644 intTests/test2304/test03.saw create mode 100644 intTests/test2304/test04.log.good create mode 100644 intTests/test2304/test04.saw create mode 100644 intTests/test2304/test05.log.good create mode 100644 intTests/test2304/test05.saw diff --git a/intTests/test2304/.gitignore b/intTests/test2304/.gitignore new file mode 100644 index 0000000000..4619758def --- /dev/null +++ b/intTests/test2304/.gitignore @@ -0,0 +1,3 @@ +*.rawlog +*.log +*.diff diff --git a/intTests/test2304/Makefile b/intTests/test2304/Makefile new file mode 100644 index 0000000000..c9e12c62ae --- /dev/null +++ b/intTests/test2304/Makefile @@ -0,0 +1,5 @@ +all: ; +clean: + sh ./test.sh clean + +.PHONY: all clean diff --git a/intTests/test2304/test.sh b/intTests/test2304/test.sh new file mode 100644 index 0000000000..5fcd79d0a6 --- /dev/null +++ b/intTests/test2304/test.sh @@ -0,0 +1 @@ +exec ${TEST_SHELL:-bash} ../support/test-and-diff.sh "$@" diff --git a/intTests/test2304/test01.log.good b/intTests/test2304/test01.log.good new file mode 100644 index 0000000000..bd786801af --- /dev/null +++ b/intTests/test2304/test01.log.good @@ -0,0 +1,4 @@ + Loading file "test01.saw" + test01.saw:4:11-4:12: Warning: Redeclaration of x + test01.saw:2:8-2:9: Warning: Previous declaration was here + True diff --git a/intTests/test2304/test01.saw b/intTests/test2304/test01.saw new file mode 100644 index 0000000000..2a2bf41b03 --- /dev/null +++ b/intTests/test2304/test01.saw @@ -0,0 +1,8 @@ +do { + let x = {{ 3 : [8] }}; + do { + let x = {{ 4 : Integer }}; + return (); + }; + print {{ x == (3 : [8]) }}; +}; diff --git a/intTests/test2304/test02.log.good b/intTests/test2304/test02.log.good new file mode 100644 index 0000000000..f70625d716 --- /dev/null +++ b/intTests/test2304/test02.log.good @@ -0,0 +1,11 @@ + Loading file "test02.saw" + Stack trace: + (builtin) (at top level) +Cryptol error: +[error] at test02.saw:7:19--7:26: + Type mismatch: + Expected type: Integer + Inferred type: [8] + When checking type of function argument + +FAILED diff --git a/intTests/test2304/test02.saw b/intTests/test2304/test02.saw new file mode 100644 index 0000000000..25c5ba1260 --- /dev/null +++ b/intTests/test2304/test02.saw @@ -0,0 +1,8 @@ +do { + let {{ x = 3 : [8] }}; + do { + let {{ x = 4 : Integer }}; + return (); + }; + print {{ x == (3 : [8]) }}; +}; diff --git a/intTests/test2304/test03.log.good b/intTests/test2304/test03.log.good new file mode 100644 index 0000000000..3e5dceb8f9 --- /dev/null +++ b/intTests/test2304/test03.log.good @@ -0,0 +1,11 @@ + Loading file "test03.saw" + Stack trace: + (builtin) (at top level) +Cryptol error: +[error] at test03.saw:11:19--11:26: + Type mismatch: + Expected type: Integer + Inferred type: [8] + When checking type of function argument + +FAILED diff --git a/intTests/test2304/test03.saw b/intTests/test2304/test03.saw new file mode 100644 index 0000000000..bcdd08fd69 --- /dev/null +++ b/intTests/test2304/test03.saw @@ -0,0 +1,12 @@ +do { + let {{ x = 3 : [8] }}; + do { + let {{ x = 4 : Integer }}; + return (); + }; + do { + let {{ x = 5 : Integer }}; + return (); + }; + print {{ x == (3 : [8]) }}; +}; diff --git a/intTests/test2304/test04.log.good b/intTests/test2304/test04.log.good new file mode 100644 index 0000000000..86278ed34e --- /dev/null +++ b/intTests/test2304/test04.log.good @@ -0,0 +1,7 @@ + Loading file "test04.saw" + ("a",\(u1218 : isort 0) -> + \(_P : PLiteral u1218) -> ecNumber (TCNum 3) u1218 _P) + ("b",\(u1218 : isort 0) -> + \(_P : PLiteral u1218) -> ecNumber (TCNum 4) u1218 _P) + ("c",\(u1218 : isort 0) -> + \(_P : PLiteral u1218) -> ecNumber (TCNum 5) u1218 _P) diff --git a/intTests/test2304/test04.saw b/intTests/test2304/test04.saw new file mode 100644 index 0000000000..e6cc34ccdf --- /dev/null +++ b/intTests/test2304/test04.saw @@ -0,0 +1,12 @@ +let f (x: Integer) = {{ `x }}; +let g (x: Integer) = return {{ `x }}; +let h (x: Integer) = do { return {{ `x }}; }; + +let a = f 3; +print ("a", a); + +b <- g 4; +print ("b", b); + +c <- h 5; +print ("c", c); diff --git a/intTests/test2304/test05.log.good b/intTests/test2304/test05.log.good new file mode 100644 index 0000000000..2b3f0fcc58 --- /dev/null +++ b/intTests/test2304/test05.log.good @@ -0,0 +1,7 @@ + Loading file "test05.saw" + ("a",\(u1218 : isort 0) -> + \(_P : PLiteral u1218) -> ecNumber (TCNum 3) u1218 _P) + ("b",\(u1218 : isort 0) -> + \(_P : PLiteral u1218) -> ecNumber (TCNum 4) u1218 _P) + ("c",\(u1218 : isort 0) -> + \(_P : PLiteral u1218) -> ecNumber (TCNum 5) u1218 _P) diff --git a/intTests/test2304/test05.saw b/intTests/test2304/test05.saw new file mode 100644 index 0000000000..acb881f5f0 --- /dev/null +++ b/intTests/test2304/test05.saw @@ -0,0 +1,12 @@ +let f (x: Integer) (y: Integer) = {{ `x }}; +let g (x: Integer) (y: Integer) = return {{ `x }}; +let h (x: Integer) (y: Integer) = do { return {{ `x }}; }; + +let a = f 3 6; +print ("a", a); + +b <- g 4 7; +print ("b", b); + +c <- h 5 8; +print ("c", c); From 8ffc3790fcaaf410648ccfcf5d2d1383b2d6025d Mon Sep 17 00:00:00 2001 From: David Holland Date: Mon, 20 Oct 2025 17:42:31 -0400 Subject: [PATCH 08/13] Simplify the ecdsa example a bit to avoid stepping on #2726. This removes uses of "let {{ thm = ... }}" followed by explicitly binding and unfolding "thm" with just binding a Cryptol-level lambda, like other code in the same file. This is simpler and probably better for an example regardless of other considerations. But also, the "let {{ thm = ... }}" binds a SAWCore-level name "thm", which causes errors about redefining it because the SAWCore environment doesn't get SAWScript-level scopes. That's #2726. After the upcoming fixes so the Cryptol environment _does_ get SAWScript-level scope handling it does, anyway. It isn't obvious why this code didn't already exhibit that behavior. Perhaps there's something down inside that overwrites the corresponding SAWCore definition when you overwrite a Cryptol definition, which no longer applies since we no longer do that. (And maybe that logic checks to make sure the SAWCore manipulation is sound, and maybe it doesn't...) Regardless, we have at least one other test that explicitly captures #2726. --- examples/ecdsa/ecdsa.saw | 65 ++++++++++++++++------------------------ 1 file changed, 26 insertions(+), 39 deletions(-) diff --git a/examples/ecdsa/ecdsa.saw b/examples/ecdsa/ecdsa.saw index 66e23645ee..9d9a5b8ed1 100644 --- a/examples/ecdsa/ecdsa.saw +++ b/examples/ecdsa/ecdsa.saw @@ -412,115 +412,102 @@ p384_point_ops_sub_simp <- do { }; p384_point_ops_field_mul_simp <- do { - let {{ thm x = p384_ec_point_ops::p384_point_ops.field.mul x == - p384_field::p384_field_mul x }}; + let t = {{ \x -> p384_ec_point_ops::p384_point_ops.field.mul x == + p384_field::p384_field_mul x }}; // This is pretty quick even without the rewriting and uniterpretation // used above. - let t = unfold_term ["thm"] {{ thm }}; let t = rewrite ss0 t; //print_term t; prove_print z3 t; }; p384_point_ops_field_sq_simp <- do { - let {{ thm x = p384_ec_point_ops::p384_point_ops.field.sq x == - p384_field::p384_field_sq x }}; + let t = {{ \x -> p384_ec_point_ops::p384_point_ops.field.sq x == + p384_field::p384_field_sq x }}; // This is pretty quick even without the rewriting and uninterpretation // used above. - let t = unfold_term ["thm"] {{ thm }}; let t = rewrite ss0 t; //print_term t; prove_print z3 t; }; p384_point_ops_field_mul_simp2 <- do { - let {{ thm x = ecc::p384_curve.point_ops.field.mul x == - p384_field::p384_field_mul x }}; + let t = {{ \x -> ecc::p384_curve.point_ops.field.mul x == + p384_field::p384_field_mul x }}; // This is pretty quick even without the rewriting and uniterpretation // used above. - let t = unfold_term ["thm"] {{ thm }}; let t = rewrite ss0 t; //print_term t; prove_print z3 t; }; p384_point_ops_field_sq_simp2 <- do { - let {{ thm x = ecc::p384_curve.point_ops.field.sq x == - p384_field::p384_field_sq x }}; + let t = {{ \x -> ecc::p384_curve.point_ops.field.sq x == + p384_field::p384_field_sq x }}; // This is pretty quick even without the rewriting and uniterpretation // used above. - let t = unfold_term ["thm"] {{ thm }}; let t = rewrite ss0 t; //print_term t; prove_print z3 t; }; p384_curve_field_mul_simp <- do { - let {{ thm x y = ecc::p384_curve.point_ops.group_field.mul (x, y) == - mul_java::p384_group_mul (p384_field::p384_group_size, x, y) }}; - let t = unfold_term ["thm"] {{ thm }}; + let t = {{ \x y -> ecc::p384_curve.point_ops.group_field.mul (x, y) == + mul_java::p384_group_mul (p384_field::p384_group_size, x, y) }}; let t = rewrite ss0 t; //print_term t; prove_print (unint_z3 ["p384_group_mul"]) t; }; p384_curve_field_sq_simp <- do { - let {{ thm x = ecc::p384_curve.point_ops.group_field.sq x == - p384_field::p384_mod_mul (p384_field::p384_group_size, x, x) }}; - let t = unfold_term ["thm"] {{ thm }}; + let t = {{ \x -> ecc::p384_curve.point_ops.group_field.sq x == + p384_field::p384_mod_mul (p384_field::p384_group_size, x, x) }}; let t = rewrite ss0 t; //print_term t; prove_print (unint_z3 ["p384_mod_mul"]) t; }; p384_curve_field_div_simp <- do { - let {{ thm x y = ecc::p384_curve.point_ops.group_field.div (x,y) == - p384_field::p384_mod_div (p384_field::p384_group_size, x, y) }}; - let t = unfold_term ["thm"] {{ thm }}; + let t = {{ \x y -> ecc::p384_curve.point_ops.group_field.div (x,y) == + p384_field::p384_mod_div (p384_field::p384_group_size, x, y) }}; let t = rewrite ss0 t; //print_term t; prove_print (unint_z3 ["p384_mod_div"]) t; }; p384_curve_twin_mul_simp <- do { - let {{ thm x = ecc::p384_curve.twin_mul x == - p384_ec_mul::p384_ec_twin_mul x }}; - let t = unfold_term ["thm"] {{ thm }}; + let t = {{ \x -> ecc::p384_curve.twin_mul x == + p384_ec_mul::p384_ec_twin_mul x }}; let t = rewrite ss0 t; //print_term t; prove_print (unint_z3 ["p384_ec_twin_mul"]) t; }; p384_curve_is_equal_simp <- do { - let {{ thm x y = ecc::p384_curve.point_ops.group_field.is_equal (x, y) == - (x == y) }}; - let t = unfold_term ["thm"] {{ thm }}; + let t = {{ \x y -> ecc::p384_curve.point_ops.group_field.is_equal (x, y) == + (x == y) }}; let t = rewrite ss0 t; //print_term t; prove_print z3 t; }; p384_curve_is_val_simp <- do { - let {{ thm x = ecc::p384_curve.point_ops.group_field.is_val x == - p384_field::p384_is_group_val x }}; - let t = unfold_term ["thm"] {{ thm }}; + let t = {{ \x -> ecc::p384_curve.point_ops.group_field.is_val x == + p384_field::p384_is_group_val x }}; let t = rewrite ss0 t; //print_term t; prove_print z3 t; }; p384_curve_norm_simp <- do { - let {{ thm x = ecc::p384_curve.point_ops.group_field.normalize x == - (if x < p384_field::p384_group_size - then x - else x - p384_field::p384_group_size) }}; - let t = unfold_term ["thm"] {{ thm }}; + let t = {{ \x -> ecc::p384_curve.point_ops.group_field.normalize x == + (if x < p384_field::p384_group_size + then x + else x - p384_field::p384_group_size) }}; let t = rewrite ss0 t; //print_term t; prove_print z3 t; }; p384_curve_field_zero_simp <- do { - let {{ thm = ecc::p384_curve.point_ops.group_field.field_zero == 0 }}; - let t = unfold_term ["thm"] {{ thm }}; + let t = {{ ecc::p384_curve.point_ops.group_field.field_zero == 0 }}; let t = rewrite ss0 t; //print_term t; prove_print z3 t; }; p384_curve_base_simp <- do { - let {{ thm = ecc::p384_curve.base == ecc::p384_base }}; - let t = unfold_term ["thm"] {{ thm }}; + let t = {{ ecc::p384_curve.base == ecc::p384_base }}; let t = rewrite ss0 t; //print_term t; prove_print z3 t; From 1e9c6da93aeb0d582bb5638a283c3dea2cdefed4 Mon Sep 17 00:00:00 2001 From: David Holland Date: Tue, 21 Oct 2025 19:54:16 -0400 Subject: [PATCH 09/13] interpreter: Add CryptolEnvStack. A CryptolEnvStack is a stack of CryptolEnv; the idea is that the stack allows pushing and popping the Cryptol environment at runtime to match SAWScript scopes. This adds the possibility of having the Cryptol environment track the SAWScript scopes as they come and go, in pursuit of #2304. However, it's not hooked up yet. The interpreter environments cleanup needs to happen before that's feasible; however, making these changes first allows them to appear as their own commit. (It was found that fixing the interpreter's environment handling demanded also fixing the Cryptol environment scoping. Otherwise a lot of things break. The interpreter's old environment handling defers updating the Cryptol environment in some circumstances, which is apparently enough to get a closer approximation of correct behavior in the Cryptol environment than a rational approach. Because of this, these changes were first written on top of the environment handling cleanup and then moved before it. Because of _that_, this commit has not been tested with a full CI run, because GH won't run actions on commits that aren't the tips of pull-request branches. I've taken some precautions, and I _think_ I've kept every access to the Cryptol environment the same with respect to using "getMergedEnv", but I might have fumbled one, or something else might break. Anyway, there's some risk of this commit turning out to be non-testable in the future. It is not _supposed_ to make any functional change.) Note that there are a couple new error paths where attempting import-like operations in a nested scope will fail; these are not reachable until the scopes are connected up. Besides that: - Add more accessors for the Cryptol environment and deploy them to simplify the accesses in the REPL and in saw-server. This avoids baking in exactly where and how the Cryptol environment appears in TopLevelRW (note that saw-server shouldn't be using TopLevelRW at all anyway...) - Canonicalize some of the related naming: - The canonical variable name for a CryptolEnv will be "ce" or "cenv", plural "ces" or "cenvs". - The canonical name for a CryptolEnvStack will be "cryenvs". - Tidy some of the adjacent code. --- saw-central/src/SAWCentral/Builtins.hs | 66 ++++---- .../src/SAWCentral/Crucible/LLVM/X86.hs | 2 +- saw-central/src/SAWCentral/Value.hs | 145 +++++++++++++++++- saw-script/src/SAWScript/Interpreter.hs | 25 +-- saw-script/src/SAWScript/REPL/Monad.hs | 10 +- saw-script/src/SAWScript/ValueOps.hs | 23 ++- saw-server/src/SAWServer/CryptolExpression.hs | 6 +- saw-server/src/SAWServer/CryptolSetup.hs | 12 +- saw-server/src/SAWServer/Eval.hs | 2 +- saw-server/src/SAWServer/JVMVerify.hs | 4 +- saw-server/src/SAWServer/LLVMVerify.hs | 6 +- saw-server/src/SAWServer/MIRVerify.hs | 4 +- saw-server/src/SAWServer/ProofScript.hs | 2 +- saw-server/src/SAWServer/SAWServer.hs | 8 +- saw-server/src/SAWServer/Yosys.hs | 7 +- 15 files changed, 236 insertions(+), 86 deletions(-) diff --git a/saw-central/src/SAWCentral/Builtins.hs b/saw-central/src/SAWCentral/Builtins.hs index d19babe325..0ef6d3c427 100644 --- a/saw-central/src/SAWCentral/Builtins.hs +++ b/saw-central/src/SAWCentral/Builtins.hs @@ -558,7 +558,7 @@ resolveNameIO sc cenv nm = -- exception is thrown. resolveName :: SharedContext -> Text -> TopLevel [VarIndex] resolveName sc nm = - do cenv <- rwCryptol <$> getTopLevelRW + do cenv <- SV.getCryptolEnv' scnms <- io (resolveNameIO sc cenv nm) case scnms of [] -> fail $ Text.unpack $ "Could not resolve name: " <> nm @@ -1590,7 +1590,7 @@ check_term :: TypedTerm -> TopLevel () check_term tt = do sc <- getSharedContext opts <- getTopLevelPPOpts - cenv <- rwCryptol <$> getTopLevelRW + cenv <- SV.getCryptolEnv' let t = ttTerm tt ty <- io $ scTypeCheckError sc t expectedTy <- @@ -1766,7 +1766,7 @@ eval_bool t = do eval_int :: TypedTerm -> TopLevel Integer eval_int t = do sc <- getSharedContext - cenv <- fmap rwCryptol getTopLevelRW + cenv <- SV.getCryptolEnv' let cfg = CEnv.meSolverConfig (CEnv.eModuleEnv cenv) unless (null (getAllExts (ttTerm t))) $ fail "term contains symbolic variables" @@ -1825,7 +1825,7 @@ term_theories unints t = do default_typed_term :: TypedTerm -> TopLevel TypedTerm default_typed_term tt = do sc <- getSharedContext - cenv <- fmap rwCryptol getTopLevelRW + cenv <- SV.getCryptolEnv' let cfg = CEnv.meSolverConfig (CEnv.eModuleEnv cenv) opts <- getOptions io $ defaultTypedTerm opts sc cfg tt @@ -2074,64 +2074,62 @@ cryptol_prims = parsePrim :: (Text, Ident, Text) -> TopLevel (C.Name, TypedTerm) parsePrim (n, i, s) = do sc <- getSharedContext - rw <- getTopLevelRW - let cenv = rwCryptol rw + SV.CryptolEnvStack cenv cenvs <- SV.getCryptolEnvStack + unless (null cenvs) $ do + fail "cryptol_prims is an import operation and may not be done in a nested block" let mname = C.packModName ["Prims"] let ?fileReader = StrictBS.readFile (n', cenv') <- io $ CEnv.declareName cenv mname n s' <- io $ CEnv.parseSchema cenv' (noLoc s) t' <- io $ scGlobalDef sc i - putTopLevelRW $ rw { rwCryptol = cenv' } + SV.setCryptolEnv cenv' return (n', TypedTerm (TypedTermSchema s') t') cryptol_load :: (FilePath -> IO StrictBS.ByteString) -> FilePath -> TopLevel CEnv.ExtCryptolModule cryptol_load fileReader path = do sc <- getSharedContext - rw <- getTopLevelRW - let ce = rwCryptol rw + SV.CryptolEnvStack ce ces <- SV.getCryptolEnvStack + unless (null ces) $ do + fail "cryptol_load is an import operation and is not permitted in nested blocks" let ?fileReader = fileReader (m, ce') <- io $ CEnv.loadExtCryptolModule sc ce path - putTopLevelRW $ rw { rwCryptol = ce' } + SV.setCryptolEnv ce' return m cryptol_extract :: CEnv.ExtCryptolModule -> Text -> TopLevel TypedTerm cryptol_extract ecm var = do sc <- getSharedContext - rw <- getTopLevelRW - let ce = rwCryptol rw + ce <- SV.getCryptolEnv' let ?fileReader = StrictBS.readFile io $ CEnv.extractDefFromExtCryptolModule sc ce ecm var +-- XXX: This is kind of a top-level style operation; should it be +-- prohibited in nested scopes? (Note that while we could update the +-- whole stack of Cryptol environments here, so the operation escapes +-- the current scope, we won't be able to hunt down and update copies +-- of the environment closed in with lambdas and do-blocks, so that's +-- probably a bad idea.) cryptol_add_path :: FilePath -> TopLevel () -cryptol_add_path path = - do rw <- getTopLevelRW - let ce = rwCryptol rw +cryptol_add_path path = do + ce <- SV.getCryptolEnv' let me = CEnv.eModuleEnv ce let me' = me { C.meSearchPath = path : C.meSearchPath me } let ce' = ce { CEnv.eModuleEnv = me' } - let rw' = rw { rwCryptol = ce' } - putTopLevelRW rw' + SV.setCryptolEnv ce' cryptol_add_prim :: Text -> Text -> TypedTerm -> TopLevel () -cryptol_add_prim mnm nm trm = - do rw <- getTopLevelRW - let env = rwCryptol rw - let prim_name = - C.PrimIdent (C.textToModName mnm) nm - let env' = - env { CEnv.ePrims = - Map.insert prim_name (ttTerm trm) (CEnv.ePrims env) } - putTopLevelRW (rw { rwCryptol = env' }) +cryptol_add_prim mnm nm trm = do + ce <- SV.getCryptolEnv' + let prim_name = C.PrimIdent (C.textToModName mnm) nm + prims' = Map.insert prim_name (ttTerm trm) (CEnv.ePrims ce) + SV.setCryptolEnv $ ce { CEnv.ePrims = prims' } cryptol_add_prim_type :: Text -> Text -> TypedTerm -> TopLevel () -cryptol_add_prim_type mnm nm tp = - do rw <- getTopLevelRW - let env = rwCryptol rw - let prim_name = - C.PrimIdent (C.textToModName mnm) nm - let env' = env { CEnv.ePrimTypes = - Map.insert prim_name (ttTerm tp) (CEnv.ePrimTypes env) } - putTopLevelRW (rw { rwCryptol = env' }) +cryptol_add_prim_type mnm nm tp = do + ce <- SV.getCryptolEnv' + let prim_name = C.PrimIdent (C.textToModName mnm) nm + prim_types' = Map.insert prim_name (ttTerm tp) (CEnv.ePrimTypes ce) + SV.setCryptolEnv $ ce { CEnv.ePrimTypes = prim_types' } -- | Call 'Cryptol.importSchema' using a 'CEnv.CryptolEnv' importSchemaCEnv :: SharedContext -> CEnv.CryptolEnv -> Cryptol.Schema -> diff --git a/saw-central/src/SAWCentral/Crucible/LLVM/X86.hs b/saw-central/src/SAWCentral/Crucible/LLVM/X86.hs index dbea5dfa93..889f15a2ca 100644 --- a/saw-central/src/SAWCentral/Crucible/LLVM/X86.hs +++ b/saw-central/src/SAWCentral/Crucible/LLVM/X86.hs @@ -437,6 +437,7 @@ llvm_verify_x86_common (Some (llvmModule :: LLVMModule x)) path nm globsyms chec opts <- getOptions basic_ss <- getBasicSS rw <- getTopLevelRW + cenv <- getCryptolEnv' sym <- liftIO $ newSAWCoreExprBuilder sc False mdMap <- liftIO $ newIORef mempty SomeOnlineBackend bak <- liftIO $ @@ -458,7 +459,6 @@ llvm_verify_x86_common (Some (llvmModule :: LLVMModule x)) path nm globsyms chec halloc <- getHandleAlloc let mvar = C.LLVM.llvmMemVar . view C.LLVM.transContext $ modTrans llvmModule sfs <- liftIO $ Macaw.newSymFuns sym - let cenv = rwCryptol rw liftIO $ sawRegisterSymFunInterp sawst (Macaw.fnAesEnc sfs) $ cryptolUninterpreted path nm cenv "aesenc" liftIO $ sawRegisterSymFunInterp sawst (Macaw.fnAesEncLast sfs) $ cryptolUninterpreted path nm cenv "aesenclast" liftIO $ sawRegisterSymFunInterp sawst (Macaw.fnAesDec sfs) $ cryptolUninterpreted path nm cenv "aesdec" diff --git a/saw-central/src/SAWCentral/Value.hs b/saw-central/src/SAWCentral/Value.hs index 8fc4236b52..25e7a640f8 100644 --- a/saw-central/src/SAWCentral/Value.hs +++ b/saw-central/src/SAWCentral/Value.hs @@ -61,8 +61,29 @@ module SAWCentral.Value ( mergeLocalEnv, -- used by SAWCentral.Builtins, SAWScript.Interpreter, and by getCryptolEnv getMergedEnv, getMergedEnv', - -- used by SAWCentral.Crucible.LLVM.FFI - getCryptolEnv, + -- used by SAWCentral.Builtins, SAWScript.ValueOps, SAWScript.Interpreter, + -- SAWServer.SAWServer + CryptolEnvStack(..), + -- used by SAWCentral.Crucible.LLVM.FFI, SAWCentral.Crucible.LLVM.X86, + -- SAWCentral.Crucible.MIR.Builtins, SAWCentral.Builtins, + -- SAWScript.Interpreter, SAWScript.REPL.Monad + getCryptolEnv, getCryptolEnv', + -- used by SAWCentral.Builtins + getCryptolEnvStack, + -- used by SAWCentral.Builtins, SAWScript.Interpreter, SAWScript.REPL.Monad + setCryptolEnv, + -- used by SAWScript.REPL.Monad, SAWServer.Eval, + -- SAWServer.ProofScript, SAWServer.CryptolSetup, SAWServer.CryptolExpression, + -- SAWServer.LLVMVerify, SAWServer.JVMVerify, SAWServer.MIRVerify, SAWServer.Yosys, + rwGetCryptolEnv, + -- used by SAWScript.ValueOps + rwGetCryptolEnvStack, + -- used by SAWServer.CryptolSetup + rwSetCryptolEnv, + -- used by SAWScript.ValueOps + rwSetCryptolEnvStack, + -- used by SAWScript.REPL.Monad, SAWServer.SAWServer, SAWServer.Yosys + rwModifyCryptolEnv, -- used by SAWScript.Automatch, SAWScript.REPL.*, SAWScript.Interpreter, -- SAWServer.SAWServer TopLevelRO(..), @@ -220,6 +241,7 @@ import qualified Data.AIG as AIG import qualified SAWSupport.Pretty as PPS (Opts, defaultOpts, showBrackets, showBraces, showCommaSep) +import SAWCentral.Panic (panic) import SAWCentral.Trace (Trace) import qualified SAWCentral.Trace as Trace @@ -736,6 +758,12 @@ evaluateTypedTerm _sc (TypedTerm tp _) = -- TopLevel Monad -------------------------------------------------------------- +-- | The full Cryptol environment. We maintain a stack of plain +-- Cryptol environments and push/pop them as we enter and leave +-- scopes; otherwise the Cryptol environment doesn't track SAWScript +-- scopes and horribly confusing wrong things happen. +data CryptolEnvStack = CryptolEnvStack CEnv.CryptolEnv [CEnv.CryptolEnv] + -- | Entry in the interpreter's local (as opposed to global) variable -- environment. -- @@ -786,10 +814,113 @@ getMergedEnv' env = do rw <- getTopLevelRW liftIO $ mergeLocalEnv sc env rw +-- | Get the current Cryptol environment. getCryptolEnv :: TopLevel CEnv.CryptolEnv getCryptolEnv = do - env <- getMergedEnv - return $ rwCryptol env + env <- getMergedEnv + let CryptolEnvStack ce _ = rwCryptol env + return ce + +-- | Get the current Cryptol environment. +-- +-- Variant version that doesn't call getMergedEnv, to avoid +-- unexpected behavioral changes in this commit. +getCryptolEnv' :: TopLevel CEnv.CryptolEnv +getCryptolEnv' = do + CryptolEnvStack ce _ <- gets rwCryptol + return ce + +-- | Get the current full stack of Cryptol environments. +getCryptolEnvStack :: TopLevel CryptolEnvStack +getCryptolEnvStack = + gets rwCryptol + +-- | Update the current Cryptol environment. +-- +-- Overwrites the previous value; the caller must ensure that the +-- value applied has not become stale. +setCryptolEnv :: CEnv.CryptolEnv -> TopLevel () +setCryptolEnv ce = do + CryptolEnvStack _ ces <- gets rwCryptol + modify (\rw -> rw { rwCryptol = CryptolEnvStack ce ces }) + +-- | Get the current Cryptol environment from a TopLevelRW. +-- +-- (Accessor method for use in SAWServer and SAWScript.REPL, which +-- have their own monads and thus different access to TopLevelRW.) +-- +-- XXX: SAWServer shouldn't be using, or need to use, TopLevelRW at +-- all. +rwGetCryptolEnv :: TopLevelRW -> CEnv.CryptolEnv +rwGetCryptolEnv rw = + let CryptolEnvStack ce _ = rwCryptol rw in + ce + +-- | Get the current full stack of Cryptol environments from a +-- TopLevelRW. Used by the checkpointing logic, in a fairly dubious +-- way. (XXX) +rwGetCryptolEnvStack :: TopLevelRW -> CryptolEnvStack +rwGetCryptolEnvStack rw = + rwCryptol rw + +-- | Update the current Cryptol environment in a TopLevelRW. +-- +-- Overwrites the previous environment; caller must ensure they +-- haven't done anything to make the value they're working with +-- stale. +-- +-- (Accessor method for use in SAWServer and SAWScript.REPL, which +-- have their own monads and thus different access to TopLevelRW.) +-- +-- XXX: SAWServer shouldn't be using, or need to use, TopLevelRW at +-- all. +rwSetCryptolEnv :: CEnv.CryptolEnv -> TopLevelRW -> TopLevelRW +rwSetCryptolEnv ce rw = + let CryptolEnvStack _ ces = rwCryptol rw in + rw { rwCryptol = CryptolEnvStack ce ces } + +-- | Update the current full stack of Cryptol environments in a +-- TopLevelRW. Used by the checkpointing logic, in a fairly +-- dubious way. (XXX) +-- +-- Overwrites the previous stack; caller must ensure they haven't +-- done anything to make the value they're working with stale. +rwSetCryptolEnvStack :: CryptolEnvStack -> TopLevelRW -> TopLevelRW +rwSetCryptolEnvStack cryenvs rw = + rw { rwCryptol = cryenvs } + +-- | Modify the current Cryptol environment in a TopLevelRW. +-- +-- (Accessor method for use in SAWServer and SAWScript.REPL, which +-- have their own monads and thus different access to TopLevelRW.) +-- +-- XXX: SAWServer shouldn't be using, or need to use, TopLevelRW at +-- all. +rwModifyCryptolEnv :: (CEnv.CryptolEnv -> CEnv.CryptolEnv) -> TopLevelRW -> TopLevelRW +rwModifyCryptolEnv f rw = + let CryptolEnvStack ce ces = rwCryptol rw + ce' = f ce + in + rw { rwCryptol = CryptolEnvStack ce' ces } + +-- | Push a new scope on the Cryptol environment stack. +-- +-- (Not used yet.) +_cryptolPush :: CryptolEnvStack -> CryptolEnvStack +_cryptolPush (CryptolEnvStack ce ces) = + -- Each entry is the whole environment, so duplicate the top entry + CryptolEnvStack ce (ce : ces) + +-- | Pop the current scope off the Cryptol environment stack. +-- +-- (Not used yet.) +_cryptolPop :: CryptolEnvStack -> CryptolEnvStack +_cryptolPop (CryptolEnvStack _ ces) = + -- Discard the top + case ces of + [] -> panic "cryptolPop" ["Cryptol environment scope stack ran out"] + ce : ces' -> CryptolEnvStack ce ces' + -- | TopLevel Read-Only Environment. data TopLevelRO = @@ -841,7 +972,7 @@ data TopLevelRW = , rwTypeInfo :: Map SS.Name (SS.PrimitiveLifecycle, SS.NamedType) -- | The Cryptol naming environment. - , rwCryptol :: CEnv.CryptolEnv + , rwCryptol :: CryptolEnvStack -- | The current execution position. This is only valid when the -- interpreter is calling out into saw-central to execute a @@ -1183,11 +1314,11 @@ extendEnv sc pos name rb ty doc v rw = pure ce let valenv = rwValueInfo rw valenv' = M.insert name (pos, SS.Current, rb, ty, v, doc) valenv - pure $ rw { rwValueInfo = valenv', rwCryptol = ce' } + pure $ rw { rwValueInfo = valenv', rwCryptol = CryptolEnvStack ce' ces } where ident = T.mkIdent name modname = T.packModName [name] - ce = rwCryptol rw + CryptolEnvStack ce ces = rwCryptol rw typedTermOfString :: SharedContext -> String -> IO TypedTerm typedTermOfString sc str = diff --git a/saw-script/src/SAWScript/Interpreter.hs b/saw-script/src/SAWScript/Interpreter.hs index dd383b5f97..cae0cd7f3f 100644 --- a/saw-script/src/SAWScript/Interpreter.hs +++ b/saw-script/src/SAWScript/Interpreter.hs @@ -490,14 +490,14 @@ interpretExpr expr = return $ VInteger z SS.Code pos str -> do sc <- getSharedContext - cenv <- fmap rwCryptol getMergedEnv + cenv <- getCryptolEnv --io $ putStrLn $ "Parsing code: " ++ show str --showCryptolEnv' cenv let str' = toInputText pos str t <- io $ CEnv.parseTypedTerm sc cenv str' return (VTerm t) SS.CType pos str -> do - cenv <- fmap rwCryptol getMergedEnv + cenv <- getCryptolEnv let str' = toInputText pos str s <- io $ CEnv.parseSchema cenv str' return (VType s) @@ -733,12 +733,11 @@ interpretDoStmt stmt = liftTopLevel $ do sc <- getSharedContext rw <- getMergedEnv + let ce = rwGetCryptolEnv rw let str' = toInputText spos str - ce' <- io $ CEnv.parseDecls sc (rwCryptol rw) str' - -- FIXME: Local bindings get saved into the global cryptol environment here. - -- We should change parseDecls to return only the new bindings instead. - putTopLevelRW $ rw{rwCryptol = ce'} + ce' <- io $ CEnv.parseDecls sc ce str' + putTopLevelRW $ rwSetCryptolEnv ce' rw -- return the current local environment unchanged liftTopLevel getLocalEnv SS.StmtImport _ _ -> @@ -904,21 +903,23 @@ interpretTopStmt printBinds stmt = do SS.StmtCode _ spos str -> liftTopLevel $ do sc <- getSharedContext + let cenv = rwGetCryptolEnv rw --io $ putStrLn $ "Processing toplevel code: " ++ show str --showCryptolEnv - cenv' <- io $ CEnv.parseDecls sc (rwCryptol rw) $ toInputText spos str - putTopLevelRW $ rw { rwCryptol = cenv' } + cenv' <- io $ CEnv.parseDecls sc cenv $ toInputText spos str + putTopLevelRW $ rwSetCryptolEnv cenv' rw --showCryptolEnv SS.StmtImport _ imp -> liftTopLevel $ do sc <- getSharedContext + let cenv = rwGetCryptolEnv rw --showCryptolEnv let mLoc = iModule imp qual = iAs imp spec = iSpec imp - cenv' <- io $ CEnv.importCryptolModule sc (rwCryptol rw) mLoc qual CEnv.PublicAndPrivate spec - putTopLevelRW $ rw { rwCryptol = cenv' } + cenv' <- io $ CEnv.importCryptolModule sc cenv mLoc qual CEnv.PublicAndPrivate spec + putTopLevelRW $ rwSetCryptolEnv cenv' rw --showCryptolEnv SS.StmtTypedef _ _ name ty -> @@ -1063,7 +1064,7 @@ buildTopLevelEnv proxy opts scriptArgv = let rw0 = TopLevelRW { rwValueInfo = primValueEnv opts bic , rwTypeInfo = primNamedTypeEnv - , rwCryptol = ce0 + , rwCryptol = CryptolEnvStack ce0 [] , rwPosition = SS.Unknown , rwStackTrace = Trace.empty , rwLocalEnv = [] @@ -2067,7 +2068,7 @@ print_value :: Value -> TopLevel () print_value (VString s) = printOutLnTop Info (Text.unpack s) print_value (VTerm t) = do sc <- getSharedContext - cenv <- fmap rwCryptol getTopLevelRW + cenv <- getCryptolEnv' let cfg = CEnv.meSolverConfig (CEnv.eModuleEnv cenv) unless (null (getAllExts (ttTerm t))) $ fail "term contains symbolic variables" diff --git a/saw-script/src/SAWScript/REPL/Monad.hs b/saw-script/src/SAWScript/REPL/Monad.hs index 378cb3247b..8987776617 100644 --- a/saw-script/src/SAWScript/REPL/Monad.hs +++ b/saw-script/src/SAWScript/REPL/Monad.hs @@ -99,7 +99,8 @@ import SAWCentral.Proof (ProofState, ProofResult(..), psGoals) import SAWCentral.TopLevel (TopLevelRO(..), TopLevelRW(..), TopLevel(..), runTopLevel) import SAWCentral.Value ( AIGProxy(..), mergeLocalEnv - , ProofScript(..), showsProofResult, + , ProofScript(..), showsProofResult + , rwGetCryptolEnv, rwModifyCryptolEnv ) import SAWScript.Interpreter (buildTopLevelEnv) @@ -456,10 +457,13 @@ setModuleEnv :: M.ModuleEnv -> REPL () setModuleEnv me = modifyCryptolEnv (\ce -> ce { eModuleEnv = me }) getCryptolEnv :: REPL CryptolEnv -getCryptolEnv = rwCryptol `fmap` getTopLevelRW +getCryptolEnv = do + rw <- getTopLevelRW + return $ rwGetCryptolEnv rw modifyCryptolEnv :: (CryptolEnv -> CryptolEnv) -> REPL () -modifyCryptolEnv f = modifyTopLevelRW (\rw -> rw { rwCryptol = f (rwCryptol rw) }) +modifyCryptolEnv f = + modifyTopLevelRW $ rwModifyCryptolEnv f setCryptolEnv :: CryptolEnv -> REPL () setCryptolEnv x = modifyCryptolEnv (const x) diff --git a/saw-script/src/SAWScript/ValueOps.hs b/saw-script/src/SAWScript/ValueOps.hs index e05b2e3db4..4439a35e43 100644 --- a/saw-script/src/SAWScript/ValueOps.hs +++ b/saw-script/src/SAWScript/ValueOps.hs @@ -49,6 +49,7 @@ module SAWScript.ValueOps ( import Prelude hiding (fail) +import Control.Monad (zipWithM) import Control.Monad.Catch (MonadThrow(..), try) import Control.Monad.State (get, gets, modify, put) import qualified Control.Exception as X @@ -134,13 +135,25 @@ bracketTopLevel acquire release action = Left (bad :: X.SomeException) -> release resource >> throwM bad Right good -> release resource >> pure good +-- Note: this is used only by restoreCheckpoint and restoreCheckpoint is +-- not really expected to work. +-- +-- This is good, because whatever this function is doing does not seem +-- to make a great deal of sense. (Which has become more overt with recent +-- reorgs and cleanup, but hasn't itself changed.) combineRW :: TopLevelCheckpoint -> TopLevelRW -> IO TopLevelRW -combineRW (TopLevelCheckpoint chk scc) rw = - do cenv' <- CEnv.combineCryptolEnv (rwCryptol chk) (rwCryptol rw) +combineRW (TopLevelCheckpoint chk scc) rw = do + let CryptolEnvStack chk'cenv chk'cenvs = rwGetCryptolEnvStack chk + CryptolEnvStack rw'cenv rw'cenvs = rwGetCryptolEnvStack rw + -- Caution: this merge may have unexpected results if the + -- number of scopes doesn't match. But, it doesn't make sense + -- to do that in the first place. Caveat emptor... + cenv' <- CEnv.combineCryptolEnv chk'cenv rw'cenv + cenvs' <- zipWithM CEnv.combineCryptolEnv chk'cenvs rw'cenvs sc' <- restoreSharedContext scc (rwSharedContext rw) - return chk{ rwCryptol = cenv' - , rwSharedContext = sc' - } + let cryenv' = CryptolEnvStack cenv' cenvs' + let chk' = rwSetCryptolEnvStack cryenv' chk + return chk' { rwSharedContext = sc' } -- | Represents the mutable state of the TopLevel monad -- that can later be restored. diff --git a/saw-server/src/SAWServer/CryptolExpression.hs b/saw-server/src/SAWServer/CryptolExpression.hs index b18f27cc44..8d7bb95c4f 100644 --- a/saw-server/src/SAWServer/CryptolExpression.hs +++ b/saw-server/src/SAWServer/CryptolExpression.hs @@ -30,7 +30,7 @@ import Cryptol.TypeCheck.Solver.SMT (withSolver) import Cryptol.Utils.Ident (interactiveName) import Cryptol.Utils.Logger (quietLogger) import Cryptol.Utils.PP ( defaultPPOpts, pp ) -import SAWCentral.Value (biSharedContext, TopLevelRW(..)) +import SAWCentral.Value (biSharedContext, rwGetCryptolEnv) import CryptolSAWCore.CryptolEnv ( getAllIfaceDecls, getNamingEnv, @@ -48,8 +48,8 @@ import CryptolServer.Exceptions (cryptolError) import SAWServer.SAWServer getTypedTerm :: Expression -> Argo.Command SAWState TypedTerm -getTypedTerm inputExpr = - do cenv <- rwCryptol . view sawTopLevelRW <$> Argo.getState +getTypedTerm inputExpr = do + cenv <- rwGetCryptolEnv . view sawTopLevelRW <$> Argo.getState fileReader <- Argo.getFileReader expr <- getCryptolExpr inputExpr sc <- biSharedContext . view sawBIC <$> Argo.getState diff --git a/saw-server/src/SAWServer/CryptolSetup.hs b/saw-server/src/SAWServer/CryptolSetup.hs index 4340489eec..c7e15c4cbe 100644 --- a/saw-server/src/SAWServer/CryptolSetup.hs +++ b/saw-server/src/SAWServer/CryptolSetup.hs @@ -18,7 +18,7 @@ import qualified Data.Text as T import qualified Cryptol.Parser.AST as P import Cryptol.Utils.Ident (textToModName) -import SAWCentral.Value (biSharedContext, rwCryptol) +import SAWCentral.Value (biSharedContext, rwGetCryptolEnv, rwSetCryptolEnv) import qualified CryptolSAWCore.CryptolEnv as CEnv import qualified Argo @@ -36,7 +36,8 @@ cryptolLoadModuleDescr = cryptolLoadModule :: CryptolLoadModuleParams -> Argo.Command SAWState OK cryptolLoadModule (CryptolLoadModuleParams modName) = do sc <- biSharedContext . view sawBIC <$> Argo.getState - cenv <- rwCryptol . view sawTopLevelRW <$> Argo.getState + rw <- view sawTopLevelRW <$> Argo.getState + let cenv = rwGetCryptolEnv rw let qual = Nothing -- TODO add field to params let importSpec = Nothing -- TODO add field to params fileReader <- Argo.getFileReader @@ -45,7 +46,7 @@ cryptolLoadModule (CryptolLoadModuleParams modName) = case cenv' of Left (ex :: SomeException) -> Argo.raise $ cryptolError (show ex) Right cenv'' -> - do Argo.modifyState $ over sawTopLevelRW $ \rw -> rw { rwCryptol = cenv'' } + do Argo.modifyState $ over sawTopLevelRW $ rwSetCryptolEnv cenv'' ok newtype CryptolLoadModuleParams = @@ -71,7 +72,8 @@ cryptolLoadFileDescr = cryptolLoadFile :: CryptolLoadFileParams -> Argo.Command SAWState OK cryptolLoadFile (CryptolLoadFileParams fileName) = do sc <- biSharedContext . view sawBIC <$> Argo.getState - cenv <- rwCryptol . view sawTopLevelRW <$> Argo.getState + rw <- view sawTopLevelRW <$> Argo.getState + let cenv = rwGetCryptolEnv rw let qual = Nothing -- TODO add field to params let importSpec = Nothing -- TODO add field to params fileReader <- Argo.getFileReader @@ -80,7 +82,7 @@ cryptolLoadFile (CryptolLoadFileParams fileName) = case cenv' of Left (ex :: SomeException) -> Argo.raise $ cryptolError (show ex) Right cenv'' -> - do Argo.modifyState $ over sawTopLevelRW $ \rw -> rw { rwCryptol = cenv'' } + do Argo.modifyState $ over sawTopLevelRW $ rwSetCryptolEnv cenv'' ok newtype CryptolLoadFileParams = diff --git a/saw-server/src/SAWServer/Eval.hs b/saw-server/src/SAWServer/Eval.hs index d7f211843f..399eab9dd8 100644 --- a/saw-server/src/SAWServer/Eval.hs +++ b/saw-server/src/SAWServer/Eval.hs @@ -80,7 +80,7 @@ eval :: eval f params = do state <- Argo.getState fileReader <- Argo.getFileReader - let cenv = SV.rwCryptol (view sawTopLevelRW state) + let cenv = SV.rwGetCryptolEnv (view sawTopLevelRW state) bic = view sawBIC state cexp <- getCryptolExpr $ evalExpr params (eterm, warnings) <- liftIO $ getTypedTermOfCExp fileReader (SV.biSharedContext bic) cenv cexp diff --git a/saw-server/src/SAWServer/JVMVerify.hs b/saw-server/src/SAWServer/JVMVerify.hs index c556f74f2f..8cb7221447 100644 --- a/saw-server/src/SAWServer/JVMVerify.hs +++ b/saw-server/src/SAWServer/JVMVerify.hs @@ -14,7 +14,7 @@ import qualified Data.Map as Map import SAWCentral.Crucible.JVM.Builtins ( jvm_unsafe_assume_spec, jvm_verify ) import SAWCentral.JavaExpr (JavaType(..)) -import SAWCentral.Value (rwCryptol) +import SAWCentral.Value (rwGetCryptolEnv) import qualified Argo import qualified Argo.Doc as Doc @@ -51,7 +51,7 @@ jvmVerifyAssume mode (VerifyParams className fun lemmaNames checkSat contract sc state <- Argo.getState cls <- getJVMClass className let bic = view sawBIC state - cenv = rwCryptol (view sawTopLevelRW state) + cenv = rwGetCryptolEnv (view sawTopLevelRW state) fileReader <- Argo.getFileReader ghostEnv <- Map.fromList <$> getGhosts setup <- compileJVMContract fileReader bic ghostEnv cenv <$> traverse getCryptolExpr contract diff --git a/saw-server/src/SAWServer/LLVMVerify.hs b/saw-server/src/SAWServer/LLVMVerify.hs index f9623ff2ab..4f8491e6f8 100644 --- a/saw-server/src/SAWServer/LLVMVerify.hs +++ b/saw-server/src/SAWServer/LLVMVerify.hs @@ -16,7 +16,7 @@ import qualified Data.Map as Map import SAWCentral.Crucible.LLVM.Builtins ( llvm_unsafe_assume_spec, llvm_verify ) import SAWCentral.Crucible.LLVM.X86 ( llvm_verify_x86 ) -import SAWCentral.Value (rwCryptol) +import SAWCentral.Value (rwGetCryptolEnv) import qualified Argo import qualified Argo.Doc as Doc @@ -57,7 +57,7 @@ llvmVerifyAssume mode (VerifyParams modName fun lemmaNames checkSat contract scr state <- Argo.getState mod <- getLLVMModule modName let bic = view sawBIC state - cenv = rwCryptol (view sawTopLevelRW state) + cenv = rwGetCryptolEnv (view sawTopLevelRW state) fileReader <- Argo.getFileReader ghostEnv <- Map.fromList <$> getGhosts setup <- compileLLVMContract fileReader bic ghostEnv cenv <$> @@ -113,7 +113,7 @@ llvmVerifyX86 (X86VerifyParams modName objName fun globals _lemmaNames checkSat state <- Argo.getState mod <- getLLVMModule modName let bic = view sawBIC state - cenv = rwCryptol (view sawTopLevelRW state) + cenv = rwGetCryptolEnv (view sawTopLevelRW state) allocs = map (\(X86Alloc name size) -> (name, size)) globals proofScript <- interpretProofScript script fileReader <- Argo.getFileReader diff --git a/saw-server/src/SAWServer/MIRVerify.hs b/saw-server/src/SAWServer/MIRVerify.hs index 69ed710603..f29f6604d5 100644 --- a/saw-server/src/SAWServer/MIRVerify.hs +++ b/saw-server/src/SAWServer/MIRVerify.hs @@ -13,7 +13,7 @@ import qualified Data.Map as Map import SAWCentral.Crucible.MIR.Builtins ( mir_unsafe_assume_spec, mir_verify ) -import SAWCentral.Value (rwCryptol) +import SAWCentral.Value (rwGetCryptolEnv) import qualified Argo import qualified Argo.Doc as Doc @@ -52,7 +52,7 @@ mirVerifyAssume mode (VerifyParams modName fun lemmaNames checkSat contract scri state <- Argo.getState rm <- getMIRModule modName let bic = view sawBIC state - cenv = rwCryptol (view sawTopLevelRW state) + cenv = rwGetCryptolEnv (view sawTopLevelRW state) sawenv = view sawEnv state fileReader <- Argo.getFileReader ghostEnv <- Map.fromList <$> getGhosts diff --git a/saw-server/src/SAWServer/ProofScript.hs b/saw-server/src/SAWServer/ProofScript.hs index afa597b62a..90195b4041 100644 --- a/saw-server/src/SAWServer/ProofScript.hs +++ b/saw-server/src/SAWServer/ProofScript.hs @@ -259,7 +259,7 @@ prove :: ProveParams Expression -> Argo.Command SAWState ProveResult prove params = do state <- Argo.getState fileReader <- Argo.getFileReader - let cenv = SV.rwCryptol (view sawTopLevelRW state) + let cenv = SV.rwGetCryptolEnv (view sawTopLevelRW state) bic = view sawBIC state cexp <- getCryptolExpr (ppGoal params) (eterm, warnings) <- liftIO $ getTypedTermOfCExp fileReader (SV.biSharedContext bic) cenv cexp diff --git a/saw-server/src/SAWServer/SAWServer.hs b/saw-server/src/SAWServer/SAWServer.hs index a2275b688b..527b01cdfe 100644 --- a/saw-server/src/SAWServer/SAWServer.hs +++ b/saw-server/src/SAWServer/SAWServer.hs @@ -63,7 +63,7 @@ import SAWCentral.Options (processEnv, defaultOptions) import SAWCentral.Position (Pos(..)) import SAWCentral.Prover.Rewrite (basic_ss) import SAWCentral.Proof (emptyTheoremDB) -import SAWCentral.Value (AIGProxy(..), BuiltinContext(..), JVMSetupM, LLVMCrucibleSetupM, TopLevelRO(..), TopLevelRW(..), SAWSimpset,JavaCodebase(..)) +import SAWCentral.Value (AIGProxy(..), BuiltinContext(..), JVMSetupM, LLVMCrucibleSetupM, TopLevelRO(..), TopLevelRW(..), SAWSimpset, JavaCodebase(..), CryptolEnvStack(..), rwModifyCryptolEnv) import SAWCentral.Yosys.State (YosysSequential) import SAWCentral.Yosys.Theorem (YosysImport, YosysTheorem) import qualified CryptolSAWCore.Prelude as CryptolSAW @@ -245,7 +245,7 @@ initialState readFileFn = rw = TopLevelRW { rwValueInfo = mempty , rwTypeInfo = mempty - , rwCryptol = cenv + , rwCryptol = CryptolEnvStack cenv [] , rwPosition = PosInternal "SAWServer" , rwStackTrace = Trace.empty , rwLocalEnv = [] @@ -457,8 +457,8 @@ getServerValEither (SAWEnv serverEnv) n = bindCryptolVar :: Text -> TypedTerm -> Argo.Command SAWState () bindCryptolVar x t = - do Argo.modifyState $ over sawTopLevelRW $ \rw -> - rw { rwCryptol = bindTypedTerm (Cryptol.mkIdent x, t) (rwCryptol rw) } + do Argo.modifyState $ over sawTopLevelRW $ rwModifyCryptolEnv $ \cenv -> + bindTypedTerm (Cryptol.mkIdent x, t) cenv getJVMClass :: ServerName -> Argo.Command SAWState JSS.Class getJVMClass n = diff --git a/saw-server/src/SAWServer/Yosys.hs b/saw-server/src/SAWServer/Yosys.hs index 91f9210ee5..158e3d527d 100644 --- a/saw-server/src/SAWServer/Yosys.hs +++ b/saw-server/src/SAWServer/Yosys.hs @@ -30,7 +30,7 @@ import SAWServer.OK (OK, ok) import SAWServer.ProofScript (ProofScript, interpretProofScript) import SAWServer.TopLevel (tl) -import SAWCentral.Value (getSharedContext, getTopLevelRW, rwCryptol) +import SAWCentral.Value (getSharedContext, getTopLevelRW, rwGetCryptolEnv, rwModifyCryptolEnv) import SAWCentral.Yosys (loadYosysIR, yosysIRToTypedTerms, yosys_verify, yosys_import_sequential, yosys_extract_sequential) import SAWCentral.Yosys.Theorem (YosysImport(..)) @@ -121,7 +121,7 @@ yosysVerify params = do l <- tl $ do rw <- getTopLevelRW sc <- getSharedContext - let cenv = rwCryptol rw + let cenv = rwGetCryptolEnv rw preconds <- forM precondExprs $ \pc -> do (eterm, warnings) <- liftIO $ getTypedTermOfCExp fileReader sc cenv pc case eterm of @@ -205,7 +205,8 @@ yosysExtractSequential params = do m <- getYosysSequential $ yosysExtractSequentialModule params s <- tl $ yosys_extract_sequential m (yosysExtractSequentialCycles params) let sn@(ServerName n) = yosysExtractSequentialServerName params - sawTopLevelRW %= \rw -> rw { rwCryptol = CEnv.bindTypedTerm (mkIdent n, s) $ rwCryptol rw } + doBind cenv = CEnv.bindTypedTerm (mkIdent n, s) cenv + sawTopLevelRW %= rwModifyCryptolEnv doBind setServerVal sn s ok From 6a69402f47f561f45ca3f4e245602ce02aa20f47 Mon Sep 17 00:00:00 2001 From: David Holland Date: Fri, 10 Oct 2025 15:03:46 -0400 Subject: [PATCH 10/13] interpreter: Replace the variable and type environment handling. There are many notable consequences: - The unexplained weirdness that appeared with "undefined" in test_sawscript_builtins is now fixed. Yay! No idea why though, other than the old code was terrible. - Similarly, bindings no longer escape "proof_subshell", which closes #2243. - The old dynamic scope bug behavior (see #1646) is removed. - We now have, via attaching the new CryptolEnvStack code, and including the Cryptol environment in the new Environ type so things get closed in properly, reasonably correct scope handling for the Cryptol environment. This closes #2304. - Note though that the SAWCore environment properly speaking needs a similar treatment, but we can't currently. The result is that in obscure cases (e.g. test03.saw in test2304) using the same variable name in what should be distinct places can cause a SAWCore-level duplicate definition error. For the moment, we're going to hope that these cases are all sufficiently obscure that nobody trips on them, and track the issue in #2726. Test reference (and in some cases comments) updates: - test1646/test01 and test02: the already-bound variable no longer updates; this fixes the type system hole and ensuing panic previously shown in test02. - test1646/test05 is now broken; it was relying on the old dynamic scope bug behavior to implement "let rebindable". This will be fixed in the next commit. - test1646/test14 now behaves differently but is still wrong. This will be fixed in the next commit. - test2304/test02 now works correctly. - test2304/test03 now works at the Cryptol level but triggers #2726. - test_sawscript_builtins/undefined7 and undefined8: these now crash where they're supposed to. --- CHANGES.md | 17 +- intTests/test1646/test01.log.good | 2 +- intTests/test1646/test01.saw | 2 +- intTests/test1646/test02.log.good | 5 +- intTests/test1646/test02.saw | 4 +- intTests/test1646/test05.log.good | 2 +- intTests/test1646/test05.saw | 1 + intTests/test1646/test14.log.good | 4 +- intTests/test1646/test14.saw | 2 +- intTests/test1646/test15.log.good | 5 +- intTests/test2304/test02.log.good | 11 +- intTests/test2304/test03.log.good | 10 +- .../undefined7.log.good | 1 - .../test_sawscript_builtins/undefined7.saw | 16 +- .../undefined8.log.good | 7 +- .../test_sawscript_builtins/undefined8.saw | 3 +- saw-central/src/SAWCentral/ASTUtil.hs | 48 ++- saw-central/src/SAWCentral/Builtins.hs | 41 ++- .../src/SAWCentral/Crucible/LLVM/Builtins.hs | 7 +- .../src/SAWCentral/Crucible/LLVM/X86.hs | 2 +- saw-central/src/SAWCentral/Value.hs | 288 ++++++++------- saw-script/src/SAWScript/Interpreter.hs | 333 ++++++++++-------- saw-script/src/SAWScript/REPL/Command.hs | 86 +++-- saw-script/src/SAWScript/REPL/Monad.hs | 29 +- saw-script/src/SAWScript/Search.hs | 17 +- saw-script/src/SAWScript/Typechecker.hs | 12 +- saw-script/src/SAWScript/ValueOps.hs | 56 ++- saw-server/src/SAWServer/SAWServer.hs | 9 +- 28 files changed, 558 insertions(+), 462 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index 5205d252f4..2e2d9e25d6 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -10,8 +10,11 @@ This release supports [version arbitrarily rebound, such that existing uses would see the updated value, has been superseded. Among other problems, it wasn't type safe. - Substitute functionality is now available by using the new syntax - `let rebindable`. + Now, rebinding a variable creates a new variable that hides the + old one; prior references are not affected. + + Substitute functionality for the old behavior is now available by + using the new syntax `let rebindable`. After `let rebindable x = 3`, `x` is mutable and a subsequent `let rebindable x = 4` will change the value seen by all uses. The value type must remain the same; to avoid unnecessary @@ -174,6 +177,16 @@ This release supports [version ## Bug Fixes +* The Cryptol environment now tracks SAWScript scopes properly (#2304). + Note though that SAWCore-level names, which are for example bound by + uses of `let {{ ... }}`, are still not scoped and can trigger + duplicate variable errors. + See #2726 for further information. + +* A number of internal weirdnesses in SAWScript's internal variable handling + have been cleaned out; for example, bindings made in `proof_subshell` no + longer escape the subshell (#2243). + * Fix a bug that would cause SAW to crash when loading an instantiation of a parameterized Cryptol module that contains newtypes or enums (#2673). diff --git a/intTests/test1646/test01.log.good b/intTests/test1646/test01.log.good index 6c1406a55c..5b50ca7d31 100644 --- a/intTests/test1646/test01.log.good +++ b/intTests/test1646/test01.log.good @@ -2,4 +2,4 @@ x=a test01.saw:8:5-8:6: Warning: Redeclaration of x test01.saw:3:5-3:6: Warning: Previous declaration was here - x=b + x=a diff --git a/intTests/test1646/test01.saw b/intTests/test1646/test01.saw index fe91352f73..cc9ffecd38 100644 --- a/intTests/test1646/test01.saw +++ b/intTests/test1646/test01.saw @@ -1,4 +1,4 @@ -// The second f call will print x=b. +// The second f call nowadays will print x=a. let x = "a"; diff --git a/intTests/test1646/test02.log.good b/intTests/test1646/test02.log.good index f9427d0cef..4e3cd46602 100644 --- a/intTests/test1646/test02.log.good +++ b/intTests/test1646/test02.log.good @@ -2,7 +2,4 @@ x=a test02.saw:8:5-8:6: Warning: Redeclaration of x test02.saw:3:5-3:6: Warning: Previous declaration was here - fromValue Text -CallStack (from HasCallStack): - error, called at saw-script/src/SAWScript/Interpreter.hs -FAILED + x=a diff --git a/intTests/test1646/test02.saw b/intTests/test1646/test02.saw index a57757ce67..5f51b70f43 100644 --- a/intTests/test1646/test02.saw +++ b/intTests/test1646/test02.saw @@ -1,4 +1,4 @@ -// The second f call will panic with an internal type error. +// The second f call nowadays just prints a. let x = "a"; @@ -6,4 +6,4 @@ let f () = print (str_concat "x=" x); f (); let x = 5; -f(); +f (); diff --git a/intTests/test1646/test05.log.good b/intTests/test1646/test05.log.good index 607fa10161..dc0af5ac42 100644 --- a/intTests/test1646/test05.log.good +++ b/intTests/test1646/test05.log.good @@ -1,3 +1,3 @@ Loading file "test05.saw" x=a - x=b + x=a diff --git a/intTests/test1646/test05.saw b/intTests/test1646/test05.saw index f2542281b8..cf75ee6986 100644 --- a/intTests/test1646/test05.saw +++ b/intTests/test1646/test05.saw @@ -1,4 +1,5 @@ // The second f call will print x=b. +// XXX currently it prints x=a let rebindable x = "a"; diff --git a/intTests/test1646/test14.log.good b/intTests/test1646/test14.log.good index 01a52d821a..d793bbc2d3 100644 --- a/intTests/test1646/test14.log.good +++ b/intTests/test1646/test14.log.good @@ -1,6 +1,6 @@ Loading file "test14.saw" x=a - x=b + x=a test14.saw:12:5-12:6: Warning: Redeclaration of x test14.saw:9:16-9:17: Warning: Previous declaration was here - x=c + x=a diff --git a/intTests/test1646/test14.saw b/intTests/test1646/test14.saw index 2a7c25fa43..a360cc6bbc 100644 --- a/intTests/test1646/test14.saw +++ b/intTests/test1646/test14.saw @@ -1,5 +1,5 @@ // The second f call should print x=b. So should the third. -// XXX: currently the third prints x=c. +// XXX: currently all print x=a. let rebindable x = "a"; diff --git a/intTests/test1646/test15.log.good b/intTests/test1646/test15.log.good index 4df51e0533..1df25e0e21 100644 --- a/intTests/test1646/test15.log.good +++ b/intTests/test1646/test15.log.good @@ -342,7 +342,8 @@ write_saig : String -> Term -> TopLevel () write_saig' : String -> Term -> Int -> TopLevel () write_smtlib2 : String -> Term -> TopLevel () write_smtlib2_w4 : String -> Term -> TopLevel () -x : Int -y : Int yices : ProofScript () z3 : ProofScript () + +x : Int +y : Int diff --git a/intTests/test2304/test02.log.good b/intTests/test2304/test02.log.good index f70625d716..9bb9092f09 100644 --- a/intTests/test2304/test02.log.good +++ b/intTests/test2304/test02.log.good @@ -1,11 +1,2 @@ Loading file "test02.saw" - Stack trace: - (builtin) (at top level) -Cryptol error: -[error] at test02.saw:7:19--7:26: - Type mismatch: - Expected type: Integer - Inferred type: [8] - When checking type of function argument - -FAILED + True diff --git a/intTests/test2304/test03.log.good b/intTests/test2304/test03.log.good index 3e5dceb8f9..aa90314754 100644 --- a/intTests/test2304/test03.log.good +++ b/intTests/test2304/test03.log.good @@ -1,11 +1,3 @@ Loading file "test03.saw" - Stack trace: - (builtin) (at top level) -Cryptol error: -[error] at test03.saw:11:19--11:26: - Type mismatch: - Expected type: Integer - Inferred type: [8] - When checking type of function argument - + Attempted to register the following name twice: cryptol:x#4785 FAILED diff --git a/intTests/test_sawscript_builtins/undefined7.log.good b/intTests/test_sawscript_builtins/undefined7.log.good index 0b8d0d1ff0..cdbeb877c9 100644 --- a/intTests/test_sawscript_builtins/undefined7.log.good +++ b/intTests/test_sawscript_builtins/undefined7.log.good @@ -1,5 +1,4 @@ Loading file "undefined7.saw" - not dead yet interpret: undefined CallStack (from HasCallStack): error, called at saw-script/src/SAWScript/Interpreter.hs diff --git a/intTests/test_sawscript_builtins/undefined7.saw b/intTests/test_sawscript_builtins/undefined7.saw index 3983f0a14b..fbc884bfee 100644 --- a/intTests/test_sawscript_builtins/undefined7.saw +++ b/intTests/test_sawscript_builtins/undefined7.saw @@ -1,15 +1,7 @@ -// This currently doesn't crash unless you execute m. -// -// This is somewhat unexpected, as in theory it should trip on -// undefined evaluating the right hand side of "let m" in -// interpretExpr... or having not done so, file x in the environment -// and then never see it again and not crash at all. -// -// For the time being I'm going to let this pass as an acceptable -// weirdness, and with luck it'll change when other things in the -// interpreter get cleaned up. +// This crashes when m is bound. It will eval until it gets to +// the do-block, and that trips on the undefined. let m = let x = undefined in do { return (); }; -print "not dead yet"; -m; print "oops didn't die"; +m; +print "oops still didn't die"; diff --git a/intTests/test_sawscript_builtins/undefined8.log.good b/intTests/test_sawscript_builtins/undefined8.log.good index eb19d779bc..75aa39b6be 100644 --- a/intTests/test_sawscript_builtins/undefined8.log.good +++ b/intTests/test_sawscript_builtins/undefined8.log.good @@ -1,4 +1,5 @@ Loading file "undefined8.saw" - oops didn't die - () - oops still didn't die + interpret: undefined +CallStack (from HasCallStack): + error, called at saw-script/src/SAWScript/Interpreter.hs +FAILED diff --git a/intTests/test_sawscript_builtins/undefined8.saw b/intTests/test_sawscript_builtins/undefined8.saw index e3a3551c1f..9c2974d611 100644 --- a/intTests/test_sawscript_builtins/undefined8.saw +++ b/intTests/test_sawscript_builtins/undefined8.saw @@ -1,5 +1,4 @@ -// This does not crash, unlike undefined9. It isn't obvious -// what's different. +// This crashes immediately. let y = let x = undefined in (); print "oops didn't die"; diff --git a/saw-central/src/SAWCentral/ASTUtil.hs b/saw-central/src/SAWCentral/ASTUtil.hs index ab1a5857f8..05b315e8ef 100644 --- a/saw-central/src/SAWCentral/ASTUtil.hs +++ b/saw-central/src/SAWCentral/ASTUtil.hs @@ -3,6 +3,7 @@ module SAWCentral.ASTUtil ( namedTyVars, SubstituteTyVars(..), + SubstituteTyVars'(..), isDeprecated ) where @@ -12,6 +13,9 @@ import qualified Data.Set as Set import Data.Map (Map) import qualified Data.Map as Map +import qualified SAWSupport.ScopedMap as ScopedMap +import SAWSupport.ScopedMap (ScopedMap) + import SAWCentral.Panic import SAWCentral.Position import SAWCentral.AST @@ -66,10 +70,10 @@ instance NamedTyVars Schema where -- class SubstituteTyVars t where - -- | @substituteTyVars m x@ applies the map @m@ to type variables in @x@. + -- | @substituteTyVars m x@ applies the (scoped) map @m@ to type variables in @x@. substituteTyVars :: Set PrimitiveLifecycle -> - Map Name (PrimitiveLifecycle, NamedType) -> + ScopedMap Name (PrimitiveLifecycle, NamedType) -> t -> t instance (SubstituteTyVars a) => SubstituteTyVars (Maybe a) where @@ -84,7 +88,7 @@ instance SubstituteTyVars Type where TyRecord pos fs -> TyRecord pos (fmap (substituteTyVars avail tyenv) fs) TyUnifyVar _ _ -> ty TyVar _ n -> - case Map.lookup n tyenv of + case ScopedMap.lookup n tyenv of Nothing -> ty Just (lc, expansion) -> if not (Set.member lc avail) then @@ -96,6 +100,44 @@ instance SubstituteTyVars Type where AbstractType -> ty ConcreteType ty' -> ty' +-- +-- The prime version uses an ordinary map. +-- +-- This is used by the typechecker for the time being until the +-- typechecker gets taught to use ScopedMap. +-- + +class SubstituteTyVars' t where + -- | @substituteTyVars' m x@ applies the (ordinary) map @m@ to type variables in @x@. + substituteTyVars' :: + Set PrimitiveLifecycle -> + Map Name (PrimitiveLifecycle, NamedType) -> + t -> t + +instance (SubstituteTyVars' a) => SubstituteTyVars' (Maybe a) where + substituteTyVars' avail tyenv = fmap (substituteTyVars' avail tyenv) + +instance (SubstituteTyVars' a) => SubstituteTyVars' [a] where + substituteTyVars' avail tyenv = map (substituteTyVars' avail tyenv) + +instance SubstituteTyVars' Type where + substituteTyVars' avail tyenv ty = case ty of + TyCon pos tc ts -> TyCon pos tc (substituteTyVars' avail tyenv ts) + TyRecord pos fs -> TyRecord pos (fmap (substituteTyVars' avail tyenv) fs) + TyUnifyVar _ _ -> ty + TyVar _ n -> + case Map.lookup n tyenv of + Nothing -> ty + Just (lc, expansion) -> + if not (Set.member lc avail) then + panic "substituteTyVars'" [ + "Found reference to non-visible typedef: " <> n, + "Lifecycle setting: " <> Text.pack (show lc) + ] + else case expansion of + AbstractType -> ty + ConcreteType ty' -> ty' + -- }}} diff --git a/saw-central/src/SAWCentral/Builtins.hs b/saw-central/src/SAWCentral/Builtins.hs index 0ef6d3c427..cfa4ed7389 100644 --- a/saw-central/src/SAWCentral/Builtins.hs +++ b/saw-central/src/SAWCentral/Builtins.hs @@ -31,7 +31,7 @@ import qualified Control.Exception as Ex import qualified Data.ByteString as StrictBS import qualified Data.ByteString.Lazy as BS import qualified Data.IntMap as IntMap -import Data.List (isPrefixOf, isInfixOf, sort) +import Data.List (isPrefixOf, isInfixOf, sort, intersperse) import qualified Data.Map as Map import Data.Parameterized.Classes (KnownRepr(..)) import Data.Set (Set) @@ -60,6 +60,8 @@ import qualified CryptolSAWCore.Cryptol as Cryptol import qualified CryptolSAWCore.Simpset as Cryptol -- saw-support +import qualified SAWSupport.ScopedMap as ScopedMap +--import SAWSupport.ScopedMap (ScopedMap) import qualified SAWSupport.Pretty as PPS (MemoStyle(..), Opts(..), pShowText) -- saw-core @@ -558,7 +560,7 @@ resolveNameIO sc cenv nm = -- exception is thrown. resolveName :: SharedContext -> Text -> TopLevel [VarIndex] resolveName sc nm = - do cenv <- SV.getCryptolEnv' + do cenv <- SV.getCryptolEnv scnms <- io (resolveNameIO sc cenv nm) case scnms of [] -> fail $ Text.unpack $ "Could not resolve name: " <> nm @@ -1590,7 +1592,7 @@ check_term :: TypedTerm -> TopLevel () check_term tt = do sc <- getSharedContext opts <- getTopLevelPPOpts - cenv <- SV.getCryptolEnv' + cenv <- SV.getCryptolEnv let t = ttTerm tt ty <- io $ scTypeCheckError sc t expectedTy <- @@ -1700,14 +1702,21 @@ cexEvalFn sc args tm = do envCmd :: TopLevel () envCmd = do - rw <- SV.getMergedEnv - let avail = rwPrimsAvail rw - vals = rwValueInfo rw - keep (_x, (_pos, lc, _rb, _ty, _v, _doc)) = Set.member lc avail - vals' = filter keep $ Map.assocs vals - printit (x, (_pos, _lc, _rb, ty, _v, _doc)) = x <> " : " <> PPS.pShowText ty opts <- getOptions - io $ sequence_ [ printOutLn opts Info (Text.unpack $ printit item) | item <- vals' ] + avail <- gets rwPrimsAvail + SV.Environ varenv _tyenv _cryenv <- gets rwEnviron + let printItem (x, (_pos, _lc, _rb, ty, _v, _doc)) = + printOutLn opts Info $ Text.unpack (x <> " : " <> PPS.pShowText ty) + -- Print only the visible objects + keep (_x, (_pos, lc, _rb, _ty, _v, _doc)) = Set.member lc avail + -- Insert a blank line in the output where there's a scope boundary + printScope mItems = case mItems of + Nothing -> printOutLn opts Info "" + Just items -> mapM_ printItem $ filter keep items + -- Reverse the list of scopes so the innermost prints last, + -- because that's what people will expect to see. + itemses = reverse $ ScopedMap.scopedAssocs varenv + io $ mapM_ printScope $ intersperse Nothing $ map Just itemses exitPrim :: Integer -> IO () exitPrim code = Exit.exitWith exitCode @@ -1766,7 +1775,7 @@ eval_bool t = do eval_int :: TypedTerm -> TopLevel Integer eval_int t = do sc <- getSharedContext - cenv <- SV.getCryptolEnv' + cenv <- SV.getCryptolEnv let cfg = CEnv.meSolverConfig (CEnv.eModuleEnv cenv) unless (null (getAllExts (ttTerm t))) $ fail "term contains symbolic variables" @@ -1825,7 +1834,7 @@ term_theories unints t = do default_typed_term :: TypedTerm -> TopLevel TypedTerm default_typed_term tt = do sc <- getSharedContext - cenv <- SV.getCryptolEnv' + cenv <- SV.getCryptolEnv let cfg = CEnv.meSolverConfig (CEnv.eModuleEnv cenv) opts <- getOptions io $ defaultTypedTerm opts sc cfg tt @@ -2099,7 +2108,7 @@ cryptol_load fileReader path = do cryptol_extract :: CEnv.ExtCryptolModule -> Text -> TopLevel TypedTerm cryptol_extract ecm var = do sc <- getSharedContext - ce <- SV.getCryptolEnv' + ce <- SV.getCryptolEnv let ?fileReader = StrictBS.readFile io $ CEnv.extractDefFromExtCryptolModule sc ce ecm var @@ -2111,7 +2120,7 @@ cryptol_extract ecm var = do -- probably a bad idea.) cryptol_add_path :: FilePath -> TopLevel () cryptol_add_path path = do - ce <- SV.getCryptolEnv' + ce <- SV.getCryptolEnv let me = CEnv.eModuleEnv ce let me' = me { C.meSearchPath = path : C.meSearchPath me } let ce' = ce { CEnv.eModuleEnv = me' } @@ -2119,14 +2128,14 @@ cryptol_add_path path = do cryptol_add_prim :: Text -> Text -> TypedTerm -> TopLevel () cryptol_add_prim mnm nm trm = do - ce <- SV.getCryptolEnv' + ce <- SV.getCryptolEnv let prim_name = C.PrimIdent (C.textToModName mnm) nm prims' = Map.insert prim_name (ttTerm trm) (CEnv.ePrims ce) SV.setCryptolEnv $ ce { CEnv.ePrims = prims' } cryptol_add_prim_type :: Text -> Text -> TypedTerm -> TopLevel () cryptol_add_prim_type mnm nm tp = do - ce <- SV.getCryptolEnv' + ce <- SV.getCryptolEnv let prim_name = C.PrimIdent (C.textToModName mnm) nm prim_types' = Map.insert prim_name (ttTerm tp) (CEnv.ePrimTypes ce) SV.setCryptolEnv $ ce { CEnv.ePrimTypes = prim_types' } diff --git a/saw-central/src/SAWCentral/Crucible/LLVM/Builtins.hs b/saw-central/src/SAWCentral/Crucible/LLVM/Builtins.hs index bbf490c314..33a7a1f843 100644 --- a/saw-central/src/SAWCentral/Crucible/LLVM/Builtins.hs +++ b/saw-central/src/SAWCentral/Crucible/LLVM/Builtins.hs @@ -484,18 +484,13 @@ llvm_compositional_extract (Some lm) nm func_name lemmas checkSat setup tactic = -- XXX could have a real position... let pos = PosInternal "llvm_compositional_extract" typed_extracted_func_const <- io $ mkTypedTerm shared_context extracted_func_const - rw <- getTopLevelRW - rw' <- - liftIO $ - extendEnv shared_context + extendEnv pos func_name ReadOnlyVar (tMono $ tTerm pos) Nothing -- FUTURE: slot for doc string, could put something here (VTerm typed_extracted_func_const) - rw - putTopLevelRW rw' let lemmaSet = Set.fromList (map (view MS.psSpecIdent) lemmas') diff --git a/saw-central/src/SAWCentral/Crucible/LLVM/X86.hs b/saw-central/src/SAWCentral/Crucible/LLVM/X86.hs index 889f15a2ca..045b13f240 100644 --- a/saw-central/src/SAWCentral/Crucible/LLVM/X86.hs +++ b/saw-central/src/SAWCentral/Crucible/LLVM/X86.hs @@ -437,7 +437,7 @@ llvm_verify_x86_common (Some (llvmModule :: LLVMModule x)) path nm globsyms chec opts <- getOptions basic_ss <- getBasicSS rw <- getTopLevelRW - cenv <- getCryptolEnv' + cenv <- getCryptolEnv sym <- liftIO $ newSAWCoreExprBuilder sc False mdMap <- liftIO $ newIORef mempty SomeOnlineBackend bak <- liftIO $ diff --git a/saw-central/src/SAWCentral/Value.hs b/saw-central/src/SAWCentral/Value.hs index 25e7a640f8..290a913bc8 100644 --- a/saw-central/src/SAWCentral/Value.hs +++ b/saw-central/src/SAWCentral/Value.hs @@ -51,23 +51,20 @@ module SAWCentral.Value ( showsPrecValue, -- used by SAWCentral.Builtins, SAWScript.Interpreter evaluateTypedTerm, - -- used by SAWScript.Interpreter (and in LocalEnv) - LocalBinding(..), - -- used by SAWScript.Interpreter, and appears in TopLevelRO - LocalEnv, - -- used by SAWScript.Interpreter, and in mergeLocalEnv - addTypedef, - -- used by SAWScript.REPL.Monad, and by getMergedEnv - mergeLocalEnv, - -- used by SAWCentral.Builtins, SAWScript.Interpreter, and by getCryptolEnv - getMergedEnv, getMergedEnv', + -- used by SAWScript.Search, SAWScript.Typechecker + TyEnv, VarEnv, + -- used by SAWCentral.Builtins, SAWScript.ValueOps, SAWScript.Interpreter, + -- SAWScript.REPL.Command, SAWScript.REPL.Monad, SAWServer.SAWServer + Environ(..), + -- used by SAWScript.Interpreter + pushScope, popScope, -- used by SAWCentral.Builtins, SAWScript.ValueOps, SAWScript.Interpreter, -- SAWServer.SAWServer CryptolEnvStack(..), -- used by SAWCentral.Crucible.LLVM.FFI, SAWCentral.Crucible.LLVM.X86, -- SAWCentral.Crucible.MIR.Builtins, SAWCentral.Builtins, -- SAWScript.Interpreter, SAWScript.REPL.Monad - getCryptolEnv, getCryptolEnv', + getCryptolEnv, -- used by SAWCentral.Builtins getCryptolEnvStack, -- used by SAWCentral.Builtins, SAWScript.Interpreter, SAWScript.REPL.Monad @@ -106,8 +103,6 @@ module SAWCentral.Value ( pushTraceFrames, popTraceFrames, -- used by SAWScript.Interpreter RefChain, - -- used by SAWScript.Interpreter plus appears in getMergedEnv - getLocalEnv, -- used in various places in SAWCentral, and in selected builtins in -- SAWScript.Interpreter getPosition, @@ -154,8 +149,10 @@ module SAWCentral.Value ( -- used by SAWCentral.Crucible.LLVM.Builtins, SAWScript.Interpreter -- ... the use in LLVM is the abusive insertion done by llvm_compositional_extract -- XXX: we're going to need to clean that up - -- (also appears in mergeLocalEnv) extendEnv, + extendEnvMulti, + -- used by SAWScript.Interpreter + addTypedef, -- used by various places in SAWCentral.Crucible, SAWCentral.Builtins -- XXX: it wraps TopLevel rather than being part of it; is that necessary? CrucibleSetup, @@ -224,7 +221,6 @@ import Control.Monad.IO.Class (MonadIO, liftIO) import Control.Monad.Reader (ReaderT(..), ask, asks) import Control.Monad.State (StateT(..), MonadState(..), gets, modify) import Control.Monad.Trans.Class (MonadTrans(lift)) -import Data.Foldable(foldrM) import Data.List.Extra ( dropEnd ) import qualified Data.Map as M import Data.Map ( Map ) @@ -239,6 +235,8 @@ import System.FilePath(()) import qualified Data.AIG as AIG +import qualified SAWSupport.ScopedMap as ScopedMap +import SAWSupport.ScopedMap (ScopedMap) import qualified SAWSupport.Pretty as PPS (Opts, defaultOpts, showBrackets, showBraces, showCommaSep) import SAWCentral.Panic (panic) @@ -521,7 +519,7 @@ data Value | VArray [Value] | VTuple [Value] | VRecord (Map SS.Name Value) - | VLambda LocalEnv (Maybe SS.Name) SS.Pattern SS.Expr + | VLambda Environ (Maybe SS.Name) SS.Pattern SS.Expr -- | Function-shaped value that's a Haskell-level function. This -- is how builtins appear. Includes the name of the builtin and -- the list of arguments applied so far, as a Seq to allow @@ -535,7 +533,7 @@ data Value -- | Returned value in unspecified monad. | VReturn SS.Pos RefChain Value -- | Not-yet-executed do-block in unspecified monad. - | VDo RefChain LocalEnv ([SS.Stmt], SS.Expr) + | VDo RefChain Environ ([SS.Stmt], SS.Expr) -- | Single monadic bind in unspecified monad. -- -- This exists only to support the "for" builtin; see notes there @@ -758,82 +756,73 @@ evaluateTypedTerm _sc (TypedTerm tp _) = -- TopLevel Monad -------------------------------------------------------------- +-- | The variable environment: a map from variable names to: +-- - the definition position +-- - the lifecycle setting (experimental/current/deprecated/etc) +-- - whether the binding is rebindable +-- - the type scheme +-- - the value +-- - the help text if any +type VarEnv = ScopedMap SS.Name (SS.Pos, SS.PrimitiveLifecycle, SS.Rebindable, + SS.Schema, Value, Maybe [Text]) + +-- | The type environment: a map from type names to: +-- - the lifecycle setting (experimental/current/deprecated/etc) +-- - the expansion, which might be another type (this is how +-- typedefs/type aliases appear) or "abstract" (this is how +-- builtin types that aren't special cases in the AST appear) +type TyEnv = ScopedMap SS.Name (SS.PrimitiveLifecycle, SS.NamedType) + -- | The full Cryptol environment. We maintain a stack of plain -- Cryptol environments and push/pop them as we enter and leave -- scopes; otherwise the Cryptol environment doesn't track SAWScript -- scopes and horribly confusing wrong things happen. data CryptolEnvStack = CryptolEnvStack CEnv.CryptolEnv [CEnv.CryptolEnv] --- | Entry in the interpreter's local (as opposed to global) variable --- environment. --- --- The Maybe [Text] field is the help text for the value, if any. --- Note that currently there's no way I know of to actually provide --- help text for a local variable, nor is there any way to get at --- one with the REPL :help command to print it, but the interpreter's --- plumbing demands that the field exist... +-- | Type for the ordinary interpreter environment. -- -data LocalBinding - = LocalLet SS.Pos SS.Name SS.Rebindable SS.Schema (Maybe [Text]) Value - | LocalTypedef SS.Name SS.Type - deriving (Show) +-- There's one environment that maps variable names to values, and +-- one that maps type names to types. A third handles the Cryptol +-- domain. All three get closed in with lambdas and do-blocks at the +-- appropriate times. +data Environ = Environ { + eVarEnv :: VarEnv, + eTyEnv :: TyEnv, + eCryptol :: CryptolEnvStack +} + +-- | Enter a scope. +pushScope :: TopLevel () +pushScope = do + Environ varenv tyenv cryenv <- gets rwEnviron + let varenv' = ScopedMap.push varenv + tyenv' = ScopedMap.push tyenv + cryenv' = cryptolPush cryenv + modifyTopLevelRW (\rw -> rw { rwEnviron = Environ varenv' tyenv' cryenv' }) + +-- | Leave a scope. This will panic if you try to leave the last scope; +-- pushes and pops should be matched. +popScope :: TopLevel () +popScope = do + Environ varenv tyenv cryenv <- gets rwEnviron + let varenv' = ScopedMap.pop varenv + tyenv' = ScopedMap.pop tyenv + cryenv' = cryptolPop cryenv + modifyTopLevelRW (\rw -> rw { rwEnviron = Environ varenv' tyenv' cryenv' }) -type LocalEnv = [LocalBinding] - --- Note that the expansion type should have already been through the --- typechecker, so it's ok to panic if it turns out to be broken. -addTypedef :: SS.Name -> SS.Type -> TopLevelRW -> TopLevelRW -addTypedef name ty rw = - let primsAvail = rwPrimsAvail rw - typeInfo = rwTypeInfo rw - ty' = SS.substituteTyVars primsAvail typeInfo ty - typeInfo' = M.insert name (SS.Current, SS.ConcreteType ty') typeInfo - in - rw { rwTypeInfo = typeInfo' } - -mergeLocalEnv :: SharedContext -> LocalEnv -> TopLevelRW -> IO TopLevelRW -mergeLocalEnv sc env rw = foldrM addBinding rw env - where addBinding (LocalLet pos x rb ty md v) = extendEnv sc pos x rb ty md v - addBinding (LocalTypedef n ty) = pure . addTypedef n ty - --- XXX: it is not sane to both be in the TopLevel monad and return a TopLevelRW --- (especially since the one returned is specifically not the same as the one --- in the monad state) -getMergedEnv :: TopLevel TopLevelRW -getMergedEnv = - do sc <- getSharedContext - env <- getLocalEnv - rw <- getTopLevelRW - liftIO $ mergeLocalEnv sc env rw - --- Variant of getMergedEnv that takes an explicit local part --- (this avoids trying to use it with withLocalEnv, which doesn't work) -getMergedEnv' :: LocalEnv -> TopLevel TopLevelRW -getMergedEnv' env = do - sc <- getSharedContext - rw <- getTopLevelRW - liftIO $ mergeLocalEnv sc env rw -- | Get the current Cryptol environment. getCryptolEnv :: TopLevel CEnv.CryptolEnv getCryptolEnv = do - env <- getMergedEnv - let CryptolEnvStack ce _ = rwCryptol env - return ce - --- | Get the current Cryptol environment. --- --- Variant version that doesn't call getMergedEnv, to avoid --- unexpected behavioral changes in this commit. -getCryptolEnv' :: TopLevel CEnv.CryptolEnv -getCryptolEnv' = do - CryptolEnvStack ce _ <- gets rwCryptol + Environ _varenv _tyenv cryenvs <- gets rwEnviron + let CryptolEnvStack ce _ = cryenvs return ce -- | Get the current full stack of Cryptol environments. getCryptolEnvStack :: TopLevel CryptolEnvStack -getCryptolEnvStack = - gets rwCryptol +getCryptolEnvStack = do + Environ _varenv _tyenv cryenvs <- gets rwEnviron + return cryenvs -- | Update the current Cryptol environment. -- @@ -841,8 +830,10 @@ getCryptolEnvStack = -- value applied has not become stale. setCryptolEnv :: CEnv.CryptolEnv -> TopLevel () setCryptolEnv ce = do - CryptolEnvStack _ ces <- gets rwCryptol - modify (\rw -> rw { rwCryptol = CryptolEnvStack ce ces }) + Environ varenv tyenv cryenvs <- gets rwEnviron + let CryptolEnvStack _ ces = cryenvs + let cryenvs' = CryptolEnvStack ce ces + modify (\rw -> rw { rwEnviron = Environ varenv tyenv cryenvs' }) -- | Get the current Cryptol environment from a TopLevelRW. -- @@ -853,7 +844,9 @@ setCryptolEnv ce = do -- all. rwGetCryptolEnv :: TopLevelRW -> CEnv.CryptolEnv rwGetCryptolEnv rw = - let CryptolEnvStack ce _ = rwCryptol rw in + let Environ _varenv _tyenv cryenvs = rwEnviron rw + CryptolEnvStack ce _ = cryenvs + in ce -- | Get the current full stack of Cryptol environments from a @@ -861,7 +854,8 @@ rwGetCryptolEnv rw = -- way. (XXX) rwGetCryptolEnvStack :: TopLevelRW -> CryptolEnvStack rwGetCryptolEnvStack rw = - rwCryptol rw + let Environ _varenv _tyenv cryenvs = rwEnviron rw in + cryenvs -- | Update the current Cryptol environment in a TopLevelRW. -- @@ -876,8 +870,11 @@ rwGetCryptolEnvStack rw = -- all. rwSetCryptolEnv :: CEnv.CryptolEnv -> TopLevelRW -> TopLevelRW rwSetCryptolEnv ce rw = - let CryptolEnvStack _ ces = rwCryptol rw in - rw { rwCryptol = CryptolEnvStack ce ces } + let Environ varenv tyenv cryenvs = rwEnviron rw + CryptolEnvStack _ ces = cryenvs + cryenvs' = CryptolEnvStack ce ces + in + rw { rwEnviron = Environ varenv tyenv cryenvs' } -- | Update the current full stack of Cryptol environments in a -- TopLevelRW. Used by the checkpointing logic, in a fairly @@ -887,7 +884,8 @@ rwSetCryptolEnv ce rw = -- done anything to make the value they're working with stale. rwSetCryptolEnvStack :: CryptolEnvStack -> TopLevelRW -> TopLevelRW rwSetCryptolEnvStack cryenvs rw = - rw { rwCryptol = cryenvs } + let Environ varenv tyenv _ = rwEnviron rw in + rw { rwEnviron = Environ varenv tyenv cryenvs } -- | Modify the current Cryptol environment in a TopLevelRW. -- @@ -898,24 +896,22 @@ rwSetCryptolEnvStack cryenvs rw = -- all. rwModifyCryptolEnv :: (CEnv.CryptolEnv -> CEnv.CryptolEnv) -> TopLevelRW -> TopLevelRW rwModifyCryptolEnv f rw = - let CryptolEnvStack ce ces = rwCryptol rw + let Environ varenv tyenv cryenvs = rwEnviron rw + CryptolEnvStack ce ces = cryenvs ce' = f ce + cryenvs' = CryptolEnvStack ce' ces in - rw { rwCryptol = CryptolEnvStack ce' ces } + rw { rwEnviron = Environ varenv tyenv cryenvs' } -- | Push a new scope on the Cryptol environment stack. --- --- (Not used yet.) -_cryptolPush :: CryptolEnvStack -> CryptolEnvStack -_cryptolPush (CryptolEnvStack ce ces) = +cryptolPush :: CryptolEnvStack -> CryptolEnvStack +cryptolPush (CryptolEnvStack ce ces) = -- Each entry is the whole environment, so duplicate the top entry CryptolEnvStack ce (ce : ces) -- | Pop the current scope off the Cryptol environment stack. --- --- (Not used yet.) -_cryptolPop :: CryptolEnvStack -> CryptolEnvStack -_cryptolPop (CryptolEnvStack _ ces) = +cryptolPop :: CryptolEnvStack -> CryptolEnvStack +cryptolPop (CryptolEnvStack _ ces) = -- Discard the top case ces of [] -> panic "cryptolPop" ["Cryptol environment scope stack ran out"] @@ -954,25 +950,8 @@ data JavaCodebase = data TopLevelRW = TopLevelRW { - -- | The variable environment: a map from variable names to: - -- - the definition position - -- - the lifecycle setting (experimental/current/deprecated/etc) - -- - whether the binding is rebindable - -- - the type scheme - -- - the value - -- - the help text if any - rwValueInfo :: Map SS.Name (SS.Pos, SS.PrimitiveLifecycle, SS.Rebindable, - SS.Schema, Value, Maybe [Text]) - - -- | The type environment: a map from type names to: - -- - the lifecycle setting (experimental/current/deprecated/etc) - -- - the expansion, which might be another type (this is how - -- typedefs/type aliases appear) or "abstract" (this is how - -- builtin types that aren't special cases in the AST appear) - , rwTypeInfo :: Map SS.Name (SS.PrimitiveLifecycle, SS.NamedType) - - -- | The Cryptol naming environment. - , rwCryptol :: CryptolEnvStack + -- | The variable and type naming environment. + rwEnviron :: Environ -- | The current execution position. This is only valid when the -- interpreter is calling out into saw-central to execute a @@ -984,8 +963,6 @@ data TopLevelRW = -- | The current stack trace. The most recent frame is at the front. , rwStackTrace :: Trace - , rwLocalEnv :: LocalEnv - , rwJavaCodebase :: JavaCodebase -- ^ Current state of Java sub-system. , rwProofs :: [Value] {- ^ Values, generated anywhere, that represent proofs. -} @@ -1130,10 +1107,6 @@ popTraceFrames :: [a] -> TopLevel () popTraceFrames frames = mapM_ (\_ -> popTraceFrame) frames -getLocalEnv :: TopLevel LocalEnv -getLocalEnv = - gets rwLocalEnv - -- | Get the current execution position. getPosition :: TopLevel SS.Pos getPosition = @@ -1289,12 +1262,19 @@ addJVMTrans trans = do let jvmt = rwJVMTrans rw putTopLevelRW ( rw { rwJVMTrans = trans <> jvmt }) -extendEnv :: - SharedContext -> - SS.Pos -> SS.Name -> SS.Rebindable -> SS.Schema -> Maybe [Text] -> Value -> - TopLevelRW -> IO TopLevelRW -extendEnv sc pos name rb ty doc v rw = - do ce' <- +extendEnv :: SS.Pos -> SS.Name -> SS.Rebindable -> SS.Schema -> Maybe [Text] -> Value -> TopLevel () +extendEnv pos name rb ty doc v = do + sc <- gets rwSharedContext + let ident = T.mkIdent name + modname = T.packModName [name] + + -- Update the SAWScript environment. + Environ varenv tyenv cryenvs <- gets rwEnviron + let varenv' = ScopedMap.insert name (pos, SS.Current, rb, ty, v, doc) varenv + + -- Mirror the value into the Cryptol environment if appropriate. + let CryptolEnvStack ce ces = cryenvs + ce' <- case v of VTerm t -> pure $ CEnv.bindTypedTerm (ident, t) ce @@ -1305,20 +1285,60 @@ extendEnv sc pos name rb ty doc v rw = VCryptolModule m -> pure $ CEnv.bindExtCryptolModule (modname, m) ce VString s -> - do tt <- typedTermOfString sc (Text.unpack s) + do tt <- io $ typedTermOfString sc (Text.unpack s) pure $ CEnv.bindTypedTerm (ident, tt) ce VBool b -> - do tt <- typedTermOfBool sc b + do tt <- io $ typedTermOfBool sc b pure $ CEnv.bindTypedTerm (ident, tt) ce _ -> pure ce - let valenv = rwValueInfo rw - valenv' = M.insert name (pos, SS.Current, rb, ty, v, doc) valenv - pure $ rw { rwValueInfo = valenv', rwCryptol = CryptolEnvStack ce' ces } - where - ident = T.mkIdent name - modname = T.packModName [name] - CryptolEnvStack ce ces = rwCryptol rw + let cryenvs' = CryptolEnvStack ce' ces + + -- Drop the new bits into place. + modify (\rw -> rw { rwEnviron = Environ varenv' tyenv cryenvs' }) + +extendEnvMulti :: [(SS.Pos, SS.Name, SS.Rebindable, SS.Schema, Maybe [Text], Environ -> Value)] -> TopLevel () +extendEnvMulti bindings = do + + -- Update the SAWScript environment. + Environ varenv tyenv cryenv <- gets rwEnviron + + -- Insert all the bindings at once, and feed the final resulting + -- interpreter environment into each value. This circular + -- definition only works because of laziness and it's only legal + -- when the pieces are in a single let-block. + -- + -- Only allow lambda values because that's the only use case + -- (functions in mutually recursive "rec" sets) and it lets us + -- ignore the Cryptol environment. + -- + -- Be sure to insert v' (rather than v) so the panic check is + -- actually performed. + let insert (pos, name, rb, ty, doc, fv) tmpenv = + let v = fv environ' + v' = case v of + VLambda{} -> v + _ -> + panic "extendEnvMulti" [ + "Non-lambda value: " <> Text.pack (show v) + ] + in + ScopedMap.insert name (pos, SS.Current, rb, ty, v', doc) tmpenv + varenv' = foldr insert varenv bindings + environ' = Environ varenv' tyenv cryenv + + -- Drop the new bits into place. + modify (\rw -> rw { rwEnviron = environ' }) + +-- Note that the expansion type should have already been through the +-- typechecker, so it's ok to panic if it turns out to be broken. +addTypedef :: SS.Name -> SS.Type -> TopLevel () +addTypedef name ty = do + avail <- gets rwPrimsAvail + Environ varenv tyenv cryenv <- gets rwEnviron + let ty' = SS.substituteTyVars avail tyenv ty + tyenv' = ScopedMap.insert name (SS.Current, SS.ConcreteType ty') tyenv + modify (\rw -> rw { rwEnviron = Environ varenv tyenv' cryenv }) typedTermOfString :: SharedContext -> String -> IO TypedTerm typedTermOfString sc str = diff --git a/saw-script/src/SAWScript/Interpreter.hs b/saw-script/src/SAWScript/Interpreter.hs index cae0cd7f3f..5a986fbcf4 100644 --- a/saw-script/src/SAWScript/Interpreter.hs +++ b/saw-script/src/SAWScript/Interpreter.hs @@ -33,9 +33,8 @@ import qualified Control.Exception as X import Control.Monad (unless, (>=>), when) import Control.Monad.Reader (ask, asks) import Control.Monad.State (gets) -import Control.Monad.IO.Class (liftIO) import qualified Data.ByteString as BS -import Data.Maybe (fromMaybe) +import Data.Maybe (fromMaybe, mapMaybe) import Data.List (genericLength) import qualified Data.Map as Map import Data.Map ( Map ) @@ -64,6 +63,8 @@ import Mir.Intrinsics (MIR) import qualified Mir.Generator as MIR (RustModule) import qualified Mir.Mir as MIR +import qualified SAWSupport.ScopedMap as ScopedMap +--import SAWSupport.ScopedMap (ScopedMap) import qualified SAWSupport.Pretty as PPS (MemoStyle(..), Opts(..), defaultOpts, pShow, pShowText) import SAWCore.FiniteValue (FirstOrderValue(..)) @@ -131,6 +132,7 @@ import qualified Cryptol.Backend.Monad as V (runEval) import qualified Cryptol.Eval.Value as V (defaultPPOpts, ppValue) import qualified Cryptol.Eval.Concrete as V (Concrete(..)) +import qualified Prettyprinter as PP (pretty) import qualified Prettyprinter.Render.Text as PP (putDoc) import SAWScript.AutoMatch @@ -288,71 +290,38 @@ propagateRefChain chain1 v = -- -- XXX: at some point clean this up further. -- -bindPatternLocal :: - SS.Rebindable -> SS.Pattern -> Maybe SS.Schema -> Value -> - LocalEnv -> LocalEnv -bindPatternLocal rb pat ms v env = +bindPattern :: SS.Rebindable -> SS.Pattern -> Maybe SS.Schema -> Value -> TopLevel () +bindPattern rb pat ms v = case pat of SS.PWild _pos _ -> - env + pure () SS.PVar allpos _xpos _x Nothing -> - panic "bindPatternLocal" [ + panic "bindPattern" [ "Found pattern with no type in it", "Source position: " <> Text.pack (show allpos), "Pattern: " <> Text.pack (show pat) ] SS.PVar _allpos xpos x (Just ty) -> let s = fromMaybe (SS.tMono ty) ms in - extendLocal xpos x rb s Nothing v env + extendEnv xpos x rb s Nothing v SS.PTuple _pos ps -> case v of - VTuple vs -> foldr ($) env (zipWith3 (bindPatternLocal rb) ps mss vs) - where mss = case ms of - Nothing -> - repeat Nothing - Just (SS.Forall ks (SS.TyCon _ (SS.TupleCon _) ts)) -> - [ Just (SS.Forall ks t) | t <- ts ] - Just t -> - panic "bindPatternLocal" [ - "Expected tuple type, got " <> Text.pack (show t) - ] + VTuple vs -> do + let mss = case ms of + Nothing -> + repeat Nothing + Just (SS.Forall ks (SS.TyCon _ (SS.TupleCon _) ts)) -> + [ Just (SS.Forall ks t) | t <- ts ] + Just t -> + panic "bindPattern" [ + "Expected tuple type, got " <> Text.pack (show t) + ] + sequence_ $ zipWith3 (bindPattern rb) ps mss vs _ -> panic "bindPatternLocal" [ "Expected tuple value; got " <> Text.pack (show v) ] --- See notes in bindPatternLocal above regarding the schema argument. -bindPatternEnv :: SS.Pattern -> Maybe SS.Schema -> Value -> TopLevelRW -> TopLevel TopLevelRW -bindPatternEnv pat ms v env = - case pat of - SS.PWild _pos _ -> - pure env - SS.PVar allpos _xpos _x Nothing -> - panic "bindPatternEnv" [ - "Found pattern with no type in it", - "Source position: " <> Text.pack (show allpos), - "Pattern: " <> Text.pack (show pat) - ] - SS.PVar _allpos xpos x (Just ty) -> do - sc <- getSharedContext - let s = fromMaybe (SS.tMono ty) ms - liftIO $ extendEnv sc xpos x SS.ReadOnlyVar s Nothing v env - SS.PTuple _pos ps -> - case v of - VTuple vs -> foldr (=<<) (pure env) (zipWith3 bindPatternEnv ps mss vs) - where mss = case ms of - Nothing -> repeat Nothing - Just (SS.Forall ks (SS.TyCon _ (SS.TupleCon _) ts)) -> - [ Just (SS.Forall ks t) | t <- ts ] - Just t -> - panic "bindPatternEnv" [ - "Expected tuple type, got " <> Text.pack (show t) - ] - _ -> - panic "bindPatternEnv" [ - "Expected tuple value; got " <> Text.pack (show v) - ] - ------------------------------------------------------------ -- InterpreterMonad @@ -365,42 +334,54 @@ class (Monad m, MonadFail m) => InterpreterMonad m where actionFromValue :: FromValue a => FromValueHow -> Value -> m a mkValue :: SS.Pos -> RefChain -> m Value -> Value getMonadContext :: m SS.Context - withLocalEnvAny :: LocalEnv -> m a -> m a + pushScopeAny :: m () + popScopeAny :: m () + withEnvironAny :: Environ -> m a -> m a instance InterpreterMonad TopLevel where liftTopLevel m = m actionFromValue = fromValue mkValue pos chain m = VTopLevel pos chain m getMonadContext = return SS.TopLevel - withLocalEnvAny = withLocalEnv + pushScopeAny = pushScope + popScopeAny = popScope + withEnvironAny = withEnviron instance InterpreterMonad ProofScript where liftTopLevel m = scriptTopLevel m actionFromValue = fromValue mkValue pos chain m = VProofScript pos chain m getMonadContext = return SS.ProofScript - withLocalEnvAny = withLocalEnvProof + pushScopeAny = scriptTopLevel pushScope + popScopeAny = scriptTopLevel popScope + withEnvironAny = withEnvironProofScript instance InterpreterMonad LLVMCrucibleSetupM where liftTopLevel m = llvmTopLevel m actionFromValue = fromValue mkValue pos chain m = VLLVMCrucibleSetup pos chain m getMonadContext = return SS.LLVMSetup - withLocalEnvAny = withLocalEnvLLVM + pushScopeAny = llvmTopLevel pushScope + popScopeAny = llvmTopLevel popScope + withEnvironAny = withEnvironLLVM instance InterpreterMonad JVMSetupM where liftTopLevel m = jvmTopLevel m actionFromValue = fromValue mkValue pos chain m = VJVMSetup pos chain m getMonadContext = return SS.JavaSetup - withLocalEnvAny = withLocalEnvJVM + pushScopeAny = jvmTopLevel pushScope + popScopeAny = jvmTopLevel popScope + withEnvironAny = withEnvironJVM instance InterpreterMonad MIRSetupM where liftTopLevel m = mirTopLevel m actionFromValue = fromValue mkValue pos chain m = VMIRSetup pos chain m getMonadContext = return SS.MIRSetup - withLocalEnvAny = withLocalEnvMIR + pushScopeAny = mirTopLevel pushScope + popScopeAny = mirTopLevel popScope + withEnvironAny = withEnvironMIR ------------------------------------------------------------ @@ -441,7 +422,12 @@ applyValue pos v1info v1 v2 = VLambda env mname pat e -> do let name = fromMaybe "(lambda)" mname enter name - r <- withLocalEnv (bindPatternLocal SS.ReadOnlyVar pat Nothing v2 env) (interpretExpr e) + r <- withEnviron env $ do + pushScope + bindPattern SS.ReadOnlyVar pat Nothing v2 + r' <- interpretExpr e + popScope + return r' leave return $ insertRefChain pos name r VBuiltin name args wf -> case wf of @@ -504,7 +490,7 @@ interpretExpr expr = SS.Array _pos es -> VArray <$> traverse interpretExpr es SS.Block _pos stmts -> do - env <- getLocalEnv + env <- gets rwEnviron return $ VDo [] env stmts SS.Tuple _pos es -> VTuple <$> traverse interpretExpr es @@ -521,15 +507,16 @@ interpretExpr expr = a <- interpretExpr e return (tupleLookupValue pos a i) SS.Var pos x -> do - rw <- getMergedEnv - case Map.lookup x (rwValueInfo rw) of + avail <- gets rwPrimsAvail + Environ varenv _tyenv _cryenv <- gets rwEnviron + case ScopedMap.lookup x varenv of Nothing -> -- This should be rejected by the typechecker, so panic panic "interpretExpr" [ "Read of unknown variable " <> x ] Just (_defpos, lc, _rebindable, _ty, v, _doc) - | Set.member lc (rwPrimsAvail rw) -> do + | Set.member lc avail -> do let v' = injectPositionIntoMonadicValue pos v v'' = insertRefChain pos x v' return v'' @@ -539,7 +526,7 @@ interpretExpr expr = "Read of inaccessible variable " <> x ] SS.Lambda _pos mname pat e -> do - env <- getLocalEnv + env <- gets rwEnviron return $ VLambda env mname pat e SS.Application pos e1 e2 -> do let v1info = "Expression: " <> PPS.pShowText e1 @@ -548,8 +535,11 @@ interpretExpr expr = let v2' = injectPositionIntoMonadicValue (SS.getPos e2) v2 applyValue pos v1info v1 v2' SS.Let _ dg e -> do - env' <- interpretDeclGroup SS.ReadOnlyVar dg - withLocalEnv env' (interpretExpr e) + pushScope + interpretDeclGroup SS.ReadOnlyVar dg + v <- interpretExpr e + popScope + return v SS.TSig _ e _ -> interpretExpr e SS.IfThenElse pos e1 e2 e3 -> do @@ -565,39 +555,73 @@ interpretExpr expr = "Expression: " <> PPS.pShowText e1 ] --- Eval a "decl", which is the RHS of a let-binding. --- Evaluates the body expression purely. -interpretDecl :: SS.Rebindable -> LocalEnv -> SS.Decl -> TopLevel LocalEnv -interpretDecl rebindable env (SS.Decl _ pat mt expr) = do - v <- interpretExpr expr - return (bindPatternLocal rebindable pat mt v env) - --- Eval the RHS of a single let-binding in a mutually recursive group. --- These are required to be functions; that's enforced by the --- typechecker. -interpretFunction :: LocalEnv -> SS.Expr -> Value -interpretFunction env expr = - case expr of - SS.Lambda _ mname pat e -> VLambda env mname pat e - SS.TSig _ e _ -> interpretFunction env e - _ -> - panic "interpretFunction" [ - "Not a function", - "Expression found: " <> PPS.pShowText expr - ] - -- Eval a "decl group", which is a let-binding or group of mutually -- recursive let-bindings. -interpretDeclGroup :: SS.Rebindable -> SS.DeclGroup -> TopLevel LocalEnv -interpretDeclGroup rebindable (SS.NonRecursive d) = do - env <- getLocalEnv - interpretDecl rebindable env d -interpretDeclGroup rebindable (SS.Recursive ds) = do - env <- getLocalEnv - let addDecl (SS.Decl _ pat mty e) = - bindPatternLocal rebindable pat mty (interpretFunction env' e) - env' = foldr addDecl env ds - return env' +-- +-- The bodies are interpreted purely. +interpretDeclGroup :: SS.Rebindable -> SS.DeclGroup -> TopLevel () +interpretDeclGroup rebindable dg = case dg of + SS.NonRecursive (SS.Decl _ pat mt expr) -> do + v <- interpretExpr expr + bindPattern rebindable pat mt v + SS.Recursive ds -> do + let + + -- Get a value for the body of one of the declarations. + -- Recursive declaration sets are only allowed to contain + -- functions; panic if we get anything else. + -- + -- We return a function taking an environment because we + -- need to close in the environment containing _all_ the + -- declarations _into_ all the declarations, which is a + -- circular knot that can only be constructed in very + -- specific ways. + extractFunction e0 = case e0 of + SS.Lambda _ mname pat e1 -> + \env -> VLambda env mname pat e1 + SS.TSig _ e1 _ -> + extractFunction e1 + _ -> + panic "interpretDeclGroup" [ + "Found non-function in a recursive declaration group", + -- XXX should print the name here! + "Expression found: " <> PPS.pShowText e0 + ] + + -- Get the name (and type) for one of the declarations. + -- Recursive declaration sets are only allowed to contain + -- functions, so the pattern cannot be a tuple. + extractName pat = case pat of + SS.PWild _ _ -> Nothing + SS.PVar _ xpos x (Just ty) -> Just (xpos, x, ty) + SS.PVar _ _ x Nothing -> + panic "interpretDeclGroup" [ + "Found variable with no type in a recursive decl group", + "Variable: " <> x + ] + SS.PTuple{} -> + panic "interpretDeclGroup" [ + "Found tuple pattern in a recursive declaration group", + "Pattern: " <> Text.pack (show (PP.pretty pat)) + ] + + -- Get all the info for a decl. + extractBoth (SS.Decl _ pat _mty e) = + case extractName pat of + Nothing -> Nothing + Just (xpos, x, ty) -> + let fv = extractFunction e in + Just (xpos, x, rebindable, SS.tMono ty, Nothing, fv) + + -- Extract all the info for all decls. + ds' = mapMaybe extractBoth ds + + -- Now add all the declarations. + -- + -- Note that the lambdas in all the declarations need the final + -- resulting environment that contains all the declarations, + -- which is something of a headache to arrange in Haskell. + extendEnvMulti ds' -- Bind a monadic value into the monadic execution sequence. -- @@ -648,7 +672,11 @@ interpretMonadAction fromHow v = case v of FromArgument -> pushTraceFrame SS.PosInsideBuiltin "(callback)" pushTraceFrames chain - r <- withLocalEnvAny env (interpretDoStmts body) + r <- withEnvironAny env $ do + pushScopeAny + r' <- interpretDoStmts body + popScopeAny + return r' liftTopLevel $ do popTraceFrames chain @@ -708,13 +736,12 @@ interpretMonadAction fromHow v = case v of -- (XXX: should that be stored into the monad context or not? Apparently -- not, currently.) -- -interpretDoStmt :: forall m. InterpreterMonad m => SS.Stmt -> m LocalEnv +interpretDoStmt :: forall m. InterpreterMonad m => SS.Stmt -> m () interpretDoStmt stmt = let ?fileReader = BS.readFile in -- XXX are the uses of push/popPosition here suitable? not super clear case stmt of SS.StmtBind pos pat e -> do - env <- liftTopLevel getLocalEnv -- Execute the expression purely first. ("purely") baseVal :: Value <- liftTopLevel $ interpretExpr e -- Now bind the resulting value to execute it. @@ -725,26 +752,21 @@ interpretDoStmt stmt = result :: Value <- bindMonadAction pos baseVal -- Bind (in the name-binding, not monad-binding sense) the -- result to the pattern. - return $ bindPatternLocal SS.ReadOnlyVar pat Nothing result env + liftTopLevel $ bindPattern SS.ReadOnlyVar pat Nothing result SS.StmtLet _pos rebindable dg -> do -- Process the declarations liftTopLevel $ interpretDeclGroup rebindable dg SS.StmtCode _ spos str -> do liftTopLevel $ do sc <- getSharedContext - rw <- getMergedEnv - let ce = rwGetCryptolEnv rw - + ce <- getCryptolEnv let str' = toInputText spos str ce' <- io $ CEnv.parseDecls sc ce str' - putTopLevelRW $ rwSetCryptolEnv ce' rw - -- return the current local environment unchanged - liftTopLevel getLocalEnv + setCryptolEnv ce' SS.StmtImport _ _ -> fail "block-level import unimplemented" SS.StmtTypedef _ _ name ty -> do - env <- liftTopLevel $ getLocalEnv - return $ LocalTypedef name ty : env + liftTopLevel $ addTypedef name ty -- Eval some statements from a do-block. -- @@ -800,10 +822,11 @@ interpretDoStmts (stmts, lastexpr) = return $ mkValue pos [] result' stmt : more -> do - -- Execute the expression and get the updated environment - env' <- interpretDoStmt stmt + -- Execute the expression and update the environment + interpretDoStmt stmt -- Run the rest of the block with the updated environment - withLocalEnvAny env' (interpretDoStmts (more, lastexpr)) + v <- interpretDoStmts (more, lastexpr) + return v -- Execute a top-level bind. processStmtBind :: @@ -813,8 +836,7 @@ processStmtBind :: SS.Pattern -> SS.Expr -> m () -processStmtBind printBinds pos pat expr = do -- mx mt - rw <- liftTopLevel getMergedEnv +processStmtBind printBinds pos pat expr = do -- Eval the expression baseVal <- liftTopLevel $ interpretExpr expr @@ -844,7 +866,7 @@ processStmtBind printBinds pos pat expr = do -- mx mt -- When in the repl, print the result. when printBinds $ do - let opts = rwPPOpts rw + opts <- liftTopLevel $ gets rwPPOpts -- Extract the variable, if any, from the pattern. If there isn't -- any single variable use "it". @@ -867,9 +889,7 @@ processStmtBind printBinds pos pat expr = do -- mx mt liftTopLevel $ printOutLnTop Info $ Text.unpack $ name <> " : " <> PPS.pShowText ty _ -> return () - liftTopLevel $ - do rw' <- getTopLevelRW - putTopLevelRW =<< bindPatternEnv pat (Just (SS.tMono ty)) result rw' + liftTopLevel $ bindPattern SS.ReadOnlyVar pat (Just (SS.tMono ty)) result -- | Interpret a top-level statement in an interpreter monad (any of the SAWScript monads) -- This duplicates the logic in interpretDoStmt for no particularly good reason. @@ -880,11 +900,17 @@ interpretTopStmt :: InterpreterMonad m => interpretTopStmt printBinds stmt = do let ?fileReader = BS.readFile + avail <- liftTopLevel $ gets rwPrimsAvail ctx <- getMonadContext - rw <- liftTopLevel getMergedEnv - let valueInfo = rwValueInfo rw - valueInfo' = Map.map (\(pos, lc, rb, ty, _v, _doc) -> (pos, lc, rb, ty)) valueInfo - stmt' <- processTypeCheck $ checkStmt (rwPrimsAvail rw) valueInfo' (rwTypeInfo rw) ctx stmt + + stmt' <- do + -- XXX this is not the right way to do this + -- - shouldn't have to flatten the environments + -- - shouldn't be typechecking one statement at a time regardless + Environ varenv tyenv _cryenvs <- liftTopLevel $ gets rwEnviron + let varenv' = Map.map (\(pos, lc, rb, ty, _v, _doc) -> (pos, lc, rb, ty)) $ ScopedMap.flatten varenv + let tyenv' = ScopedMap.flatten tyenv + processTypeCheck $ checkStmt avail varenv' tyenv' ctx stmt case stmt' of @@ -895,36 +921,32 @@ interpretTopStmt printBinds stmt = do processStmtBind printBinds pos pat expr SS.StmtLet _pos rebindable dg -> - liftTopLevel $ do - env <- interpretDeclGroup rebindable dg - rw' <- getMergedEnv' env - putTopLevelRW rw' + liftTopLevel $ interpretDeclGroup rebindable dg SS.StmtCode _ spos str -> liftTopLevel $ do sc <- getSharedContext - let cenv = rwGetCryptolEnv rw + cenv <- getCryptolEnv --io $ putStrLn $ "Processing toplevel code: " ++ show str --showCryptolEnv cenv' <- io $ CEnv.parseDecls sc cenv $ toInputText spos str - putTopLevelRW $ rwSetCryptolEnv cenv' rw + setCryptolEnv cenv' --showCryptolEnv SS.StmtImport _ imp -> liftTopLevel $ do sc <- getSharedContext - let cenv = rwGetCryptolEnv rw + cenv <- getCryptolEnv --showCryptolEnv let mLoc = iModule imp qual = iAs imp spec = iSpec imp cenv' <- io $ CEnv.importCryptolModule sc cenv mLoc qual CEnv.PublicAndPrivate spec - putTopLevelRW $ rwSetCryptolEnv cenv' rw + setCryptolEnv cenv' --showCryptolEnv SS.StmtTypedef _ _ name ty -> - liftTopLevel $ do - putTopLevelRW $ addTypedef name ty rw + liftTopLevel $ addTypedef name ty -- Hook for AutoMatch stmtInterpreter :: StmtInterpreter @@ -934,7 +956,16 @@ stmtInterpreter ro rw stmts = -- so as to (a) get the right behavior (as long as interpretTopStmt -- and interpretDoStmt are different, which they are) and (b) avoid -- needing to provide a block result value. - fst <$> runTopLevel (withLocalEnv emptyLocal (mapM_ (interpretTopStmt False) stmts)) ro rw + -- + -- XXX what scope should this use? Prior to #2720 it substituted an + -- empty "local environment" for the current "local environment", + -- which would have dropped an ill-specified part of the namespace. + -- That wasn't particularly sensible and probably wasn't correct, + -- but we could reasonably here want either the current environment + -- or a copy of the environment captured when we start AutoMatch, + -- and it's not obvious which. For the moment, we'll use the current + -- environment because that doesn't require any fiddling. + fst <$> runTopLevel (mapM_ (interpretTopStmt False) stmts) ro rw interpretFile :: FilePath -> Bool {- ^ run main? -} -> TopLevel () interpretFile file runMain = @@ -964,9 +995,8 @@ interpretFile file runMain = -- | Evaluate the value called 'main' from the current environment. interpretMain :: TopLevel () interpretMain = do - rw <- getTopLevelRW avail <- gets rwPrimsAvail - tyenv <- gets rwTypeInfo + Environ varenv tyenv _cryenv <- gets rwEnviron let pos = SS.PosInternal "entry" -- We need the type to be "TopLevel a", not just "TopLevel ()". -- There are several (old) tests in the test suite whose main @@ -976,14 +1006,16 @@ interpretMain = do tyRet = SS.TyVar pos "a" tyMonadic = SS.tBlock pos (SS.tContext pos SS.TopLevel) tyRet tyExpected = SS.Forall [(pos, "a")] tyMonadic - case Map.lookup "main" (rwValueInfo rw) of + case ScopedMap.lookup "main" varenv of Nothing -> -- Don't fail or complain if there's no main. return () Just (_defpos, Current, _rebindable, tyFound, v, _doc) -> case tyFound of SS.Forall _ (SS.TyCon _ SS.BlockCon [_, _]) -> + -- XXX shouldn't have to do this + let tyenv' = ScopedMap.flatten tyenv in -- It looks like a monadic value, so check more carefully. - case typesMatch avail tyenv tyFound tyExpected of + case typesMatch avail tyenv' tyFound tyExpected of False -> -- While we accept any TopLevel a, don't encourage people -- to do that. @@ -1058,16 +1090,14 @@ buildTopLevelEnv proxy opts scriptArgv = , biBasicSS = ss } ce0 <- CEnv.initCryptolEnv sc + let cryenv0 = CryptolEnvStack ce0 [] jvmTrans <- CJ.mkInitialJVMContext halloc let rw0 = TopLevelRW - { rwValueInfo = primValueEnv opts bic - , rwTypeInfo = primNamedTypeEnv - , rwCryptol = CryptolEnvStack ce0 [] + { rwEnviron = primEnviron opts bic cryenv0 , rwPosition = SS.Unknown , rwStackTrace = Trace.empty - , rwLocalEnv = [] , rwProofs = [] , rwPPOpts = PPS.defaultOpts , rwSharedContext = sc @@ -1682,14 +1712,12 @@ add_primitives lc _bic _opts = do toplevelSubshell :: () -> TopLevel Value toplevelSubshell () = do m <- roSubshell <$> ask - env <- getLocalEnv - toValue "subshell" <$> withLocalEnv env m + toValue "subshell" <$> m proofScriptSubshell :: () -> ProofScript Value proofScriptSubshell () = do m <- scriptTopLevel $ asks roProofSubshell - env <- scriptTopLevel $ getLocalEnv - toValue "proof_subshell" <$> withLocalEnvProof env m + toValue "proof_subshell" <$> m -- The "for" builtin. -- @@ -2068,7 +2096,7 @@ print_value :: Value -> TopLevel () print_value (VString s) = printOutLnTop Info (Text.unpack s) print_value (VTerm t) = do sc <- getSharedContext - cenv <- getCryptolEnv' + cenv <- getCryptolEnv let cfg = CEnv.meSolverConfig (CEnv.eModuleEnv cenv) unless (null (getAllExts (ttTerm t))) $ fail "term contains symbolic variables" @@ -6448,3 +6476,18 @@ primValueEnv opts bic = Map.mapWithKey extract primitives let pos = SS.PosInternal "<>" in (pos, primitiveLife p, SS.ReadOnlyVar, primitiveType p, (primitiveFn p) opts bic, Just $ doc n p) + +primEnviron :: Options -> BuiltinContext -> CryptolEnvStack -> Environ +primEnviron opts bic cryenvs = + + -- Do a scope push so the builtins live by themselves in their own + -- scope layer. This has the result of separating them from the + -- user's variables in the :env output (which is now grouped by + -- scope) and, because the builtin layer is readonly, might be + -- marginally more efficient as the user's globals are added. + + let tyenv = ScopedMap.push $ ScopedMap.seed primNamedTypeEnv + varenv = ScopedMap.push $ ScopedMap.seed $ primValueEnv opts bic + in + Environ varenv tyenv cryenvs + diff --git a/saw-script/src/SAWScript/REPL/Command.hs b/saw-script/src/SAWScript/REPL/Command.hs index 01aad94c18..284834e6df 100644 --- a/saw-script/src/SAWScript/REPL/Command.hs +++ b/saw-script/src/SAWScript/REPL/Command.hs @@ -33,10 +33,13 @@ module SAWScript.REPL.Command ( --import SAWCore.SharedTerm (SharedContext) +import qualified SAWSupport.ScopedMap as ScopedMap + +import SAWCentral.Position (getPos, Pos) +import SAWCentral.Value (Environ(..)) import SAWScript.REPL.Monad import SAWScript.REPL.Trie -import SAWCentral.Position (getPos, Pos) import SAWScript.Token (Token) import Cryptol.Parser (ParseError()) @@ -45,7 +48,7 @@ import Control.Monad (guard, void) import Data.Char (isSpace,isPunctuation,isSymbol) import Data.Function (on) -import Data.List (intercalate, nub) +import Data.List (intercalate, intersperse, nub) import qualified Data.Text as Text import System.FilePath((), isPathSeparator) import System.Directory(getHomeDirectory,getCurrentDirectory,setCurrentDirectory,doesDirectoryExist) @@ -199,14 +202,15 @@ typeOfCmd str Right expr -> return expr let pos = getPos expr decl = SS.Decl pos (SS.PWild pos Nothing) Nothing expr - rw <- getTopLevelRWForValues + rw <- getTopLevelRW decl' <- do let primsAvail = rwPrimsAvail rw - valueInfo = rwValueInfo rw + Environ varenv tyenv _cryenvs = rwEnviron rw + -- XXX it should not be necessary to do this munging squash (defpos, lc, rb, ty, _val, _doc) = (defpos, lc, rb, ty) - valueInfo' = Map.map squash valueInfo - typeInfo = rwTypeInfo rw - let (errs_or_results, warns) = checkDecl primsAvail valueInfo' typeInfo decl + varenv' = Map.map squash $ ScopedMap.flatten varenv + tyenv' = ScopedMap.flatten tyenv + let (errs_or_results, warns) = checkDecl primsAvail varenv' tyenv' decl let issueWarning (msgpos, msg) = -- XXX the print functions should be what knows how to show positions... putStrLn (show msgpos ++ ": Warning: " ++ msg) @@ -223,7 +227,7 @@ searchCmd str pat <- case SAWScript.Parser.parseSchemaPattern tokens of Left err -> fail (show err) Right pat -> return pat - rw <- getTopLevelRWForValues + rw <- getTopLevelRW -- Always search the entire environment and recognize all type -- names in the user's pattern, regardless of whether @@ -240,19 +244,20 @@ searchCmd str -- for deprecated functions that take Terms. let primsAvail = rwPrimsAvail rw - valueInfo = rwValueInfo rw + -- XXX it should not be necessary to do this munging + Environ varenv tyenv _cryenv = rwEnviron rw squash (pos, lc, rb, ty, _val, _doc) = (pos, lc, rb, ty) - valueInfo' = Map.map squash valueInfo - typeInfo = rwTypeInfo rw - (errs_or_results, warns) = checkSchemaPattern everythingAvailable valueInfo' typeInfo pat + varenv' = Map.map squash $ ScopedMap.flatten varenv + tyenv' = ScopedMap.flatten tyenv + (errs_or_results, warns) = checkSchemaPattern everythingAvailable varenv' tyenv' pat let issueWarning (msgpos, msg) = -- XXX the print functions should be what knows how to show positions... putStrLn (show msgpos ++ ": Warning: " ++ msg) io $ mapM_ issueWarning warns pat' <- either failTypecheck return $ errs_or_results - let search = compileSearchPattern typeInfo pat' + let search = compileSearchPattern tyenv pat' keep (_pos, _lc, _rb, ty) = matchSearchPattern search ty - allMatches = Map.filter keep valueInfo' + allMatches = Map.filter keep varenv' -- Divide the results into visible, experimental-not-visible, -- and deprecated-not-visible. @@ -339,31 +344,52 @@ quitCmd = stop envCmd :: REPL () envCmd = do - rw <- getTopLevelRWForValues - let avail = rwPrimsAvail rw - valueInfo = rwValueInfo rw - keep (_pos, lc, _rb, _ty, _v, _doc) = Set.member lc avail - valueInfo' = Map.filter keep valueInfo - say (x, (_pos, _lc, _rb, ty, _val, _doc)) = - TextIO.putStrLn (x <> " : " <> PPS.pShowText ty) - io $ mapM_ say $ Map.assocs valueInfo' + rw <- getTopLevelRW + let Environ varenv _tyenv _cryenv = rwEnviron rw + avail = rwPrimsAvail rw + say (x, (_pos, _lc, _rb, ty, _v, _doc)) = do + let ty' = PPS.pShowText ty + TextIO.putStrLn (x <> " : " <> ty') + -- Print only the visible objects + keep (_x, (_pos, lc, _rb, _ty, _v, _doc)) = Set.member lc avail + -- Insert a blank line in the output where there's a scope boundary + printScope mItems = case mItems of + Nothing -> TextIO.putStrLn "" + Just items -> mapM_ say $ filter keep items + -- Reverse the list of scopes so the innermost prints last, + -- because that's what people will expect to see. + itemses = reverse $ ScopedMap.scopedAssocs varenv + io $ mapM_ printScope $ intersperse Nothing $ map Just itemses tenvCmd :: REPL () tenvCmd = do - rw <- getTopLevelRWForValues + rw <- getTopLevelRW let avail = rwPrimsAvail rw - typeInfo = rwTypeInfo rw - typeInfo' = Map.filter (\(lc, _ty) -> Set.member lc avail) typeInfo - say (a, (_lc, ty)) = - TextIO.putStrLn (a <> " : " <> PPS.pShowText ty) - io $ mapM_ say $ Map.assocs typeInfo' + Environ _varenv tyenv _cryenv = rwEnviron rw + say (x, (_lc, ty)) = do + let ty' = PPS.pShowText ty + TextIO.putStrLn (x <> " : " <> ty') + -- Print only the visible objects + keep (_x, (lc, _ty)) = Set.member lc avail + -- Insert a blank line in the output where there's a scope boundary + printScope mItems = case mItems of + Nothing -> TextIO.putStrLn "" + Just items -> mapM_ say $ filter keep items + -- Reverse the list of scopes so the innermost prints last, + -- because that's what people will expect to see. + itemses = reverse $ ScopedMap.scopedAssocs tyenv + io $ mapM_ printScope $ intersperse Nothing $ map Just itemses helpCmd :: String -> REPL () helpCmd cmd | null cmd = io (mapM_ putStrLn (genHelp commandList)) | otherwise = - do env <- getTopLevelRW - case Map.lookup (Text.pack cmd) (rwValueInfo env) of + do rw <- getTopLevelRW + -- Note: there's no rebindable builtins and thus no way to + -- attach help text to anything rebindable, so we can ignore + -- the rebindables. + let Environ varenv _tyenv _cryenvs = rwEnviron rw + case ScopedMap.lookup (Text.pack cmd) varenv of Just (_pos, _lc, _rb, _ty, _v, Just doc) -> io $ mapM_ TextIO.putStrLn doc Just (_pos, _lc, _rb, _ty, _v, Nothing) -> do diff --git a/saw-script/src/SAWScript/REPL/Monad.hs b/saw-script/src/SAWScript/REPL/Monad.hs index 8987776617..24b138cd55 100644 --- a/saw-script/src/SAWScript/REPL/Monad.hs +++ b/saw-script/src/SAWScript/REPL/Monad.hs @@ -49,7 +49,6 @@ module SAWScript.REPL.Monad ( -- ** SAWScript stuff , getSharedContext , getTopLevelRO - , getTopLevelRWForValues , getTopLevelRW, modifyTopLevelRW, putTopLevelRW , getTopLevelRWRef , getProofStateRef @@ -85,6 +84,8 @@ import qualified Control.Exception as X import System.IO.Error (isUserError, ioeGetErrorString) import System.Exit (ExitCode) +import qualified SAWSupport.ScopedMap as ScopedMap + import SAWCore.SharedTerm (Term) import CryptolSAWCore.CryptolEnv import qualified Data.AIG as AIG @@ -97,11 +98,8 @@ import SAWCore.SAWCore (SharedContext) import SAWCentral.Options (Options) import SAWCentral.Proof (ProofState, ProofResult(..), psGoals) import SAWCentral.TopLevel (TopLevelRO(..), TopLevelRW(..), TopLevel(..), runTopLevel) -import SAWCentral.Value - ( AIGProxy(..), mergeLocalEnv - , ProofScript(..), showsProofResult - , rwGetCryptolEnv, rwModifyCryptolEnv - ) +import SAWCentral.Value (AIGProxy(..), ProofScript(..), showsProofResult, Environ(..), + rwGetCryptolEnv, rwModifyCryptolEnv) import SAWScript.Interpreter (buildTopLevelEnv) import SAWScript.ValueOps (makeCheckpoint, restoreCheckpoint) @@ -483,11 +481,6 @@ getProofStateRef = rProofState <$> getRefs getTopLevelRW :: REPL TopLevelRW getTopLevelRW = readRef rTopLevelRW -getTopLevelRWForValues :: REPL TopLevelRW -getTopLevelRWForValues = - do rw <- getTopLevelRW - io (mergeLocalEnv (rwSharedContext rw) (rwLocalEnv rw) rw) - putTopLevelRW :: TopLevelRW -> REPL () putTopLevelRW = modifyTopLevelRW . const @@ -497,19 +490,21 @@ modifyTopLevelRW = modifyRef rTopLevelRW -- | Get visible variable names for Haskeline completion. getSAWScriptValueNames :: REPL [String] getSAWScriptValueNames = do - env <- getTopLevelRW - let avail = rwPrimsAvail env + rw <- getTopLevelRW + let avail = rwPrimsAvail rw visible (_, lc, _, _, _, _) = Set.member lc avail - let rnames = Map.keys $ Map.filter visible $ rwValueInfo env + Environ valenv _tyenv _cryenv = rwEnviron rw + let rnames = ScopedMap.allKeys $ ScopedMap.filter visible valenv return (map Text.unpack rnames) -- | Get visible type names for Haskeline completion. getSAWScriptTypeNames :: REPL [String] getSAWScriptTypeNames = do - env <- getTopLevelRW - let avail = rwPrimsAvail env + rw <- getTopLevelRW + let avail = rwPrimsAvail rw visible (lc, _) = Set.member lc avail - let rnames = Map.keys $ Map.filter visible $ rwTypeInfo env + Environ _valenv tyenv _cryenv = rwEnviron rw + let rnames = ScopedMap.allKeys $ ScopedMap.filter visible tyenv return (map Text.unpack rnames) -- User Environment Interaction ------------------------------------------------ diff --git a/saw-script/src/SAWScript/Search.hs b/saw-script/src/SAWScript/Search.hs index 9bc3b771cf..42b8990bd1 100644 --- a/saw-script/src/SAWScript/Search.hs +++ b/saw-script/src/SAWScript/Search.hs @@ -22,8 +22,10 @@ import qualified Data.Map as Map import Data.Set (Set) import qualified Data.Set as Set +import qualified SAWSupport.ScopedMap as ScopedMap import SAWCentral.AST import SAWCentral.ASTUtil (namedTyVars) +import SAWCentral.Value (TyEnv) import SAWScript.Panic (panic) -- @@ -472,17 +474,6 @@ matchFragList ctx cand0 tgtType patTypes = ------------------------------------------------------------ -- External interface {{{ --- short name for the environment type we use --- --- Let this be polymorphic in the things it carries because all we --- need from it is the keys. --- --- (XXX: this type really belongs to the interpreter and should really --- be in its public interface or shared from somewhere else, but that --- requires the interpreter to have an interface, which requires --- still-pending interpreter cleanup) -type TyEnv a = Map Name a - -- | Check and compile a type schema pattern. -- -- We get passed a list of forall bindings (will often be empty) @@ -493,10 +484,10 @@ type TyEnv a = Map Name a -- different match semantics from forall-bound type variables. See -- notes at the top of the file. -- -compileSearchPattern :: TyEnv a -> SchemaPattern -> SearchPattern +compileSearchPattern :: TyEnv -> SchemaPattern -> SearchPattern compileSearchPattern tyEnv (SchemaPattern forallList tys) = let foralls = Set.fromList $ map (\(_pos, name) -> name) forallList - boundVars = Map.keysSet tyEnv + boundVars = ScopedMap.allKeysSet tyEnv -- treat '_' as a bound var to avoid assorted confusion boundVars' = Set.insert "_" boundVars oneType ty freeVarsSoFar = diff --git a/saw-script/src/SAWScript/Typechecker.hs b/saw-script/src/SAWScript/Typechecker.hs index 4a79eba017..e068712e6a 100644 --- a/saw-script/src/SAWScript/Typechecker.hs +++ b/saw-script/src/SAWScript/Typechecker.hs @@ -41,7 +41,7 @@ import SAWSupport.Pretty (pShow) import qualified SAWSupport.Pretty as PPS import SAWCentral.AST -import SAWCentral.ASTUtil (namedTyVars, SubstituteTyVars(..), isDeprecated) +import SAWCentral.ASTUtil (namedTyVars, SubstituteTyVars'(..), isDeprecated) import SAWScript.Panic (panic) import SAWCentral.Position (Inference(..), Pos(..), Positioned(..), choosePos) @@ -416,11 +416,11 @@ applyCurrentSubst t = do -- -- The type t has already been checked, so it's ok to panic if it refers -- to something in the typedef collection that's not visible. -resolveCurrentTypedefs :: SubstituteTyVars t => t -> TI t +resolveCurrentTypedefs :: SubstituteTyVars' t => t -> TI t resolveCurrentTypedefs t = do avail <- asks primsAvail s <- gets tyEnv - return $ substituteTyVars avail s t + return $ substituteTyVars' avail s t -- Get the unification vars that are used in the current variable typing -- and named type environments. @@ -1156,7 +1156,7 @@ inferExpr (ln, expr) = case expr of at <- getFreshTyVar apos return (a, (Current, ConcreteType at)) substs <- mapM once as - let t' = substituteTyVars avail (M.fromList substs) t + let t' = substituteTyVars' avail (M.fromList substs) t return (Var pos x, t') | otherwise -> do recordError pos $ "Inaccessible variable: " ++ show x ++ " (" ++ show pos ++ ")" @@ -1307,7 +1307,7 @@ addTypedef :: Name -> Type -> TI () addTypedef a ty = do avail <- asks primsAvail env <- gets tyEnv - let ty' = substituteTyVars avail env ty + let ty' = substituteTyVars' avail env ty env' = M.insert a (Current, ConcreteType ty') env modify (\rw -> rw { tyEnv = env' }) @@ -1997,7 +1997,7 @@ typesMatch avail tenv schema'found schema'expected = return (a, (Current, ConcreteType ty'a)) substs <- mapM generate as -- Substitute them into the type - let ty' = substituteTyVars avail (M.fromList substs) ty + let ty' = substituteTyVars' avail (M.fromList substs) ty return ty' match = do -- Unpack the schemas and check if they match diff --git a/saw-script/src/SAWScript/ValueOps.hs b/saw-script/src/SAWScript/ValueOps.hs index 4439a35e43..9e96a9f857 100644 --- a/saw-script/src/SAWScript/ValueOps.hs +++ b/saw-script/src/SAWScript/ValueOps.hs @@ -22,10 +22,6 @@ module SAWScript.ValueOps ( -- used by SAWScript.Interpreter tupleLookupValue, -- used by SAWScript.Interpreter - emptyLocal, - -- used by SAWScript.Interpreter - extendLocal, - -- used by SAWScript.Interpreter bracketTopLevel, -- unused but that probably won't stay that way TopLevelCheckpoint(..), @@ -38,11 +34,11 @@ module SAWScript.ValueOps ( -- used by SAWScript.Interpreter proof_checkpoint, -- used by SAWScript.Interpreter - withLocalEnv, - withLocalEnvProof, - withLocalEnvLLVM, - withLocalEnvJVM, - withLocalEnvMIR, + withEnviron, + withEnvironProofScript, + withEnvironLLVM, + withEnvironJVM, + withEnvironMIR, -- used in SAWScript.Interpreter withOptions, ) where @@ -67,7 +63,7 @@ import SAWCore.SharedTerm import CryptolSAWCore.CryptolEnv as CEnv import qualified SAWCentral.Position as SS -import qualified SAWCentral.AST as SS +--import qualified SAWCentral.AST as SS --import qualified SAWCentral.Crucible.JVM.MethodSpecIR () --import qualified SAWCentral.Crucible.MIR.MethodSpecIR () import SAWCentral.Options (Options, Verbosity(..)) @@ -119,12 +115,6 @@ tupleLookupValue pos v1 v2 = "Index value: " <> Text.pack (show v2) ] -emptyLocal :: LocalEnv -emptyLocal = [] - -extendLocal :: SS.Pos -> SS.Name -> SS.Rebindable -> SS.Schema -> Maybe [Text] -> Value -> LocalEnv -> LocalEnv -extendLocal pos x rb ty md v env = LocalLet pos x rb ty md v : env - -- | A version of 'Control.Exception.bracket' specialized to 'TopLevel'. We -- can't use 'Control.Monad.Catch.bracket' because it requires 'TopLevel' to -- implement 'Control.Monad.Catch.MonadMask', which it can't do. @@ -192,29 +182,29 @@ proof_checkpoint = do scriptTopLevel (printOutLnTop Info "Restoring proof state from checkpoint") put ps -withLocalEnv :: LocalEnv -> TopLevel a -> TopLevel a -withLocalEnv env m = do - prevEnv <- gets rwLocalEnv - modify (\rw -> rw { rwLocalEnv = env }) +withEnviron :: Environ -> TopLevel a -> TopLevel a +withEnviron env m = do + prevEnv <- gets rwEnviron + modify (\rw -> rw { rwEnviron = env }) result <- m - modify (\rw -> rw { rwLocalEnv = prevEnv }) + modify (\rw -> rw { rwEnviron = prevEnv }) return result -withLocalEnvProof :: LocalEnv -> ProofScript a -> ProofScript a -withLocalEnvProof env (ProofScript m) = do - ProofScript (underExceptT (underStateT (withLocalEnv env)) m) +withEnvironProofScript :: Environ -> ProofScript a -> ProofScript a +withEnvironProofScript env (ProofScript m) = do + ProofScript (underExceptT (underStateT (withEnviron env)) m) -withLocalEnvLLVM :: LocalEnv -> LLVMCrucibleSetupM a -> LLVMCrucibleSetupM a -withLocalEnvLLVM env (LLVMCrucibleSetupM m) = do - LLVMCrucibleSetupM (underReaderT (underStateT (withLocalEnv env)) m) +withEnvironLLVM :: Environ -> LLVMCrucibleSetupM a -> LLVMCrucibleSetupM a +withEnvironLLVM env (LLVMCrucibleSetupM m) = do + LLVMCrucibleSetupM (underReaderT (underStateT (withEnviron env)) m) -withLocalEnvJVM :: LocalEnv -> JVMSetupM a -> JVMSetupM a -withLocalEnvJVM env (JVMSetupM m) = do - JVMSetupM (underReaderT (underStateT (withLocalEnv env)) m) +withEnvironJVM :: Environ -> JVMSetupM a -> JVMSetupM a +withEnvironJVM env (JVMSetupM m) = do + JVMSetupM (underReaderT (underStateT (withEnviron env)) m) -withLocalEnvMIR :: LocalEnv -> MIRSetupM a -> MIRSetupM a -withLocalEnvMIR env (MIRSetupM m) = do - MIRSetupM (underReaderT (underStateT (withLocalEnv env)) m) +withEnvironMIR :: Environ -> MIRSetupM a -> MIRSetupM a +withEnvironMIR env (MIRSetupM m) = do + MIRSetupM (underReaderT (underStateT (withEnviron env)) m) withOptions :: (Options -> Options) -> TopLevel a -> TopLevel a withOptions f (TopLevel_ m) = diff --git a/saw-server/src/SAWServer/SAWServer.hs b/saw-server/src/SAWServer/SAWServer.hs index 527b01cdfe..2bf702e103 100644 --- a/saw-server/src/SAWServer/SAWServer.hs +++ b/saw-server/src/SAWServer/SAWServer.hs @@ -44,6 +44,7 @@ import Mir.Generator (RustModule) import Mir.Intrinsics (MIR) import Mir.Mir (Adt) +import qualified SAWSupport.ScopedMap as ScopedMap import qualified SAWSupport.Pretty as PPS (defaultOpts) import qualified SAWCentral.Trace as Trace (empty) @@ -63,7 +64,7 @@ import SAWCentral.Options (processEnv, defaultOptions) import SAWCentral.Position (Pos(..)) import SAWCentral.Prover.Rewrite (basic_ss) import SAWCentral.Proof (emptyTheoremDB) -import SAWCentral.Value (AIGProxy(..), BuiltinContext(..), JVMSetupM, LLVMCrucibleSetupM, TopLevelRO(..), TopLevelRW(..), SAWSimpset, JavaCodebase(..), CryptolEnvStack(..), rwModifyCryptolEnv) +import SAWCentral.Value (AIGProxy(..), BuiltinContext(..), JVMSetupM, LLVMCrucibleSetupM, Environ(..), TopLevelRO(..), TopLevelRW(..), SAWSimpset, JavaCodebase(..), CryptolEnvStack(..), rwModifyCryptolEnv) import SAWCentral.Yosys.State (YosysSequential) import SAWCentral.Yosys.Theorem (YosysImport, YosysTheorem) import qualified CryptolSAWCore.Prelude as CryptolSAW @@ -222,6 +223,7 @@ initialState readFileFn = , biBasicSS = ss } cenv <- initCryptolEnv sc + let cryenvs = CryptolEnvStack cenv [] halloc <- Crucible.newHandleAllocator jvmTrans <- CJ.mkInitialJVMContext halloc cwd <- getCurrentDirectory @@ -243,12 +245,9 @@ initialState readFileFn = , roProofSubshell = fail "SAW server does not support subshells." } rw = TopLevelRW - { rwValueInfo = mempty - , rwTypeInfo = mempty - , rwCryptol = CryptolEnvStack cenv [] + { rwEnviron = Environ ScopedMap.empty ScopedMap.empty cryenvs , rwPosition = PosInternal "SAWServer" , rwStackTrace = Trace.empty - , rwLocalEnv = [] , rwPPOpts = PPS.defaultOpts , rwSolverCache = mb_cache , rwTheoremDB = emptyTheoremDB From 190d5639300b503989ee8e24598d8cc83ad68278 Mon Sep 17 00:00:00 2001 From: David Holland Date: Wed, 15 Oct 2025 01:20:55 -0400 Subject: [PATCH 11/13] SAWScript: Add an extra global environment for "let rebindable". This makes the new "let rebindable" functionality work, fixing the test05 and test14 cases of test1646, and finally closes #1646. --- intTests/test1646/test05.log.good | 2 +- intTests/test1646/test05.saw | 1 - intTests/test1646/test14.log.good | 8 +-- intTests/test1646/test14.saw | 1 - intTests/test1646/test15.log.good | 4 +- saw-central/src/SAWCentral/Builtins.hs | 15 +++++- saw-central/src/SAWCentral/Value.hs | 50 ++++++++++++++--- saw-script/src/SAWScript/Interpreter.hs | 69 ++++++++++++++++-------- saw-script/src/SAWScript/REPL/Command.hs | 41 ++++++++++---- saw-script/src/SAWScript/REPL/Monad.hs | 8 +-- saw-server/src/SAWServer/SAWServer.hs | 1 + 11 files changed, 147 insertions(+), 53 deletions(-) diff --git a/intTests/test1646/test05.log.good b/intTests/test1646/test05.log.good index dc0af5ac42..607fa10161 100644 --- a/intTests/test1646/test05.log.good +++ b/intTests/test1646/test05.log.good @@ -1,3 +1,3 @@ Loading file "test05.saw" x=a - x=a + x=b diff --git a/intTests/test1646/test05.saw b/intTests/test1646/test05.saw index cf75ee6986..f2542281b8 100644 --- a/intTests/test1646/test05.saw +++ b/intTests/test1646/test05.saw @@ -1,5 +1,4 @@ // The second f call will print x=b. -// XXX currently it prints x=a let rebindable x = "a"; diff --git a/intTests/test1646/test14.log.good b/intTests/test1646/test14.log.good index d793bbc2d3..c48add3cb8 100644 --- a/intTests/test1646/test14.log.good +++ b/intTests/test1646/test14.log.good @@ -1,6 +1,6 @@ Loading file "test14.saw" x=a - x=a - test14.saw:12:5-12:6: Warning: Redeclaration of x - test14.saw:9:16-9:17: Warning: Previous declaration was here - x=a + x=b + test14.saw:11:5-11:6: Warning: Redeclaration of x + test14.saw:8:16-8:17: Warning: Previous declaration was here + x=b diff --git a/intTests/test1646/test14.saw b/intTests/test1646/test14.saw index a360cc6bbc..ccfbb96743 100644 --- a/intTests/test1646/test14.saw +++ b/intTests/test1646/test14.saw @@ -1,5 +1,4 @@ // The second f call should print x=b. So should the third. -// XXX: currently all print x=a. let rebindable x = "a"; diff --git a/intTests/test1646/test15.log.good b/intTests/test1646/test15.log.good index 1df25e0e21..2d10dee2f4 100644 --- a/intTests/test1646/test15.log.good +++ b/intTests/test1646/test15.log.good @@ -1,5 +1,8 @@ :1:5-1:6: Warning: Redeclaration of y :1:16-1:17: Warning: Previous declaration was here +x : rebindable Int +y : rebindable Int + abc : ProofScript () abstract_symbolic : Term -> Term add_cryptol_defs : [String] -> Simpset -> Simpset @@ -345,5 +348,4 @@ write_smtlib2_w4 : String -> Term -> TopLevel () yices : ProofScript () z3 : ProofScript () -x : Int y : Int diff --git a/saw-central/src/SAWCentral/Builtins.hs b/saw-central/src/SAWCentral/Builtins.hs index cfa4ed7389..ddf33518a7 100644 --- a/saw-central/src/SAWCentral/Builtins.hs +++ b/saw-central/src/SAWCentral/Builtins.hs @@ -1705,10 +1705,21 @@ envCmd = do opts <- getOptions avail <- gets rwPrimsAvail SV.Environ varenv _tyenv _cryenv <- gets rwEnviron - let printItem (x, (_pos, _lc, _rb, ty, _v, _doc)) = + rbenv <- gets rwRebindables + + -- print rebindables first if there are any + unless (Map.null rbenv) $ do + io $ printOutLn opts Info $ "Rebindable globals:" + io $ printOutLn opts Info $ "" + let printRB (x, (_pos, ty, _v)) = do + let str = x <> " : rebindable " <> PPS.pShowText ty + printOutLn opts Info $ Text.unpack str + io $ mapM_ printRB $ Map.assocs rbenv + + let printItem (x, (_pos, _lc, ty, _v, _doc)) = printOutLn opts Info $ Text.unpack (x <> " : " <> PPS.pShowText ty) -- Print only the visible objects - keep (_x, (_pos, lc, _rb, _ty, _v, _doc)) = Set.member lc avail + keep (_x, (_pos, lc, _ty, _v, _doc)) = Set.member lc avail -- Insert a blank line in the output where there's a scope boundary printScope mItems = case mItems of Nothing -> printOutLn opts Info "" diff --git a/saw-central/src/SAWCentral/Value.hs b/saw-central/src/SAWCentral/Value.hs index 290a913bc8..ad63d94458 100644 --- a/saw-central/src/SAWCentral/Value.hs +++ b/saw-central/src/SAWCentral/Value.hs @@ -759,11 +759,10 @@ evaluateTypedTerm _sc (TypedTerm tp _) = -- | The variable environment: a map from variable names to: -- - the definition position -- - the lifecycle setting (experimental/current/deprecated/etc) --- - whether the binding is rebindable -- - the type scheme -- - the value -- - the help text if any -type VarEnv = ScopedMap SS.Name (SS.Pos, SS.PrimitiveLifecycle, SS.Rebindable, +type VarEnv = ScopedMap SS.Name (SS.Pos, SS.PrimitiveLifecycle, SS.Schema, Value, Maybe [Text]) -- | The type environment: a map from type names to: @@ -785,12 +784,23 @@ data CryptolEnvStack = CryptolEnvStack CEnv.CryptolEnv [CEnv.CryptolEnv] -- one that maps type names to types. A third handles the Cryptol -- domain. All three get closed in with lambdas and do-blocks at the -- appropriate times. +-- +-- Note that rebindable variables are sold separately. This is so +-- they don't get closed in; references to rebindable variables +-- always retrieve the most recent version. data Environ = Environ { eVarEnv :: VarEnv, eTyEnv :: TyEnv, eCryptol :: CryptolEnvStack } +-- | The extra environment for rebindable globals. +-- +-- Note: because no builtins are rebindable, there are no lifecycle +-- or help text fields. There is, currently at least, no way to +-- populate those for non-builtins. +type RebindableEnv = Map SS.Name (SS.Pos, SS.Schema, Value) + -- | Enter a scope. pushScope :: TopLevel () pushScope = do @@ -952,6 +962,7 @@ data TopLevelRW = { -- | The variable and type naming environment. rwEnviron :: Environ + , rwRebindables :: RebindableEnv -- | The current execution position. This is only valid when the -- interpreter is calling out into saw-central to execute a @@ -1270,7 +1281,22 @@ extendEnv pos name rb ty doc v = do -- Update the SAWScript environment. Environ varenv tyenv cryenvs <- gets rwEnviron - let varenv' = ScopedMap.insert name (pos, SS.Current, rb, ty, v, doc) varenv + rbenv <- gets rwRebindables + let (varenv', rbenv') = case rb of + SS.ReadOnlyVar -> + -- If we replace a rebindable variable at the top level with a + -- readonly one, the readonly version in varenv will hide it + -- ever after. We ought to remove it from rbenv; however, it's + -- not easy to know here whether we're at the top level or not. + -- FUTURE: maybe this will become easier in the long run. + let ve' = ScopedMap.insert name (pos, SS.Current, ty, v, doc) varenv in + (ve', rbenv) + SS.RebindableVar -> + -- The typechecker restricts this to happen only at the + -- top level and only if any existing variable is already + -- rebindable, so we don't have to update varenv. + let re' = M.insert name (pos, ty, v) rbenv in + (varenv, re') -- Mirror the value into the Cryptol environment if appropriate. let CryptolEnvStack ce ces = cryenvs @@ -1295,7 +1321,10 @@ extendEnv pos name rb ty doc v = do let cryenvs' = CryptolEnvStack ce' ces -- Drop the new bits into place. - modify (\rw -> rw { rwEnviron = Environ varenv' tyenv cryenvs' }) + modify (\rw -> rw { + rwEnviron = Environ varenv' tyenv cryenvs', + rwRebindables = rbenv' + }) extendEnvMulti :: [(SS.Pos, SS.Name, SS.Rebindable, SS.Schema, Maybe [Text], Environ -> Value)] -> TopLevel () extendEnvMulti bindings = do @@ -1320,10 +1349,19 @@ extendEnvMulti bindings = do VLambda{} -> v _ -> panic "extendEnvMulti" [ - "Non-lambda value: " <> Text.pack (show v) + "Non-lambda value: " <> Text.pack (show v), + "Source position: " <> Text.pack (show pos) + ] + v'' = case rb of + SS.ReadOnlyVar -> v' + SS.RebindableVar -> + -- "rec" declarations can't be rebindable + panic "extendEnvMulti" [ + "Rebindable variable: " <> name, + "Source position: " <> Text.pack (show pos) ] in - ScopedMap.insert name (pos, SS.Current, rb, ty, v', doc) tmpenv + ScopedMap.insert name (pos, SS.Current, ty, v'', doc) tmpenv varenv' = foldr insert varenv bindings environ' = Environ varenv' tyenv cryenv diff --git a/saw-script/src/SAWScript/Interpreter.hs b/saw-script/src/SAWScript/Interpreter.hs index 5a986fbcf4..f5a35f31ef 100644 --- a/saw-script/src/SAWScript/Interpreter.hs +++ b/saw-script/src/SAWScript/Interpreter.hs @@ -509,22 +509,30 @@ interpretExpr expr = SS.Var pos x -> do avail <- gets rwPrimsAvail Environ varenv _tyenv _cryenv <- gets rwEnviron - case ScopedMap.lookup x varenv of - Nothing -> - -- This should be rejected by the typechecker, so panic - panic "interpretExpr" [ - "Read of unknown variable " <> x - ] - Just (_defpos, lc, _rebindable, _ty, v, _doc) - | Set.member lc avail -> do - let v' = injectPositionIntoMonadicValue pos v - v'' = insertRefChain pos x v' - return v'' - | otherwise -> - -- This case is also rejected by the typechecker - panic "interpretExpr" [ - "Read of inaccessible variable " <> x - ] + rbenv <- gets rwRebindables + let info = case ScopedMap.lookup x varenv of + Nothing -> + -- Try the rebindable environment + case Map.lookup x rbenv of + Nothing -> Nothing + Just (_defpos, _ty, v) -> Just (Current, v) + Just (_defpos, lc, _ty, v, _doc) -> Just (lc, v) + case info of + Nothing -> + -- This should be rejected by the typechecker; panic + panic "interpretExpr" [ + "Read of unknown variable " <> x + ] + Just (lc, v) + | Set.member lc avail -> do + let v' = injectPositionIntoMonadicValue pos v + v'' = insertRefChain pos x v' + return v'' + | otherwise -> + -- This case is also rejected by the typechecker + panic "interpretExpr" [ + "Read of inaccessible variable " <> x + ] SS.Lambda _pos mname pat e -> do env <- gets rwEnviron return $ VLambda env mname pat e @@ -908,9 +916,14 @@ interpretTopStmt printBinds stmt = do -- - shouldn't have to flatten the environments -- - shouldn't be typechecking one statement at a time regardless Environ varenv tyenv _cryenvs <- liftTopLevel $ gets rwEnviron - let varenv' = Map.map (\(pos, lc, rb, ty, _v, _doc) -> (pos, lc, rb, ty)) $ ScopedMap.flatten varenv + rbenv <- liftTopLevel $ gets rwRebindables + let varenv' = Map.map (\(pos, lc, ty, _v, _doc) -> (pos, lc, SS.ReadOnlyVar, ty)) $ ScopedMap.flatten varenv + rbenv' = Map.map (\(pos, ty, _v) -> (pos, SS.Current, SS.RebindableVar, ty)) rbenv + -- If anything appears in both, favor the real environment + varenv'' = Map.union varenv' rbenv' + let tyenv' = ScopedMap.flatten tyenv - processTypeCheck $ checkStmt avail varenv' tyenv' ctx stmt + processTypeCheck $ checkStmt avail varenv'' tyenv' ctx stmt case stmt' of @@ -997,6 +1010,7 @@ interpretMain :: TopLevel () interpretMain = do avail <- gets rwPrimsAvail Environ varenv tyenv _cryenv <- gets rwEnviron + rbenv <- gets rwRebindables let pos = SS.PosInternal "entry" -- We need the type to be "TopLevel a", not just "TopLevel ()". -- There are several (old) tests in the test suite whose main @@ -1006,11 +1020,19 @@ interpretMain = do tyRet = SS.TyVar pos "a" tyMonadic = SS.tBlock pos (SS.tContext pos SS.TopLevel) tyRet tyExpected = SS.Forall [(pos, "a")] tyMonadic - case ScopedMap.lookup "main" varenv of + let main = case ScopedMap.lookup "main" varenv of + Just (_defpos, lc, tyFound, v, _doc) -> Just (lc, tyFound, v) + -- Having main be rebindable doesn't make much sense, but + -- it's easier to have this code than to spend time + -- explaining that it's not allowed. + Nothing -> case Map.lookup "main" rbenv of + Nothing -> Nothing + Just (_defpos, tyFound, v) -> Just (Current, tyFound, v) + case main of Nothing -> -- Don't fail or complain if there's no main. return () - Just (_defpos, Current, _rebindable, tyFound, v, _doc) -> case tyFound of + Just (Current, tyFound, v) -> case tyFound of SS.Forall _ (SS.TyCon _ SS.BlockCon [_, _]) -> -- XXX shouldn't have to do this let tyenv' = ScopedMap.flatten tyenv in @@ -1028,7 +1050,7 @@ interpretMain = do -- If the type is something entirely random, like a Term or a -- String or something, just ignore it. return () - Just (_defpos, lc, _rebindable, _ty, _v, _doc) -> + Just (lc, _ty, _v) -> -- There is no way for things other than primitives to get marked -- experimental or deprecated, so this isn't possible. If we allow -- users to deprecate their own functions in the future, change @@ -1096,6 +1118,7 @@ buildTopLevelEnv proxy opts scriptArgv = let rw0 = TopLevelRW { rwEnviron = primEnviron opts bic cryenv0 + , rwRebindables = Map.empty , rwPosition = SS.Unknown , rwStackTrace = Trace.empty , rwProofs = [] @@ -6453,7 +6476,7 @@ primNamedTypeEnv = fmap extract primTypes primValueEnv :: Options -> BuiltinContext -> - Map SS.Name (SS.Pos, PrimitiveLifecycle, SS.Rebindable, SS.Schema, Value, Maybe [Text]) + Map SS.Name (SS.Pos, PrimitiveLifecycle, SS.Schema, Value, Maybe [Text]) primValueEnv opts bic = Map.mapWithKey extract primitives where header = [ @@ -6474,7 +6497,7 @@ primValueEnv opts bic = Map.mapWithKey extract primitives header <> tag p <> name n p <> primitiveDoc p extract n p = let pos = SS.PosInternal "<>" in - (pos, primitiveLife p, SS.ReadOnlyVar, primitiveType p, + (pos, primitiveLife p, primitiveType p, (primitiveFn p) opts bic, Just $ doc n p) primEnviron :: Options -> BuiltinContext -> CryptolEnvStack -> Environ diff --git a/saw-script/src/SAWScript/REPL/Command.hs b/saw-script/src/SAWScript/REPL/Command.hs index 284834e6df..bcb0504df9 100644 --- a/saw-script/src/SAWScript/REPL/Command.hs +++ b/saw-script/src/SAWScript/REPL/Command.hs @@ -44,7 +44,7 @@ import SAWScript.Token (Token) import Cryptol.Parser (ParseError()) -import Control.Monad (guard, void) +import Control.Monad (guard, unless, void) import Data.Char (isSpace,isPunctuation,isSymbol) import Data.Function (on) @@ -77,7 +77,7 @@ import SAWScript.Interpreter (interpretTopStmt) import qualified SAWScript.Lexer (lexSAW) import qualified SAWScript.Parser (parseStmtSemi, parseExpression, parseSchemaPattern) import SAWCentral.TopLevel (TopLevelRW(..)) -import SAWCentral.AST (PrimitiveLifecycle(..), everythingAvailable) +import SAWCentral.AST (PrimitiveLifecycle(..), everythingAvailable, Rebindable(..)) -- Commands -------------------------------------------------------------------- @@ -205,12 +205,16 @@ typeOfCmd str rw <- getTopLevelRW decl' <- do let primsAvail = rwPrimsAvail rw - Environ varenv tyenv _cryenvs = rwEnviron rw -- XXX it should not be necessary to do this munging - squash (defpos, lc, rb, ty, _val, _doc) = (defpos, lc, rb, ty) + Environ varenv tyenv _cryenvs = rwEnviron rw + squash (defpos, lc, ty, _val, _doc) = (defpos, lc, ReadOnlyVar, ty) varenv' = Map.map squash $ ScopedMap.flatten varenv tyenv' = ScopedMap.flatten tyenv - let (errs_or_results, warns) = checkDecl primsAvail varenv' tyenv' decl + rbenv = rwRebindables rw + rbsquash (defpos, ty, _val) = (defpos, Current, RebindableVar, ty) + rbenv' = Map.map rbsquash rbenv + varenv'' = Map.union varenv' rbenv' + let (errs_or_results, warns) = checkDecl primsAvail varenv'' tyenv' decl let issueWarning (msgpos, msg) = -- XXX the print functions should be what knows how to show positions... putStrLn (show msgpos ++ ": Warning: " ++ msg) @@ -246,10 +250,14 @@ searchCmd str let primsAvail = rwPrimsAvail rw -- XXX it should not be necessary to do this munging Environ varenv tyenv _cryenv = rwEnviron rw - squash (pos, lc, rb, ty, _val, _doc) = (pos, lc, rb, ty) + rbenv = rwRebindables rw + squash (pos, lc, ty, _val, _doc) = (pos, lc, ReadOnlyVar, ty) varenv' = Map.map squash $ ScopedMap.flatten varenv tyenv' = ScopedMap.flatten tyenv - (errs_or_results, warns) = checkSchemaPattern everythingAvailable varenv' tyenv' pat + rbsquash (pos, ty, _val) = (pos, Current, RebindableVar, ty) + rbenv' = Map.map rbsquash rbenv + varenv'' = Map.union varenv' rbenv' + (errs_or_results, warns) = checkSchemaPattern everythingAvailable varenv'' tyenv' pat let issueWarning (msgpos, msg) = -- XXX the print functions should be what knows how to show positions... putStrLn (show msgpos ++ ": Warning: " ++ msg) @@ -346,12 +354,23 @@ envCmd :: REPL () envCmd = do rw <- getTopLevelRW let Environ varenv _tyenv _cryenv = rwEnviron rw + rbenv = rwRebindables rw avail = rwPrimsAvail rw - say (x, (_pos, _lc, _rb, ty, _v, _doc)) = do + + -- print the rebindable globals first, if any + unless (Map.null rbenv) $ do + let rbsay (x, (_pos, ty, _v)) = do + let ty' = PPS.pShowText ty + TextIO.putStrLn (x <> " : rebindable " <> ty') + io $ mapM_ rbsay $ Map.assocs rbenv + io $ TextIO.putStrLn "" + + -- print the normal environment + let say (x, (_pos, _lc, ty, _v, _doc)) = do let ty' = PPS.pShowText ty TextIO.putStrLn (x <> " : " <> ty') -- Print only the visible objects - keep (_x, (_pos, lc, _rb, _ty, _v, _doc)) = Set.member lc avail + keep (_x, (_pos, lc, _ty, _v, _doc)) = Set.member lc avail -- Insert a blank line in the output where there's a scope boundary printScope mItems = case mItems of Nothing -> TextIO.putStrLn "" @@ -390,9 +409,9 @@ helpCmd cmd -- the rebindables. let Environ varenv _tyenv _cryenvs = rwEnviron rw case ScopedMap.lookup (Text.pack cmd) varenv of - Just (_pos, _lc, _rb, _ty, _v, Just doc) -> + Just (_pos, _lc, _ty, _v, Just doc) -> io $ mapM_ TextIO.putStrLn doc - Just (_pos, _lc, _rb, _ty, _v, Nothing) -> do + Just (_pos, _lc, _ty, _v, Nothing) -> do io $ putStrLn $ "// No documentation is available." typeOfCmd cmd Nothing -> diff --git a/saw-script/src/SAWScript/REPL/Monad.hs b/saw-script/src/SAWScript/REPL/Monad.hs index 24b138cd55..300d019e83 100644 --- a/saw-script/src/SAWScript/REPL/Monad.hs +++ b/saw-script/src/SAWScript/REPL/Monad.hs @@ -492,10 +492,12 @@ getSAWScriptValueNames :: REPL [String] getSAWScriptValueNames = do rw <- getTopLevelRW let avail = rwPrimsAvail rw - visible (_, lc, _, _, _, _) = Set.member lc avail + visible (_, lc, _, _, _) = Set.member lc avail Environ valenv _tyenv _cryenv = rwEnviron rw - let rnames = ScopedMap.allKeys $ ScopedMap.filter visible valenv - return (map Text.unpack rnames) + rbenv = rwRebindables rw + let rnames1 = ScopedMap.allKeys $ ScopedMap.filter visible valenv + rnames2 = Map.keys rbenv + return (map Text.unpack (rnames1 ++ rnames2)) -- | Get visible type names for Haskeline completion. getSAWScriptTypeNames :: REPL [String] diff --git a/saw-server/src/SAWServer/SAWServer.hs b/saw-server/src/SAWServer/SAWServer.hs index 2bf702e103..f5325c77ab 100644 --- a/saw-server/src/SAWServer/SAWServer.hs +++ b/saw-server/src/SAWServer/SAWServer.hs @@ -246,6 +246,7 @@ initialState readFileFn = } rw = TopLevelRW { rwEnviron = Environ ScopedMap.empty ScopedMap.empty cryenvs + , rwRebindables = M.empty , rwPosition = PosInternal "SAWServer" , rwStackTrace = Trace.empty , rwPPOpts = PPS.defaultOpts From c9b1540bf51189dfcb2ce7adedc781ea8af37f15 Mon Sep 17 00:00:00 2001 From: David Holland Date: Tue, 21 Oct 2025 23:46:43 -0400 Subject: [PATCH 12/13] Add tests for the subshell naming shenanigans in #2242 and #2243. --- intTests/test2242_2243/README | 9 +++++++++ intTests/test2242_2243/leak01.saw | 10 ++++++++++ intTests/test2242_2243/leak01.stdin | 1 + intTests/test2242_2243/leak02.saw | 11 +++++++++++ intTests/test2242_2243/leak02.stdin | 2 ++ intTests/test2242_2243/leak03.saw | 20 ++++++++++++++++++++ intTests/test2242_2243/leak03.stdin | 2 ++ intTests/test2242_2243/present01.saw | 13 +++++++++++++ intTests/test2242_2243/present01.stdin | 1 + intTests/test2242_2243/present02.saw | 16 ++++++++++++++++ intTests/test2242_2243/present02.stdin | 1 + intTests/test2242_2243/test.sh | 8 ++++++++ 12 files changed, 94 insertions(+) create mode 100644 intTests/test2242_2243/README create mode 100644 intTests/test2242_2243/leak01.saw create mode 100644 intTests/test2242_2243/leak01.stdin create mode 100644 intTests/test2242_2243/leak02.saw create mode 100644 intTests/test2242_2243/leak02.stdin create mode 100644 intTests/test2242_2243/leak03.saw create mode 100644 intTests/test2242_2243/leak03.stdin create mode 100644 intTests/test2242_2243/present01.saw create mode 100644 intTests/test2242_2243/present01.stdin create mode 100644 intTests/test2242_2243/present02.saw create mode 100644 intTests/test2242_2243/present02.stdin create mode 100644 intTests/test2242_2243/test.sh diff --git a/intTests/test2242_2243/README b/intTests/test2242_2243/README new file mode 100644 index 0000000000..a4872a631e --- /dev/null +++ b/intTests/test2242_2243/README @@ -0,0 +1,9 @@ +Examples from #2242 (scoping regression in proof_subshell) and #2243 +(bindings escape proof_subshell). + +It might be better to use test-and-diff.sh here so as to capture the +output; however, it doesn't work. For a TopLevel subshell, the input +for the subshell needs to be on stdin, even if you use .isaw files +with saw -B, and test-and-diff.sh can't do that. For a ProofScript +subshell, it's even worse: for some reason one gets "Proof subshells +not supported". diff --git a/intTests/test2242_2243/leak01.saw b/intTests/test2242_2243/leak01.saw new file mode 100644 index 0000000000..c3a1488c8d --- /dev/null +++ b/intTests/test2242_2243/leak01.saw @@ -0,0 +1,10 @@ +// Example of plain subshell leaking a binding from #2243 + +enable_experimental; + +let f () = do { subshell (); print "(exit)"; return (); }; +let x = 3; +f (); +print "should be 3"; +print x; +prove_print z3 {{ `x == 3 }}; diff --git a/intTests/test2242_2243/leak01.stdin b/intTests/test2242_2243/leak01.stdin new file mode 100644 index 0000000000..08f32c2eef --- /dev/null +++ b/intTests/test2242_2243/leak01.stdin @@ -0,0 +1 @@ +let x = 5 diff --git a/intTests/test2242_2243/leak02.saw b/intTests/test2242_2243/leak02.saw new file mode 100644 index 0000000000..3d292f0a55 --- /dev/null +++ b/intTests/test2242_2243/leak02.saw @@ -0,0 +1,11 @@ +// Proof subshell analogue of leak01 + +enable_experimental; + +let f () = do { proof_subshell (); let _ = run (print "(exit)"); return (); }; +let x = 3; +prove_print (f ()) {{ `x == 3 }}; + +print "should be 3"; +print x; +prove_print z3 {{ `x == 3 }}; diff --git a/intTests/test2242_2243/leak02.stdin b/intTests/test2242_2243/leak02.stdin new file mode 100644 index 0000000000..ac23298015 --- /dev/null +++ b/intTests/test2242_2243/leak02.stdin @@ -0,0 +1,2 @@ +let x = 5 +z3 diff --git a/intTests/test2242_2243/leak03.saw b/intTests/test2242_2243/leak03.saw new file mode 100644 index 0000000000..a22c3d1c06 --- /dev/null +++ b/intTests/test2242_2243/leak03.saw @@ -0,0 +1,20 @@ +// Example from #2243 using the Cryptol scope. + +enable_experimental; + +let foo () = do { + prove_print do { + proof_subshell (); + let _ = run (print {{ quack }}); + return (); + } {{ True }}; +}; + +let bar () = do { + print {{ quack }}; +}; + +print "this should print 3"; +foo (); +print "this should fail"; +fails (bar ()); diff --git a/intTests/test2242_2243/leak03.stdin b/intTests/test2242_2243/leak03.stdin new file mode 100644 index 0000000000..447452620f --- /dev/null +++ b/intTests/test2242_2243/leak03.stdin @@ -0,0 +1,2 @@ +let quack = {{ 3 : [8] }} +trivial diff --git a/intTests/test2242_2243/present01.saw b/intTests/test2242_2243/present01.saw new file mode 100644 index 0000000000..8f91a449cb --- /dev/null +++ b/intTests/test2242_2243/present01.saw @@ -0,0 +1,13 @@ +// TopLevel analogue of present02. +// +// The stdin file feeds f () to subshell; if f is missing from +// the nested environment that won't work. + +enable_experimental; + +let foo (x : Integer) : TopLevel () = do { + let f () = print x; + subshell (); +}; + +foo 5; diff --git a/intTests/test2242_2243/present01.stdin b/intTests/test2242_2243/present01.stdin new file mode 100644 index 0000000000..39270e49c8 --- /dev/null +++ b/intTests/test2242_2243/present01.stdin @@ -0,0 +1 @@ +f () diff --git a/intTests/test2242_2243/present02.saw b/intTests/test2242_2243/present02.saw new file mode 100644 index 0000000000..1ce098a2f3 --- /dev/null +++ b/intTests/test2242_2243/present02.saw @@ -0,0 +1,16 @@ +// Simple example akin to the failure case from #2242. +// +// The stdin file feeds f () to proof_subshell; if f is missing from +// the nested environment that won't work. + +enable_experimental; + +let foo (x : Integer) : TopLevel Theorem = do { + let f () = z3; + + prove_print do { + proof_subshell (); + } {{ `x == 5 }}; +}; + +foo 5; diff --git a/intTests/test2242_2243/present02.stdin b/intTests/test2242_2243/present02.stdin new file mode 100644 index 0000000000..39270e49c8 --- /dev/null +++ b/intTests/test2242_2243/present02.stdin @@ -0,0 +1 @@ +f () diff --git a/intTests/test2242_2243/test.sh b/intTests/test2242_2243/test.sh new file mode 100644 index 0000000000..8f4083c91a --- /dev/null +++ b/intTests/test2242_2243/test.sh @@ -0,0 +1,8 @@ +set -e + +$SAW present01.saw < present01.stdin +$SAW present02.saw < present02.stdin + +$SAW leak01.saw < leak01.stdin +$SAW leak02.saw < leak02.stdin +$SAW leak03.saw < leak03.stdin From fcb80623a78d19bafc06e87ab5148aa726280094 Mon Sep 17 00:00:00 2001 From: David Holland Date: Wed, 22 Oct 2025 00:35:12 -0400 Subject: [PATCH 13/13] Add CHANGES note about new cryptol_load/cryptol_prims restriction. These are now explicitly prohibited in nested blocks. --- CHANGES.md | 3 +++ 1 file changed, 3 insertions(+) diff --git a/CHANGES.md b/CHANGES.md index 2e2d9e25d6..6100f40b21 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -6,6 +6,9 @@ This release supports [version ## Changes +* The `cryptol_load` and `cryptol_prims` commands now fail if used + in a nested scope, instead of behaving strangely. + * The old behavior of SAWScript where top-level names could be arbitrarily rebound, such that existing uses would see the updated value, has been superseded. Among other problems, it wasn't