如何使用 Halmos 编写符号测试

如何使用 Halmos 编写符号测试

符号测试看起来与模糊测试相似，但有一些需要理解的差异。本指南将引导你完成编写符号测试的过程，重点介绍与模糊测试相比的差异。它适用于那些已经熟悉 Dapptools-/Foundry-风格的模糊测试的人。如果你之前没有体验过模糊测试，请参考 Foundry 文档 以掌握基本概念。

0. 安装 Halmos

如果你尚未安装 Halmos，请参考安装指南或使用以下命令快速安装：

uv tool install halmos

1. 编写 setUp()

与 Foundry 测试类似，你可以提供 setUp() 函数，该函数将在每次测试之前执行。在 setup 函数中，你可以创建目标合约的实例，并初始化它们的状态。这些初始化的合约随后可用于每个测试。

此外，你还可以使用符号参数调用构造函数，将合约状态初始化为符号状态。你可以使用 Halmos cheatcodes 创建这些符号。

例如，考虑一个基本的 ERC20 代币合约，如下所示：

import {ERC20} from "openzeppelin/token/ERC20/ERC20.sol";

contract MyToken is ERC20 {
    constructor(uint256 initialSupply) ERC20("MyToken", "MT") {
        _mint(msg.sender, initialSupply);
    }
}

然后，你可以编写一个 setUp() 函数，该函数创建一个具有_符号_初始供应量的新代币合约，如下所示：

import {SymTest} from "halmos-cheatcodes/SymTest.sol";
import {Test} from "forge-std/Test.sol";
import {MyToken} from "../src/MyToken.sol";

contract MyTokenTest is SymTest, Test {
    MyToken token;

    function setUp() public {
        uint256 initialSupply = svm.createUint256('initialSupply');
        token = new MyToken(initialSupply);
    }
}

在上面的例子中，svm.createUint256() 是一个符号作弊码，它生成一个 uint256 类型的新符号。重要的是要理解，创建的符号表示 [0, 2^256 - 1] 范围内的所有整数的集合，而不是从该范围中选择的随机值。 <!--Refer to the symbolic execution document to learn more about the concept of symbols.-->

通过使用符号初始供应量，你可以检查给定的测试是否通过所有可能的初始供应量配置，而不仅仅是随机选择的供应量设置。

提示：

• Halmos cheatcodes 可以像任何其他 Solidity 依赖项一样安装：

  forge install a16z/halmos-cheatcodes

• 当前可用的 Halmos cheatcodes 列表可以在这里找到。

2. 编写符号测试

符号测试的结构与模糊测试类似。在大多数情况下，它们遵循下面列出的模式：

function check_<function-name>_<behavior-description> ( <parameters> ) {
    // 指定输入条件
    ...

    // 调用目标合约
    ...

    // 检查输出状态
    ...
}

下面是代币转账函数的示例符号测试：

function check_transfer(address sender, address receiver, uint256 amount) public {
    // 指定输入条件
    vm.assume(receiver != address(0));
    vm.assume(token.balanceOf(sender) >= amount);

    // 记录发送者和接收者的当前余额
    uint256 balanceOfSender = token.balanceOf(sender);
    uint256 balanceOfReceiver = token.balanceOf(receiver);

    // 调用目标合约
    vm.prank(sender);
    token.transfer(receiver, amount);

    // 检查输出状态
    assert(token.balanceOf(sender) == balanceOfSender - amount);
    assert(token.balanceOf(receiver) == balanceOfReceiver + amount);
}

我们将以上述测试为例来解释每个组成部分。

2.1 声明或创建符号输入

与模糊测试类似，你可以为每个测试指定输入参数。

例如，我们的示例测试声明了三个输入参数：sender、receiver 和 amount，如下所示：

function check_transfer(address sender, address receiver, uint256 amount) ...

然而，与模糊测试不同的是，在符号测试中，每个输入参数都被分配一个符号，该符号表示给定类型的所有可能值。在我们的示例中，sender 和 receiver 被分配了一个地址符号，范围从 0x0 到 0xffff...ffff，而 amount 被分配了一个整数符号，范围为 [0, 2^256-1]。

从概念上讲，每个符号测试都代表大量的测试用例，这些测试用例通过将符号替换为每个可能的输入组合来生成。换句话说，它类似于运行一个广泛的循环，如下所示：[^symbolic-execution]

// `check_transfer()` 符号测试的概念效果
for (uint160 sender = 0; sender < type(uint160).max; sender++) {
    for (uint160 receiver = 0; receiver < type(uint160).max; receiver++) {
        for (uint256 amount = 0; amount < type(uint256).max; amount++) {
            check_transfer(address(sender), address(receiver), amount);
        }
    }
}

[^symbolic-execution]: 请注意，在我们的示例中，可能的输入组合的数量是 2^160 * 2^160 * 2^256，并且实际上单独运行所有这些输入在计算上是不可行的。作为一种解决方案，符号测试采用符号执行技术，该技术允许在不实际单独运行所有输入的情况下测试所有输入组合。

提示：

