-
Notifications
You must be signed in to change notification settings - Fork 47
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
feat: call constant methods occasionally and allow assertion testing …
…them (#363) * feat: call constant methods ocassionally and allow assertion testing them * add test
- Loading branch information
1 parent
5e5d0e0
commit 827dbed
Showing
6 changed files
with
190 additions
and
19 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
148 changes: 148 additions & 0 deletions
148
fuzzing/testdata/contracts/assertions/assert_constant_method.sol
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,148 @@ | ||
| // An assertion failure in the constant method should be detected | ||
| // Contract updated to solc > 0.8.0 and taken from https://github.com/crytic/echidna/blob/5757f8c3c07d0248cbe1728506ff0f8daccbef12/tests/solidity/assert/fullmath.sol | ||
| library FullMath { | ||
| /// @notice Calculates floor(a×b÷denominator) with full precision. Throws if result overflows a uint256 or denominator == 0 | ||
| /// @param a The multiplicand | ||
| /// @param b The multiplier | ||
| /// @param denominator The divisor | ||
| /// @return result The 256-bit result | ||
| /// @dev Credit to Remco Bloemen under MIT license https://xn--2-umb.com/21/muldiv | ||
| function mulDiv( | ||
| uint256 a, | ||
| uint256 b, | ||
| uint256 denominator | ||
| ) internal pure returns (uint256 result) { | ||
| unchecked { | ||
|
|
||
|
|
||
| // 512-bit multiply [prod1 prod0] = a * b | ||
| // Compute the product mod 2**256 and mod 2**256 - 1 | ||
| // then use the Chinese Remainder Theorem to reconstruct | ||
| // the 512 bit result. The result is stored in two 256 | ||
| // variables such that product = prod1 * 2**256 + prod0 | ||
| uint256 prod0; // Least significant 256 bits of the product | ||
| uint256 prod1; // Most significant 256 bits of the product | ||
| assembly { | ||
| let mm := mulmod(a, b, not(0)) | ||
| prod0 := mul(a, b) | ||
| prod1 := sub(sub(mm, prod0), lt(mm, prod0)) | ||
| } | ||
|
|
||
| // Handle non-overflow cases, 256 by 256 division | ||
| if (prod1 == 0) { | ||
| require(denominator > 0); | ||
| assembly { | ||
| result := div(prod0, denominator) | ||
| } | ||
| return result; | ||
| } | ||
|
|
||
| // Make sure the result is less than 2**256. | ||
| // Also prevents denominator == 0 | ||
| require(denominator > prod1); | ||
|
|
||
| /////////////////////////////////////////////// | ||
| // 512 by 256 division. | ||
| /////////////////////////////////////////////// | ||
|
|
||
| // Make division exact by subtracting the remainder from [prod1 prod0] | ||
| // Compute remainder using mulmod | ||
| uint256 remainder; | ||
| assembly { | ||
| remainder := mulmod(a, b, denominator) | ||
| } | ||
| // Subtract 256 bit number from 512 bit number | ||
| assembly { | ||
| prod1 := sub(prod1, gt(remainder, prod0)) | ||
| prod0 := sub(prod0, remainder) | ||
| } | ||
|
|
||
| // Factor powers of two out of denominator | ||
| // Compute largest power of two divisor of denominator. | ||
| // Always >= 1. | ||
| uint256 twos = (0 - denominator) & denominator; | ||
| // Divide denominator by power of two | ||
| assembly { | ||
| denominator := div(denominator, twos) | ||
| } | ||
|
|
||
| // Divide [prod1 prod0] by the factors of two | ||
| assembly { | ||
| prod0 := div(prod0, twos) | ||
| } | ||
| // Shift in bits from prod1 into prod0. For this we need | ||
| // to flip `twos` such that it is 2**256 / twos. | ||
| // If twos is zero, then it becomes one | ||
| assembly { | ||
| twos := add(div(sub(0, twos), twos), 1) | ||
| } | ||
| prod0 |= prod1 * twos; | ||
|
|
||
| // Invert denominator mod 2**256 | ||
| // Now that denominator is an odd number, it has an inverse | ||
| // modulo 2**256 such that denominator * inv = 1 mod 2**256. | ||
| // Compute the inverse by starting with a seed that is correct | ||
| // correct for four bits. That is, denominator * inv = 1 mod 2**4 | ||
| uint256 inv = (3 * denominator) ^ 2; | ||
| // Now use Newton-Raphson iteration to improve the precision. | ||
| // Thanks to Hensel's lifting lemma, this also works in modular | ||
| // arithmetic, doubling the correct bits in each step. | ||
| inv *= 2 - denominator * inv; // inverse mod 2**8 | ||
| inv *= 2 - denominator * inv; // inverse mod 2**16 | ||
| inv *= 2 - denominator * inv; // inverse mod 2**32 | ||
| inv *= 2 - denominator * inv; // inverse mod 2**64 | ||
| inv *= 2 - denominator * inv; // inverse mod 2**128 | ||
| inv *= 2 - denominator * inv; // inverse mod 2**256 | ||
|
|
||
| // Because the division is now exact we can divide by multiplying | ||
| // with the modular inverse of denominator. This will give us the | ||
| // correct result modulo 2**256. Since the precoditions guarantee | ||
| // that the outcome is less than 2**256, this is the final result. | ||
| // We don't need to compute the high bits of the result and prod1 | ||
| // is no longer required. | ||
| result = prod0 * inv; | ||
| return result; | ||
| } | ||
| } | ||
|
|
||
| /// @notice Calculates ceil(a×b÷denominator) with full precision. Throws if result overflows a uint256 or denominator == 0 | ||
| /// @param a The multiplicand | ||
| /// @param b The multiplier | ||
| /// @param denominator The divisor | ||
| /// @return result The 256-bit result | ||
| function mulDivRoundingUp( | ||
| uint256 a, | ||
| uint256 b, | ||
| uint256 denominator | ||
| ) internal pure returns (uint256 result) { | ||
| // BUG | ||
| unchecked { | ||
| return mulDiv(a, b, denominator) + (mulmod(a, b, denominator) > 0 ? 1 : 0); | ||
| } | ||
| } | ||
| } | ||
|
|
||
| contract TestContract { | ||
| function checkMulDivRoundingUp( | ||
| uint256 x, | ||
| uint256 y, | ||
| uint256 d | ||
| ) external pure { | ||
| require(d > 0); | ||
| uint256 z = FullMath.mulDivRoundingUp(x, y, d); | ||
| if (x == 0 || y == 0) { | ||
| assert(z == 0); | ||
| return; | ||
| } | ||
|
|
||
| // recompute x and y via mulDiv of the result of floor(x*y/d), should always be less than original inputs by < d | ||
| uint256 x2 = FullMath.mulDiv(z, d, y); | ||
| uint256 y2 = FullMath.mulDiv(z, d, x); | ||
| assert(x2 >= x); | ||
| assert(y2 >= y); | ||
|
|
||
| assert(x2 - x < d); | ||
| assert(y2 - y < d); | ||
| } | ||
| fallback() external {} | ||
| } |