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

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

9. let blk′=(n_expr_lst[EGasPush,EGasJump,EGasJumpDest] EGasPush|rtl|) ++ blk blk ++ es post_es in
10. [〈((blk′,(zip(map fst ptl) (map peel es))@rzl,fs′,Some (FunctionV f ptl rtl blk)) B
11. #((if (|rtl|≠0) then (EList(map(λxt.(ERetId xt)) rtl)) else EStop),ls,fs) E #lstk′),gs,ck〉 N ])
12. |Some (CallBuiltinV callgb)⇒(
13. if (callgb∈{Call,CallCode,DelegateCall,Return,Revert,Selfdestruct,Stop,Invalid})
14. then ((step_callbuiltin〈(EImFunCall f es,ls,fs) E #lstk′,gs,ck〉 N callgb lits))
15. else [ ]
16. …
17. )
18. ))
表达式 EImFunCall f es 的执行首先考虑 es 中是否有未完全求值的参数表达式:若有,则在相应上下文中执
行最右侧的未完全求值表达式(第 4 行);否则,按照所调用函数是否为自定义函数作不同描述.
若函数标识符在环境(aggr_fs((EImFunCall f es,ls,fs) E # lstk′))@builtin_ctx 中被映射为形如 FunctionV f ptl
rtl blk 的值(第 8 行),说明所调用函数为自定义函数.此种情况下,向被调函数的函数体 blk 前后分别添加表示调
用时进行跳转和参数入栈所消耗 gas 的表达式以及表示返回时调整栈布局(包括参数和局部变量出栈等操作)
所消耗 gas 的表达式,形成代码块 bl′.在 blk′定义中,使用了代码块与表达式列表的连接符++ es 以及表达式列表
与代码块的连接符++ blk .代码块 blk′放在新的局部栈帧中,准备执行.而调用者栈帧中的表达式置为 if (|rtl|≠0)
then (EList(map(λxt.(ERetId xt)) rtl)) else EStop,表示若返回值个数不为零,则设置相应个数的用于接收返回值
的占位符;否则,函数调用在该栈帧再次成为栈顶时已结束(EStop).
若函数标识符在环境(aggr_fs((EImFunCall f es,ls,fs) E # lstk′))@builtin_ctx 中被映射为形如 CallBuiltinV
callgb(第 12 行),OpBuiltinV callgb,RBuiltinV callgb 等值,则表示所调用函数为相应类型的内置函数.其中,形如
CallBuiltinV callgb 的值表示与外部调用和返回相关的内置函数,具体是哪个函数,由 callgb 表示.若 callgb 在 Yul
所支持的此类内置函数范围内,则借助辅助函数 step_callbuiltin 给出调用的执行结果(略去进一步技术细节);否
则,给出表示出错的空全局栈.其余种类的内置函数调用作类似描述.
若外部调用发生后,被调合约正常终止,则全局栈栈顶为形如〈gs′,ret_data,ck′〉 H 的栈帧(对应图 1(G)).在语义
中,该外部调用返回后的全局栈由 step tre (〈gs′,ret_data,ck′〉 H #gstk′)给出(对某个 gstk′).而该表达式的定义根据外
部调用的种类(对应于太坊中的 CALL 指令、CALLCODE 指令还是 DELEGATECALL 指令),借助不同辅助函数
给出.当外部调用由 CALL 指令触发,即 ck′由 CKCall 构造时,step tre (〈gs′,ret_data,ck′〉 H #gstk′)定义为 callret (〈gs′,
ret_data,ck′〉 H #gstk′),其中,辅助函数 callret 定义如下.
1. callret (〈gs′,ret_data,(CKCall g to val io is oo os)〉 H #〈(Blk(e#es),ls,fs,cf) B #lstk′,gs,ck〉 N #gstk′)
2. =(let … in
3. let flag=if (accs gs to=None) then 0 else 1 in
4. let c_call=Cgascap val flag g (gas gs) in
5. let c=(Cbase val flag)+(Cmem(uint(naws gs)) (uint naws))+(sint c_call) in
6. (〈(Blk((expr_fill_retids e [(extcall_ret_id,((NL 1):L U256))])#es),ls,fs,cf) B #lstk′,
7. (gs (| gas:=(gas gs′)+(gas gs)−(word_of_int c),… |) ),ck〉 N #gstk′))
由于被调合约正常终止,返回值为 1.上述定义中,利用函数 expr_fill_retids 将该返回值写入此前发生调用时
留在全局栈次栈顶中局部栈栈顶表达式中的辅助变量 extcall_ret_id(第 6 行).定义中,第 3 行~第 5 行计算调用
的总 gas 成本 c.返回后,全局状态中的 gas 值更新为当前全局栈中的 gas 值与次栈顶中的 gas 值(即被调合约终
止时的 gas 余量)的和,减去一次调用所消耗的成本 c 所得结果(第 7 行).
关于其他种类外部调用的正常返回、外部调用的异常返回以及所有其他语义规则,不再详细阐释.