将失败的属性测试导入 Foundry

为什么？

当你有一个失败的 Echidna/Medusa 测试时，调用痕迹中显示的输出有时不足以理解问题所在，因此创建一个 foundry 单元测试可以让你以更高的详细级别（-vvv）检查调用痕迹，以找出你的测试究竟在哪里失败。

Foundry 单元测试的运行速度比 Echidna/Medusa 作业要快得多，因此如果你有一个单元测试破坏了你的属性，你可以使用它轻松测试修复代码后是否解决了问题，而不是可能需要等待几个小时的 Echidna/Medusa 运行来测试相同的调用痕迹。

定义不变性

我们将使用启动 新 Foundry 项目 时设置的默认 Foundry 模板，该模板创建以下 Counter 合约：

contract Counter {
    uint256 public number;

    function setNumber(uint256 newNumber) public {
        number = newNumber;
    }

    function increment() public {
        number++;
    }
}

在用 Recon 搭建测试套件后，我们可以在 Properties 合约中定义以下简单的不变性：

function invariant_neverZero() public returns (bool) {
        return counter.number() != 0;
}

这个不变性仅说明 Counter 中 number 状态变量的值永远不为 0。很明显，由于 setNumber 中没有条件语句，模糊器只需要调用 setNumber(0) 就能破坏不变性。

运行模糊器

Medusa

使用 Medusa 运行我们的属性测试，它在 3 秒内找到违反并给出以下输出：

破坏不变性的 Medusa 调用痕迹

从这里我们只需复制从“模糊器停止，测试结果如下...”开始的日志，我们将粘贴到 Recon Medusa 工具 的 Paste Medusa Logs Here 文本框中。

Echidna

使用 Echidna 运行我们的属性测试，它同样迅速地破坏了不变性，并给出以下输出：

我们从“invariant_neverZero: failed!”那一行复制这些日志，粘贴到 Recon Echidna 工具 的 Paste Echidna Logs Here 文本框中。

创建测试

使用日志，Recon 将为使用的模糊器生成一个 Foundry 单元测试：

使用上述 Medusa 日志生成的测试

使用上述 Echidna 日志生成的测试

我们可以看到 Foundry 测试复制了在 Echidna/Medusa 日志中生成的调用序列。

我们还可以在 Add a Prefix for your convenience 文本框中添加前缀。这将输入值附加到测试名称的末尾：

添加作为前缀的失败

前缀被添加到测试名称的末尾

这些可以很方便地添加到 Recon 为我们创建的 CryticToFoundry 合约中。将不变性测试中的相同断言添加到这些单元测试中，可以让我们以更易于运行的格式重复单元测试的功能：

// medusa 测试：重命名以去掉 invariant_ 前缀，以免混淆 foundry 把它作为不变性测试运行
function test_neverZero() public {
        counter_setNumber(0);
        t(counter.number() != 0, "number can be 0");
}

// echidna 测试
function test_prefix_0() public {
        counter_setNumber(0);
        t(counter.number() != 0, "number can be 0");
}

运行这些测试时，我们得到断言违反，导致测试失败：

Medusa 测试

Echidna 测试

使用 -vvv 的详细级别标志运行我们的测试，可以得到比 Echidna/Medusa 日志中提供的更详细的调用痕迹描述，这导致我们断言失败：

修复错误

我们现在可以使用这个单元测试修复 Counter 合约中破坏我们不变性的那一行：

function setNumber(uint256 newNumber) public {
        // 添加条件语句以不允许更改数字为 0
        if(newNumber != 0) {
            number = newNumber;
        }
}

我们可以使用我们的单元测试快速验证我们确实已经解决了问题：

在生产代码库中，这将为我们节省时间，因为 Echidna/Medusa 的运行通常比 Foundry 单元测试需要更长的时间。此外，现在由于这个单元测试是我们测试套件的一部分，我们可以将其添加到 Counter 合约的测试文件中，以便在每次运行测试时执行，从而确保未来的任何更改不会再次导致该不变性被破坏。

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