Merge pull request #589 from ethereum/mult-thread-z3

Preliminary support for multi-threaded Z3

CHANGELOG.md

@@ -35,6 +35,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - All fuzz tests now run twice, once with expected SAT and once with expected UNSAT to check
   against incorrectly trivial UNSAT queries
 - Allow --num-solvers option for equivalence checking, use num cores by default
+- Preliminary support for multi-threaded Z3
 
 ## Fixed
 - `concat` is a 2-ary, not an n-ary function in SMT2LIB, declare-const does not exist in QF_AUFBV, replacing

bench/bench.hs

@@ -91,7 +91,7 @@ runBCTest x =
 
 findPanics :: App m => Solver -> Natural -> Integer -> ByteString -> m ()
 findPanics solver count iters c = do
-  _ <- withSolvers solver count Nothing $ \s -> do
+  _ <- withSolvers solver count 1 Nothing $ \s -> do
     let opts = defaultVeriOpts
           { maxIter = Just iters
           , askSmtIters = iters + 1

cli/cli.hs

@@ -94,6 +94,7 @@ data Command w
       , askSmtIterations :: w ::: Integer         <!> "1" <?> "Number of times we may revisit a particular branching point before we consult the smt solver to check reachability (default: 1)"
       , numCexFuzz    :: w ::: Integer            <!> "3" <?> "Number of fuzzing tries to do to generate a counterexample (default: 3)"
       , numSolvers    :: w ::: Maybe Natural      <?> "Number of solver instances to use (default: number of cpu cores)"
+      , solverThreads :: w ::: Maybe Natural      <?> "Number of threads for each solver instance. Only respected for Z3 (default: 1)"
       , loopDetectionHeuristic :: w ::: LoopHeuristic <!> "StackBased" <?> "Which heuristic should be used to determine if we are in a loop: StackBased (default) or Naive"
       , abstractArithmetic    :: w ::: Bool             <?> "Use abstraction-refinement for complicated arithmetic functions such as MulMod. This runs the solver first with abstraction turned on, and if it returns a potential counterexample, the counterexample is refined to make sure it is a counterexample for the actual (not the abstracted) problem"
       , abstractMemory    :: w ::: Bool                      <?> "Use abstraction-refinement for Memory. This runs the solver first with abstraction turned on, and if it returns a potential counterexample, the counterexample is refined to make sure it is a counterexample for the actual (not the abstracted) problem"
@@ -115,6 +116,7 @@ data Command w
       , askSmtIterations :: w ::: Integer       <!> "1" <?> "Number of times we may revisit a particular branching point before we consult the smt solver to check reachability (default: 1)"
       , numCexFuzz    :: w ::: Integer          <!> "3" <?> "Number of fuzzing tries to do to generate a counterexample (default: 3)"
       , numSolvers    :: w ::: Maybe Natural    <?> "Number of solver instances to use (default: number of cpu cores)"
+      , solverThreads :: w ::: Maybe Natural    <?> "Number of threads for each solver instance. Only respected for Z3 (default: 1)"
       , loopDetectionHeuristic :: w ::: LoopHeuristic <!> "StackBased" <?> "Which heuristic should be used to determine if we are in a loop: StackBased (default) or Naive"
       , abstractArithmetic    :: w ::: Bool             <?> "Use abstraction-refinement for complicated arithmetic functions such as MulMod. This runs the solver first with abstraction turned on, and if it returns a potential counterexample, the counterexample is refined to make sure it is a counterexample for the actual (not the abstracted) problem"
       , abstractMemory    :: w ::: Bool                      <?> "Use abstraction-refinement for Memory. This runs the solver first with abstraction turned on, and if it returns a potential counterexample, the counterexample is refined to make sure it is a counterexample for the actual (not the abstracted) problem"
@@ -157,6 +159,7 @@ data Command w
       , match         :: w ::: Maybe String             <?> "Test case filter - only run methods matching regex"
       , solver        :: w ::: Maybe Text               <?> "Used SMT solver: z3 (default), cvc5, or bitwuzla"
       , numSolvers    :: w ::: Maybe Natural            <?> "Number of solver instances to use (default: number of cpu cores)"
+      , solverThreads :: w ::: Maybe Natural            <?> "Number of threads for each solver instance. Only respected for Z3 (default: 1)"
       , smtdebug      :: w ::: Bool                     <?> "Print smt queries sent to the solver"
       , debug         :: w ::: Bool                     <?> "Debug printing of internal behaviour, and dump internal expressions"
       , trace         :: w ::: Bool                     <?> "Dump trace"
@@ -226,7 +229,7 @@ main = withUtf8 $ do
       solver <- getSolver cmd
       cores <- liftIO $ unsafeInto <$> getNumProcessors
       let solverCount = fromMaybe cores cmd.numSolvers
-      runEnv env $ withSolvers solver solverCount cmd.smttimeout $ \solvers -> do
+      runEnv env $ withSolvers solver solverCount (fromMaybe 1 cmd.solverThreads) cmd.smttimeout $ \solvers -> do
         buildOut <- readBuildOutput root (getProjectType cmd)
         case buildOut of
           Left e -> liftIO $ do
@@ -252,7 +255,7 @@ equivalence cmd = do
   solver <- liftIO $ getSolver cmd
   cores <- liftIO $ unsafeInto <$> getNumProcessors
   let solverCount = fromMaybe cores cmd.numSolvers
-  withSolvers solver solverCount cmd.smttimeout $ \s -> do
+  withSolvers solver solverCount (fromMaybe 1 cmd.solverThreads) cmd.smttimeout $ \s -> do
     res <- equivalenceCheck s bytecodeA bytecodeB veriOpts calldata
     case any isCex res of
       False -> liftIO $ do
@@ -328,7 +331,7 @@ assert cmd = do
   cores <- liftIO $ unsafeInto <$> getNumProcessors
   let solverCount = fromMaybe cores cmd.numSolvers
   solver <- liftIO $ getSolver cmd
-  withSolvers solver solverCount cmd.smttimeout $ \solvers -> do
+  withSolvers solver solverCount (fromMaybe 1 cmd.solverThreads) cmd.smttimeout $ \solvers -> do
     let opts = VeriOpts { simp = True
                         , maxIter = cmd.maxIterations
                         , askSmtIters = cmd.askSmtIterations
@@ -393,7 +396,7 @@ launchExec cmd = do
     rpcinfo = (,) block <$> cmd.rpc
 
   -- TODO: we shouldn't need solvers to execute this code
-  withSolvers Z3 0 Nothing $ \solvers -> do
+  withSolvers Z3 0 1 Nothing $ \solvers -> do
     vm' <- EVM.Stepper.interpret (Fetch.oracle solvers rpcinfo) vm EVM.Stepper.runFully
     writeTraceDapp dapp vm'
     case vm'.result of

src/EVM/Fetch.hs

@@ -186,12 +186,12 @@ fetchChainIdFrom url = do
 
 http :: Natural -> Maybe Natural -> BlockNumber -> Text -> Fetcher t m s
 http smtjobs smttimeout n url q =
-  withSolvers Z3 smtjobs smttimeout $ \s ->
+  withSolvers Z3 smtjobs 1 smttimeout $ \s ->
     oracle s (Just (n, url)) q
 
 zero :: Natural -> Maybe Natural -> Fetcher t m s
 zero smtjobs smttimeout q =
-  withSolvers Z3 smtjobs smttimeout $ \s ->
+  withSolvers Z3 smtjobs 1 smttimeout $ \s ->
     oracle s Nothing q
 
 -- smtsolving + (http or zero)

src/EVM/Solvers.hs

@@ -96,10 +96,10 @@ writeSMT2File smt2 count abst =
     let content = formatSMT2 smt2 <> "\n\n(check-sat)"
     T.writeFile ("query-" <> (show count) <> "-" <> abst <> ".smt2") content
 
-withSolvers :: App m => Solver -> Natural -> Maybe Natural -> (SolverGroup -> m a) -> m a
-withSolvers solver count timeout cont = do
+withSolvers :: App m => Solver -> Natural -> Natural -> Maybe Natural -> (SolverGroup -> m a) -> m a
+withSolvers solver count threads timeout cont = do
     -- spawn solvers
-    instances <- mapM (const $ liftIO $ spawnSolver solver timeout) [1..count]
+    instances <- mapM (const $ liftIO $ spawnSolver solver threads timeout) [1..count]
     -- spawn orchestration thread
     taskQueue <- liftIO newChan
     availableInstances <- liftIO newChan
@@ -254,16 +254,18 @@ mkTimeout t = T.pack $ show $ (1000 *)$ case t of
   Just t' -> t'
 
 -- | Arguments used when spawning a solver instance
-solverArgs :: Solver -> Maybe Natural -> [Text]
-solverArgs solver timeout = case solver of
+solverArgs :: Solver -> Natural -> Maybe Natural -> [Text]
+solverArgs solver threads timeout = case solver of
   Bitwuzla ->
     [ "--lang=smt2"
     , "--produce-models"
     , "--time-limit-per=" <> mkTimeout timeout
     , "--bv-solver=preprop"
     ]
   Z3 ->
-    [ "-in" ]
+    [ "-st"
+    , "smt.threads=" <> (T.pack $ show threads)
+    , "-in" ]
   CVC5 ->
     [ "--lang=smt"
     , "--produce-models"
@@ -275,11 +277,11 @@ solverArgs solver timeout = case solver of
   Custom _ -> []
 
 -- | Spawns a solver instance, and sets the various global config options that we use for our queries
-spawnSolver :: Solver -> Maybe (Natural) -> IO SolverInstance
-spawnSolver solver timeout = do
+spawnSolver :: Solver -> Natural -> Maybe (Natural) -> IO SolverInstance
+spawnSolver solver threads timeout = do
   (readout, writeout) <- createPipe
   let cmd
-        = (proc (show solver) (fmap T.unpack $ solverArgs solver timeout))
+        = (proc (show solver) (fmap T.unpack $ solverArgs solver threads timeout ))
             { std_in = CreatePipe
             , std_out = UseHandle writeout
             , std_err = UseHandle writeout

test/EVM/Test/Tracing.hs

@@ -435,7 +435,7 @@ runCodeWithTrace
   :: App m
   => Fetch.RpcInfo -> EVMToolEnv -> EVMToolAlloc -> EVM.Transaction.Transaction
   -> Expr EAddr -> Expr EAddr -> m (Either (EvmError, [VMTrace]) ((Expr 'End, [VMTrace], VMTraceResult)))
-runCodeWithTrace rpcinfo evmEnv alloc txn fromAddr toAddress = withSolvers Z3 0 Nothing $ \solvers -> do
+runCodeWithTrace rpcinfo evmEnv alloc txn fromAddr toAddress = withSolvers Z3 0 1 Nothing $ \solvers -> do
   let calldata' = ConcreteBuf txn.txdata
       code' = alloc.code
       buildExpr s vm = interpret (Fetch.oracle s Nothing) Nothing 1 Naive vm runExpr
@@ -483,7 +483,7 @@ vmForRuntimeCode runtimecode calldata' evmToolEnv alloc txn fromAddr toAddress =
        <&> set (#state % #calldata) calldata'
 
 runCode :: App m => Fetch.RpcInfo -> ByteString -> Expr Buf -> m (Maybe (Expr Buf))
-runCode rpcinfo code' calldata' = withSolvers Z3 0 Nothing $ \solvers -> do
+runCode rpcinfo code' calldata' = withSolvers Z3 0 1 Nothing $ \solvers -> do
   origVM <- liftIO $ stToIO $ vmForRuntimeCode
               code'
               calldata'

test/EVM/Test/Utils.hs

@@ -38,7 +38,7 @@ runSolidityTestCustom testFile match timeout maxIter ffiAllowed rpcinfo projectT
     (compile projectType root testFile) >>= \case
       Left e -> error e
       Right bo@(BuildOutput contracts _) -> do
-        withSolvers Z3 1 timeout $ \solvers -> do
+        withSolvers Z3 1 1 timeout $ \solvers -> do
           opts <- liftIO $ testOpts solvers root (Just bo) match maxIter ffiAllowed rpcinfo
           unitTest opts contracts
 

test/rpc.hs

@@ -82,7 +82,7 @@ tests = testGroup "rpc"
           wad = 0x999999999999999999
           calldata' = ConcreteBuf $ abiMethod "transfer(address,uint256)" (AbiTuple (V.fromList [AbiAddress (Addr 0xdead), AbiUInt 256 wad]))
         vm <- liftIO $ weth9VM blockNum (calldata', [])
-        postVm <- withSolvers Z3 1 Nothing $ \solvers ->
+        postVm <- withSolvers Z3 1 1 Nothing $ \solvers ->
           Stepper.interpret (oracle solvers (Just (BlockNumber blockNum, testRpc))) vm Stepper.runFully
         let
           wethStore = (fromJust $ Map.lookup (LitAddr 0xC02aaA39b223FE8D0A0e5C4F27eAD9083C756Cc2) postVm.env.contracts).storage
@@ -106,7 +106,7 @@ tests = testGroup "rpc"
           postc _ (Failure _ _ (Revert _)) = PBool False
           postc _ _ = PBool True
         vm <- liftIO $ weth9VM blockNum calldata'
-        (_, [Cex (_, model)]) <- withSolvers Z3 1 Nothing $ \solvers ->
+        (_, [Cex (_, model)]) <- withSolvers Z3 1 1 Nothing $ \solvers ->
           verify solvers (rpcVeriOpts (BlockNumber blockNum, testRpc)) (symbolify vm) (Just postc)
         liftIO $ assertBool "model should exceed caller balance" (getVar model "arg2" >= 695836005599316055372648)
     ]