Page 154 - 《软件学报》2021年第6期

1728 Journal of Software 软件学报 Vol.32, No.6, June 2021

5.3 测 试
本工作中,开发了由 120 个简单 Yul 语言程序组成的测试集(test suite),对形式化语义进行了测试.测试用例
的分布覆盖了已形式化的 Yul 语言的全部语言特性(字面值、变量、变量声明和赋值、函数定义和调用、各种
控制流结构、代码块等)以及内置函数.内置函数的测试分为 5 类,分别针对关于逻辑操作的内置函数、关于算
术操作的内置函数、关于内存与存储的内置函数、关于执行与控制的内置函数和关于区块链状态查询与哈希
值计算的内置函数.
采取白盒测试的思路,使测试用例覆盖语义函数 step 和 step_ctx 定义中的所有顶层情形,并尽可能覆盖每种
情形中的子情形以及 step,step_ctx 中所调用辅助函数中的各种情形.例如,if 语句的测试覆盖 3 种情况:条件成立
时、条件不成立时、条件表达式不是布尔字面值因而需要进一步求值时.再如函数调用的测试覆盖内置函数调
用、自定义函数调用、外部函数调用、内部函数调用及调用函数后正常返回和异常返回.
对每个测试用例,在 Isabelle/HOL 中使用 value 命令,在某个交易环境下,从某个全局栈开始对语义进行执
行.为观察多步执行的结果,基于语义函数 step 定义了多步执行函数 multi_step.一个在测试中对表达式进行多步
执行的例子是:
value “multi_step tre0 gstk_EIf 4”.
该命令在交易环境 tre0 下,从全局栈 gstk_EIf 开始进行 4 步执行,其中,全局栈 gstk_EIf 形如:
[〈[(EIf(ELit(TL:L Bool))(Blk[ ]),ls0,[ ]) E ],gs0,CKDummy〉 N ].
最后,在 Isabelle/HOL 中定义辅助函数,对每个测试中 Yul 语言程序的执行结果进行检查,包括结果的全局
栈帧形式、所计算数值、gas 消耗量等方面.本工作所定义的形式化语义通过了 120 个测试用例的测试.
5.4 对break,continue和leave的支持
本工作对 Yul 语言的形式化不包含用于细粒度循环控制的 break,continue 语句以及用于退出当前函数的
leave 语句.本节讨论如何在语义形式化中加入对这 3 个语句的支持.
首先,leave 语句的语义规则可将当前代码块置为空,从而引发当前局部栈帧的弹出,以反映从当前函数退
出的动作;其次,为形式化 break 的语义,可在局部栈帧中记录当前最内层循环退出后需要执行的代码,并在 break
的语义规则中将当前控制状态改为该代码;最后,为形式化 continue 的语义,可在局部栈帧中记录当前最内层循
环的后处理(post-processing)部分开始时仍需执行的代码,并在 continue 的语义规则中将当前控制状态改为该代
码.在语义形式化中,支持 break,continue,leave 不会造成实质性的技术难度,但会使语义状态的构成及其在语义
规则中的维护更加复杂.

6 代币合约案例

本节通过一个用于管理代币(token)的实用智能合约,演示 Yul 语言合约的类型检查和小步执行.在以太坊
中,为了给代币智能合约提供一个特征与接口的标准而推出 ERC20 标准 [39] .本节案例中的合约遵循该标准,故
可称为 ERC20 代币合约.
6.1 代币合约
用于演示的代币合约名为 MyToken,其主要功能包括代币余额查询、代币转账等.该合约总共有 19 个函数,
其中有 6 个接口函数,以下是对接口函数的介绍,其中所涉及的用户账户由账户地址表示.
(1) 函数 totalSupply:返回当前的代币发行总量;
(2) 函数 balanceOf:返回给定用户账户 account 的代币余额;
(3) 函数 allowance:返回当前允许指定账户 by 从指定账户 from 取出代币的额度;
(4) 函数 approve:将允许指定账户 spender 从本账户(即调用该函数的账户)提取代币的总额度更新为指定
值 amount;
(5) 函数 transfer:从本账户(即调用者账户)向指定账户 to 转移数量为 amount 的代币,并在本账户余额不