Allow configuring zero delay (#1541)

* Fix genDelay to use 0 as lower bound for random delay

genDelay used getRandomR(1, maxDelay) which caused undefined behavior
when maxDelay was 0 (inverted bounds). In practice this leaked delay=1
even when the user configured maxTimeDelay or maxBlockDelay to 0.

Change the lower bound to 0, which fixes the inverted bounds issue and
also allows zero delays naturally (consecutive txs in same block/time),
consistent with how genValue already uses getRandomR(0, ...).

* tests: add no-delay test for maxTimeDelay/maxBlockDelay = 0

Test that with maxTimeDelay: 0 and maxBlockDelay: 0, block numbers
and timestamps remain consistent across transactions (no delay leaks).

Author: elopez

lib/Echidna/Transaction.hs

@@ -89,7 +89,7 @@ genTx world deployedContracts = do
 genDelay :: MonadRandom m => W256 -> Set W256 -> m W256
 genDelay mv ds =
   join $ oftenUsually fromDict randValue
-  where randValue = fromIntegral <$> getRandomR (1 :: Integer, fromIntegral mv)
+  where randValue = fromIntegral <$> getRandomR (0 :: Integer, fromIntegral mv)
         fromDict = (`mod` (mv + 1)) <$> rElem' ds
 
 genValue

src/test/Tests/Integration.hs

@@ -70,6 +70,9 @@ integrationTests = testGroup "Solidity Integration Testing"
   , testContract "basic/delay.sol"        Nothing
       [ ("echidna_block_number passed",            solved    "echidna_block_number")
       , ("echidna_timestamp passed",               solved    "echidna_timestamp") ]
+  , testContract "basic/no-delay.sol"   (Just "basic/no-delay.yaml")
+      [ ("echidna_block_number failed",            passed    "echidna_block_number")
+      , ("echidna_timestamp failed",               passed    "echidna_timestamp") ]
   , testContractV "basic/immutable.sol"    (Just (>= solcV (0,6,0))) Nothing
       [ ("echidna_test passed",                    solved      "echidna_test") ]
   , testContractV "basic/immutable-2.sol"    (Just (>= solcV (0,6,0))) Nothing

tests/solidity/basic/no-delay.sol

@@ -0,0 +1,31 @@
+contract C {
+  uint blockA;
+  uint timeA;
+  uint blockB;
+  uint timeB;
+
+  constructor() public {
+    blockA = block.number;
+    timeA = block.timestamp;
+    blockB = block.number;
+    timeB = block.timestamp;
+  }
+
+  function f() public {
+    blockA = block.number;
+    timeA = block.timestamp;
+  }
+
+  function g() public {
+    blockB = block.number;
+    timeB = block.timestamp;
+  }
+
+  function echidna_block_number() public returns (bool) {
+    return blockA == blockB;
+  }
+
+  function echidna_timestamp() public returns (bool) {
+    return timeA == timeB;
+  }
+}

tests/solidity/basic/no-delay.yaml

@@ -0,0 +1,2 @@
+maxTimeDelay: 0
+maxBlockDelay: 0