Move unsat cache to Solver.hs in a central location

msooseth · msooseth · commit 63c8e81a29e4 · 2025-05-19T10:09:30.000+02:00
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -51,6 +51,8 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
   currently executed branch is in fact impossible. In these cases, unwind all
   frames and return a Revert with empty returndata.
 - More rewrite rules for PEq, PNeg, missing eqByte call, and distributivity for And
+- UNSAT cache is now in `Solvers.hs` and is therefore shared across all threads.
+  Hence, it is now active even during branch queries.
 
 ## Fixed
 - We now try to simplify expressions fully before trying to cast them to a concrete value
diff --git a/src/EVM.hs b/src/EVM.hs
@@ -2968,7 +2968,7 @@ writeMemory memory offset buf = do
       let growthFactor = 2
       let targetSize = requiredSize * growthFactor
       -- Always grow at least 8k
-      let toGrow = max 8192 $ targetSize - currentSize 
+      let toGrow = max 8192 $ targetSize - currentSize
       memory' <- VUnboxed.Mutable.grow memory toGrow
       assign (#state % #memory) (ConcreteMemory memory')
       pure memory'
diff --git a/src/EVM/Solvers.hs b/src/EVM/Solvers.hs
@@ -16,6 +16,7 @@ import Control.Monad.IO.Unlift
 import Data.Char (isSpace)
 import Data.Map (Map)
 import Data.Map qualified as Map
+import Data.Set (Set, isSubsetOf, fromList)
 import Data.Maybe (fromMaybe, isJust, fromJust)
 import Data.Either (isLeft)
 import Data.Text qualified as TStrict
@@ -67,7 +68,7 @@ data MultiSol = MultiSol
   }
 
 -- | A script to be executed, a list of models to be extracted in the case of a sat result, and a channel where the result should be written
