Sign Analysis for Expressions and Programs

Sign Analysis for 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?

$\begin{equation*} (pos \oplus pos) \otimes neg \otimes (neg \oplus (pos \otimes neg)) = pos \otimes neg \otimes neg = pos \end{equation*}$

What is (quickly) the sign of

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

$\begin{equation*} (pos \oplus (pos \otimes neg)) \otimes pos = (pos \oplus neg) \otimes pos = \top \otimes pos = \top \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 for Programs

Abstract state $V \to A$ , maps each variable to element of $A$

We have $|A|^K$ possible states for $K$ variables.

Computation over control-flow graph for our example

a more complex 'table' than above
given
- an abstract state (sign or each var)
- a control-flow graph edge
- find state at the other end of the edge
rules for merging abstract states

When is such computation correct?

What does it even mean for such computation to be correct?

Abstract Domain

Special case of interval analysis

Which intervals does it correspond to?
What is the height of the lattice for one variable, and what if we have $p$ program points and $q$ variables?