Don't dispatch SMT queries that can be proven False via simp

Using a function specifically tailored to do this. Thanks to @blishko
for the help and idea!

Cleanup

Author: msooseth

CHANGELOG.md

@@ -39,7 +39,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
   so we don't get too large buffers as counterexamples
 - More symbolic overapproximation for Balance and ExtCodeHash opcodes, fixing
   CodeHash SMT representation
-
+- We no longer dispatch Props to SMT that can be solved by a simplification
 
 ## Fixed
 - We now try to simplify expressions fully before trying to cast them to a concrete value

src/EVM/Fetch.hs

@@ -270,19 +270,20 @@ getSolutions solvers symExprPreSimp numBytes pathconditions = do
 -- will be pruned anyway.
 checkBranch :: App m => SolverGroup -> Prop -> Prop -> m BranchCondition
 checkBranch solvers branchcondition pathconditions = do
-  conf <- readConfig
-  liftIO $ checkSat solvers (assertProps conf [(branchcondition .&& pathconditions)]) >>= \case
+  let props = [pathconditions .&& branchcondition]
+  checkSatWithProps solvers props >>= \case
     -- the condition is unsatisfiable
-    Unsat -> -- if pathconditions are consistent then the condition must be false
+    (Unsat, _) -> -- if pathconditions are consistent then the condition must be false
       pure $ Case False
     -- Sat means its possible for condition to hold
-    Sat _ -> do -- is its negation also possible?
-      checkSat solvers (assertProps conf [(pathconditions .&& (PNeg branchcondition))]) >>= \case
+    (Sat {}, _) -> do -- is its negation also possible?
+      let propsNeg = [pathconditions .&& (PNeg branchcondition)]
+      checkSatWithProps solvers propsNeg >>= \case
         -- No. The condition must hold
-        Unsat -> pure $ Case True
+        (Unsat, _) -> pure $ Case True
         -- Yes. Both branches possible
-        Sat _ -> pure EVM.Types.Unknown
-    -- If the query times out, or can't be executed (e.g. symbolic copyslice) we simply explore both paths
+        (Sat {}, _) -> pure EVM.Types.Unknown
+        -- If the query times out, or can't be executed (e.g. symbolic copyslice) we simply explore both paths
         _ -> pure EVM.Types.Unknown
     -- If the query times out, or can't be executed (e.g. symbolic copyslice) we simply explore both paths
     _ -> pure EVM.Types.Unknown

src/EVM/Solvers.hs

@@ -30,6 +30,7 @@ import EVM.Fuzz (tryCexFuzz)
 import Numeric (readHex)
 import Data.Bits ((.&.))
 import Numeric (showHex)
+import EVM.Expr (simplifyProps)
 
 import EVM.SMT
 import EVM.Types
@@ -106,6 +107,19 @@ checkMulti (SolverGroup taskQueue) smt2 multiSol = do
     -- collect result
     readChan resChan
 
+checkSatWithProps :: App m => SolverGroup -> [Prop] ->m (CheckSatResult, Err SMT2)
+checkSatWithProps (SolverGroup taskQueue) props = do
+  conf <- readConfig
+  let psSimp = simplifyProps props
+  if psSimp == [PBool False] then pure (Unsat, Right mempty)
+  else do
+    let smt2 = assertProps conf psSimp
+    if isLeft smt2 then
+      let err = getError smt2 in pure (EVM.Solvers.Unknown err, Left err)
+    else do
+      res <- liftIO $ checkSat (SolverGroup taskQueue) smt2
+      pure (res, Right (getNonError smt2))
+
 checkSat :: SolverGroup -> Err SMT2 -> IO CheckSatResult
 checkSat (SolverGroup taskQueue) smt2 = do
   if isLeft smt2 then pure $ Error $ getError smt2

src/EVM/SymExec.hs

@@ -550,8 +550,7 @@ flattenExpr = go []
 -- TODO: handle errors properly
 reachable :: App m => SolverGroup -> Expr End -> m ([SMT2], Expr End)
 reachable solvers e = do
-  conf <- readConfig
-  res <- liftIO $ go conf [] e
+  res <- go [] e
   pure $ second (fromMaybe (internalError "no reachable paths found")) res
   where
     {-
@@ -560,24 +559,23 @@ reachable solvers e = do
        If reachable return the expr wrapped in a Just. If not return Nothing.
        When walking back up the tree drop unreachable subbranches.
     -}
-    go :: Config -> [Prop] -> Expr End -> IO ([SMT2], Maybe (Expr End))
-    go conf pcs = \case
+    go :: (App m, MonadUnliftIO m) => [Prop] -> Expr End -> m ([SMT2], Maybe (Expr End))
+    go pcs = \case
       ITE c t f -> do
