This is an old revision of the document!
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.