Solidity 0.6.9 版本发布公告

Solidity v0.6.9 为 solc-js 添加了 SMT 检查功能，允许calldata 用于所有变量，并提供了一种指定导入目录的机制。

请注意，solc-js / soljson 二进制文件包含内置的 Z3 SMT 求解器，这会导致二进制文件大小增加。

重要的新功能

SMTChecker

The SMTChecker 是 Solidity 编译器的一个组件，已经开发了一段时间了。

其目标是将形式化验证方法引入 Solidity 编译器。Solidity 实现了一种基于 SMT/Horn 求解的形式化验证方法。SMTChecker 模块会自动尝试证明代码是否满足由 require/assert 语句给出的规范。SMTChecker 还会自动检查算术下溢/上溢、琐碎条件、不可达代码以及弹出空存储数组。

到目前为止，SMTChecker 缺乏一种简单易用的方法。困难在于它需要将 SMT 求解器编译或链接到编译器中。为了解决这个问题，我们现在将包含已编译的 Z3 SMT 求解器的 solc-js 随附发布。这意味着您可以直接使用 SMTChecker 以及所有使用 solc-js 的工具 - 包括 Remix！

下面，您将找到一个简单的示例合约，其中显示了上溢检查报告。如果您将其复制粘贴到 Remix 中，它将显示错误。

// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.6.9;
pragma experimental SMTChecker;

contract Token {
  mapping(address => uint) balances;
  address owner;
  constructor () public { owner = msg.sender; }
  function transfer(address recipient, uint amount) public {
    // If we comment out the next line, SMTChecker
    // will complain about underflow.
    require(balances[msg.sender] >= amount);
    balances[msg.sender] -= amount;
    // SMTChecker detects a possible overflow in the next line
    // and even provides example inputs:
    // Warning: Overflow (resulting value larger than 2**256 - 1) happens here
    // for:
    // <result> = 2**256
    // amount = 1
    // balances[msg.sender] = 0
    // balances[recipient] = 2**256 - 1
    balances[recipient] += amount;
  }
  function mint(address recipient, uint amount) public {
      require(msg.sender == owner);
      balances[recipient] += amount;
  }
}

该组件还可以分析更复杂的情况，包括来自外部调用者的可能的调用链，如下面的错误状态机示例所示

// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.6.9;
pragma experimental SMTChecker;

contract StateMachine {
    enum State { Init, End }
    State state;
    uint[] a;

    constructor() public {
        state = State.Init;
        a.push();
    }

    function move() public {
        require(state == State.Init);
        state = State.End;
        a.pop();
    }

    function reset() public {
        require(state == State.End);
        state = State.Init;
        a.pop();
    }
}

一系列 3 个交易（部署、move、reset）会导致弹出空数组，此时 SMTChecker 会报告

browser/state_machine.sol:24:9: Warning: Empty array "pop" detected here.
        a.pop();
        ^-----^

请注意，SMTChecker 会向 SMT 求解器发出多个查询，这可能需要一些时间，因为它是一个计算量很大的过程。

Calldata 变量

您现在可以在任何地方使用 calldata 作为引用变量的数据位置，而不仅仅是在外部函数中。请注意，由于 EVM 不允许修改 calldata，因此您不能在 calldata 中创建新值或将某些内容复制到 calldata 中。

// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.6.9;

contract C {
  address[] owners;
  function addOwners(address[] calldata _newOwners) public {
    // We pass _newOwners on as a calldata array.
    checkUnique(_newOwners);
    for (uint i = 0; i < _newOwners.length; i++)
      owners.push(_newOwners[i]);
  }
  /// This internal function can iterate over the calldata array.
  /// Creating a copy in memory is not required.
  function checkUnique(address[] calldata _newOwners) internal pure {
    for (uint i = 0; i < _newOwners.length; i++)
      for (uint j = i + 1; j < _newOwners.length; j++)
        require(_newOwners[i] != _newOwners[j]);
  }
}

使用 calldata 变量的好处是它节省了从 calldata 到内存的复制，并且您可以确保数组或结构体不会被修改。

通常，ABI 解码器在将 calldata 复制到内存时会对整个 calldata 执行范围检查，以避免格式错误的 calldata 造成任何问题。请注意，当对嵌套的 calldata 结构体或数组使用 calldata 变量时，这些检查将仅在您访问它们时执行。

BasePath

通过在 solc 和 solcjs 中引入 --base-path 选项，我们希望导入更容易使用。

如果您运行 solc --base-path ./contracts/ ./contracts/MainContract.sol 并且该文件包含 import "./OtherContract.sol";，Solidity 编译器将自动搜索 ./contracts/OtherContract.sol 并导入它。

虽然这听起来像是一个非常琐碎的功能，但我们希望您仍然喜欢它！

另请注意，如果您使用 --base-path，则基本路径本身将不会包含在任何元数据工件中，您只会获得从基本路径开始的相对路径。

完整变更日志

语言特性

• 允许 calldata 位置用于所有变量。
• NatSpec: 支持状态变量上的 NatSpec 注释。
• Yul: EVM 指令 pc() 被标记为已弃用，将在下一个重大版本中删除。

编译器特性

• 构建系统: 将 soljson.js 构建更新到 emscripten 1.39.15 和 boost 1.73.0，并包含 Z3 以支持集成 SMTChecker，无需回调机制。
• 构建系统: 将 emscripten 构建从 fastcomp 后端切换到上游后端。
• 代码生成器: 不要为小的编译器例程引入新的内部源引用。
• 命令行界面: 添加新选项 --base-path PATH 以使用给定路径作为源树的根目录（默认为文件系统的根目录）。
• SMTChecker: 支持数组 length。
• SMTChecker: 支持数组 push 和 pop。
• SMTChecker: 对 BitVectors 和按位 and 运算符提供通用支持。

错误修复

此版本包含许多次要的、与安全无关的错误修复。相应的错误不会影响生成的字节码（的正确性）。

您可以在 Solidity 错误 json 文件 中跟踪所有重要的、与安全相关的错误。

• 代码生成器: 在某些数组复制操作上触发正确的未实现错误。
• 命令行界面: 修复在使用 --assemble 或 --yul 选项以及 --machine ewasm 但未指定 --yul-dialect 时发生的内部错误。
• NatSpec: 遇到空行时终止 DocString 块。
• 优化器: 修复了 BlockDeDuplicator 中的一个错误。
• 扫描器: 修复当两个空 NatSpec 注释导致扫描超过 EOL 时的错误。
• SMTChecker: 修复带参数的 try/catch 子句中的内部错误。
• SMTChecker: 修复对定点变量应用算术运算符时的内部错误。
• SMTChecker: 修复在分支内部对索引访问赋值时的内部错误。
• SMTChecker: 修复在状态变量初始化中使用函数调用对布尔表达式进行短路时的内部错误。
• 类型检查器: 禁止对类型为 mapping 的存储变量进行赋值。
• 类型检查器: 禁止不可命名的类型的内联数组。
• 类型检查器: 禁止对非公共状态变量使用 override。
• 类型检查器: 修复访问数组切片成员时的内部编译器错误。
• 类型检查器: 修复从内联汇编中向前引用非字面常量时的内部编译器错误。
• 类型检查器: 修复尝试解码过大的静态数组时的内部编译器错误。
• 类型检查器: 修复在引用重写函数但不调用它时出现的错误编译器错误。

最后但并非最不重要的是，一如既往，我们要感谢所有帮助使此版本成为可能的贡献者！

您可以在此处下载 Solidity 的新版本。