From 24def9b226ea3b0f2e8856a104b38b52ebe17576 Mon Sep 17 00:00:00 2001
From: Rob Dockins <rdockins@galois.com>
Date: Tue, 21 Jun 2022 12:14:10 -0700
Subject: [PATCH] Add a command to clear the SAWCore term cache.

This cache is used for hash-consing.  It shouldn't affect
correctness to clear it, although it may make hash-consing
less effective.
---
 saw-core/src/Verifier/SAW/SharedTerm.hs | 3 +++
 src/SAWScript/Builtins.hs               | 5 +++++
 src/SAWScript/Interpreter.hs            | 8 ++++++++
 3 files changed, 16 insertions(+)

diff --git a/saw-core/src/Verifier/SAW/SharedTerm.hs b/saw-core/src/Verifier/SAW/SharedTerm.hs
index d0cfae71e7..96fe94b555 100644
--- a/saw-core/src/Verifier/SAW/SharedTerm.hs
+++ b/saw-core/src/Verifier/SAW/SharedTerm.hs
@@ -59,6 +59,7 @@ module Verifier.SAW.SharedTerm
   , SharedContext
   , mkSharedContext
   , scGetModuleMap
+  , scClearTermCache
     -- ** Low-level generic term constructors
   , scTermF
   , scFlatTermF
@@ -358,6 +359,7 @@ data SharedContext = SharedContext
   , scNamingEnv      :: IORef SAWNamingEnv
   , scGlobalEnv      :: IORef (HashMap Ident Term)
   , scFreshGlobalVar :: IO VarIndex
+  , scClearTermCache :: IO ()
   }
 
 -- | Create a new term from a lower-level 'FlatTermF' term.
@@ -2331,6 +2333,7 @@ mkSharedContext = do
            , scFreshGlobalVar = freshGlobalVar
            , scNamingEnv = envRef
            , scGlobalEnv = gr
+           , scClearTermCache = modifyMVar cr (\_ -> return (emptyAppCache , ()))
            }
 
 useChangeCache :: C m => Cache m k (Change v) -> k -> ChangeT m v -> ChangeT m v
diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs
index 36044e1bb7..7d16f31292 100644
--- a/src/SAWScript/Builtins.hs
+++ b/src/SAWScript/Builtins.hs
@@ -411,6 +411,11 @@ getTopLevelPPOpts = do
   opts <- fmap rwPPOpts getTopLevelRW
   return (SV.sawPPOpts opts)
 
+clear_term_cache :: TopLevel ()
+clear_term_cache =
+  do sc <- getSharedContext
+     io $ scClearTermCache sc
+
 show_term :: Term -> TopLevel String
 show_term t =
   do opts <- getTopLevelPPOpts
diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs
index ed8c1fb123..9fcf662ef7 100644
--- a/src/SAWScript/Interpreter.hs
+++ b/src/SAWScript/Interpreter.hs
@@ -1033,6 +1033,14 @@ primitives = Map.fromList
     Current
     [ "Return the type of the given term." ]
 
+  , prim "clear_term_cache"    "TopLevel ()"
+    (pureVal clear_term_cache)
+    Experimental
+    [ "Empty the hash-consing cache for SAWCore terms."
+    , "This can be useful to help control memory usage, but makes"
+    , "hash-consing less effective."
+    ]
+
   , prim "show_term"           "Term -> String"
     (funVal1 show_term)
     Current