-data Task = TaskSingle SingleData | TaskMulti MultiData
+data Task = TaskSingle SingleData | TaskMulti MultiData | TaskAddCache [Prop]
 
 data MultiData = MultiData
   { smt2 :: SMT2
@@ -77,9 +78,14 @@ data MultiData = MultiData
 
 data SingleData = SingleData
   { smt2 :: SMT2
+  , props :: [Prop]
   , resultChan :: Chan SMTResult
   }
 
+-- returns True if a is a subset of any of the sets in b
+subsetAny :: [Prop] -> [Set Prop] -> Bool
+subsetAny a b = let s = fromList a in foldr (\bp acc -> acc || isSubsetOf s bp) False b
+
 checkMulti :: SolverGroup -> Err SMT2 -> MultiSol -> IO (Maybe [W256])
 checkMulti (SolverGroup taskQueue) smt2 multiSol = do
   if isLeft smt2 then pure Nothing
@@ -92,7 +98,7 @@ checkMulti (SolverGroup taskQueue) smt2 multiSol = do
     readChan resChan
 
 checkSatWithProps :: App m => SolverGroup -> [Prop] -> m (SMTResult, Err SMT2)
-checkSatWithProps (SolverGroup taskQueue) props = do
+checkSatWithProps sg props = do
   conf <- readConfig
   let psSimp = simplifyProps props
   if psSimp == [PBool False] then pure (Qed, Right mempty)
@@ -101,19 +107,20 @@ checkSatWithProps (SolverGroup taskQueue) props = do
     if isLeft smt2 then
       let err = getError smt2 in pure (Error err, Left err)
     else do
-      res <- liftIO $ checkSat (SolverGroup taskQueue) smt2
+      res <- liftIO $ checkSat sg smt2
       pure (res, Right (getNonError smt2))
 
-checkSat :: SolverGroup -> Err SMT2 -> IO SMTResult
-checkSat (SolverGroup taskQueue) smt2 = do
-  if isLeft smt2 then pure $ Error $ getError smt2
-  else do
-    -- prepare result channel
-    resChan <- newChan
-    -- send task to solver group
-    writeChan taskQueue (TaskSingle (SingleData (getNonError smt2) resChan))
-    -- collect result
-    readChan resChan
+  where
+    checkSat :: SolverGroup -> Err SMT2 -> IO SMTResult
+    checkSat (SolverGroup taskQueue) smt2 = do
+      if isLeft smt2 then pure $ Error $ getError smt2
+      else do
+        -- prepare result channel
+        resChan <- newChan
+        -- send task to solver group
+        writeChan taskQueue (TaskSingle (SingleData (getNonError smt2) props resChan))
+        -- collect result
+        readChan resChan
 
 writeSMT2File :: SMT2 -> String -> IO ()
 writeSMT2File smt2 postfix =
@@ -128,7 +135,7 @@ withSolvers solver count threads timeout cont = do
     taskQueue <- liftIO newChan
     availableInstances <- liftIO newChan
     liftIO $ forM_ instances (writeChan availableInstances)
-    orchestrate' <- toIO $ orchestrate taskQueue availableInstances 0
+    orchestrate' <- toIO $ orchestrate taskQueue availableInstances [] 0
     orchestrateId <- liftIO $ forkIO orchestrate'
 
     -- run continuation with task queue
@@ -139,15 +146,26 @@ withSolvers solver count threads timeout cont = do
     liftIO $ killThread orchestrateId
     pure res
   where
-    orchestrate :: App m => Chan Task -> Chan SolverInstance -> Int -> m b
-    orchestrate queue avail fileCounter = do
+    orchestrate :: App m => Chan Task -> Chan SolverInstance -> [Set Prop] -> Int -> m b
+    orchestrate queue avail knownUnsat fileCounter = do
+      conf <- readConfig
       task <- liftIO $ readChan queue
-      inst <- liftIO $ readChan avail
-      runTask' <- case task of
-        TaskSingle (SingleData smt2 r) -> toIO $ getOneSol smt2 r inst avail fileCounter
-        TaskMulti (MultiData smt2 multiSol r) -> toIO $ getMultiSol smt2 multiSol r inst avail fileCounter
-      _ <- liftIO $ forkIO runTask'
-      orchestrate queue avail (fileCounter + 1)
+      case task of
+        TaskAddCache props -> do
+          let knownUnsat' = (fromList props):knownUnsat
+          when conf.debug $ liftIO $ putStrLn "   adding UNSAT cache"
+          orchestrate queue avail knownUnsat' fileCounter
+        TaskSingle (SingleData _ props r) | subsetAny props knownUnsat -> do
+          liftIO $ writeChan r Qed
+          when conf.debug $ liftIO $ putStrLn "   Qed found via cache!"
+          orchestrate queue avail knownUnsat fileCounter
+        _ -> do
+          inst <- liftIO $ readChan avail
+          runTask' <- case task of
+            TaskSingle (SingleData smt2 props r) -> toIO $ getOneSol smt2 props r inst avail queue fileCounter
+            TaskMulti (MultiData smt2 multiSol r) -> toIO $ getMultiSol smt2 multiSol r inst avail fileCounter
+          _ <- liftIO $ forkIO runTask'
+          orchestrate queue avail knownUnsat (fileCounter + 1)
 
 getMultiSol :: forall m. (MonadIO m, ReadConfig m) => SMT2 -> MultiSol -> (Chan (Maybe [W256])) -> SolverInstance -> Chan SolverInstance -> Int -> m ()
 getMultiSol smt2@(SMT2 cmds cexvars _) multiSol r inst availableInstances fileCounter = do
@@ -211,8 +229,8 @@ getMultiSol smt2@(SMT2 cmds cexvars _) multiSol r inst availableInstances fileCo
           when conf.debug $ putStrLn $ "Unable to write SMT to solver: " <> (T.unpack err)
           writeChan r Nothing
 
-getOneSol :: (MonadIO m, ReadConfig m) => SMT2 -> (Chan SMTResult) -> SolverInstance -> Chan SolverInstance -> Int -> m ()
-getOneSol smt2@(SMT2 cmds cexvars ps) r inst availableInstances fileCounter = do
+getOneSol :: (MonadIO m, ReadConfig m) => SMT2 -> [Prop] -> Chan SMTResult -> SolverInstance -> Chan SolverInstance -> (Chan Task) -> Int -> m ()
+getOneSol smt2@(SMT2 cmds cexvars ps) props r inst availableInstances task fileCounter = do
   conf <- readConfig
   let fuzzResult = tryCexFuzz ps conf.numCexFuzz
   liftIO $ do
@@ -232,7 +250,9 @@ getOneSol smt2@(SMT2 cmds cexvars ps) r inst availableInstances fileCounter = do
             sat <- sendLine inst "(check-sat)"
             res <- do
                 case sat of
-                  "unsat" -> pure Qed
+                  "unsat" -> do
+                    writeChan task (TaskAddCache props)
+                    pure Qed
                   "timeout" -> pure $ Unknown "Result timeout by SMT solver"
                   "unknown" -> pure $ Unknown "Result unknown by SMT solver"
                   "sat" -> Cex <$> getModel inst cexvars
diff --git a/src/EVM/SymExec.hs b/src/EVM/SymExec.hs
@@ -5,13 +5,12 @@ module EVM.SymExec where
 
 import Control.Concurrent.Async (concurrently, mapConcurrently)
 import Control.Concurrent.Spawn (parMapIO, pool)
-import Control.Concurrent.STM (TVar, readTVarIO, newTVarIO)
 import Control.Monad (when, forM_, forM)
 import Control.Monad.IO.Unlift
 import Control.Monad.Operational qualified as Operational
 import Control.Monad.ST (RealWorld, stToIO, ST)
 import Control.Monad.State.Strict (runStateT)
-import Data.Bifunctor (second, first)
+import Data.Bifunctor (second)
 import Data.ByteString (ByteString)
 import Data.ByteString qualified as BS
 import Data.Containers.ListUtils (nubOrd)
@@ -22,7 +21,7 @@ import Data.Maybe (fromMaybe, listToMaybe, mapMaybe)
 import Data.Map.Strict (Map)
 import Data.Map.Strict qualified as Map
 import Data.Map.Merge.Strict qualified as Map
-import Data.Set (Set, isSubsetOf)
+import Data.Set (Set)
 import Data.Set qualified as Set
 import Data.Text (Text)
 import Data.Text qualified as T
@@ -676,34 +675,33 @@ verify solvers opts preState maybepost = do
 
   exprInter <- interpret (Fetch.oracle solvers opts.rpcInfo) opts.iterConf preState runExpr
   when conf.dumpExprs $ liftIO $ T.writeFile "unsimplified.expr" (formatExpr exprInter)
-  liftIO $ do
-    when conf.debug $ putStrLn "   Simplifying expression"
+  do
+    when conf.debug $ liftIO $ putStrLn "   Simplifying expression"
     let expr = if opts.simp then (Expr.simplify exprInter) else exprInter
-    when conf.dumpExprs $ T.writeFile "simplified.expr" (formatExpr expr)
-    when conf.dumpExprs $ T.writeFile "simplified-conc.expr" (formatExpr $ Expr.simplify $ mapExpr Expr.concKeccakOnePass expr)
+    when conf.dumpExprs $ liftIO $ T.writeFile "simplified.expr" (formatExpr expr)
+    when conf.dumpExprs $ liftIO $ T.writeFile "simplified-conc.expr" (formatExpr $ Expr.simplify $ mapExpr Expr.concKeccakOnePass expr)
     let flattened = flattenExpr expr
-    when conf.debug $ do
+    when conf.debug $ liftIO $ do
       printPartialIssues flattened ("the call " <> call)
       putStrLn $ "   Exploration finished, " <> show (Expr.numBranches expr) <> " branch(es) to check in call " <> call
 
     case maybepost of
       Nothing -> pure (expr, [Qed])
-      Just post -> liftIO $ do
+      Just post -> do
         let
           -- Filter out any leaves from `flattened` that can be statically shown to be safe
           tocheck = flip map flattened $ \leaf -> (toPropsFinal leaf preState.constraints post, leaf)
-          withQueries = filter canBeSat tocheck <&> first (SMT.assertProps conf)
-        when conf.debug $
-          putStrLn $ "   Checking for reachability of " <> show (length withQueries)
-                     <> " potential property violation(s) in call " <> call
+          withQueries = filter canBeSat tocheck
+        when conf.debug $ liftIO $ putStrLn $ "   Checking for reachability of " <> show (length withQueries) <> " potential property violation(s) in call " <> call
 
         -- Dispatch the remaining branches to the solver to check for violations
-        results <- flip mapConcurrently withQueries $ \(query, leaf) -> do
-          res <- checkSat solvers query
-          when conf.debug $ putStrLn $ "   SMT result: " <> show res
-          pure (res, leaf)
-        let cexs = filter (\(res, _) -> not . isQed $ res) results
-        when conf.debug $ putStrLn $ "   Found " <> show (length cexs) <> " potential counterexample(s) in call " <> call
+        --
+        results <- withRunInIO $ \env -> flip mapConcurrently withQueries $ \(query, leaf) -> do
+          res <- env $ checkSatWithProps solvers query
+          when conf.debug $ putStrLn $ "   SMT result: " <> show (fst res)
+          pure (fst res, leaf)
+        let cexs = filter (not . isQed . fst) results
+        when conf.debug $ liftIO $ putStrLn $ "   Found " <> show (length cexs) <> " potential counterexample(s) in call " <> call
         pure $ if Prelude.null cexs then (expr, [Qed]) else (expr, fmap toVRes cexs)
   where
     getCallPrefix :: Expr Buf -> String
@@ -715,7 +713,7 @@ verify solvers opts preState maybepost = do
     canBeSat (a, _) = case a of
         [PBool False] -> False
         _ -> True
-    toVRes :: (SMTResult, Expr End) -> VerifyResult
+    toVRes :: (SMTResult , Expr End) -> VerifyResult
     toVRes (res, leaf) = case res of
       Cex model -> Cex (leaf, expandCex preState model)
       Unknown reason -> Unknown (reason, leaf)
@@ -732,8 +730,6 @@ expandCex prestate c = c { store = Map.union c.store concretePreStore }
       ConcreteStore _ -> True
       _ -> False
 
-type UnsatCache = TVar [Set Prop]
-
 data EqIssues = EqIssues
   { res :: [(EquivResult, String)]
     , partials :: [Expr End]
@@ -835,43 +831,28 @@ equivalenceCheck' solvers branchesA branchesB create = do
       when conf.dumpEndStates $ forM_ (zip differingEndStates [(1::Integer)..]) (\(x, i) ->
         liftIO $ T.writeFile ("prop-checked-" <> show i <> ".prop") (T.pack $ show x))
 
-      knownUnsat <- liftIO $ newTVarIO []
       procs <- liftIO getNumProcessors
-      newDifferences <- checkAll differingEndStates knownUnsat procs
+      newDifferences <- checkAll differingEndStates procs
       let additionalIssues = EqIssues newDifferences mempty
       pure $ knownIssues <> additionalIssues
 
   where
-    -- we order the sets by size because this gives us more cache hits when
+    -- we order the sets by size because this gives us more UNSAT cache hits when
     -- running our queries later on (since we rely on a subset check)
     sortBySize :: [(Set a, b)] -> [(Set a, b)]
     sortBySize = sortBy (\(a, _) (b, _) -> if Set.size a > Set.size b then Prelude.LT else Prelude.GT)
 
-    -- returns True if a is a subset of any of the sets in b
-    subsetAny :: Set Prop -> [Set Prop] -> Bool
-    subsetAny a b = foldr (\bp acc -> acc || isSubsetOf a bp) False b
-
-    -- checks for satisfiability of all the props in the provided set. skips
-    -- the solver if we can determine unsatisfiability from the cache already
-    -- the last element of the returned tuple indicates whether the cache was
-    -- used or not
-    check :: App m => UnsatCache -> Set Prop -> m EquivResult
-    check knownUnsat props = do
-      ku <- liftIO $ readTVarIO knownUnsat
-      if subsetAny props ku then pure Qed
-      else fst <$> checkSatWithProps solvers (Set.toList props)
-
     -- Allows us to run the queries in parallel. Note that this (seems to) run it
     -- from left-to-right, and with a max of K threads. This is in contrast to
     -- mapConcurrently which would spawn as many threads as there are jobs, and
     -- run them in a random order. We ordered them correctly, though so that'd be bad
-    checkAll :: (App m, MonadUnliftIO m) => [(Set Prop, String)] -> UnsatCache -> Int -> m [(EquivResult, String)]
-    checkAll input cache numproc = withRunInIO $ \env -> do
+    checkAll :: (App m, MonadUnliftIO m) => [(Set Prop, String)] -> Int -> m [(EquivResult, String)]
+    checkAll input numproc = withRunInIO $ \env -> do
        wrap <- pool numproc
        parMapIO (runOne env wrap) input
        where
          runOne env wrap (props, meaning) = do
-           res <- wrap (env $ check cache props)
+           res <- wrap (env $ fst <$> checkSatWithProps solvers (Set.toList props))
            pure (res, meaning)
 
     -- Takes two branches and returns a set of props that will need to be
@@ -996,10 +977,9 @@ both' f (x, y) = (f x, f y)
 produceModels :: App m => SolverGroup -> Expr End -> m [(Expr End, SMTResult)]
 produceModels solvers expr = do
   let flattened = flattenExpr expr
-      withQueries conf = fmap (\e -> ((SMT.assertProps conf) . extractProps $ e, e)) flattened
-  conf <- readConfig
-  results <- liftIO $ (flip mapConcurrently) (withQueries conf) $ \(query, leaf) -> do
-    res <- checkSat solvers query
+      withQueries = fmap (\e -> (extractProps e, e)) flattened
+  results <- withRunInIO $ \runInIO -> (flip mapConcurrently) withQueries $ \(query, leaf) -> do
+    (res, _) <- runInIO $ checkSatWithProps solvers query
     pure (res, leaf)
   pure $ fmap swap $ filter (\(res, _) -> not . isQed $ res) results
 
diff --git a/src/EVM/Types.hs b/src/EVM/Types.hs
@@ -1199,8 +1199,8 @@ instance (Eq a, Eq b) => Eq (ProofResult a b) where
     _                        -> False
 
 type VerifyResult = ProofResult (Expr End, SMTCex) (String, Expr End)
-type EquivResult = ProofResult (SMTCex) String
-type SMTResult = ProofResult (SMTCex) String
+type EquivResult = ProofResult SMTCex String
+type SMTResult = ProofResult SMTCex String
 
 getUnknown :: ProofResult a b -> Maybe b
 getUnknown (Unknown a) = Just a
