Page 110 - 《软件学报》2025年第9期

王小兵 等: Solidity 到 MSVL 转换的等价性研究 4021

表 10 Solidity 到 MSVL 的核心转换规则

类型 Solidity程序 MSVL程序
uint public a=0; int a and a<== 0 and skip;
声明语句
uint[] public arr; int arr[MAX] and skip;
struct id{ struct id{
结构体 block s block m
} }
function vote (int id){
function vote(uint id) public{ frame(a) and (
函数 uint a= id; int a and a<== id and skip
} )
};
throw;
skip;
block s ;
function fun(int return_value) {
转向语句 function fun() { frame(return_flag)(
return 0; int return_flag <== 0 and skip;
} return_flag := 1 and return_value:= 0)
};
if(expression){ if(expression) then {
block s block m
条件语句 }else{ }else{
block s block m
} }
while(e1) {
for(statedef;e1;e2){
循环语句 block s block m
e2;
}
}
e1[+, -, *, /, %]e2 e1[+, -, *, /, %]e2
含算术运算符的表达式
e1[++, --] e1:= e1[+, -]1
e1=e2 e1:= e2
含赋值运算符的表达式
e1[+, -, *, /, %]=e2 e1:= e1[+, -, *, /, %]e2
e1&&e2 e1 AND e2
含逻辑运算符的表达式
e1||e2 e1 OR e2

3.2 引理定义
本文在第 2 节定义了 Solidity 状态 µ =< a,σ, M >, 其中网络状态 σ =< b, p,S >. S 表示 storage 存储状态,
storage 用于保存合约的状态变量, M 表示 memory 内存状态, memory 用于保存合约函数内的局部变量. 本文重点
关注 Solidity 语言本身的语法操作, 因此可以认为 Solidity 状态 µ 的改变仅由其存储状态 S 和内存状态 M 决定,
而 MSVL 中无论是状态变量还是局部变量, 均存放在同一内存中, 没有相应的结构可以区分 storage 与 memory.
因此本文从语义逻辑的角度出发, 将 MSVL 内存分为两部分, 记为 mstorage 与 mmemory, 分别对应 Solidity 中的
storage 与 memory. 这两部分对应的 MSVL 内存状态分别记为 s[s] 与 s[m], 当其分别与 Solidity 的存储状态 S 和
M 等价时, 认为 Solidity µ 与 MSVL s 等价时, 即状态等价. 在本节证明过程不对其分别
内存状态 状态 的内存状态
证明.
本文使用函数 α 表示内存注入 [24] , 定义为一个从 Solidity 的 storage 地址 addr 或者 memory 地址 loc 到
MSVL 的存储位置 (bl,δ m ) 的单射函数, 表明 Solidity 程序中的 addr 或者 loc 对应 MSVL 程序中的块索引 bl 和偏
移 δ m .
基于内存注入函数 α, Solidity 中的值 v s 和 MSVL 中的值 v m 的等价关系记为 α ⊢ v s ∼ v m , 定义如下:
α ⊢ c ∼ c,其中v s = v m = c.
● V1
,
● V2 α ⊢ ptr(addr,i s ) ptr(bl,i m ), 其中 v s = ptr(addr,i s ) v m = ptr(bl,i m ), 当且仅当存在 δ m ∈ N 0 满足 α(addr) =