From ac2a9109ed8271baeaec5ccf5700f2890c08fef7 Mon Sep 17 00:00:00 2001
From: Rob Dockins <rdockins@galois.com>
Date: Wed, 27 Apr 2022 16:35:17 -0700
Subject: [PATCH] Make `checkpoint` somewhat less broken. This change causes
 the `NameSeeds` value used internally by Cryptol to be carried forward across
 checkpoints.  This prevents internal nonce values from being reused, which,
 in turn, avoids errors about registering duplicate names.

It is unclear if this is the correct long-term fix, but it allows
checkpoint to work more reliably when importing Cryptol modules
or using `let {{ ... }}` constructs.
---
 .../src/Verifier/SAW/CryptolEnv.hs            | 10 +++++++
 src/SAWScript/Value.hs                        | 28 +++++++++++++++++--
 2 files changed, 36 insertions(+), 2 deletions(-)

diff --git a/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs b/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs
index ab10fb9921..61e21e0d11 100644
--- a/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs
+++ b/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs
@@ -16,6 +16,7 @@ module Verifier.SAW.CryptolEnv
   , loadCryptolModule
   , bindCryptolModule
   , lookupCryptolModule
+  , combineCryptolEnv
   , importModule
   , bindTypedTerm
   , bindType
@@ -342,6 +343,15 @@ genTermEnv sc modEnv cryEnv0 = do
 
 --------------------------------------------------------------------------------
 
+
+combineCryptolEnv :: CryptolEnv -> CryptolEnv -> IO CryptolEnv
+combineCryptolEnv chkEnv newEnv =
+  do let newMEnv = eModuleEnv newEnv
+     let chkMEnv = eModuleEnv chkEnv
+     let menv' = chkMEnv{ ME.meNameSeeds = ME.meNameSeeds newMEnv }
+     return chkEnv{ eModuleEnv = menv' }
+
+
 checkNotParameterized :: T.Module -> IO ()
 checkNotParameterized m =
   when (T.isParametrizedModule m) $
diff --git a/src/SAWScript/Value.hs b/src/SAWScript/Value.hs
index 49f5e707fb..33023a601a 100644
--- a/src/SAWScript/Value.hs
+++ b/src/SAWScript/Value.hs
@@ -568,15 +568,39 @@ io f = (TopLevel_ (liftIO f))
       do pos <- getPosition
          rethrow (SS.TopLevelException pos ("Error in x86 code: " ++ s))
 
+
+
+
+combineRW :: TopLevelCheckpoint -> TopLevelRW -> IO TopLevelRW
+combineRW (TopLevelCheckpoint chk) rw =
+  do cenv' <- CEnv.combineCryptolEnv (rwCryptol chk) (rwCryptol rw)
+     return chk{ rwCryptol = cenv' }
+
+-- | Represents the mutable state of the TopLevel monad
+--   that can later be restored.
+newtype TopLevelCheckpoint =
+  TopLevelCheckpoint TopLevelRW
+
+makeCheckpoint :: TopLevel TopLevelCheckpoint
+makeCheckpoint =
+  do rw <- getTopLevelRW
+     return (TopLevelCheckpoint rw)
+
+restoreCheckpoint :: TopLevelCheckpoint -> TopLevel ()
+restoreCheckpoint chk =
+  do rw <- getTopLevelRW
+     rw' <- io (combineRW chk rw)
+     putTopLevelRW rw'
+
 -- | Capture the current state of the TopLevel monad
 --   and return an action that, if invoked, resets
 --   the state back to that point.
 checkpoint :: TopLevel (() -> TopLevel ())
 checkpoint =
-  do rw <- getTopLevelRW
+  do chk <- makeCheckpoint
      return $ \_ ->
        do printOutLnTop Info "Restoring state from checkpoint"
-          putTopLevelRW rw
+          restoreCheckpoint chk
 
 throwTopLevel :: String -> TopLevel a
 throwTopLevel msg = do