ROBERTO BRUNI, University of Pisa, Italy
ROBERTO GIACOBAZZI, University of Verona, Italy
ROBERTA GORI, University of Pisa, Italy
FRANCESCO RANZATO, University of Padova, Italy
只记录重点信息。
# 一个例子
考虑两个程序:
c 1 = if even ( x ) then 0 else 1 c 2 = if even ( x ) then x else x + 1 c_1=\textbf{if }\text{even}(x)\textbf{ then }0\textbf{ else }1\\
c_2=\textbf{if }\text{even}(x)\textbf{ then }x\textbf{ else }x+1\\
c 1 = if even ( x ) then 0 else 1 c 2 = if even ( x ) then x else x + 1
然后定义[ ∣ c ∣ ] A = α ∘ [ ∣ c ∣ ] ∘ γ [|c|]^A=\alpha\circ[|c|]\circ\gamma [ ∣ c ∣ ] A = α ∘ [ ∣ c ∣ ] ∘ γ ,对于某个 abstract domain A A A 。那么假如A = Interval A=\textbf{Interval} A = Interval ,那么:
[ ∣ c 1 ∣ ] A ∘ [ ∣ c 2 ∣ ] A ( [ 0 , 1 ] ) = [ ∣ c 1 ∣ ] A ( [ 0 , 2 ] ) = [ 0 , 1 ] \begin{aligned}
\;[|c_1|]^{A}\circ[|c_2|]^A([0,1])&=[|c_1|]^A([0,2])\\
&=[0,1]
\end{aligned}
[ ∣ c 1 ∣ ] A ∘ [ ∣ c 2 ∣ ] A ( [ 0 , 1 ] ) = [ ∣ c 1 ∣ ] A ( [ 0 , 2 ] ) = [ 0 , 1 ]
而( [ ∣ c 1 ∣ ] ∘ [ ∣ c 2 ∣ ] ) A ( [ 0 , 1 ] ) = [ 0 , 0 ] ([|c_1|]\circ[|c_2|])^A([0,1])=[0,0] ( [ ∣ c 1 ∣ ] ∘ [ ∣ c 2 ∣ ] ) A ( [ 0 , 1 ] ) = [ 0 , 0 ] 。故有:
( [ ∣ c 1 ∣ ] ∘ [ ∣ c 2 ∣ ] ) A ⊊ [ ∣ c 1 ∣ ] A ∘ [ ∣ c 2 ∣ ] A ([|c_1|]\circ[|c_2|])^A\subsetneq[|c_1|]^A\circ[|c_2|]^A
( [ ∣ c 1 ∣ ] ∘ [ ∣ c 2 ∣ ] ) A ⊊ [ ∣ c 1 ∣ ] A ∘ [ ∣ c 2 ∣ ] A
原文中对其的意义说明是:
The lack of compositionality is the main cause of the interdependence between the precision of an abstract interpretation and the way programs are written.
# Correctness/Incorrectness Logic 要做的事情
首先它们想做的事仍然是 combine proof for correctness and incorrectness,和 outcome logic 的 motivation 是一样的。
然后做法是:利用 triple 去 under-approximation 证明 incorrectness,然后利用 abstract interpretation 去 over-approximation 证明 correctness。形式化地,考虑一个 triple 和 abstract domain A A A ,如果令函数A = γ ∘ α A=\gamma\circ\alpha A = γ ∘ α :
⊨ A [ p ] c [ q ] \vDash_A[p]c[q] ⊨ A [ p ] c [ q ] 当且仅当同时满足:
q ⊆ post [ c ] p q\subseteq\text{post}[c]p q ⊆ post [ c ] p ,即 under-approximation。
A ( q ) = A ( post [ c ] p ) A(q)=A(\text{post}[c]p) A ( q ) = A ( post [ c ] p ) 。即有相同的 abstraction。
post [ c ] \text{post}[c] post [ c ] is locally complete for input p p p on A A A 。
这三个条件其实是说,一个是q ⊆ post [ c ] p ⊆ A ( post [ c ] p ) = A ( q ) q\subseteq\text{post}[c]p\subseteq A(\text{post}[c]p)=A(q) q ⊆ post [ c ] p ⊆ A ( post [ c ] p ) = A ( q ) ,即post [ c ] p \text{post}[c]p post [ c ] p 是夹在[ q , A ( q ) ] [q,A(q)] [ q , A ( q ) ] 之间的。
# Global Completeness and Local Completeness
Definition . The abstract domain A A A is called a complete abstraction for f f f if there exists a complete approximation f # : A → A f^\#:A\rightarrow A f # : A → A satisfying:
α ∘ f = f # ∘ α \alpha\circ f=f^\#\circ\alpha
α ∘ f = f # ∘ α
这个定义实际上说明了:In a complete approximation f # f^\# f # , then only loss of precision is due to the abstract domain and not to the definition of the abstract function itself !
可以证明,A A A is a complete abstraction for f f f if and only if α ∘ f = ( α ∘ f ∘ γ ) ∘ α \alpha\circ f=(\alpha\circ f\circ\gamma)\circ\alpha α ∘ f = ( α ∘ f ∘ γ ) ∘ α (前提是α , γ \alpha,\gamma α , γ 是 Galois embedding)
令A = γ ∘ α A=\gamma\circ\alpha A = γ ∘ α ,由于γ \gamma γ 是单射,那么上述条件其实也可以等价于A ∘ f = A ∘ f ∘ A A\circ f=A\circ f\circ A A ∘ f = A ∘ f ∘ A 。
我们记C A ( f ) \mathbb{C}^A(f) C A ( f ) 表示 A is a complete abstraction for f f f 。即C A ( f ) : A f = A f A \mathbb{C}^A(f):Af=AfA C A ( f ) : A f = A f A 。
其实在程序语言中,我们也希望对于所有程序c c c 都有C A ( f ) \mathbb{C}^A(f) C A ( f ) 。但这是非常罕见的情况:
…the standard notion of (global) completeness for Boolean guards is a too strong requirement for abstract domains, often met in practice just by trivial guards or domains.
所以试图引入 local completeness:
Definition . An abstract domain A A A is locally complete for f : C → C f:C\rightarrow C f : C → C at a concrete value c ∈ C c\in C c ∈ C , written C c A ( f ) \mathbb{C}^A_c(f) C c A ( f ) , if:
C c A ( f ) ⟺ A f ( c ) = A f A ( c ) \mathbb{C}^A_c(f)\iff Af(c)=AfA(c)
C c A ( f ) ⟺ A f ( c ) = A f A ( c )
而 local 和 complete 联系就是:C A ( f ) ⟺ ∀ c ∈ C . C c A ( f ) \mathbb{C}^A(f)\iff\forall c\in C.\;\mathbb{C}_c^A(f) C A ( f ) ⟺ ∀ c ∈ C . C c A ( f ) .
Proposition : C A ( c ) A ( f ) \mathbb{C}_{A(c)}^A(f) C A ( c ) A ( f ) 自然成立。(A A A is trivially locally complete for any f f f on any abstract value A ( c ) A(c) A ( c ) )
证明:考虑到α , γ \alpha,\gamma α , γ 是 Galois embedding,那么有:
A f A ( A ( c ) ) = A f γ α γ α ( c ) = A f γ ( α γ ) α ( c ) = A f A ( c ) = A f ( A ( c ) ) □ . \begin{aligned}
AfA(A(c))&=Af\gamma\alpha\gamma\alpha(c)\\
&=Af\gamma(\alpha\gamma)\alpha(c)\\
&=AfA(c)\\
&=Af(A(c))\\
&\square.
\end{aligned}
A f A ( A ( c ) ) = A f γ α γ α ( c ) = A f γ ( α γ ) α ( c ) = A f A ( c ) = A f ( A ( c ) ) □ .
例 :考虑函数[ ∣ 0 < x ? ∣ ] [|0<x?|] [ ∣ 0 < x ? ∣ ] 和 Intervals,它不是 global complete 的,譬如对c = { 0 , 4 } c=\{0,4\} c = { 0 , 4 } 那么:
A ∘ [ ∣ 0 < x ? ∣ ] ( c ) = A ( { 4 } ) = { 4 } A ∘ [ ∣ 0 < x ? ∣ ] ∘ A ( c ) = A ∘ [ ∣ 0 < x ? ∣ ] ( { 0 , 1 , 2 , 3 , 4 } ) = A ( { 1 , 2 , 3 , 4 } ) = { 1 , 2 , 3 , 4 } A\circ[|0<x?|](c)=A(\{4\})=\{4\}\\
A\circ[|0<x?|]\circ A(c)=A\circ[|0<x?|](\{0,1,2,3,4\})=A(\{1,2,3,4\})=\{1,2,3,4\}
A ∘ [ ∣ 0 < x ? ∣ ] ( c ) = A ( { 4 } ) = { 4 } A ∘ [ ∣ 0 < x ? ∣ ] ∘ A ( c ) = A ∘ [ ∣ 0 < x ? ∣ ] ( { 0 , 1 , 2 , 3 , 4 } ) = A ( { 1 , 2 , 3 , 4 } ) = { 1 , 2 , 3 , 4 }
因此A ∘ [ ∣ 0 < x ? ∣ ] ≠ A ∘ [ ∣ 0 < x ? ∣ ] ∘ A A\circ[|0<x?|]\neq A\circ[|0<x?|]\circ A A ∘ [ ∣ 0 < x ? ∣ ] = A ∘ [ ∣ 0 < x ? ∣ ] ∘ A 。但是当c c c 满足以下情况之一时,它是 complete 的:
c ⊆ Z > 0 c\subseteq\mathbb{Z}_{>0} c ⊆ Z > 0 .
c ⊆ Z ≤ 0 c\subseteq\mathbb{Z}_{\leq 0} c ⊆ Z ≤ 0 .
{ 0 , 1 } ⊆ c \{0,1\}\subseteq c { 0 , 1 } ⊆ c .
譬如c = { 0 , 1 , 4 } c=\{0,1,4\} c = { 0 , 1 , 4 } ,那么:
A ∘ [ ∣ 0 < x ? ∣ ] ( c ) = A ( { 1 , 4 } ) = { 1 , 2 , 3 , 4 } A ∘ [ ∣ 0 < x ? ∣ ] ∘ A ( c ) = A ∘ [ ∣ 0 < x ? ∣ ] ( { 0 , 1 , 2 , 3 , 4 } ) = A ( { 1 , 2 , 3 , 4 } ) = { 1 , 2 , 3 , 4 } A\circ[|0<x?|](c)=A(\{1,4\})=\{1,2,3,4\}\\
A\circ[|0<x?|]\circ A(c)=A\circ[|0<x?|](\{0,1,2,3,4\})=A(\{1,2,3,4\})=\{1,2,3,4\}
A ∘ [ ∣ 0 < x ? ∣ ] ( c ) = A ( { 1 , 4 } ) = { 1 , 2 , 3 , 4 } A ∘ [ ∣ 0 < x ? ∣ ] ∘ A ( c ) = A ∘ [ ∣ 0 < x ? ∣ ] ( { 0 , 1 , 2 , 3 , 4 } ) = A ( { 1 , 2 , 3 , 4 } ) = { 1 , 2 , 3 , 4 }
Theorem : A A A is locally complete for both [ ∣ b ? ∣ ] [|b?|] [ ∣ b ? ∣ ] and [ ∣ ¬ b ? ∣ ] [|\neg b?|] [ ∣ ¬ b ? ∣ ] on p p p if and only if:
C p A ( [ ∣ b ? ∣ ] ) and C p A ( [ ∣ ¬ b ? ∣ ] ) ⟺ A ( c ) = c \mathbb{C}^A_p([|b?|])\text{ and }\mathbb{C}^A_p([|\neg b?|])\iff A(c)=c
C p A ( [ ∣ b ? ∣ ] ) and C p A ( [ ∣ ¬ b ? ∣ ] ) ⟺ A ( c ) = c
其中,c = ( [ ∣ b ? ∣ ] ∘ A ∘ [ ∣ b ? ∣ ] p ) ∪ ( [ ∣ ¬ b ? ∣ ] ∘ A ∘ [ ∣ ¬ b ? ∣ ] p ) c=([|b?|]\circ A\circ[|b?|]p)\cup([|\neg b?|]\circ A\circ[|\neg b?|]p) c = ( [ ∣ b ? ∣ ] ∘ A ∘ [ ∣ b ? ∣ ] p ) ∪ ( [ ∣ ¬ b ? ∣ ] ∘ A ∘ [ ∣ ¬ b ? ∣ ] p ) 。
证明:
(=>) 假设C p A ( [ ∣ b ? ∣ ] ) and C p A ( [ ∣ ¬ b ? ∣ ] ) \mathbb{C}^A_p([|b?|])\text{ and }\mathbb{C}^A_p([|\neg b?|]) C p A ( [ ∣ b ? ∣ ] ) and C p A ( [ ∣ ¬ b ? ∣ ] ) ,那么:
A ( c ) = A ( ( [ ∣ b ? ∣ ] ∘ A ∘ [ ∣ b ? ∣ ] p ) ∪ ( [ ∣ ¬ b ? ∣ ] ∘ A ∘ [ ∣ ¬ b ? ∣ ] p ) ) [by monotonicity] ⊆ A ( ( A ∘ [ ∣ b ? ∣ ] p ) ∪ ( A ∘ [ ∣ ¬ b ? ∣ ] p ) ) [by following lemma] = A ( [ ∣ b ? ∣ ] p ∪ [ ∣ ¬ b ? ∣ ] p ) = A ( p ) \begin{aligned}
A(c)&=A(([|b?|]\circ A\circ[|b?|]p)\cup([|\neg b?|]\circ A\circ[|\neg b?|]p))\\
\text{[by monotonicity]}&\subseteq A((A\circ[|b?|]p)\cup (A\circ[|\neg b?|]p))\\
\text{[by following lemma]}&=A([|b?|]p\cup[|\neg b?|]p)\\
&=A(p)
\end{aligned}
A ( c ) [by monotonicity] [by following lemma] = A ( ( [ ∣ b ? ∣ ] ∘ A ∘ [ ∣ b ? ∣ ] p ) ∪ ( [ ∣ ¬ b ? ∣ ] ∘ A ∘ [ ∣ ¬ b ? ∣ ] p ) ) ⊆ A ( ( A ∘ [ ∣ b ? ∣ ] p ) ∪ ( A ∘ [ ∣ ¬ b ? ∣ ] p ) ) = A ( [ ∣ b ? ∣ ] p ∪ [ ∣ ¬ b ? ∣ ] p ) = A ( p )
其中,我们要说明A ( A ( q ) ∪ A ( w ) ) = A ( q ∪ w ) A(A(q)\cup A(w))=A(q\cup w) A ( A ( q ) ∪ A ( w ) ) = A ( q ∪ w ) 。由于 Galois embedding 可以得到α \alpha α is additive,那么:
γ α ( A ( q ) ∪ A ( w ) ) = γ ( α A ( q ) ∪ α A ( w ) ) = γ ( ( α γ ) α ( q ) ∪ ( α γ ) α ( w ) ) [Since Galois embedding] = γ ( α ( q ) ∪ α ( w ) ) = A ( q ∪ w ) □ . \begin{aligned}
\gamma\alpha(A(q)\cup A(w))&=\gamma(\alpha A(q)\cup\alpha A(w))\\
&=\gamma((\alpha\gamma)\alpha(q)\cup(\alpha\gamma)\alpha(w))\\
\text{[Since Galois embedding]}&=\gamma(\alpha(q)\cup\alpha(w))\\
&=A(q\cup w)\\
&\square.
\end{aligned}
γ α ( A ( q ) ∪ A ( w ) ) [Since Galois embedding] = γ ( α A ( q ) ∪ α A ( w ) ) = γ ( ( α γ ) α ( q ) ∪ ( α γ ) α ( w ) ) = γ ( α ( q ) ∪ α ( w ) ) = A ( q ∪ w ) □ .
因此,有:
[ ∣ b ? ∣ ] A ( c ) ⊆ [ ∣ b ? ∣ ] A ( p ) ⊆ [ ∣ b ? ∣ ] ∘ A ∘ [ ∣ b ? ∣ ] ∘ A ( p ) = [ ∣ b ? ∣ ] A [ ∣ b ? ∣ ] ( p ) [|b?|]A(c)\subseteq[|b?|]A(p)\subseteq [|b?|]\circ A\circ[|b?|]\circ A(p)=[|b?|]A[|b?|](p)
[ ∣ b ? ∣ ] A ( c ) ⊆ [ ∣ b ? ∣ ] A ( p ) ⊆ [ ∣ b ? ∣ ] ∘ A ∘ [ ∣ b ? ∣ ] ∘ A ( p ) = [ ∣ b ? ∣ ] A [ ∣ b ? ∣ ] ( p )
其中,第三个等号是因为 local completeness,第二个⊆ \subseteq ⊆ 是因为:
∀ p . [ ∣ b ? ∣ ] p ⊆ [ ∣ b ? ∣ ] A [ ∣ b ? ∣ ] p \forall p.\;[|b?|]p\subseteq [|b?|]A[|b?|]p
∀ p . [ ∣ b ? ∣ ] p ⊆ [ ∣ b ? ∣ ] A [ ∣ b ? ∣ ] p
证明也很显然,不妨设t ≜ [ ∣ b ? ∣ ] p t\triangleq [|b?|]p t ≜ [ ∣ b ? ∣ ] p ,那么因为 Galois embedding 有t ⊆ A ( t ) t\subseteq A(t) t ⊆ A ( t ) 。那么对于任意σ ∈ t \sigma\in t σ ∈ t ,都有[ ∣ b ∣ ] e x p σ = true [|b|]_{exp}\sigma=\textbf{true} [ ∣ b ∣ ] e x p σ = true 且σ ∈ A ( t ) \sigma\in A(t) σ ∈ A ( t ) 。所以也就有σ ∈ [ ∣ b ? ∣ ] A ( t ) \sigma\in[|b?|]A(t) σ ∈ [ ∣ b ? ∣ ] A ( t ) ,证毕。
因此,实际上有:
[ ∣ b ? ∣ ] A ( c ) ⊆ [ ∣ b ? ∣ ] A [ ∣ b ? ∣ ] ( p ) [ ∣ ¬ b ? ∣ ] A ( c ) ⊆ [ ∣ ¬ b ? ∣ ] A [ ∣ ¬ b ? ∣ ] ( p ) [|b?|]A(c)\subseteq[|b?|]A[|b?|](p)\\
[|\neg b?|]A(c)\subseteq [|\neg b?|]A[|\neg b?|](p)
[ ∣ b ? ∣ ] A ( c ) ⊆ [ ∣ b ? ∣ ] A [ ∣ b ? ∣ ] ( p ) [ ∣ ¬ b ? ∣ ] A ( c ) ⊆ [ ∣ ¬ b ? ∣ ] A [ ∣ ¬ b ? ∣ ] ( p )
所以:
A ( c ) = [ ∣ b ? ∣ ] A ( c ) ∪ [ ∣ ¬ b ? ∣ ] A ( c ) ⊆ [ ∣ b ? ∣ ] A [ ∣ b ? ∣ ] ( p ) ∪ [ ∣ ¬ b ? ∣ ] A [ ∣ ¬ b ? ∣ ] ( p ) = c \begin{aligned}
A(c)&=[|b?|]A(c)\cup[|\neg b?|]A(c)\\
&\subseteq[|b?|]A[|b?|](p)\cup [|\neg b?|]A[|\neg b?|](p)\\
&=c
\end{aligned}
A ( c ) = [ ∣ b ? ∣ ] A ( c ) ∪ [ ∣ ¬ b ? ∣ ] A ( c ) ⊆ [ ∣ b ? ∣ ] A [ ∣ b ? ∣ ] ( p ) ∪ [ ∣ ¬ b ? ∣ ] A [ ∣ ¬ b ? ∣ ] ( p ) = c
而c ⊆ A ( c ) c\subseteq A(c) c ⊆ A ( c ) 是显然的,因为A A A 的单调性,故A ( c ) = c A(c)=c A ( c ) = c 。
(<=) 首先,我们有p = [ ∣ b ? ∣ ] p ∪ [ ∣ ¬ b ? ∣ ] p ⊆ ( [ ∣ b ? ∣ ] A [ ∣ b ? ∣ ] p ) ∪ ( [ ∣ ¬ b ? ∣ ] A [ ∣ ¬ b ? ∣ ] p ) = c p=[|b?|]p\cup[|\neg b?|]p\subseteq ([|b?|]A[|b?|]p)\cup([|\neg b?|]A[|\neg b?|]p)=c p = [ ∣ b ? ∣ ] p ∪ [ ∣ ¬ b ? ∣ ] p ⊆ ( [ ∣ b ? ∣ ] A [ ∣ b ? ∣ ] p ) ∪ ( [ ∣ ¬ b ? ∣ ] A [ ∣ ¬ b ? ∣ ] p ) = c .
所以有
A ( p ) ⊆ A ( c ) = c = ( [ ∣ b ? ∣ ] A [ ∣ b ? ∣ ] p ) ∪ ( [ ∣ ¬ b ? ∣ ] A [ ∣ ¬ b ? ∣ ] p ) A(p)\subseteq A(c)=c=([|b?|]A[|b?|]p)\cup([|\neg b?|]A[|\neg b?|]p)
A ( p ) ⊆ A ( c ) = c = ( [ ∣ b ? ∣ ] A [ ∣ b ? ∣ ] p ) ∪ ( [ ∣ ¬ b ? ∣ ] A [ ∣ ¬ b ? ∣ ] p )
所以有
[ ∣ b ? ∣ ] A ( p ) ⊆ [ ∣ b ? ∣ ] c = [ ∣ b ? ∣ ] A [ ∣ b ? ∣ ] p ⊆ A [ ∣ b ? ∣ ] p [|b?|]A(p)\subseteq[|b?|]c=[|b?|]A[|b?|]p\subseteq A[|b?|]p
[ ∣ b ? ∣ ] A ( p ) ⊆ [ ∣ b ? ∣ ] c = [ ∣ b ? ∣ ] A [ ∣ b ? ∣ ] p ⊆ A [ ∣ b ? ∣ ] p
又因为A ∘ A = γ ( α γ ) α = γ α = A A\circ A=\gamma(\alpha\gamma)\alpha=\gamma\alpha=A A ∘ A = γ ( α γ ) α = γ α = A ,故左右同时套上A A A :
A [ ∣ b ? ∣ ] A ( p ) ⊆ A A [ ∣ b ? ∣ ] p = A [ ∣ b ? ∣ ] p A[|b?|]A(p)\subseteq AA[|b?|]p=A[|b?|]p
A [ ∣ b ? ∣ ] A ( p ) ⊆ A A [ ∣ b ? ∣ ] p = A [ ∣ b ? ∣ ] p
此外,因为A ( p ) ⊇ p A(p)\supseteq p A ( p ) ⊇ p ,故有A [ ∣ b ? ∣ ] A ( p ) ⊇ A [ ∣ b ? ∣ ] p A[|b?|]A(p)\supseteq A[|b?|]p A [ ∣ b ? ∣ ] A ( p ) ⊇ A [ ∣ b ? ∣ ] p ,结合上式,故得到A [ ∣ b ? ∣ ] A ( p ) = A [ ∣ b ? ∣ ] p A[|b?|]A(p)=A[|b?|]p A [ ∣ b ? ∣ ] A ( p ) = A [ ∣ b ? ∣ ] p 。
同理也可以得到A [ ∣ ¬ b ? ∣ ] A ( p ) = A [ ∣ ¬ b ? ∣ ] p A[|\neg b?|]A(p)=A[|\neg b?|]p A [ ∣ ¬ b ? ∣ ] A ( p ) = A [ ∣ ¬ b ? ∣ ] p 。
□ \square □ 证毕。