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

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

(3) ∧ k (p,g,l ⊢ e i ,µ ⇒ v i )∧vs = (v 1 ,...,v k )∧alloc_mem(M,l, par +dcl) = (M 1 ,loc)∧
i=1
store_mem(M 1 ,loc,l, par,vs) = M 2 ∧ p,g,l, f ⊢ stmt,µ 2 ⇒ Return v s ,µ 3 ∧
free_mem(M 3 ,loc) = M 4 ∧ P(stmt,µ 2 ,µ 3 ,Return v s ) 归纳假设
(4) α ⊢ µ 2 ∼ s u 假设
∗ (
)

(5) ⇒ (ms,σ u−1 , s u ,u) → true,σ j ,∅, j+1 ∧(α ⊢ µ 3 ∼ s j ) TER, (3)
(6) ( f (ra 1 ,...,ra k ,RVal),σ i−1 , s i ,i)
↣ (id(ra 1 ,...,ra k ,RVal),σ i−1 , s i ,i)

k
↣ ((∧ τ r y r ∧mdcl ⇐ ra r );ms;〇(ext mfree(y 1 ,...,y k ,mdcl)∧empty),σ i−1 , s i ,i) FUN
r=1
∗ ( )
→ (ms;〇 ext mfree(y 1 ,...,y k ,mdcl)∧empty ,σ u−1 , s u ,u) MIN1, TR1
( )
(7) (ms;〇 ext mfree(y 1 ,...,y k ,mdcl)∧empty ,σ u−1 , s u ,u)
∗ ( )
→ (RVal ⇐ ra∧empty;〇 ext mfree(y 1 ,...,y k ,mdcl)∧empty ,σ j−1 , s j , j) (6)
( ) l r
↣ (empty;〇 ext mfree(y 1 ,...,y k ,mdcl)∧empty ,σ j−1 ,(s , s [v m /RVal]), j) MIN1
j j
→ (ext mfree(y 1 ,...,y k ,mdcl)∧empty,σ j , s j+1 , j+1) CHOP, TR1
→ (true,σ j+1 ,∅, j+2) EXT2, TR2
Solidity 中, 函数内部的参数变量默认为 memory 类型, 在函数退出时自动释放内存. MSVL 中同样在函数
中先给变量 y 1 ,...,y k 分配内存块, 并在函数退出时释放内存. 变量声明的前后, Solidity 状态由 µ 变为 , MSVL 内
µ 2
存状态由 s i 变为 , 整个过程不影响语句的执行和其他变量的值与位置, 且对所有的 1 ⩽ r ⩽ k, MSVL 中有
s u
(ra r ,σ i−1 , s i ,i) ⇓ v mr , 由 (1) 和 (2) 可知 α ⊢ v sr ∼ v mr , 因此有 α ⊢ µ 2 ∼ s µ . 由 (5) 可知, α ⊢ µ 3 ∼ s j . 又因为 Solidity 中
从 µ 3 到 µ 4 仅是将局部变量从 s j 中移除, 而 MSVL 中从 s j 到 s j+1 也是将 y 1 ,...,y k 和 mcdl 中的变量从 s j 中移除, 其
α ⊢ µ 4 ∼ s j+1 .
他变量的值和位置没有发生变化, 因此有
∗ ( )
(8) ⇒ ( f (ra 1 ,...,ra k ,RVal),σ i−1 , s i ,i) → true,σ j+1 ,∅, j+2 ∧α ⊢ µ 4 ∼ s j+1 (5, 6)

( (
(9) ⇔ P id f e ),µ,µ 4 ,out) TER, (7)
∗

同理可证, 如果函数没有返回值, 结论依然成立.
( )
12) 规则 (S-19) 与 (S-22) 处理外部函数调用“ e 1 .e 2 e ∗ ”. MSVL 中有 TranStmt(e 1 .e 2 (e )) = ext f(ra ) ”, 其中
∗
∗
“
3 3
( )
,
∗
∗
∗
∗
f = TranExp(e 2 ) e = (e s1 ,...,e sk ) 且 ra = (ra 1 ,...,ra k ), 有 ra r = TranExp(e sr )(1 ⩽ r ⩽ k), 即 TranExp e = ra .
3 3
( { } )
(1) ∧ 〇empty,ext f(ra 1 ,...,ra k ) ,σ i−1 , s i ,i
( )
→ empty,σ i , s i+1 ,i+1 EXT2
→ (true,σ i+1 ,∅,i+2)∧ s i = s i+1 TR2
}
( {
(2) ⇒ ∧ 〇empty,ext f(ra 1 ,...,ra k ) ,σ i−1 , s i ,i )

∗
→ (true,σ i+1 ,∅,i+2)∧α ⊢ µ ∼ s i+1 (1)
( )
(3) ⇔ P(e 1 .e 2 e ,µ,µ,out) TER, (2)

∗
3
s i = s i+1 .
其中, (1) 表示
定理 3. 通过 SOL2M 转换器, Solidity 程序 P s 转换为 MSVL 程序 P m , 那么 P s 和 P m 语义等价, 记作 P s ∼ P m .
证明: 假设 Solidity 程序 P s 由 k 1 个表达式和 k 2 条语句构成, 其中 k 1 和 k 2 是常数. 当通过 SOL2M 转换器将
Solidity 程序转换为 MSVL 程序时, 有 P m = TranPrgm(P s ). 其中 a i = TranExp(e i )(0 ⩽ i ⩽ k 1 ) 和 ms j = TranStmt
( )
stmt j (0 ⩽ j ⩽ k 2 ). 令 S 和 s 0 为程序的初始状态, 根据定理 1 和定理 2, 对给定的 α, 如果 α ⊢ S ∼ s 0 , 那么对于所有
的 0 ⩽ i ⩽ k 1 和 0 ⩽ j < k 2 , 有 α ⊢ e i ∼ e a i 和 α ⊢ stmt j ∼ ms j . 因此, P s 等价于 P m , 即 P s ∼ P m .
推论 1. 通过 SOL2M 转换器, Solidity 程序 P s 转换为 MSVL 程序 P m , 那么 P s 和 P m 的执行结束状态等价.
证明: 根据定理 3 可知 P s 和 P m 等价, 根据定义 6 可知对于给定的内存注入 , P m 执行终止时有
α P s 和
′
α ⊢ µ ∼ s |σ| , 即 P s 和 P m 的执行结束状态等价.