Sign Analysis of Expressions and Programs

Sign Analysis of Expressions

Suppose we want to test quickly whether the result of an expression is positive, negative or zero.

What is (quickly) the sign of

$\begin{equation*} (31283321 + 8629184) \times (-34234) \times (-4 + (123123 \times (-3))) \end{equation*}$

Why?

What is (quickly) the sign of

$\begin{equation*} (28166461706 + (723497 \times (- 38931))) \times 42 \end{equation*}$

Concrete domain: $\mathbb{Z} = \{ \ldots, -2, -1, 0, 1, 2, \ldots \}$

Concrete operations: ${+}, {\times} : \mathbb{Z}^2 \to \mathbb{Z}$

Abstract domain: $A = \{ neg, nul, pos, \top \}$

Abstract operations: $\oplus, \otimes : A^2 \to A$ defined by tables:

$\begin{tabular}{ |c |c |c |c |c |c |} \hline \oplus & neg & nul & pos & \top \\ \hline neg & neg & neg & \top & \top \\ \hline nul & neg & nul & pos & \top \\ \hline pos & \top & pos & pos & \top \\ \hline \top & \top & \top & \top & \top \\ \hline \end{tabular}$

$\begin{tabular}{ |c |c |c |c |c |c |} \hline \otimes & neg & nul & pos & \top \\ \hline neg & pos & nul & neg & \top \\ \hline nul & nul & nul & nul & nul \\ \hline pos & neg & nul & pos & \top \\ \hline \top & \top & nul & \top & \top \\ \hline \end{tabular}$

Sign Analysis of Programs

Prove that this program never reports error:

i = 20;
x = 2;
while (i > 0) {
  x = x + 4;
  i = i - 1;
}
if (x==0) {
  error;
} else {
  y = 1000/x;
}

Abstract state: map each variable to element of $A$ . Here we have $|A|^3$ possible states.

computation over control-flow graph

What does it mean for such computation to be correct?