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

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

ECond e blk 实现“若表达式 e 求值为真则执行代码块 blk”的分支控制逻辑,但忽略部分 gas 消耗.中间表达式
ECond e blk 的语义规则如下.
1. step tre [〈((ECond e blk,ls,fs) E #lstk′),gs,ck〉 N ]=(
2. case e of
3. (EImLit(TL:L Bool))⇒
4. if (valid (gas gs) (3+3+10) (ct gs))
5. then (let gs′=gs (| gas:=(gas gs)−(word_of_int 16) |) in
6. [〈((blk,[ ],get_func_values blk,None) B #(EStop,ls,fs) E #lstk′),gs′,ck〉 N ])
7. else [〈ck〉 E ]
8. |(EImLit(FL:L Bool))⇒
9. if (valid (gas gs) (3+3+10) (ct gs))
10. then (let gs′=gs (| gas:=(gas gs)−(word_of_int 16) |) in [〈((EGasJumpDest,ls,fs) E #lstk′),gs′,ck〉 N ])
11. else [〈ck〉 E ]
12. |_⇒step_ctx tre e (ECCond Hole blk) [〈((EStop,ls,fs) E #lstk′) gs ck〉 N ]
13. )
故若表达式 e 已求值为字面值(第 3 行、第 8 行),则检查全局状态中 gas 剩余是否能够支持判断条件表达
式真值以及执行条件转移所消耗的 gas 量.若该检查通过,则从全局状态中扣除该消耗量,并在所形成的全局状
态下视 e 为布尔值“真”或“假”执行不同操作:若 e 为布尔值“真”,则在新的局部栈帧(blk,[ ],get_func_values blk,
None) B 中执行代码块 blk;若 e 为布尔值假,则执行表达式 EGasJumpDest,以产生分支逻辑结尾标签(字节码
JUMPDEST)所对应的 gas 消耗.若表达式并非字面值(第 12 行),则借助 step_ctx 函数首先在条件分支上下文
ECCond Hole blk 中对 e 进行小步执行.
条件语句的语义规则将 EIf e blk 的执行转化为 ECond e (blk++ es [EGasJumpDest])的执行,其中,++ es 在代码
块 blk 结束位置添加列表[EGasJumpDest]中的表达式.结合 ECond 表达式的语义,这保证无论条件表达式 e 是否
求值为真,条件分支结束后均发生字节码 JUMPDEST 所引起的 gas 消耗.而循环语句的语义规则将 EFor blk0 e
blk1 blk 的执行转化为下列表达式在新局部栈帧中的执行:
blk0++ blk [EGasJumpDest,ECond e (blk++blk1++ es [EGasPush,EGasJump,EFor(Blk[ ]) e blk1 blk])].
故循环初始化代码块 blk0 首先执行,其中声明的变量在本循环内(对应于新建的局部栈帧)有效.而后产生
字节码标签 JUMPDEST(用于继续循环所需的跳转)所引起的 gas 消耗.此后,若表达式 e 求值为真,则继续执行循
环体 blk 以及进行后处理(post-processing)的代码块 blk1,产生跳转回循环表达式 e 开始处所引起的 gas 消耗,并
继续执行初始化代码块为空的循环 EFor(Blk[ ]) e blk1 blk.
代码块的语义规则给出全局栈 gstk0=〈(Blk es,ls,fs,fg) B #lstk′,gs,ck〉 N #gstk′的单步执行结果.若代码块不为空
(即 es 为非空表达式列表),则根据含有单个栈帧的全局栈[〈(e,ls,fs) E #lstk′,gs,ck〉 N ]的单步执行结果更新全局栈
gstk0,其中,e 为 es 中的第 1 个表达式.若代码块为空(即 es 为空的表达式列表),而局部栈 lstk′不为空,则弹出局部
栈帧(Blk es,ls,fs,fg) B ,表示代码块及其作用域的结束.若代码块为空,且局部栈 lstk′亦为空,则将全局栈帧改为
〈gs1,[ ],ck〉 H ,表示对当前合约调用的结束,其中,gs1 是由全局状态 gs 消耗一定量 gas 得到的全局状态.代码块的
完整语义规则较为复杂,故在此不作展示.
以下对函数调用中栈的变化进行说明.图 1 所示为形如〈lfrm#lstk,…〉 N #gstk 的全局栈完成一次成功的自定
义函数调用,到被调函数执行结束并返回,全局栈和局部栈的主要变化情况.单步执行由实线箭头表示,多步执
行由虚线箭头表示.调用栈的变化部分粗体显示.
考虑局部栈帧 lfrm 中的调用 EFunCall f es 被执行的情形.首先,在第一步执行 A→B 中,实际调用并不发生,
而是将 EFunCall f es 转化为中间表达式 EImFunCall f es,并更新全局状态,扣除实际调用发生前,返回地址入栈
引起的 gas 消耗量(仅在调用自定义函数时为非零值).此时,含有 EImFunCall f es 的局部栈帧为 lfrm′ .而后,视该
0