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

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

用 δ 表示 δ = field_offset(id,φ) = sizeof (τ 1 )+...+ sizeo f (τ k−1 ). E-4 为反向使用, 因为结构体成员变量的位置具有唯
一性, 由首地址与偏移量决定, 所以可进行逆向推理.
(1) α ⊢ le∼ e la∧α ⊢ id s ∼ e id m 归纳假设
(2) α ⊢ µ ∼ s 已知条件
l
(3) p,g,l ⊢ le.id s ,µ ⇒ addr +i s 定义2, 假设
l
(4) ⇒ p,g,l ⊢ le,µ ⇒ addr ∧i s = δ E-4, (3)

l
(5) (la.id m ,σ, s,|σ|+1) ⇒ (bl,i m ) 假设
l

(6) ⇒ (la,σ, s,|σ|+1) ⇒ (bl, j m )∧(i m = j m +δ) L4, (5)

(7) ⇒ α ⊢ load(S,addr, sizeof (τ s )) ∼ ptr(bl, j m ) 定义2, 4, (1, 2, 4, 6)

(8) ⇒ α ⊢ load(S,addr +δ, sizeo f (τ s )) ∼ ptr(bl, j m +δ) 引理1, (4, 6, 7)

(9) ⇒ α ⊢ load(S,i s , sizeo f (τ s )) ∼ ptr(bl,i m ) (8)
(10) ⇔ α ⊢ le.id s ∼ l la.id m 定义2, (9)
(11) ⇒ α ⊢ le.id s ∼ e la.id m 定义4, (10)

5) 对于类型为 τ 的一维数组元素, Solidity 中表示为 le[e], 其中 le 为 id, MSVL 中表示为 id m [ra], 其中
,
,
id m [ra] = TranExp(le[e]) ra = TranExp(e) id m 和 le 均为左值表达式, id m [ra]、le[e]、e 和 ra 均为右值表达式. E-
2 与 E-6 为反向使用, 因为数组元素的位置具有唯一性, 由首地址与偏移量决定, 所以可进行逆向推理.
(1) α ⊢ le[e]∼ l id m [ra]∧α ⊢ e∼ e ra 归纳假设
(2) α ⊢ µ ∼ s 已知条件
(3) p,g,l ⊢ le[e],µ ⇒ v s 定义3, 假设
l
(4) ⇒ p,g,l ⊢ le[e],µ ⇒ addr +i s ∧v s = load(S,addr +i s , sizeo f (τ s )) E-2, E-6, (3)

(5) (id m [ra],σ, s,|σ|+1) ⇓ v m 假设
l
(6) ⇒ (id m ,σ, s,|σ|+1) ⇒ (bl,i m )∧v m = ptr(bl,i m ) L2, R5, (5)

,

(7) ⇒ α ⊢ load(S,addr +i s sizeo f (τ s )) ∼ ptr(bl,i m ) 定义2, (1, 2, 4, 6)
(8) ⇔ α ⊢ v s ∼ v m 定义1, (4, 6, 7)

(9) ⇒ α ⊢ le[e]∼ r id m [ra] 定义3, (8)
(10) ⇔ α ⊢ le[e]∼ e id m [ra] 定义4, (9)
二维数组同理可证.
6) 对于结构体成员变量, Solidity 中表示为 le.id s , MSVL 中表示为 la.id m , 且 la.id m = TranExp(le.id s ) la =
,
,
TranExp(le) le 和 la 为左值表达式, le.id s 、la.id m 、id m 和 id s 均为右值表达式. E-4 与 E-8 为反向使用, 因为结构体
成员变量的位置具有唯一性, 由首地址与偏移量决定, 所以可进行逆向推理.
(1) α ⊢ le.id s ∼ l la.id m ∧α ⊢ id s ∼ e id m 归纳假设
(2) α ⊢ µ ∼ s 已知条件
(3) p,g,l ⊢ le.id s ,µ ⇒ v s 定义3, 假设
l
(4) ⇒ (p,g,l ⊢ le,µ ⇒ addr +i s )∧(v s = load(S,addr +i s , sizeo f (τ s ))) E-4, E-8, (3)
(5) (la.id m ,σ, s,|σ|+1) ⇓ v m 假设
l
(6) ⇒ (la,σ, s,|σ|+1) ⇒ (bl,i m )∧v m = ptr(bl,i m ) L4, R7, (5)

(7) ⇒ α ⊢ load(S,addr +i s , sizeo f (τ s )) ∼ ptr(bl,i m ) 定义2, (1, 2, 4, 6)

(8) ⇔ α ⊢ v s ∼ v m 定义1, (4, 6, 7)

(9) ⇒ α ⊢ le.id s ∼ r la.id m 定义3, 假设, (8)

(10) ⇒ α ⊢ le.id s ∼ e la.id m 定义4, (9)
7) 对于 Solidity 中除自增自减表达式外的其他单目运算 unope, MSVL 中有 mop 1 ra = TranExp(unope), 其中