ethereum / hevm

symbolic EVM evaluator
https://hevm.dev
GNU Affero General Public License v3.0
223 stars 45 forks source link

Better better results printing #472

Closed msooseth closed 5 months ago

msooseth commented 5 months ago

Description

This PR improves the presentation of the results. Currently, the presentation is quite bad and can be misunderstood, for example here someone is rightfully confused: https://github.com/ethereum/hevm/issues/439

Fixed issues:

I am using https://github.com/msooseth/hevm-result-test-contracts to help me test, and I put it under "tmp", then I call hevm through cabal: cabal run exe:hevm -- test --root tmp --max-iterations 6

Output without this PR:

Running 2 tests for src/contract-allrevert-somenot.sol:MyContract
Exploring contract
Simplifying expression
Explored contract (1 branches)
Checking for reachability of 0 potential property violation(s)
[FAIL] prove_allrevert_somenot_thisrevert(uint256)
Exploring contract
Simplifying expression
Explored contract (3 branches)
Checking for reachability of 1 potential property violation(s)
[PASS] prove_allrevert_somenot_thisok(uint256)

Failure: prove_allrevert_somenot_thisrevert(uint256)

  No reachable assertion violations, but all branches reverted
  Prefix this testname with `proveFail` if this is expected

Exploring contract
Simplifying expression
Explored contract (1 branches)
Checking for reachability of 0 potential property violation(s)
[FAIL] prove_allrevert(uint256)

Failure: prove_allrevert(uint256)

  No reachable assertion violations, but all branches reverted
  Prefix this testname with `proveFail` if this is expected

Running 2 tests for src/contract-dual-diff-func-fail.sol:MyContract
Exploring contract
Simplifying expression
Explored contract (2 branches)
Checking for reachability of 1 potential property violation(s)
[FAIL] prove_dual_diff_func1(address,uint256)
Exploring contract
Simplifying expression
Explored contract (3 branches)
Checking for reachability of 2 potential property violation(s)
[FAIL] prove_dual_diff_func2(address,uint256)

Failure: prove_dual_diff_func1(address,uint256)

  Counterexample:

    result:   Revert: 0x4e487b710000000000000000000000000000000000000000000000000000000000000001
    calldata: prove_dual_diff_func1(000000000000000000000000000000000000000000000000000000000000131200000000000000000000000000000000000000000000000000000000000003e8fba908a0e6fae6c6b51002)

Failure: prove_dual_diff_func2(address,uint256)

  Counterexample:

    result:   Revert: 0x4e487b710000000000000000000000000000000000000000000000000000000000000001
    calldata: prove_dual_diff_func2(0x0000000000000000000000000000000000000000,0)

Running 1 tests for src/contract-dualfail.sol:MyContract
Exploring contract
Simplifying expression
Explored contract (9 branches)
Checking for reachability of 4 potential property violation(s)
[FAIL] prove_dualfail(address,uint256,bool)

Failure: prove_dualfail(address,uint256,bool)

  Counterexample:

    result:   Revert: 0x4e487b710000000000000000000000000000000000000000000000000000000000000001
    calldata: prove_dualfail(0x0000000000000000000000000000000000000000,0,false)

  Counterexample:

    result:   Revert: 0x4e487b710000000000000000000000000000000000000000000000000000000000000001
    calldata: prove_dualfail(0x0000000000000000000000000000000000000000,100,true)

Running 1 tests for src/contract-fail.sol:MyContract
Exploring contract
Simplifying expression
Explored contract (6 branches)
Checking for reachability of 3 potential property violation(s)
[FAIL] prove_single_fail(address,uint256)

Failure: prove_single_fail(address,uint256)

  Counterexample:

    result:   Revert: 0x4e487b710000000000000000000000000000000000000000000000000000000000000001
    calldata: prove_single_fail(0x0000000000000000000000000000000000000000,100)

Running 2 tests for src/contract-maxiters.sol:MyContract
Exploring contract
Simplifying expression
Explored contract (14 branches)

WARNING: hevm was only able to partially explore the given contract due to the following issues:

  - Max Iterations Reached in contract: 0x000000000000000000000000000000000000ACAb pc: 868

Checking for reachability of 6 potential property violation(s)
[FAIL] prove_maxiters_fail(uint256)
Exploring contract
Simplifying expression
Explored contract (14 branches)

WARNING: hevm was only able to partially explore the given contract due to the following issues:

  - Max Iterations Reached in contract: 0x000000000000000000000000000000000000ACAb pc: 1797

Checking for reachability of 6 potential property violation(s)
[PASS] prove_maxiters_pass(uint256)

Failure: prove_maxiters_fail(uint256)

  Counterexample:

    result:   Revert: 0x4e487b710000000000000000000000000000000000000000000000000000000000000001
    calldata: prove_maxiters_fail(1)

  Counterexample:

    result:   Revert: 0x4e487b710000000000000000000000000000000000000000000000000000000000000001
    calldata: prove_maxiters_fail(00000000000000000000000000000000000000000000000000000000000000020182dad8c17bd5e89e8043a08ada90a6d5efdee4425f85cb863109783e158ba4fba908a0e6fae6c6b51002)

  Counterexample:

    result:   Revert: 0x4e487b710000000000000000000000000000000000000000000000000000000000000001
    calldata: prove_maxiters_fail(3)

  Counterexample:

    result:   Revert: 0x4e487b710000000000000000000000000000000000000000000000000000000000000001
    calldata: prove_maxiters_fail(4)

  Counterexample:

    result:   Revert: 0x4e487b710000000000000000000000000000000000000000000000000000000000000001
    calldata: prove_maxiters_fail(5)

  Counterexample:

    result:   Revert: 0x4e487b710000000000000000000000000000000000000000000000000000000000000001
    calldata: prove_maxiters_fail(0000000000000000000000000000000000000000000000000000000000000006fedae82a06567f4ee1e26e286a98e5111604c92a95773f143a99c7cbac796c99c4e7e939c25be152558a90b1b3a2d2)

