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

4022 软件学报 2025 年第 36 卷第 9 期

(bl,δ m ) 且 i s /getSize(g,τ s ) = (i m −δ m )/sizeof (τ m ).
● V3 α ⊢ map(v s1 ) ∼ map(v m1 ), 当且仅当 v s1 = v m1 且 map(v s1 ) = map(v m1 ), 其中 map 为描述映射关系的函数,
在 Solidity 中对于任意映射类型的变量 mp 有 map(v s1 ) = v s = mp[v s1 ], 在 MSVL 中对于与 mp 相应的结构体数组
ma 有 map(v m1 ) = v m = ma[k].right 且 ma[k].left = v m1 .
其中, V1 表示 Solidity 与 MSVL 中常量 c 的等价. V2 表示 Solidity 的地址 i s 与 MSVL 的地址 ptr(bl,i m ) 等价.
V3 描述了 Solidity 与 MSVL 映射类型的等价.
引 理 1 . 对 于 给 定 的 α , 任 意 的 addr,bl,i m , j ∈ Z, 如 果 α ⊢ ptr(addr,i s ) ∼ ptr(bl,i m ) , 那 么 α ⊢ ptr(addr,i s +

j∗ sizeo f(τ s )) ∼ ptr(bl,i m + j∗ sizeo f (τ m )) .
证明:
(1) α ⊢ ptr(addr,i s ) ∼ ptr(bl,i m ) 已知
(2) ⇒ α(addr) = (bl,δ m )∧i s /sizeo f (τ s ) = (i m −δ m )/sizeof (τ m ) V2
(3) ⇒ α(addr) = (bl,δ m )∧i s /sizeo f (τ s )+ j = (i m −δ m )/sizeo f (τ m )+ j (2)

(4) ⇒ α(addr) = (bl,δ m )∧(i s + j∗ sizeo f(τ s ))/sizeof (τ s ) = (i m + j∗ sizeo f(τ m )−δ m )/sizeo f (τ m ) (3)
(5) ⇒ α ⊢ ptr(addr,i s + j∗ sizeo f(τ s )) ∼ ptr(bl,i m + j∗ sizeof (τ m )) V2
值得注意的是, addr+i s + j∗ sizeo f (τ s ) 与 bl+i m + j∗ sizeof (τ m ) 上限均为计算机内存大小.
定义 1 (状态等价). 对于给定的内存注入 α, Solidity 与 MSVL 的内存状态等价, 记为 α ⊢ µ ∼ s, 当且仅当以下
条件成立:
对 Solidity 程序中任意的状态变量 x s ∈ Dom(g), MSVL 程序中对于变量 x m ∈ Dom(s), 且 addr,bl,i m ∈ Z, 以及
l
v s ,v m ∈ D. 如果在 Solidity 程序中有 p,g,l ⊢ x s ,µ ⇒ addr 且 p,g,l ⊢ x s ,µ ⇒ v s . 在 MSVL 程序中有 s (x m ) = (bl,i m ) 且
l
r α ⊢ v s ∼ v m . 局部变量分析过程与全局类似不再赘述.
s (x m ) = v m , 那么有 α ⊢ addr ∼ ptr(bl,i m ) 且
定义 1 描述了 Solidity 程序与 MSVL 程序之间的状态等价关系, 其实质是, 当 Solidity 程序中的任意变量与
MSVL 程序中相对应变量的存储位置和值都等价, 则 Solidity 程序和 MSVL 程序状态等价.
定义 2 (左值表达式等价). 对于给定的内存注入 α, Solidity 与 MSVL 的左值表达式 e 与 a 等价, 记为 α ⊢ e∼ l a,
当且仅当以下条件成立:
l
对于任意的 µ, s,addr,bl,i m ,σ, 如果 α ⊢ µ ∼ s, 并且在 Solidity 程序中有 p,g,l ⊢ e,µ ⇒ addr, 在 MSVL 程序中
l
有 (a,σ, s,|σ|+1) ⇒ (bl,i m ), 那么有 α ⊢ addr ∼ ptr(bl,i m ).
定义 2 描述了 Solidity 与 MSVL 的左值表达式的等价定义. 其实质是对于 Solidity 中任意的左值表达式 e 和
MSVL 中相对应的左值表达式 a, 其所表示的存储位置等价, 则说明表达式表示相同的值, 因此左值表达式等价.
定义 3 (右值表达式等价). 对于给定的内存注入 α, Solidity 与 MSVL 的右值表达式 e 与 a 等价, 记为 α ⊢ e∼ r a,
当且仅当以下条件成立:
对于任意的 µ, s,v s ,v m ,σ, 如果 α ⊢ µ ∼ s, 并且在 Solidity 程序中有 p,g,l ⊢ e,µ ⇒ v s , 在 MSVL 程序中有
(a,σ, s,|σ|+1) ⇓ v m , 那么有 α ⊢ v s ∼ v m .
定义 3 描述了 Solidity 与 MSVL 的右值表达式的等价定义. 对于 Solidity 中任意的右值表达式 e 和 MSVL 中
a, 其所表示的值等价, 则说明右值表达式等价. 右值表达式等价实际上就是状态等价条件下
相对应的右值表达式
的表达式等价.
定义 4 (表达式等价). 对于给定的内存注入 α, Solidity 与 MSVL 的表达式 e 与 a 等价, 记为 α ⊢ e∼ e a, 当且仅
e
当 e 和 a 均为左值表达式时, 有 α ⊢ e∼ l a, 或者, 当 和 a 均为右值表达式时, 有 α ⊢ e∼ r a.
定义 5 (Solidity 语句等价). 从状态 u =< a,σ, M > (其中 σ =< b, p,S >) 开始执行语句 stmt 等价于执行 stmt ,
′
′
′
′
记为 (stmt,µ) (stmt ,µ ), 当且仅当从 Solidity 状态 u 出发执行 stmt 和 stmt 分别得到两个区间 µ σ = (µ 1 ,µ 2 ,...) 和
′ ′ ′ ′
µ = (µ ,µ ,...), 且这两个区间满足, 对所有的 i ⩾ 0 有 µ i = µ .
σ
2
1
i
定义 6 (语句等价). 对于给定的内存注入 α, Solidity 语句 stmt 与 MSVL 语句 ms 等价, 记为 α ⊢ stmt ms, 当且