[DRAFT] Changing default --max-iterations to 5. NOTE: 5 is not enough... WAT

[msooseth]

Description

Maximum iterations explored of loops has been set to 5 by default instead of the infinite before. This is to:

• Keep more in line with other symbolic execution systems' defaults (e.g hevm). They tend to a have a fixed default, usually 1. However, 1 is so low that it can cause issues with std-test.
• Not get stuck on a single loop and find potential issues outside of the loop. Otherwise, users would have a very bad experience of getting stuck on one thing where there could be bugs elsewhere.

We now print a better warning, with explanation how to increase the loop bound.

Checklist

• tested locally
• added automated tests
• updated the docs
• updated the changelog

[blishko]

I agree that 1 is too small of a bound.
Other symbolic execution engines use 5 as the bound?

[msooseth]

Actually, even 5 is low. What is even going on.

contract ZoeToken {
  /* account balances mapping */
  mapping(address => uint256) public bal;

  function setUp() public {
    bal[address(0)] = 1000;
  }

  /* Transfer amt from the sender's account to x */
  function transfer(address x, uint256 amt) public {
    if (amt != 42) {
      bal[msg.sender] -= amt;
    }
    bal[x] += amt;
  }
}

// SPDX-License-Identifier: UNLICENSED
import "forge-std/Test.sol";
import "src/ZoeToken.sol";

contract TokenTest is Test {
  ZoeToken token;

  function setUp() public {
      token = new ZoeToken();
      token.setUp(); 
  }

  function prove_zoe_transfer(address to, uint256 amt) public {
    uint256 fromBal= token.bal(msg.sender);
    token.transfer(to, amt);
    unchecked { 
    assertEq(fromBal - amt, token.bal(msg.sender)); }
    }
}

With 1:

$ cabal run  exe:hevm -- test --root tmp --max-iterations 1 --match "prove_zoe_transfer"

Checking 1 function(s) in contract src/Stuff.sol:TokenTest
[RUNNING] prove_zoe_transfer(address,uint256)
   WARNING: hevm was only able to partially explore the call prefix 0xf3fd44ce due to the following issue(s):
     - Max Iterations Reached in contract: 0xD95322745865822719164b1fC167930754c248DE pc: 11
   [FAIL] prove_zoe_transfer(address,uint256)
   Reason:
     No reachable assertion violations, but all branches reverted
     Prefix this testname with `proveFail` if this is expected

With 5:

$ cabal run  exe:hevm -- test --root tmp --max-iterations 5 --match "prove_zoe_transfer"

Checking 1 function(s) in contract src/Stuff.sol:TokenTest
[RUNNING] prove_zoe_transfer(address,uint256)
   WARNING: hevm was only able to partially explore the call prefix 0xf3fd44ce due to the following issue(s):
     - Max Iterations Reached in contract: 0x000000000000000000000000000000000000ACAb pc: 3455
     - Max Iterations Reached in contract: 0x000000000000000000000000000000000000ACAb pc: 3455
   [PASS] prove_zoe_transfer(address,uint256)

With 10:

$ cabal run  exe:hevm -- test --root tmp --max-iterations 10 --match "prove_zoe_transfer"

Checking 1 function(s) in contract src/Stuff.sol:TokenTest
[RUNNING] prove_zoe_transfer(address,uint256)
   [FAIL] prove_zoe_transfer(address,uint256)
   Counterexample:
     result:   Failed: DSTest Assertion Violation
     calldata: prove_zoe_transfer(0x0000000000000000000000000000000800000000,42)

I am soooo confused

[d-xo]

I think that this is because of some abi encoding stuff that happens in fail in ds-test unfortunately, shouldn't be too hard to modify ds-test, or we could also just switch to these cheatcode based assertions from foundry and move on with our lives probably.