Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Better better results printing #472

Merged
merged 5 commits into from
Mar 15, 2024
Merged

Better better results printing #472

merged 5 commits into from
Mar 15, 2024

Conversation

msooseth
Copy link
Collaborator

@msooseth msooseth commented Mar 11, 2024 •
edited
Loading

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: #439

Fixed issues:

  • Too many empty lines removed, thing that belong together are now printed together
  • When we emit a warning, but here is more than one function present, we didn't say which function lead to the warning. This is now printed as a hex function prefix. Not perfect, but way better than before.
  • It is now easy to see which function the counterexamples belong to. Before, things were not grouped, and that lead to some very weird printings/scenarios.
  • When things are FAIL-in because of all-revert, the pass/fail would get mixed in ways that are very hard to decipher.
  • Warnings are now yellow
  • It's a prettier printing overall

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

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

@msooseth msooseth marked this pull request as draft March 11, 2024 17:55
@msooseth msooseth changed the title [DRAFT] Better better results printing Better better results printing Mar 12, 2024
@msooseth msooseth requested a review from zoep March 12, 2024 18:57
@msooseth msooseth mentioned this pull request Mar 12, 2024
Closed
@msooseth msooseth marked this pull request as ready for review March 13, 2024 11:22
zoep
zoep reviewed Mar 13, 2024
View reviewed changes
src/EVM/SymExec.hs Outdated Show resolved Hide resolved
zoep
zoep approved these changes Mar 13, 2024
View reviewed changes
Copy link
Collaborator

@zoep zoep left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

lgtm! Code and output are much cleaner now!

@msooseth msooseth merged commit 05b3812 into main Mar 15, 2024
1 check failed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@zoep zoep zoep approved these changes

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@msooseth @zoep