From d19920a88bacdc3adbb96dfa36d8b66cb2fbaf62 Mon Sep 17 00:00:00 2001
From: Daniel Matichuk <dmatichuk@galois.com>
Date: Fri, 25 Oct 2024 16:32:01 -0700
Subject: [PATCH] allow forked solver instances to share the sat/unsat cache

a forked instance of the solver has the same assumption context,
and so any results about satisfiability/unsatisfiability can
be re-used by other threads
---
 src/Pate/Monad.hs                       | 31 ++++++++++++++++++++-----
 src/Pate/Verification/StrongestPosts.hs |  2 +-
 2 files changed, 26 insertions(+), 7 deletions(-)

diff --git a/src/Pate/Monad.hs b/src/Pate/Monad.hs
index 2426dd4e..d7d40047 100644
--- a/src/Pate/Monad.hs
+++ b/src/Pate/Monad.hs
@@ -110,6 +110,7 @@ module Pate.Monad
   , withFreshSolver
   , forkBins
   , withForkedSolver
+  , withForkedSolver_
   )
   where
 
@@ -1627,22 +1628,40 @@ withFreshSolver f = do
   let solver = PC.cfgSolver vcfg
   PSo.Sym n sym _ <- CMR.asks envValidSym
   asm <- currentAsm
-  PSo.withOnlineSolver solver Nothing sym $ \bak ->
+  PSo.withOnlineSolver solver Nothing sym $ \bak -> do
+    unsatCacheRef <- asks envUnsatCacheRef
+    satCache <- asks envSatCacheRef
+
     CMR.local (\env -> env {envValidSym = PSo.Sym n sym bak, envCurrentFrame = mempty }) $ 
-      withAssumptionSet asm $ f
+      withAssumptionSet asm $ CMR.local (\env -> env { envUnsatCacheRef = unsatCacheRef, envSatCacheRef = satCache }) f
 
--- | Run the given computation in a forked thread with a fresh solver process.
---   This is non-blocking and the current solver process is left unmodified.
-withForkedSolver ::
+
+-- | Similar to 'withForkedSolver' but does not return a result.
+withForkedSolver_ ::
   EquivM_ sym arch () ->
   EquivM sym arch ()
-withForkedSolver f = do
+withForkedSolver_ f = do
   thistid <- IO.liftIO $ IO.myThreadId
   _ <- IO.withRunInIO $ \runInIO -> 
     IO.forkFinally (runInIO $ withFreshSolver f)
       (\case Left err -> IO.throwTo thistid err; Right () -> return ())
   return ()
 
+-- | Run the given function in a forked thread with a fresh solver process.
+--   This is non-blocking and the current solver process is left unmodified.
+--   The returned IO action will block until the given function has finished.
+withForkedSolver ::
+  EquivM_ sym arch a ->
+  EquivM sym arch (IO a)
+withForkedSolver f = do
+  thistid <- IO.liftIO $ IO.myThreadId
+  outVar <- IO.liftIO $ IO.newEmptyMVar
+  _ <- IO.withRunInIO $ \runInIO -> 
+    IO.forkFinally (runInIO $ withFreshSolver f)
+      (\case Left err -> IO.throwTo thistid err; Right a -> IO.putMVar outVar a)
+  return $ IO.readMVar outVar
+
+
 -- | Similar to 'forBins' but runs the 'Patched' process in a separate thread
 --   concurrently with a fresh solver process.
 forkBins ::
diff --git a/src/Pate/Verification/StrongestPosts.hs b/src/Pate/Verification/StrongestPosts.hs
index d528eb41..837a203e 100644
--- a/src/Pate/Verification/StrongestPosts.hs
+++ b/src/Pate/Verification/StrongestPosts.hs
@@ -1320,7 +1320,7 @@ getTracesForPred ::
 getTracesForPred scope bundle dom p = withSym $ \sym -> do
   not_p <- liftIO $ W4.notPred sym p
   withTracing @"expr" (Some p) $ do
-    withTracing @"message" "Simplified Condition" $ withForkedSolver $ do
+    withTracing @"message" "Simplified Condition" $ withForkedSolver_ $ do
       p_pretty <- withTracing @"debug" "simplifier" $ PSi.applySimpStrategy PSi.prettySimplifier p
       emitTrace @"expr" (Some p_pretty)
     mtraceT <- withTracing @"message" "With condition assumed" $