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

韩宁 等:以太坊中间语言的可执行语义 1721

3 Yul 语言语法的形式化

Yul 语言程序包括代码块、语句、表达式、变量、字面值等构成单位.由于在 Yul 中语句可作为表达式使
用,所以表达式和语句均用类型 expr 进行形式化.该处理简化形式化定义而不影响表达能力.
智能合约在 Yul 语言中表示为代码块.一个代码块由一系列表达式组成.代码块类型 block 由 Blk 构造,提供
一表达式列表作为参量.其形式化定义如下面第一行所示.为突出重点,略去了关键字 datatype 以及类型定义中
的部分内容(后文中往往作类似简化).
block = Blk “expr list”
expr = EId id0|ELit literal|EFunCall id0 “expr list”|
EFunDef id0 “(id0*type_name) list” “(id0*type_name) list”block|
EAssg “id0 list” expr|EIf expr block|EFor block expr block block|...
—‹Intermediate expressions›
EStop|ERetId “(id0*type_name)”|EImLit literal|
EImFunCall id0 “expr list”|ECond expr block|EGasPop|…
表达式类型 expr 有多种构造方式,其中,变量类型 EId id0 表示标识符为(v::id0)的变量.这里,id0 为 int 的别
名,即不同的变量标识符基于不同整数进行构造.字面值类型 ELit literal 表示数值或布尔值常量.其中,literal 类
型包含字面值内容(lit_content 类型)和类型名称(type_name)两部分信息.例如,(TL:L Bool)表示其字面值内容为
TL(真),类型名为 Bool.函数调用类型 EFunCall id0 “expr list”表示对标识符为(f::id0)的函数以某个参数列表(es::
“expr list”)进行调用.函数调用分为内置函数调用和自定义函数调用,根据标识符 f 进行区分.函数定义类型
EFunDef id0 “(id0*type_name) list” “(id0*type_name) list” block 中的 id0 为所定义函数标识符的类型,两个
“(id0*type_name) list”分别为形式参数列表类型和返回值列表的类型,而 block 为函数体的类型(函数体为一代
码块).赋值类型 EAssg “id0 list” expr 表示将某表达式(e::expr)的值赋给某个变量列表(xs::“id0 list”)中变量的赋
值语句.条件表达式类型 EIf expr block 表示在某条件表达式(e::expr)为真时执行某代码块(blk::block)的条件语
句.循环表达式类型 EFor block expr block block 表示具有初始化代码块、条件表达式及后处理代码块的循环语
句(类似 C 语言中的 for 循环).此外,关于变量声明、赋值、分支(switch)等 Yul 语言语法特性的形式化不再赘述.
除 Yul 语言本身的表达式外,本工作定义一系列中间表达式,以支撑语义的形式化.其中,EStop 表示执行结
束;调用返回表达式 ERetId “(id0*type_name)”表示函数调用的返回值需要写入的变量(v::id0)及其类型名(t::
type_name);其他中间表达式 EImLit literal,EImFunCall id0 “expr list”,ECond expr block,EGasPop 等的引入,是为
了保证动态语义中能够正确计算 gas 消耗量.这些中间表达式在 Yul 语言的语法中并不存在,合约编写者无法直
接使用.
4 Yul 语言类型系统的定义和形式化

在 Yul 语言官方文档中,给出了一系列数据类型、函数类型以及变量、函数的直观作用域规则.本工作结合
该文档和实际编译 Yul 程序的实验结果,给出 Yul 语言类型系统(或称静态语义)的完整定义,及其在 Isabelle/
HOL 中的形式化.
4.1 类型检查函数
Yul 语言类型系统的形式化是通过定义类型检查函数进行的.函数 type_e 对表达式进行类型检查,该函数在
给定变量类型环境(vte::type_env)、外层声明变量集合(xs::id0 set)和函数类型环境(fte::ftype_env)下,判断给定表
达式(e::expr)是否为良类型(well-typed),并给出表达式的具体类型以及更新的变量类型环境.函数 type_es 对表
达式列表进行类型检查,该函数在给定变量类型环境(vte::type_env),外层声明变量集合(xs::id0 set)和函数类型
环境(fte::ftype_env)下,判断给定表达式列表(es::expr list)是否为良类型.函数 type_b 在给定变量类型环境(vte::
type_env)、外层声明变量集合(xs::id0 set)和函数类型环境(fte::ftype_env)下判断给定代码块(blk::block)是否为良