• 除了声明符号输入参数之外，你还可以使用 Halmos cheatcodes 在测试中动态创建符号。例如，我们的运行示例可以重写如下：

  function check_transfer() {
    address sender = svm.createAddress("sender");
    address receiver = svm.createAddress("receiver");
    uint256 amount = svm.createUint256("amount");
    ...
  }

• Halmos 要求动态大小的数组（包括 bytes 和 string）具有固定大小。因此，它们不能声明为输入参数，而需要以编程方式构造。例如，可以使用 svm.createBytes() cheatcode 生成字节数组，如下所示：

  bytes memory data = svm.createBytes(96, 'data');

  类似地，可以创建动态整数数组，如下所示：

  uint256[] memory arr = new uint256[3];
  for (uint i = 0; i < 3; i++) {
    arr[i] = svm.createUint256('element');
  }

  我们计划实现更多的 cheatcodes 和功能，以便更容易地声明或创建动态数组。

2.2 指定输入条件

回想一下，符号测试会考虑所有可能的输入组合。但是，并非所有输入组合都与每个测试场景相关或有效。与模糊测试类似，你可以使用 vm.assume() 来指定有效输入的条件。

在我们的示例中，有效发送者和接收者地址的条件指定如下：

vm.assume(receiver != address(0));
vm.assume(token.balanceOf(sender) >= amount);

与模糊测试一样，任何不满足 assume() 条件的输入组合都会被忽略。这意味着，在执行上述 assume() 语句后，只会考虑接收者非零且发送者有足够余额的输入组合。违反这些条件的其他输入组合将被忽略。

提示：

• 你需要小心，不要通过设置过强的输入条件来排除有效输入。

• 在符号测试中，避免使用 bound()，因为它往往表现不佳。相反，使用 vm.assume()，它更有效并且提高了可读性：

  uint256 tokenId = svm.createUint256("tokenId");
  
  // ❌ 不要这样做
  tokenId = bound(tokenId, 1, MAX_TOKEN_ID);
  
  // ✅ 这样做
  vm.assume(1 <= tokenId && tokenId <= MAX_TOKEN_ID);

2.3 调用目标合约

现在，你可以使用准备好的输入符号调用目标合约。

在我们的示例中，使用符号接收者地址和数量调用 transfer 函数。prank() cheatcode 也用于将 msg.sender 设置为符号发送者地址，如下所示：

vm.prank(sender);
token.transfer(receiver, amount);

提示：

• 如果你的目标是检查目标合约是否在预期条件下还原，则应使用低级调用。即使外部调用失败，这也允许执行继续。下面是对代币转账函数进行低级调用的示例。请注意，返回值 success 随后可用于检查还原条件。

  vm.prank(sender);
  (bool success,) = address(token).call(
    abi.encodeWithSelector(token.transfer.selector, receiver, amount)
  );
  if (!success) {
    // 检查转移失败的条件
  }

2.4 检查输出状态

调用目标合约后，你可以针对合约的输出状态编写断言。

在我们的示例中，提供了以下针对代币合约输出状态的断言：

assert(token.balanceOf(sender) == balanceOfSender - amount);
assert(token.balanceOf(receiver) == balanceOfReceiver + amount);

如果有任何输入违反这些断言，Halmos 将报告这些输入，称为反例。

对于我们的示例，Halmos 将识别发送者地址与接收者地址相同的输入组合。这是因为自我转移不会改变余额，从而导致上述断言无法满足的情况。

提示：

• Halmos 仅关注断言冲突（即，还原为 Panic(1)），而忽略其他还原情况。这意味着 Halmos 不会报告任何导致其他类型还原的输入。例如，在我们的示例中，任何触发 balanceOfReceiver + amount 溢出的输入，或导致外部合约调用失败的输入都将被忽略。为避免忽略此类输入，你可以使用 unchecked 块或低级调用。

• 如果你使用的是旧版本的编译器（< 0.8.0），该编译器使用 INVALID 操作码进行断言冲突，而不是 Panic(1) 错误代码，那么 Halmos 将_不会_报告任何反例。在这种情况下，你需要使用在失败时还原为 Panic(1) 的自定义断言，如下所示：

  function myAssert(bool cond) internal pure {
    if (!cond) {
        assembly {
            mstore(0x00, 0x4e487b71) // Panic()
            mstore(0x20, 0x01)       // 1
            revert(0x1c, 0x24)       // revert Panic(1)
        }
    }
  }

总结

与模糊测试类似，符号测试的结构如下：

• 声明测试输入参数。
• 指定有效输入的条件。
• 调用目标合约。
• 关于预期输出状态的断言。

但是，由于符号测试是以符号方式执行的，因此需要考虑某些行为差异：

• 测试输入被分配为符号，而不是随机值。
• 仅报告断言冲突，即 Panic(1) 错误，而忽略其他错误，如算术溢出。
• vm.assume() cheatcode 的性能优于 bound()。

有关更多见解，请参阅符号测试的示例。

如有任何疑问或进一步讨论，请加入 Halmos Telegram Group。

• 原文链接： github.com/a16z/halmos/b...
• 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～