From c41d54ceea733b7234980742b15e8df0fafeffdb Mon Sep 17 00:00:00 2001 From: sudo rm -rf --no-preserve-root / Date: Thu, 19 Sep 2024 12:58:43 +0200 Subject: [PATCH] =?UTF-8?q?=E2=99=BB=EF=B8=8F=20Use=20Native=20`halmos`=20?= =?UTF-8?q?`createCalldata`=20Cheat=20Code=20(#273)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit ### 🕓 Changelog [`halmos`](https://github.com/a16z/halmos) has released support for the following new cheat codes via PRs [#360](https://github.com/a16z/halmos/pull/360) and (small patch) [#364](https://github.com/a16z/halmos/pull/364): ```solidity createCalldata(string contractName); createCalldata(string contractName, bool includeViewFunctions); createCalldata(string filename, string contractName); createCalldata(string filename, string contractName, bool includeViewFunctions); ``` > Please note that `includeViewFunctions` defaults to `false`, if not provided. This PR refactors the `halmos`-based tests to capitalise on these new cheat codes. To verify the correct behaviour of the Vyper compiler for `view` and `pure` functions, we include read-only functions in the calldata creation. --------- Signed-off-by: Pascal Marco Caversaccio --- CHANGELOG.md | 7 ++ test/halmos.toml | 18 ++-- test/tokens/halmos/ERC1155TestHalmos.t.sol | 96 +++++++--------------- test/tokens/halmos/ERC20TestHalmos.t.sol | 23 +++--- test/tokens/halmos/ERC721TestHalmos.t.sol | 49 +++++------ test/utils/halmos/MathTestHalmos.t.sol | 38 ++++----- 6 files changed, 96 insertions(+), 135 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 492c979b..f0b711ba 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -18,6 +18,13 @@ - [`eip712_domain_separator`](https://github.com/pcaversaccio/snekmate/blob/v0.1.1/src/snekmate/utils/eip712_domain_separator.vy): Use relative `interfaces` `import`s. ([#263](https://github.com/pcaversaccio/snekmate/pull/263)) - [`math`](https://github.com/pcaversaccio/snekmate/blob/v0.1.1/src/snekmate/utils/math.vy): Use mutable `internal` function parameters. ([#267](https://github.com/pcaversaccio/snekmate/pull/267)) +### 🥢 Test Coverage + +- **Tokens** + - [`erc20`](https://github.com/pcaversaccio/snekmate/blob/v0.1.1/src/snekmate/tokens/erc20.vy): Use native `halmos` `createCalldata` cheat code. ([#273](https://github.com/pcaversaccio/snekmate/pull/273)) + - [`erc721`](https://github.com/pcaversaccio/snekmate/blob/v0.1.1/src/snekmate/tokens/erc721.vy): Use native `halmos` `createCalldata` cheat code. ([#273](https://github.com/pcaversaccio/snekmate/pull/273)) + - [`erc1155`](https://github.com/pcaversaccio/snekmate/blob/v0.1.1/src/snekmate/tokens/erc1155.vy): Use native `halmos` `createCalldata` cheat code. ([#273](https://github.com/pcaversaccio/snekmate/pull/273)) + ### 👀 Full Changelog - [`v0.1.0...v0.1.1`](https://github.com/pcaversaccio/snekmate/compare/v0.1.0...v0.1.1) diff --git a/test/halmos.toml b/test/halmos.toml index 5d0faebd..07f2cfac 100644 --- a/test/halmos.toml +++ b/test/halmos.toml @@ -1,14 +1,16 @@ [global] # Test settings. -function = "testHalmos" # Run tests matching the given prefix. -storage-layout = "generic" # Set the generic storage layout model. -early-exit = true # Stop after a counterexample is found. -ffi = true # Enable the foreign function interface (ffi) cheatcode. +function = "testHalmos" # Run tests matching the given prefix. +loop = 5 # Set the loop unrolling bound. +default-bytes-lengths = "0,32,96,1024" # Set the default length candidates for `bytes` and `string` types. +storage-layout = "generic" # Set the generic storage layout model. +ffi = true # Enable the foreign function interface (ffi) cheatcode. # Debugging settings. -statistics = true # Print the statistics. -verbose = 1 # Set the verbosity level for the tests. +verbose = 1 # Set the verbosity level for the tests. +statistics = true # Print the statistics. +early-exit = true # Stop after a counterexample is found. # Solver settings. -solver-command = "yices-smt2" # Use the Yices 2 SMT solver. -cache-solver = true # Cache unsatisfiable queries using unsatisfiable cores. +solver-command = "yices-smt2" # Use the Yices 2 SMT solver. +cache-solver = true # Cache unsatisfiable queries using unsatisfiable cores. diff --git a/test/tokens/halmos/ERC1155TestHalmos.t.sol b/test/tokens/halmos/ERC1155TestHalmos.t.sol index 414d31ea..5e4cf16b 100644 --- a/test/tokens/halmos/ERC1155TestHalmos.t.sol +++ b/test/tokens/halmos/ERC1155TestHalmos.t.sol @@ -6,12 +6,13 @@ import {SymTest} from "halmos-cheatcodes/SymTest.sol"; import {VyperDeployer} from "utils/VyperDeployer.sol"; import {IERC1155} from "openzeppelin/token/ERC1155/IERC1155.sol"; +import {IERC1155MetadataURI} from "openzeppelin/token/ERC1155/extensions/IERC1155MetadataURI.sol"; import {IERC1155Extended} from "../interfaces/IERC1155Extended.sol"; /** - * @dev Sets the timeout (in milliseconds) for solving assertion - * violation conditions; `0` means no timeout. + * @dev Set the timeout (in milliseconds) for solving assertion violation + * conditions; `0` means no timeout. * @custom:halmos --solver-timeout-assertion 0 */ contract ERC1155TestHalmos is Test, SymTest { @@ -25,6 +26,11 @@ contract ERC1155TestHalmos is Test, SymTest { uint256[] private tokenIds; uint256[] private amounts; + /** + * @dev Set the timeout (in milliseconds) for solving branching conditions; + * `0` means no timeout. + * @custom:halmos --solver-timeout-branching 1000 + */ function setUp() public { bytes memory args = abi.encode(_BASE_URI); /** @@ -124,25 +130,32 @@ contract ERC1155TestHalmos is Test, SymTest { vm.stopPrank(); } - function testHalmosAssertNoBackdoor( - bytes4 selector, - address caller, - address other - ) public { + /** + * Set the length of the dynamically-sized arrays in the `IERC1155` interface. + * @custom:halmos --array-lengths ids=5,values=5,amounts=5 + */ + function testHalmosAssertNoBackdoor(address caller, address other) public { + /** + * @dev To verify the correct behaviour of the Vyper compiler for `view` and `pure` + * functions, we include read-only functions in the calldata creation. + */ + bytes memory data = svm.createCalldata( + "IERC1155Extended.sol", + "IERC1155Extended", + true + ); + bytes4 selector = bytes4(data); + /** * @dev Using a single `assume` with conjunctions would result in the creation of * multiple paths, negatively impacting performance. */ vm.assume(caller != other); + vm.assume(selector != IERC1155MetadataURI.uri.selector); + vm.assume(selector != IERC1155Extended.set_uri.selector); vm.assume(selector != IERC1155Extended._customMint.selector); vm.assume(selector != IERC1155Extended.safe_mint.selector); vm.assume(selector != IERC1155Extended.safe_mint_batch.selector); - - /** - * @dev For convenience, ignore `view` functions that use dynamic arrays. - */ - vm.assume(selector != IERC1155.balanceOfBatch.selector); - for (uint256 i = 0; i < holders.length; i++) { vm.assume(!erc1155.isApprovedForAll(holders[i], caller)); } @@ -164,61 +177,8 @@ contract ERC1155TestHalmos is Test, SymTest { ); vm.startPrank(caller); - bool success; - if (selector == IERC1155.safeTransferFrom.selector) { - // solhint-disable-next-line avoid-low-level-calls - (success, ) = token.call( - abi.encodeWithSelector( - selector, - svm.createAddress("owner"), - svm.createAddress("to"), - svm.createUint256("tokenId"), - svm.createUint256("amount"), - svm.createBytes(96, "YOLO") - ) - ); - } else if ( - selector == IERC1155.safeBatchTransferFrom.selector || - selector == IERC1155Extended.burn_batch.selector - ) { - uint256[] memory ids = new uint256[](5); - uint256[] memory values = new uint256[](5); - for (uint256 i = 0; i < ids.length; i++) { - ids[i] = svm.createUint256("ids"); - values[i] = svm.createUint256("values"); - } - bytes memory data = (selector == - IERC1155.safeBatchTransferFrom.selector) - ? abi.encodeWithSelector( - selector, - svm.createAddress("owner"), - svm.createAddress("to"), - ids, - values, - svm.createBytes(96, "YOLO") - ) - : abi.encodeWithSelector( - selector, - svm.createAddress("owner"), - ids, - values - ); - // solhint-disable-next-line avoid-low-level-calls - (success, ) = token.call(data); - } else if (selector == IERC1155Extended.set_uri.selector) { - // solhint-disable-next-line avoid-low-level-calls - (success, ) = token.call( - abi.encodeWithSelector( - selector, - svm.createUint256("id"), - svm.createBytes(96, "uri") - ) - ); - } else { - bytes memory args = svm.createBytes(1_024, "WAGMI"); - // solhint-disable-next-line avoid-low-level-calls - (success, ) = address(token).call(abi.encodePacked(selector, args)); - } + // solhint-disable-next-line avoid-low-level-calls + (bool success, ) = token.call(data); vm.assume(success); vm.stopPrank(); diff --git a/test/tokens/halmos/ERC20TestHalmos.t.sol b/test/tokens/halmos/ERC20TestHalmos.t.sol index 7437cd6a..a4c70b8d 100644 --- a/test/tokens/halmos/ERC20TestHalmos.t.sol +++ b/test/tokens/halmos/ERC20TestHalmos.t.sol @@ -8,8 +8,8 @@ import {VyperDeployer} from "utils/VyperDeployer.sol"; import {IERC20} from "openzeppelin/token/ERC20/IERC20.sol"; /** - * @dev Sets the timeout (in milliseconds) for solving assertion - * violation conditions; `0` means no timeout. + * @dev Set the timeout (in milliseconds) for solving assertion violation + * conditions; `0` means no timeout. * @custom:halmos --solver-timeout-assertion 0 */ contract ERC20TestHalmos is Test, SymTest { @@ -25,8 +25,8 @@ contract ERC20TestHalmos is Test, SymTest { address[] private holders; /** - * @dev Sets timeout (in milliseconds) for solving branching - * conditions; `0` means no timeout. + * @dev Set the timeout (in milliseconds) for solving branching conditions; + * `0` means no timeout. * @custom:halmos --solver-timeout-branching 1000 */ function setUpSymbolic(uint256 initialSupply_) public { @@ -86,12 +86,7 @@ contract ERC20TestHalmos is Test, SymTest { * @notice Forked and adjusted accordingly from here: * https://github.com/a16z/halmos/blob/main/examples/tokens/ERC20/test/ERC20Test.sol. */ - function testHalmosAssertNoBackdoor( - bytes4 selector, - address caller, - address other - ) public { - bytes memory args = svm.createBytes(1_024, "WAGMI"); + function testHalmosAssertNoBackdoor(address caller, address other) public { vm.assume(other != caller); uint256 oldBalanceOther = erc20.balanceOf(other); @@ -99,7 +94,13 @@ contract ERC20TestHalmos is Test, SymTest { vm.startPrank(caller); // solhint-disable-next-line avoid-low-level-calls - (bool success, ) = token.call(abi.encodePacked(selector, args)); + (bool success, ) = token.call( + /** + * @dev To verify the correct behaviour of the Vyper compiler for `view` and `pure` + * functions, we include read-only functions in the calldata creation. + */ + svm.createCalldata("IERC20Extended.sol", "IERC20Extended", true) + ); vm.assume(success); vm.stopPrank(); diff --git a/test/tokens/halmos/ERC721TestHalmos.t.sol b/test/tokens/halmos/ERC721TestHalmos.t.sol index 28cf42ba..f8173631 100644 --- a/test/tokens/halmos/ERC721TestHalmos.t.sol +++ b/test/tokens/halmos/ERC721TestHalmos.t.sol @@ -6,12 +6,13 @@ import {SymTest} from "halmos-cheatcodes/SymTest.sol"; import {VyperDeployer} from "utils/VyperDeployer.sol"; import {IERC721} from "openzeppelin/token/ERC721/IERC721.sol"; +import {IERC721Metadata} from "openzeppelin/token/ERC721/extensions/IERC721Metadata.sol"; import {IERC721Extended} from "../interfaces/IERC721Extended.sol"; /** - * @dev Sets the timeout (in milliseconds) for solving assertion - * violation conditions; `0` means no timeout. + * @dev Set the timeout (in milliseconds) for solving assertion violation + * conditions; `0` means no timeout. * @custom:halmos --solver-timeout-assertion 0 */ contract ERC721TestHalmos is Test, SymTest { @@ -29,8 +30,8 @@ contract ERC721TestHalmos is Test, SymTest { uint256[] private tokenIds; /** - * @dev Sets timeout (in milliseconds) for solving branching - * conditions; `0` means no timeout. + * @dev Set the timeout (in milliseconds) for solving branching conditions; + * `0` means no timeout. * @custom:halmos --solver-timeout-branching 1000 */ function setUp() public { @@ -95,16 +96,24 @@ contract ERC721TestHalmos is Test, SymTest { * @notice Forked and adjusted accordingly from here: * https://github.com/a16z/halmos/blob/main/examples/tokens/ERC721/test/ERC721Test.sol. */ - function testHalmosAssertNoBackdoor( - bytes4 selector, - address caller, - address other - ) public { + function testHalmosAssertNoBackdoor(address caller, address other) public { + /** + * @dev To verify the correct behaviour of the Vyper compiler for `view` and `pure` + * functions, we include read-only functions in the calldata creation. + */ + bytes memory data = svm.createCalldata( + "IERC721Extended.sol", + "IERC721Extended", + true + ); + bytes4 selector = bytes4(data); + /** * @dev Using a single `assume` with conjunctions would result in the creation of * multiple paths, negatively impacting performance. */ vm.assume(caller != other); + vm.assume(selector != IERC721Metadata.tokenURI.selector); vm.assume(selector != IERC721Extended._customMint.selector); vm.assume(selector != IERC721Extended.safe_mint.selector); for (uint256 i = 0; i < holders.length; i++) { @@ -118,26 +127,8 @@ contract ERC721TestHalmos is Test, SymTest { uint256 oldBalanceOther = erc721.balanceOf(other); vm.startPrank(caller); - bool success; - if ( - selector == - bytes4(keccak256("safeTransferFrom(address,address,uint256,bytes)")) - ) { - // solhint-disable-next-line avoid-low-level-calls - (success, ) = token.call( - abi.encodeWithSelector( - selector, - svm.createAddress("owner"), - svm.createAddress("to"), - svm.createUint256("tokenId"), - svm.createBytes(96, "YOLO") - ) - ); - } else { - bytes memory args = svm.createBytes(1_024, "WAGMI"); - // solhint-disable-next-line avoid-low-level-calls - (success, ) = address(token).call(abi.encodePacked(selector, args)); - } + // solhint-disable-next-line avoid-low-level-calls + (bool success, ) = token.call(data); vm.assume(success); vm.stopPrank(); diff --git a/test/utils/halmos/MathTestHalmos.t.sol b/test/utils/halmos/MathTestHalmos.t.sol index b15b7845..01b414a3 100644 --- a/test/utils/halmos/MathTestHalmos.t.sol +++ b/test/utils/halmos/MathTestHalmos.t.sol @@ -11,8 +11,8 @@ import {FixedPointMathLib} from "solady/utils/FixedPointMathLib.sol"; import {IMath} from "../interfaces/IMath.sol"; /** - * @dev Sets the timeout (in milliseconds) for solving assertion - * violation conditions; `0` means no timeout. + * @dev Set the timeout (in milliseconds) for solving assertion violation + * conditions; `0` means no timeout. * @custom:halmos --solver-timeout-assertion 0 */ contract MathTestHalmos is Test, SymTest { @@ -21,8 +21,8 @@ contract MathTestHalmos is Test, SymTest { IMath private math; /** - * @dev Sets timeout (in milliseconds) for solving branching - * conditions; `0` means no timeout. + * @dev Set the timeout (in milliseconds) for solving branching conditions; + * `0` means no timeout. * @custom:halmos --solver-timeout-branching 1000 */ function setUp() public { @@ -65,9 +65,9 @@ contract MathTestHalmos is Test, SymTest { } /** - * @dev Currently commented out, as the timeout for the Z3 solver does not work for - * the queries of this test, where the Z3 solver is constantly running and consumes - * a lot of memory, causing the CI to crash due to out of memory. + * @dev Currently commented out, as the timeout for the Yices 2 SMT solver does not + * work for the queries of this test, where the Yices 2 SMT solver is constantly + * running and consumes a lot of memory, causing the CI to crash due to out of memory. */ // function testHalmosAssertMulDiv( // uint256 x, @@ -112,27 +112,27 @@ contract MathTestHalmos is Test, SymTest { } /** - * @dev Currently commented out, as the timeout for the Z3 solver does not work for - * the queries of this test, where the Z3 solver is constantly running and consumes - * a lot of memory, causing the CI to crash due to out of memory. + * @dev Currently commented out, as the timeout for the Yices 2 SMT solver does not + * work for the queries of this test, where the Yices 2 SMT solver is constantly + * running and consumes a lot of memory, causing the CI to crash due to out of memory. */ // function testHalmosAssertWadLn(int256 x) public view { // assertEq(math.wad_ln(x), FixedPointMathLib.lnWad(x)); // } /** - * @dev Currently commented out, as the timeout for the Z3 solver does not work for - * the queries of this test, where the Z3 solver is constantly running and consumes - * a lot of memory, causing the CI to crash due to out of memory. + * @dev Currently commented out, as the timeout for the Yices 2 SMT solver does not + * work for the queries of this test, where the Yices 2 SMT solver is constantly + * running and consumes a lot of memory, causing the CI to crash due to out of memory. */ // function testHalmosAssertWadExp(int256 x) public view { // assertEq(math.wad_exp(x), FixedPointMathLib.expWad(x)); // } /** - * @dev Currently commented out, as the timeout for the Z3 solver does not work for - * the queries of this test, where the Z3 solver is constantly running and consumes - * a lot of memory, causing the CI to crash due to out of memory. + * @dev Currently commented out, as the timeout for the Yices 2 SMT solver does not + * work for the queries of this test, where the Yices 2 SMT solver is constantly + * running and consumes a lot of memory, causing the CI to crash due to out of memory. */ // function testHalmosAssertCbrt(uint256 x, bool roundup) public view { // if (!roundup) { @@ -146,9 +146,9 @@ contract MathTestHalmos is Test, SymTest { // } /** - * @dev Currently commented out, as the timeout for the Z3 solver does not work for - * the queries of this test, where the Z3 solver is constantly running and consumes - * a lot of memory, causing the CI to crash due to out of memory. + * @dev Currently commented out, as the timeout for the Yices 2 SMT solver does not + * work for the queries of this test, where the Yices 2 SMT solver is constantly + * running and consumes a lot of memory, causing the CI to crash due to out of memory. */ // function testHalmosAssertWadCbrt(uint256 x) public view { // assertEq(math.wad_cbrt(x), FixedPointMathLib.cbrtWad(x));