CS6620 Compiler Note 4 Path Sensitivity

Posted on In Disqus:

If we ignore the value of conditions by treating if or while statements as nondeterministic choices between two branches, we call these analyses as path insensitive analysis.

Path sensitive analysis is used to increase pessimistic accuracy of path insensitive analysis.

Assertions

In interval analysis, the constraints introduced by assertions will narrow the intervals by exploiting information in conditionals.

A trivial assertion constraint can be done in interval analysis by
$$
\begin{aligned}
& &\lbrack \lbrack v\rbrack\rbrack &= JOIN(v)\newline
\text{assert}(x> E)&:&\lbrack \lbrack v \rbrack\rbrack &= JOIN(v)\lbrack x\mapsto gt(JOIN(v)(x), eval(JOIN(v), E))\rbrack\newline
& & gt(\lbrack l_1, r_1\rbrack, \lbrack l_2, r_2\rbrack) &= \lbrack l_1, h_1 \rbrack \sqcap\lbrack l_2,\infty\rbrack\newline
\text{assert}(x< E)&:&\lbrack \lbrack v \rbrack\rbrack &= JOIN(v)\lbrack x\mapsto lt(JOIN(v)(x), eval(JOIN(v), E))\rbrack\newline
& & gt(\lbrack l_1, r_1\rbrack, \lbrack l_2, r_2\rbrack) &= \lbrack l_1, h_1 \rbrack \sqcap\lbrack -\infty, h_2\rbrack
\end{aligned}
$$

Branch Correlations

For an example program like

1
2
3
4
5
6
7
8
9
10
if (condition) {
	open();
	flag = 1;
} else {
	flag = 0;
}
...
if (flag) {
	close();
}

We want to ensure the follow flowchart is established and close every opened file / open any closed file.

graph LR;
A[Entry Point] --> B[Closed]
subgraph Branch Correlation
B -. "open()" .-> C[Open]
C -. "close()" .-> B
end

Analysis that keeps track of relations between variables is needed. This can be achieved by generalizing analysis to maintain multiple abstract states per program point.

The expansion can be done on $L’’ = Paths \to L$ where $L$ is the original lattice and $Paths$ is a finite set of path contexts.

A path context is used to predict over the program state. In general, each statement is analyzed in $|Paths|$ path contexts.

For the example, $Paths = \lbrace flag = 0,flag\ne 0\rbrace$. The constraint rules can be shown as
$$
\begin{aligned}
&JOIN(v)(p) &=& \bigcup_{w\in pred(v)} \lbrack\lbrack w\rbrack\rbrack(p)\newline
\text{open}() &\phantom{“”} \lbrack\lbrack v\rbrack\rbrack &=& \lambda p.\lbrace\text{open}\rbrace\newline
\text{close}() &\phantom{“”} \lbrack\lbrack v \rbrack\rbrack &=& \lambda p. \lbrace\text{close}\rbrace\newline
entry &\phantom{“”} \lbrack\lbrack v \rbrack\rbrack &=& \lambda p. \lbrace\text{close}\rbrace\newline
\text{flag} = 0 &\phantom{“”} \lbrack\lbrack v\rbrack \rbrack &=& \lbrack \text{flag} = 0 \mapsto \bigcup_{p\in Paths} JOIN(v)(p),\newline & & &\ \text{flag} \neq 0 \mapsto \varnothing\rbrack\newline
\text{flag} = I &\phantom{“”} \lbrack\lbrack v\rbrack \rbrack &=& \lbrack \text{flag} \ne 0 \mapsto \bigcup_{p\in Paths} JOIN(v)(p),\newline & & &\ \text{flag} = 0 \mapsto \varnothing\rbrack\newline
\text{flag} = E &\phantom{“”} \lbrack\lbrack v\rbrack \rbrack &=&\lambda q. \bigcup_{p\in Paths} JOIN(v)(p)\newline
\text{assert}(\text{flag}) &\phantom{“”} \lbrack\lbrack v\rbrack\rbrack &=& \lbrack \text{flag} \ne 0 \mapsto JOIN(v)(\text{flag}\ne 0),\newline & & &\ \text{flag} = 0 \mapsto \varnothing\rbrack\newline
\text{assert}(\text{!flag}) &\phantom{“”} \lbrack\lbrack v\rbrack\rbrack &=& \lbrack \text{flag} = 0 \mapsto JOIN(v)(\text{flag}= 0),\newline & & &\ \text{flag} \ne 0 \mapsto \varnothing\rbrack\newline
&\phantom{“”} \lbrack\lbrack v\rbrack\rbrack &=& \lambda p.JOIN(v)(p)
\end{aligned}
$$

$\varnothing$ stands for infeasible here, which means normal code cannot reach here, or program crashes.

The example can be see from SPA page 84.