SMTChecker 和形式化验证
使用形式化验证，可以对您的源代码进行自动的数学证明，以验证其是否满足特定的形式化规范。规范仍然是形式化的（就像源代码一样），但通常更简单。
请注意，形式化验证本身只能帮助您了解所做内容（规范）与做事方式（实际实现）之间的差异。您仍然需要检查规范是否符合您的预期，以及是否错过了规范的任何意外影响。
Solidity 实现了基于 SMT (Satisfiability Modulo Theories) 和 Horn 求解的形式化验证方法。SMTChecker 模块会自动尝试证明代码是否满足由 require 和 assert 语句给出的规范。也就是说，它将 require 语句视为假设，并尝试证明 assert 语句中的条件始终为真。如果发现断言失败，则可能会向用户提供一个反例，说明如何违反断言。如果 SMTChecker 对某个属性没有给出警告，则表示该属性是安全的。
SMTChecker 在编译时检查的其他验证目标是
算术下溢和上溢。
除零。
平凡条件和不可达代码。
弹出空数组。
超出边界索引访问。
转账资金不足。
上述所有目标在默认情况下都会自动检查，前提是所有引擎都已启用，除了 Solidity >=0.8.7 的下溢和上溢。
SMTChecker 可能报告的潜在警告是
<failing property> happens here.。这意味着 SMTChecker 证明了某个属性失败。可能会提供一个反例，但在复杂情况下，它也可能不显示反例。在某些情况下，此结果也可能是假阳性，当 SMT 编码对 Solidity 代码进行抽象时，这些代码要么难以表达，要么根本无法表达。<failing property> might happen here。这意味着求解器在给定的超时时间内无法证明任何一种情况。由于结果未知，SMTChecker 报告潜在的失败以保证健壮性。这可以通过增加查询超时时间来解决，但问题也可能只是对引擎来说过于复杂而无法解决。
要启用 SMTChecker，您必须选择 要运行哪个引擎，默认情况下不启用任何引擎。选择引擎将在所有文件上启用 SMTChecker。
注意
在 Solidity 0.8.4 之前，启用 SMTChecker 的默认方法是通过 pragma experimental SMTChecker;，并且只有包含此编译指示的合约才会被分析。该编译指示已被弃用，尽管它仍然出于向后兼容性而启用 SMTChecker，但它将在 Solidity 0.9.0 中被移除。另请注意，现在即使在一个文件中使用编译指示也会对所有文件启用 SMTChecker。
注意
对于验证目标，没有收到警告代表对正确性的无可争议的数学证明，假设 SMTChecker 和底层求解器中没有错误。请记住，这些问题在一般情况下非常困难，有时甚至不可能自动解决。因此，某些属性可能无法解决，或者可能导致大型合约出现假阳性。每个经过证明的属性都应视为一项重要的成就。对于高级用户，请参阅 SMTChecker 调整 了解一些可能有助于证明更复杂属性的选项。
教程
溢出
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.8.0;
contract Overflow {
uint immutable x;
uint immutable y;
function add(uint x_, uint y_) internal pure returns (uint) {
return x_ + y_;
}
constructor(uint x_, uint y_) {
(x, y) = (x_, y_);
}
function stateAdd() public view returns (uint) {
return add(x, y);
}
}
上面的合约显示了溢出检查示例。对于 Solidity >=0.8.7，SMTChecker 默认情况下不会检查下溢和上溢，因此我们需要使用命令行选项 --model-checker-targets "underflow,overflow" 或 JSON 选项 settings.modelChecker.targets = ["underflow", "overflow"]。请参阅 有关目标配置的这部分。在这里，它报告以下内容
Warning: CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
Counterexample:
x = 1, y = 115792089237316195423570985008687907853269984665640564039457584007913129639935
= 0
Transaction trace:
Overflow.constructor(1, 115792089237316195423570985008687907853269984665640564039457584007913129639935)
State: x = 1, y = 115792089237316195423570985008687907853269984665640564039457584007913129639935
Overflow.stateAdd()
Overflow.add(1, 115792089237316195423570985008687907853269984665640564039457584007913129639935) -- internal call
--> o.sol:9:20:
|
9 | return x_ + y_;
| ^^^^^^^
如果我们添加 require 语句来过滤掉溢出情况，SMTChecker 将证明没有溢出可以访问（通过不报告警告）
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.8.0;
contract Overflow {
uint immutable x;
uint immutable y;
function add(uint x_, uint y_) internal pure returns (uint) {
return x_ + y_;
}
constructor(uint x_, uint y_) {
(x, y) = (x_, y_);
}
function stateAdd() public view returns (uint) {
require(x < type(uint128).max);
require(y < type(uint128).max);
return add(x, y);
}
}
断言
断言代表代码中的不变式：必须始终为真的属性，对于所有交易，包括所有输入和存储值，否则存在错误。
下面的代码定义了一个函数 f，它保证不会发生溢出。函数 inv 定义了规范，即 f 严格单调递增：对于所有可能的对 (a, b)，如果 b > a 那么 f(b) > f(a)。由于 f 确实是严格单调递增的，因此 SMTChecker 证明了我们的属性是正确的。我们鼓励您尝试更改属性和函数定义，以查看结果。
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.8.0;
contract Monotonic {
function f(uint x) internal pure returns (uint) {
require(x < type(uint128).max);
return x * 42;
}
function inv(uint a, uint b) public pure {
require(b > a);
assert(f(b) > f(a));
}
}
我们还可以添加循环内的断言来验证更复杂的属性。以下代码在无限制的数字数组中搜索最大元素，并断言找到的元素必须大于或等于数组中的每个元素。
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.8.0;
contract Max {
function max(uint[] memory a) public pure returns (uint) {
uint m = 0;
for (uint i = 0; i < a.length; ++i)
if (a[i] > m)
m = a[i];
for (uint i = 0; i < a.length; ++i)
assert(m >= a[i]);
return m;
}
}
请注意，在此示例中，SMTChecker 将自动尝试证明三个属性
++i在第一个循环中不会溢出。++i在第二个循环中不会溢出。断言始终为真。
注意
这些属性涉及循环，这使得它比之前的示例难得多得多，因此请小心循环！
所有属性都已正确证明安全。您可以随意更改属性和/或添加数组的限制以查看不同的结果。例如，将代码更改为
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.8.0;
contract Max {
function max(uint[] memory a) public pure returns (uint) {
require(a.length >= 5);
uint m = 0;
for (uint i = 0; i < a.length; ++i)
if (a[i] > m)
m = a[i];
for (uint i = 0; i < a.length; ++i)
assert(m > a[i]);
return m;
}
}
会得到
Warning: CHC: Assertion violation happens here.
Counterexample:
a = [0, 0, 0, 0, 0]
= 0
Transaction trace:
Test.constructor()
Test.max([0, 0, 0, 0, 0])
--> max.sol:14:4:
|
14 | assert(m > a[i]);
状态属性
到目前为止，这些示例仅展示了 SMTChecker 在纯代码上的使用，证明了特定操作或算法的属性。智能合约中常见的一种属性是涉及合约状态的属性。可能需要多个交易才能使此类属性的断言失败。
例如，考虑一个 2D 网格，其中两个轴的坐标范围为 (-2^128, 2^128 - 1)。让我们将一个机器人放置在 (0, 0) 位置。机器人只能对角线移动，一次一步，并且不能移动到网格之外。机器人的状态机可以用下面的智能合约来表示。
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.8.0;
contract Robot {
int x = 0;
int y = 0;
modifier wall {
require(x > type(int128).min && x < type(int128).max);
require(y > type(int128).min && y < type(int128).max);
_;
}
function moveLeftUp() wall public {
--x;
++y;
}
function moveLeftDown() wall public {
--x;
--y;
}
function moveRightUp() wall public {
++x;
++y;
}
function moveRightDown() wall public {
++x;
--y;
}
function inv() public view {
assert((x + y) % 2 == 0);
}
}
函数 inv 代表状态机的一个不变式，即 x + y 必须是偶数。SMTChecker 设法证明，无论我们对机器人发出多少命令，即使是无限多个命令，不变式也永远不会失败。有兴趣的读者可能也想手动证明这一事实。提示：这个不变式是归纳式的。
我们还可以欺骗 SMTChecker，让它告诉我们到达我们认为可能可达的某个位置的路径。我们可以添加一个属性，即 (2, 4) 不可达，方法是添加以下函数。
function reach_2_4() public view {
assert(!(x == 2 && y == 4));
}
这个属性是错误的，在证明该属性错误的同时，SMTChecker 会告诉我们如何到达 (2, 4)
Warning: CHC: Assertion violation happens here.
Counterexample:
x = 2, y = 4
Transaction trace:
Robot.constructor()
State: x = 0, y = 0
Robot.moveLeftUp()
State: x = (- 1), y = 1
Robot.moveRightUp()
State: x = 0, y = 2
Robot.moveRightUp()
State: x = 1, y = 3
Robot.moveRightUp()
State: x = 2, y = 4
Robot.reach_2_4()
--> r.sol:35:4:
|
35 | assert(!(x == 2 && y == 4));
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^
请注意，上面的路径不一定是确定的，因为还有其他路径可以到达 (2, 4)。显示哪个路径的选择可能会根据所使用的求解器、它的版本或随机性而改变。
外部调用和重入
SMTChecker 将每个外部调用都视为对未知代码的调用。这样做的理由是，即使被调用合约的代码在编译时可用，也不能保证部署的合约与编译时接口来自的合约完全相同。
在某些情况下，可以自动推断出状态变量的属性，这些属性即使在被调用代码可以执行任何操作（包括重新进入调用者合约）的情况下仍然为真。
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.8.0;
interface Unknown {
function run() external;
}
contract Mutex {
uint x;
bool lock;
Unknown immutable unknown;
constructor(Unknown u) {
require(address(u) != address(0));
unknown = u;
}
modifier mutex {
require(!lock);
lock = true;
_;
lock = false;
}
function set(uint x_) mutex public {
x = x_;
}
function run() mutex public {
uint xPre = x;
unknown.run();
assert(xPre == x);
}
}
上面的示例展示了一个使用互斥锁标志来禁止重入的合约。求解器能够推断出，当调用 unknown.run() 时，合约已经被“锁定”，因此无论未知调用的代码做什么，都不可能改变 x 的值。
如果我们“忘记”在函数 set 上使用 mutex 修饰符，SMTChecker 能够合成外部调用代码的行为，导致断言失败。
Warning: CHC: Assertion violation happens here.
Counterexample:
x = 1, lock = true, unknown = 1
Transaction trace:
Mutex.constructor(1)
State: x = 0, lock = false, unknown = 1
Mutex.run()
unknown.run() -- untrusted external call, synthesized as:
Mutex.set(1) -- reentrant call
--> m.sol:32:3:
|
32 | assert(xPre == x);
| ^^^^^^^^^^^^^^^^^
SMTChecker 选项和调优
超时
SMTChecker 使用一个针对每个求解器选择的硬编码资源限制 (rlimit)，它与时间没有直接关系。我们选择 rlimit 选项作为默认值，因为它比求解器内部的时间提供了更多确定性保证。
这个选项大致相当于每个查询“几秒钟的超时”。当然，许多属性非常复杂，需要大量时间才能解决，此时确定性并不重要。如果 SMTChecker 无法使用默认的 rlimit 解决合约属性，可以通过 CLI 选项 --model-checker-timeout <time> 或 JSON 选项 settings.modelChecker.timeout=<time> 以毫秒为单位提供超时时间，其中 0 表示没有超时。
验证目标
SMTChecker 创建的验证目标类型也可以通过 CLI 选项 --model-checker-target <targets> 或 JSON 选项 settings.modelChecker.targets=<targets> 进行自定义。在 CLI 情况下，<targets> 是一个无空格逗号分隔的列表，包含一个或多个验证目标，而 JSON 输入中则是一个或多个字符串形式的目标数组。代表目标的关键字如下：
断言：
assert。算术下溢：
underflow。算术上溢：
overflow。除以零：
divByZero。平凡条件和不可达代码：
constantCondition。从空数组弹出元素：
popEmptyArray。数组/固定字节索引访问越界：
outOfBounds。转账资金不足：
balance。以上所有：
default（仅限 CLI）。
例如，一个常见的目标子集可能是：--model-checker-targets assert,overflow。
默认情况下会检查所有目标，除了 Solidity >=0.8.7 中的下溢和上溢。
关于如何以及何时拆分验证目标没有精确的启发式方法，但在处理大型合约时它可能很有用。
已验证目标
如果有任何已验证目标，SMTChecker 会为每个引擎发出一个警告，说明验证了多少个目标。如果用户希望查看所有具体的已验证目标，可以使用 CLI 选项 --model-checker-show-proved 和 JSON 选项 settings.modelChecker.showProved = true。
未验证目标
如果有任何未验证目标，SMTChecker 会发出一个警告，说明有多少个未验证目标。如果用户希望查看所有具体的未验证目标，可以使用 CLI 选项 --model-checker-show-unproved 和 JSON 选项 settings.modelChecker.showUnproved = true。
不支持的语言特性
某些 Solidity 语言特性不受 SMTChecker 应用的 SMT 编码完全支持，例如汇编块。不支持的构造通过过度逼近进行抽象以保持健壮性，这意味着任何报告为安全的属性都是安全的，即使此特性不受支持。但是，这种抽象可能会在目标属性依赖于不支持特性的精确行为时导致假阳性。如果编码器遇到这种情况，默认情况下会报告一个通用警告，说明它遇到了多少个不支持的特性。如果用户希望查看所有具体的不支持的特性，可以使用 CLI 选项 --model-checker-show-unsupported 和 JSON 选项 settings.modelChecker.showUnsupported = true，它们的默认值为 false。
已验证合约
默认情况下，给定源代码中的所有可部署合约都会被单独分析，作为要部署的合约。这意味着，如果一个合约有许多直接和间接继承父类，它们都会被单独分析，即使只有最派生的合约可以直接在区块链上访问。这会给 SMTChecker 和求解器带来不必要的负担。为了帮助解决这种情况，用户可以指定哪些合约应该被分析为部署的合约。当然，父合约仍然会被分析，但只在最派生合约的上下文中分析，从而降低了编码和生成的查询的复杂性。请注意，抽象合约默认情况下不会被 SMTChecker 分析为最派生的。
所选合约可以通过 CLI 中的 <source>:<contract> 对的逗号分隔列表（不允许使用空格）给出：--model-checker-contracts "<source1.sol:contract1>,<source2.sol:contract2>,<source2.sol:contract3>"，以及 JSON 输入 中的对象 settings.modelChecker.contracts，它具有以下形式
"contracts": {
"source1.sol": ["contract1"],
"source2.sol": ["contract2", "contract3"]
}
受信任的外部调用
默认情况下，SMTChecker 不会假设编译时可用的代码与外部调用的运行时代码相同。以以下合约为例
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.8.0;
contract Ext {
uint public x;
function setX(uint _x) public { x = _x; }
}
contract MyContract {
function callExt(Ext _e) public {
_e.setX(42);
assert(_e.x() == 42);
}
}
当调用 MyContract.callExt 时，会给出一个地址作为参数。在部署时，我们无法确定地址 _e 实际上是否包含合约 Ext 的部署。因此，SMTChecker 会警告说上面的断言可能会被违反，如果 _e 包含除 Ext 之外的其他合约，这将是正确的。
但是，将这些外部调用视为受信任的可能很有用，例如，测试接口的不同实现是否符合相同的属性。这意味着假设地址 _e 确实是作为合约 Ext 部署的。可以通过 CLI 选项 --model-checker-ext-calls=trusted 或 JSON 字段 settings.modelChecker.extCalls: "trusted" 启用此模式。
请注意，启用此模式可能会使 SMTChecker 分析的计算成本更高。
此模式的一个重要部分是，它应用于合约类型和对合约的高级外部调用，而不是低级调用，例如 call 和 delegatecall。地址的存储是按合约类型存储的，SMTChecker 假设外部调用的合约具有调用者表达式的类型。因此，将 address 或合约强制转换为不同的合约类型将产生不同的存储值，如果假设不一致，例如以下示例，可能会导致不正确的结果
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.8.0;
contract D {
constructor(uint _x) { x = _x; }
uint public x;
function setX(uint _x) public { x = _x; }
}
contract E {
constructor() { x = 2; }
uint public x;
function setX(uint _x) public { x = _x; }
}
contract C {
function f() public {
address d = address(new D(42));
// `d` was deployed as `D`, so its `x` should be 42 now.
assert(D(d).x() == 42); // should hold
assert(D(d).x() == 43); // should fail
// E and D have the same interface, so the following
// call would also work at runtime.
// However, the change to `E(d)` is not reflected in `D(d)`.
E(d).setX(1024);
// Reading from `D(d)` now will show old values.
// The assertion below should fail at runtime,
// but succeeds in this mode's analysis (unsound).
assert(D(d).x() == 42);
// The assertion below should succeed at runtime,
// but fails in this mode's analysis (false positive).
assert(D(d).x() == 1024);
}
}
因此，确保对 address 或 contract 类型的特定变量的受信任外部调用始终具有相同的调用者表达式类型。
在继承的情况下，将调用合约的变量强制转换为最派生类型的类型也有帮助。
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.8.0;
interface Token {
function balanceOf(address _a) external view returns (uint);
function transfer(address _to, uint _amt) external;
}
contract TokenCorrect is Token {
mapping (address => uint) balance;
constructor(address _a, uint _b) {
balance[_a] = _b;
}
function balanceOf(address _a) public view override returns (uint) {
return balance[_a];
}
function transfer(address _to, uint _amt) public override {
require(balance[msg.sender] >= _amt);
balance[msg.sender] -= _amt;
balance[_to] += _amt;
}
}
contract Test {
function property_transfer(address _token, address _to, uint _amt) public {
require(_to != address(this));
TokenCorrect t = TokenCorrect(_token);
uint xPre = t.balanceOf(address(this));
require(xPre >= _amt);
uint yPre = t.balanceOf(_to);
t.transfer(_to, _amt);
uint xPost = t.balanceOf(address(this));
uint yPost = t.balanceOf(_to);
assert(xPost == xPre - _amt);
assert(yPost == yPre + _amt);
}
}
请注意，在函数 property_transfer 中，外部调用是在变量 t 上执行的。
此模式的另一个注意事项是对分析合约外部的合约类型状态变量的调用。在下面的代码中，即使 B 部署了 A，存储在 B.a 中的地址也可能在对 B 本身的交易之间被 B 之外的任何人调用。为了反映对 B.a 的可能更改，编码允许对 B.a 进行无限制的外部调用。编码将跟踪 B.a 的存储，因此断言 (2) 应该成立。但是，目前编码允许从 B 概念上进行此类调用，因此断言 (3) 失败。从逻辑上增强编码是受信任模式的扩展，目前正在开发中。请注意，编码不跟踪 address 变量的存储，因此如果 B.a 的类型为 address，编码将假设它的存储在对 B 的交易之间不会改变。
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.8.0;
contract A {
uint public x;
address immutable public owner;
constructor() {
owner = msg.sender;
}
function setX(uint _x) public {
require(msg.sender == owner);
x = _x;
}
}
contract B {
A a;
constructor() {
a = new A();
assert(a.x() == 0); // (1) should hold
}
function g() public view {
assert(a.owner() == address(this)); // (2) should hold
assert(a.x() == 0); // (3) should hold, but fails due to a false positive
}
}
报告的推断归纳不变式
对于使用 CHC 引擎证明为安全的属性，SMTChecker 可以检索由 Horn 求解器作为证明一部分推断的归纳不变式。目前，只有两种类型的变式可以报告给用户
合约不变式：这些是关于合约状态变量的属性，在合约可能运行的任何交易之前和之后都为真。例如，
x >= y，其中x和y是合约的状态变量。重入属性：它们代表合约在存在对未知代码的外部调用时的行为。这些属性可以表示在外部调用之前和之后状态变量的值之间的关系，其中外部调用可以自由执行任何操作，包括对分析的合约进行重入调用。带撇号的变量表示在上述外部调用之后状态变量的值。例如：
lock -> x = x'。
用户可以使用 CLI 选项 --model-checker-invariants "contract,reentrancy" 或在 JSON 输入 中的字段 settings.modelChecker.invariants 中作为数组来选择要报告的不变式类型。默认情况下，SMTChecker 不报告不变式。
带松弛变量的除法和取模
Spacer 是 SMTChecker 使用的默认 Horn 求解器，它通常不喜欢 Horn 规则中的除法和取模运算。因此，默认情况下，Solidity 除法和取模运算使用约束 a = b * d + m 来编码，其中 d = a / b 和 m = a % b。但是，其他求解器，例如 Eldarica，更喜欢语法精确的操作。命令行标志 --model-checker-div-mod-no-slacks 和 JSON 选项 settings.modelChecker.divModNoSlacks 可用于根据使用的求解器偏好切换编码。
Natspec 函数抽象
某些函数，包括常见的数学方法，例如 pow 和 sqrt，可能过于复杂，无法以完全自动化的方式进行分析。这些函数可以使用 Natspec 标记进行注释，这些标记指示 SMTChecker 应该抽象这些函数。这意味着函数体不会被使用，并且在调用时，该函数将
返回一个非确定性值，如果抽象的函数是视图/纯函数，则保持状态变量不变，否则还将状态变量设置为非确定性值。这可以通过注释
/// @custom:smtchecker abstract-function-nondet来使用。充当一个未解释函数。这意味着忽略函数的语义（由函数体给出），而该函数唯一的属性是，对于相同的输入，它保证相同的输出。目前这项功能还在开发中，可以通过注释
/// @custom:smtchecker abstract-function-uf来使用。
模型检查引擎
SMTChecker 模块实现了两种不同的推理引擎：有界模型检查器 (BMC) 和约束 Horn 子句 (CHC) 系统。这两个引擎目前都处于开发阶段，并且具有不同的特性。这些引擎是独立的，每个属性警告都说明了它是来自哪个引擎。请注意，上面所有带有反例的示例都是由 CHC 报告的，CHC 是功能更强大的引擎。
默认情况下，两个引擎都使用，其中 CHC 首先运行，每个未被证明的属性都会传递给 BMC。你可以通过 CLI 选项 --model-checker-engine {all,bmc,chc,none} 或 JSON 选项 settings.modelChecker.engine={all,bmc,chc,none} 来选择特定的引擎。
有界模型检查器 (BMC)
BMC 引擎单独分析函数，也就是说，在分析每个函数时，它不会考虑合约在多个交易中的整体行为。循环目前也在该引擎中被忽略。内部函数调用会被内联，只要它们不是递归的，无论是直接还是间接。如果可能，外部函数调用会被内联。可能受重入影响的知识会被清除。
上述特性使得 BMC 容易报告误报，但它也很轻量级，应该能够快速找到小的本地错误。
约束 Horn 子句 (CHC)
合约的控制流图 (CFG) 被建模为一个 Horn 子句系统，其中合约的生命周期由一个循环表示，该循环可以非确定性地访问每个公共/外部函数。这样，在分析任何函数时，都会考虑到整个合约在无限次交易中的行为。循环得到该引擎的完全支持。内部函数调用得到支持，外部函数调用假设被调用的代码是未知的，并且可以执行任何操作。
CHC 引擎在证明能力方面比 BMC 强大得多，并且可能需要更多计算资源。
SMT 和 Horn 求解器
上面详细介绍的两个引擎都使用自动定理证明器作为其逻辑后端。BMC 使用 SMT 求解器，而 CHC 使用 Horn 求解器。通常同一个工具可以充当两者，如 z3，它主要是一个 SMT 求解器，并且提供 Spacer 作为 Horn 求解器，以及 Eldarica，它两者都做。
用户可以通过 CLI 选项 --model-checker-solvers {all,cvc4,eld,smtlib2,z3} 或 JSON 选项 settings.modelChecker.solvers=[smtlib2,z3] 来选择应该使用哪些求解器（如果可用），其中
cvc4仅在solc二进制文件使用它编译时才可用。只有 BMC 使用cvc4。eld通过其二进制文件使用，该二进制文件必须安装在系统中。只有 CHC 使用eld，并且仅在未启用z3时才使用。smtlib2以 smtlib2 格式输出 SMT/Horn 查询。这些可以与编译器的 回调机制 一起使用，以便可以使用系统中的任何求解器二进制文件同步地将查询的结果返回给编译器。这可以由 BMC 和 CHC 根据调用的求解器使用。z3可用如果
solc使用它编译；如果在 Linux 系统中安装了版本 >=4.8.x 的动态
z3库（从 Solidity 0.7.6 开始）；静态地在
soljson.js中（从 Solidity 0.6.9 开始），即编译器的 JavaScript 二进制文件。
注意
z3 版本 4.8.16 中断了与先前版本的 ABI 兼容性，不能与 solc <=0.8.13 一起使用。如果你使用 z3 >=4.8.16，请使用 solc >=0.8.14，反之，仅使用较旧的 z3 与较旧的 solc 版本。我们还建议使用最新的 z3 版本，这也是 SMTChecker 所使用的版本。
由于 BMC 和 CHC 都使用 z3，并且 z3 在多种环境中可用，包括在浏览器中，因此大多数用户几乎永远不需要关心此选项。更高级的用户可能会将此选项应用于更复杂的问题以尝试使用其他求解器。
请注意，某些选择的引擎和求解器组合会导致 SMTChecker 什么也不做，例如选择 CHC 和 cvc4。
抽象和误报
SMTChecker 以不完全且健全的方式实现抽象：如果报告了错误，则该错误可能是由抽象引入的误报（由于清除知识或使用不精确的类型）。如果它确定验证目标是安全的，那么它确实是安全的，也就是说，没有误报（除非 SMTChecker 中存在错误）。
如果无法证明目标，你可以尝试使用上一节中的调优选项来帮助求解器。如果你确定是误报，则在代码中添加带有更多信息的 require 语句，也可以为求解器提供更多能力。
SMT 编码和类型
SMTChecker 编码试图尽可能精确，将 Solidity 类型和表达式映射到其最接近的 SMT-LIB 表示，如下表所示。
Solidity 类型 |
SMT 排序 |
理论 |
|---|---|---|
布尔值 |
Bool |
Bool |
intN, uintN, address, bytesN, enum, contract |
整数 |
LIA, NIA |
数组, 映射, 字节, 字符串 |
元组（数组元素，整数长度） |
数据类型, 数组, LIA |
结构体 |
元组 |
数据类型 |
其他类型 |
整数 |
LIA |
尚不支持的类型由一个 256 位无符号整数进行抽象，其中不支持的操作将被忽略。
有关 SMT 编码如何在内部工作的更多详细信息，请参阅论文 SMT-based Verification of Solidity Smart Contracts。
函数调用
在 BMC 引擎中，如果可能，对同一个合约（或基合约）的函数调用会被内联，也就是说，当它们的实现可用时。即使其他合约中的函数代码可用，也不会对它们进行内联，因为我们无法保证实际部署的代码是相同的。
CHC 引擎创建非线性 Horn 子句，这些子句使用被调用函数的摘要来支持内部函数调用。外部函数调用被视为对未知代码的调用，包括潜在的重入调用。
复杂的纯函数由一个关于参数的未解释函数 (UF) 进行抽象。
函数 |
BMC/CHC 行为 |
|---|---|
|
验证目标。 |
|
假设。 |
内部调用 |
BMC：内联函数调用。CHC：函数摘要。 |
对已知代码的外部调用 |
BMC：内联函数调用或清除有关状态变量和本地存储引用的知识。CHC：假设被调用的代码是未知的。尝试推断调用返回后持有的不变式。 |
存储数组推送/弹出 |
精确支持。检查它是否正在弹出空数组。 |
ABI 函数 |
使用 UF 进行抽象。 |
|
精确支持。 |
|
使用 UF 进行抽象。 |
无实现的纯函数（外部或复杂） |
使用 UF 抽象 |
无实现的外部函数 |
BMC：清除状态信息并假设结果是非确定性的。 CHC：非确定性摘要。尝试推断调用返回后保持不变的不变式。 |
转账 |
BMC：检查合约余额是否足够。 CHC：尚未执行检查。 |
其他 |
当前不支持 |
使用抽象意味着失去精确的知识，但在很多情况下并不意味着失去证明能力。
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.8.0;
contract Recover
{
function f(
bytes32 hash,
uint8 v1, uint8 v2,
bytes32 r1, bytes32 r2,
bytes32 s1, bytes32 s2
) public pure returns (address) {
address a1 = ecrecover(hash, v1, r1, s1);
require(v1 == v2);
require(r1 == r2);
require(s1 == s2);
address a2 = ecrecover(hash, v2, r2, s2);
assert(a1 == a2);
return a1;
}
}
在上面的示例中，SMTChecker 的表达能力不足以实际计算 ecrecover，但通过将函数调用建模为未解释函数，我们知道在对等效参数调用时返回值是相同的。这足以证明上面的断言始终为真。
可以使用 UF 抽象已知为确定性的函数调用，并且可以轻松地用于纯函数。然而，对于一般的外部函数来说，这样做很困难，因为它们可能依赖于状态变量。
引用类型和别名
Solidity 对具有相同数据位置的引用类型实现别名。这意味着一个变量可以通过对同一数据区域的引用进行修改。SMTChecker 不会跟踪哪些引用指向相同的数据。这意味着每当分配一个引用类型的本地引用或状态变量时，都会清除有关相同类型和数据位置的变量的所有信息。如果类型是嵌套的，则知识清除还包括所有前缀基本类型。
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.8.0;
contract Aliasing
{
uint[] array1;
uint[][] array2;
function f(
uint[] memory a,
uint[] memory b,
uint[][] memory c,
uint[] storage d
) internal {
array1[0] = 42;
a[0] = 2;
c[0][0] = 2;
b[0] = 1;
// Erasing knowledge about memory references should not
// erase knowledge about state variables.
assert(array1[0] == 42);
// However, an assignment to a storage reference will erase
// storage knowledge accordingly.
d[0] = 2;
// Fails as false positive because of the assignment above.
assert(array1[0] == 42);
// Fails because `a == b` is possible.
assert(a[0] == 2);
// Fails because `c[i] == b` is possible.
assert(c[0][0] == 2);
assert(d[0] == 2);
assert(b[0] == 1);
}
function g(
uint[] memory a,
uint[] memory b,
uint[][] memory c,
uint x
) public {
f(a, b, c, array2[x]);
}
}
在分配给 b[0] 之后，我们需要清除关于 a 的知识，因为它具有相同的类型 (uint[]) 和数据位置（内存）。我们还需要清除关于 c 的知识，因为它的基本类型也是内存中的 uint[]。这意味着某些 c[i] 可能与 b 或 a 指向相同的数据。
请注意，我们不会清除关于 array 和 d 的知识，因为它们位于存储中，即使它们也具有类型 uint[]。但是，如果 d 被分配，我们需要清除关于 array 的知识，反之亦然。
合约余额
如果部署交易中的 msg.value > 0，则可以将合约与发送给它的资金一起部署。但是，合约的地址可能在部署之前已经拥有资金，这些资金由合约保留。因此，SMTChecker 假设在构造函数中 address(this).balance >= msg.value，以与 EVM 规则一致。如果，合约的余额也可能在没有触发对合约的任何调用时增加
selfdestruct由另一个合约执行，并将分析的合约作为剩余资金的目标，合约是某个区块的 coinbase（即
block.coinbase）。
为了正确地模拟这一点，SMTChecker 假设在每次新交易中，合约的余额至少可以增加 msg.value。
现实世界假设
一些场景可以在 Solidity 和 EVM 中表达，但实际上预计永远不会发生。其中一个情况是动态存储数组的长度在 push 期间溢出：如果 push 操作应用于长度为 2^256 - 1 的数组，它的长度会静默溢出。但是，这种情况在实践中不太可能发生，因为将数组增长到该点的所需操作需要数十亿年才能执行。SMTChecker 做出的另一个类似假设是地址的余额永远不会溢出。
类似的想法在EIP-1985中提出。