hevm loop heuristic triggers even when using code without loops

[gustavo-grieco]

After #853 is fixed, another issue related with the loop heuristic was found: it can be confused to detect loops where there is nothing like that.

To reproduce, clone the abdk verification repository and run the exploration using make verify-hevm T=prove_inv_identity. It will explore certain number of states. However, if you modify the Makefile to use --loop-detection-heuristic StackBased in the hevm call, you will see the number of states explored is around half of them (and the results will be available much faster!). Interestingly enough, the code has no loops at all (but some function calls are repeated).

Should we have a "no loop heuristic mode" ?

[msooseth]

Right.... I'm looking. I have a feeling it's because of abs and similar that is being called again and again:

    function prove_inv_identity(int128 x) public view {
        require(x != ZERO_FP);

        int128 inv_x = inv(x);
        int128 identity = mul(inv_x, x);

        // They should agree with a tolerance of one tenth of a percent
        assert(equal_within_tolerance(identity, ONE_FP, ONE_TENTH_FP));
    }

where:

    function equal_within_tolerance(
        int128 a,
        int128 b,
        int128 error_percent
    ) public pure returns (bool) {
        int128 ref = abs(a) > abs(b) ? abs(a) : abs(b); 
        int128 tol_value = abs(mul(ref, div(error_percent, fromUInt(100))));

        return (abs(sub(b, a)) <= tol_value);
    }

I'll try to make this into a test-case and make sense of it. Currently it's a bit large to be understood as-is.

[msooseth]

Here's a minimal version of this contract: https://github.com/msooseth/hevm-result-test-contracts/blob/main/src/loop-detect-fail-854.sol It only contains the constants/functions that are being used. One good thing about it is that it does find the CEX:

$ cabal run exe:hevm -- test --root tmp --solver bitwuzla --num-cex-fuzz 0 --only-deployed --match ".*prove_inv_identity.*" --debug --smttimeout 10 --max-iterations 1 --loop-detection-heuristic StackBased
[...]
   Exploration finished, 78 branch(es) to check in call prefix 0xacce097a
[...]
   [FAIL] prove_inv_identity
   Counterexample:   [validated]
     calldata: prove_inv_identity(-70427735148495640502223729299493508356)
     result:   Revert: 0x4e487b710000000000000000000000000000000000000000000000000000000000000001
   [WARNING] hevm was only able to partially explore the test prove_inv_identity due to:
      3x -> SMT solver says: Result unknown by SMT solver

So that's good. Notice that it's even validated! ❤️

With Naive, however:

   [WARNING] prove_inv_identity all branches reverted
   [WARNING] hevm was only able to partially explore the test prove_inv_identity due to:
      1x -> Max iterations reached in file "src/loop-detect-fail-854.sol" on line 36 : "require (x != MIN_64x64)"

So that's an interesting iteration :D Maybe Solidity emits some loop to check for int128? I'll check...

[msooseth]

Hmmm, this:

contract C {
    int128 private constant MIN_64x64 = 0x55aabbccddeeff;
  function abs (int128 x) public pure returns (int128) {
    unchecked {
      require (x != MIN_64x64);
      return x;
    }
  }
}

Becomes:

            function fun_abs_20(var_x_5) -> var__8 {
                /// @src 0:119:125  "int128"
                let zero_t_int128_1 := zero_value_for_split_t_int128()
                var__8 := zero_t_int128_1

                /// @src 0:160:161  "x"
                let _2 := var_x_5
                let expr_11 := _2
                /// @src 0:165:174  "MIN_64x64"
                let expr_12 := constant_MIN_64x64_3()
                /// @src 0:160:174  "x != MIN_64x64"
                let expr_13 := iszero(eq(cleanup_t_int128(expr_11), cleanup_t_int128(expr_12)))
                /// @src 0:151:175  "require (x != MIN_64x64)"
                require_helper(expr_13)
                /// @src 0:190:191  "x"
                let _4 := var_x_5
                let expr_16 := _4
                /// @src 0:183:191  "return x"
                var__8 := expr_16
                leave

            }

And cleanup_t_int128 is just signextend, and the rest is pretty obvious. No loops.

[msooseth]

Oooh, but we might enter cleanup_t_int128 code more than once, and that could mislead the Naive... let me check.

[msooseth]

OK, yeah, I am pretty sure what's happening is that we jump to the same function, and Naive doesn't care -- as long as the (addr,pc) matches again, it's a loop:

maxIterationsReached vm (Just maxIter) =
  let codelocation = getCodeLocation vm
      (iters, _) = view (at codelocation % non (0, [])) vm.iterations
  in if unsafeInto maxIter <= iters
     then Map.lookup (codelocation, iters - 1) vm.cache.path
     else Nothing

And Naive for isLoopHead is:

isLoopHead Naive _ = Just True

So calling the same function twice is a loop I think! It's super-naive :)

[msooseth]

I think maybe using -1 would be sufficient as a "no loop heuristic" mode? That disables loop detection and continues on all paths, always.

[gustavo-grieco]

Is there a branch to test this?

[msooseth]

I think it's already supported by the CLI, this -1 thing. It disables the loop heuristic and will run out of resources in case there is a loop. But if there isn't a loop, then it should "just work", not detecting loops, continuing no matter what... maybe you can try? See what happens...

BTW, the loop detection heuristic is probably not great, so it's a valid complaint, and we should try to improve it. These issues should help us improve it. So I'm glad you filed it, even if it can be fixed via this hack of using -1

[gustavo-grieco]

For reference, using --loop-detection-heuristic Naive --max-iterations -1 does not change the result. It still seems to be exploring forever. Tested with 2da8772. To re-test this bug, make sure you are using the latest revision from the abdk verification repository and follow the instructions in the first message.

[msooseth]

I think Naive is broken and shouldn't really be an option I thihnk. And -1 is supposed to explore forever, because -1 means no limit. But I feel like there must be something here, that I don't understand... I am sure you actually found a bug, I am just having a hard time understanding it, sorry :( I'll come back sometime later and see if I can understand it.