-        (tres, fres) <- concurrently
-          (go conf (PEq (Lit 1) c : pcs) t)
-          (go conf (PEq (Lit 0) c : pcs) f)
+        (tres, fres) <- withRunInIO $ \env -> concurrently
+          (env $ go (PEq (Lit 1) c : pcs) t)
+          (env $ go (PEq (Lit 0) c : pcs) f)
         let subexpr = case (snd tres, snd fres) of
               (Just t', Just f') -> Just $ ITE c t' f'
               (Just t', Nothing) -> Just t'
               (Nothing, Just f') -> Just f'
               (Nothing, Nothing) -> Nothing
         pure (fst tres <> fst fres, subexpr)
       leaf -> do
-        let query = assertProps conf pcs
-        res <- checkSat solvers query
+        (res, smt2) <- checkSatWithProps solvers pcs
         case res of
-          Sat _ -> pure ([getNonError query], Just leaf)
-          Unsat -> pure ([getNonError query], Nothing)
+          Sat _ -> pure ([getNonError smt2], Just leaf)
+          Unsat -> pure ([getNonError smt2], Nothing)
           r -> internalError $ "Invalid solver result: " <> show r
 
 -- | Extract constraints stored in Expr End nodes
@@ -766,35 +764,32 @@ equivalenceCheck' solvers branchesA branchesB = do
     -- 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 :: Config -> UnsatCache -> (Set Prop) -> IO (EquivResult, Bool)
-    check conf knownUnsat props = do
-      let smt = assertProps conf (Set.toList props)
-      ku <- readTVarIO knownUnsat
-      res <- if subsetAny props ku
-             then pure (True, Unsat)
-             else (fmap ((False),) (checkSat solvers smt))
+    check :: App m => UnsatCache -> Set Prop -> m (EquivResult, Bool)
+    check knownUnsat props = do
+      ku <- liftIO $ readTVarIO knownUnsat
+      res <- if subsetAny props ku then pure (True, Unsat)
+             else do
+               (res, _) <- checkSatWithProps solvers $ Set.toList props
+               pure (False, res)
       case res of
         (_, Sat x) -> pure (Cex x, False)
-        (quick, Unsat) ->
-          case quick of
-            True  -> pure (Qed (), quick)
-            False -> do
-              -- nb: we might end up with duplicates here due to a
-              -- potential race, but it doesn't matter for correctness
-              atomically $ readTVar knownUnsat >>= writeTVar knownUnsat . (props :)
-              pure (Qed (), False)
+        (True, Unsat) -> pure (Qed (), True)
+        (False, Unsat) -> do
+          -- nb: we might end up with duplicates here due to a
+          -- potential race, but it doesn't matter for correctness
+          liftIO $ atomically $ readTVar knownUnsat >>= writeTVar knownUnsat . (props :)
+          pure (Qed (), False)
         (_, EVM.Solvers.Unknown _) -> pure (EVM.SymExec.Unknown (), False)
         (_, EVM.Solvers.Error txt) -> pure (EVM.SymExec.Error txt, False)
 
     -- Allows us to run it 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 => [(Set Prop)] -> UnsatCache -> Int -> m [(EquivResult, Bool)]
-    checkAll input cache numproc = do
-       conf <- readConfig
-       wrap <- liftIO $ pool numproc
-       liftIO $ parMapIO (wrap . (check conf cache)) input
+    checkAll :: (App m, MonadUnliftIO m) => [(Set Prop)] -> UnsatCache -> Int -> m [(EquivResult, Bool)]
+    checkAll input cache numproc = withRunInIO $ \env -> do
+       wrap <- pool numproc
+       parMapIO (\e -> wrap (env $ check cache e)) input
 
 
     -- Takes two branches and returns a set of props that will need to be

test/test.hs

@@ -1770,7 +1770,7 @@ tests = testGroup "hevm"
             |]
         (e, [Qed _]) <- withDefaultSolver $
           \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256)" [AbiUIntType 256])) [] (defaultVeriOpts{ maxIter = Just 5 })
-        assertBoolM "The expression is not partial" $ Expr.containsNode isPartial e
+        assertBoolM "The expression MUST be partial" $ Expr.containsNode isPartial e
     , test "inconsistent-paths" $ do
         Just c <- solcRuntime "C"
             [i|
@@ -1829,9 +1829,8 @@ tests = testGroup "hevm"
             -- askSmtIters is low enough here to avoid the inconsistent path
             -- conditions, so we never hit maxIters
             opts = defaultVeriOpts{ maxIter = Just 5, askSmtIters = 1 }
-        (e, [Qed _]) <- withDefaultSolver $
-          \s -> checkAssert s defaultPanicCodes c sig [] opts
-        assertBoolM "The expression is partial" $ not (Expr.containsNode isPartial e)
+        (e, [Qed _]) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c sig [] opts
+        assertBoolM "The expression MUST NOT be partial" $ not (Expr.containsNode isPartial e)
     ]
   , testGroup "Symbolic Addresses"
     [ test "symbolic-address-create" $ do
@@ -4590,16 +4589,15 @@ checkEquivAndLHS orig simp = do
 
 checkEquivBase :: (Eq a, App m) => (a -> a -> Prop) -> a -> a -> Bool -> m (Maybe Bool)
 checkEquivBase mkprop l r expect = do
-  withSolvers Z3 1 1 (Just 1) $ \solvers -> liftIO $ do
-     let smt = assertPropsNoSimp [mkprop l r]
-     res <- checkSat solvers smt
+  withSolvers Z3 1 1 (Just 1) $ \solvers -> do
+     (res, _) <- checkSatWithProps solvers [mkprop l r]
      let
        ret = case res of
          Unsat -> Just True
          Sat _ -> Just False
          EVM.Solvers.Error _ -> Just (not expect)
          EVM.Solvers.Unknown _ -> Nothing
-     when (ret == Just (not expect)) $ print res
+     when (ret == Just (not expect)) $ liftIO $ print res
      pure ret
 
 -- | Takes a runtime code and calls it with the provided calldata