From f099221164ff2ca9e2f2260e69ce136461d32b6b Mon Sep 17 00:00:00 2001
From: Mate Soos <mate.soos@ethereum.org>
Date: Tue, 8 Oct 2024 12:12:06 +0200
Subject: [PATCH] Multi-threading allowed for Z3
---
CHANGELOG.md | 2 +
bench/bench.hs | 2 +-
cli/cli.hs | 11 +-
src/EVM.hs | 25 ++--
src/EVM/Fetch.hs | 4 +-
src/EVM/Solvers.hs | 20 +--
test/EVM/Test/Tracing.hs | 4 +-
test/EVM/Test/Utils.hs | 2 +-
test/rpc.hs | 4 +-
test/test.hs | 254 +++++++++++++++++++++------------------
10 files changed, 177 insertions(+), 151 deletions(-)
diff --git a/CHANGELOG.md b/CHANGELOG.md
index 459a7a235..f71e2b430 100644
--- a/CHANGELOG.md
+++ b/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
@@ -55,6 +56,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
- Fixed bug in SMT encoding that caused empty and all-zero byte arrays to be considered equal
and hence lead to false negatives through trivially UNSAT SMT expressions
- Respect --smt-timeout in equivalence checking
+- Fixed the handling of returndata with an abstract size during transaction finalization
## [0.53.0] - 2024-02-23
diff --git a/bench/bench.hs b/bench/bench.hs
index 6f0a9a6aa..ea29eb333 100644
--- a/bench/bench.hs
+++ b/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
diff --git a/cli/cli.hs b/cli/cli.hs
index 6a79f82f8..24ee152d7 100644
--- a/cli/cli.hs
+++ b/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
diff --git a/src/EVM.hs b/src/EVM.hs
index 6596bf77b..f18729fd3 100644
--- a/src/EVM.hs
+++ b/src/EVM.hs
@@ -1504,19 +1504,18 @@ finalize = do
creation <- use (#tx % #isCreate)
createe <- use (#state % #contract)
createeExists <- (Map.member createe) <$> use (#env % #contracts)
- let onContractCode contractCode =
- when (creation && createeExists) $ replaceCode createe contractCode
- case output of
- ConcreteBuf bs ->
- onContractCode $ RuntimeCode (ConcreteRuntimeCode bs)
- _ ->
- case Expr.toList output of
- Nothing -> do
- state <- use #state
- partial $
- UnexpectedSymbolicArg pc' (getOpName state) "runtime code cannot have an abstract length" (wrap [output])
- Just ops ->
- onContractCode $ RuntimeCode (SymbolicRuntimeCode ops)
+ when (creation && createeExists) $
+ case output of
+ ConcreteBuf bs ->
+ replaceCode createe (RuntimeCode (ConcreteRuntimeCode bs))
+ _ ->
+ case Expr.toList output of
+ Nothing -> do
+ state <- use #state
+ partial $
+ UnexpectedSymbolicArg pc' (getOpName state) "runtime code cannot have an abstract length" (wrap [output])
+ Just ops ->
+ replaceCode createe (RuntimeCode (SymbolicRuntimeCode ops))
_ ->
internalError "Finalising an unfinished tx."
diff --git a/src/EVM/Fetch.hs b/src/EVM/Fetch.hs
index 033ffd63d..8b546c686 100644
--- a/src/EVM/Fetch.hs
+++ b/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)
diff --git a/src/EVM/Solvers.hs b/src/EVM/Solvers.hs
index 870ecbcd3..17d48bea2 100644
--- a/src/EVM/Solvers.hs
+++ b/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,8 +254,8 @@ 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"
@@ -263,7 +263,9 @@ solverArgs solver timeout = case solver of
, "--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
diff --git a/test/EVM/Test/Tracing.hs b/test/EVM/Test/Tracing.hs
index badf8f53e..a791c4d7b 100644
--- a/test/EVM/Test/Tracing.hs
+++ b/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'
diff --git a/test/EVM/Test/Utils.hs b/test/EVM/Test/Utils.hs
index 4167e5911..93c89913f 100644
--- a/test/EVM/Test/Utils.hs
+++ b/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
diff --git a/test/rpc.hs b/test/rpc.hs
index 618e067bc..5cc8fac89 100644
--- a/test/rpc.hs
+++ b/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)
]
diff --git a/test/test.hs b/test/test.hs
index bed280908..120cbfccd 100644
--- a/test/test.hs
+++ b/test/test.hs
@@ -105,6 +105,12 @@ testFuzz a b = testCase a $ runEnv (testEnv {config = testEnv.config {numCexFuzz
prop :: Testable prop => ReaderT Env IO prop -> Property
prop a = ioProperty $ runEnv testEnv a
+withDefaultSolver :: App m => (SolverGroup -> m a) -> m a
+withDefaultSolver = withSolvers Z3 1 1 Nothing
+
+withCVC5Solver :: App m => (SolverGroup -> m a) -> m a
+withCVC5Solver = withSolvers CVC5 1 1 Nothing
+
main :: IO ()
main = defaultMain tests
@@ -131,7 +137,7 @@ tests = testGroup "hevm"
}
}
|]
- expr <- withSolvers Z3 1 Nothing $ \s -> getExpr s c (Just (Sig "transfer(uint256,uint256,uint256)" [AbiUIntType 256, AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts
+ expr <- withDefaultSolver $ \s -> getExpr s c (Just (Sig "transfer(uint256,uint256,uint256)" [AbiUIntType 256, AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts
assertEqualM "Expression is not clean." (badStoresInExpr expr) False
-- This case is somewhat artificial. We can't simplify this using only
-- static rewrite rules, because acct is totally abstract and acct + 1
@@ -151,7 +157,7 @@ tests = testGroup "hevm"
}
}
|]
- expr <- withSolvers Z3 1 Nothing $ \s -> getExpr s c (Just (Sig "transfer(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts
+ expr <- withDefaultSolver $ \s -> getExpr s c (Just (Sig "transfer(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts
-- T.writeFile "symbolic-index.expr" $ formatExpr expr
assertEqualM "Expression is not clean." (badStoresInExpr expr) False
, expectFail $ test "simplify-storage-array-of-struct-symbolic-index" $ do
@@ -172,7 +178,7 @@ tests = testGroup "hevm"
}
}
|]
- expr <- withSolvers Z3 1 Nothing $ \s -> getExpr s c (Just (Sig "transfer(uint256,uint256,uint256)" [AbiUIntType 256, AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts
+ expr <- withDefaultSolver $ \s -> getExpr s c (Just (Sig "transfer(uint256,uint256,uint256)" [AbiUIntType 256, AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts
assertEqualM "Expression is not clean." (badStoresInExpr expr) False
, test "simplify-storage-array-loop-nonstruct" $ do
Just c <- solcRuntime "MyContract"
@@ -187,7 +193,7 @@ tests = testGroup "hevm"
}
}
|]
- expr <- withSolvers Z3 1 Nothing $ \s -> getExpr s c (Just (Sig "transfer(uint256)" [AbiUIntType 256])) [] (defaultVeriOpts { maxIter = Just 5 })
+ expr <- withDefaultSolver $ \s -> getExpr s c (Just (Sig "transfer(uint256)" [AbiUIntType 256])) [] (defaultVeriOpts { maxIter = Just 5 })
assertEqualM "Expression is not clean." (badStoresInExpr expr) False
, test "simplify-storage-map-newtest1" $ do
Just c <- solcRuntime "MyContract"
@@ -206,9 +212,9 @@ tests = testGroup "hevm"
}
}
|]
- expr <- withSolvers Z3 1 Nothing $ \s -> getExpr s c (Just (Sig "fun(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts
+ expr <- withDefaultSolver $ \s -> getExpr s c (Just (Sig "fun(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts
assertEqualM "Expression is not clean." (badStoresInExpr expr) False
- (_, [(Qed _)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s [0x11] c (Just (Sig "fun(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts
+ (_, [(Qed _)]) <- withDefaultSolver $ \s -> checkAssert s [0x11] c (Just (Sig "fun(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts
liftIO $ putStrLn "OK"
, ignoreTest $ test "simplify-storage-map-todo" $ do
Just c <- solcRuntime "MyContract"
@@ -230,9 +236,9 @@ tests = testGroup "hevm"
-- TODO: expression below contains (load idx1 (store idx1 (store idx1 (store idx0)))), and the idx0
-- is not stripped. This is due to us not doing all we can in this case, see
-- note above readStorage. Decompose remedies this (when it can be decomposed)
- -- expr <- withSolvers Z3 1 Nothing $ \s -> getExpr s c (Just (Sig "fun(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts
+ -- expr <- withDefaultSolver $ \s -> getExpr s c (Just (Sig "fun(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts
-- putStrLnM $ T.unpack $ formatExpr expr
- (_, [Cex _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts
+ (_, [Cex _]) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts
liftIO $ putStrLn "OK"
, test "simplify-storage-array-loop-struct" $ do
Just c <- solcRuntime "MyContract"
@@ -252,7 +258,7 @@ tests = testGroup "hevm"
}
}
|]
- expr <- withSolvers Z3 1 Nothing $ \s -> getExpr s c (Just (Sig "transfer(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] (defaultVeriOpts { maxIter = Just 5 })
+ expr <- withDefaultSolver $ \s -> getExpr s c (Just (Sig "transfer(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] (defaultVeriOpts { maxIter = Just 5 })
assertEqualM "Expression is not clean." (badStoresInExpr expr) False
, test "decompose-1" $ do
Just c <- solcRuntime "MyContract"
@@ -267,7 +273,7 @@ tests = testGroup "hevm"
}
}
|]
- expr <- withSolvers Z3 1 Nothing $ \s -> getExpr s c (Just (Sig "prove_mapping_access(address,address)" [AbiAddressType, AbiAddressType])) [] defaultVeriOpts
+ expr <- withDefaultSolver $ \s -> getExpr s c (Just (Sig "prove_mapping_access(address,address)" [AbiAddressType, AbiAddressType])) [] defaultVeriOpts
putStrLnM $ T.unpack $ formatExpr expr
let simpExpr = mapExprM Expr.decomposeStorage expr
-- putStrLnM $ T.unpack $ formatExpr (fromJust simpExpr)
@@ -284,7 +290,7 @@ tests = testGroup "hevm"
}
}
|]
- expr <- withSolvers Z3 1 Nothing $ \s -> getExpr s c (Just (Sig "prove_mixed_symoblic_concrete_writes(address,uint256)" [AbiAddressType, AbiUIntType 256])) [] defaultVeriOpts
+ expr <- withDefaultSolver $ \s -> getExpr s c (Just (Sig "prove_mixed_symoblic_concrete_writes(address,uint256)" [AbiAddressType, AbiUIntType 256])) [] defaultVeriOpts
let simpExpr = mapExprM Expr.decomposeStorage expr
-- putStrLnM $ T.unpack $ formatExpr (fromJust simpExpr)
assertEqualM "Decompose did not succeed." (isJust simpExpr) True
@@ -301,7 +307,7 @@ tests = testGroup "hevm"
}
}
|]
- expr <- withSolvers Z3 1 Nothing $ \s -> getExpr s c (Just (Sig "prove_array(uint256,uint256,uint256,uint256)" [AbiUIntType 256, AbiUIntType 256, AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts
+ expr <- withDefaultSolver $ \s -> getExpr s c (Just (Sig "prove_array(uint256,uint256,uint256,uint256)" [AbiUIntType 256, AbiUIntType 256, AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts
let simpExpr = mapExprM Expr.decomposeStorage expr
assertEqualM "Decompose did not succeed." (isJust simpExpr) True
, test "decompose-4-mixed" $ do
@@ -319,7 +325,7 @@ tests = testGroup "hevm"
}
}
|]
- expr <- withSolvers Z3 1 Nothing $ \s -> getExpr s c (Just (Sig "prove_array(uint256,uint256,uint256,uint256)" [AbiUIntType 256, AbiUIntType 256, AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts
+ expr <- withDefaultSolver $ \s -> getExpr s c (Just (Sig "prove_array(uint256,uint256,uint256,uint256)" [AbiUIntType 256, AbiUIntType 256, AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts
let simpExpr = mapExprM Expr.decomposeStorage expr
-- putStrLnM $ T.unpack $ formatExpr (fromJust simpExpr)
assertEqualM "Decompose did not succeed." (isJust simpExpr) True
@@ -346,7 +352,7 @@ tests = testGroup "hevm"
}
}
|]
- expr <- withSolvers Z3 1 Nothing $ \s -> getExpr s c (Just (Sig "prove_mixed(address,address,uint256)" [AbiAddressType, AbiAddressType, AbiUIntType 256])) [] defaultVeriOpts
+ expr <- withDefaultSolver $ \s -> getExpr s c (Just (Sig "prove_mixed(address,address,uint256)" [AbiAddressType, AbiAddressType, AbiUIntType 256])) [] defaultVeriOpts
let simpExpr = mapExprM Expr.decomposeStorage expr
-- putStrLnM $ T.unpack $ formatExpr (fromJust simpExpr)
assertEqualM "Decompose did not succeed." (isJust simpExpr) True
@@ -363,7 +369,7 @@ tests = testGroup "hevm"
}
}
|]
- expr <- withSolvers Z3 1 Nothing $ \s -> getExpr s c (Just (Sig "prove_mixed(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
+ expr <- withDefaultSolver $ \s -> getExpr s c (Just (Sig "prove_mixed(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
let simpExpr = mapExprM Expr.decomposeStorage expr
-- putStrLnM $ T.unpack $ formatExpr (fromJust simpExpr)
assertEqualM "Decompose did not succeed." (isJust simpExpr) True
@@ -381,7 +387,7 @@ tests = testGroup "hevm"
}
}
|]
- expr <- withSolvers Z3 1 Nothing $ \s -> getExpr s c (Just (Sig "transfer(uint256,uint256,uint256)" [AbiUIntType 256, AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts
+ expr <- withDefaultSolver $ \s -> getExpr s c (Just (Sig "transfer(uint256,uint256,uint256)" [AbiUIntType 256, AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts
assertEqualM "Expression is not clean." (badStoresInExpr expr) False
, test "simplify-storage-map-only-2" $ do
Just c <- solcRuntime "MyContract"
@@ -397,7 +403,7 @@ tests = testGroup "hevm"
}
}
|]
- expr <- withSolvers Z3 1 Nothing $ \s -> getExpr s c (Just (Sig "transfer(uint256,uint256,uint256)" [AbiUIntType 256, AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts
+ expr <- withDefaultSolver $ \s -> getExpr s c (Just (Sig "transfer(uint256,uint256,uint256)" [AbiUIntType 256, AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts
-- putStrLnM $ T.unpack $ formatExpr expr
assertEqualM "Expression is not clean." (badStoresInExpr expr) False
, test "simplify-storage-map-with-struct" $ do
@@ -418,7 +424,7 @@ tests = testGroup "hevm"
}
}
|]
- expr <- withSolvers Z3 1 Nothing $ \s -> getExpr s c (Just (Sig "transfer(uint256,uint256,uint256)" [AbiUIntType 256, AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts
+ expr <- withDefaultSolver $ \s -> getExpr s c (Just (Sig "transfer(uint256,uint256,uint256)" [AbiUIntType 256, AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts
assertEqualM "Expression is not clean." (badStoresInExpr expr) False
, test "simplify-storage-map-and-array" $ do
Just c <- solcRuntime "MyContract"
@@ -440,7 +446,7 @@ tests = testGroup "hevm"
}
}
|]
- expr <- withSolvers Z3 1 Nothing $ \s -> getExpr s c (Just (Sig "transfer(uint256,uint256,uint256)" [AbiUIntType 256, AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts
+ expr <- withDefaultSolver $ \s -> getExpr s c (Just (Sig "transfer(uint256,uint256,uint256)" [AbiUIntType 256, AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts
-- putStrLnM $ T.unpack $ formatExpr expr
assertEqualM "Expression is not clean." (badStoresInExpr expr) False
]
@@ -1050,7 +1056,7 @@ tests = testGroup "hevm"
}
}
|]
- (_, [Cex (_, ctr)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s [0x01] c (Just (Sig "fun(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
+ (_, [Cex (_, ctr)]) <- withDefaultSolver $ \s -> checkAssert s [0x01] c (Just (Sig "fun(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
assertEqualM "Must be 0" 0 $ getVar ctr "arg1"
putStrLnM $ "expected counterexample found, and it's correct: " <> (show $ getVar ctr "arg1")
,
@@ -1063,7 +1069,7 @@ tests = testGroup "hevm"
}
}
|]
- (_, [Cex (_, ctr)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s [0x11] c (Just (Sig "fun(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts
+ (_, [Cex (_, ctr)]) <- withDefaultSolver $ \s -> checkAssert s [0x11] c (Just (Sig "fun(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts
let x = getVar ctr "arg1"
let y = getVar ctr "arg2"
@@ -1080,7 +1086,7 @@ tests = testGroup "hevm"
}
}
|]
- (_, [Cex (_, ctr)]) <- withSolvers Bitwuzla 1 Nothing $ \s -> checkAssert s [0x12] c (Just (Sig "fun(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts
+ (_, [Cex (_, ctr)]) <- withSolvers Bitwuzla 1 1 Nothing $ \s -> checkAssert s [0x12] c (Just (Sig "fun(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts
assertEqualM "Division by 0 needs b=0" (getVar ctr "arg2") 0
putStrLnM "expected counterexample found"
,
@@ -1093,7 +1099,7 @@ tests = testGroup "hevm"
}
}
|]
- (_, [Cex _]) <- withSolvers Bitwuzla 1 Nothing $ \s -> checkAssert s [0x1] c Nothing [] defaultVeriOpts
+ (_, [Cex _]) <- withSolvers Bitwuzla 1 1 Nothing $ \s -> checkAssert s [0x1] c Nothing [] defaultVeriOpts
putStrLnM "expected counterexample found"
,
test "enum-conversion-fail" $ do
@@ -1106,7 +1112,7 @@ tests = testGroup "hevm"
}
}
|]
- (_, [Cex (_, ctr)]) <- withSolvers Bitwuzla 1 Nothing $ \s -> checkAssert s [0x21] c (Just (Sig "fun(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
+ (_, [Cex (_, ctr)]) <- withSolvers Bitwuzla 1 1 Nothing $ \s -> checkAssert s [0x21] c (Just (Sig "fun(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
assertBoolM "Enum is only defined for 0 and 1" $ (getVar ctr "arg1") > 1
putStrLnM "expected counterexample found"
,
@@ -1127,7 +1133,7 @@ tests = testGroup "hevm"
}
}
|]
- a <- withSolvers Z3 1 Nothing $ \s -> checkAssert s [0x31] c (Just (Sig "fun(uint8)" [AbiUIntType 8])) [] defaultVeriOpts
+ a <- withDefaultSolver $ \s -> checkAssert s [0x31] c (Just (Sig "fun(uint8)" [AbiUIntType 8])) [] defaultVeriOpts
liftIO $ do
print $ length a
print $ show a
@@ -1145,7 +1151,7 @@ tests = testGroup "hevm"
}
}
|]
- (_, [Cex (_, _)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s [0x32] c (Just (Sig "fun(uint8)" [AbiUIntType 8])) [] defaultVeriOpts
+ (_, [Cex (_, _)]) <- withDefaultSolver $ \s -> checkAssert s [0x32] c (Just (Sig "fun(uint8)" [AbiUIntType 8])) [] defaultVeriOpts
-- assertBoolM "Access must be beyond element 2" $ (getVar ctr "arg1") > 1
putStrLnM "expected counterexample found"
,
@@ -1159,7 +1165,7 @@ tests = testGroup "hevm"
}
}
|]
- (_, [Cex _]) <- withSolvers Z3 1 Nothing $ \s ->
+ (_, [Cex _]) <- withDefaultSolver $ \s ->
checkAssert s [0x41] c (Just (Sig "fun(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
putStrLnM "expected counterexample found"
,
@@ -1247,7 +1253,7 @@ tests = testGroup "hevm"
}
}
|]
- (_, [Cex (_, cex)]) <- withSolvers Z3 1 Nothing $
+ (_, [Cex (_, cex)]) <- withDefaultSolver $
\s -> checkAssert s [0x51] c (Just (Sig "fun(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
let a = fromJust $ Map.lookup (Var "arg1") cex.vars
assertEqualM "unexpected cex value" a 44
@@ -1275,7 +1281,7 @@ tests = testGroup "hevm"
}
}
|]
- withSolvers Bitwuzla 1 Nothing $ \s -> do
+ withSolvers Bitwuzla 1 1 Nothing $ \s -> do
let calldata = (WriteWord (Lit 0x0) (Var "u") (ConcreteBuf ""), [])
initVM <- liftIO $ stToIO $ abstractVM calldata initCode Nothing True
expr <- Expr.simplify <$> interpret (Fetch.oracle s Nothing) Nothing 1 StackBased initVM runExpr
@@ -1330,7 +1336,7 @@ tests = testGroup "hevm"
, OpPush (Lit 0x0)
, OpCreate
])
- withSolvers Z3 1 Nothing $ \s -> do
+ withDefaultSolver $ \s -> do
vm <- liftIO $ stToIO $ loadSymVM runtimecode (Lit 0) initCode False
expr <- Expr.simplify <$> interpret (Fetch.oracle s Nothing) Nothing 1 StackBased vm runExpr
case expr of
@@ -1414,7 +1420,7 @@ tests = testGroup "hevm"
|]
let sig = Just $ Sig "fun()" []
opts = defaultVeriOpts{ maxIter = Just 3 }
- (e, [Qed _]) <- withSolvers Z3 1 Nothing $
+ (e, [Qed _]) <- withDefaultSolver $
\s -> checkAssert s defaultPanicCodes c sig [] opts
assertBoolM "The expression is not partial" $ isPartial e
, test "concrete-loops-not-reached" $ do
@@ -1431,7 +1437,7 @@ tests = testGroup "hevm"
let sig = Just $ Sig "fun()" []
opts = defaultVeriOpts{ maxIter = Just 6 }
- (e, [Qed _]) <- withSolvers Z3 1 Nothing $
+ (e, [Qed _]) <- withDefaultSolver $
\s -> checkAssert s defaultPanicCodes c sig [] opts
assertBoolM "The expression is partial" $ not $ isPartial e
, test "symbolic-loops-reached" $ do
@@ -1445,7 +1451,7 @@ tests = testGroup "hevm"
}
}
|]
- (e, [Qed _]) <- withSolvers Z3 1 Nothing $
+ (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
, test "inconsistent-paths" $ do
@@ -1465,7 +1471,7 @@ tests = testGroup "hevm"
-- already in an inconsistent path (i == 5, j <= 3, i < j), so we
-- will continue looping here until we hit max iterations
opts = defaultVeriOpts{ maxIter = Just 10, askSmtIters = 5 }
- (e, [Qed _]) <- withSolvers Z3 1 Nothing $
+ (e, [Qed _]) <- withDefaultSolver $
\s -> checkAssert s defaultPanicCodes c sig [] opts
assertBoolM "The expression is not partial" $ Expr.containsNode isPartial e
, test "symbolic-loops-not-reached" $ do
@@ -1484,7 +1490,7 @@ 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 _]) <- withSolvers Z3 1 Nothing $
+ (e, [Qed _]) <- withDefaultSolver $
\s -> checkAssert s defaultPanicCodes c sig [] opts
assertBoolM "The expression is partial" $ not (Expr.containsNode isPartial e)
]
@@ -1504,7 +1510,7 @@ tests = testGroup "hevm"
Just a <- solcRuntime "A" src
Just c <- solcRuntime "C" src
let sig = Sig "fun(uint256)" [AbiUIntType 256]
- (expr, [Qed _]) <- withSolvers Z3 1 Nothing $ \s ->
+ (expr, [Qed _]) <- withDefaultSolver $ \s ->
verifyContract s c (Just sig) [] defaultVeriOpts Nothing Nothing
let isSuc (Success {}) = True
isSuc _ = False
@@ -1687,7 +1693,7 @@ tests = testGroup "hevm"
}
}
|]
- (_, [Cex _]) <- withSolvers Z3 1 Nothing $ \s ->
+ (_, [Cex _]) <- withDefaultSolver $ \s ->
verifyContract s c Nothing [] defaultVeriOpts Nothing (Just $ checkBadCheatCode "load(address,bytes32)")
pure ()
, test "vm.store fails for a potentially aliased address" $ do
@@ -1703,7 +1709,7 @@ tests = testGroup "hevm"
}
}
|]
- (_, [Cex _]) <- withSolvers Z3 1 Nothing $ \s ->
+ (_, [Cex _]) <- withDefaultSolver $ \s ->
verifyContract s c Nothing [] defaultVeriOpts Nothing (Just $ checkBadCheatCode "store(address,bytes32,bytes32)")
pure ()
-- TODO: make this work properly
@@ -1793,7 +1799,7 @@ tests = testGroup "hevm"
}
}
|]
- (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(int256)" [AbiIntType 256])) [] defaultVeriOpts
+ (_, [Qed _]) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(int256)" [AbiIntType 256])) [] defaultVeriOpts
putStrLnM "Require works as expected"
,
-- here test
@@ -1814,7 +1820,7 @@ tests = testGroup "hevm"
}
|]
-- should find a counterexample
- (_, [Cex _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "f(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
+ (_, [Cex _]) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "f(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
putStrLnM "expected counterexample found"
,
test "ITE-with-bitwise-OR" $ do
@@ -1832,8 +1838,22 @@ tests = testGroup "hevm"
}
}
|]
- (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "f(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
+ (_, [Qed _]) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "f(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
putStrLnM "this should always be true, due to bitwise OR with positive value"
+ ,
+ test "abstract-returndata-size" $ do
+ Just c <- solcRuntime "C"
+ [i|
+ contract C {
+ function f(uint256 x) public pure {
+ assembly {
+ return(0, x)
+ }
+ }
+ }
+ |]
+ expr <- withDefaultSolver $ \s -> getExpr s c (Just (Sig "f(uint256)" [])) [] defaultVeriOpts
+ assertBoolM "The expression is partial" $ not $ Expr.containsNode isPartial expr
,
-- CopySlice check
-- uses identity precompiled contract (0x4) to copy memory
@@ -1859,7 +1879,7 @@ tests = testGroup "hevm"
}
|]
let sig = Just (Sig "checkval(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])
- (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s ->
+ (res, [Qed _]) <- withDefaultSolver $ \s ->
checkAssert s defaultPanicCodes c sig [] defaultVeriOpts
putStrLnM $ "successfully explored: " <> show (Expr.numBranches res) <> " paths"
,
@@ -1882,7 +1902,7 @@ tests = testGroup "hevm"
}
}
|]
- (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(int256,int256,int256)" [AbiIntType 256, AbiIntType 256, AbiIntType 256])) [] defaultVeriOpts
+ (_, [Qed _]) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(int256,int256,int256)" [AbiIntType 256, AbiIntType 256, AbiIntType 256])) [] defaultVeriOpts
putStrLnM "MUL is associative"
,
-- TODO look at tests here for SAR: https://github.com/dapphub/dapptools/blob/01ef8ea418c3fe49089a44d56013d8fcc34a1ec2/src/dapp-tests/pass/constantinople.sol#L250
@@ -1900,7 +1920,7 @@ tests = testGroup "hevm"
}
}
|]
- (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(int256,int256)" [AbiIntType 256, AbiIntType 256])) [] defaultVeriOpts
+ (_, [Qed _]) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(int256,int256)" [AbiIntType 256, AbiIntType 256])) [] defaultVeriOpts
putStrLnM "SAR works as expected"
,
test "opcode-sar-pos" $ do
@@ -1917,7 +1937,7 @@ tests = testGroup "hevm"
}
}
|]
- (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(int256,int256)" [AbiIntType 256, AbiIntType 256])) [] defaultVeriOpts
+ (_, [Qed _]) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(int256,int256)" [AbiIntType 256, AbiIntType 256])) [] defaultVeriOpts
putStrLnM "SAR works as expected"
,
test "opcode-sar-fixedval-pos" $ do
@@ -1934,7 +1954,7 @@ tests = testGroup "hevm"
}
}
|]
- (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(int256,int256)" [AbiIntType 256, AbiIntType 256])) [] defaultVeriOpts
+ (_, [Qed _]) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(int256,int256)" [AbiIntType 256, AbiIntType 256])) [] defaultVeriOpts
putStrLnM "SAR works as expected"
,
test "opcode-sar-fixedval-neg" $ do
@@ -1951,7 +1971,7 @@ tests = testGroup "hevm"
}
}
|]
- (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(int256,int256)" [AbiIntType 256, AbiIntType 256])) [] defaultVeriOpts
+ (_, [Qed _]) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(int256,int256)" [AbiIntType 256, AbiIntType 256])) [] defaultVeriOpts
putStrLnM "SAR works as expected"
,
test "opcode-div-zero-1" $ do
@@ -1968,7 +1988,7 @@ tests = testGroup "hevm"
}
}
|]
- (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
+ (_, [Qed _]) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
putStrLnM "sdiv works as expected"
,
test "opcode-sdiv-zero-1" $ do
@@ -1985,7 +2005,7 @@ tests = testGroup "hevm"
}
}
|]
- (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
+ (_, [Qed _]) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
putStrLnM "sdiv works as expected"
,
test "opcode-sdiv-zero-2" $ do
@@ -2002,7 +2022,7 @@ tests = testGroup "hevm"
}
}
|]
- (_, [Qed _]) <- withSolvers CVC5 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
+ (_, [Qed _]) <- withCVC5Solver $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
putStrLnM "sdiv works as expected"
,
test "signed-overflow-checks" $ do
@@ -2014,7 +2034,7 @@ tests = testGroup "hevm"
}
}
|]
- (_, [Cex (_, _)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s [0x11] c (Just (Sig "fun(int256)" [AbiIntType 256])) [] defaultVeriOpts
+ (_, [Cex (_, _)]) <- withDefaultSolver $ \s -> checkAssert s [0x11] c (Just (Sig "fun(int256)" [AbiIntType 256])) [] defaultVeriOpts
putStrLnM "expected cex discovered"
,
test "opcode-signextend-neg" $ do
@@ -2036,7 +2056,7 @@ tests = testGroup "hevm"
}
}
|]
- (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "foo(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
+ (_, [Qed _]) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "foo(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
putStrLnM "signextend works as expected"
,
test "opcode-signextend-pos-nochop" $ do
@@ -2054,7 +2074,7 @@ tests = testGroup "hevm"
}
}
|]
- (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256,uint8)" [AbiUIntType 256, AbiUIntType 8])) [] defaultVeriOpts
+ (_, [Qed _]) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256,uint8)" [AbiUIntType 256, AbiUIntType 8])) [] defaultVeriOpts
putStrLnM "signextend works as expected"
,
test "opcode-signextend-pos-chopped" $ do
@@ -2072,7 +2092,7 @@ tests = testGroup "hevm"
}
}
|]
- (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256,uint8)" [AbiUIntType 256, AbiUIntType 8])) [] defaultVeriOpts
+ (_, [Qed _]) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256,uint8)" [AbiUIntType 256, AbiUIntType 8])) [] defaultVeriOpts
putStrLnM "signextend works as expected"
,
-- when b is too large, value is unchanged
@@ -2090,7 +2110,7 @@ tests = testGroup "hevm"
}
}
|]
- (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256,uint8)" [AbiUIntType 256, AbiUIntType 8])) [] defaultVeriOpts
+ (_, [Qed _]) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256,uint8)" [AbiUIntType 256, AbiUIntType 8])) [] defaultVeriOpts
putStrLnM "signextend works as expected"
,
test "opcode-shl" $ do
@@ -2108,7 +2128,7 @@ tests = testGroup "hevm"
}
}
|]
- (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts
+ (_, [Qed _]) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts
putStrLnM "SAR works as expected"
,
test "opcode-xor-cancel" $ do
@@ -2125,7 +2145,7 @@ tests = testGroup "hevm"
}
}
|]
- (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts
+ (_, [Qed _]) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts
putStrLnM "XOR works as expected"
,
test "opcode-xor-reimplement" $ do
@@ -2141,7 +2161,7 @@ tests = testGroup "hevm"
}
}
|]
- (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts
+ (_, [Qed _]) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts
putStrLnM "XOR works as expected"
,
test "opcode-add-commutative" $ do
@@ -2159,7 +2179,7 @@ tests = testGroup "hevm"
}
}
|]
- a <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts
+ a <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts
case a of
(_, [Cex (_, ctr)]) -> do
let x = getVar ctr "arg1"
@@ -2185,7 +2205,7 @@ tests = testGroup "hevm"
}
}
|]
- (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint16)" [AbiUIntType 16])) [] defaultVeriOpts
+ (_, [Qed _]) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint16)" [AbiUIntType 16])) [] defaultVeriOpts
putStrLnM "DIV by zero is zero"
,
-- Somewhat tautological since we are asserting the precondition
@@ -2213,7 +2233,7 @@ tests = testGroup "hevm"
Success _ _ b _ -> (ReadWord (Lit 0) b) .== (Add x y)
_ -> PBool True
sig = Just (Sig "add(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])
- (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s ->
+ (res, [Qed _]) <- withDefaultSolver $ \s ->
verifyContract s safeAdd sig [] defaultVeriOpts (Just pre) (Just post)
putStrLnM $ "successfully explored: " <> show (Expr.numBranches res) <> " paths"
,
@@ -2240,7 +2260,7 @@ tests = testGroup "hevm"
in case leaf of
Success _ _ b _ -> (ReadWord (Lit 0) b) .== (Mul (Lit 2) y)
_ -> PBool True
- (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s ->
+ (res, [Qed _]) <- withDefaultSolver $ \s ->
verifyContract s safeAdd (Just (Sig "add(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts (Just pre) (Just post)
putStrLnM $ "successfully explored: " <> show (Expr.numBranches res) <> " paths"
,
@@ -2271,7 +2291,7 @@ tests = testGroup "hevm"
in Expr.add prex (Expr.mul (Lit 2) y) .== (Expr.readStorage' (Lit 0) poststore)
_ -> PBool True
sig = Just (Sig "f(uint256)" [AbiUIntType 256])
- (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s ->
+ (res, [Qed _]) <- withDefaultSolver $ \s ->
verifyContract s c sig [] defaultVeriOpts (Just pre) (Just post)
putStrLnM $ "successfully explored: " <> show (Expr.numBranches res) <> " paths"
,
@@ -2297,7 +2317,7 @@ tests = testGroup "hevm"
}
|]
Just c <- liftIO $ yulRuntime "Neg" src
- (res, [Qed _]) <- withSolvers Z3 4 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "hello(address)" [AbiAddressType])) [] defaultVeriOpts
+ (res, [Qed _]) <- withSolvers Z3 4 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "hello(address)" [AbiAddressType])) [] defaultVeriOpts
putStrLnM $ "successfully explored: " <> show (Expr.numBranches res) <> " paths"
,
test "catch-storage-collisions-noproblem" $ do
@@ -2333,7 +2353,7 @@ tests = testGroup "hevm"
in Expr.add prex prey .== Expr.add postx posty
_ -> PBool True
sig = Just (Sig "f(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])
- (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s ->
+ (_, [Qed _]) <- withDefaultSolver $ \s ->
verifyContract s c sig [] defaultVeriOpts (Just pre) (Just post)
putStrLnM "Correct, this can never fail"
,
@@ -2370,7 +2390,7 @@ tests = testGroup "hevm"
in Expr.add prex prey .== Expr.add postx posty
_ -> PBool True
sig = Just (Sig "f(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])
- (_, [Cex (_, ctr)]) <- withSolvers Z3 1 Nothing $ \s ->
+ (_, [Cex (_, ctr)]) <- withDefaultSolver $ \s ->
verifyContract s c sig [] defaultVeriOpts (Just pre) (Just post)
let x = getVar ctr "arg1"
let y = getVar ctr "arg2"
@@ -2388,7 +2408,7 @@ tests = testGroup "hevm"
}
}
|]
- (_, [Cex (Failure _ _ (Revert msg), _)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "foo()" [])) [] defaultVeriOpts
+ (_, [Cex (Failure _ _ (Revert msg), _)]) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "foo()" [])) [] defaultVeriOpts
assertEqualM "incorrect revert msg" msg (ConcreteBuf $ panicMsg 0x01)
,
test "simple-assert-2" $ do
@@ -2400,7 +2420,7 @@ tests = testGroup "hevm"
}
}
|]
- (_, [(Cex (_, ctr))]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "foo(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
+ (_, [(Cex (_, ctr))]) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "foo(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
assertEqualM "Must be 10" 10 $ getVar ctr "arg1"
putStrLnM "Got 10 Cex, as expected"
,
@@ -2414,7 +2434,7 @@ tests = testGroup "hevm"
}
}
|]
- (_, [Cex (_, a), Cex (_, b)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
+ (_, [Cex (_, a), Cex (_, b)]) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
let ints = map (flip getVar "arg1") [a,b]
assertBoolM "0 must be one of the Cex-es" $ isJust $ List.elemIndex 0 ints
putStrLnM "expected 2 counterexamples found, one Cex is the 0 value"
@@ -2429,7 +2449,7 @@ tests = testGroup "hevm"
}
}
|]
- (_, [Cex (_, a), Cex (_, b)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
+ (_, [Cex (_, a), Cex (_, b)]) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
let x = getVar a "arg1"
let y = getVar b "arg1"
assertBoolM "At least one has to be 0, to go through the first assert" (x == 0 || y == 0)
@@ -2445,7 +2465,7 @@ tests = testGroup "hevm"
}
}
|]
- (_, [Cex _, Cex _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts
+ (_, [Cex _, Cex _]) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts
putStrLnM "expected 2 counterexamples found"
,
test "assert-2nd-arg" $ do
@@ -2457,7 +2477,7 @@ tests = testGroup "hevm"
}
}
|]
- (_, [Cex (_, ctr)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts
+ (_, [Cex (_, ctr)]) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts
assertEqualM "Must be 666" 666 $ getVar ctr "arg2"
putStrLnM "Found arg2 Ctx to be 666"
,
@@ -2474,7 +2494,7 @@ tests = testGroup "hevm"
}
}
|]
- (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "foo(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
+ (res, [Qed _]) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "foo(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
putStrLnM $ "successfully explored: " <> show (Expr.numBranches res) <> " paths"
,
-- We zero out everything but the LSB byte. However, byte(31,x) takes the LSB byte
@@ -2491,7 +2511,7 @@ tests = testGroup "hevm"
}
}
|]
- (_, [Cex (_, ctr)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "foo(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
+ (_, [Cex (_, ctr)]) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "foo(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
assertBoolM "last byte must be non-zero" $ ((Data.Bits..&.) (getVar ctr "arg1") 0xff) > 0
putStrLnM "Expected counterexample found"
,
@@ -2509,7 +2529,7 @@ tests = testGroup "hevm"
}
}
|]
- (_, [Cex (_, ctr)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "foo(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
+ (_, [Cex (_, ctr)]) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "foo(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
assertBoolM "second to last byte must be non-zero" $ ((Data.Bits..&.) (getVar ctr "arg1") 0xff00) > 0
putStrLnM "Expected counterexample found"
,
@@ -2528,7 +2548,7 @@ tests = testGroup "hevm"
}
}
|]
- (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "foo(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
+ (res, [Qed _]) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "foo(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
putStrLnM $ "successfully explored: " <> show (Expr.numBranches res) <> " paths"
,
-- Bitwise OR operation test
@@ -2544,7 +2564,7 @@ tests = testGroup "hevm"
}
}
|]
- (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "foo(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
+ (_, [Qed _]) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "foo(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
putStrLnM "When OR-ing with full 1's we should get back full 1's"
,
-- Bitwise OR operation test
@@ -2561,7 +2581,7 @@ tests = testGroup "hevm"
}
}
|]
- (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "foo(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
+ (_, [Qed _]) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "foo(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
putStrLnM "When OR-ing with a byte of 1's, we should get 1's back there"
,
test "Deposit contract loop (z3)" $ do
@@ -2583,7 +2603,7 @@ tests = testGroup "hevm"
}
}
|]
- (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "deposit(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
+ (res, [Qed _]) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "deposit(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
putStrLnM $ "successfully explored: " <> show (Expr.numBranches res) <> " paths"
,
test "Deposit-contract-loop-error-version" $ do
@@ -2605,7 +2625,7 @@ tests = testGroup "hevm"
}
}
|]
- (_, [Cex (_, ctr)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s allPanicCodes c (Just (Sig "deposit(uint8)" [AbiUIntType 8])) [] defaultVeriOpts
+ (_, [Cex (_, ctr)]) <- withDefaultSolver $ \s -> checkAssert s allPanicCodes c (Just (Sig "deposit(uint8)" [AbiUIntType 8])) [] defaultVeriOpts
assertEqualM "Must be 255" 255 $ getVar ctr "arg1"
putStrLnM $ "expected counterexample found, and it's correct: " <> (show $ getVar ctr "arg1")
,
@@ -2618,7 +2638,7 @@ tests = testGroup "hevm"
}
}
|]
- (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts
+ (res, [Qed _]) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts
putStrLnM $ "successfully explored: " <> show (Expr.numBranches res) <> " paths"
,
test "check-asm-byte-in-bounds" $ do
@@ -2637,7 +2657,7 @@ tests = testGroup "hevm"
}
}
|]
- (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts
+ (_, [Qed _]) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts
putStrLnM "in bounds byte reads return the expected value"
,
test "check-div-mod-sdiv-smod-by-zero-constant-prop" $ do
@@ -2667,7 +2687,7 @@ tests = testGroup "hevm"
}
}
|]
- (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "foo(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
+ (_, [Qed _]) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "foo(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
putStrLnM "div/mod/sdiv/smod by zero works as expected during constant propagation"
,
test "check-asm-byte-oob" $ do
@@ -2682,7 +2702,7 @@ tests = testGroup "hevm"
}
}
|]
- (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts
+ (_, [Qed _]) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts
putStrLnM "oob byte reads always return 0"
,
test "injectivity of keccak (diff sizes)" $ do
@@ -2709,7 +2729,7 @@ tests = testGroup "hevm"
}
}
|]
- (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "f(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts
+ (res, [Qed _]) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "f(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts
putStrLnM $ "successfully explored: " <> show (Expr.numBranches res) <> " paths"
,
test "injectivity of keccak contrapositive (32 bytes)" $ do
@@ -2722,7 +2742,7 @@ tests = testGroup "hevm"
}
}
|]
- (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "f(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts
+ (res, [Qed _]) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "f(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts
putStrLnM $ "successfully explored: " <> show (Expr.numBranches res) <> " paths"
,
test "injectivity of keccak (64 bytes)" $ do
@@ -2734,7 +2754,7 @@ tests = testGroup "hevm"
}
}
|]
- (_, [Cex (_, ctr)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "f(uint256,uint256,uint256,uint256)" (replicate 4 (AbiUIntType 256)))) [] defaultVeriOpts
+ (_, [Cex (_, ctr)]) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "f(uint256,uint256,uint256,uint256)" (replicate 4 (AbiUIntType 256)))) [] defaultVeriOpts
let x = getVar ctr "arg1"
let y = getVar ctr "arg2"
let w = getVar ctr "arg3"
@@ -2757,7 +2777,7 @@ tests = testGroup "hevm"
}
}
|]
- (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts
+ (res, [Qed _]) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts
putStrLnM $ "successfully explored: " <> show (Expr.numBranches res) <> " paths"
,
test "calldata beyond calldatasize is 0 (concrete dalldata prefix)" $ do
@@ -2774,7 +2794,7 @@ tests = testGroup "hevm"
}
}
|]
- (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "f(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
+ (res, [Qed _]) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "f(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
putStrLnM $ "successfully explored: " <> show (Expr.numBranches res) <> " paths"
,
test "calldata symbolic access" $ do
@@ -2794,7 +2814,7 @@ tests = testGroup "hevm"
}
}
|]
- (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "f(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
+ (res, [Qed _]) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "f(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
putStrLnM $ "successfully explored: " <> show (Expr.numBranches res) <> " paths"
,
test "multiple-contracts" $ do
@@ -2817,7 +2837,7 @@ tests = testGroup "hevm"
cAddr = SymAddr "entrypoint"
Just c <- solcRuntime "C" code
Just a <- solcRuntime "A" code
- (_, [Cex (_, cex)]) <- withSolvers Z3 1 Nothing $ \s -> do
+ (_, [Cex (_, cex)]) <- withDefaultSolver $ \s -> do
vm <- liftIO $ stToIO $ abstractVM (mkCalldata (Just (Sig "call_A()" [])) []) c Nothing False
<&> set (#state % #callvalue) (Lit 0)
<&> over (#env % #contracts)
@@ -2851,7 +2871,7 @@ tests = testGroup "hevm"
uint public x;
}
|]
- (_, [Cex _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "call_A()" [])) [] defaultVeriOpts
+ (_, [Cex _]) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "call_A()" [])) [] defaultVeriOpts
putStrLnM "expected counterexample found"
,
test "keccak-concrete-and-sym-agree" $ do
@@ -2865,7 +2885,7 @@ tests = testGroup "hevm"
}
}
|]
- (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "kecc(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
+ (res, [Qed _]) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "kecc(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
putStrLnM $ "successfully explored: " <> show (Expr.numBranches res) <> " paths"
,
test "keccak-concrete-and-sym-agree-nonzero" $ do
@@ -2880,7 +2900,7 @@ tests = testGroup "hevm"
}
}
|]
- (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "kecc(uint256)" [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts
+ (res, [Qed _]) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "kecc(uint256)" [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts
putStrLnM $ "successfully explored: " <> show (Expr.numBranches res) <> " paths"
,
test "keccak concrete and sym injectivity" $ do
@@ -2892,13 +2912,13 @@ tests = testGroup "hevm"
}
}
|]
- (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "f(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
+ (res, [Qed _]) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "f(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
putStrLnM $ "successfully explored: " <> show (Expr.numBranches res) <> " paths"
,
test "safemath-distributivity-yul" $ do
let yulsafeDistributivity = hex "6355a79a6260003560e01c14156016576015601f565b5b60006000fd60a1565b603d602d604435600435607c565b6039602435600435607c565b605d565b6052604b604435602435605d565b600435607c565b141515605a57fe5b5b565b6000828201821115151560705760006000fd5b82820190505b92915050565b6000818384048302146000841417151560955760006000fd5b82820290505b92915050565b"
vm <- liftIO $ stToIO $ abstractVM (mkCalldata (Just (Sig "distributivity(uint256,uint256,uint256)" [AbiUIntType 256, AbiUIntType 256, AbiUIntType 256])) []) yulsafeDistributivity Nothing False
- (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> verify s defaultVeriOpts vm (Just $ checkAssertions defaultPanicCodes)
+ (_, [Qed _]) <- withDefaultSolver $ \s -> verify s defaultVeriOpts vm (Just $ checkAssertions defaultPanicCodes)
putStrLnM "Proven"
,
test "safemath-distributivity-sol" $ do
@@ -2923,7 +2943,7 @@ tests = testGroup "hevm"
}
|]
- (_, [Qed _]) <- withSolvers Bitwuzla 1 (Just 99999999) $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "distributivity(uint256,uint256,uint256)" [AbiUIntType 256, AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts
+ (_, [Qed _]) <- withSolvers Bitwuzla 1 1 (Just 99999999) $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "distributivity(uint256,uint256,uint256)" [AbiUIntType 256, AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts
putStrLnM "Proven"
,
test "storage-cex-1" $ do
@@ -2939,7 +2959,7 @@ tests = testGroup "hevm"
}
}
|]
- (_, [(Cex (_, cex))]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s [0x01] c (Just (Sig "fun(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
+ (_, [(Cex (_, cex))]) <- withDefaultSolver $ \s -> checkAssert s [0x01] c (Just (Sig "fun(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
let addr = SymAddr "entrypoint"
testCex = Map.size cex.store == 1 &&
case Map.lookup addr cex.store of
@@ -2962,7 +2982,7 @@ tests = testGroup "hevm"
}
}
|]
- (_, [(Cex (_, cex))]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s [0x01] c (Just (Sig "fun(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
+ (_, [(Cex (_, cex))]) <- withDefaultSolver $ \s -> checkAssert s [0x01] c (Just (Sig "fun(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
let addr = SymAddr "entrypoint"
a = getVar cex "arg1"
testCex = Map.size cex.store == 1 &&
@@ -2989,7 +3009,7 @@ tests = testGroup "hevm"
}
|]
let sig = Just (Sig "fun(uint256)" [AbiUIntType 256])
- (_, [Cex (_, cex)]) <- withSolvers Z3 1 Nothing $
+ (_, [Cex (_, cex)]) <- withDefaultSolver $
\s -> verifyContract s c sig [] defaultVeriOpts Nothing (Just $ checkAssertions [0x01])
let addr = SymAddr "entrypoint"
testCex = Map.size cex.store == 1 &&
@@ -3022,7 +3042,7 @@ tests = testGroup "hevm"
}
|]
let sig = (Just (Sig "stuff(address)" [AbiAddressType]))
- (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c sig [] defaultVeriOpts
+ (_, [Qed _]) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c sig [] defaultVeriOpts
putStrLnM $ "Basic tstore check passed"
]
, testGroup "concr-fuzz"
@@ -3042,7 +3062,7 @@ tests = testGroup "hevm"
}
|]
let sig = (Sig "complicated(uint256,uint256,uint256)" [AbiUIntType 256, AbiUIntType 256, AbiUIntType 256])
- (_, [Cex (_, ctr)]) <- withSolvers CVC5 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just sig) [] defaultVeriOpts
+ (_, [Cex (_, ctr)]) <- withCVC5Solver $ \s -> checkAssert s defaultPanicCodes c (Just sig) [] defaultVeriOpts
let
x = getVar ctr "arg1"
y = getVar ctr "arg2"
@@ -3064,7 +3084,7 @@ tests = testGroup "hevm"
}
|]
let sig = (Sig "func()" [])
- (_, [Cex (_, ctr)]) <- withSolvers CVC5 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just sig) [] defaultVeriOpts
+ (_, [Cex (_, ctr)]) <- withCVC5Solver $ \s -> checkAssert s defaultPanicCodes c (Just sig) [] defaultVeriOpts
putStrLnM $ "expected counterexample found. ctr: " <> (show ctr)
, testFuzz "fuzz-simple-fixed-value" $ do
Just c <- solcRuntime "MyContract"
@@ -3077,7 +3097,7 @@ tests = testGroup "hevm"
}
|]
let sig = (Sig "func(uint256)" [AbiUIntType 256])
- (_, [Cex (_, ctr)]) <- withSolvers CVC5 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just sig) [] defaultVeriOpts
+ (_, [Cex (_, ctr)]) <- withCVC5Solver $ \s -> checkAssert s defaultPanicCodes c (Just sig) [] defaultVeriOpts
putStrLnM $ "expected counterexample found. ctr: " <> (show ctr)
, testFuzz "fuzz-simple-fixed-value2" $ do
Just c <- solcRuntime "MyContract"
@@ -3089,7 +3109,7 @@ tests = testGroup "hevm"
}
|]
let sig = (Sig "func(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])
- (_, [Cex (_, ctr)]) <- withSolvers CVC5 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just sig) [] defaultVeriOpts
+ (_, [Cex (_, ctr)]) <- withCVC5Solver $ \s -> checkAssert s defaultPanicCodes c (Just sig) [] defaultVeriOpts
putStrLnM $ "expected counterexample found. ctr: " <> (show ctr)
, testFuzz "fuzz-simple-fixed-value3" $ do
Just c <- solcRuntime "MyContract"
@@ -3101,7 +3121,7 @@ tests = testGroup "hevm"
}
|]
let sig = (Sig "func(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])
- (_, [Cex (_, ctr1), Cex (_, ctr2)]) <- withSolvers Bitwuzla 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just sig) [] defaultVeriOpts
+ (_, [Cex (_, ctr1), Cex (_, ctr2)]) <- withSolvers Bitwuzla 1 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just sig) [] defaultVeriOpts
putStrLnM $ "expected counterexamples found. ctr1: " <> (show ctr1) <> " ctr2: " <> (show ctr2)
, testFuzz "fuzz-simple-fixed-value-store1" $ do
Just c <- solcRuntime "MyContract"
@@ -3115,7 +3135,7 @@ tests = testGroup "hevm"
}
|]
let sig = (Sig "func(uint256)" [AbiUIntType 256, AbiUIntType 256])
- (_, [Cex _]) <- withSolvers CVC5 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just sig) [] defaultVeriOpts
+ (_, [Cex _]) <- withCVC5Solver $ \s -> checkAssert s defaultPanicCodes c (Just sig) [] defaultVeriOpts
putStrLnM $ "expected counterexamples found"
, testFuzz "fuzz-simple-fixed-value-store2" $ do
Just c <- solcRuntime "MyContract"
@@ -3129,7 +3149,7 @@ tests = testGroup "hevm"
}
|]
let sig = (Sig "func(uint256)" [AbiUIntType 256, AbiUIntType 256])
- (_, [Cex (_, ctr1)]) <- withSolvers CVC5 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just sig) [] defaultVeriOpts
+ (_, [Cex (_, ctr1)]) <- withCVC5Solver $ \s -> checkAssert s defaultPanicCodes c (Just sig) [] defaultVeriOpts
putStrLnM $ "expected counterexamples found: " <> show ctr1
]
, testGroup "simplification-working"
@@ -3221,7 +3241,7 @@ tests = testGroup "hevm"
default { invalid() }
}
|]
- withSolvers Z3 3 Nothing $ \s -> do
+ withSolvers Z3 3 1 Nothing $ \s -> do
a <- equivalenceCheck s aPrgm bPrgm defaultVeriOpts (mkCalldata Nothing [])
assertBoolM "Must have a difference" (any isCex a)
,
@@ -3246,7 +3266,7 @@ tests = testGroup "hevm"
}
}
|]
- withSolvers Z3 3 Nothing $ \s -> do
+ withSolvers Z3 3 1 Nothing $ \s -> do
a <- equivalenceCheck s aPrgm bPrgm defaultVeriOpts (mkCalldata Nothing [])
assertEqualM "Must have no difference" [Qed ()] a
,
@@ -3277,7 +3297,7 @@ tests = testGroup "hevm"
}
}
|]
- withSolvers Z3 3 Nothing $ \s -> do
+ withSolvers Z3 3 1 Nothing $ \s -> do
a <- equivalenceCheck s aPrgm bPrgm defaultVeriOpts (mkCalldata Nothing [])
assertBoolM "Must differ" (all isCex a)
,
@@ -3338,7 +3358,7 @@ tests = testGroup "hevm"
}
}
|]
- withSolvers Z3 3 Nothing $ \s -> do
+ withSolvers Z3 3 1 Nothing $ \s -> do
a <- equivalenceCheck s aPrgm bPrgm defaultVeriOpts (mkCalldata Nothing [])
assertBoolM "Must differ" (all isCex a)
,
@@ -3361,7 +3381,7 @@ tests = testGroup "hevm"
}
}
|]
- withSolvers Z3 3 Nothing $ \s -> do
+ withSolvers Z3 3 1 Nothing $ \s -> do
let cd = mkCalldata (Just (Sig "a(address,address)" [AbiAddressType, AbiAddressType])) []
a <- equivalenceCheck s aPrgm bPrgm defaultVeriOpts cd
assertEqualM "Must be different" (any isCex a) True
@@ -3387,7 +3407,7 @@ tests = testGroup "hevm"
}
}
|]
- withSolvers Bitwuzla 3 Nothing $ \s -> do
+ withSolvers Bitwuzla 3 1 Nothing $ \s -> do
a <- equivalenceCheck s aPrgm bPrgm defaultVeriOpts (mkCalldata Nothing [])
assertEqualM "Must be different" (any isCex a) True
, test "eq-all-yul-optimization-tests" $ do
@@ -3596,7 +3616,7 @@ tests = testGroup "hevm"
Just aPrgm <- liftIO $ yul "" $ T.pack $ unlines filteredASym
Just bPrgm <- liftIO $ yul "" $ T.pack $ unlines filteredBSym
procs <- liftIO $ getNumProcessors
- withSolvers CVC5 (unsafeInto procs) (Just 100) $ \s -> do
+ withSolvers CVC5 (unsafeInto procs) 1 (Just 100) $ \s -> do
res <- equivalenceCheck s aPrgm bPrgm opts (mkCalldata Nothing [])
end <- liftIO $ getCurrentTime
case any isCex res of
@@ -3646,7 +3666,7 @@ checkEquivAndLHS orig simp = do
checkEquivBase :: (Eq a, App m) => (a -> a -> Prop) -> a -> a -> Bool -> m (Maybe Bool)
checkEquivBase mkprop l r expect = do
conf <- readConfig
- withSolvers Z3 1 (Just 1) $ \solvers -> liftIO $ do
+ withSolvers Z3 1 1 (Just 1) $ \solvers -> liftIO $ do
let smt = assertPropsNoSimp conf [mkprop l r]
res <- checkSat solvers smt
let
@@ -4402,7 +4422,7 @@ reachableUserAsserts = checkPost (Just $ checkAssertions [0x01])
checkPost :: App m => Maybe (Postcondition RealWorld) -> ByteString -> Maybe Sig -> m (Either [SMTCex] (Expr End))
checkPost post c sig = do
- (e, res) <- withSolvers Z3 1 Nothing $ \s ->
+ (e, res) <- withDefaultSolver $ \s ->
verifyContract s c sig [] defaultVeriOpts Nothing post
let cexs = snd <$> mapMaybe getCex res
case cexs of