The Trace Partitioning Abstract Domain

Laurent Mauborgne and Xavier Rival École Normale Supérieure

In order to achieve better precision of abstract interpretation based static analysis, we introduce a new generic abstract domain, the trace partitioning abstract domain. We develop a theoretical framework allowing a wide range of instantiations of the domain, proving that all these instantiations give correct results. From this theoretical framework, we go into implementation details of a particular instance developed in the Astrée static analyzer. We show how the domain is automatically configured in Astrée and the gain and cost in terms of performance and precision. Categories and Subject Descriptors: F.3.1 [Logics and Meaning of Programs]: Specifying and Verifying and Reasoning about Programs; F.3.2 [Logics and Meaning of Programs]: Semantics of Programming Languages—Program analysis General Terms: Verification, Experimentation, Theory

1. INTRODUCTION

Usually, concrete program executions can be described with traces; yet, most static analyses abstract them and focus on proving properties of the set of reachable states. For instance, checking the absence of runtime errors in C programs can be done by computing an over-approximation of the reachable states of the program and then checking that none of these states is erroneous. When computing a set of reachable states, any information about the execution history and the concrete flow paths are lost.

However, this reachable states abstraction might lead to too harsh an approximation of the program behavior, resulting in a failure of the analyzer to prove the desired property. This is easily illustrated with the following example.

1.1 A Simple Motivating Example

Let us consider the program:

int x, sgn;
l_{0} if(x < 0){
l_{1} sgn = −1;
l_{2} }else{
l_{3} sgn = 1;
l_{4} }
l_{5} y = x/sgn;
l_{6} …

Clearly sgn is either equal to 1 or −1 at point l_{4}; in particular, sgn cannot be equal to 0. As a consequence, dividing by sgn at point l_{5} is safe. However, a simple interval analysis [Cousot and Cousot 1977] would not discover it, since the least upper bound of the intervals [−1, −1] and [1, 1] is the interval [−1, 1] and 0 ∈ [−1, 1]. Indeed, it is well-known that the least upper bound operator of domains expressing convex constraints may induce a loss of precision, since elements in the convex hull

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year, Pages 1–48.

2 · X. Rival and L. Mauborgne

may be added to the result, which are not in either arguments. A simple fix would be to use a more expressive abstract domain.

The easiest refinement for this very simple example is to track zero-values for variables. But that approach is not general enough and it cannot cover the cases when we need to track an infinite number of values. It would be the case if we add to the example a random variable k, and sgn is either k − 1 or k + 1 and we divide by sgn − k.

A first possible refinement relies on disjunctive completion [Cousot and Cousot 1979], i.e., the possible values for a variable are abstracted into the union of a set of intervals. An abstract value would be a finite union of intervals; hence, the analysis would report x to be in [−1, −1] ∪ [1, 1] at the end of the above program. An important drawback of disjunctive completion is its cost: when applied to a finite domain of cardinal n, it produces a domain of 2^{n} elements, with chains of length n + 1. Moreover, the design of a widening for the domains obtained by disjunctive completion is a non-trivial issue; in particular, a good widening operator should decide which elements of a partition to merge or to widen.

A second solution to these issues is to refine the abstract domain, so as to express a relation between x and sgn. For instance, we would get the following constraint, at point l_{5}:

\{ \begin{matrix}x < 0 & ⇒ & sgn = −1 \\ x ≥ 0 & ⇒ & sgn = 1 \end{matrix}

Such an abstraction would be very costly if applied exhaustively, to every variable (especially if the program to analyze contains thousands of variables), therefore a strategy should be used in order to determine which relations may be useful to improve the precision of the result. However, the choice of the predicate which should guide the partitioning (i.e., x < 0 in the above example) may not always be obvious.

For instance, common relational domains like octagons [Miné 2001] or polyhedra [Cousot and Halbwachs 1978] would not help here, since they describe convex sets of values, so the abstract union operator is an imprecise over-approximation of the concrete union. A reduced product of the domain of intervals with a congruence domain [Granger 1989] succeeds in proving the property, since −1 and 1 are both in {1 + 2 × k | k ∈ ℕ}.

However, a more intuitive way to solve the difficulty would be to relate the value of sgn to the way it is computed. Indeed, if the true branch of the conditional was executed, then sgn = −1; otherwise, sgn = 1. This amounts to keeping some disjunctions based on control criteria. Each element of the disjunction is related to some property about the history of concrete computations, such as “which branch of the conditional was taken”. This approach was first suggested by [Handjieva and Tzolovski 1998]; yet, it was presented in a rather limited framework and no implementation result was provided. The same idea was already present in the context of data-flow analysis in [Holley and Rosen 1980], where the history of computation is traced using an automaton chosen before the analysis.

Intuitively, this approach amounts to analyzing a slightly modified version of the initial program, where the assignment at point l_{5} is duplicated and moved at the end of both branches in the if-statement as shown below. This program has a

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

The Trace Partitioning Abstract Domain · 3

strong semantic relation with the initial code; in particular, it will compute exactly the same value for y at point l_{6}, for any input x.

int x, sgn;
l_{0} if(x < 0){
l_{1} sgn = −1;
l′_{5} y = x/sgn;
l_{2} }else{
l_{3} sgn = 1;
l′′_{5} y = x/sgn;
l_{4} }
l_{6} …

Though, this technique based on syntactic program rewriting may not be completely satisfactory, since we may want to perform partitioning operations which cannot be expressed in the programming language under consideration. As a consequence, we propose a specific abstract domain construction, which allows for a more flexible and more general use of partitioning in static analyses. Furthermore, we propose to state and prove the semantic correctness of this domain in the same way as other abstract domains are usually formalized, which makes this technique a good candidate for being integrated in other static analysis tools.

Choosing the relevant partitioning (which explicit disjunctions to keep during the static analysis) is a rather difficult and crucial point. In practice, it can be necessary to make this choice at analysis time. Another possibility presented in [Ammons and Larus 1998] is to use profiling to determine the partitions, but this approach is relevant in optimization problems only.

1.2 Trace Partitioning in the Astrée Analyzer

The previous example —and many others— were encountered during the development of the Astrée analyzer [Blanchet et al. 2002; 2003; Cousot et al. 2005]. The Astrée analyzer is an abstract interpretation-based static program analyzer aiming at proving automatically the absence of run time errors in programs written in the C programming language. The errors detected by Astrée include out-of-bound array access, illegal arithmetic operations, overflows and violated simple user-defined assertions [Mauborgne 2004]. Astrée has been applied with success to large safety critical real-time software, producing a correctness proof for complex software without any false alarm in a few hours of computation [Cousot et al. 2005]. The challenge of analyzing such large codes without any false alarms is very demanding, especially in a context of large number of global variables and intensive floating point computation. In order to achieve that result, we needed techniques which are

— well founded theoretically to provide a good confidence in the correctness proofs;

— efficient to scale up to programs with thousands of global variables and hundred of thousands of lines of code;

— flexible enough to provide a solution to many precision issues, in order to be reactive to end-users of the analyzer.

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

The trace partitioning abstract domain presented in this paper fulfills those requirements. We provide a theoretical framework for trace partitioning, that can be instantiated in a broad series of cases. More partitioning configurations are supported than in [Handjieva and Tzolovski 1998] and the framework also supports dynamic partitioning (choice of the partitions during the abstract computation).

Also, we provide detailed practical information about the use of the trace partitioning domain. In particular, we describe the cases where partitioning can be performed and the strategies used in Astrée to apply these techniques in an efficient way so as to get few or no false alarms and maintain a reasonable analysis cost. Efficient data-structures are very important for the efficiency of the analysis, so we also describe them precisely. These features are supported by the experience of the design, implementation and practical use of the Astrée analyzer.

Finally, we assess the efficiency of the technique by presenting experimental results with Astrée and more examples where Astrée uses trace partitioning to solve precision issues. Furthermore, we discuss these results so as to stress the subtle interactions between partitioning, precision and analysis cost.

1.3 Outline of the Paper

Section 2 introduces the most basic notions and notations used throughout the paper.

The next two sections are devoted to the theoretical trace partitioning framework. The control-based partitioning of a transition system is formalized in Section 3; it is the basis for the definition of trace partitioning abstract domains in Section 4.

Then, we describe the structure of the trace partitioning domain used in the Astrée analyzer in Section 5, and the implementation of this domain, together with partitioning strategies and detailed experimental evaluations in Section 6.

Last, Section 7 concludes and reviews related works.

2. ABSTRACT INTERPRETATION-BASED STATIC ANALYSIS

This section introduces basic notions and notations used in the paper. It also collects the most important technical facts about the Astrée analyzer, which are required in order to understand the future sections about trace partitioning in Astrée.

2.1 Notations

In this paper, all example programs are written in the C language (which is the language analyzed by Astrée). However, we provide here a formal model of programs, as transition systems, so that all techniques and algorithms can be generalized to other languages as well.

2.1.1 Syntax. We describe an imperative (C) program with a transition system. More precisely, we let 𝕍 denote a set of values; 𝕏 denote a finite set of memory

locations (aka variables). A memory state (or store) describes the values stored in the memory at a precise time in the execution of the program; it is a mapping of program variables into values. A store is a function σ ∈ 𝕄, where 𝕄 = 𝕏 → 𝕍.

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

A control state (or program point) roughly corresponds to the program counter at a precise time in the execution of the program; we usually write 𝕃 for the set of control states.

A state s is a pair made of a control state l ∈ 𝕃 and a memory state σ ∈ 𝕄. We write 𝕊 for the set of states, so 𝕊 = 𝕃 × 𝕄.

A program (or transition system) is defined by a set of initial states 𝕊^{i}, and a transition relation (→) ⊆ 𝕊 × 𝕊, which describes how the execution of the program steps from one state to the next one. In practice, 𝕊^{i} = {l^{i}} × 𝕄, where l^{i} ∈ 𝕃 is the entry control state, i.e. the first point in the program.

Example 2.1.1. (Simple Program) Applying those notations to the simple program of section 1, we have 𝕃 = {l_{0}, l_{1}, l_{2}, l_{3}, l_{4}, l_{5}} and the memory states are in 𝕄 = {x, y, sgn}→ℕ. The initial states are all the states with control states l_{0}.

Real world programs may crash, e.g., due to a memory or arithmetic error. Therefore, we could also add a special error state. But in this paper, we do not need to deal formally with errors so we omit it.

Last, we will also consider inter-procedural programs. Then, a control state is defined by a pair (κ, l ), where κ is a calling stack (stack of function names) and l a syntactic control point. We write 𝕜 for the set of stacks, and keep the notation 𝕃 for the syntactic control points, so that a state in an inter-procedural program is a tuple in (𝕜 × 𝕃) × 𝕄. Equivalently, we may denote states with 3-tuples (κ, l , ρ).

2.1.2 Semantics. We assume here that a program P is defined by the data of a tuple (𝕊^{i}, →). The most common semantics for describing the behavior of transition systems is the operational semantics, which we sketch here. It was introduced, e.g. in [Plotkin 1981].

An execution of a program is represented with a sequence of states, called a trace; the semantics of the program collects all such executions:

Definition 2.1.2. (Trace, Semantics) A trace σ is a finite sequence ⟨s_{0}, …, s_{n}⟩ where s_{0}, …, s_{n} ∈ 𝕊. We write 𝕊^{⋆} for the set of such traces.

A trace of P is a trace such that any two successive states are bound by the transition relation: ∀i, s_{i} → s_{i+1}. The semantics ⟦P ⟧ of P is the set of traces of P, i.e. ⟦P ⟧ = {⟨s_{0}, …, s_{n}⟩ ∈ 𝕊^{⋆} | s_{0} ∈ 𝕊^{i} ∧ ∀i, s_{i} → s_{i+1}}.

Note that we restricted to finite traces (and safety properties) to simplify the presentation.

We can remark that the semantics ⟦P ⟧ of P writes down as a least fixpoint:

⟦P ⟧ = lfp_{S^{i}}^{⊆}F\overrightarrow{P}

where F\overrightarrow{P} is the semantic function, defined by:

\begin{aligned}F\overrightarrow{P} : & 𝕊^{⋆} & → & 𝕊^{⋆} \\ & E & ↦ & E ∪ \{⟨s_{0}, …, s_{n}, s_{n+1}⟩ | ⟨s_{0}, …, s_{n}⟩ ∈ E ∧ s_{n} → s_{n+1}\} \end{aligned}

and S^{i} = {⟨s⟩ | s ∈ 𝕊^{i}}.

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

2.2 Abstraction

The semantics introduced in Section 2.1.2 is not decidable; therefore, proving safety properties about programs usually requires computing an approximation of the reachable states. We describe such an abstraction here.

2.2.1 Abstraction of Traces. We proceed to the abstraction of traces into reachable states: we wish to abstract the traces into an approximation for the set of states which appear in at least one execution of P.

We assume that an abstract domain (D_{𝕄}^{♯} , ⊑) for representing sets of stores is defined, together with a concretization function γ_{𝕄} : D_{𝕄}^{♯} → P(𝕄).

The abstract values in such a domain usually express constraints among the variables of the program. The interval domain [Cousot and Cousot 1977] allows to express ranges the variables should live in. Relational abstractions allow to express constraints involving several variables; we can cite the polyhedra [Cousot and Halbwachs 1978], octagons [Miné 2001] as examples of relational abstractions.

We let the abstraction for approximating the concrete semantics be defined by:

— the abstract domain D^{♯} = 𝕃 → D_{𝕄}^{♯} , with the pointwise ordering induced by ⊑ (which we also write ⊑);

— the concretization function γ : I ∈ D^{♯} ↦ {⟨(l_{0}, ρ_{0}), …, (l_{n}, ρ_{n})⟩ | ∀i, ρ_{i} ∈ γ_{𝕄} (I(l_{i}))}.

Intuitively, this very simple abstraction collects the memory states corresponding to each control state and applies the store abstraction to the resulting sets of stores.

2.2.2 Abstract Operations. Moreover, we assume that the domain D_{𝕄}^{♯} provides some sound abstract operations (in the following, we write 𝕖 for the set of expressions, 𝕝 for the set of l-values, and 𝔹 for the set of booleans):

— a least element ⊥, such that γ_{𝕄} (⊥) = ∅;

— a greatest element ⊤, such that γ_{𝕄} (⊤) = 𝕄;

— an abstract join operator ⊔, approximating the concrete operator (∀x, y ∈ P(𝕄), x^{♯}, y^{♯} ∈ D_{𝕄}^{♯} , x ⊆ γ_{𝕄} (x^{♯}) ∧ y ⊆ γ_{𝕄} (y^{♯}) ⟹ x ∪ y ⊆ γ_{𝕄} (x^{♯} ⊔ y^{♯})).

— a sound counterpart guard: 𝕖 × 𝔹 × D_{𝕄}^{♯} → D_{𝕄}^{♯} for the concrete testing of conditions:

\begin{matrix}∀ρ ∈ 𝕄, e ∈ 𝕖, b ∈ 𝔹, d ∈ D_{𝕄}^{♯} , \\ \begin{matrix}& ρ ∈ γ_{𝕄} (d) \\ ∧ & ⟦e⟧(ρ) = b \end{matrix} \} ⟹ ρ ∈ γ_{𝕄} (guard(e, b, d)) \end{matrix}

Since the operator guard: (e, b, d) ↦ d trivially satisfies the above assumption, we assume that the guardoperator is reductive:

∀ρ ∈ 𝕄, e ∈ 𝕖, b ∈ 𝔹, γ_{𝕄} (guard(e, b, d)) ⊆ γ_{𝕄} (d)

— a sound counterpart assign: 𝕝 × 𝕖 × D_{𝕄}^{♯} → D_{𝕄}^{♯} for the concrete assignment:

\begin{matrix}∀ρ ∈ 𝕄, ∀l ∈ 𝕝, e ∈ 𝕖, d ∈ D_{𝕄}^{♯} , \\ \begin{matrix}& ρ ∈ γ_{𝕄} (d) \\ ∧ & ⟦l⟧(ρ) = x \\ ∧ & ⟦e⟧(ρ) = v \end{matrix} \} ⟹ ρ[x ← v] ∈ γ_{𝕄} (assign(l, e, d)) \end{matrix}

The purpose of these abstract operations is to ensure that we can use them in the design of a static analyzer, which over-approximates each computation step. As a result, the soundness of such an analyzer follows from a simple fixpoint transfer theorem, like:

Theorem 2.2.1. (Fixpoint transfer) We let x ∈ P(𝕄), d ∈ D_{𝕄}^{♯} . Let F : P(𝕄) → P(𝕄) and F^{♯} : D_{𝕄}^{♯} → D_{𝕄}^{♯} . Then, if x ⊆ γ_{𝕄} (d), and F ∘ γ_{𝕄} ⊆ γ_{𝕄} ∘ F^{♯}, then lfp_{x}F ⊆ γ_{𝕄} (lfp_{d}F^{♯}).

2.2.3 Widening Iteration and Convergence. The fixpoint-transfer scheme presented above leaves one major issue to be addressed: the sequences of abstract iterates might be infinite, in case the abstract domain has infinite increasing chains (this is the case for most domains, including intervals, polyhedra, octagons...). Therefore, we replace the abstract join operator with a widening operator [Cousot and Cousot 1977], which is an approximate join [Cousot and Cousot 1992b], with additional termination properties:

Definition 2.2.2. (Widening operator) A widening is a binary operator ∇ on D^{♯}, which satisfies the two following properties:

(1) ∀x^{♯}, y^{♯} ∈ D^{♯}, x^{♯} ⊑ x^{♯}∇y^{♯} ∧ y^{♯} ⊑ x^{♯}∇y^{♯}

(2) For any sequence (x_{n})_{n∈ℕ} , the sequence (y_{n})_{n∈ℕ} defined below is not strictly increasing:

\{ \begin{matrix}& y_{0} & = & x_{0} \\ ∀n ∈ ℕ, & y_{n+1} & = & y_{n}∇x_{n+1} \end{matrix}

The following theorem [Cousot and Cousot 1977] shows how widening operators make it possible to compute in a finite number of iterations a sound over-approxima-tion for the concrete properties:

Theorem 2.2.3. (Abstract iteration with widening) We assume a concretization γ : D^{♯} → D is defined and that F^{♯} is such that F ∘ γ ⊆ γ ∘ F^{♯}. Let x ∈ D, x^{♯} ∈ D^{♯}, such that x ⊆ γ(x^{♯}). We define the sequence (x_{n})_{n∈ℕ} as follows:

\{ \begin{matrix}& x_{0} & = & x^{♯} \\ ∀n ∈ ℕ, & x_{n+1} & = & x_{n}∇F^{♯}(x_{n}) \end{matrix}

Then, the sequence (x_{n})_{n∈ℕ} is ultimately stationary and its limit lim(x_{n})_{n∈ℕ} is a sound approximation of lfp_{x}F:

lfp_{x}F ⊆ γ(lim(x_{n})_{n∈ℕ} )

Proof. See [Cousot and Cousot 1977].

2.3 Static Analysis

Last, we briefly review the design of a denotational style abstract interpreter for a fragment of C (in this subsection, we do not consider functions; they are added in the next section). In particular, the iterator of the Astrée analyzer follows this scheme. In this subsection, we assume that a domain D_{𝕄}^{♯} is given. Indeed, the iterator of the Astrée analyzer accepts an abstract domain for representing sets of stores as a parameter.

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

2.3.1 The Core of the Interpreter. Let s be a statement; we write l_{⊢} (resp. l_{⊣}) for the control point before (resp. after) s. We let the denotational semantics of s be the function ⟦s⟧_{δ} = α_{tF [l_{⊢},l_{⊣}]}(⟦s⟧), defined by:

\begin{aligned}∀E ⊆ 𝕊^{⋆}, α_{tF [l_{⊢},l_{⊣}]}(E) : & 𝕄 & → & P(𝕄) \\ & ρ & ↦ & \{ρ′ | ∃⟨(l_{⊢}, ρ), …, (l_{⊣}, ρ′)⟩ ∈ E\} \end{aligned}

The abstract semantics of s is the function ⟦s⟧^{♯} : D_{𝕄}^{♯} → D_{𝕄}^{♯} , which inputs an abstract pre-condition and returns a post-condition. It should be sound in the sense that the output of the abstract semantics should over-approximate the set of output states of the underlying, concrete denotational semantics.

We propose on Figure 1 the definition of a very simple denotational semanticsbased interpreter; we provide for each common language construction (assignment, conditional, loop, reading of an input, assertion) a simple abstract transfer function. The abstract semantics displayed in Figure 1 is sound:

statement s  abstract semantics
x := e;  ⟦s⟧^{♯} : d ↦ assign(x, e, d)
if(e){s_{0}}else{s_{1}} ⟦s⟧^{♯} : d ↦ ⟦s_{0}⟧^{♯}(guard(e, true, d)) ⊔ ⟦s_{1}⟧^{♯}(guard(e, false, d))
while(e){s_{0}}  ⟦s⟧^{♯} : d ↦ guard(e, false, lfp^{♯}F^{♯}) where
F^{♯} : D_{𝕄}^{♯} → D_{𝕄}^{♯}
d_{0} ↦ d_{0} ⊔ ⟦s_{0}⟧^{♯}(guard(e, true, d))

and lfp^{♯} computes an abstract post-fixpoint, using ∇

assert(e);  ⟦s⟧^{♯} : d ↦ guard(e, true, d)

Fig. 1: A simple abstract interpreter

Theorem 2.3.1. (Soundness of the analysis) The abstract semantics soundly approximates the denotational semantics:

∀ρ, ρ′ ∈ 𝕄, d ∈ D_{𝕄}^{♯} , ρ ∈ γ_{𝕄} (d) ∧ ρ′ ∈ ⟦s⟧_{δ}(ρ) ⟹ ρ′ ∈ γ_{𝕄} (⟦s⟧^{♯}(d))

Proof. By induction on the structure of the code.

The case of the loop is based on the soundness of the lfp^{♯} operator; in practice, it is derived from a widening operator ∇_{𝕄} over D_{𝕄}^{♯} , so the soundness and termination of lfp^{♯} follow from Theorem 2.2.3.

As a corollary, the abstract semantics is sound with respect to the standard, operational semantics. Indeed, if l_{⊢} : s; l_{⊣} is a program, then:

∀⟨(l_{⊢}, ρ_{⊢}), …, (l_{⊣}, ρ_{⊣})⟩ ∈ ⟦s⟧, ∀d ∈ D_{𝕄}^{♯} , ρ_{⊢} ∈ γ_{𝕄} (d) ⟹ ρ_{⊣} ∈ γ_{𝕄} (⟦s⟧^{♯}(d))

The main advantage of such a static analysis scheme is that it reduces the need for storing abstract invariants to a minimum and it provides a very natural iteration strategy.

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

2.3.2 Output of the Analysis. We showed how to compute a sound invariant after a statement from a pre-condition; however, the Astrée analyzer not only outputs an invariant in the end of the analyzed program, but also:

— Alarm reports, if the invariants do not ensure that all critical operations (including arithmetic operations, memory operations, user assertions) are safe;

— Local invariants, if the invariant export option is enabled: then, the analyzer saves local invariants for all control states in the program, so that the user can scan the results of the analysis (of course, this option requires a lot of memory, when a large program is being analyzed, which is the reason why we insisted on the choice of a strategy, where the export of all local invariants is not mandatory).

In particular, the analyzer is equivalent to an analyzer computing an invariant in D^{♯} = 𝕃 → D_{𝕄}^{♯} , even though it explicitly outputs only an invariant in D_{𝕄}^{♯} .

2.3.3 Running the Analyzer. The previous paragraphs summarize the principle of the iterator of the Astrée analyzer; however, during the analysis of a program, Astrée performs many other operations, including:

— several pre-processing steps, such as constant propagation in the code to analyze;

— the choice of analysis parameters, which affect the abstract domain and the iteration strategy, such as the choice of packs of variables relations should be computed for; similar choices will be made in the case of the trace partitioning domain (the strategy defining which partitions should be created will be exposed in Section 6.2).

The implementation of the abstract domain was guided by the kind of predicates required for tight invariants to be inferred. By default, the analyzer uses a reduced product of a series of abstract domains including intervals [Cousot and Cousot 1977], octagons [Miné 2001], boolean relations (i.e., a generalization of BDDs [Bryant 1986]), arithmetic-geometric progressions [Feret 2005], and a domain dedicated to the analysis of digital filters [Feret 2004] (command line options allow the user to disable some of these domains).

3. CONTROL-BASED PARTITIONING OF TRANSITION SYSTEMS

In this section, we formalize the notion of partition of a transition system. Such partitions should describe the same set of traces as the semantics of the initial program (or an approximation of it) and should allow to distinguish traces depending on the history of control flow. As a result, we can address the imprecision mentioned in the introduction by analyzing a partitioned system.

3.1 Partitioning Control States

First of all, we underline that partitioning the reachable states with the control states is a rather common approach in static analysis. Later, we generalize drastically this technique.

3.1.1 Non-Procedural Case. Indeed, the analysis proposed in Section 2 relies on this kind of partitioning. The abstraction of sets of traces can be seen as a two steps abstraction:

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

(1) abstraction of traces into states, with partitioning:

(P(𝕊^{⋆}), ⊆) ⟶ ⟵_{α_{P(𝕊)}}^{γ_{P(𝕊)}} (𝕃 → P(𝕄), ⊆) ; \begin{aligned}α_{P(𝕊)} : & P(𝕊^{⋆}) & → & (𝕃 → P(𝕊)) \\ & E & ↦ & λ(l ∈ 𝕃) · \{ρ | ⟨…, (l , ρ), …⟩ ∈ E\} \end{aligned}

Whenever the concretization function is defined straightforwardly from the abstraction function, we provide the abstraction function only: in a complete lattice, any monotone abstraction function defines a unique concretization [Cousot and Cousot 1977].

(2) abstraction of sets of states, defined by the concretization function γ_{𝕄} : D_{𝕄}^{♯} → P(𝕄) as in Section 2.2.1.

The first step includes a partitioning in the sense of [Cousot and Cousot 1992a, §4.2.3.2]. Indeed, it amounts to partitioning the set of sets of states using the partition {{(l , ρ) | ρ ∈ 𝕄} | l ∈ 𝕃}; the resulting domain is in bijection with 𝕃 → P(𝕄).

3.1.2 Procedural Case. In case the language features procedures, similar abstractions are usually implemented.

When designing an analysis for such a procedural language, one faces the problem of deciding how to replace the abstraction mentioned in step 1 above. Among the possible choices, we can cite [Sharir and Pnueli 1981]:

— the full abstraction of the stack: we may abstract away the stack and keep only the control states (the analysis is insensitive to the calling context):

\begin{aligned}α_{P(𝕊)} : & P(𝕊^{⋆}) & → & (𝕃 → P(𝕄)) \\ & E & ↦ & λ(l ∈ 𝕃) · \{ρ | ∃κ ∈ 𝕜, ∃⟨…, (κ, l , ρ), …⟩ ∈ E\} \end{aligned}

— the partitioning with the stack: we may keep the stack, i.e. abstract traces into functions mapping pairs made of a stack and a control state into a set of memory states (analysis completely sensitive to the calling context):

\begin{aligned}α_{P(𝕊)} : & P(𝕊^{⋆}) & → & ((𝕜 × 𝕃) → P(𝕄)) \\ & E & ↦ & λ((κ, l ) ∈ (𝕜 × 𝕃)) · \{ρ | ⟨…, (κ, l , ρ), …⟩ ∈ E\} \end{aligned}

This approach amounts to inlining functions; it works only in the case of nonrecursive function calls (the stack may grow infinite in the case of recursive calls). This technique is used in Astrée.

Many intermediate abstractions exist, which allow to retain a good level of precision in some cases and abstract long sequences of calls (the main such technique is klimiting [Jones and Muchnick 1979]).

Another approach to the analysis of procedural programs is to model the effect of each function (intra-procedural phase) and then, to perform a global iteration [Reps et al. 1995]. This technique relies on the resolution of the reachability along “inter-procedural realizable paths”, which is also based on some abstraction of the stack (this method was also used in slicing [Horwitz et al. 1988]).

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

3.2 Partitions and Coverings

We now set up the notions of partitioned set and partitioned system. Our goal is to design sets of finer partitions at the control structure level, which will be used in the following sections as a basis for building trace partitioning domains.

3.2.1 Partitioning Function. A covering of a set F is a family of nonempty subsets of F, such that any element of F belongs to some element of the family. A partition is a covering such that any two distinct elements of the family are disjoint; in particular, for any element x ∈ F, there exists a unique element A of the partition such x ∈ A. In the following, we need to index the elements of coverings (resp. partitions); hence, the following definition resorts to functions, defined on a set of indexes.

Definition 3.2.1. (Partitioned set) Let I, F be two sets, and δ : I → P(F) (I is the set of indexes). Then:

— δ is a covering of F if and only if:

∀x ∈ I, δ(x) ≠ ∅

and,

F = ⋃_{x∈I} δ(x)

— δ is a partition of F if and only if it is a covering and:

∀x, y ∈ I, x ≠ y ⟹ δ(x) ∩ δ(y) = ∅

We note that a covering (resp. partitioning) δ of F defines an abstraction of (P(F), ⊆):

Lemma 3.2.1. (Partitioning abstraction) Let α_{δ} and γ_{δ} be defined by:

α_{δ} : P(F)  → (I → P(F))
E  ↦ λ(x ∈ I) · E ∩ δ(x)
γ_{δ} : (I → P(F)) → P(F)
ϕ  ↦ ⋃_{x∈I} ϕ(x)

Then, if δ is a covering, we have a Galois-connection (P(F), ⊆) ⟶ ⟵_{α_{δ}}^{γ_{δ}} (I → P(F), ⊆), and α_{δ} is injective (Galois injection).

Moreover, if δ is a partition, then α_{δ} is bijective (Galois bijection).

Proof. Straightforward application of the definition of coverings.

Definition 3.2.1 would allow to set up very general notions of trace partitioning. In particular, the partitioning of traces using the control state of the last state (Section 3.1) fits in this framework (with I = 𝕃); the case of calling stacks is similar (with either I ≡ 𝕃, or I = 𝕜 × 𝕃, or other partitions). We may even design some weaker partitions: for instance, we may decide to merge together the states corresponding to several distinct control states (with I a partition of 𝕃). In case I is a singleton, the abstraction is flow insensitive. However, we wish to derive the partitions from the history of executions; therefore, the following introduces the notion of partitioned system.

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

3.2.2 Partitioning Transitions. In the following, we assume that a program P is given, and defined by (𝕊^{i}, →). We consider partitions finer than the partition defined by I = 𝕃 only. More precisely, we let 𝕋 be a set of tokens, and 𝔗 = P(𝕋).

We define extended transition systems as transition systems over the sets of labels extended with a set of tokens T ⊆ 𝕋; it is basically defined by T and by extensions of the set of initial states and of the transition relation.

Such a system P_{0} is a covering of P_{1} if and only if it simulates the transitions of P_{1}; moreover, P_{0} is a partition if and only if any transition in P_{1} is simulated by exactly one transition in P_{0} (and the same for the initial states). System P_{0} is complete in case it does not add any fictitious transition, when compared to P_{1}. Intuitively, a complete partition or covering P_{0} shall describe the same set of traces as P_{1}, up-to some information added in the control states. The main difference between a covering and a partition is that the covering may not ensure the unicity of the counterpart of a trace of the initial program.

The extra information embedded in the control structure of the extended system will be the basis of the partitioning abstraction. The notions of covering, partitioning and complete systems are formalized in the following definition.

Definition 3.2.2. (Partitioned system) Let T ∈ 𝔗. We write 𝕃_{T} for the set of partitioned control states 𝕃 × T, 𝕊_{T} for the set of partitioned states 𝕃_{T} × 𝕄, and 𝕊_{T}^{i} ⊆ 𝕊_{T} for a set of partitioned initial states, and →_{T} for a transition relation among partitioned states. An extended system is defined by the data of a tuple (T, 𝕊_{T}^{i} , →_{T}). Last, 𝕊_{T}^{⋆} denotes the set of traces made of states in 𝕊_{T}.

For all T, T′ ∈ 𝔗 and τ : T → T′, we define the forget functions for control states, for states and for traces as follows:

π_{τ}^{𝕃} : 𝕃_{T}  → 𝕃_{T′}
(l , t)  ↦ (l , τ(t))
π_{τ}^{𝕊} : 𝕊_{T}  → 𝕊_{T′}
((l , t), ρ) ↦ (π_{τ}^{𝕃} (l , t), ρ)
π_{τ}^{𝕊^{⋆}} : 𝕊_{T}^{⋆}  → 𝕊_{T′}^{⋆}
⟨s_{0}, …, s_{n}⟩ ↦ ⟨π_{τ}^{𝕊} (s_{0}), …, π_{τ}^{𝕊} (s_{n})⟩

We consider the extended systems P_{T} = (𝕃_{T} , 𝕃_{T}^{i} × 𝕄, →_{T}) and P_{T′} = (𝕃_{T′}, 𝕃_{T′}^{i} × 𝕄, →_{T′}), and the function τ : T → T′.

(1) P_{T} is a τ-covering of P_{T′} if and only if:

— 𝕊_{T′}^{i} ⊆ π_{τ}^{𝕊} (𝕊_{T}^{i} )

— ∀s_{0} ∈ 𝕊_{T} , s′_{1} ∈ 𝕊_{T′}, π_{τ}^{𝕊} (s_{0}) →_{T′} s′_{1} ⟹ ∃s_{1} ∈ 𝕊_{T} , \{ \begin{matrix}s′_{1} = π_{τ}^{𝕊} (s_{1}) \\ s_{0} →_{T} s_{1} \end{matrix}

(2) P_{T} is a τ-partition of P_{T′} if and only if:

— ∀s′ ∈ 𝕊_{T′}^{i}, ∃!s ∈ 𝕊_{T}^{i} , s′ = π_{τ}^{𝕊} (s)

— ∀s_{0} ∈ 𝕊_{T} , s′_{1} ∈ 𝕊_{T′}, π_{τ}^{𝕊} (s_{0}) →_{T′} s′_{1} ⟹ ∃!s_{1} ∈ 𝕊_{T} , \{ \begin{matrix}s′_{1} = π_{τ}^{𝕊} (s_{1}) \\ s_{0} →_{T} s_{1} \end{matrix}

(3) P_{T} is τ-complete with respect to P_{T′} if and only if:

— π_{τ}^{𝕊} (𝕊_{T}^{i} ) ⊆ 𝕊_{T′}^{i}

— ∀s_{0}, s_{1} ∈ 𝕊_{T} , s_{0} →_{T} s_{1} ⟹ π_{τ}^{𝕊} (s_{0}) →_{T′} π_{τ}^{𝕊} (s_{1})

\xymatrix{ & (l_{0}, t) \ar@{-->}[dl] \ar[dr] \\ (l_{1}, t) \ar[dr] &  & (l_{2}, t) \ar@{-->}[dl] \\  & (l_{3}, t) \ar[d] \\  & (l_{4}, t)}

(a) System P_{0}

\xymatrix{ & (l_{0}, t_{0}) \ar@{-->}[dl] \ar@{-->}[dr] \\ (l_{1}, t_{1}) \ar[d] &  & (l_{2}, t_{2}) \ar[d] \\ (l_{3}, t_{1}) \ar@{-->}[dr] &  & (l_{3}, t_{2}) \ar@{-->}[dl] \\  & (l_{4}, t_{0})}

(b) System P_{1}

\xymatrix{ & (l_{0}, t_{0}) \ar@{-->}[dl] \ar@{-->}[dr] \\ (l_{1}, t_{1}) \ar[d] &  & (l_{2}, t_{2}) \ar[d] \\ (l_{3}, t_{1}) \ar[d] &  & (l_{3}, t_{2}) \ar[d] \\ (l_{4}, t_{1}) &  & (l_{4}, t_{2})}

(c) System P_{2}

Fig. 2: Partitioned systems

The notions of “complete covering” or “complete partition” are derived from the above definition as well.

Example 3.2.3. (Partitioned systems) We make the assumption that 𝕄 is a singleton here, so that transitions relations are mere relations among control states. Let us consider the two extended systems P_{0} and P_{1}, displayed respectively in Figure 2(a) and in Figure 2(b).

— the original system represents a program with a conditional statement followed by one statement (each branch of the conditional contains exactly one statement);

— P_{0} is isomorphic to the original system; it corresponds to T_{0} = {t}

— P_{1} is an extended system defined by T_{1} = {t_{0}, t_{1}, t_{2}}.

We consider the following forget function τ : λ(t_{i} ∈ T_{1}) · t.

Then, any execution of P_{0} corresponds to exactly one execution of P_{1}: for instance, ⟨(l_{0}, t), (l_{1}, t), (l_{3}, t), (l_{4}, t)⟩ corresponds to ⟨(l_{0}, t_{0}), (l_{1}, t_{1}), (l_{2}, t_{1}), (l_{4}, t_{0})⟩. In particular, any transition step in P_{0} is mimicked by exactly one transition step in P_{1} as mentioned in Definition 3.2.2, 2. Therefore, P_{1} is a τ-partition of P_{0}.

Similarly, we can check that any execution, including one-step transitions of P_{1} corresponds to some execution of P_{0}. Hence, P_{1} is τ-complete with respect to P_{0}.

These two properties make P_{1} a very useful extended system, for analyzing P_{0}. Intuitively, the extended system P_{1} corresponds to a partition of P_{0} obtained

by delaying the merge in the exit of the conditional statement after the statement following the conditional, i.e. at point l_{4}; this amounts to doing the following rewriting:

l_{0} : if(e){
l_{1} : s_{1}
}else{
l_{2} : s_{2}
}
l_{3} : s_{3}
l_{4} : …

⟶

(l_{0}, t_{0}) : if(e){
(l_{1}, t_{1}) : s_{1};
(l_{3}, t_{1}) : s_{3}
}else{
(l_{2}, t_{2}) : s_{2};
(l_{3}, t_{2}) : s_{3}
}
(l_{4}, t_{0}) : …

In particular, applying this partitioning to the example presented in the introduction (Section 1.1) would solve the imprecision. Indeed, it would allow proving that

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

sgn cannot be equal to 0 at l_{5}, so that the division by sgn is safe; moreover, it allows proving that the absolute value of x computed in y is always positive.

The system P_{2} displayed in Figure 2(c) is also a complete partition of P_{0}. It amounts to performing a similar partitioning of the conditional structure without merging the traces at point l_{4}. Such a partitioning would be more costly if applied to many if-statements in a large program.

In fact, we can also note that P_{2} is a complete partition of P_{1}.

Example 3.2.4. (Covering) We now propose an example of a covering of a system, which is not a partition of it. In this example, we assume that P is made of a sequence of n conditional structures:

l_{0} : if(e){…};
l_{1} : if(e){…};
⋮
l_{n−1} : if(e){…};
l_{n} :

Moreover, we assume that we need to prove at the end of P a property which states that all final states reached after visiting the true branch of the conditional structure at point l_{i} satisfy property p_{i}, where p_{0}, p_{1}, …, p_{n−1} are simple memory state properties (for instance, each of these properties could state that the values of the variables of the program should be in a given range). For instance, we could imagine that each conditional structure tracks for some abnormal inputs and should remedy it; then, we may want to check that the resolution of each kind of abnormal input is done according to a specification.

Then, we may be tempted to apply the same partitioning scheme as we mentioned in Example 3.2.3 for each conditional structure and to define a let a partition be defined by a choice of a branch for each conditional structure. The drawback of this approach is that the number of tokens to introduce would be 2^{n}, so that the cost of the analysis would be exponential in the size of the program at best.

However, this set of partitions is overkill in this case. Indeed, we could choose the following set of partitioning tokens (the definition of the extended system from this set of tokens is straightforward):

— for all i such that 0 ≤ i ≤ n − 1, t_{i} collects the traces which visited the true branch of the conditional structure at point l_{i};

— t collects the traces which visited the false branch of all conditional structures.

Clearly, this set of partitions is adequate to prove the property mentioned above, since it allows to discriminate the traces which visited the true branch of any conditional structure in the program. Moreover, it only defines a covering of P since a trace σ may have visited the true branch of several conditional structures; then, it would be simulated by several traces of the extended system: indeed, for each point l_{i} corresponding to a conditional structure visited by σ, there is a trace of the extended system ending at (l_{n}, t_{i}) which simulates σ. Therefore, the extended system is a covering of P, whereas it is not a partition.

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

On the other hand, any transition in the extended system corresponds to a transition in P, so the extended system is a complete covering.

The number of tokens in the covering is only linear in the size of P, whereas the size of the partition suggested above is exponential. In general, we can expect coverings to express properties at a cheaper cost than partitions, since they allow for more flexibility (a trace might be in several elements of a covering).

Example 3.2.5. (Incomplete partitioning) The notion of completeness is related to the precision of the partitioning: completeness is not achieved when the partitioned system allows some transitions which do not exist in the initial program.

This is useful when one does not want to take into account e.g., a condition. For instance, we could replace a conditional structure with a non-deterministic branching, if this will not impact the proof of the property we expect the analysis to prove, as is the case in the program below, where we want to prove the correctness of the division by x, using the numerical domain of intervals.

if(complicated condition)

x = 1; else

x = 2; y = z/x;

Obviously, considering incomplete systems should help reducing the cost of static analyses, but may cause them to fail to prove the appropriate results.

Remark 3.2.6. (Extending the notion of covering) We may extend the definition of covering, by replacing the τ function with a relation (⇒_{τ}) ⊆ T × T′. Then, the function π_{τ}^{𝕃} becomes a relation (⇒_{τ}^{𝕃}) ⊆ 𝕃_{T} × 𝕃_{T′}.

Intuitively, t ⇒_{τ}^{𝕃} t′ means that the token t is “simulated” by t′ in P_{T′}. Clearly, this definition is weaker, since a token t may be simulated by several tokens in P_{T′}.

The results in the following would extend to this weaker definition of covering system.

Note that we do not require the set of partitions to be finite. This assumption is not required in order to prove the partitioning correct.

3.2.3 Trivial Extension. We let t_{ϵ} ∈ 𝕋 and write T_{ϵ} = {t_{ϵ}}. The trivial extension of P is the extended system P_{ϵ} = (𝕃_{ϵ}, 𝕊_{ϵ}^{i}, →_{ϵ}), where:

— 𝕃_{ϵ} = 𝕃 × T_{ϵ};

— 𝕊_{ϵ}^{i} = {((l , t_{ϵ}), ρ) | (l , ρ) ∈ 𝕊^{i}};

— ((l_{0}, t_{ϵ}), ρ) →_{ϵ} ((l_{1}, t_{ϵ}), ρ) ⟺ (l_{0}, ρ) → (l_{1}, ρ).

This extended system is isomorphic to P (the traces of both programs are equal up to isomorphism); it is the “simplest” extension of P. We write π_{ϵ}^{𝕊^{⋆}} for the trivial mapping of traces of P_{ϵ} into traces of P.

3.3 Soundness of Control Partitioning

In the two following subsections, we set up an ordering, so as to compare the semantics of partitioned systems and build an ordering among partitioned systems.

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

These properties are the basis for the definition of the trace partitioning domains, which will be stated in Section 4).

The semantics of extended systems is defined in the usual way, as in Section 2.1.2. Furthermore, we propose to partition the semantics with the partitioned control states including the token (i.e., we choose E = 𝕃_{T} = 𝕃 × T), of the last state in the traces, which amounts to applying the same abstraction as α_{P(𝕊)} (Section 3.1) in the case of the extended system:

Definition 3.3.1. (Partitioned semantics) If P_{T} is the extended system defined by (T, 𝕊_{T}^{i} , →_{T}), we let ⟦P_{T} ⟧^{p} be the partitioned semantics (Section 3.2.1) defined by:

⟦P_{T} ⟧^{p} = α_{δ_{𝕃_{T}}} (⟦P_{T} ⟧)

where δ_{𝕃_{T}} is defined by:

\begin{aligned}δ_{𝕃_{T}} : & P(𝕊^{⋆}) & → & (𝕃_{T} → P(𝕊^{⋆})) \\ & E & ↦ & λ((l , t) ∈ 𝕃_{T}) · \{σ ∈ E | ∃ρ ∈ 𝕄, σ = ⟨…, ((l , t), ρ)⟩\} \end{aligned}

The properties of covering (resp. partitioning, complete) systems extend to their semantics, as pointed out in the following lemma (the definitions for covering, partitioning and complete extended systems were designed so as to achieve these properties): for instance, a complete partition P_{T} of P_{T′} provides a unique counterpart σ for any trace σ′ of P_{T′}. In the following, we consider the extended systems P_{T} = (T, 𝕊_{T}^{i} , →_{T}) and P_{T′} = (T′, 𝕊_{T′}^{i}, →_{T′}), and τ : T → T′.

Lemma 3.3.1. (semantic adequacy – traces) Then:

— If P_{T} is a τ-covering of P_{T′}, then:

∀l′ ∈ 𝕃_{T′}, ∀σ′ ∈ ⟦P_{T′}⟧^{p}(l′), ∃l ∈ 𝕃_{T} , \{ \begin{matrix}l′ = π_{τ}^{𝕃} (l ) \\ ∃σ ∈ ⟦P_{T} ⟧^{p}(l ), σ′ = π_{τ}^{𝕊^{⋆}} (σ) \end{matrix}

— If P_{T} is a τ-partition of P_{T′}, then:

∀l′ ∈ 𝕃_{T′}, ∀σ′ ∈ ⟦P_{T′}⟧^{p}(l′), ∃!(l , σ) ∈ 𝕃_{T} × 𝕊_{T}^{⋆} , \{ \begin{matrix}l′ = π_{τ}^{𝕃} (l ) \\ σ ∈ ⟦P_{T} ⟧^{p}(l ), \\ σ′ = π_{τ}^{𝕊^{⋆}} (σ) \end{matrix}

— If P_{T} is τ-complete with respect to P_{T′}, then:

∀l ∈ 𝕃_{T} , ∀σ ∈ ⟦P_{T} ⟧^{p}(l ), π_{τ}^{𝕊^{⋆}} (σ) ∈ ⟦P_{T′}⟧^{p}(π_{τ}^{𝕃} (l ))

Proof. The proofs for these properties are similar, so we consider the last one only.

Therefore, we assume that P_{T} is τ-complete with respect to P_{T′}, and that l ∈ 𝕃_{T} , σ ∈ ⟦P_{T} ⟧^{p}(l ), and we attempt to prove that π_{τ}^{𝕊^{⋆}} (σ) ∈ ⟦P_{T′}⟧^{p}(π_{τ}^{𝕃} (l )).

We write σ = ⟨s_{0}, …, s_{n}⟩ and ∀i, s′_{i} = π_{τ}^{𝕊} (s_{i}) (so that σ′ = ⟨s′_{0}, …, s′_{n}⟩ = π_{τ}^{𝕊^{⋆}} (σ)).

— First, we prove by induction on the length of σ that σ′ ∈ ⟦P_{T′}⟧:

— s_{0} ∈ 𝕊_{T}^{i} ; since P_{T} is τ-complete with respect to P_{T′}, s′_{0} = π_{τ}^{𝕊} (s_{0}) ∈ 𝕊_{T′}^{i};

— Let i ∈ ℕ, 0 ≤ i < n. Since σ ∈ ⟦P_{T} ⟧, s_{i} →_{T} s_{i+1}; hence, s′_{i} →_{T′} s′_{i+1}, because P_{T} is τ-complete with respect to P_{T′}.

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

— Second, we prove that π_{τ}^{𝕊^{⋆}} (σ) ∈ ⟦P_{T′}⟧^{p}(π_{τ}^{𝕃} (l )): since σ ∈ ⟦P_{T} ⟧^{p}(l ), σ ∈ ⟦P_{T} ⟧; hence, π_{τ}^{𝕊^{⋆}} (σ) ∈ ⟦P_{T′}⟧ (as proved in the first point). Moreover, σ′ ends at point π_{τ}^{𝕃} (l ), since s′_{n} = π_{τ}^{𝕊} (s_{n}). Hence, π_{τ}^{𝕊^{⋆}} (σ) = σ′ ∈ ⟦P_{T′}⟧^{p}(π_{τ}^{𝕃} (l ))

The cases of partitioning and covering systems are similar.

Let Γ_{τ} be the function defined as:

Γ_{τ} : (𝕃_{T} → P(𝕊_{T}^{⋆})) → (𝕃_{T′} → P(𝕊_{T′}^{⋆}))
Φ  ↦ λ(l′ ∈ 𝕃_{T′}) · ⋃{π_{τ}^{𝕊^{⋆}} (Φ(l )) | l ∈ 𝕃_{T} , τ(l ) = l′}

Here are a few trivial properties of the Γ_{τ} functions:

Lemma 3.3.2. (Properties of Γ_{τ}) For all τ, Γ_{τ} is monotone. If τ_{0} : T_{0} → T_{1}, τ_{1} : T_{1} → T_{2}, then Γ_{τ_{1}∘τ_{0}} = Γ_{τ_{1}} ∘ Γ_{τ_{0}}.

The following theorem comes as a straightforward consequence of Lemma 3.3.1; it is an important step in proving the soundness of the partitioning abstractions.

Theorem 3.3.2. (Semantic adequacy) With the above notations:

— If P_{T} is a τ-partition or a τ-covering of P_{T′}, then ⟦P_{T′}⟧^{p} ⊆ Γ_{τ} (⟦P_{T} ⟧^{p}) (soundness).

— If P_{T} is τ-complete with respect to P_{T′}, then Γ_{τ} (⟦P_{T} ⟧^{p}) ⊆ ⟦P_{T′}⟧^{p} (completeness).

— Hence, if P_{T} is a τ-complete partition of P_{T′}, or a τ-complete covering of P_{T′}, then ⟦P_{T′}⟧^{p} = Γ_{τ} (⟦P_{T} ⟧^{p}) (adequacy).

— If P_{T} is a partitioning system of P_{T′}, then:

∀l , l′ ∈ 𝕃_{T} , l ≠ l′ ⟹ Γ_{τ} (⟦P_{T} ⟧^{p})(l ) ∩ Γ_{τ} (⟦P_{T} ⟧^{p})(l′) = ∅

3.4 Pre-Ordering Properties of Partitions

In the following, we use an ordering among partitions. Therefore, we study the preordering properties of the following relations, among extended transition systems:

— “is a covering of” (for some forget function τ);

— “is a partition of” (for some forget function τ);

— “is complete with respect to” (for some forget function τ).

Then, we can prove that, any such ordering ⋞ is transitive:

Lemma 3.4.1. (Transitivity) Let P_{T} be (T, 𝕊_{T}^{i} , →_{T}), P_{T′} be (T′, 𝕊_{T′}^{i}, →_{T′}), and P_{T′′} be (T′′, 𝕊_{T′′}^{i}, →_{T′′}). Furthermore, we consider the forget functions τ : T → T′, and τ′ : T′ → T′′. Then:

— if P_{T} is a τ-covering (resp. τ-partition) of P_{T′} and P_{T′} is a τ′-covering (resp. τ-partition) of P_{T′′}, then P_{T} is a (τ′ ∘ τ)-covering (resp. (τ′ ∘ τ)-partition) of P_{T′′}.

— if P_{T} is τ-complete with respect to P_{T′} and P_{T′} is τ′-complete with respect to P_{T′′}, then P_{T} is (τ′ ∘ τ)-complete with respect to P_{T′′}.

Proof. We can first remark that π_{τ′∘τ}^{𝕃} = π_{τ′}^{𝕃} ∘ π_{τ}^{𝕃} (and similarly for the other forget functions).

Let us prove the second point (transitivity of completeness).

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

— Let s ∈ 𝕊_{T}^{i} . Then, π_{τ}^{𝕊} (s) ∈ 𝕊_{T′}^{i}, since P_{T} is τ-complete with respect to P_{T′}. Moreover, π_{τ′∘τ}^{𝕊} (s) = π_{τ′}^{𝕊} ∘ π_{τ}^{𝕊} (s) ∈ 𝕃_{T′′}^{i}, since P_{T′} is τ′-complete with respect to P_{T′′}.

— Let s_{0}, s_{1} ∈ 𝕊_{T}, such that s_{0} →_{T} s_{1}. Again, we apply successively the two assumptions of completeness and derive π_{τ}^{𝕊} (s_{0}) →_{T′} π_{τ}^{𝕊} (s_{1}) (since P_{T} is τ-complete with respect to P_{T′} and then π_{τ′∘τ}^{𝕊} (s_{0}) →_{T′′} π_{τ′∘τ}^{𝕊} (s_{1}), since P_{T′} is τ′-complete with respect to P_{T′′}.

The proof of the first point is similar.

Moreover, the relations mentioned above are clearly reflexive

Lemma 3.4.2. (Reflexivity) Let P_{T} = (T, 𝕊_{T}^{i} , →_{T}) and τ : T → T; t ↦ t. Then, clearly P_{T} is a τ-covering (resp. partition) of P_{T} and P_{T} is τ-complete with respect to itself.

Such an ordering should allow to compare the precision of partitions (yet, note that the more precise partition is the greater element, instead of the smaller, as is usually the case in static analysis) and to define valid computational orderings [Cousot and Cousot 1992b], which we will illustrate in the next section.

4. TRACE PARTITIONING DOMAINS

In this section, we address the design of trace partitioning domains. Basically, an element of such a domain defines a partition of the initial system, together with a semantic denotation, relative to this partition. In the concrete level, this denotation associates sets of traces to each control state; in the abstract, level it maps control states into local invariants.

After we define the domains, we also discuss the design of widening operators and static analyses using trace partitioning domains.

4.1 The Trace Partitioning Domain

First, we consider the definition of a concrete trace partitioning domain.

4.1.1 Definition of the Basis. In this section, we assume that a transition system P = (𝕃, 𝕊^{i}, →) is given, and we consider the complete coverings of P; we write 𝔅 for the set of the extended systems which satisfy these properties.

First, we let ⋞ be the order among extended systems defined by:

P_{T_{0}} ⋞ P_{T_{1}} ⟺ ∃τ : T_{1} → T_{0}, P_{T_{1}} is a τ-covering

As remarked in Section 3.4, we may choose other definitions for ⋞, such as:

P_{T_{0}} ⋞ P_{T_{1}} ⟺ ∃τ : T_{1} → T_{0}, \{ \begin{matrix}P_{T_{1}} is a τ-partition of P_{T_{0}} \\ P_{T_{1}} is τ-complete with respect to P_{T_{0}} \end{matrix}

In case the property on the right side is satisfied, we also write P_{T_{0}} ⋞_{τ} P_{T_{1}}, so as to make τ explicit.

The trivial extension of P is clearly the least element of 𝔅 for ⋞.

Note that other choices for 𝔅 and ⋞ could have been made and would have allowed to prove the same results in the following (e.g., with different combinations of orderings).

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

Example 4.1.1. (The ordering over the basis) We showed in Example 3.2.3 that the systems P_{0}, P_{1} and P_{2} are such that:

P_{0} ⋞ P_{1} ⋞ P_{2}

4.1.2 The Domain. At this point we can define the trace partitioning domain. An element of this domain should define:

— a covering P_{T} of the original transition system;

— and a function mapping each extended control state (l , t) of the covering P_{T} into a semantic information relative to that point: in the concrete domain, this information shall consist in the set of all traces ending at point (l , t); in the abstract domain, it consists in an abstract element in D_{𝕄}^{♯} , which approximates the set of stores observed at point (l , t).

More formally:

Definition 4.1.2. (Trace partitioning domain) An element of the trace partitioning domain is a tuple (P_{T} , Φ), where:

— P_{T} denotes a complete covering (T, 𝕊_{T}^{i} , →_{T}) of P, where T ∈ 𝔗 is a set of tokens;

— Φ is a function Φ : 𝕃_{T} → P(𝕊_{T}^{⋆}).

We write 𝔻 for the set of such tuples.

Let (P_{T_{0}}, Φ_{0}), (P_{T_{1}}, Φ_{1}) ∈ 𝔻. Then, we write (P_{T_{0}}, Φ_{0}) ⪕_{τ} (P_{T_{1}}, Φ_{1}) –or, for short (P_{T_{0}}, Φ_{0}) ⪕ (P_{T_{1}}, Φ_{1})– if and only if:

— P_{T_{0}} ⋞_{τ} P_{T_{1}} for τ;

— Φ_{0} ⊆ Γ_{τ} (Φ_{1}).

It follows from the results presented in Section 3.4 that ⪕ defines a pre-ordering on 𝔻.

4.1.3 The Concretization Function. The concretization of an element (P_{T} , Φ) of 𝔻 is a set of traces of the initial system, which is computed by:

(1) merging all the partitions together, by projecting Φ onto the trivial extension P_{ϵ} of P (i.e., applying function Γ_{τ_{ϵ}}) and then collapsing the partitions with γ_{𝕃_{T}} ;

(2) applying the isomorphism π_{ϵ}^{𝕊^{⋆}} between traces of P_{ϵ} and P.

It is defined formally in the following definition:

Definition 4.1.3. (Concretization function) We let γ_{ℙ} be the concretization function based on the following partitioning concretization (Section 3.2.1):

γ_{ℙ} = π_{ϵ}^{𝕊^{⋆}} ∘ γ_{𝕃_{T}} ∘ Γ_{τ_{ϵ}}

Or equivalently, by:

\begin{aligned}γ_{ℙ} : & 𝔻 & → & 𝕊^{⋆} \\ & (P_{T} , Φ) & ↦ & \{π_{ϵ}^{𝕊^{⋆}} (σ) | ∃l ∈ 𝕃_{T} , σ ∈ Φ(l )\} \end{aligned}

Clearly, this function is monotone.

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

20 · X. Rival and L. Mauborgne

PSfrag replacements

Structure Hierarchy

P_{ϵ} P_{T_{0}} P_{T_{1}}

T_{ϵ} → 𝕊_{T_{ϵ}}^{⋆} T_{0} → 𝕊_{T_{0}}^{⋆} T_{1} → 𝕊_{T_{1}}^{⋆}

τ_{1⇀ϵ} Γ_{τ_{1⇀ϵ}} τ_{1⇀0} Γ_{τ_{1⇀0}} τ_{0⇀ϵ} Γ_{τ_{0⇀ϵ}}

least element

of domains

Fig. 3: Structure of the partitioning domain

Example 4.1.4. (Trace partitioning domain) Let us consider the case of the systems introduced in Example 3.2.3. An element of the domain is characterized by the data of a system and the denotation corresponding to this element. For instance, if the element of the basis is P_{1}, then the last element of the tuple should be a function mapping each element of the set {(l_{0}, t_{0}), (l_{1}, t_{1}), (l_{3}, t_{1}), (l_{2}, t_{2}), (l_{3}, t_{2}), (l_{4}, t_{0})} into a set of traces.

The concretization removes all the tokens; hence, it generates sets of traces of the initial system (which is isomorphic to P_{0}).

4.1.4 Soundness of the Partitioned Systems. A last, trivial yet very important remark is that the partitioning of the initial system is sound:

Theorem 4.1.5. (Soundness of control partitioning) Let P_{T_{0}} and P_{T_{1}} ∈ 𝔅, such that P_{T_{0}} ⋞_{τ} P_{T_{1}}. Then, (P_{T_{0}}, ⟦P_{T_{0}}⟧^{p}) ⪕_{τ} (P_{T_{1}}, ⟦P_{T_{1}}⟧^{p}).

In particular, in case T_{0} = T_{ϵ} and P_{T_{0}} = P_{ϵ}, then we get the soundness with respect to the original transition system: ⟦P ⟧ ⊆ γ_{ℙ} (P_{T_{1}}, ⟦P_{T_{1}}⟧^{p}).

Proof. The first point follows from Theorem 3.3.2; the second is a corollary of the first point.

This domain structure can be related to the co-fibered domain structure defined in [Venet 1996]. More precisely, the element of the basis fixes a partition of the original system, and the last argument of the tuple corresponding to an element of the domain 𝔻 provides a semantic denotation defined in a domain relative to the basis element. Figure 3 gives an overall intuition about the structure of the partitioning domain 𝔻.

The presentation in [Venet 1996] relies on categories; we use orderings instead, but the principle is similar: the structure of the basis provides the frame for a hierarchy of domains. The comparison of elements across different domains can be done thanks to the projection functions Γ_{τ} provided by the ordering on the basis.

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

4.1.5 Gain in Precision. Let (P_{T} , Φ) ∈ 𝔻 be an element of the domain. This element describes the same set of traces as the initial program P. However, it allows for a more precise description of sets of traces ending at each control state than the usual abstractions (i.e., the α_{P(𝕊)} abstraction defined in Section 3.1), if there exists a control state l ∈ 𝕃, σ, σ′ ∈ ⟦P ⟧, such that σ and σ′ both end at l but are not in the same partitions, when mapped into the extended system P_{T}. This gain in precision really pays off, when a further abstraction (such as the abstraction defined by γ_{𝕄} ) is composed, as done in the next subsection.

Example 4.1.6. (Precision improvement) Let us consider the program introduced in Section 1.1, and a partitioning similar to the one defined in Figure 2(b).

Then, in the concrete level, at point l_{5}, the partitioned semantics allows to discriminate the traces which visited the true branch and the traces which visited the false branch of the conditional structure, which the standard semantics would not allow. Note that these two semantics describe the same set of traces.

In the abstract level, if we consider the usual interval abstraction, then, at point l_{5}, we get the following results:

— if we consider the partitioned system, then, either the true branch was visited and sgn = 1, or the false branch was visited and then sgn = −1;

— if we consider the non-partitioned system, then the interval for sgn is [−1, 1], which is less precise than the above result (furthermore, it does not allow to check the correctness of the division).

4.1.6 Comparison with Other Approaches to Partitioned Systems. Our approach considerably generalizes the trace partitioning technique of [Handjieva and Tzolovski 1998], since we leave the choice of partitions as a parameter: various partitioning strategies can be implemented (for instance, we allow the merge of partitions).

The path sensitive techniques [Holley and Rosen 1980] proposed in data flow analysis context do not allow for abstractions of sets of paths to be considered. In our settings, a token stands for an approximation for a set of paths, which renders the design of analyses more flexible.

Other authors proposed to perform a partitioning of memory states or to convert part of the data into control structures, as can be done for booleans [Jeannet et al. 1999]. However, this solution presents several drawbacks in our opinion. In particular, the relations partitions are based on may not be found straightforwardly in the memory states; on the other hand, a partitioning guided by the conditions is rather intuitive. The method presented in [Jeannet et al. 1999] is based on a refinement process, which would not be so effective in the case of the Astrée analyzer. It would be possible to adapt this method using the same preprocessing phase used in Astrée, and adding variables recording trace properties during the preprocessing phase, but not all trace properties can be expressed in the imperative language we analyze, and the memory cost of keeping these variables might be prohibitive.

The following subsections express fundamental properties of 𝔻:

— composition of further abstractions (such as the abstraction of sets of stores into collections of predicates), in Section 4.2;

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

— application to static analysis and definition of widening operators on such domains, in Section 4.3;

— implementation of efficient analyzers in Section 4.4.

4.2 Composing Store Abstraction

We now propose to design an abstract trace partitioning domain.

We derive from Definition 4.1.2 the definition of a new partitioning abstraction, by abstracting sets of stores into collections of constraints in the same way as in Section 2.2. Therefore, we assume that an abstraction (D_{𝕄}^{♯} , ⊑) is defined for representing sets of stores, together with a concretization function γ_{𝕄} : D_{𝕄}^{♯} → P(𝕄), which defines the meaning of a set of abstract constraints as the set of stores which satisfy them.

The partitioning abstract domain is derived from 𝔻 by replacing functions mapping extended labels into sets of traces with functions mapping extended labels into elements of D_{𝕄}^{♯} :

Definition 4.2.1. (Partitioning abstract domain) An element of the partitioning abstract domain is a tuple (P_{T} , Φ^{♯}), where:

— T ∈ 𝔗;

— P_{T} is a complete covering (T, 𝕊_{T}^{i} , →_{T}) of P;

— Φ^{♯} is a function Φ^{♯} : 𝕃_{T} → D_{𝕄}^{♯} .

We write 𝔻^{♯} for the set of such tuples.

Remark 4.2.2. (Representation of abstract values) An abstract value is a value in 𝕃_{T} → D_{𝕄}^{♯} = (𝕃 × T) → D_{𝕄}^{♯} . By curryfication; it is isomorphic to a value in 𝕃 → (T → D_{𝕄}^{♯} ). This latter representation turns out to be very natural in practice: each control state corresponds to an abstract value in the partitioning domain D_{𝕄,ℙ(T)}^{♯} = T → D_{𝕄}^{♯} , mapping partitioning tokens into sets of stores; hence, it allows to describe precisely the partitions associated to each program point.

The ordering is also inherited from Definition 4.1.2. We let:

Γ_{τ}^{♯} : (𝕃_{T} → D_{𝕄}^{♯} ) → (𝕃_{T′} → D_{𝕄}^{♯} )
Φ^{♯}  ↦ λ(l′ ∈ 𝕃_{T′}) · ⨆{Φ(l ) | l ∈ 𝕃_{T} , τ(l ) = l′}

If the join operator ⊔ of D_{𝕄}^{♯} is not associative, commutative, the definition of Γ_{τ}^{♯} would not be unique, which would cause various technical complications; therefore, we assume that ⊔ is associative and commutative in our presentation. Then:

Definition 4.2.3. (Ordering) Let (P_{T_{0}}, Φ_{0}^{♯}), (P_{T_{1}}, Φ_{1}^{♯}) ∈ 𝔻, and a function τ : T_{1} → T_{0}. Then, we write (P_{T_{0}}, Φ_{0}^{♯}) ⪕_{τ}^{♯} (P_{T_{1}}, Φ_{1}^{♯}) (or, for short (P_{T_{0}}, Φ_{0}^{♯}) ⪕^{♯} (P_{T_{1}}, Φ_{1}^{♯})) if and only if:

— P_{T_{0}} ⋞_{τ} P_{T_{1}} for τ;

— Φ_{0}^{♯} ⊑ Γ_{τ}^{♯} (Φ_{1}^{♯}).

It follows from the results presented in Section 3.4 that ⪕ defines a pre-ordering on 𝔻.

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

The concretization of an element of 𝔻^{♯} into an element of 𝔻 applies the concretization function γ_{𝕄} pointwise, i.e. by applying it to Φ^{♯}.

Definition 4.2.4. (Concretization)

\begin{aligned}γ_{ℙ}^{♯} : & 𝔻^{♯} & → & 𝔻 \\ & (P_{T} , Φ^{♯}) & ↦ & (P_{T} , λ(l ∈ 𝕃_{T}) · γ_{𝕄} ∘ Φ^{♯}(l )) \end{aligned}

We remark, that (P_{T} , Φ^{♯}) may provide a better approximation of ⟦P ⟧ than an element in D^{♯} = 𝕃 → D_{𝕄}^{♯} whenever the extended systems distinguishes traces of P, i.e., if there exists a control state l , and σ, σ′ ∈ ⟦P ⟧ such that σ and σ′ both end at l and are in different partitions, when mapped into traces of P_{T}.

On the other hand, any approximation for ⟦P ⟧ in D^{♯} can be translated in an equivalent abstraction in (P_{T} , Φ^{♯}), for any choice of P_{T}. As a consequence, we expect the partitioning domain to provide results at least as good as the non partitioning domain, and strictly better results when the extended system P_{T} allows to distinguish real traces of P.

At this point, we can state a remark, which should give a better understanding of the ordering structure of the partitioning domain.

Remark 4.2.5. (⋞ is a computational ordering) The ordering introduced in Definition 4.2.3 is essentially a computational ordering [Cousot and Cousot 1992b]. Indeed, an analysis starts with a coarse partition, defined by the program control structure and then may perform some refinements of the system. When a refinement is performed, the basis element is replaced with a greater element, and so is the current abstract invariant. Therefore, the abstract computation should produce monotone sequences of elements for the ordering of Definition 4.2.3.

But the analysis could use any computational ordering reflecting for example an analysis that starts from the most precise partition and progressively forgets partitions in some unions or widenings. The most precise scheme would certainly be a mix a the two approaches, adding partitions when necessary and maybe finally forgetting some of them. The only requirement for that computational ordering is that we can define a widening on it.

Next subsection proposes the definition of an extrapolation operator based on ⋞ as the computational order.

4.3 Static Analysis with Partitioning and Widening Operator

The domain introduced in Section 4.2 allows to carry out a static analysis of P, with a partitioning domain. However, several approaches to such analyses are feasible:

— static partitioning relies on the choice of a fixed partition;

— dynamic partitioning allows for the partition to be changed during the static analysis.

The latter approach is more powerful but may also result in a more involved implementation. In particular, in case infinitely many partitions might be chosen and different partitions can be used for successive iterations in an abstract fixpoint computation, the termination of the analysis shall be enforced by the use of a widening operator. For instance, it may start analyzing a loop by unrolling the first iterations

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

and decide to give up the unrolling at some point, so as to guarantee termination of the analysis.

The definition of a widening operator on 𝔻^{♯} is necessary when infinite or very large sets of partitions shall be used, and when (quick) termination is required, e.g. for static analysis. This issue would not occur in case the set of partitions was chosen once for all.

We propose to define a widening operator for 𝔻^{♯} by:

— choosing a widening ∇_{𝕄} over D_{𝕄}^{♯} ;

— choosing a widening ∇_{𝔅} over the basis (in the sense of Definition 2.2.2);

— defining a pairwise widening over 𝔻^{♯}.

Formally, the widening operator for the partitioning domain is defined by:

Definition 4.3.1. (Widening for the partitioning domain) If (P_{T_{0}}, Φ_{0}^{♯}), (P_{T_{1}}, Φ_{1}^{♯}) ∈ 𝔻, then, we let:

(P_{T_{0}}, Φ_{0}^{♯})∇_{p}(P_{T_{1}}, Φ_{1}^{♯}) = (P_{T_{2}}, Φ_{2}^{♯})

where:

— P_{T_{2}} = P_{T_{0}}∇_{𝔅}P_{T_{1}}, so that P_{T_{0}} ⋞_{τ_{0}} P_{T_{2}} and P_{T_{1}} ⋞_{τ_{1}} P_{T_{2}};

— Φ_{2}^{♯} = (Φ_{0}^{♯} ∘τ_{0})∇_{𝕄} (Φ_{1}^{♯} ∘τ_{1}) (pointwise application of ∇_{𝕄} to elements of 𝕃_{T_{2}} → D_{𝕄}^{♯} ).

Indeed, this approach leads to a widening over the partitioning abstract domain, as shown in the following theorem:

Theorem 4.3.2. (Widening for partitioning domains) The operator ∇_{p} is a widening operator on 𝔻, in the sense of Definition 2.2.2.

Proof. Proving point 1 in Definition 2.2.2 is straightforward, so we consider point 2.

Let (P_{T_{n}}, Φ_{n}^{♯})_{n∈ℕ} be a sequence elements of 𝔻, and (P_{T′_{n}}, Φ_{n}^{′♯})_{n∈ℕ} be defined as:

\begin{aligned}(P_{T′_{0}}, Φ_{0}^{′♯}) & = & (P_{T_{0}}, Φ_{0}^{♯}) \\ (P_{T′_{n+1}}, Φ_{n+1}^{′♯}) & = & (P_{T′_{n}}, Φ_{n}^{′♯})∇_{p}(P_{T_{n}}, Φ_{n}^{♯}) \end{aligned}

Then:

— by definition of the widening over the basis ∇_{𝔅}, the element of the basis stabilizes after a finite number of iterations: ∃n ∈ ℕ, ∀m ∈ ℕ, m ≥ n ⟹ P_{T_{m}} = P_{T_{n}}.

— if we consider the subsequence (P_{T′_{m}}, Φ_{m}^{′♯})_{m∈ℕ,m≥n} , then ∀m ≥ n, T′_{m} = T′_{n} ∧ P_{T′_{m}} = P_{T′_{n}} and the sequence of the last arguments forms a widening sequence in 𝕃_{T′_{n}} → D_{𝕄}^{♯} ; 𝕃_{T′_{n}} is finite and ∇_{𝕄} is a widening over D_{𝕄}^{♯} , therefore this sequence is ultimately stationary.

This proves that the sequence (P_{T′_{n}}, Φ_{n}^{′♯})_{n∈ℕ} is ultimately stationary; hence, ∇_{p} is a widening operator over 𝔻.

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

Basically, a widening operator for 𝔻 should stabilize the basis first (i.e., enforce the termination of the refinement of the partition), and then stabilize the image in the abstract domain D_{𝕄}^{♯} ; therefore, an alternate definition for ∇_{p} would delay the widening in D_{𝕄}^{♯} until the element of the basis reaches a limit.

4.4 Denotational Style Partitioning Static Analysis

The design of static analyzers as abstractions of the denotational semantics of statements was proposed in Section 2.3. In particular, we showed that this design allows for natural and efficient iteration strategies. Therefore, we propose to adapt this scheme to partitioning analyses.

4.4.1 Partitioning Denotational Semantics. First, we apply the “from point to point” denotational abstraction α_{tF [l_{⊢},l_{⊣}]}.

More precisely, we consider in this subsection an extended system P_{T}, such that P ⪕_{τ} P_{T}, and let l_{⊢}, l_{⊣} ∈ 𝕃. The concrete denotational semantics from l_{⊢} to l_{⊣} maps an “input” state at point l_{⊢} to the set of possible “output” states at point l_{⊣}. Hence, the denotational semantics in the extended system should map tuples made of a partitioning token and a store into similar tuples:

Definition 4.4.1. (Partitioned denotational semantics) We define the abstraction function α_{tF ℙ[l_{⊢},l_{⊣}]} : P(𝕊^{⋆}) → ((𝕋×𝕄) → P(𝕋×𝕄)), where α_{tF ℙ[l_{⊢},l_{⊣}]}(E) is defined by:

α_{tF ℙ[l_{⊢},l_{⊣}]}(E) : (𝕋 × 𝕄) → P(𝕋 × 𝕄)
(t_{⊢}, ρ_{⊢}) ↦ {(t_{⊣}, ρ_{⊣}) | ∃σ ∈ E, σ = ⟨((l_{⊢}, t_{⊢}), ρ_{⊢}), …, ((l_{⊣}, t_{⊣}), ρ_{⊣})⟩}

We write γ_{tF ℙ[l_{⊢},l_{⊣}]} for the corresponding concretization function.

Last, the partitioned denotational semantics is α_{tF ℙ[l_{⊢},l_{⊣}]}(⟦P_{T} ⟧^{p}).

4.4.2 Abstract Partitioning Denotational Semantics. The denotational-style static analyzer of Section 2.3 was derived as an abstraction of the denotational semantics; therefore, we propose to derive a static analyzer for the partitioned system in the same way. However, we should note a slight difference: in Definition 4.4.1, an initial state consists in a pair made of a partitioning token and a store. Hence, the abstract semantics follows the same scheme:

Definition 4.4.2. (Partitioned abstract denotational semantics) We write D_{𝕄,ℙ(T)}^{♯} for T → D_{𝕄}^{♯} . A function ⟦P_{T} ⟧_{ℙ[l_{⊢},l_{⊣}]}^{♯} : D_{𝕄,ℙ(T)}^{♯} → D_{𝕄,ℙ(T)}^{♯} is a sound abstract semantics of P_{T}, between l_{⊢} and l_{⊣} if and only if:

∀(t, ρ), (t′, ρ′) ∈ 𝕋 × 𝕄, ∀d_{p} ∈ D_{𝕄,ℙ(T)}^{♯}

\begin{matrix}(t′, ρ′) ∈ α_{tF ℙ[l_{⊢},l_{⊣}]}(⟦P_{T} ⟧)(t, ρ) \\ ρ ∈ d_{p}(t) \end{matrix}\} ⟹ ρ′ ∈ ⟦P_{T} ⟧_{ℙ[l_{⊢},l_{⊣}]}^{♯} (d_{p})(t′)

In this sense, ⟦P_{T} ⟧_{ℙ[l_{⊢},l_{⊣}]}^{♯} should be an approximation of the denotational semantics introduced in Definition 4.4.1.

The partitioned denotational abstract semantics is sound with respect to the standard semantics of the initial system:

Theorem 4.4.3. (Soundness of the static partitioning analysis) Let P_{T} ∈ 𝔅 such that P_{ϵ} ⋞_{τ} P_{T}.

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

Let d_{t} ∈ D_{𝕄,ℙ(T)}^{♯} , (t, ρ) ∈ 𝕋 × 𝕄 such that ρ ∈ d_{t}(t). Moreover, we let ρ′ ∈ α_{tF [l_{⊢},l_{⊣}]}(⟦P ⟧)(ρ). Then, there exists t′ such that:

ρ′ ∈ ⟦P_{T} ⟧_{ℙ[l_{⊢},l_{⊣}]}^{♯} (d_{p})(t′)

Proof. The above result follows from the soundness of the control partitioning (Theorem 4.1.5) and the soundness of the abstract semantics ⟦P_{T} ⟧_{ℙ[l_{⊢},l_{⊣}]}^{♯} (Definition 4.4.2).

In practice, an abstract semantics ⟦P_{T} ⟧_{ℙ[l_{⊢},l_{⊣}]}^{♯} is defined in a very similar way as the abstract semantics of statements described in Section 2.3, and in Figure 1 and using similar operators.

Moreover, we can remark that the abstract semantics ⟦P_{T} ⟧_{ℙ[l_{⊢},l_{⊣}]}^{♯} may postpone the computation of abstract joins so as to approximate flows in distinct partitions. This ability allows in many cases for a greater precision (even though a local improvement in precision does not always guarantee a global improvement, since several abstract operators including widening usually are not monotone).

Example 4.4.4. (Denotational style abstraction of a if-statement) We consider the program introduced in Example 3.2.3. In particular, this program is equivalent to the transition system P_{0}, displayed in Figure 2(a). We consider the partition defined by the system P_{1} (Figure 2(b)): the analysis partitions the traces depending on the branch of the if-statement they visited before point l_{4} (the partitions are merged at this point).

We present the static analysis of various statements in this piece of code (the analysis is carried out on P_{1}):

— statement s_{1} (true branch of the conditional): the only partitions before and after this statement is t_{1}, to ⟦s_{1}⟧_{ℙ[l_{1},l_{3}]}^{♯} is a function:

⟦s_{1}⟧_{ℙ[l_{1},l_{3}]}^{♯} : ({t_{1}} → D_{𝕄}^{♯} ) ⟶ ({t_{1}} → D_{𝕄}^{♯} )

(the analysis propagates the partition t_{1});

— conditional structure (statement s = if(e) s_{1} else s_{2}): it splits the partition t_{0} into two sets of traces corresponding to t_{1} and t_{2}; hence, ⟦s⟧_{ℙ[l_{1},l_{3}]}^{♯} is a function:

⟦s⟧_{ℙ[l_{1},l_{3}]}^{♯} : ({t_{0}} → D_{𝕄}^{♯} ) ⟶ ({t_{1}, t_{2}} → D_{𝕄}^{♯} )

— statement s_{3} (statement right after the conditional): it inputs two partitions corresponding to t_{1} and t_{2} and outputs similar partitions; however, the partitions are merged right after the analysis of the statement (at point l_{4}), so we can write down ⟦s_{3}⟧_{ℙ[l_{3},l_{4}]}^{♯} as a function:

⟦s_{3}⟧_{ℙ[l_{3},l_{4}]}^{♯} : ({t_{1}, t_{2}} → D_{𝕄}^{♯} ) ⟶ ({t_{0}} → D_{𝕄}^{♯} )

— the whole program inputs and outputs only one partition, corresponding to t_{0}, so its abstract semantics is a function:

⟦P_{1}⟧_{ℙ[l_{1},l_{3}]}^{♯} : ({t_{0}} → D_{𝕄}^{♯} ) ⟶ ({t_{0}} → D_{𝕄}^{♯} )

4.4.3 Making the Partitioning Dynamic. The above definition introduces a static form of partitioning: the analysis of the statement may not change the partitions, e.g. by refining the system. Therefore, we propose a new definition for an abstract semantics for statements, which may refine the partitions.

First, we define a new partitioning abstract domain for approximating sets of stores and partitions:

Definition 4.4.5. (Domain for dynamic partitioning) An element of the domain is a tuple (T, P_{T} , d_{T}), where:

— T ∈ 𝕋;

— P_{T} is a complete covering (T, 𝕊_{T}^{i} , →_{T}) of the initial system P;

— d_{p} ∈ D_{𝕄,ℙ(T)}^{♯} is such that ∀t ∈ 𝕋 \ T, d_{p}(t) = ⊥.

We write D_{δℙ,𝕄}^{♯} for this domain; the ordering is the pointwise extension of the orderings on the basis and on D_{𝕄}^{♯} .

The latter condition ensures that d_{p} assigns invariants to “relevant” tokens only: the invariant corresponding to a token not in T (i.e., not in the current extended system) should be ⊥.

A partitioning abstract semantics can be defined as follows:

Definition 4.4.6. (Dynamic partitioning analysis) The abstract semantics of P_{T} between l_{⊢} and l_{⊣} is a function ⟦P_{T} ⟧_{ℙ[l_{⊢},l_{⊣}]}^{♯} : D_{δℙ,𝕄}^{♯} → D_{δℙ,𝕄}^{♯} such that, if

(P_{T} , d_{T}), (P_{T′}, d_{T′}) ∈ D_{δℙ,𝕄}^{♯} are such that (P_{T′}, d′_{T′}) = ⟦P_{T} ⟧_{ℙ[l_{⊢},l_{⊣}]}^{♯} (P_{T} , d_{T}), then, there exists τ : T′ → T satisfying the following conditions:

— P_{T′} refines P_{T}, i.e. P_{T} ⋞_{τ} P_{T′};

— d′_{T′} approximates the output of P_{T′} at l_{⊣} when the input at l_{⊢} is described by d_{T} in the previous system in a sound manner, which is expressed by the following condition, where d_{T′} = d_{T} ∘ τ:

∀(t, ρ), (t′, ρ′) ∈ 𝕋 × 𝕄,

\begin{matrix}(t′, ρ′) ∈ α_{tF ℙ[l_{⊢},l_{⊣}]}(⟦P_{T′}⟧)(t, ρ) \\ ρ ∈ d_{T′}(t) \end{matrix}\} ⟹ ρ′ ∈ d′_{T′}(t′)

Note that the soundness of the “abstract transfer function” in the second point of Definition 4.4.6 is expressed in the refined system: the input invariant d_{T} is refined into d_{T′} first, and then the abstract transition is performed in T′.

This abstract semantics is sound as well:

Theorem 4.4.7. (Soundness of the dynamic partitioning analysis) Let P_{T} ∈ 𝔅 such that P_{ϵ} ⋞_{τ} P_{T}. Let d_{t} ∈ D_{𝕄,ℙ(T)}^{♯} , (t, ρ) ∈ 𝕋 × 𝕄 such that ρ ∈ d_{t}(t).

We write (P_{T′}, d′_{T′}) for the result of the analysis ⟦P_{T} ⟧_{ℙ[l_{⊢},l_{⊣}]}^{♯} (P_{T} , d_{T}). Moreover, we let ρ′ ∈ α_{tF [l_{⊢},l_{⊣}]}(⟦P ⟧)(ρ). Then, there exists t′ such that

ρ′ ∈ d′_{T′}(t′)

Proof. Similar to the proof of 4.4.3.

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

Again, the core of the soundness of the analysis lies in the definition of the abstract transformer in the refined transition system, which should soundly approximate the partitioning of the transitions of the original system.

Example 4.4.8. (Denotational style abstraction of a if-statement (Example 4.4.4 continued)) Example 4.4.4 demonstrates the analysis of a conditional statement, based on a static partitioning of P_{0} into P_{1}.

In the case of dynamic partitioning, the main difference is that, before the analysis of the conditional, the system under consideration is P_{0} and that the analysis refines P_{0} into P_{1} at point l_{1} (beginning of the conditional). After this refinement, the book-keeping of the partitions is the same as in Example 4.4.4.

5. STATIC ANALYSIS WITH A TRACE PARTITIONING DOMAIN

We now introduce the trace partitioning domain integrated in the Astrée analyzer, together with some examples showing how it contributes to improving precision.

Basically, this domain is an instantiation of the framework for defining trace partitioning domains, which we set up in Section 3 and in Section 4. This domain is tailored to cope with imprecisions observed when analyzing real programs.

5.1 Operations on Partitions

First, we list the operations allowed on partitions, in the Astrée analyzer:

(1) Partitioning of conditional structures, by delaying the merge of flows in the end of conditional structures;

(2) Partitioning of loop structures, by distinguishing the first iterations in the analysis of the loop body and delaying the merge of flows after the end of the loop. This criteria allow for:

— more precise invariants to be derived in the first iterations, thanks to unrolling;

— relations between numbers of iterations and values to be inferred and used after the loop, thanks to the delayed abstract join;

(3) Partitioning guided by the value of a variable x at some point l : this partitioning is similar to a case analysis based on the value of a variable (this partitioning scheme is most useful when dealing with weak updates, and array accesses); note that the partitions are computed at point l and not modified by an assignment to x unlike what would be done in the case of a state partitioning with respect to variable x (in state partitioning such as [Jeannet et al. 1999], any assignment to x would require a new set of partitions be computed);

(4) Inlining of functions (as suggested in Section 3.1);

(5) Merge of partitions: the cost of successive creations of partitions would be prohibitive in practice. For instance, the partitioning of a conditional structure multiplies by 2 the number of partitions in the current flow, so a series of n conditional structures would lead to a 2^{n} blow-up, which is not acceptable (no scalable analysis can afford an exponential cost). Therefore, we avail ourselves the possibility of merging together unnecessary partitions (i.e. partitions which are not expected to lead to further improvements in precision), in any order.

Some of these cases could be handled by transforming the code. This approach is depicted in Figure 4(a), in the case of the partitioning of a conditional structure

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

l_{0} : if(e){
l_{1} : s_{1}

}else{

l_{2} : s_{2}

}

l_{3} : s_{3}
l_{4} : …

⟶

(l_{0}) : if(e){
(l_{1}) : s_{1};
(l_{3}) : s_{3}
}else{
(l_{2}) : s_{2};
(l_{3}) : s_{3}
}
(l_{4}) : …

(a) Partitioning of a conditional

l_{0} : while(e){
l_{1} : s;
l_{2} : }
l_{3} : …

⟶

(l_{0}) if(e){
(l_{1}) s;
(l_{0}) while(e){
(l_{1})  s;
(l_{2}) }
(l_{2}) }
(l_{3}) …

(b) Loop unrolling

Control states in parentheses denote partitioned control states. Fig. 4: Code rewriting

(case 1), as suggested in Example 3.2.3: the statements following the conditional are duplicated in the end of both branches. Case 2 (loops) and case 4 (function inlining) could be handled in a similar manner. For instance, Figure 4(b) displays the rewriting equivalent to the unrolling of the first iteration of a loop.

However, we show in Section 5.3 that the design of a trace partitioning domain was preferable, so that finer partitions can be handled.

5.2 Applications of Trace Partitioning to the Computation of More Precise Invariants

Before we set up the partitioning domain, we provide a few examples, so as to show how the main criteria for partitioning introduced in Section 5.1 are useful, in Astrée.

5.2.1 Linear Interpolation Function, via Indirection Arrays. We consider the case of the interpolation function f_{lin} described in Figure 5 first.

The piece of code for this function determines what formula should be used by localizing in what range x can be found, using a loop and an array of input values. Then, two arrays contain the coefficients which should be used in order to compute the value of f_{lin}(x). Clearly, the output of this function is bounded: ∀x, f_{lin}(x) ∈ [−1, 2].

However, inferring this most precise range is not feasible with a standard interval analysis, even if we partition the traces depending on the values of i at point l_{3}. Let us try with −100 ≤ x ≤ 0: then, we get i ∈ {0, 1} at point l_{3}. The range for y at point l_{4} is [−0.5 + 0.5 × (−100.), −0.5] ≡ [−50.5, −0.5] (this range is obtained in the case i = 1; the case i = 0 yields y = −1). Accumulating such huge imprecisions during the analysis may cause the properties of interest (e.g. the absence of runtime errors or the range of output values) not to be proved. We clearly see that some relations between the value of x and the value of i are required here.

Our approach is to partition the traces according to the number of iterations in the loop. Indeed, if the loop is not iterated, then i = 0 at point l_{3} and x < −1; if it is iterated exactly once, then i = 1 at point l_{3} and −1 ≤ x ≤ 1 and so forth. This approach yields the most precise range. Let us resume the analysis, with the initial constraint −100 ≤ x ≤ 0. The loop is iterated at most once and the partitions at point l_{3} give:

— 0 iteration: i = 0; x < −1; y = −1

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

\underline{PSfrag replacements} x y 0 1 y = \{ \begin{matrix}−1 & if x ≤ −1 \\ −0.5 + 0.5 × x & if − 1 ≤ x ≤ 1 \\ −1 + x & if 1 ≤ x ≤ 3 \\ 2 & if 3 ≤ x \end{matrix}

(a) Function

l_{0} : int i = 0;
l_{1} : while(i < n && x > tx[i + 1])
l_{2} :  i + +;
l_{3} : y = tc[i] × (x − tx[i]) + ty[i]
l_{4} : …

\begin{aligned}tc & = & \{0; 0.5; 1; 0\} \\ tx & = & \{0; −1; 1; 3\} \\ ty & = & \{−1; −0.5; −1; 2\} \end{aligned}

(b) Implementation

Fig. 5: Linear interpolation, via indirection arrays

— 1 iteration: i = 1; −1 ≤ x ≤ 0; −1 ≤ y ≤ −0.5.

Therefore, the resulting range is y ∈ [−1, −0.5], which is the optimal range (i.e. exactly the range of all output values that can be observed in concrete executions).

This optimal result is obtained thanks to a partitioning of the traces by the number of iterations in the loop. The partitions can be merged after the output of the function, since they should not result in any further gain in precision.

5.2.2 Linear Interpolation Function, via Discretization. The second example consists in another kind of interpolation function: the input value is disctretized, and then a formula depending on the discretized value is applied to it. More precisely, if ⌊x⌋ = n, and f is the function to approximate, then the interpolation f_{lin} returns f(n)+(x−n)×(f(n+1)−f(n)). From the mathematical point of view, it is a particular case of the interpolation function considered in the previous paragraph, where the values of the array tx are successive integer values. In the example presented in Figure 6, the array ty is such that ty[n] = f(n). Any interpolation based on a regular partition of a bounded range could be implemented in a similar way, by applying a linear function to the argument so as to recover a partition of the form 0, 1, …, n.

We found that this kind of interpolations were rather common, e.g. for approximating trigonometric functions. For the same reason as in the case of the previous interpolation function, the computation of a precise range for the output of f_{lin} requires some precise relation between n and x.

However, the possible values for n cannot be related to distinct control flow paths; therefore, we propose to perform a partitioning guided by the value of n computed at l_{1}. Doing the same partitioning at point l_{2} would not allow for relations between x and i to be obtained.

5.3 The Domain

We now introduce the trace partitioning domain used in Astrée formally.

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

The Trace Partitioning Abstract Domain · 31

PSfrag replacements

x y 0 1 2 3 4 5

if n ≤ x < n + 1, where n ∈ ℤ
y = f(n) + (x − n) × (f(n + 1) − f(n))

(a) Mathematical definition

l_{0} : int n = 0;
l_{1} : n = cast_{float→int}x;
l_{2} : y = ty[n] + (x − cast_{int→float}n)∗

(ty[n + 1] − ty[n])

l_{3} : …

(b) Implementation

Fig. 6: Linear interpolation function, via discretization

5.3.1 Need for a Trace Partitioning Domain. As we pointed out in Section 5.1, some of the partitioning configurations could have been carried out by rewriting the code. However, we enumerate a number of reasons in favor of the design of a real domain.

First, the “syntactic transformation” approach is limiting. In particular, it would not allow to represent and handle large sets of partitions in the same way as a dedicated domain would:

— using a specific abstract domain allows representing more partitions than mere syntactic rewriting, since not all possible partitions need to be generated during the analysis despite the syntactic approach would require to generate them all prior to the analysis;

— a syntactic rewriting of the code would be inherently static, which is not practically compatible with very large sets of partitions. For instance, a partitioning guided by the values of a variable may generate a huge number of partitions if the variable may take a large number of values (e.g., thousands of values); in this case, a built-in strategy would not perform the partitioning (by not sending the partitioning order to the domain), whereas the decision whether to partition or not would need to be made prior to the analysis in the case of syntactic partitioning. In this case, the implementation of a partitioning domain allows to tune the partitioning strategy during the analysis, so that better decisions can be taken about whether or not some partitions should be generated.

Secondly, as we pointed out above, the partitions sometimes need to be merged together. Currently, where and which partitions are merged is the result of some strategies (Section 6.2). However, the last partition created may not be merged first, which implies that the structure of partitions should be found in abstract elements (as a consequence, the code rewriting approach would fail to offer the same flexibility).

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

Thirdly, in some cases, partitions could be created in a lazy way for other reasons than cost, as in the following cases:

— in the case of a function call, where the function is the result of the dereference of a pointer, the function called can be known precisely at analysis time only;

— some strategies may determine that a loop should be unrolled n times and the analysis may prove that after m < n iterations the execution of the loop terminates; then a syntactic unrolling would not make sense.

Last, the inspection of analysis results is easier, when the invariants can be related to the original program, with accurate partition names (i.e., tokens in the scheme of Section 3). Rewriting large pieces of code as suggested in Figure 4 would make the understanding of the result of static analyses more difficult, since the user would have to relate the invariants computed for the transformed program to the original program. Further, it would make the merging of partitions awkward, or even impossible if we try to merge partitions in another order than the reverse order of creation. By contrast, the values of the partitioning domain should tell what partitions numerical constraints correspond to, thanks to the partitioning tokens.

5.3.2 Elements. We now define formally the instantiation of the framework presented in Section 4 implementing to the techniques listed in Section 5.1.

Intuitively, the creation of a partition corresponds to a partitioning directive. We provide the formal definition of directives in Figure 7(a). The name of each directive corresponds very intuitively to an operation listed in Section 5.1, except for the last one: the purpose of the directive 𝔭𝔞𝔯𝔱⟨None⟩ is to allow for some abstract operations to be defined properly. At this point, it appears only during final stages of static analyses (in particular, during the invariant export phase, mentioned in Section 2.3). Therefore, we postpone the definition of the meaning of this directive to Section 6.1.

The name of a partition (i.e., token corresponding to it, in the sense of Section 3.2) consists in the series of the partitioning directives encountered before creating this partition. We give the formal definition for tokens in Figure 7(b). We note that each partitioning directive encloses a control state, which stands for the point the partition was created at. The directive 𝔭𝔞𝔯𝔱⟨None⟩ stands for a void directive, and as such, it does not provide any information about the history of the traces corresponding to the partitions 𝔭𝔞𝔯𝔱⟨None⟩ appears in the name of, as opposed to the other tokens.

For instance, in the case of a conditional at point l , two partitions are created right after the testing of the condition, corresponding to the directives “true branch of the conditional at point l ” and “false branch of the conditional at point l ”. When these partitions are merged, these directives are removed from the names of the partitions.

As usual, we write D_{𝕄}^{♯} for the domain for representing sets of stores (Section 2.2). In the same way as in Section 4.4, the domain D_{𝕄,ℙ(𝕋)}^{♯} is defined as 𝕋 → D_{𝕄}^{♯} .

5.3.3 Hints (or Directives) in the Code. A pre-processing phase inserts directives as special commands in the source code. We do not introduce them formally here (the directives are represented as text between braces in programs). Intuitively,

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

d ::= 𝔭𝔞𝔯𝔱⟨If, l , b⟩  traces in the b branch of the conditional at point l
| 𝔭𝔞𝔯𝔱⟨While, l , n⟩ traces with exactly n iterations in the loop at point l
| 𝔭𝔞𝔯𝔱⟨While, l , > n⟩ traces with more than n iterations in the loop at point l
| 𝔭𝔞𝔯𝔱⟨Val, l , x = n⟩ traces such that x = n at point l
| 𝔭𝔞𝔯𝔱⟨Fun, l , f⟩  traces calling f at point l
| 𝔭𝔞𝔯𝔱⟨None⟩  void directive

(a) Directives (notation for directives: d ∈ D)

t ::= ϵ  empty stack, initial partition
| d :: t′ addition of a directive on top of t′

(b) Tokens (t ∈ 𝕋)

Fig. 7: Naming partitions

directives in the code cause directives to be added in tokens (partition creation) or be deleted from tokens (partition merge).

5.3.4 Widening. The set of tokens is clearly infinite, since the length of tokens as sequences of directives is not bounded. Even in case we limit the length of tokens, the number of tokens is very large: indeed, if we fix l ∈ 𝕃 and x ∈ 𝕏, the number of directives of the form 𝔭𝔞𝔯𝔱⟨Val, l , x = n⟩ is equal to the number of integer values in the language (i.e., in practice 2^{32}). Therefore, the termination of the analysis should rely on a widening operator, designed as in Section 4.3.

In practice,

— the widening operator on the basis forbids the synthesis of arbitrary long tokens, by preventing the generation of tokens containing two directives corresponding to the same control point l : basically, this operator interrupts the generation of partitions;

— the generation of partitions after a directive recommending the partitioning guided by the values of a variable x is performed only if the size of the set of possible values for x determined by the analysis is small enough (e.g., below 1000);

— the current partitioning strategy is designed so as not to keep partitions beyond the scope they should improve the precision in; this strategy allows to merge partitions soon enough, so that the widening operator does not need to collapse partitions down (widening is applied at loop heads only [Bourdoncle 1993]).

5.4 Structure of the Abstract Interpreter

As stated in Section 2.3, the iterator consists in a function mapping statements into abstractions of their denotational semantics, as defined in Section 2.3. As a consequence, the design of the abstract interpreter follows the principle described in Section 4.4: the abstract interpretation ⟦s⟧^{♯} of a statement s should map a pair (P_{T} , d_{T}) ∈ 𝔅 × D_{𝕄,ℙ(𝕋)}^{♯} , where ∀t ∉ T, d_{T} (t) = ⊥ into a pair (P_{T′}, d′_{T′}) ∈

𝔅 × D_{𝕄,ℙ(𝕋)}^{♯} , where P_{T′} is a refinement of P_{T} and d′_{T′} is an over-approximation of the output of s when applied to the input d_{T} (Definition 4.4.6).

The iterator of Astrée does not keep track of the whole refined program P_{T}. Instead, it keeps track of the current partitions, i.e. of the tokens corresponding to a set of partitions covering the ongoing flows:

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

Definition 5.4.1. (Ongoing token set) The ongoing token set corresponding to the abstract flow d_{T} ∈ D_{𝕄,ℙ(𝕋)}^{♯} is tokens_{T} ⟨d_{T} ⟩ = {t ∈ 𝕋 | d_{T} ≠ ⊥}.

This notion was implicitly illustrated in Example 4.4.4 (we described the partitioning abstract interpretation of an if-statement).

If (P_{T} , d_{T}) is the result of the static analysis of a statement, then, the property tokens_{T} ⟨d_{T} ⟩ ⊆ T is straightforward.

The abstract interpretation ⟦s⟧^{♯} of a statement s simply maps an element d_{T} ∈ D_{𝕄,ℙ(𝕋)}^{♯} into a second element d′_{T′} ∈ D_{𝕄,ℙ(𝕋)}^{♯} : all the information about the partitioning carried out by the analysis are enclosed in the d_{T} element.

This is a common advantage of denotational style abstract interpreters: this iteration scheme keeps only the information which are useful for the end of the analysis and discards the values which were useful only in the past and will not be required anymore. For instance, we remarked that the analyzer presented in Section 2.3 does not need to store invariants at every control point. The restriction to the set of tokens corresponding to the ongoing flows is similar.

This approach is feasible, since the partitioning tokens contain all the information about the transitions associated to them.

Last, we note that the pre-processing phase inserts hints in the code and selects this way a family of extended systems which may be used during the analysis. As a consequence, most of the partitioning decisions are made statically; the only decisions taken at analysis time are whether or not to obey to some directives. In this sense, the partitioning implemented in Astrée is dynamic, but mostly determined statically; reducing the number of choices made at analysis time simplifies the implementation.

5.5 Transfer Functions

We consider three kinds of transfer functions:

— the “partition creation” transfer function generate new partitions;

— the “partition merge” folds partitions together;

— the “standard” transfer functions (i.e., which are not specific to partitioning analyses, such as assign, guard...) stand for e.g., abstract assignments, condition testing...

5.5.1 “Standard” transfer function, e.g. assignment. We extend pointwisely the usual transfer functions presented in Section 2.2 to D_{𝕄,ℙ(𝕋)}^{♯} .

5.5.2 Partition creation. We let generate: D × D_{𝕄,ℙ(𝕋)}^{♯} → D_{𝕄,ℙ(𝕋)}^{♯} be the partition creation abstract transfer function. It inputs a directive ∂ and an abstract element d ∈ D_{𝕄,ℙ(𝕋)}^{♯} and adds the directive ∂ to all ongoing tokens in d. Formally, it outputs an element d′, defined by:

\{ \begin{matrix}tokens_{T} ⟨d′⟩ = \{(∂ :: t) | t ∈ tokens_{T} ⟨d⟩\} \\ ∀t ∈ tokens_{T} ⟨d⟩, d′(∂ :: t) = d(t) \end{matrix}

5.5.3 Partition merge. We let merge: P(D)×D_{𝕄,ℙ(𝕋)}^{♯} → D_{𝕄,ℙ(𝕋)}^{♯} be the transfer function for merging partitions. It folds partitions by removing any directive in

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

D for the partition names (tokens). Therefore mergeinputs a set of directives D and an abstract element d and returns a new abstract element d′, where any reference to the directives in D are removed. Formally, if the first argument of merge , D is the singleton {∂}, then the result d′ is defined by:

(∂_{i_{0}} :: …:: ∂_{i_{m}}) ∈ tokens_{T} ⟨d′⟩ ⟺ \{ \begin{matrix}(∂_{0} :: …:: ∂_{n}) ∈ tokens_{T} ⟨d⟩ \\ \{i_{k} | k ∈ ⦇0, m⦈\} = \{i ∈ ⦇0, n⦈ | ∂_{i} ≠ ∂\} \\ i_{0} < … < i_{m} \end{matrix}

With the above notations, d′(∂_{i_{0}} :: …:: ∂_{i_{m}}) = d(∂_{0} :: …:: ∂_{n})

The above definition extends straightforwardly to the general case (D not necessarily a singleton).

Example 5.5.1. (Transfer functions in a partitioning analysis) Figure 8 displays a simple piece of code, containing an if-statement (Figure 8(a)). The pre-processing phase of Astrée inserts some directives in the code, which specify hints about what partitions should be created. We assume that the strategies recommend to partition the traces in the beginning of the if-statement and to merge the partitions at point l_{5}, as shown in Figure 8(b)).

l_{0} : s_{0};
l_{1} : if(c){
l_{2} :  s_{1}

}else{

l_{3} :  s_{2}

}

l_{4} : s_{3};
l_{5} : s_{4};

(a) Initial program

l_{0} : s_{0};

⟅Partition the traces

in the following if statement⟆

l_{1} : if(c){
l_{2} :  s_{1}

}else{

l_{3} :  s_{2}

}

l_{4} : s_{3};

⟅Merge the partitions of

the if statement at this point⟆

l_{5} : s_{4};

(b) Program with directives added

Fig. 8: Partitioning analysis of a if-statement: directives

Here are the main steps of the analysis:

— at point l_{0}, only one partition exist; it corresponds to the void token ϵ;

— when entering the if-statement, the analyzer creates two partitions corresponding to the directives 𝔭𝔞𝔯𝔱⟨If, l_{0}, true⟩ (true branch) and 𝔭𝔞𝔯𝔱⟨If, l_{0}, false⟩ (false branch): at this step it applies the transfer function which associates the abstract element generate (𝔭𝔞𝔯𝔱⟨If, l_{0}, true⟩, d) to d and d ↦ generate (𝔭𝔞𝔯𝔱⟨If, l_{0}, false⟩, d);

— the analysis of the body of both branches involve usual transfer functions;

— at point l_{4} the join of the invariants corresponding to both branches should be computed, so that we get an invariant d_{4}, such that tokens_{T} ⟨d_{4}⟩ ={𝔭𝔞𝔯𝔱⟨If, l_{0}, true⟩ :: ϵ, 𝔭𝔞𝔯𝔱⟨If, l_{0}, false⟩ :: ϵ};

— at point l_{5} the analyzer merges the partitions together, by applying the transfer functions d ↦ merge ({𝔭𝔞𝔯𝔱⟨If, l_{0}, true⟩, 𝔭𝔞𝔯𝔱⟨If, l_{0}, false⟩}, d).

6. TRACE PARTITIONING IN THE ASTRÉE ANALYZER

In this section, we deal with practical issues related to the implementation of the trace partitioning domain presented in Section 5 in Astrée. We describe the data structures and the partitioning strategies. Last, we provide extensive implementation results.

6.1 Implementation of the Domain

6.1.1 The Data-Structure. In practice, tokens_{T} ⟨d_{T} ⟩ can be considered the set of paths into the leaves of a tree, where each branch in the tree is labeled with a directive. Therefore, trees are a natural representation for the elements of D_{𝕄,ℙ(𝕋)}^{♯} ,

with elements of D_{𝕄}^{♯} at the leaves and with directives as labels for the branches:

Definition 6.1.1. (Representation of the elements of D_{𝕄,ℙ(𝕋)}^{♯} ) The phys-

ical representation of the elements of D_{𝕄,ℙ(𝕋)}^{♯} is defined by induction by:

d_{T} ::= leaf[d] where d ∈ D_{𝕄}^{♯}  (leaf D_{𝕄}^{♯} element)
| node[ϕ] where ϕ ∈ D → D_{𝕄,ℙ(𝕋)}^{♯} (function mapping directives into D_{𝕄,ℙ(𝕋)}^{♯} )

The use of this representation is exemplified in Example 6.1.3, after we define the transfer functions.

6.1.2 The Transfer Functions. The implementation of the transfer functions proceeds by induction on the structure of the trees. Indeed, let us consider the three kinds of transfer functions, which we introduced in Section 5.5 (in the following, we augment the names of the transfer functions for the partitioning domain with the index _{ℙ} ):

— Abstract binary operators, e.g. join are defined by induction on the structure of trees. If the join of the set of paths in both trees contains two tokens t_{0}, t_{1} such that t_{0} is a strict prefix of t_{1}, then t_{0} is replaced with 𝔭𝔞𝔯𝔱⟨None⟩ :: t_{0} so that the result can be represented (for more details, see Remark 6.1.2).

— “Usual” transfer functions: we consider the case of the guard_{ℙ} : 𝕖 × 𝔹 × D_{𝕄,ℙ(𝕋)}^{♯} → D_{𝕄,ℙ(𝕋)}^{♯} transfer function, which inputs a condition e ∈ 𝕖, a boolean b ∈ 𝔹, and an abstract element d and outputs an over-approximation of the stores in d which evaluate e into b (the case of assignments is similar). The definition of guard_{ℙ} is based on the function guarddefined over D_{𝕄}^{♯} :

∀e ∈ 𝕖, ∀b ∈ 𝔹, \{ \begin{matrix}guard_{ℙ} (e, b, leaf[d]) & = & leaf[guard(e, b, d)] \\ guard_{ℙ} (e, b, node[ϕ]) & = & node[∂_{p} ↦ guard(e, b, ϕ(∂_{p}))] \end{matrix}

— Partition creation: the partition creation abstract transfer function generate: D × D_{𝕄,ℙ(𝕋)}^{♯} → D_{𝕄,ℙ(𝕋)}^{♯} inputs a partitioning directive ∂ and an abstract element d and pushes the token ∂ on top of the tokens. Basically, it mimics the creation of a partition triggered by the directive ∂, which amounts to adding a node on top of each leaf in d, with a branch indexed by ∂ in between:

∀∂ ∈ D, \{ \begin{matrix}generate (∂, leaf[d]) & = & node[∂ ↦ leaf[d]] \\ generate (∂, node[ϕ]) & = & node[∂_{p} ↦ generate (∂, ϕ(∂_{p}))] \end{matrix}

In practice, the partition generation function takes into account the names of the partitions, so as to create only some partitions.

— Partition merge: the transfer function merge: P(D) × D_{𝕄,ℙ(𝕋)}^{♯} → D_{𝕄,ℙ(𝕋)}^{♯}

inputs D ⊆ D, d ∈ D_{𝕄,ℙ(𝕋)}^{♯} ; it goes recursively through the tree representing d and removes all occurrences of a directive in D. The implementation follows the following algorithm:

∀D ∈ P(D), \{ merge (D, leaf[d]) = leaf[d] merge (D, node[ϕ]) = node[ϕ′] where ϕ′ : \{ \begin{matrix}∂ ∉ D & ↦ & merge (D, ϕ(∂)) \\ 𝔭𝔞𝔯𝔱⟨None⟩ & ↦ & ⨆\{d at a leaf of ϕ(∂) | ∂ ∈ D\} \end{matrix}

The directive 𝔭𝔞𝔯𝔱⟨None⟩ allows to fold together some branches leaving from a node. In case all branches can be folded, then these directives can be safely removed from trees:

node[{𝔭𝔞𝔯𝔱⟨None⟩ ↦ d_{0}}] → d_{0}

Remark 6.1.2. (Use of the 𝔭𝔞𝔯𝔱⟨None⟩ directive) We proposed to represent abstract elements with trees, so that the prefix sequences of tokens common to different partition names could be shared (which allows for faster algorithms in transfer functions). However, in some cases, such as the case of abstract binary operators, such a representation could not be found without the 𝔭𝔞𝔯𝔱⟨None⟩ directive.

For instance, after a join of two abstract elements, we may need to represent an invariant d_{T}, such that t ∈ tokens_{T} ⟨d_{T} ⟩ and (∂ :: t) ∈ tokens_{T} ⟨d_{T} ⟩, for some token t and some directive ∂. The problem is that our definition for the elements of the abstract domain allows numerical invariants at the leaves of trees only.

The 𝔭𝔞𝔯𝔱⟨None⟩ directive solves this problem: indeed, 𝔭𝔞𝔯𝔱⟨None⟩ :: t stands for t, and a numerical invariant can be assigned to the leaf corresponding to 𝔭𝔞𝔯𝔱⟨None⟩ :: t. Therefore, we can build a tree, where the node corresponding to t has two leaves, which are respectively labeled with ∂ and 𝔭𝔞𝔯𝔱⟨None⟩.

Such configurations do not occur in the analysis; they may arise in the invariant export (Section 2.3), when all local invariants corresponding to a control state l_{0} (possibly in different contexts, e.g., for different function calls) should be represented together. In particular the abstract join operator may generate 𝔭𝔞𝔯𝔱⟨None⟩ directives.

Example 6.1.3. (Application to the partitioning of an if-statement) We consider the program considered in Example 5.5.1, with the partitioning strategy displayed in Figure 8(b). We assume that the analysis starts with a single partition (i.e., only one ongoing token at point l_{0}).

Figure 9 displays the partitions obtained when the analysis reaches each control state in this program:

— statement s_{0} does not generate any new partition, so the layout of the abstract element for l_{1} (Figure 9(a)) is the same as for l_{0} (Figure 9(b));

— the conditional causes a partitioning of the traces at l_{1}, so two trees are created after this point (yet, the partition corresponding to false is not created explicitly

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

in the true branch, since it would be empty), which are depicted in Figure 9(c) and Figure 9(d);

— the abstract join outputs a new abstract element, with two partitions corresponding to both sides of the conditional at point l_{4} (Figure 9(e));

— the merge of partitions is performed after the analysis of s_{3}, so that the tree in l_{5} consists in only a leaf (Figure 9(f)) at in l_{0}.

As a shortcut, we write ∂_{t} for 𝔭𝔞𝔯𝔱⟨If, false, l_{1}⟩ and ∂_{f} for 𝔭𝔞𝔯𝔱⟨If, true, l_{1}⟩, and d for any invariant in D_{𝕄}^{♯} . Dotted lines denote the partitions which are not generated, since the analysis proves them empty.

PSfrag replacements

d
(a) l_{0}

PSfrag replacements

d
(b) l_{1}

PSfrag replacements

d ∂_{t} ∂_{f}

(c) l_{2}

PSfrag replacements

d ∂_{t} ∂_{f}

(d) l_{3}

PSfrag replacements

d
∂_{t}
∂_{f}
(e) l_{4}

PSfrag replacements

d
(f) l_{5}

Fig. 9: Application to the partitioning of an if-statement

6.2 Strategies for Trace Partitioning

6.2.1 Implementation of a Partitioning Strategy. As mentioned in Section 2.3, a pre-processing phase generates hints for the abstract domains, including the partitioning domain. Such hints specify the cases where partitions might be helpful in order to compute tighter invariants. In the analysis phase, partitioning may or may not be performed at these points, depending on the choice of the interpreter. Indeed, in case the pre-processing phase recommends a partitioning guided by the values of a variable v and the analyzer infers too large a range for v (i.e., the number of generated partitions would be prohibitive), the analyzer will not perform the partitioning. Similarly, it will not create empty partitions: for instance, in the case of a conditional statements which should be partitioned, if the analysis proves the condition always evaluates to true, then, the partition corresponding to the false branch will not be generated.

6.2.2 Strategies for Generating “Good” Partitions. We enumerate a few cases where the current pre-processing phase suggests partitions to be generated:

6.2.2.1 Sequences of Conditional Statements. Partitioning the traces in the first if-statement may greatly improve the precision in the following conditional statements, if the condition of the second if-statement depends on the content of the branches of the first one, or if its value depends on the value of the condition of

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

the first if-statement (a simple dependence analysis is performed during the preprocessing phase).

6.2.2.2 Non Standard Relational Invariants. We identified common expressions where a relational information would be useful, but where we don’t know the shape of the relations. So far, two kinds of expressions are identified:

— Array access: expressions containing two array accesses such that the accesses have a variable i in common. Then, there is a relation between the two array accesses and the easy way to express it is to use a discrimination of i. Such relations occur in interpolation functions (Section 5.2).

— Divisions: expressions containing a division such that the dividend and the divisor share a variable i. If we just know the range of i, then the imprecision might be large. One may fail to recognize that i/(i + 1) is smaller than one for example. If we discriminate on i, then each division is very precise. This is encountered in the calculus of barycenters.

6.2.2.3 How to Discriminate a Variable i. Once we identify an expression which would be more precise by discriminating a variable i, we look for the place where the variable was last assigned. We add some partitioning directive depending on that place and then a merging directive after the expression. The partitioning directive can be of two kinds:

— assignment to an integer variable the partitioning guided by the value of i generates some relations with the variables in the right hand side of the assignment and may improve the precision of the subsequent array operation, since distinct array cells are treated separately, in a refined environment. This criterion causes the right partitions to be generated in the case of the interpolation function with regular discretization of the input, which we presented in Section 5.2, and Figure 6.

— small loops assigning an integer variable the unrolling of the loop allows for the same kind of relations to be computed as in the previous point; hence, it results in the same opportunities for gains in precision. Note that the size of the loop is not inferred during the pre-processing phase, but during the analysis which can partition the whole loop or just part of it, depending on its size and a parameter of the analysis. This criterion triggers the generation of the right partitions in the case of the interpolation function with indirection arrays, which we described in Section 5.2 and Figure 5.

6.3 Experimental Evaluation

6.3.1 Methodology for the Benchmarks. The results below were obtained on a 2 GHz Bi-opteron desktop, with 8 Gb of RAM (total) and 1 Mb of cache memory (per processor), running Linux. All the analyses reported in the sequel used only one processor, despite Astrée also features the ability of being ran in “parallel” mode [?].

The analyzer was ran on a series of programs, chosen among two families of safety critical embedded codes, the size of which we detail in table I. These programs are C code generated automatically from a high-level specification in a synchronous language. For a deeper overview of the structure and features of these programs, we refer the reader to [Blanchet et al. 2003]. Programs in family 1 (denoted with

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

Table I. Benchmarks

Program  Size Functions  Variables
(LOCs)  Global and static  Local
int  float  int  float
P_{1}^{1}  370  20  23  87  2  0
P_{2}^{1}  9 500  236  35 100  835  4  8
P_{3}^{1}  70 000  2 010  11 700 27 400  22  516
P_{1}^{2}  70 000  1 150  71 400  8 670  11 700 5 700
P_{2}^{2}  226 000  3 410  35 700 24 900 44 300 21 900
P_{3}^{2}  400 000  5 680  58 700 35 500 83 400 35 100

Table II. Partitioning Strategy

Program Size Conditional Loops Value-based
(LOCs) partitioned total partitioned total partitioning
P_{1}^{1}  370  4  28  1  1  0
P_{2}^{1}  9 500  18  283  1  3  0
P_{3}^{1}  70 000  498  4 617  3  5  112
P_{1}^{2}  70 000  300  2 624  106  106  0
P_{2}^{2}  226 000  1 805  9 381  591  591  19
P_{3}^{2}  400 000  2 802  17 562  906  916  32

P_{i}^{1}) are part of an earlier generation, and of smaller size than programs in family 2 (denoted with P_{i}^{2}).

6.3.2 Partitioning Strategy. Table II displays the results of the partitioning strategy. We give the total number of conditional structures, and the number of partitioned conditional structures. We provide similar information about the partitioning of loop structures; however, only the internal loops are taken into account here (we recall that a program in either families consists in a main loop, which contains almost all the code and which is executed every t milliseconds). Last, we mention the number of directives recommending a partitioning guided by the values of a variable. Overall, partitioning directives are inserted in the case of 10 % to 20 % of the conditional structures and for almost all internal loops. The partitioning guided by the values of variables tend to have less importance (much fewer directives inserted, and only in the larger applications).

6.3.3 Analysis with Partitioning Enabled. In the following T.p.I. stands for “Time per iteration”; it corresponds to the average time spent in one iteration of the main loop of the program being analyzed. This time is roughly representative of the efficiency of the transfer functions and of the precision of the abstract control flow. The number of iterations assesses the efficiency of the convergence. The global time of the analysis depends both on the efficiency of transfer functions and the speed of the convergence.

Times are written in seconds (s); amounts of memory in megabytes (Mb).

Table III displays the result of the analysis with the default settings: trace partitioning is enabled and the directives are inserted by the automatic strategy evoked in Section 6.2.

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

Table III. Results of the Analysis with Trace Partitioning

Size Memory peak Analysis time  Iterations  Alarms
(LOCs)  (Mb)  (s)  ♯ T.p.I. (s)
P_{1}^{1}  370  45  1.96  9  0.21  0
P_{2}^{1}  9 500  175  104  17  6.1  8
P_{3}^{1}  70 000  636  2 818  35  80.5  0
P_{1}^{2}  70 000  434  1 064  20  53.2  0
P_{2}^{2} 226 000  1 533  17 035  51  334  0
P_{3}^{2} 400 000  2 423  36 480  72  507  0

Table IV. Analysis without Partitioning

Size  Memory peak  Analysis time  Iterations  Alarms
(LOCs)  (Mb)  (s)  ♯ T.p.I.
P_{1}^{1}  370  45 (-)  1.55 (-21 %)  9 0.17s  0 (0)
P_{2}^{1}  9 500  170 (- 3 %)  87 (- 17 %)  17 5.1s  8 (8)
P_{3}^{1} 70 000  660 (+ 3 %)  1 614 (- 43 %)  35 46.1s  750 (0)
P_{1}^{2} 70 000  376 (-13 %)  921 (- 13 %)  20  46s  443 (0)
P_{2}^{2} 226 000 1 341 (- 12 %) 37 274 (+ 112 %) 282 134s 5 402 (0)
P_{3}^{2} 400 000 2 040 (- 16 %)  34 147 ( - 6 %)  127 269s 7 524 (0)

6.3.4 Global Impact of Partitioning. First, we compare the results of the analyses with or without trace partitioning enabled: table IV displays the results without trace partitioning. Note that the partitioning inherent in the function calls (function inlining) is not affected by the disabling of trace partitioning: turning off partitioning removes the partitioning relative to loop iterations, conditional and values of variables only.

The numbers in parentheses allow to compare with the default, partitioning analyses. This first comparison shows the great impact of partitioning in most cases, and especially in the case of the large applications, i.e., the programs which compare most closely with real applications due to their size and structure. The first two programs are experimental programs, which do not comprise all the features of the largest applications and involve smaller chains of computations, so the trace partitioning does not impact the number of alarms. Yet, the invariants are noticeably less precise, even in the case of the first example. The analyses of larger, real-world applications generate a dramatic number of alarms: trace partitioning proves a crucial technique in Astrée.

Secondly, we remark that the execution time is not necessarily better when trace partitioning is disabled. In particular, the analysis of the two largest programs require a much larger number of iterations when trace partitioning is turned off: this effect was most noticeable in the case of the second program in the second family (282 iterations instead of 52!). In fact, a lower precision may result in a longer analysis time for many reasons related to the exploration of a larger state space:

— the widening of the analyzer attempts to stabilize variables, with a widening threshold scale [Blanchet et al. 2003]; therefore, if some variable cannot be stabilized to a small range (for instance, because some property cannot be proved due to the

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

Table V. Impact of the Partitioning of Conditional Structures

Size Memory peak  Analysis time  Iterations  Alarms
(LOCs)  (Mb)  (s)  ♯ T.p.I.
P_{1}^{1}  370  45 (-)  1.96 (-)  9 0.17s  0 (0)
P_{2}^{1}  9 500  173 (- 1 %)  88 (- 15 %)  17  5.2s  8 (8)
P_{3}^{1}  70 000  616 (- 3 %)  5 004 (+ 76 %)  32 156s  398 (0)
P_{1}^{2}  70 000  467 (+ 8 %)  1 466 (+ 38 %)  20 73.2s  389 (0)
P_{2}^{2} 226 000 1 680 (+ 10 %) 199 500 (+ 1 071 %) 290 688s 5 190 (0)
P_{3}^{2} 400 000 2 735 (+ 12 %) 187 773 (+ 415 %) 125 1 502s 5 542 (0)

trace partitioning being turned off), it goes through a longer sequence of widened ranges (the analyzer attempts to find a larger, stable range), before it eventually reaches the “top” value (i.e., range containing all concrete values). This is an explanation for larger numbers of iterations in the case of less precise analyses.

— the control flow of the static analysis need to be more exhaustive when the precision is worse: for instance, in the case of a conditional, a less precise input invariant may require the analysis of both branches of the conditional whereas a more precise invariant may require analyzing only one branch, hence, require less time to complete.

Overall, we remark that the time per iteration is lower in the case of non-partitioning analyses and the partitioning analyses tend to require a lower number of iterations However, it is difficult to say for sure what is the most important factor: we may guess that only the first factor plays a significant role here (longer analyses due to longer widening chains), however, we should remark that the non-partitioning transfer functions handle much simpler data-structures; the latter factor may explain the shorter iterations.

Moreover, it is rather intuitive that one iteration of a partitioning analysis should take longer than one iteration of a non-partitioning analysis; however, the cost in time of trace partitioning (whether global analysis time or time per iteration) never turns out prohibitive.

Last, we remark that partitioning analyses require more memory in most cases; this result is to be expected, since partitioning analyses generate more data-structures and handle more numerical invariants. Yet, this cost is rather reasonable, since it never goes above 20 % (10 % average). This is mostly due to the fact that most partitioning criteria are local: they do not yield to huge sets of global partitions, thanks to the insertion of merge directives (Section 5.1).

In the following, we focus on several kinds of partitioning criteria and measure their impact on the results of the analysis.

6.3.5 Impact of the Partitioning of Conditional Structures. Second, we compare the default, partitioning analysis with analyses carried out without some partitions. Table V reports the result of the analysis without partitioning of conditional structures. The results in precision fall between the results of the partitioning analysis and the results of the non-partitioning analysis. In the case of the largest applications, the number of alarms is still dramatic.

In the resource usage point of view, these results are much worse than those of the non-partitioning analysis and of the partitioning analysis. Not only the number

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

Table VI. Impact of Inner Loops Partitioning

Size Memory peak  Analysis time  Iterations  Alarms
(LOCs)  (Mb)  (s)  ♯ T.p.I.
P_{1}^{1}  370  45  1.96 (-)  9 0.21s  0 (0)
P_{2}^{1}  9 500  173 (-1 %)  85 (-18 %)  17  5s  8 (8)
P_{3}^{1}  70 000  596 (- 6 %)  3 928 (+ 39 %)  63 62.3s  529 (0)
P_{1}^{2}  70 000 391 (- 10 %) 12 319 (+1 058 %) 292 42.2s  208 (0)
P_{2}^{2} 226 000 1 400 (- 9 %)  14 277 (- 16 %)  75 190s 2 954 (0)
P_{3}^{2} 400 000 2 204 (- 9 %)  41 932 (+ 15 %) 115 364s 4 017 (0)

Table VII. Impact of Value-Guided Partitioning

Size Memory peak Analysis time  Iterations Alarms
(LOCs)  (Mb)  (s)  ♯ T.p.I.
P_{1}^{1}  370  45 (-)  1.58 (- 27 %)  9 0.18s  0 (0)
P_{2}^{1}  9 500  173 (-)  82 (- 20 %)  17 4.8s  8 (8)
P_{3}^{1}  70 000 682 (+ 7 %) 2 236 (+ 26 %) 33 67.8s 563 (0)
P_{1}^{2} 70 000 438 (+ 1 %) 1 335 (+ 25 %) 20 66.7s 4 (0)
P_{2}^{2} 226 000 1 550 (+ 1 %) 16 589 (- 3 %) 66 251s  3 (0)
P_{3}^{2} 400 000  2 434 (-)  26 165 (- 28 %) 64 409s  8 (0)

of iterations but also the time per iteration tend to be worse than those of the partitioning analysis (despite simpler structures being used). At this point, we can imagine that not only the disabling of the partitioning of if-statements caused the analyzer to go through longer widening chains but also that it resulted in a coarser approximation of control flow. Another possibility is that the imprecision due to the absence of partitioning after if-statement may cause more imprecise partitions based on other criteria (loops, values of variables) to be generated, resulting in worse performances.

6.3.6 Inner Loops Partitioning. Table VI reports the result of the analysis without partitioning of loops. Again, we remark that loop partitioning is crucial for the precision of the analyses in the case of large applications, since the analysis of the four larger applications generate hundreds or thousands of false alarms. The invariants generated for the other programs are also significantly less precise (even though, the imprecision does not cause a larger number of alarms).

In the analysis time point of view, the same comments as above apply: in general the number of iterations is bigger, the time per iteration is smaller. In some cases (P_{2}^{2}), the analysis is faster; in other cases (P_{3}^{1}, P_{1}^{2}, P_{3}^{2}) it is slower. We note that P_{1}^{2} requires a very large number of iterations.

6.3.7 Impact of Value-Guided Partitioning. The impact of partitioning guided by values is presented in Table VII; it is less significant than the impact of the previous partitioning criteria, except in the case of the program P_{3}^{1} (dramatic number of alarms). In fact, a large number of these alarms result from worse ranges being inferred for computations such as (a∗x+b)/(x+1), whereas partitioning the traces locally according to the value of x allows for a precise range to be found.

In the case of the programs of the second series, value-guided partitioning helps

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

in proving precise ranges for mathematical functions, computed using linear interpolations as sketched in Figure 6.

We report no very important difference in execution time. Yet, we note that the more precise analysis of P_{2}^{2} requires more iterations, when partitioning is disabled.

Overall, it turns out extremely difficult to explain all variations in resources required by static analyses: no rule allows to predict the speed of an analysis; and, in practice, too many factors play a role, even though one may be able to tell in some cases what the most important ones are.

7. CONCLUSION

7.1 Contribution

We proposed a generic framework for defining trace partitioning domains, which allow the partitioning of traces to be based on the history of memory and control states. In particular, we allow for static partitioning analyses (the partition is chosen before the abstract iteration is carried out) and dynamic partitioning analyses (the analysis may refine the choice of partitions) to be designed in this framework.

We described an instantiation of this framework in the context of the Astrée project and presented the main data-structures and the strategies used in order to choose the partitions which should be created. In particular, the structure of the domain does not require any specific assumption to be made about the numerical domain; moreover, the iterator does not need much adaptation either.

Last, we provided experimental evidence of the role played by trace partitioning in the success of the analyzer, which can analyze very large industrial applications, and prove their safety (or at least, produce a very low number of false alarms). In fact, we noticed that trace partitioning not only improved the precision (which was to be expected) but also significantly reduces the execution time (which was not so intuitive), mainly due to faster convergence to stable ranges.

7.2 Related Work

The partitioning of control systems was introduced early in the static analysis field, e.g., in [Cousot 1981].

Among the closest related works, we can cite the trace partitioning static analysis framework proposed in [Handjieva and Tzolovski 1998]; however, this framework does not allow for the merge of partitions. Therefore, it incurs an exponential cost (in the number of if and while statements). Moreover, it does not allow for the dynamic partitioning guided by the values of a variable. By comparison, our work exploits a more powerful design of the domain, which allows for a more flexible and dynamic partitioning. The structure of our domain can be considered a kind of cofibered domain [Venet 1996], where the basis element defines a partition, for which a semantic value is given.

Another approach to partitioning in static analysis can be found in [Jeannet et al. 1999; Jeannet 2003]. It is based on a partitioning defined by predicates about the memory state, such as the value of boolean variables. The main difference is that we focus on traces history, instead of the values of some variables. Of course, in many cases, the trace properties could be stored in new variables used to instrument the program, but we believe our approach is more general, since the

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

predicates partitioning should be based on might not be expressible in the language we analyze, and also that approach would require a non fixed (or an infinite) number of instrumenting variables in the case of dynamic partitioning. Also the approach of using instrumenting variables could lead to a too big memory consumption by the analysis.

We can also find several occurrences of refinements of the control structure in the literature about data-flow analysis. For instance, [Sharir and Pnueli 1981] studied the most common approaches to inter-procedural analyses. A finer handling of paths in control flow graphs was proposed in [Holley and Rosen 1980]: it proceeds by integrating some information about the paths in the edges of the control flow graph, so as to allow for a finer approximation of the control flow to be computed. In particular, this technique was used in order to infer sets of feasible paths, so as to allow for more precise data-flow analyses. Similarly [Bodík et al. 1997] determines branch correlations so as to detect incompatible branchings and cut down the approximation set of feasible paths. Our approach not only performs intuitive abstractions of the paths, but also takes the path into account dynamically during the analysis.

The qualified flow analysis technique was extended with path profiles [Ball and Larus 1996] in [Ammons and Larus 1998]: profiling data should determine a set of hot paths (i.e., more frequently taken); then, these paths can be analyzed separately, with a higher precision (no path joins). Similarly, the express lane transformation [Melski and Reps 2003] aims at duplicating hot paths, so as to improve precision. However, this approach does not apply in our case. First, profiling very large applications with very large numbers of variables does not seem a realistic solution (at least in the time point of view). Secondly, this approach analyzes all “non-hot paths” together (i.e., with no partitioning), which would result in a low precision, with possibly many alarms. Indeed, the precision required in the analysis of a path for proving it safe is not related to how frequently it is used; therefore, our approach ignoring the frequency of paths is more adapted to program certification.

Recently, a large number of path sensitive analyses were proposed and implemented in various frameworks, such as [Ball and Rajamani 2001; Flanagan et al. 2002] and contributed to the verification of complex properties. However, path sensitivity is very costly in practice: we could not apply this technique to a single iteration of the main loop of either of the programs considered in Section 6.3. An interesting solution to the cost of path sensitivity (yet, not applicable in our case) proposed in [Das et al. 2002] relies on the encoding of the property of interest into an automaton (finite state machine): the transitions in the automaton can be used as criteria for partitioning the paths, and a heuristic is introduced so as to merge paths as well.

7.3 Exploring Other Partitioning Criteria

The definition of other kinds of partitioning criteria is a nice area for future work.

In particular, we are working on another instantiation of the framework described in Section 4, so as to partition traces according to an abstraction of the history of program executions defined by a collection of “events”.

This approach should allow to discriminate traces which satisfy some conditions defined from the history of program executions (such as: condition P was satisfied

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

at point l_{0} at the previous iteration in a loop and is violated at the current iteration) prove some functional properties of programs. We can relate this technique with the notion of synchronous product of the program to analyze with an adapted control structure: this method has been proposed and widely used for the verification of synchronous programs [Halbwachs et al. 1993].

We already applied this technique to the semantic slicing involved in the investigation of alarms raised by Astrée in [Rival 2005]. Though, we only considered rather simple abstractions of control flow history (based on automata), and we plan to consider more ambitious families of abstractions.

ACKNOWLEDGMENTS

We would like to thank the other members of the Astrée team, Patrick Cousot, Radhia Cousot, Jérôme Feret, Antoine Miné and David Monniaux for their help, suggestions and comments during the early developments of this work. We acknowledge Bruno Blanchet for his contribution to the Astrée project and the anonymous referees for their comments, which allowed to improve this paper.

REFERENCES

Ammons, G. and Larus, J. R. 1998. Improving data-flow analysis with path profiles. In Proc. of the Conference on Programming Languages, Design and Implementation (PLDI’98). ACM Press, New York, NY, Montréal (Canada), 72–84.

Ball, T. and Larus, J. R. 1996. Efficient path profiling. In ACM International Symposium on

Microarchitecture (MICRO 96). IEEE Computer Society, Washington DC, USA, 46–57. Ball, T. and Rajamani, S. K. 2001. Automatically validating temporal safety properties of

interfaces. In 8th International SPIN Workshop. Lecture Notes in Computer Science. Springer-Verlag, Toronto (Canada), 103–122.

Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., and Rival, X. 2002. Design and Implementation of a Special-Purpose Static Program Analyzer for Safety-Critical Real-Time Embedded Software, invited chapter. In The Essence of Computation: Complexity, Analysis, Transformation. Essays Dedicated to Neil D. Jones, T. Mogensen, D. Schmidt, and I. Sudborough, Eds. Lecture Notes in Computer Science 2566. Springer-Verlag, Berlin, Germany, 85–108.

Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., and Rival, X. 2003. A Static Analyzer for Large Safety Critical Software. In Conference on Programming Languages, Design and Implementation (PLDI’03). ACM Press, New York, San Diego (USA), 196–207.

Bodík, R., Gupta, R., and Soffa, M. L. 1997. Refining data flow information using infeasible paths. In 6th European Software Engineering Conference and 5th ACM SIGSOFT Symposium on Foundations of Software Engineering. Springer-Verlag, Zurich (Switzerland), 361–377.

Bourdoncle, F. 1993. Efficient chaotic iteration strategies with widenings. Lecture Notes in

Computer Science 735, 128–142. Bryant, R. 1986. Graph based algorithms for boolean function manipulation. IEEE Trans.

Comput. C-35, 677–691. Cousot, P. 1981. Semantic foundations of program analysis. In Program Flow Analysis: Theory

and Applications, S. Muchnick and N. Jones, Eds. Prentice-Hall, Inc., Englewood Cliffs, New Jersey, Chapter 10, 303–342.

Cousot, P. and Cousot, R. 1977. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Conference Record of the 4th Symposium on Principles of Programming Languages (POPL’77). ACM Press, New York, NY, Los Angeles, California, 238–252.

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

Cousot, P. and Cousot, R. 1979. Systematic design of program analysis frameworks. In Conference Record of the 6th Symposium on Principles of Programming Languages (POPL’79). ACM Press, New York, NY, San Antonio, Texas, 269–282.

Cousot, P. and Cousot, R. 1992a. Abstract interpretation and application to logic programs.

Journal of Logic Programming 13, 2–3, 103–179. Cousot, P. and Cousot, R. 1992b. Abstract interpretation frameworks. Journal of Logic and

Computation 2, 4 (Aug.), 511–547. Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., and Rival, X.

2005. The ASTRÉE analyzer. In European Symposium On Programming (ESOP’05). Lecture Notes in Computer Science, vol. 3444. Springer-Verlag, Edimburgh (Scotland).

Cousot, P. and Halbwachs, N. 1978. Automatic discovery of linear restraints among variables of a program. In Conference Record of the 5th Symposium on Principles of Programming Languages (POPL’78). ACM Press, New York, NY, Tucson, Arizona, 84–97.

Das, M., Lerner, S., and Seigle, M. 2002. Esp: Path-sensitive program verification in polynomial time. In Proc. of the Conference on Programming Languages, Design and Implementation (PLDI’02). ACM Press, New York, NY, Berlin (Germany), 57–68.

Feret, J. 2004. Static analysis of digital filters. In European Symposium On Programming (ESOP’04). Number 2986 in Lecture Notes in Computer Science. Springer-Verlag, Barcelona, Spain, 33–48.

Feret, J. 2005. The arithmetic-geometric progression abstract domain. In 6th conference on Verification, Model-Cecking and Abstract Interpretation (VMCAI’05), R. Cousot, Ed. Lecture Notes in Computer Science 3385. Springer-Verlag, Paris, France, 2–18.

Flanagan, C., Leino, K. R., Lillibridge, M., Nelson, G., Saxe, J. B., and Stata, R. 2002. Extended static checking for java. In Proc. of the Conference on Programming Languages, Design and Implementation (PLDI’02). ACM Press, New York, NY, 234–245.

Granger, P. 1989. Static analysis of arithmetical congruences. In International Journal of

Computer Mathematics. Vol. 30. 165–190. Halbwachs, N., Lagnier, F., and Raymond, P. 1993. Synchronous observers and the verifica-

tion of reactive systems. In Algebraic Methodology and Software Technology (AMAST ’93). Workshops in Computing. Springer, Twente (Netherlands), 83–96.

Handjieva, M. and Tzolovski, S. 1998. Refining static analyses by trace-based partitioning using control flow. In 5th International Static Analysis Symposium (SAS’98). Lecture Notes in Computer Science. Springer Verlag, 200–214.

Holley, L. H. and Rosen, B. K. 1980. Qualified data flow problems. In Proc. of the 7th ACM Symposium on Principles of Programming Languages (POPL’80). ACM Press, New York, NY, Las Vegas (Nevada), 68 – 82.

Horwitz, S., Reps, T., and Binkley, D. 1988. Interprocedural slicing using dependence graphs. In Conference on Programming Languages, Design and Implementation (PLDI’03). ACM Press, New York, Atlanta (USA), 35–46.

Jeannet, B. 2003. Dynamic partitioning in linear relation analysis: Application to the verification

of reactive systems. Formal Methods in System Design 23, 1, 5–37. Jeannet, B., Halbwachs, N., and Raymond, P. 1999. Dynamic partitioning in analyses of

numerical properties. In 6th Static Analysis Symposium SAS. Lecture Notes in Computer Science, vol. 1694. Springer-Verlag, Venice (Italy), 39–50.

Jones, N. D. and Muchnick, S. S. 1979. Flow analysis and optimization of LISP-like structures.

In 6th POPL. ACM Press, San Antonio, Texas, 244–256. Mauborgne, L. 2004. ASTRÉE: Verification of absence of run-time error. In Building the Infor-

mation Society. Kluwer Academic Publishers, Toulouse, France, Chapter 4, 384–392. Melski, D. and Reps, T. W. 2003. The interprocedural express-lane transformation. In 12th

International Conference on Compiler Construction (CC’03). Lecture Notes in Computer Science. Springer-Verlag, Varsaw (Poland), 200–216.

Miné, A. 2001. The Octagon Abstract Domain. In Analysis, Slicing and Transformation (in WCRE). IEEE. IEEE CS Press, Stuttgart, Germany, 310–319.

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

Plotkin, G. D. 1981. A structural approach to operational semantics. Tech. Rep. DAIMI FN-19,

Aarhus University, Denmark. Sept. Reps, T., Horwitz, S., and Sagiv, M. 1995. Precise interprocedural dataflow analysis via graph

reachability. In 22nd Symposium on Principles of Programming Languages (POPL’95). ACM Press, New York, San Francisco (USA), 49–61.

Rival, X. 2005. Understanding the origin of alarms in astrée. In 12th Static Analysis Symposium

(SAS’05). LNCS, vol. 3672. Springer-Verlag, London (UK), 303–319. Sharir, M. and Pnueli, A. 1981. Two approaches to interprocedural data flow analysis. In

Program Flow Analysis: Theory and Applications, S. Muchnick and N. Jones, Eds. Prentice-Hall, Inc., Englewood Cliffs, New Jersey, Chapter 7, 189–233.

Venet, A. 1996. Abstract Cofibered Domains: Application to the Alias Analysis of Untyped Programs. In Static Analysis Symposium (SAS’96). Lecture Notes in Computer Science, vol. 1145. Springer-Verlag, Aachen, Germany.

Received September 2005.