Running 1 tests for src/contract-pass.sol:MyContract
Exploring contract
Simplifying expression
Explored contract (6 branches)
Checking for reachability of 3 potential property violation(s)
[PASS] prove_pass(address,uint256)

New printing:

Checking 2 function(s) in contract src/contract-allrevert-somenot.sol:MyContract
[RUNNING] prove_allrevert_somenot_thisrevert(uint256)
   [FAIL] prove_allrevert_somenot_thisrevert(uint256)
   Reason:
     No reachable assertion violations, but all branches reverted
     Prefix this testname with `proveFail` if this is expected
[RUNNING] prove_allrevert_somenot_thisok(uint256)
   [PASS] prove_allrevert_somenot_thisok(uint256)

Checking 1 function(s) in contract src/contract-allrevert.sol:MyContract
[RUNNING] prove_allrevert(uint256)
   [FAIL] prove_allrevert(uint256)
   Reason:
     No reachable assertion violations, but all branches reverted
     Prefix this testname with `proveFail` if this is expected

Checking 2 function(s) in contract src/contract-dual-diff-func-fail.sol:MyContract
[RUNNING] prove_dual_diff_func1(address,uint256)
   [FAIL] prove_dual_diff_func1(address,uint256)
   Counterexample:
     result:   Revert: 0x4e487b710000000000000000000000000000000000000000000000000000000000000001
     calldata: prove_dual_diff_func1(000000000000000000000000000000000000000000000000000000000000131200000000000000000000000000000000000000000000000000000000000003e8fba908a0e6fae6c6b51002)
[RUNNING] prove_dual_diff_func2(address,uint256)
   [FAIL] prove_dual_diff_func2(address,uint256)
   Counterexample:
     result:   Revert: 0x4e487b710000000000000000000000000000000000000000000000000000000000000001
     calldata: prove_dual_diff_func2(0x0000000000000000000000000000000000000000,0)

Checking 1 function(s) in contract src/contract-dualfail.sol:MyContract
[RUNNING] prove_dualfail(address,uint256,bool)
   [FAIL] prove_dualfail(address,uint256,bool)
   Counterexample:
     result:   Revert: 0x4e487b710000000000000000000000000000000000000000000000000000000000000001
     calldata: prove_dualfail(0x0000000000000000000000000000000000000000,0,false)
   Counterexample:
     result:   Revert: 0x4e487b710000000000000000000000000000000000000000000000000000000000000001
     calldata: prove_dualfail(0x0000000000000000000000000000000000000000,100,true)

Checking 1 function(s) in contract src/contract-fail.sol:MyContract
[RUNNING] prove_single_fail(address,uint256)
   [FAIL] prove_single_fail(address,uint256)
   Counterexample:
     result:   Revert: 0x4e487b710000000000000000000000000000000000000000000000000000000000000001
     calldata: prove_single_fail(0x0000000000000000000000000000000000000000,100)

Checking 2 function(s) in contract src/contract-maxiters.sol:MyContract
[RUNNING] prove_maxiters_fail(uint256)
   WARNING: hevm was only able to partially explore the call prefix 0x36c026db due to the following issue(s):
     - Max Iterations Reached in contract: 0x000000000000000000000000000000000000ACAb pc: 868
   [FAIL] prove_maxiters_fail(uint256)
   Counterexample:
     result:   Revert: 0x4e487b710000000000000000000000000000000000000000000000000000000000000001
     calldata: prove_maxiters_fail(1)
   Counterexample:
     result:   Revert: 0x4e487b710000000000000000000000000000000000000000000000000000000000000001
     calldata: prove_maxiters_fail(00000000000000000000000000000000000000000000000000000000000000020182dad8c17bd5e89e8043a08ada90a6d5efdee4425f85cb863109783e158ba4fba908a0e6fae6c6b51002)
   Counterexample:
     result:   Revert: 0x4e487b710000000000000000000000000000000000000000000000000000000000000001
     calldata: prove_maxiters_fail(3)
   Counterexample:
     result:   Revert: 0x4e487b710000000000000000000000000000000000000000000000000000000000000001
     calldata: prove_maxiters_fail(4)
   Counterexample:
     result:   Revert: 0x4e487b710000000000000000000000000000000000000000000000000000000000000001
     calldata: prove_maxiters_fail(5)
   Counterexample:
     result:   Revert: 0x4e487b710000000000000000000000000000000000000000000000000000000000000001
     calldata: prove_maxiters_fail(0000000000000000000000000000000000000000000000000000000000000006fedae82a06567f4ee1e26e286a98e5111604c92a95773f143a99c7cbac796c99c4e7e939c25be152558a90b1b3a2d2)
[RUNNING] prove_maxiters_pass(uint256)
   WARNING: hevm was only able to partially explore the call prefix 0xb2f66016 due to the following issue(s):
     - Max Iterations Reached in contract: 0x000000000000000000000000000000000000ACAb pc: 1797
   [PASS] prove_maxiters_pass(uint256)

Checking 1 function(s) in contract src/contract-pass.sol:MyContract
[RUNNING] prove_pass(address,uint256)
   [PASS] prove_pass(address,uint256)

Checklist