Static Program Analysis
Part 10 – abstract interpretation
http://cs.au.dk/~amoeller/spa/
Anders Møller & Michael I. Schwartzbach Computer Science, Aarhus University
Agenda
• Collecting semantics
• Abstraction and concretization • Soundness
• Optimality
2
Program semantics as constraint systems
3
The semantics of expressions
4
Successors and joins
5
Semantics of statements
6
The resulting constraint system
7
Example
the least solution
8
A fixed point theorem for continuous functions
If f is continuous:
(even when L has infinite height!)
9
Semantics vs. analysis
10
Agenda
• Collecting semantics
• Abstraction and concretization • Soundness
• Optimality
11
Abstraction functions for sign analysis
12
Concretization functions for sign analysis
13
Galois connections
14
Galois connections
For Galois connections, the concretization function uniquely determines the abstraction function and vice versa:
15
Galois connections
For each of these two lattices, given the “obvious” concretization function, is there an abstraction function such that the concretization function
and the abstraction function form a Galois connection?
16
Agenda
• Collecting semantics
• Abstraction and concretization • Soundness
• Optimality
17
Soundness
18
Soundness
19
Safe approximations
20
Safe approximations
21
The two constraint systems
22
Safe approximations
23
The soundness theorem
24
Agenda
• Collecting semantics
• Abstraction and concretization • Soundness
• Optimality
25
Optimal approximations
26
Optimal approximations in sign analysis?
Even if we could make optimal, the analysis result is not always optimal:
27