Lecture 7: Formulas as a unifying domain for static analysis
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
- 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).
- 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
Conjunctions of fixed predicates as analysis domain
Disjunctions of conjunctions of predicates
Comparison of precision and efficiency.
- predicate abstraction (Cartesian abstraction)
- 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;
y = x.next; x.f = 1; y.f = 2;
Allocation-site based analyses