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.

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

[Bug-Candidate]: ABDKMath64x64PropertyTests.sol: Tests output false negatives #13

Open
beber89 opened this issue Mar 15, 2023 · 3 comments

Comments

@beber89
Copy link

beber89 commented Mar 15, 2023

Describe the issue:

These 2 tests:

contract CryticABDKMath64x64Properties {
    ...
    function add_test_range(int128 x, int128 y) public view {
        int128 result;
        try this.add(x, y) {
            result = this.add(x, y);
            assert(result <= MAX_64x64 && result >= MIN_64x64);
        } catch {
            // If it reverts, just ignore
        }
    }

    function sub_test_range(int128 x, int128 y) public view {
        int128 result;
        try this.sub(x, y) {
            result = this.sub(x, y);
            assert(result <= MAX_64x64 && result >= MIN_64x64);
        } catch {
            // If it reverts, just ignore
        }
    }
}

They are not actually showing failure in case this.add/this.sub overflow or underflow.
It looks like result being int128 makes it always conforming with the assert statement despite the failure in this.add/this.sub.

Steps to reproduce the issue:

  • Create a smart contract to contain the test in ``tests/ABDKMath64x64PropertyTests/hardhat/contracts/CryticMathTest.sol`
pragma solidity ^0.8.0;
import "@crytic/properties/contracts/Math/ABDKMath64x64/ABDKMath64x64PropertyTests.sol";

contract CryticABDKMath64x64Harness is CryticABDKMath64x64Properties {
    /* Any additional test can be added here */
}
  • Working directory: tests/ABDKMath64x64PropertyTests/hardhat

  • Force ABDKMath64x64 to overflow/underflow by commenting out the require statement on the tested methods.

library ABDKMath64x64 {
   ....
  function add (int128 x, int128 y) internal pure returns (int128) {
    unchecked {
      int256 result = int256(x) + y;
      // COMMENTED THIS TO FORCE IT TO FAIL
      //  require (result >= MIN_64x64 && result <= MAX_64x64);
      return int128 (result);
    }
  }
  function sub (int128 x, int128 y) internal pure returns (int128) {
    unchecked {
      int256 result = int256(x) - y;
      // COMMENTED THIS TO FORCE IT TO FAIL
      //  require (result >= MIN_64x64 && result <= MAX_64x64);
      return int128 (result);
    }
  }
}
  • Run echidna-test . --contract CryticABDKMath64x64Harness --test-mode assertion

  • Output:

sub_test_range(int128,int128):  passed! 🎉
abs(int128):  passed! 🎉
add_test_maximum_value():  passed! 🎉
mulu(int128,uint256):  passed! 🎉
add_test_range(int128,int128):  passed! 🎉
  • Some other tests failed due to that change but add_test_range and sub_test_range did not fail as expected.

If additional code is needed for reproducing, please copy it here, or drop us a link to the repository:

No response

Echidna version:

Echidna 2.0.1

Additional information:

No response

@glarregay-tob
Copy link
Contributor

Hey, thanks for your submission!
This is an interesting point. I'll test this and the PR locally and get back to you.

@glarregay-tob
Copy link
Contributor

Hey @beber89, sorry for the delay. I ran some tests on this issue, thanks again for bringing it up.

The way that the add and sub functions are implemented in ABDKMath64x64 make the add_test_range and sub_test_range tests to be unnecesary, as you stated. This is due to the fact that ABDKMath's implementations of add and sub are using type casting from int256 to int128, and in the case where the result doesn't fit, the implementation just drops the higher order bits. In summary, there is no way it can overflow, as the result will always be in int128 range, and it is exactly the same range as the valid results.

Your PR addresses a condition that we weren't directly checking, that is overflow. I mean "directly" in the sense that if those functions were to overflow, the issue would be quite probably detected by the other failing tests that you mentioned in your report (add_test_values, add_test_maximum_value_plus_one, etc), but there is no specific test for it with fuzzable parameters.

Another point is that even if the math tests are now tailored to ABDKMath64x64, they are meant to be reusable for other libraries too. So we shouldn't assume that all libraries will implement overflow checks the same way, tests should be created for them. I think the overflow test you implemented can be useful in the cases where the valid result range is different than the underlying type range (for example, a 32x32 fixed point lib implemented with int128 as underlying). I am not aware if such libraries exist, though.

So, in summary, I think we can add your suggestions to the repo as a new overflow test. Before defining how it should be implemented, I'd like to read your opinion on this @ggrieco-tob.

@beber89
Copy link
Author

beber89 commented Mar 22, 2023

Hey @glarregay-tob , sorry for all that time it took me to respond.

I wrote that test based on the fact that the require statement applied on int128 is not actually checking anything and I assumed that testing for overflow/underflow can be seen as checking that the value is confined within the int128 range afterall.

But I got your point now, I understand that the pull request which I am suggesting looks like it tests a different thing. It can be a general overflow/underflow test but not a range test. I had another idea also then but it still contradicts the purpose of the test I think as this one.

I think the overflow test you implemented can be useful in the cases where the valid result range is different than the underlying type range (for example, a 32x32 fixed point lib implemented with int128 as underlying). I am not aware if such libraries exist, though.

I took a look but I could not find a library among the ones I know that does this .

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants