程序代写代做代考 Static Program Analysis

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