Example: Coalescent product

let $M_{\bot}^{\#}$ to be the abstract element defined by $M_{\bot}^{\#}(x) = M_{\bot}^{\#}(y) = \bot$

when $M^{\#}$ maps any variable into $\bot$, it should be

*reduced*into $M_{\bot}^{\#}$=> can improve the analysis precision of condition tests, etc.

this technique is also used in Julia abstract interpretation, e.g.

`abstract_statement`

NOTE: this is why the abstract element is initialized

`NOT_FOUND`

, rather than`Bottom`

, I think

Note

A static analysis based on a reduced product is in general more precise than a *product of static analysis*. Because the former can refine abstract information at any time, rather than only at the very end.

In practice, the first iteration(s) of a loop often has a special effect. => unroll the first $N$ iterations, and delays the abstract joins, which introduces a loss of precision.

$M_0^{\#} = M^{\#}\\ M_{k+1}^{\#} = \begin{cases} F^{\#}(M_k^{\#}) &\text{if } k < N \\ M_k^{\#} \triangledown F^{\#}(M_k^{\#}) &\text{otherwise} \end{cases}$Use regular abstract union $\sqcup^{\#}$ for the first $N$ iterations in the loop.

$M_0^{\#} = M^{\#}\\ M_{k+1}^{\#} = \begin{cases} M_k^{\#} \sqcup^{\#} F^{\#}(M_k^{\#}) &\text{if } k \le N \\ M_k^{\#} \triangledown F^{\#}(M_k^{\#}) &\text{otherwise} \end{cases}$Given a concrete fixpoint of the concrete function $G$, applying $G^{\#}$ again to any sound approximation of this concrete fixpoint produces another sound approximation.

This means that, once the algorithm stabilizes, we can simply compute one more iteration in the abstract level and still obtain a sound approximation of the states at the loop head.

```
x = 0;
while (rand() && x < 50) {
x += 1;
}
```

after abstract iteration: $\{ x \rightarrow [0, +\infty) \}$

after additional one $F^{\#}$ application: $\{ x \rightarrow [1, 50] \}$

merged with the entry state: $\{ x \rightarrow [0, 50] \}$

spatial sparsity: usually, each program portion (an expression, a statement, a sequence of statements, a procedure, a loop body, etc.) access only a small part of the whole memory

temporal sparsity: after the definition (write)of a memory location, its use (read) is not immediate but a while later

E.g.:

unit of module analysis: procedure (function)

first, separately analyze procedures by "parameterizing" its call context

symbolic pre-state → symbolic post-state

later, at link time, the global behavior of the program is obtained by instantiating parameterized pre/post states with the actual calling context, and stitching the procedure summaries

xref: https://research.fb.com/inferbo-infer-based-buffer-overrun-analyzer/

We can actually design static analyses to compute over-approximate *pre-conditions from a post-condition*.x

e.g. Boolean filter $ℱ_B$ reconciled.

$ℱ_B$: takes as inputs a boolean expression $B$ and a set of states, filters out the states such that $B$ evaluate to false, keeping only those states such that $B$ evaluates to true.

$ℱ_B(M) = \{ m \in M | \llbracket B \rrbracket(m) = \text{true} \}$can be re-defined with *backward semantics* $\llbracket B \rrbracket_{\textbf{bwd}}$:

The semantics $\llbracket B \rrbracket_{\textbf{bwd}}$ is defined in *backward* style, as it takes a value (i.e. a result) and returns the set of states that lead to this value.

Example program: given the abstract post-condition $\{x_0 \mapsto \top, x_1 \mapsto [-\infty, -3]\}$, a backward-analysis returns an empty set (i.e. no pre-condition exists)

```
int x₀, x₁;
input(x₀);
if (x₀ > 0) {
x₁ := x₀;
} else {
x₁ := -x₀;
}
```

By computing an over-approximation of the sets of states leading to some given behavior, backward analysis:

provides a

*necessary*condition for this behavior to occurdually, also computes a

*sufficient*condition for a given behavior*not*to occur

```
L0 ...
if (y ≤ x) {
L1 ...
if (x ≤ 4) {
L2 ...
if (5 ≤ y) {
L3 ...
```

non-relational forward-analysis can't prove

`L3`

is actually not reachablebackward analysis:

assumes the abstract state $\{x \mapsto (-\infty), 4], y \mapsto [5, +\infty) ]\}$

back-propagated to

`if (y ≤ x)`

, we obtain the empty pre-condition, which indicates the assumed abstract post-state is not feasible

Backward analysis can be applied very locally to refine the analysis of tests, etc. as Julia's compiler does.

© Shuhei Kadowaki.

Last modified: 2023-02-16.

Website built with Franklin.jl and the Julia programming language.

Last modified: 2023-02-16.

Website built with Franklin.jl and the Julia programming language.