The parallel implementation of the Astrée static analyzer

David Monniaux

http://www.di.ens.fr/~monniaux

Centre National de la Recherche Scientifique

École Normale Supérieure

Département d’Informatique 45, rue d’Ulm 75230 Paris cedex 5

D. Monniaux — The parallel implementation of the Astrée static analyzer 2

Introduction[1]Introductionsection.3

D. Monniaux — The parallel implementation of the Astrée static analyzer 3

The Astrée static analyzer

[2]The Astrée static analyzerfoil.4

Astrée http://www.astree.ens.fr is a static analyzer based on abstract interpretation.

• Analyzes a subset of the C language.

• Machine integers and floating-point numbers, not “mathematical” integers and real numbers.

• Tuned for large-scale control/command codes, automatically

generated from high-level specifications.

D. Monniaux — The parallel implementation of the Astrée static analyzer 4

• Precise domains for numerical computations.

• Detects runtime errors.

Challenges

[2]Challengesfoil.6 Has to analyze the original source code, not a derived “model”. Has to be sound (i.e. not say “there is no runtime error possible” when there are) Has to be precise (i.e. not warn about many possible alarms that can’t happen — false alarms) Handle floating-point well, including digital filtering algorithms

D. Monniaux — The parallel implementation of the Astrée static analyzer 6

The biggest challenge

[2]The biggest challengefoil.7

Very large software (≫ 300,000 LOC) ⇒ efficiency questions ! Commodity PC hardware ⇒ keep memory requirements low

D. Monniaux — The parallel implementation of the Astrée static analyzer 7

⇒ keep analysis times low

D. Monniaux — The parallel implementation of the Astrée static analyzer 8

Efficiency considerations

[2]Efficiency considerationsfoil.9 \underline{False “good idea”} For final “certification” of the system, only need a single pass of analysis, even if it is slow. \underline{In reality...} You want fast analysis

• for debugging the analyzer

• for using it while you develop the analyzed code

• for debugging input specifications (i.e. bounds on the inputs)

D. Monniaux — The parallel implementation of the Astrée static analyzer 9

Abstract interpretation[1]Abstract interpretationsection.10

Basic idea

[2]Basic ideafoil.11 To each program point, set of reachable memory (variable) states at this point Over-approximate the set by some constraints

Abstract operations

[2]Abstract operationsfoil.12 A program statement has semantics P: X →^{∪} X (X = possible memory states). γ(x): x abstraction (ex: shape of polyhedron), γ(x) set of concrete memory states represented Abstraction of a program statement: P: X → X Soundness: P∘γ(x) ⊆ γ ∘ P(x)

D. Monniaux — The parallel implementation of the Astrée static analyzer 12