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

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

( l r ) l r
i
表示当前状态, 且有 s i = s , s , s (x) 表示变量 x 在 s i 状态下的存储位置, s (x) 表示 x 在 s i 状态下的值, 是区间
i i i i
σ i−1 包含的状态个数, 亦可记作 |σ i−1 |. 程序起始格局为 co 0 = (P m ,ϵ, s 0 ,0) , 终止格局为 co f = (true,σ,∅,|σ|+1). 令 ↣
∗ +
,
表示在相同状态内格局间的变化关系, co ↣ co 表示格局 co 在同一状态下经过多步转换为格局 co co ↣ co 表示
′
′
′
∗ +
至少一步. 令 → 表示不同状态下格局间的变化, → 表示不同状态下格局间经过多步发生的变化, → 表示至少一
步. 令 V 为变量的集合, D 为所有类型数据的集合, N 0 为非负整数的集合. 对于表达式 exp, 其格局为四元组
l
l
(exp,σ i−1 , s i ,i). 左值表达式的求值规则为 (la,σ i−1 , s i ,i) ⇒ (bl,δ), 表示左值表达式 la 的存储位置是 s (la) = (bl,δ), 其
i
中 bl 表示内存块索引, 是一个表示地址的整数, δ 表示块内字节偏移量. 右值表达式的求值规则为 (ra,σ i−1 , s i ,i) ⇓ n,
表示右值表达式 ra 的值为 n.
表 1 为 MSVL 的左值表达式求值规则, 其中 sizeof(τ) 表示类型 的存储大小, type(a) 表示表达式 a 的类型,
τ
field_offset(v φ ,φ) 表示结构体成员列表 φ 中名称为 v φ 的成员变量距结构体首地址的偏移量, ptr(bl,δ) 表示指向存
储位置 (bl,δ) 的指针值, 布尔值处理为整数. 规则 L1 处理变量, L2 和 L3 处理数组元素, L4 和 L5 处理结构体成员,
L6 处理指针解引用.

表 1 左值表达式求值规则

序号 求值规则
l
L1 (id,σ i−1 , s i ,i) ⇒ s (id)
l
i
l
(ra,σ i−1 , s i ,i) ⇓ v(id,σ i−1 , s i ,i) ⇒ (bl,δ)
L2 其中,τ为id[ra]的类型
l ( )
(id[ra],σ i−1 , s i ,i) ⇒ bl,δ+v·sizeof(τ)
l
(ra 1 ,σ i−1 , s i ,i) ⇓ v 1 (ra 2 ,σ i−1 , s i ,i) ⇓ v 2 (id,σ i−1 , s i ,i) ⇒ (bl,δ)
L3 其中,n表示数组id的列数,τ为id[ra 1 ][ra 2 ]的类型
l ( )
(id[ra 1 ][ra 2 ],σ i−1 , s i ,i) ⇒ bl,δ+(v 1 ·n+v 2 )·sizeof(τ)
l
(la,σ i−1 , s i ,i) ⇒ (bl,δ)
L4 type(la) = struct id{φ}field_offset(v φ ,φ) = δ ′
( ) l
la.v φ ,σ i−1 , s i ,i ⇒ (bl,δ+δ )
′
(pt,σ i−1 , s i ,i) ⇓ ptr(bl,δ)
type(pt) = struct id{φ}∗field_offset(v φ ,φ) = δ ′
L5
l
(pt → v φ ,σ i−1 , s i ,i) ⇒ (bl,δ+δ )
′
(pt,σ i−1 , s i ,i) ⇓ ptr(bl,δ)
L6 l
(∗pt,σ i−1 , s i ,i) ⇒ (bl,δ)

命题 1. 对于任意给定的表达式 la, 使用左值表达式求值规则求出的值 (bl,δ) 是唯一的.
证明: 反证法, 若 la 的左值不唯一, 有两个不同的存储位置 (bl,δ) 和 (bl ,δ ), 对 la 进行赋值, 则有:
′
′
′
′
(1) (bl,δ) 和 (bl ,δ ) 都发生变化, 表明 la 同时影响两个存储位置, 与左值表达式定义不符;
(2) (bl,δ) 和 (bl ,δ ) 都不发生变化, 表明 la 不影响两个存储位置, 与左值表达式定义不符;
′
′
′
(3) (bl,δ) 和 (bl ,δ ) 其中一个发生变化另一个不发生变化, 表明 la 只有一个存储位置, 与假设不符.
′
表 2 为 MSVL 的右值表达式求值规则, 其中 c 表示常量, x 表示 V 中的变量, v,v 1 ,v 2 表示 D 中的值, (τ)v 1 为
cast( v 1 , type( v 1 ,τ)) 的简写, 表示将 v 1 从它原始类型 type( v 1 ) 强制转换为期望的类型 τ. 规则 R1 处理常量, R2 处理
可以作为左值表达式的表达式, R3 处理取地址表达式, R4 处理强制类型转换, R5 和 R6 处理数组元素, R7 处理结
构体成员, R8 和 R9 处理算数运算, R10 和 R11 处理 if 语句求值, R12 处理前一状态 ( ⊝) 操作, R13 处理参数列表
求值.