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

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

示异常状态的全局栈帧只包括外部调用类型(ck::call_kind);表示合约执行终止状态的全局栈帧包括全局状态
(gs::gstate)、返回数据(ret_data::“(8 word) list”)和外部调用类型(ck::call_kind).以下依次介绍全局栈帧的 3 个组
成部分,即局部栈、全局状态和外部调用类型.
1) 局部栈(类型为 lstack)用来跟踪同一合约内部因函数调用或执行局部代码块所产生的作用域变化.每
一个局部栈帧(类型为 lstack_frame)记录当前作用域相关信息.局部栈帧由符号 lfrm 表示,有两种可能
形态:包含表达式形态的局部栈帧(e,ls,fs) E 和包含代码块形态的局部栈帧(blk,ls,fs,cf) B .包含表达式的
局部栈帧记录的信息有表达式(e::expr)、变量状态(ls)和函数状态(fs);包含代码块的局部栈帧记录的
信息有代码块(blk::block)、变量状态(ls)、函数状态(fs)和判断当前是否为自定义函数调用的标志(cf::
cflag).其中,变量状态 ls 记录每个变量的当前值,形式化为变量标识符和值所组成二元组的列表,其类
型为“literal list_map”.函数状态 fs 将当前作用域内可调用的函数标识符映射到其函数定义(表示为
fvalue 类型的值),将其形式化为函数标识符和值(即函数的语义表示)所组成二元组的列表,类型为
“fvalue list_map”.由于可调用的内置函数不随作用域变化,故函数状态 fs 中不包括内置函数信息.标
志(cf::cflag)有两种可能的取值:若本局部栈帧记录由函数调用所产生的局部作用域相关信息,则 cf 为
被调函数的 fvalue 值;若本局部栈帧记录由执行局部代码块所形成的局部作用域相关信息,则 cf 为空;
2) 全局状态(类型为 gstate)记录属于整个合约调用、而非合约的某个内部调用的状态信息.具体包括当
前地址 addr、发送方地址 saddr、交易时的转移金额 money、交易的输入数据 input、本地内存 mem、
内存中的活跃字数 naws、当前账户中可用的 gas 数量 gas、记录当前字栈的大小 ct、所有账户的状
态 accs(由账户地址到账户状态的映射,反映每个账户的余额、代码、存储)、退还的余额 refund、日
志列表 logs 和自杀集 ss;
3) 外部调 用类 型(ck::call_kind)给出 了形成 全局栈 帧的 外部调 用的 类型,包括 CKCall,CKDelCall,
CKCallCode 和 CKDummy,分别对应于以太坊指令 CALL,DELEGATECALL,CALLCODE 所引发调用以
及当前全局栈帧为栈底元素的情况.
5.2 语义规则

本节围绕赋值、条件语句、循环语句、代码块以及函数调用和返回说明 Yul 语言语义规则的要点.
赋值的语义规则如下.
1 step tre [〈((xs::=e,ls,fs) E #lstk′),gs,ck〉 N ]=(
2 case e of
3 EImLit lit⇒(
4 let new_lstk=upd_var_in_lstack((EStop,ls,fs) E #lstk′) (xs!0) lit in
5 if (valid (gas_of gs) (5*(size xs)) (ct_of gs))
6 then (let gs′=gs (| gas:=(gas gs)−(word_of_int(5*(int(size xs)))) |) in [〈new_lstk,gs′,ck〉 N ])
7 else [〈ck〉 E ])
8 |EList es⇒…
9 |_⇒step_ctx tre e(ECAssg xs Hole) [〈((EStop,ls,fs) E #lstk′),gs,ck〉 N ])
其中,表达式 e 形如 EImLit lit 对应于赋值右侧表达式已经求值完毕、且结果为单个字面值的情形(第 3 行
开始).此时使用辅助函数 upd_var_in_lstack 将右侧表达式的求值结果 lit 写入局部栈最靠近栈顶且定义域中含
有变量 xs!0(xs 中的首个变量)的变量状态中,形成更新的局部栈 new_lstk.若当前 gas 剩余能够支撑赋值操作的
gas 消耗,则从前者中扣除后者,形成新的全局状态 gs′;反之,抛出异常.其次,表达式 e 形如 EList es 的情形对应于
将值列表赋给变量列表的情形(第 8 行).值列表中实际包含某函数返回的一系列字面值.此时,对局部栈以及 gas
剩余的更新操作类似于第 1 种情况.若表达式 e 不具备上述两种形式中的任何一种,则 e 为尚未求值完全的表达
式(第 9 行).此时,借助 step_ctx 函数首先在赋值上下文 ECAssg xs Hole 中对 e 进行小步执行.
条件语句和循环语句的语义均借助中间表达式 ECond e blk 进行定义.类似分支语句 EIf e blk,中间表达式