From 680bcb41a204978ce9deb235ddd1a507781282bf Mon Sep 17 00:00:00 2001 From: Gustavo Grieco <31542053+ggrieco-tob@users.noreply.github.com> Date: Mon, 21 Mar 2022 13:39:37 +0100 Subject: [PATCH] Dapp mode fuzzing support (#733) * preliminary code for foundry fuzz test support * added call to setUp * added some tests, that needed to be fixed * added missing file, fixed tests and some optimization * fix solc version * fix * show an error if setUp reverts * fix hlint issues * fixed and reorganized tests * renamed test mode --- lib/Echidna/Exec.hs | 6 +- lib/Echidna/Solidity.hs | 39 +++++++--- lib/Echidna/Test.hs | 44 +++++++++-- lib/Echidna/Transaction.hs | 4 +- lib/Echidna/Types/Solidity.hs | 2 + lib/Echidna/Types/Test.hs | 12 +-- lib/Echidna/UI/Report.hs | 2 +- lib/Echidna/UI/Widgets.hs | 2 +- src/test/Common.hs | 10 +-- src/test/Spec.hs | 3 +- src/test/Tests/Dapptest.hs | 22 ++++++ src/test/Tests/Research.hs | 6 +- tests/solidity/dapptest/basic.sol | 91 ++++++++++++++++++++++ tests/solidity/dapptest/config.yaml | 4 + tests/solidity/research/ilf_crowdsale.yaml | 1 - 15 files changed, 208 insertions(+), 40 deletions(-) create mode 100644 src/test/Tests/Dapptest.hs create mode 100644 tests/solidity/dapptest/basic.sol create mode 100644 tests/solidity/dapptest/config.yaml diff --git a/lib/Echidna/Exec.hs b/lib/Echidna/Exec.hs index ad8100f4..070c9bcb 100644 --- a/lib/Echidna/Exec.hs +++ b/lib/Echidna/Exec.hs @@ -123,14 +123,16 @@ handleErrorsAndConstruction onErr vmResult' vmBeforeTx tx' = case (vmResult', tx (Reversion, _) -> do tracesBeforeVMReset <- use $ hasLens . traces codeContractBeforeVMReset <- use $ hasLens . state . codeContract - calldataBeforeReset <- use $ hasLens . state . calldata + calldataBeforeVMReset <- use $ hasLens . state . calldata + callvalueBeforeVMReset <- use $ hasLens . state . callvalue -- If a transaction reverts reset VM to state before the transaction. hasLens .= vmBeforeTx -- Undo reset of some of the VM state. -- Otherwise we'd loose all information about the reverted transaction like -- contract address, calldata, result and traces. hasLens . result ?= vmResult' - hasLens . state . calldata .= calldataBeforeReset + hasLens . state . calldata .= calldataBeforeVMReset + hasLens . state . callvalue .= callvalueBeforeVMReset hasLens . traces .= tracesBeforeVMReset hasLens . state . codeContract .= codeContractBeforeVMReset (VMFailure x, _) -> onErr x diff --git a/lib/Echidna/Solidity.hs b/lib/Echidna/Solidity.hs index 97ed4f80..5bd97e75 100644 --- a/lib/Echidna/Solidity.hs +++ b/lib/Echidna/Solidity.hs @@ -28,11 +28,11 @@ import System.FilePath.Posix (()) import Echidna.ABI (encodeSig, encodeSigWithName, hashSig, fallback, commonTypeSizes, mkValidAbiInt, mkValidAbiUInt) import Echidna.Exec (execTx, initialVM) import Echidna.Events (EventMap) -import Echidna.Test (createTests, isAssertionMode, isPropertyMode) +import Echidna.Test (createTests, isAssertionMode, isPropertyMode, isDapptestMode) import Echidna.RPC (loadEthenoBatch) import Echidna.Types.Solidity import Echidna.Types.Signature (ContractName, FunctionHash, SolSignature, SignatureMap, getBytecodeMetadata) -import Echidna.Types.Tx (TxConf, createTxWithValue, unlimitedGasPerBlock, initialTimestamp, initialBlockNumber) +import Echidna.Types.Tx (TxConf, basicTx, createTxWithValue, unlimitedGasPerBlock, initialTimestamp, initialBlockNumber) import Echidna.Types.Test (TestConf(..), EchidnaTest(..)) import Echidna.Types.World (World(..)) import Echidna.Fetch (deployContracts) @@ -134,6 +134,7 @@ linkLibraries [] = "" linkLibraries ls = "--libraries " ++ iconcatMap (\i x -> concat [x, ":", show $ addrLibrary + toEnum i, ","]) ls +-- | Filter methods using a whitelist/blacklist filterMethods :: Text -> Filter -> NE.NonEmpty SolSignature -> NE.NonEmpty SolSignature filterMethods _ f@(Whitelist []) _ = error $ show $ InvalidMethodFilters f filterMethods cn f@(Whitelist ic) ms = case NE.filter (\s -> encodeSigWithName cn s `elem` ic) ms of @@ -143,6 +144,12 @@ filterMethods cn f@(Blacklist ig) ms = case NE.filter (\s -> encodeSigWithName c [] -> error $ show $ InvalidMethodFilters f fs -> NE.fromList fs +-- | Filter methods with arguments, used for dapptest mode +filterMethodsWithArgs :: NE.NonEmpty SolSignature -> NE.NonEmpty SolSignature +filterMethodsWithArgs ms = case NE.filter (\(_, xs) -> not $ null xs) ms of + [] -> error "No dapptest tests found" + fs -> NE.fromList fs + abiOf :: Text -> SolcContract -> NE.NonEmpty SolSignature abiOf pref cc = fallback NE.:| filter (not . isPrefixOf pref . fst) (elems (cc ^. abiMap) <&> \m -> (m ^. methodName, m ^.. methodInputs . traverse . _2)) @@ -174,14 +181,14 @@ loadSpecified name cs = do -- Filter ABI according to the config options - let fabiOfc = filterMethods (c ^. contractName) fs $ abiOf pref c - -- Filter again for assertions checking if enabled + let fabiOfc = if isDapptestMode tm then filterMethodsWithArgs (abiOf pref c) else filterMethods (c ^. contractName) fs $ abiOf pref c + -- Filter again for dapptest tests or assertions checking if enabled let neFuns = filterMethods (c ^. contractName) fs (fallback NE.:| funs) - -- Construct ABI mapping for World let abiMapping = if ma then M.fromList $ cs <&> \cc -> (getBytecodeMetadata $ cc ^. runtimeCode, filterMethods (cc ^. contractName) fs $ abiOf pref cc) else M.singleton (getBytecodeMetadata $ c ^. runtimeCode) fabiOfc + -- Set up initial VM, either with chosen contract or Etheno initialization file -- need to use snd to add to ABI dict blank' <- maybe (pure (initialVM & block . gaslimit .~ fromInteger unlimitedGasPerBlock & block . maxCodeSize .~ w256 (fromInteger mcs))) @@ -201,23 +208,31 @@ loadSpecified name cs = do Just (t,_) -> throwM $ TestArgsFound t -- Test args check Nothing -> do -- library deployment - vm <- deployContracts (zip [addrLibrary ..] ls) d blank + vm0 <- deployContracts (zip [addrLibrary ..] ls) d blank -- additional contracts deployment --(ctd, _) <- if null atd then return ([], []) else contracts $ NE.fromList $ map show atd --let mainContract = head $ map (\x -> head $ T.splitOn "." $ last $ T.splitOn "-" $ head $ T.splitOn ":" (view contractName x)) ctd --let ctd' = filter (\x -> (last $ T.splitOn ":" (view contractName x)) == mainContract) ctd --vm' <- deployContracts (zip atd ctd') ca vm -- main contract deployment - let transaction = execTx $ createTxWithValue bc d ca (fromInteger unlimitedGasPerBlock) (w256 $ fromInteger balc) (0, 0) - vm'' <- execStateT transaction vm - case currentContract vm'' of - Just _ -> return (vm'', unions $ map (view eventMap) cs, neFuns, fst <$> tests, abiMapping) - Nothing -> throwM $ DeploymentFailed ca + let deployment = execTx $ createTxWithValue bc d ca (fromInteger unlimitedGasPerBlock) (w256 $ fromInteger balc) (0, 0) + vm1 <- execStateT deployment vm0 + when (isNothing $ currentContract vm1) (throwM $ DeploymentFailed ca) + + -- Run + let transaction = execTx $ uncurry basicTx setUpFunction d ca (fromInteger unlimitedGasPerBlock) (0, 0) + vm2 <- if isDapptestMode tm && setUpFunction `elem` abi then execStateT transaction vm1 else return vm1 + + case vm2 ^. result of + Just (VMFailure _) -> throwM SetUpCallFailed + _ -> return (vm2, unions $ map (view eventMap) cs, neFuns, fst <$> tests, abiMapping) where choose [] _ = throwM NoContracts choose (c:_) Nothing = return c choose _ (Just n) = maybe (throwM $ ContractNotFound n) pure $ find (Data.Text.isSuffixOf (if T.any (== ':') n then n else ":" `append` n) . view contractName) cs + setUpFunction = ("setUp", []) + -- | Given a file and an optional contract name, compile the file as solidity, then, if a name is -- given, try to fine the specified contract (assuming it is in the file provided), otherwise, find @@ -242,7 +257,7 @@ prepareForTest (vm, em, a, ts, m) c si = do a' = NE.toList a ps = filterResults c $ payableFunctions si as = if isAssertionMode tm then filterResults c $ asserts si else [] - cs = filterResults c (constantFunctions si) \\ as + cs = if isDapptestMode tm then [] else filterResults c (constantFunctions si) \\ as (hm, lm) = prepareHashMaps cs as m pure (vm, World s hm lm ps em, createTests tm td ts r a') diff --git a/lib/Echidna/Test.hs b/lib/Echidna/Test.hs index 81ebf081..d7e193b6 100644 --- a/lib/Echidna/Test.hs +++ b/lib/Echidna/Test.hs @@ -10,9 +10,10 @@ import Control.Monad.Reader.Class (MonadReader) import Control.Monad.State.Strict (MonadState(get, put), gets) import Data.Has (Has(..)) import Data.Text (Text) -import EVM (Error(..), VMResult(..), VM, calldata, codeContract, result, tx, state, substate, selfdestructs) +import EVM (Error(..), VMResult(..), VM, calldata, callvalue, codeContract, result, tx, state, substate, selfdestructs) import EVM.ABI (AbiValue(..), AbiType(..), encodeAbiValue, decodeAbiValue, ) import EVM.Types (Addr) +import EVM.Symbolic (forceLit) import qualified Data.ByteString as BS import qualified Data.ByteString.Lazy as LBS @@ -56,12 +57,13 @@ createTest m = EchidnaTest (Open (-1)) m v [] Stop [] _ -> NoValue validateTestModeError :: String -validateTestModeError = "Invalid test mode (should be property, assertion, optimization, overflow or exploration)" +validateTestModeError = "Invalid test mode (should be property, assertion, dapptest, optimization, overflow or exploration)" validateTestMode :: String -> TestMode validateTestMode s = case s of "property" -> s "assertion" -> s + "dapptest" -> s "exploration" -> s "overflow" -> s "optimization" -> s @@ -79,13 +81,18 @@ isPropertyMode :: TestMode -> Bool isPropertyMode "property" = True isPropertyMode _ = False +isDapptestMode :: TestMode -> Bool +isDapptestMode "dapptest" = True +isDapptestMode _ = False + createTests :: TestMode -> Bool -> [Text] -> Addr -> [SolSignature] -> [EchidnaTest] createTests m td ts r ss = case m of "exploration" -> [createTest Exploration] "overflow" -> [createTest (CallTest "Integer (over/under)flow" checkOverflowTest)] "property" -> map (\t -> createTest (PropertyTest t r)) ts "optimization" -> map (\t -> createTest (OptimizationTest t r)) ts - "assertion" -> map (\s -> createTest (AssertionTest s r)) (filter (/= fallback) ss) ++ [createTest (CallTest "AssertionFailed(..)" checkAssertionTest)] + "assertion" -> map (\s -> createTest (AssertionTest False s r)) (filter (/= fallback) ss) ++ [createTest (CallTest "AssertionFailed(..)" checkAssertionTest)] + "dapptest" -> map (\s -> createTest (AssertionTest True s r)) (filter (\(_, xs) -> not $ null xs) ss) _ -> error validateTestModeError ++ (if td then [sdt, sdat] else []) @@ -113,7 +120,7 @@ checkETest test = case test ^. testType of Exploration -> return (BoolValue True, [], Stop) -- These values are never used PropertyTest n a -> checkProperty (n, a) OptimizationTest n a -> checkOptimization (n, a) - AssertionTest n a -> checkAssertion (n, a) + AssertionTest dt n a -> if dt then checkDapptestAssertion (n, a) else checkStatefullAssertion (n, a) CallTest _ f -> checkCall f checkProperty :: (MonadReader x m, Has TestConf x, Has TxConf x, Has DappInfo x, MonadState y m, Has VM y, MonadThrow m) @@ -167,9 +174,9 @@ checkOptimization (f,a) = do pure (getIntFromResult (vm' ^. result), extractEvents dappInfo vm', getResultFromVM vm') -checkAssertion :: (MonadReader x m, Has TestConf x, Has TxConf x, Has DappInfo x, MonadState y m, Has VM y, MonadThrow m) +checkStatefullAssertion :: (MonadReader x m, Has TestConf x, Has TxConf x, Has DappInfo x, MonadState y m, Has VM y, MonadThrow m) => (SolSignature, Addr) -> m (TestValue, Events, TxResult) -checkAssertion (sig, addr) = do +checkStatefullAssertion (sig, addr) = do dappInfo <- view hasLens vm <- use hasLens -- Whether the last transaction called the function `sig`. @@ -190,6 +197,31 @@ checkAssertion (sig, addr) = do isFailure = isCorrectTarget && (eventFailure || isAssertionFailure) pure (BoolValue (not isFailure), events, getResultFromVM vm) +assumeMagicReturnCode :: BS.ByteString +assumeMagicReturnCode = "FOUNDRY::ASSUME\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0" + +checkDapptestAssertion :: (MonadReader x m, Has TestConf x, Has TxConf x, Has DappInfo x, MonadState y m, Has VM y, MonadThrow m) + => (SolSignature, Addr) -> m (TestValue, Events, TxResult) +checkDapptestAssertion (sig, addr) = do + dappInfo <- view hasLens + vm <- use hasLens + -- Whether the last transaction has any value + let hasValue = forceLit (vm ^. state . callvalue) /= 0 + -- Whether the last transaction called the function `sig`. + let isCorrectFn = case viewBuffer $ vm ^. state . calldata . _1 of + Just cd -> BS.isPrefixOf (BS.take 4 (abiCalldata (encodeSig sig) mempty)) cd + Nothing -> False + isAssertionFailure = case vm ^. result of + Just (VMFailure (Revert bs)) -> not $ BS.isSuffixOf assumeMagicReturnCode bs + Just (VMFailure _) -> True + _ -> False + isCorrectAddr = addr == vm ^. state . codeContract + isCorrectTarget = isCorrectFn && isCorrectAddr + events = extractEvents dappInfo vm + isFailure = not hasValue && (isCorrectTarget && isAssertionFailure) + pure (BoolValue (not isFailure), events, getResultFromVM vm) + + checkCall :: (MonadReader x m, Has TestConf x, Has TxConf x, Has DappInfo x, MonadState y m, Has VM y, MonadThrow m) => (DappInfo -> VM -> TestValue) -> m (TestValue, Events, TxResult) checkCall f = do diff --git a/lib/Echidna/Transaction.hs b/lib/Echidna/Transaction.hs index df0c9af8..13c126ef 100644 --- a/lib/Echidna/Transaction.hs +++ b/lib/Echidna/Transaction.hs @@ -89,9 +89,9 @@ genValue mv ds ps sc = g <- oftenUsually randValue $ rElem (0 NE.:| ds') fromIntegral <$> g else do - g <- usuallyRarely (pure 0) randValue -- once in a while, this will generate value in a non-payable function + g <- usuallyVeryRarely (pure 0) randValue -- once in a while, this will generate value in a non-payable function fromIntegral <$> g - where randValue = getRandomR (1 :: Integer, fromIntegral mv) + where randValue = getRandomR (0 :: Integer, fromIntegral mv) sig = (hashSig . encodeSig . signatureCall) sc -- | Check if a 'Transaction' is as \"small\" (simple) as possible (using ad-hoc heuristics). diff --git a/lib/Echidna/Types/Solidity.hs b/lib/Echidna/Types/Solidity.hs index 56f6f32a..bdf6e432 100644 --- a/lib/Echidna/Types/Solidity.hs +++ b/lib/Echidna/Types/Solidity.hs @@ -34,6 +34,7 @@ data SolException = BadAddr Addr | OnlyTests | ConstructorArgs String | DeploymentFailed Addr + | SetUpCallFailed | NoCryticCompile | InvalidMethodFilters Filter makePrisms ''SolException @@ -53,6 +54,7 @@ instance Show SolException where (ConstructorArgs s) -> "Constructor arguments are required: " ++ s NoCryticCompile -> "crytic-compile not installed or not found in PATH. To install it, run:\n pip install crytic-compile" (InvalidMethodFilters f) -> "Applying " ++ show f ++ " to the methods produces an empty list. Are you filtering the correct functions or fuzzing the correct contract?" + SetUpCallFailed -> "Calling the setUp() funciton failed (revert, out-of-gas, sending ether to an non-payable constructor, etc.)" (DeploymentFailed a) -> "Deploying the contract " ++ show a ++ " failed (revert, out-of-gas, sending ether to an non-payable constructor, etc.)" instance Exception SolException diff --git a/lib/Echidna/Types/Test.hs b/lib/Echidna/Types/Test.hs index 729f5679..d71df64b 100644 --- a/lib/Echidna/Types/Test.hs +++ b/lib/Echidna/Types/Test.hs @@ -50,17 +50,17 @@ instance Show TestValue where data TestType = PropertyTest Text Addr | OptimizationTest Text Addr - | AssertionTest SolSignature Addr + | AssertionTest Bool SolSignature Addr | CallTest Text (DappInfo -> VM -> TestValue) | Exploration instance Eq TestType where - (PropertyTest t a) == (PropertyTest t' a') = t == t' && a == a' - (AssertionTest s a) == (AssertionTest s' a') = s == s' && a == a' + (PropertyTest t a) == (PropertyTest t' a') = t == t' && a == a' + (AssertionTest b s a) == (AssertionTest b' s' a') = b == b' && s == s' && a == a' (OptimizationTest s a) == (OptimizationTest s' a') = s == s' && a == a' - (CallTest t _) == (CallTest t' _) = t == t' - Exploration == Exploration = True - _ == _ = False + (CallTest t _) == (CallTest t' _) = t == t' + Exploration == Exploration = True + _ == _ = False instance Eq TestState where diff --git a/lib/Echidna/UI/Report.hs b/lib/Echidna/UI/Report.hs index b6571f2c..5a9c14cf 100644 --- a/lib/Echidna/UI/Report.hs +++ b/lib/Echidna/UI/Report.hs @@ -104,7 +104,7 @@ ppTests Campaign { _tests = ts } = unlines . catMaybes <$> mapM pp ts where pp t = case t ^. testType of PropertyTest n _ -> Just . ((T.unpack n ++ ": ") ++) <$> ppTS (t ^. testState) (t ^. testEvents) (t ^. testReproducer) CallTest n _ -> Just . ((T.unpack n ++ ": ") ++) <$> ppTS (t ^. testState) (t ^. testEvents) (t ^. testReproducer) - AssertionTest s _ -> Just . ((T.unpack (encodeSig s) ++ ": ") ++) <$> ppTS (t ^. testState) (t ^. testEvents) (t ^. testReproducer) + AssertionTest _ s _ -> Just . ((T.unpack (encodeSig s) ++ ": ") ++) <$> ppTS (t ^. testState) (t ^. testEvents) (t ^. testReproducer) OptimizationTest n _ -> Just . ((T.unpack n ++ ": max value: " ++ show (t ^. testValue)) ++) <$> ppTS (t ^. testState) (t ^. testEvents) (t ^. testReproducer) Exploration -> return Nothing diff --git a/lib/Echidna/UI/Widgets.hs b/lib/Echidna/UI/Widgets.hs index 3682d107..aafa4354 100644 --- a/lib/Echidna/UI/Widgets.hs +++ b/lib/Echidna/UI/Widgets.hs @@ -91,7 +91,7 @@ testWidget etest = Exploration -> widget tsWidget "exploration" "" PropertyTest n _ -> widget tsWidget n "" OptimizationTest n _ -> widget optWidget n "optimizing " - AssertionTest s _ -> widget tsWidget (encodeSig s) "assertion in " + AssertionTest _ s _ -> widget tsWidget (encodeSig s) "assertion in " CallTest n _ -> widget tsWidget n "" where diff --git a/src/test/Common.hs b/src/test/Common.hs index f7f7c766..5e3019be 100644 --- a/src/test/Common.hs +++ b/src/test/Common.hs @@ -119,11 +119,11 @@ getResult n c = _ -> error "found more than one tests" where findTest test = case view testType test of - PropertyTest t _ -> t == n - AssertionTest (t,_) _ -> t == n - CallTest t _ -> t == n - OptimizationTest t _ -> t == n - _ -> False + PropertyTest t _ -> t == n + AssertionTest _ (t,_) _ -> t == n + CallTest t _ -> t == n + OptimizationTest t _ -> t == n + _ -> False optnFor :: Text -> Campaign -> Maybe TestValue optnFor n c = case getResult n c of diff --git a/src/test/Spec.hs b/src/test/Spec.hs index 8c15b593..b952fb91 100644 --- a/src/test/Spec.hs +++ b/src/test/Spec.hs @@ -14,12 +14,12 @@ import Tests.Overflow (overflowTests) import Tests.Research (researchTests) import Tests.Values (valuesTests) import Tests.Seed (seedTests) +import Tests.Dapptest (dapptestTests) main :: IO () main = withCurrentDirectory "./tests/solidity" . defaultMain $ testGroup "Echidna" [ configTests - , researchTests , compilationTests , seedTests , integrationTests @@ -30,5 +30,6 @@ main = withCurrentDirectory "./tests/solidity" . defaultMain $ , overflowTests , optimizationTests , researchTests + , dapptestTests , encodingJSONTests ] diff --git a/src/test/Tests/Dapptest.hs b/src/test/Tests/Dapptest.hs new file mode 100644 index 00000000..7cf0dd8d --- /dev/null +++ b/src/test/Tests/Dapptest.hs @@ -0,0 +1,22 @@ +module Tests.Dapptest (dapptestTests) where + +import Test.Tasty (TestTree, testGroup) + +import Common (testContract', solcV, solved, passed) + +dapptestTests :: TestTree +dapptestTests = testGroup "Dapptest Integration Testing" + [ testContract' "dapptest/basic.sol" (Just "GreeterTest") (Just (\v -> v >= solcV (0,7,5))) (Just "dapptest/config.yaml") False + [ + ("testShrinking passed", solved "testShrinking"), + ("testFuzzFixedArray passed", solved "testFuzzFixedArray"), + ("testFuzzVariableArray passed", solved "testFuzzVariableArray"), + ("testFuzzVariableArray passed", solved "testFuzzVariableArray"), + ("testFuzzBytes1 passed", solved "testFuzzBytes1"), + ("testFuzzBytes14 passed", solved "testFuzzBytes14"), + ("testFuzzBytes32 passed", solved "testFuzzBytes32"), + ("testFuzzI256 passed", solved "testFuzzI256"), + ("testFuzzAbiCoderV2 passed", solved "testFuzzAbiCoderV2"), + ("testAssume failed", passed "testFuzzAssume") + ] + ] diff --git a/src/test/Tests/Research.hs b/src/test/Tests/Research.hs index b560b70e..ecb7cca8 100644 --- a/src/test/Tests/Research.hs +++ b/src/test/Tests/Research.hs @@ -2,15 +2,15 @@ module Tests.Research (researchTests) where import Test.Tasty (TestTree, testGroup) -import Common (testContract, testContractV, testContract', solcV, solved) +import Common (testContract, testContract', solcV, solved) researchTests :: TestTree researchTests = testGroup "Research-based Integration Testing" [ testContract "research/harvey_foo.sol" Nothing [ ("echidna_assert failed", solved "echidna_assert") ] - , testContract "research/harvey_baz.sol" Nothing + , testContract' "research/harvey_baz.sol" Nothing Nothing Nothing False [ ("echidna_all_states failed", solved "echidna_all_states") ] - , testContractV "research/ilf_crowdsale.sol" (Just (\v -> v >= solcV (0,5,0) && v < solcV (0,6,0))) (Just "research/ilf_crowdsale.yaml") + , testContract' "research/ilf_crowdsale.sol" Nothing (Just (\v -> v >= solcV (0,5,0) && v < solcV (0,6,0))) (Just "research/ilf_crowdsale.yaml") False [ ("echidna_assert failed", solved "withdraw") ] , testContract' "research/solcfuzz_funwithnumbers.sol" (Just "VerifyFunWithNumbers") (Just (< solcV (0,6,0))) (Just "research/solcfuzz_funwithnumbers.yaml") True [ ("echidna_assert failed", solved "sellTokens"), diff --git a/tests/solidity/dapptest/basic.sol b/tests/solidity/dapptest/basic.sol new file mode 100644 index 00000000..572c2efc --- /dev/null +++ b/tests/solidity/dapptest/basic.sol @@ -0,0 +1,91 @@ +// SPDX-License-Identifier: UNLICENSED +pragma abicoder v2; +pragma solidity >=0.7.5; + +contract Greeter { + string public greeting; + + function greet(string memory _greeting) public { + greeting = _greeting; + } + + function gm() public { + greeting = "gm"; + } +} + +contract GreeterTestSetup { + Greeter greeter; + + function greeting() public view returns (string memory) { + return greeter.greeting(); + } + + function setUp() public { + greeter = new Greeter(); + } +} + +contract GreeterTest is GreeterTestSetup { + function greet(string memory _greeting) public { + greeter.greet(_greeting); + } + + function testShrinking(uint256 x, uint256 y) public { + require(x * y <= 100, "product greater than 100"); + } + + function testStringFuzz(string memory myGreeting) public { + greeter.greet(myGreeting); + require(keccak256(abi.encodePacked(greeter.greeting())) == keccak256(abi.encodePacked(myGreeting)), "not equal"); + } + + function testFuzzFixedArray(uint256[2] memory x) public { + // filter out x[1] == 0 since it'll drain all our gas in the + // division by zero from all future tests + if (x[1] == 0) return; + require(x[1] / x[1] == 0); + } + + function testFuzzVariableArray(uint256[] memory x) public { + require(x[0] == x[1]); + } + + function testFuzzBytes1(bytes1 x) public { + require(x == 0); + } + + function testFuzzBytes14(bytes14 x) public { + require(x == 0); + } + + function testFuzzBytes32(bytes32 x) public { + require(x == 0); + } + + function testFuzzI256(int256 x) public { + require(x >= 0); + } + + struct Foo { + Bar bar; + } + + struct Bar { + uint256 baz; + } + + function testFuzzAbiCoderV2(Foo memory foo) public { + require(foo.bar.baz < 5); + } + + function testGreeting(string memory message) public { + greeter.greet(message); + require(keccak256(abi.encodePacked(greeter.greeting())) == keccak256(abi.encodePacked(message)), "not equal"); + } + + function testFuzzAssume(uint256 x) public { + require(false, "FOUNDRY::ASSUME"); + // unreachable + } +} diff --git a/tests/solidity/dapptest/config.yaml b/tests/solidity/dapptest/config.yaml new file mode 100644 index 00000000..cf513962 --- /dev/null +++ b/tests/solidity/dapptest/config.yaml @@ -0,0 +1,4 @@ +testMode: dapptest +testLimit: 1000 +shrinkLimit: 100 +seqLen: 1 diff --git a/tests/solidity/research/ilf_crowdsale.yaml b/tests/solidity/research/ilf_crowdsale.yaml index 8a04b545..8ef313b2 100644 --- a/tests/solidity/research/ilf_crowdsale.yaml +++ b/tests/solidity/research/ilf_crowdsale.yaml @@ -1,3 +1,2 @@ maxValue: 10000000000000000000000000 -coverage: true testMode: assertion