Fixed wait bug when shrinking

.github/workflows/ci.yml

@@ -15,12 +15,12 @@ jobs:
       matrix:
         os:
           - ubuntu-latest
-          - macos-latest
+            #- macos-latest
         include:
           - os: ubuntu-latest
             apt-get: autoconf automake libtool
-          - os: macos-latest
-            brew: automake
+            #- os: macos-latest
+            #brew: automake
 
     steps:
       - name: Workaround for actions/virtual-environments#1811

examples/solidity/basic/push_long.sol

@@ -0,0 +1,25 @@
+contract TEST {
+
+  address [] a;
+  bool lengthChecking = false;
+
+  function push_1() public {
+    a.push(address(1));
+  }
+
+  function turn_on_length_checking() public {
+    lengthChecking = true;
+  }
+
+  function turn_off_length_checking() public {
+    lengthChecking = false;
+  }
+
+  function test_long_5() public {
+    if (a.length >= 5) {
+      if (lengthChecking) {
+	    assert(false);
+      }
+    }
+  }
+}

examples/solidity/basic/push_long.yaml

@@ -0,0 +1 @@
+checkAsserts: true

lib/Echidna/Transaction.hs

@@ -141,7 +141,7 @@ liftSH = stateST . runState . zoom hasLens
 -- 'Transaction's \"on-chain\".
 setupTx :: (MonadState x m, Has VM x) => Tx -> m ()
 setupTx (Tx NoCall _ r _ _ _ (t, b)) = liftSH . sequence_ $
-  [ result .= Nothing, state . pc .= 0, state . stack .= mempty, state . memory .= mempty
+  [ state . pc .= 0, state . stack .= mempty, state . memory .= mempty
   , block . timestamp += litWord t, block . number += b, loadContract r]
 
 setupTx (Tx c s r g gp v (t, b)) = liftSH . sequence_ $

src/test/Common.hs

@@ -9,6 +9,7 @@ module Common
   , passed
   , solvedLen
   , solvedWith
+  , solvedWithout 
   , getGas
   , gasInRange
   , countCorpus
@@ -37,7 +38,6 @@ import Echidna.Config (EConfig, _econfig, parseConfig, defaultConfig, sConf, cCo
 import Echidna.Solidity (loadSolTests, quiet)
 import Echidna.Test (checkETest)
 import Echidna.Types.Campaign (Campaign, TestState(..), testLimit, shrinkLimit, tests, gasInfo, corpus, coverage)
-import Echidna.Types.Signature (SolCall)
 import Echidna.Types.Tx (Tx(..), TxCall(..), call)
 import Echidna.Types.World (eventMap)
 
@@ -96,8 +96,11 @@ solvedLen :: Int -> Text -> Campaign -> Bool
 solvedLen i t = (== Just i) . fmap length . solnFor t
 
 -- NOTE: this just verifies a call was found in the solution. Doesn't care about ordering/seq length
-solvedWith :: SolCall -> Text -> Campaign -> Bool
-solvedWith c t = maybe False (any $ (== SolCall c) . view call) . solnFor t
+solvedWith :: TxCall -> Text -> Campaign -> Bool
+solvedWith tx t = maybe False (any $ (== tx) . view call) . solnFor t
+
+solvedWithout :: TxCall -> Text -> Campaign -> Bool
+solvedWithout tx t = maybe False (all $ (/= tx) . view call) . solnFor t
 
 getGas :: Text -> Campaign -> Maybe (Int, [Tx])
 getGas t = lookup t . view gasInfo

src/test/Tests/Integration.hs

@@ -3,14 +3,15 @@ module Tests.Integration (integrationTests) where
 import Test.Tasty (TestTree, testGroup)
 import Test.Tasty.HUnit (testCase, assertBool)
 
-import Common (runContract, testContract, testContract', checkConstructorConditions, testConfig, passed, solved, solvedLen, solvedWith, coverageEmpty, testsEmpty, gasInRange, countCorpus)
+import Common (runContract, testContract, testContract', checkConstructorConditions, testConfig, passed, solved, solvedLen, solvedWith, solvedWithout, coverageEmpty, testsEmpty, gasInRange, countCorpus)
 import Control.Lens (set)
 import Control.Monad (when)
 import Data.Functor ((<&>))
 import Data.List (isInfixOf)
 import Data.Text (unpack)
 import Echidna.Config (_econfig, parseConfig, sConf)
 import Echidna.Solidity (quiet)
+import Echidna.Types.Tx (TxCall(..))
 import EVM.ABI (AbiValue(..))
 import System.Process (readProcess)
 
@@ -44,7 +45,7 @@ integrationTests = testGroup "Solidity Integration Testing"
       , ("echidna_fails_on_revert didn't shrink to one transaction",
          solvedLen 1 "echidna_fails_on_revert")
       , ("echidna_revert_is_false didn't shrink to f(-1, 0x0, 0xdeadbeef)",
-         solvedWith ("f", [AbiInt 256 (-1), AbiAddress 0, AbiAddress 0xdeadbeef]) "echidna_fails_on_revert")
+         solvedWith (SolCall ("f", [AbiInt 256 (-1), AbiAddress 0, AbiAddress 0xdeadbeef])) "echidna_fails_on_revert")
       ]
   , testContract "basic/nearbyMining.sol" (Just "coverage/test.yaml")
       [ ("echidna_findNearby passed", solved "echidna_findNearby") ]
@@ -54,7 +55,7 @@ integrationTests = testGroup "Solidity Integration Testing"
       [ ("echidna_all_sender passed",                      solved             "echidna_all_sender")
       , ("echidna_all_sender didn't shrink optimally",     solvedLen 3        "echidna_all_sender")
       ] ++ (["s1", "s2", "s3"] <&> \n ->
-        ("echidna_all_sender solved without " ++ unpack n, solvedWith (n, []) "echidna_all_sender"))
+        ("echidna_all_sender solved without " ++ unpack n, solvedWith (SolCall (n, [])) "echidna_all_sender"))
   , testContract "basic/memory-reset.sol" Nothing
       [ ("echidna_memory failed",                  passed      "echidna_memory") ]
   , testContract "basic/contractAddr.sol" Nothing
@@ -90,6 +91,8 @@ integrationTests = testGroup "Solidity Integration Testing"
   , testContract "basic/darray.sol"       Nothing
       [ ("echidna_darray passed",                  solved      "echidna_darray")
       , ("echidna_darray didn't shrink optimally", solvedLen 1 "echidna_darray") ]
+  , testContract "basic/push_long.sol" (Just "basic/push_long.yaml")
+      [ ("test_long_5 passed",                     solvedWithout NoCall "ASSERTION test_long_5")]
   , testContract "basic/propGasLimit.sol" (Just "basic/propGasLimit.yaml")
       [ ("echidna_runForever passed",              solved      "echidna_runForever") ]
   , testContract "basic/assert.sol"       (Just "basic/assert.yaml")