# Lecture 7: Formulas as a unifying domain for static analysis

### General setup

Analysis domain based on formulas and main operations:

- - set of all first-order formulas (or other set closed under propositional operations and quantifiers)
- - subset of formulas that we use as our analysis domain, e.g. finite. If we used abstract interpretation framework, we would have
- - normalization function, ensuring that the result is in our domain, works as but goes from formulas to formulas
- key requirement: is a valid formula ( produces a weaker formula)

- - computes strongest postcondition on formulas precisely, e.g. .

Control-flow graph is graph where are program points (between statements) and are edges labelled with program commands.

The state of our analysis (set of computed facts) maps program points to formulas in , that is: .

Basic philosophy of the analysis: compute precise result whenever possibly, then apply to fit it into .

Initial state: , except for initial program point , where unless we know something about the initial program state.

- intuition: computing abstraction of the set of reachable states

Update rule:

- compute the impact of all incoming edges

Correctness: if for each program point for all , then the facts are true in all program executions.

(If we stopped the analysis before this happens, then the result is not correct, it does not take into account all executions).

Termination

- observe the sequence of formulas for
- start from false, become weaker and weaker
- require that there are no infinite ascending chains of weaker and weaker formulas

## Examples

### Conjunctions of fixed predicates as analysis domain

### Disjunctions of conjunctions of predicates

### Linear inequalities

Example implementation: Parma Polyhedra Library and a paper about Parma.

Special cases:

- constant propagation
- interval analysis
- octagon domain

### Simple pointer analysis

Consider constant field propagation with

x = new Node(); y = new Node(); x.f = 1; y.f = 2;

or with

y = x.next; x.f = 1; y.f = 2;

Allocation-site based analyses