Antoine Toubhans
email: toubhans@di.ens.fr

Bor-Yuh Evan Chang

Xavier Rival
email: rival@di.ens.fr

Bor-Yuh Evan

An Abstract Domain Combinator for Separately Conjoining Memory Abstractions

published or not. The documents may come   L'archive ouverte pluridisciplinaire

Introduction

While there exist static analyses for the most common data structures such as lists, trees, or even overlaid lists and trees [START_REF] Distefano | A local shape analysis based on separation logic[END_REF][START_REF] Chang | Relational inductive shape analysis[END_REF][START_REF] Lee | Program analysis for overlaid data structures[END_REF][START_REF] Dragoi | Local shape analysis for overlaid data structures[END_REF], it is uncommon for static analyses to efficiently support all of these simultaneously. For instance, consider the code fragment of Fig. 1 that simultaneously manipulates linked lists and trees, iteratively picking some value from the list and searching for it in the tree. Although verification of the memory safety and data structures preservation is possible with several tools (e.g. [START_REF] Rival | Calling context abstraction with shapes[END_REF][START_REF] Sagiv | Parametric shape analysis via 3-valued logic[END_REF]), this will not take into account most efficient data-structure-specific algorithms (e.g. analysis for linked lists presented in [START_REF] Manevich | Shape analysis by graph decomposition[END_REF] achieves polynomial complexity transfer functions). On the other hand, using only a linked-list-specific efficient analysis will lead to a dramatic loss of precision, as tree features are not supported. The general problem is much broader than just lists and trees: in real-world programs, it is common to find not only lists, trees, and overlaid lists and trees, but also buffers, arrays, and other complex heap structures, and therefore static analysis is either imprecise or inefficient.

Instead of using one monolithic analysis, we propose to combine off-the-shelf datastructure-specific analyses that reason about disjoint regions of memory. The approach presented in this paper is in the context of abstract interpretation [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF]. Therefore, combining analyses is realized by a separating combination of memory abstract domains called 01 : int * x = NULL; 10 : while( . . . ){ 24 : r = searchTree( * x, t); 02 : List * h, * e;

11 : x = malloc(sizeof(int)); 25 : // do something on r 03 : Tree * t, * r;

12 : * x = e -> data . . . . . . . . . 30 : } Fig. 1. A code fragment manipulating simultaneously several data structures the sub-domains. Combined memory abstract domains describe each disjoint memory region using one of its sub-domains. We show how separation (i.e. the fact that data structures do not share cell blocks) can be used to decompose a heterogeneous memory into several sub-instances that can be handled independently. This construction increases and eases the abstract domain design capabilities. Combined abstract domains are more extensible and flexible, as a sub-domain can be individually added, removed, strengthened, or weakened in the combination. Moreover, it allows paying the cost of complex algorithms that usually come with expressive abstract domains only in the memory region that really requires it. On the other hand, simpler light-weight abstract domains can be used to represent a significant part of the memory that does not contain complex structures.

Such a combination poses several challenges. Because, even if disjoint in memory, concrete data structures can still be correlated (e.g. have shared values or pointers to each other), we need to carefully abstract the interface between memory regions in the combination. Maintaining a right partitioning (i.e. which memory region should be abstracted in which sub-domain) during the analysis process is also challenging. For example, when analyzing a memory allocation, the analysis decides which sub-domains should handle it. Even though any choice is sound, there are sub-domains more relevant than others in many cases. This approach has been successfully applied to numerical domains and made it possible to obtain scalable and precise analyses [START_REF] Blanchet | A static analyzer for large safety-critical software[END_REF] and reusable abstract domains [START_REF] Jeannet | Apron: A library of numerical abstract domains for static analysis[END_REF]. Our proposal brings, in a way, the same improvement to memory abstract domains. We justify this statement by the following contributions:

we introduce (Section 2) and formalize (Section 3.2) the separating combination functor that takes two memory abstract sub-domains matching the signature given in Section 3.1 and returns a new combined memory abstract domain; -we define an abstract domain for the interface between memory regions (Section 3.2) that carefully describes correlations between memory regions; -we set up the abstract transfer functions (Section 4) that compose abstract transfer functions of sub-domains and extract information from an abstract interface; -we give a heuristic for the decision of which sub-domain should handle a newly allocated block (Section 4.1); -we evaluate the separating combination functor by an implementation in the Mem-CAD analyzer (Section 5) and empirically verify that combined analyses remain efficient and precise while offering greater flexibility.

Overview

In this section, we provide an informal description of our combined analysis (formal details are presented in Sections 3 and 4). We present an abstract interpretation [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF] based analysis of the code fragment of Fig. 1, using a combination of memory abstract domains. The analysis goal is to prove memory safety and data structure (lists and trees) preservation. Fig. 2 shows two abstract memories computed during the analysis.

An abstraction of the memory using several memory abstract domains. The program manipulates a memory that can be decomposed in three disjoint regions (i) the list region (denoted L ) containing linked-list nodes (ii) the tree region (denoted T ) containing tree nodes (iii) the region accounting for the rest of the memory that contains only bounded data structures (denoted B ). This naturally leads to the choice of a separating combination of three memory abstract sub-domains M ♯ l , M ♯ t , M ♯ b that will reason respectively about region L , T and B .

Fig. 2(a) shows the combined abstract memory computed by the analysis before line 11. Each thick black bordered boxes (labeled B , L and T ) contains an element

m ♯ b ∈ M ♯ b , m ♯ l ∈ M ♯ l and m ♯ t ∈ M ♯ t called abstract sub-memories.
Greek letters that appear in the sub-memories are called the symbolic names and are used by sub-domains to internally represent concrete values and heap addresses. The combined abstract memory represents a set of memories where variable h (resp. e) points to the head (resp. the last element) of a linked list, variable t points to the root of a tree, variable x is the null pointer and content of variable r can be any concrete value.

Describing the interface between memory regions is crucial for precision. In particular, the combined abstract memory should account for (i) pointers from region B to regions L and T and (ii) sharing of values between cells of different memory regions such as value v in the last list node and the left tree node from the tree root. The interface abstract domain I ♯ (Section 3.2) achieves this by maintaining a set of equalities between symbolic names of different abstract sub-memories. An equality between two symbolic names simply means that they represent the same concrete value. For instance, pointer h crossing the memory regions B and L is represented by (i) β 0 representing the content of cell h in the m ♯ b , (ii) λ 0 representing the address of the head of the list in the m ♯ l , and (iii) equality β 0 = λ 0 in the abstract interface. Thus, this combined abstract memory is a quadruple made of three abstract sub-memories m ♯ b ∈ M ♯ b , m ♯ l ∈ M ♯ l and m ♯ t ∈ M ♯ t and an abstract interface i ♯ ∈ I ♯ . In the two combined abstract memories shown in Fig. 2, abstract sub-memories are represented in gray inside the thick black boxes whereas dark blue edges and values depict the abstract interface. In the following, we demonstrate the key features of the combination of memory abstract domains by analyzing the two program statements at line 11 and 12. In particular, the assignment at line 11 involves a memory allocation but remains quite simple compared to the assignment at line 12 that requires post-condition computations to be distributed across sub-memories using the abstract interface. The first step when analyzing an assignment consists in evaluating its left and right hand-sides, that is, finding symbolic names representing the address of the updated cell and the written value (Section 4.2).

β 0 β 1 0 β 2 ⊤ λ 0 λ 1 λ 2 ⊤ λ 1 ⊤ v 0 . . . τ 0 τ 2 τ 1 τ 1 τ 2 ⊤ ⊤ v . . . . . . . . . . . .
β 0 β 1 β 3 v β 2 β 4 λ 0 λ 1 λ 2 ⊤ λ 1 ⊤ v 0 . . . τ 0 τ 2 τ 1 τ 1 τ 2 ⊤ ⊤ v . . .
The right hand side of the assignment at line 11 contains a memory allocation instruction, hence the analysis should decide which sub-domain is the most relevant for handling it. Indeed, even though any choice is sound for the analysis, a bad decision could lead to a loss in precision or in efficiency. While the three sub-domains could precisely handle the memory allocation, M ♯ b is expected to be more efficient for handling bounded data structures. Because of the type passed to malloc, the new cell will likely never be summarized as part of a list or a tree, m ♯ b should therefore handle the memory allocation. While not complete (C types cannot fully describe the programmer intended data structure), we find that this simple heuristic works well in practice. In Fig. 2(b), this sub-memory contains a new cell at abstract address β 3 (red background highlights created cells). The right hand side is evaluated to β 3 and evaluation of the left hand side is trivial and provides a symbolic name that is in m ♯ b so that both are evaluated in the same sub-memory. Therefore and thanks to the local reasoning principle, the postcondition can be computed only for abstract sub-memory m ♯ b , using the sound abstract transfer function provided by M ♯ b . In Fig. 2(b), the cell that correspond to x has been updated to β 3 (green background highlights updated cells).

Computing an abstract post-condition of the assignment at line 12 poses two main issues. First, the evaluation of its right hand side crosses abstract sub-memories that involves a mechanism for extracting information from i ♯ . Secondly, the left and right hand sides are not evaluated in the same sub-memories. Thus, accurately handling this assignment requires sound abstract transfer functions for I ♯ . The right hand side is evaluated iteratively over its syntax: (i) the content of cell e is evaluated to

β 1 in m ♯ b (ii) β 1 cannot be resolved as an address of a cell in m ♯ b (iii) equality β 1 = λ 2 can be extracted from the abstract interface i ♯ , that allows the resolution to continue in m ♯ l (iv) the content of abstract address λ 2 at field data is v in m ♯ l . As * x is evaluated to β 3 in m ♯
b , the left and right hand sides are evaluated respectively in m ♯ b and m ♯ l . Thus, the post-condition will be computed (i) in m ♯ b as the written cell is abstracted in this abstract sub-memory (ii) in i ♯ as the written value is not represented in m ♯ b . The cell whose abstract address is β 3 is updated to a fresh symbolic name in m ♯ b , that is then set to be equal to v in i ♯ using the abstract transfer function for I ♯ .

The separating combination of memory abstract domains

In this section, we first set up a general notion of a memory abstract domain (Section 3.1). before introducing the separating combination (Section 3.2). A memory abstract domain M ♯ provides a representation for sets of concrete memories. Intuitively, it consists of a set of predicates describing memory quantified on symbolic names (denoted N M ♯ ) that represent concrete values (denoted V). Thus, concretization involves valuations mapping symbolic names to the value they represent. Once this general notion is formalized, we formally introduce the separating combination as a binary functor that takes as input two memory abstract domains

M ♯ 1 , M ♯ 2 and returns a new memory abstract domain M ♯ 1 M ♯ 2 .
The functor can be iteratively applied in order to cope with more than two memory abstract sub-domains. The combined abstract domain describes disjoint memory regions using either predicates of M ♯ 1 or M ♯ 2 . Moreover, correlations between regions are described by the interface abstract domain I ♯ that maintains equalities between symbolic names quantified in different sub-memories.

Memory abstract domain

Concrete memories. We let A denote the set of concrete addresses, and we assume addresses to be concrete values (i.e. A ⊆ V). Henceforth, we adopt a standard model for concrete memories where a concrete memory m is a finite map from addresses to values. Therefore, the set of concrete memories is defined by M def = A ⇀ fin V. We let F = {f, g, . . .} denote the set of valid field names, and we treat them as numerical offsets so that for a ∈ A and f ∈ F, a + f denotes the address at field f of the block at address a. As the separating combination is reasoning about disjoint memory region, we write m 1 ⊎ m 2 for the union of two disjoint memories (i.e. dom(m 1 ) ∩ dom(m 2 ) = ∅, where dom(m i ) denotes the domain of m i as a partial function).

A memory abstract domain is a lattice of abstract memories M ♯ , together with a fixed infinite set of symbolic names N M ♯ , a concretization function γ M ♯ and sound abstract transfer functions (detailed in Section 4). An abstract memory m ♯ ∈ M ♯ internally utilizes symbolic names to represent concrete values. We define the set of valuations

V M ♯ def = N M ♯ ⇀ fin V. Intuitively, a valuation ν ∈ V M ♯ relates symbolic names to con- crete values when concretizing. Concretization is a function γ M ♯ : M ♯ → P(M × V M ♯ ) and γ M ♯ (m ♯ ) collects a set of couples (m, ν) ∈ M × V M ♯
made of a concrete memory and a valuation that maps symbolic names quantified in m ♯ to concrete values in m.

Example 1 (Bounded structure abstract domain). As a first example, we describe a memory abstract domain that represents precisely block contents, but is unable to summarize unbounded regions such as list and tree data structures. This memory abstract domain can be considered an instantiation of M ♯ b seen in the overview (Section 2). The set of symbolic names consists of either symbols for addresses (denoted α a 0 , α a 1 , . . .) or symbols for cell contents (denoted β c 0 , β c 1 , . . .). Definitions of abstract memories and

m ♯ b = α a 0 → {0 : β c 0 } * α a 1 → {0 : β c 1 } * α a 2 → {0 : β c 2 } * α a 3 → {0 : β c 3 } * α a 4 → {0 : β c 4 } ∧ &h = α a 0 ∧ &e = α a 1 ∧ &x = α a 2 ∧ &t = α a 3 ∧ &r = α a 4 ∧ β c 2 = 0 (
α a 0 → 0x...a0 β c 0 → 0x...b0 α a 1 → 0x...a4 β c 1 → 0x...c0 α a 2 → 0x...a8 β c 2 → 0x0 α a 3 → 0x...a12 β c 3 → 0x...d0 α a 4 → 0x...a16 β c 4 → 0x0 (c) Valuation ν b : N M ♯ b → V Fig. 3. Bounded data structure abstract domain: (m b , ν b ) ∈ γ M ♯ b (m ♯ b ) 0x...c4 0x
ν l : λ0 → 0x...b0 λ2 → 0x0 λ1 → 0x...c0 λ3 → 666 (b) Valuation ν l : N M ♯ l → V λ0 λ1 λ2 λ3 λ 2 = 0x0
(m l , ν l ) ∈ γ M ♯ l (m ♯ l )
the concretization function is given by:

m ♯ ::= abstract memories γ M ♯ b (m ♯ ) | emp empty memory {([ ], ν) | ν ∈ V M ♯ } | α a → {f : β c } memory cell {([ν(α a ) + f → ν(β c )], ν) | ν ∈ V M ♯ } | m ♯ 1 * m ♯ 2 disjoint memory {(m 1 ⊎ m 2 , ν) | ∀i ∈ {1, 2}. (m i , ν) ∈ γ M ♯ b (m ♯ i )} | m ♯ b ∧ n ♯ with constraints {(m, ν) | (m, ν) ∈ γ M ♯ b (m ♯ b ) ∧ ν n ♯ }
An abstract memory m ♯ consists of a separating conjunction of atomic predicates α a → {f : β c } abstracting a cell at address α a + f of content β c . Fig. 3 shows the abstract submemory m ♯ b depicted in labeled box B in Fig. 2(a) and a pair (m b , ν b ) that concretizes it. Properties about values and addresses are expressed in n ♯ , using a product with a numerical domain [START_REF] Chang | Modular construction of shape-numeric analyzers[END_REF]. For instance, a numerical domain enabling linear equalities is used in Fig. 3(a). Besides, a product with a pointer domain may be used to capture, for example, aliasing relations. The memory abstract domain of [START_REF] Miné | Field-sensitive value analysis of embedded C programs with union types and pointer arithmetics[END_REF] extends this basic layout (and handles unions, non-fixed cell sizes, etc.).

Example 2 (Separating shape graphs). The separating shape graph abstract domain of [START_REF] Chang | Relational inductive shape analysis[END_REF] provides a second example of a memory abstract domain. An abstract memory is a separating conjunction [START_REF] Reynolds | Separation logic: A logic for shared mutable data structures[END_REF] of predicates, which could be either points-to predicates (depicted as thin edges in Fig. 4(c in Fig. 4(c)). Inductive predicates are annotated with inductive definitions supplied as a parameter of the domain. Thus, depending on the parameterization, this domain may provide an instantiation for M ♯ l or M ♯ t in the example of Section 2. Non-parameterizable abstract domains [START_REF] Distefano | A local shape analysis based on separation logic[END_REF] have a similar layout. A graph containing only points-to edges is concretized into the disjoint merge of the cells described by each points-to edge. The concretization of inductive predicates proceeds by unfolding. For instance the inductive definition for list leads to the unfolding rule shown in Figure 5. As in the previous example, a numerical abstract domain should be used in order to express content properties. Fig. 4(c) presents an instance m ♯ l of the separating shape graph domain parameterized by a list definition that corresponds to the labeled box L depicted in Fig. 2(a) in the overview. A pair (m l , ν l ) that concretizes m ♯ l is given in Fig. 4(a) and Fig. 4(b).

The separating combination

In this section, we assume a pair of memory abstract domains

M ♯ 1 , M ♯ 2 are fixed, with in- dependent sets of symbolic names N M ♯ 1 , N M ♯ 2 and concretization functions γ M ♯ 1 , γ M ♯ 2 .
In the following, we introduce the interface abstract domain before defining the combined memory abstract domain

M ♯ 1 M ♯ 2 .
Interface abstract domain. We let I ♯ M ♯ 1 , M ♯ 2 denote the interface abstract domain that expresses sets of equality relations between symbolic names of M ♯ 1 and M ♯ 2 . Intuitively, an abstract interface is a finite set of pairs representing equalities. Thus, the interface abstract domain is defined by

I ♯ M ♯ 1 , M ♯ 2 def = P fin (N M ♯ 1 ×N M ♯ 2
) and an abstract interface i ♯ is concretized into a set of pairs of valuations of M ♯ 1 and M ♯ 2 in the following way:

γ I ♯ (i ♯ ) def = (ν 1 , ν 2 ) ∈ V M ♯ 1 × V M ♯ 2 | ∀(α 1 , α 2 ) ∈ i ♯ . ν 1 (α 1 ) = ν 2 (α 2 )
We write I ♯ instead of I ♯ M ♯ 1 , M ♯ 2 when there is no ambiguity about the choice of the memory abstract sub-domains. We also define a judgment i ♯ ⊢ α 1 = α 2 meaning that the pair (α 1 , α 2 ) belongs to the transitive closure of the relation induced by i ♯ . Thus, it meets the soundness condition i

♯ ⊢ α 1 = α 2 ∧ (ν 1 , ν 2 ) ∈ γ I ♯ (i ♯ ) ⇒ ν 1 (α 1 ) = ν 2 (α 2 ).
The separating abstract domain combinator. Combined abstract memories consist of triples (m ♯ 1 , m ♯ 2 , i ♯ ) made of two abstract sub-memories describing disjoint memory regions and an abstract interface representing correlations between the sub-memories. Thus, the combined abstract domain is defined by

M ♯ 1 M ♯ 2 def = M ♯ 1 × M ♯ 2 × I ♯ M ♯ 1 , M ♯ 2 .
We define the set of symbolic names of the combined abstract domain as the disjoint

m ♯ b = α a 0 → {0 : β c 0 } * α a 1 → {0 : β c 1 } * α a 2 → {0 : β c 2 } * α a 3 → {0 : β c 3 } * α a 4 → {0 : β c 4 } ∧ &h = α a 0 ∧ . . .
ν b ⊕ ν l : N M ♯ b M ♯ l -→ V (M ♯ b : α a 0 ) → 0x...a0 (M ♯ b : β c 0 ) → 0x...b0 (M ♯ b : α a 1 ) → 0x...a4 (M ♯ b : β c 1 ) → 0x...c0 (M ♯ b : α a 2 ) → 0x...a8 (M ♯ b : β c 2 ) → 0x0 (M ♯ b : α a 3 ) → 0x...a12 (M ♯ b : β c 3 ) → 0x...d0 (M ♯ b : α a 4 ) → 0x...a16 (M ♯ b : β c 4 ) → 0x0 (M ♯ l : λ0) → 0x...b0 (M ♯ l : λ2) → 0x0 (M ♯ l : λ1) → 0x...c0 (M ♯ l : λ3) → 666 (c) Valuation ν b ⊕ ν l ∈ V M ♯ b M ♯ l
Fig. 6. Combined memory abstract domain:

(m b ⊎ m l , ν b ⊕ ν l ) ∈ γ M ♯ b M ♯ l (m ♯ b , m ♯ l , i ♯ ) as (m b , ν b ) ∈ γ M ♯ b (m ♯ b ) (Fig. 3), (m l , ν l ) ∈ γ M ♯ l (m ♯ l ) (Fig. 4) and (ν b , ν l ) ∈ γ I ♯ (i ♯ )
union of symbolic names of the abstract sub-domains. Formally:

N M ♯ 1 M ♯ 2 def = (M ♯ 1 : α 1 ) | α 1 ∈ N M ♯ 1 ⊎ (M ♯ 2 : α 2 ) | α 2 ∈ N M ♯ 2
At the combined abstract domain level, (M ♯ i : α i ) denotes symbolic name α i of the abstract sub-domain M ♯ i . To define the meaning of a combined abstract memory, we give a concretization function

γ M ♯ 1 M ♯ 2 : M ♯ 1 M ♯ 2 → P(M × V M ♯ 1 M ♯ 2 ) that derives from concretization functions γ M ♯ i : M ♯ i → P(M × V M ♯ i
) of the memory abstract subdomains. To achieve this, we define a valuation combinator ⊕ :

V M ♯ 1 × V M ♯ 2 → V M ♯ 1 M ♯ 2
that puts two valuations aside:

(ν 1 ⊕ ν 2 )(M ♯ 1 : α 1 ) def = ν 1 (α 1 ) (ν 1 ⊕ ν 2 )(M ♯ 2 : α 2 ) def = ν 2 (α 2 )
Then, the concretization of a combined abstract memory is given by:

γ M ♯ 1 M ♯ 2 (m ♯ 1 , m ♯ 2 , i ♯ ) def = (m 1 ⊎ m 2 , ν 1 ⊕ ν 2 ) ∀i ∈ {1, 2}. (m i , ν i ) ∈ γ M ♯ i (m ♯ i ) ∧ (ν 1 , ν 2 ) ∈ γ I ♯ (i ♯ )
Example 3 (Separating combination of M ♯ b and M ♯ l ). We now consider an instantiation of the separating combination functor, with the bounded data structure domain M ♯ b (presented in Example 1) and the list-parameterized separating shape graph domain M ♯ l (presented in Example 2). Fig. 6(a) presents a combined abstract memory (m ♯ b , m ♯ l , i ♯ ) that combines abstract sub-memories already presented in Fig. 3(a) and Fig. 4(c) together with the abstract interface i ♯ = {(β c 0 , λ 0 ), (β c 1 , λ 1 )}. We provide a pair (m, ν) in Fig. 6(b) and Fig. 6(c) concretizing (m ♯ b , m ♯ l , i ♯ ) obtained by combining the concrete pairs (m b , ν b ) and (m l , ν l ) presented in Fig. 3 and Fig. 4. Note that

(ν b , ν l ) ∈ γ I ♯ (i ♯ ) as ν b (β c 0 ) = ν l (λ 0 ) = 0x...b0 and ν b (β c 1 ) = ν l (λ 1 ) = 0x...c0.

Analysis algorithms

We now discuss the inference of invariants in the combined domain. A memory abstract domain M ♯ provides for each concrete memory operation f : M → P(M), a counterpart abstract transfer function

f ♯ : M ♯ → M ♯ that is sound (i.e. ∀(m, ν) ∈ γ M ♯ (m ♯ ). ∀m ′ ∈ f (m). ∃ν ′ ⊇ ν. (m ′ , ν ′ ) ∈ (γ M ♯ • f ♯ )(m ♯ )).
Abstract transfer functions may introduce new symbolic names but may not remove nor change the meaning of existing symbolic names. Hence, a valuation ν ′ in the concretization of the postcondition must extend valuation ν that concretizes the pre-condition. Abstract interpreters also require lattice operations (e.g. inclusion checking, widening) to achieve precise fixed point computations.

In a combined abstract domain, abstract transfer functions should distribute computations to the sub-memories and the abstract interface, using abstract transfer functions provided by sub-domains. In this section, we detail this mechanism for abstract transfer functions handling memory allocations (Section 4.1), assignments (Sections 4.2, and 4.3), and for inclusion checking (Section 4.4).

Creation of memory cells

Creation of new memory cells occurs either when a block for a new variable is created or when heap space is allocated at run time (e.g. malloc as at line 11 in Fig. 1). In a memory abstract domain M ♯ , this operation is handled by the abstract transfer function new M ♯ , which is the abstract counterpart of the concrete transfer function new : int × M → P(A × M) (defined in a standard way). Intuitively, new M ♯ takes as input an integer size s and an abstract memory m ♯ pre and returns a pair consisting of a symbolic name α representing the address of the allocated block and an abstract memory m ♯ post where the cell has been created. Therefore, it ensures that, if new M ♯ (s, m ♯ pre ) = (α, m ♯ post ) and (m, ν) ∈ γ M ♯ (m ♯ pre ), then the following holds:

(a, m ′ ) ∈ new (s, m) ⇒ ∃ν ′ ⊇ ν. (m ′ , ν ′ ) ∈ γ M ♯ (m ♯ post ) ∧ ν ′ (α) = a
Creation of memory cells in a combined domain. Because of the separation principle (Section 3.2), a cell must be represented in exactly one sub-memory in a combined abstract memory m ♯ = (m ♯ 1 , m ♯ 2 , i ♯ ). Therefore, we provide two possible definitions for new M ♯ 1 M ♯ 2 deriving from two symmetric rules NEW1 and NEW2 (NEW2 is shown in Appendix A.1). Intuitively, the abstract transfer function defined by rule NEW1 (resp. NEW2) always represents new cells using sub-domain

M ♯ 1 (resp. M ♯ 2 ). NEW1 new M ♯ 1 (s, m ♯ 1 ) = (α 1 , m ♯ 1,post ) new M ♯ 1 M ♯ 2 (s, (m ♯ 1 , m ♯ 2 , i ♯ )) = ((M ♯ 1 : α 1 ), (m ♯ 1,post , m ♯ 2 , i ♯ ))
While both choices are sound, some sub-domains are more suitable than others. For instance, in M ♯ b M ♯ l , it would be inappropriate to let the allocation of a cell expected to be summarized as part of a list be done in M ♯ b , where summarization cannot be achieved.

derives from rule WRITEACROSSWEAK1, and produces the following post-condition:

m ♯ b = α a 0 → {0 : β c 0 } * α a 1 → {0 : β c 1 } * α a 2 → {0 : β c 2 } * α a 3 → {0 : β c 3 } * α a 4 → {0 : β c 4 } * α a 5 → {0 : γ c } ∧ &x = α a 2 ∧ . . . ∧ β c 2 = α a 5 λ0 λ1 λ2 λ3 m ♯ l λ 2 = 0x0 next data list list i ♯ = {(β c 0 , λ 0 ) , (β c 1 , λ 1 ) (γ c , λ 3 )}

Inclusion checking

Fix-point computations [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF] require widening and inclusion checking operators. In this section, we only detail the algorithm for inclusion checking as the widening algorithm is similar [START_REF] Chang | Modular construction of shape-numeric analyzers[END_REF]. At a memory abstract domain M ♯ level, the inclusion checking relies on the abstract comparison operator compare M ♯ that inputs two abstract memories m ♯ l and m ♯ r and returns a mapping Φ when it successfully establishes the abstract inclusion m ♯ l ⊑ m ♯ r . Intuitively, the returned mapping relates symbolic names in m ♯ r to symbolic names in m ♯ l that valuations should map to the same value for the inclusion to hold. More formally, the soundness condition states the following:

compare M ♯ (m ♯ l , m ♯ r ) = Φ ∧ (m, ν) ∈ γ M ♯ (m ♯ l ) =⇒ (m, ν • Φ) ∈ γ M ♯ (m ♯ r )
Inclusion checking in a combined domain. To compare the two combined abstract mem-

ories m ♯ l = (m ♯ 1,l , m ♯ 2,l , i ♯ l ) and m ♯ r = (m ♯ 1,r , m ♯ 2,r , i ♯ r
), the analysis first invokes the abstract comparisons of the sub-domains respectively on (m ♯ 1,l , m ♯ 1,r ) and (m ♯ 2,l , m ♯ 2,r ). When both succeed and thus return Φ 1 and Φ 2 , the analysis checks the inclusion of the abstract interfaces by: i

♯ l ⊑ Φ2 Φ1 i ♯ r ⇐⇒ ∀(α 1 , α 2 ) ∈ i ♯ r . i ♯ l ⊢ Φ 1 (α 1 ) = Φ 2 (α 2 )
. Therefore, the abstract comparison operator is defined by the following rule:

INCL compare M ♯ 1 (m ♯ 1,l , m ♯ 1,r ) = Φ 1 compare M ♯ 2 (m ♯ 2,l , m ♯ 2,r ) = Φ 2 i ♯ l ⊑ Φ2 Φ1 i ♯ r compare M ♯ 1 M ♯ 2 ((m ♯ 1,l , m ♯ 2,l , i ♯ l ), (m ♯ 1,r , m ♯ 2,r , i ♯ r )) = Φ 1 ⊕ Φ 2
Refinement using initial mappings. While sound, such a definition could lead to a loss of precision. For some memory abstract domains (such as the separating shape graphs domain), the abstract comparison operator internally initializes a mapping between symbolic names representing addresses of the same program variable (that valuations should clearly map to the same value). However, in a combined domain, a sub-memory with no such symbolic names is plausible (e.g. consider m ♯ l in the combined abstract memory of Fig. 6(a)), and the sub-domain abstract comparison will therefore likely fail to establish the inclusion. To cope with that issue, the analysis provides an initial mapping as hint to the unsuccessful abstract comparison, that derives from the relationship inferred by the successful abstract comparison. More precisely, if compare M ♯ 1 succeeds and returns Φ 1 , the initial mapping defined by Fig. 8. Analysis results (measured on a 2.2 Ghz Intel Core i7 with 8 GB of RAM): MAD is the memory abstract domain used (B stands for the bounded data structure domain, I<.> stands for the separating shape graphs domain instantiated with inductive definitions that are either list or tree, stands for separating combination of domains), #P is the number of properties proven by the analysis, ∨ is average number of disjuncts at each program point, t is the total analysis time in seconds,% is the time of analysis compared to analysis using a monolithic domain, tCF (resp. tSD) is the time of analysis spent in the combination functor (resp. sub-domains), #R is the number of read operation calls and #RA is the number of read operations crossing sub-memories.

Φ init 2 (β 2,r ) = β 2,l ⇔ ∃β 1,r ∈ N M ♯ 1 . i ♯ r ⊢ β 1,r = β 2,r ∧ i ♯ l ⊢ Φ 1 (β 1,r ) = β 2,

Implementation and empirical evaluation

We test empirically the precision and efficiency of the combined analysis compared to a monolithic one and describe the results here. The separating combination described in this paper is implemented in the MemCAD analyzer 3 . The analysis is fully automatic. It takes as input C code and the desired structure of the memory abstract domain. The two analysis variants were applied to a set of over 15 micro-benchmarks, similar to the code fragment in Fig. 1. We verify memory safety properties, such as the absence of null pointer dereferences, as well as structural assertions (annotated in the code). In Fig. 8, we report on some representative analysis results relevant to questions in this paper. The C programs considered consist of data structure-manipulation routines (e.g. insertion, deletion, search) for lists and trees either called sequentially or interleaved. They can all be analyzed using a monolithic domain. First, we note that importantly the combined analyses retain the same level of precision as the monolithic analyses in terms of the number of properties that can be proven (column #P). For each program, the number of properties proven on the first line (monolithic) is the same as the number proven on the subsequent lines (various combinations). The key part of the combined analysis is the interface between sub-memories. Its necessity is demonstrated by the ratio of read operations that cross the sub-memories in the combined analyses (column #RA over #R).

Next, we consider the relative efficiency of the various memory abstract domain combinations with respect to the monolithic version. Regardless of configuration, the MemCAD analyzer computes for each program point, a finite disjunction of abstract memories. We first observe that the use of a combined domain does not introduce an extra combinatorial factor as the number of disjuncts is the same for the monolithic and the combined analyses (column ∨). To probe into the overhead of our combination functor, we considered in search_list_tree.c decomposing the memory abstract domain into list-and tree-specific regions (I<list> I<tree>). In this case, the list and tree do-mains are instantiations of the same generic, parametric separating shape graph domain. Thus, this instantiation pays for the overhead of the separating combination without the benefit of an optimized sub-domain. We observe that there is an overhead, but it seems acceptable given that the separating combination offers the possibility of replacing the sub-domains with specialized and optimized versions (a ratio of 110%-120% in the two instances shown here).

The win with our separating combination functor comes from applying it with an optimized sub-domain. In the variants with B • • • , we use a bounded data structure domain to efficiently manage the bounded part of the memory (e.g. the top activation record in the call stack). This sub-domain is implemented efficiently knowing that it only needs to abstract bounded data structures. From Fig. 8, we see that separating out the bounded part of memory into a more efficient specialized domain is highly effective-noticeably decreasing the overall analysis times despite the overhead of combination (a ratio of around 60% in all cases).

Related work

The first important abstract domain combination operation to be introduced is the reduced product [START_REF] Cousot | Systematic design of program analysis frameworks[END_REF], which has enabled constructing very expressive abstract domains from simpler ones. Intuitively, a property is decomposed into a conjunction of (possibly radically different) basic properties. This construction was applied to a wide range of analyzers, including ASTRÉE [START_REF] Blanchet | A static analyzer for large safety-critical software[END_REF], where a large set of numerical abstract domains exchange information over a chain of reduced products [START_REF] Cousot | Combination of abstractions in the astrée static analyzer[END_REF]. The benefit of reduced product is even greater for libraries of abstractions with a common interface such as APRON [START_REF] Jeannet | Apron: A library of numerical abstract domains for static analysis[END_REF]. It was also used to describe the Nelson-Oppen procedure [START_REF] Cousot | The reduced product of abstract domains and the combination of decision procedures[END_REF].

Our contribution seeks to simplify abstract domain construction, while allowing greater expressiveness. It exploits separation [START_REF] Reynolds | Separation logic: A logic for shared mutable data structures[END_REF], albeit in a different way than the numerous shape analyses that exploit it in the definition of their summarization predicates [START_REF] Distefano | A local shape analysis based on separation logic[END_REF][START_REF] Berdine | Shape analysis for composite data structures[END_REF][START_REF] Chang | Relational inductive shape analysis[END_REF]. In these analyses, separation permits (hopefully all) updates to be handled as strong updates, which is crucial for both precision and efficiency. Our analysis exploits separation so as to combine independent memory abstract domains, so as to achieve at least the same precision and better efficiency by delegating the abstraction of particular data structures to the most appropriate sub-domains. Note that the subdomains may (and in all the examples shown in this paper, do) also make use of separation as the aforementioned analyses. In [START_REF] Yahav | Verifying safety properties using separation and heterogeneous asbtractions[END_REF], separation was used to represent distinct heap regions using heterogeneous abstractions, yet this work relies on code specifications transformed into sub-problems handled by different abstractions, and proceeds by verification, although our combinator allows inference of invariants.

Other combinations of abstractions have been proposed so as to enhance memory analyses. In particular, [START_REF] Lee | Program analysis for overlaid data structures[END_REF] presents an approach that uses classical conjunction together with zone variables to relate corresponding regions. Moreover, [START_REF] Dragoi | Local shape analysis for overlaid data structures[END_REF] combines formulae by distinguishing per-field and per-object separating conjunctions. In [START_REF] Manevich | Shape analysis by graph decomposition[END_REF], sets of sub-graphs are used to represent properties about non-correlated data structures and to realize a gain in performance. These analyses are based on problem specific de-compositions while our domain combinator is generic, in the sense that it does not make any assumptions on the way the memory properties are represented in the sub-domains.

In previous work [START_REF] Toubhans | Reduced product combination of abstract domains for shapes[END_REF], we proposed a reduced product for memory abstractions as a generic abstract domain combinator. This combinator does not rely on separation and provides a different form of separation of concerns than our separating combinator: in [START_REF] Toubhans | Reduced product combination of abstract domains for shapes[END_REF], sub-domains express a collection of properties of the same structure whereas the separating conjunction operator combines domains representing distinct structures. Moreover, we introduced a hierarchical memory abstraction to abstract structures allocated inside other structures [START_REF] Sotin | Hierarchical shape abstraction of dynamic structures in static blocks[END_REF]; in that work the whole memory is abstracted in the main domain, and a sub-domain describes nested structures. These combinators are implemented as ML functors in the MemCAD analyzer and can be used together (although assessing such compositions is beyond the scope of this paper).

Conclusion

In this paper, we introduced a combinator for separately conjoining memory abstract domains, enabling composite analyses that are precise, efficient, and flexible. Our proposal enables a separation of concerns when designing static analyses that need to deal with complex data structures, as very different domains can be combined to abstract disjoint memory regions. A natural extension of our study would be to integrate other memory abstractions, as found in 3-valued logic shape analyses [START_REF] Sagiv | Parametric shape analysis via 3-valued logic[END_REF][START_REF] Arnold | Combining shape analyses by intersecting abstractions[END_REF][START_REF] Ferrara | TVLA+ : TVLA and value analyses together[END_REF], into our framework.

(a) Abstract memory state before line 11 B L T

 11L &h &e &x β 3 &t &r

memory state after line 24 Fig. 2 .

 242 Fig. 2. Two combined abstract memories inferred during the analysis

  a) Abstract memory m ♯ b &r = 0x...a16 &t = 0x...a12 &x = 0x...a8 &e = 0x...a4 &h = 0x...a0 0x0 0x...d0 0x0 0x...c0 0x...b0 (b) Concrete memory m b ν b :

Fig. 4 .

 4 Fig. 4. Separating shape graph abstract domain, parameterized by list inductive definition: (m l , ν l ) ∈ γ M ♯

Fig. 5 .

 5 Fig. 5. List inductive definition rewriting rule

  0 ) , (β c 1 , λ 1 )} (a) Combined abstract memory (m ♯ b , m ♯ l , i ♯ ) &r = 0x...a16 &t = 0x...a12 &x = 0x...a8 &e = 0x...a4 &h = 0x..Concrete memory m b ⊎ m l

  l can be passed as optional argument to compare M ♯

	Filename	MAD	#P ∨	t(s)	% tCF(s) tSD(s) #R #RA
	insert_remove.c	I<list>	3 2.09 0.248 basis	-	0.174 230	-
	(158 LOC)	B I<list>	3 2.09 0.151 60 0.035 0.055 230	16
	balancing.c	I<tree>	3 2.56 0.501 basis	-	0.376 314	-
	(188 LOC)	B I<tree>	3 2.56 0.323 64 0.068 0.125 314	72
	search_list_tree.c	I<list,tree>	5 3.40 0.330 basis	-	0.286 172	-
	(138 LOC)	I<list> I<tree>	5 3.40 0.364 110 0.031 0.292 172	48
		B I<list,tree>	5 3.40 0.194 59 0.035 0.098 172	70
		B I<list> I<tree> 5 3.40 0.231 70 0.071 0.113 172	70
							.
							2

http://www.di.ens.fr/~rival/memcad.html

⋆ The research leading to these results has received funding from the European Research Council under the FP7 grant agreement 278673, Project MemCAD and the United States National Science Foundation under grant CCF-1055066.

a) Syntax of l-value and r-value expressions

If we consider the analysis of the memory allocation at line 11 in Fig. 1, the choice is guided by C types: the created cell has type int which is not recursive, and thus it will likely never require summarization. Therefore, the cell creation can be handled by any sub-memories without any loss in precision. As sub-domain M ♯ b is more lightweight than M ♯ l in terms of computational cost, it should abstract the new cell. Then, invoking new M ♯ b M ♯ l deriving from rule NEW1 to the combined memory of Fig. 6(a) returns symbolic name (M ♯ b : α a 5 ) and the following combined abstract memory:

While not being critical for soundness, such empirical hints are important to avoid either a loss of precision or a slowdown in the analysis.

Evaluation of l-value and r-value expressions

We consider the abstract transfer functions handling operations such as assignments and tests. These operations involve l-values l ∈ L M ♯ and r-values r ∈ R M ♯ . Their syntax (shown in Fig. 7(a)) includes classical forms of expressions encountered in a C-like language (structure fields, dereferences, address of, etc.). In this section, we define a mechanism for evaluating l-value and r-value expressions. More formally, the evaluation of an l-value l in abstract memory m ♯ returns a pair L M ♯ l m ♯ = (α, f) consisting of a symbolic name α and a field f such that α + f denotes the address represented by l . Similarly, the evaluation of a r-value r returns an symbolic expression R M ♯ r m ♯ = e that denotes the value represented by r . A symbolic expression e ∈ E M ♯ is either of the form α + f (where α ∈ N M ♯ and f ∈ F) or a concrete value v ∈ V.

Evaluation algorithm. The computation of L M ♯ . and R M ♯ . proceeds by induction over the expressions syntax as shown in Fig. 7(b), assuming a read operation read M ♯ is provided by memory abstract domain M ♯ , so as to "extract" the contents of a cell at the abstract level: partial function read M ♯ inputs a symbolic name α representing the base address of a concrete block, a field f and an abstract memory state m ♯ , and returns a symbolic expression representing the contents of that field. It may also fail to identify the cell and is then undefined (this may happen in a combined memory abstract domain when reading a cell in the "wrong" sub-memory). In some memory abstract domains (such as the separating shape graph domain presented in Example 2), read M ♯ may need to perform unfolding [START_REF] Chang | Relational inductive shape analysis[END_REF] and thus, return a finite set of disjuncts, however this issue is orthogonal to the present development, so we leave it out here. Overall, it should satisfy the following soundness condition:

Read operation in the combined domain. To read a cell at address

Therefore, the read operation derives from the following rule:

The symmetric rule READDIRECT2 is shown in Appendix A.2. It may turn out that the cell at address (M ♯ 1 : α 1 ) is abstracted in sub-memory m ♯ 2 in which case rule READ-DIRECT1 cannot be applied. In fact, by the separation principle (Section 3.2), a cell is represented in exactly one sub-memory. To cope with this issue, the reading operation can retrieve the cell by looking for a symbolic name of sub-domain M ♯ 2 that is bound to α 1 by the abstract interface. In such cases, the definition of

Example 4 (An evaluation across sub-memories). We consider the evaluation of the right hand side e -> data of assignment at line 12 in Fig. 1 on the following combined abstract memory that is computed by the analysis after assignment at line 11 (assignment is treated in Section 4.3).

First, variable e is replaced by symbolic name (M ♯ b : α a 1 ) denoting its address and its content is evaluated to (M ♯ b : β c 1 ). Then, reading cell at address (M ♯ b :

b as the cell is actually abstracted in M ♯ l . Therefore, the reading operation retrieves that cell at address (M ♯ l : λ 1 ) + data, using the equality (β c 1 , λ 1 ) ∈ i ♯ . Finally, the evaluation ends up with symbolic r-value (M ♯ l : λ 3 ).

Abstract transfer function for assignment

The analysis requires a set of abstract transfer functions handling operations such as assignment and test that need to evaluate l-value and r-value expressions [START_REF] Chang | Modular construction of shape-numeric analyzers[END_REF]. Among those, the assignment is arguably the most sophisticated one, thus we describe only this operation here. The classical analysis of assignment l = r shown in [START_REF] Chang | Modular construction of shape-numeric analyzers[END_REF] proceeds as follows:

(1) the left hand side is evaluated to a pair L M ♯ l m ♯ = (α, f) representing the address of the cell that will be updated; (2) the right hand side is evaluated to a symbolic expression R M ♯ r m ♯ = e representing the written value; and (3) the cell is updated in the abstract level, using the abstract cell write operation write M ♯ provided by the memory abstract domain M ♯ . Intuitively, write M ♯ (α, f, e, m ♯ ) returns an abstract memory where the cell at address α + f has been updated to e. To state the soundness of this operation, we extend a valuation ν to cope with symbolic expressions in a natural way by defining ν(α + f)

Therefore, write M ♯ satisfies the condition:

Cell write operation in a combined domain. A simple case occurs when left and right hand sides are both evaluated in the same sub-memory, in which case the cell write operation simply lifts computation to the corresponding sub-domain. However, a trickier case occurs when l-value and r-value are evaluated to different sub-memories, such as ((M ♯ 1 : α 1 ), f) and (M ♯ 2 : β 2 ) + g. In this case, the cell writing is performed in m ♯ 1 as the cell requiring update is abstracted there. However, to avoid losing precision, the analysis needs a symbolic expression in m ♯ 1 to relate the new content. Therefore, two cases may be encountered:

-

by the abstract interface, in which case

is defined following the rule:

β 2 is not bound in the abstract interface, in which case a fresh variable

is defined following the rule: In this section, we give the rules for defining abstract transfer functions of a combined memory abstract domain M ♯ 1 M ♯ 2 , from the abstract transfer functions of memory abstract sub-domains M ♯ 1 and M ♯ 2 .

A.1 Cell creation operation

In a combined domain, the cell creation should be handled by exactly one domain (to avoid violating the separation principle). Therefore, depending on which submemory is chosen to account for the new cell, we give two definitions for the cell creation operation, that derives from the following rules:

The read operation (Section 4.2) extracts the content of a cell in the abstract level. In a combined domain, cell read operation first attempts to extract the content of a cell in the sub-memory where the symbolic name representing its address belongs. Therefore, the cell read operation is first defined by the two following rules:

β 2 ) + g However, cell read operation of sub-domains may fail. In such cases, the cell read operation attempts to retrieve the cell using the abstract interface. It is then defined by the two rules:

The analysis uses the cell write operation (Section 4.3) to compute post-condition of assignments. It updates the content of a cell in the abstract level. In a combined domain, several cases may be encountered depending on which sub-memory belong the address of the updated cell and the written content. When both are in the same sub-memory, the cell writing operation simply lifts the sub-domain operation:

When the written content is a value v, the cell reading operation is defined by the two following rules:

The four following rules define read operation when the address of the updated cell and the written value are in different sub-memories.


Michel A Kinsy
email: mkinsy@mit.edu

Dusan Majstorovic

Pierre Haessig

Jason Poon

Nikola Celanovic

Ivan Celanovic

Srinivas Devadas

High-speed real-time

teaching and research institutions in France or abroad, or from public or private research centers.

INTRODUCTION

Power electronics is one of the key technologies enabling wider proliferation of renewable energy generation and realization of the smart grid vision. Power electronics could potentially reduce overall electricity consumption by more than 30% [START_REF] Fed | Power electronics system integration-a cpes perspective[END_REF]. In order for power electronics to reach this point, advancements are needed in the area of Electronic Design Automation (EDA) tools, among others. Design automation could significantly reduce development cycles, improve reliability, and accelerate the development of more complex systems. In particular, we believe that an integrated EDA tool would immensely benefit the area of automated control testing and rapid design prototyping.

In this paper, we propose a new software/hardware co-design EDA platform for comprehensive testing and validation of power electronics controller hardware, firmware, and software performance by means of high-fidelity, real-time emulation of power electronics in Hardware-in-the-Loop (HiL) configuration. In HiL testing configuration, the power electronics converter is replaced by an ultra-fast real-time emulator that interacts with the controller via high-speed physical input/output interfaces. From the controller point of view, the emulation is so seamless that there is no distinction between the real-time control of the physical plant and the hardware emulator. The paper is organized in five sections. Section 2 frames the challenges facing the design automation and testing of power electronics. Section 3 describes the proposed framework for real-time hardware emulation. Section 4 compares the fidelity of the proposed real-time emulator with the real power electronics system, and presents two more design examples. Section 5 summarizes the paper.

DESIGN REQUIREMENTS FOR HiL POWER ELECTRONICS

Benefits of Hardware Emulation for Power Electronics

Today, power electronics engineers mostly rely on off-line simulations in the early design stage, and on hardware prototypes-low voltage simulators-in the final stages of the design and testing. However, off-line simulations are generally slow and only provide a certain level of functional faithfulness, especially when modeling embedded controller and its interactions. Hardware emulation in HiL configuration enables more realistic testing while reducing the complexity and cost. The key benefits of the real-time emulation for HiL testing are: (1) accelerated testing and validation; (2) reduced testing time needed in the lab; (3) simulation of all operating points and scenarios that are difficult or impossible to recreate with a real system (4) fault injection capability; (5) real-time access to all signals that are difficult to measure in a real system.

Hardware Emulation: A Known Design Concept in Design Automation

The automotive industry has been using HiL simulation as a ubiquitous tool for testing the engine control unit (ECU). Connecting an ECU to a real-time simulator of a car enables exhaustive testing of ECU. In computer engineering, hardware emulation, or in-circuit emulation, is used in processor design by using another system (hardware emulator) that imitates the behavior of the system under test. In power electronics, replacing the power converter, grid, and electromechanical components with a real-time digital emulation takes high-power hardware out of the testing environment with minimal loss of fidelity (from the controller point of view). However, high-fidelity testing of power electronics requires a real-time emulation system with: (1) ultra-low latency and high-speed simulation (∼1µs); (2) ability to simulate switched and nonlinear systems; (3) flexibile modeling; (4) ease of use, and variable levels of modeling abstractions. Most HiL simulators, based on off-the-shelf processors, exhibit large latencies on the order of 50µs. Yet, power converters operate at switching frequencies of ∼10kHz, thus limiting the fidelity and applicability of HiL platforms based on the standard processors.

HiL SYSTEM ARCHITECTURE

We present a new design automation framework based on a unified software/hardware platform that spans the design space from off-line simulation and real-time hardware emulation, to design prototyping, and testing. The proposed software simulation platform is used for offline tasks, such as power electronics converter modeling, analysis, and optimization. System simulations can automatically be ported to the hardware platform that can serve as an accelerator. In addition, the hardware platform is used for real-time emulation and rapid system prototyping. Our approach to high-speed, low-latency simulation of power electronics is based on a switched hybrid system framework, which is suited for modeling of power electronics, and also lends itself to digital architecture implementation [START_REF] Senesky | Hybrid modelling and control of power electronics[END_REF]. The real-time hardware emulator system consists of two main components:

• Application software: including a schematic editor, circuit compiler, and emulation controller;

• Custom-designed multicore hardware system: including real-time emulation processors with fast analog/digital input/output interfaces.

Schematic

Modeling Approach: Switched Hybrid Automaton

The proposed switched hybrid system approach to power electronics converter modeling relies on piecewise linear passive elements, piece-wise linear switches, current and voltage sources (both controlled and idependent). The switched hybrid system model is given in the state space form, as:

ẋ(t) = A q x(t) + B q u(t) (1)
where x(t) ∈ X ⊂ R n is the continuous state space vector, A q ∈ R n×n ; B q ∈ R n×m ; and u ∈ R m is the input vector. Any discrete state of the circuit belongs to a finite set Q = {q 1 ..q n } and further defines the given state space representation. Every discrete state q i therefore has a unique dynamic behavior associated with it that defines the operation of the circuit. In this framework one can also define a mode, denoted m q , where q ∈ Q, is the operation of the system defined by given state space ẋ(t) = A q x(t) + B q u(t) and a given q.

Definition 1 (Switched Hybrid Automaton) A switched hybrid system is a collection H = (Q, X, f, E, G) where:

Q = {q 1 ..q n } is set of discrete states, X ⊆ R n is the continuous state space; f : Q → (X → R n )
assigns to every discrete state continuous vector field on X; E ⊆ Q × Q is a collection of discrete transitions; G : E → 2 X assigns each e = (q, q ) ∈ E a guard.

The state space representation of hybrid automaton modes, as defined in Equation 1, can be discretized. We use the exact discretization method via state-transition matrix. The discretized state space system matrices, for a given mode are given as:

ẋ(k + 1) = A d(q) x(k) + B d(q) u(k) (2)
y(k) = C d(q) x(k) + D d(q) u(k) (3)
g(k) = C gd(q) x(k) + D gd(q) u(k) (4)
where k is the discrete time, y is the output vector, g is the guard vector (it is treated as the output vector). In the discretized form the set of matrices {A d(q) , B d(q) , C d(q) , D d(q) , C gd(q) , D gd(q) } defines the dynamic behavior of the system.

Application Software

Application software is the interface for specifying the system that is emulated in hardware. After the system is specified in the schematic editor, the circuit compiler analyzes the circuit, and extracts the full switched hybrid system representation, followed by compilation and linking of the model into the processor executable binary file. The simulation controller loads the binary file into the processor and provides control of the simulation via start/stop commands, etc. and configures the "in-circuit" probing.

Application Software Implementation

The software environment comprises three layers: (1) the power electronics modeling layer, (2) formulation and analysis layer, and (3) the synthesis and simulation layer. In the software domain, we focus on abstraction, structure, and modularity. Figure 1(a) shows the software modules and the data flows. The first layer consists of the schematic editor and the circuit netlist abstractor. The Schematic Editor library components include piece-wise linear circuit elements (e.g. resistors, inductors, capacitors), machine models, semiconductor devices (e.g. diodes and IGBTs), independent and controlled sources, contactors and predefined power electronics switching blocks(e.g., a three-phase two-level voltage source inverter etc.) and control blocks. Given a power electronics circuit, the Netlist Extractor module generates a list of components, values, and connectivity. The hybrid model formulation is done through the System Synthesizer module, which generates the set of state space matrices, modes, transition equations, guards, etc. The synthesizer output files can be used by the offline simulator, or by the realtime controller to be mapped onto the the hardware. The Offline Simulator module uses hybrid model formulation (both preset and actively user controlled), and outputs time-domain signals via the Virtual Oscilloscope module. The Real-Time Control Graphic User Interface module allows user to run the model in real-time on the hardware, and to control the emulation manually or via script.

Multicore Hardware Architecture

We develop a domain-specific digital processor architecture that consists of two sets of computational elements: high-speed, low-latency, dynamic system state space solver (discretized with fixed timestep), vector cores, and reduced instruction set computing (RISC) cores that control simulation and input/output access. The architecture guarantees combined real-time emulation latency and execution times of 1µs.

Hardware Implementation

Figure 1(b) shows the macro-view of the architecture. Processing cores are connected via an irregular, two dimensional mesh network of bufferless reconfigurable routers. The number of any class of processing cores (e.g., vector-machines, DSPs, RISC cores) is expandable, and the interconnect network is scalable. The architecture uses two techniques to achieve parallelism: namely, Single Program-Multiple Data (SPMD), where the two autonomous vector processors can simultaneously execute the same program on different data sets, and Multiple Program-Multiple Data (MPMD) style approach, where the different processors and micro-processors simultaneously operate on independent programs. The architecture comprises: two four-lane chained vector-machine cores for fast and parallel matrix computation [START_REF] Asanovic | Vector microprocessors[END_REF][START_REF] Bhandarkar | Vax vector architecture[END_REF], two RISC cores, two digital signal processors (DSP), a 16-bit programmable microprocessor, an 8-bit programmable microprocessor, a bank style main memory, with no cache for deterministic data access [START_REF] Cogswell | A cacheless architecture for real time systems[END_REF], and two memory controllers for off-chip communication.

The performance of the proposed hardware architecture is verified on a Xilinx ML506 FPGA development board, with a custom-designed analog/digital I/O board for the controller under test and user outputs.

Our current design roughly uses 90% of the slices and BRAMs on the FPGA, and runs at 200M Hz.

EXPERIMENTAL RESULTS AND APPLICATION EXAMPLES

To demonstrate the fidelity and the versatility of our full electronic systems design and automation approach, and our integrated software/hardware system solution, we present Hardware-in-the-Loop simulations of three representative systems: namely, a variable speed induction motor drive, a utility grid connected photovoltaic converter system, and a hybrid electric vehicle motor drive.

  Software/Hardware Architecture for Power Electronics Emulation and Rapid Prototyping.

  Custom-designed Multicore Architecture for Real-Time Hybrid Applications (MARTHA).

Figure 1 :

 1 Figure 1: HiL Software/Hardware System Architecture.

SUMMARY AND CONCLUSIONS

This work proposes an industrial grade real-time emulation platform based on a novel digital processor design and a software tool chain that makes it flexible, easy to use, and scalable. The proposed platform brings a true emulator performance to the control design and test engineers desks. It enables a highfidelity (with 1µs latency and simulation time-step), safe, and fully realistic testing and validation of the most detailed aspects of power electronics systems.

Variable Speed Induction Motor Drive

The variable speed drive consists of a three-phase voltage source, a three-phase diode bridge rectifier, a DC-link, a three-phase two-level voltage-source inverter, an output filter and an induction machine. To illustrate the fidelity of our real-time digital emulation platform, we run in parallel an industrial grade open-loop variable speed drive, ABB ACS-150, and our real-time hardware emulator, both driven from the same controller. Figure 2 shows the system comprising three-phase diode rectifier and three-phase two-level IGBT inverter. Figure 3 shows the experimental setup, where the same controller is used for both the real system and the real-time emulated system. Measured waveforms on both the real system and the emulator are shown in Figure 4(a) with almost one-to-one matching. Emulator response latency is measured to be less than(1.3µs), as shown in Figure 4(b).

Utility Grid Connected Photovoltaic Converter System

To illustrate, that beyond the real-time high-fidelity, our EDA environment also provides support for flexible modeling, design, prototyping, and HiL testing for a wide range of applications, we present another example system: a grid connected photovoltaic converter system. Figure 5(a) shows a two-stage utility grid connected photovoltaic converter model, that consists of a photovoltaic panel module, boost converter, a three-level NPC inverter, an input filter, and a grid. Figure 5(b) shows voltages V ab and V bc on channels 1 and 2, respectively.

Hybrid Electric Vehicle Motor Drive

In recent years, we have witnessed a significant increase in the development efforts focused on hybrid and electric vehicle drivetrains. Being a safety critical application, these system require ever increas- Figure 6 shows a simplified voltage-source inverter model of the system, with switching frequency of 4 kHz.


Xavier Rival
email: rival@di.ens.fr

Antoine Toubhans
email: toubhans@di.ens.fr

Bor-Yuh Evan Chang

Construction of Abstract Domains for Heterogeneous Properties (Position Paper) ⋆

The aim of static analysis is to infer invariants about programs that are tight enough to establish semantic properties, like the absence of run-time errors. In the last decades, several branches of the static analysis of imperative programs have made significant progress, such as in the inference of numeric invariants or the computation of data structures properties (using pointer abstractions or shape analyzers). Although simultaneous inference of shape-numeric invariants is often needed, this case is especially challenging and less well explored. Notably, simultaneous shape-numeric inference raises complex issues in the design of the static analyzer itself. We study the modular construction of static analyzers, based on combinations of atomic abstract domains to describe several kinds of memory properties and value properties.

Static analysis to infer heterogeneous properties. Static analysis by abstract interpretation [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF] utilizes an abstraction to over-approximate (non-computable) sets of program states, using computer-representable elements, that stand for logical properties of concrete program states. As an example, for numerical properties, the interval abstract domain [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF] uses constraints of the form n ≤ x and x ≤ p to describe possible values of variable x, where n, p are scalars.

To construct a static analyzer capable of inferring sound approximations of program behaviors, one designs an abstract domain, which consists of an abstraction, and abstract operations for sound post-condition operators, join and widening:

1. An abstraction is defined by a set of abstract elements A and a concretization function γ : A → P(C), which maps each abstract property a into the set of concrete elements γ(a) that satisfy it. The set A of abstract elements will be assumed to be defined by a grammar of admissible logical predicates (e.g., for intervals, 3. Abstract join computes an over approximation of union and widening [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF] enforces the termination of abstract iterates for the analysis of loops. The combination of post-condition operators and widening operators allows us to define a sound static analyzer [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF].

a(∈ A) ::= a ∧ a | n ≤ x | x ≤ p). 2. A post-condition operator is a function f : A → A which
In the following, we discuss the design of an abstraction able to handle heterogeneous properties, about both data-structures and values. For instance, Figure 1 shows a couple of concrete states containing lists of numbers that are all positive except for the first one, which belongs to interval [-10, 0]: our goal is to engineer abstract domains able to express such properties, yet can be applied to many static analysis problems.

Abstraction of dynamic memory properties. For instance, a memory abstract domain consists of a set of predicates describing memory regions, together with operators for the analysis of memory operations (look-ups, assignments) and widening. XISA [START_REF] Chang | Shape analysis with structural invariant checkers[END_REF][START_REF] Chang | Relational inductive shape analysis[END_REF] relies on points-to predicates, inductive predicates and segment predicates. A simplified version of this abstraction, where the only inductive predicates and segments that are considered are lists boils down to the following: symbolic variables α, α ′ , . . . denote values and addresses

m(∈ M) ::= m * m separating conjunction of predicates | α • f → α ′ cell field f at address α containing value α ′ | list(α) a list at address α | list(α ′ ) = * list(α)
a list segment starting at α and ending at α ′

The XISA [START_REF] Chang | Shape analysis with structural invariant checkers[END_REF] implementation actually represents a larger set of predicates, with arbitrary inductive definitions (including trees, doubly-linked lists and others). Other analysis frameworks utilize other sets of logical properties, such as, e.g., TVLA [START_REF] Sagiv | Solving shape-analysis problems in languages with destructive updating[END_REF], which is based on reachability predicates.

Adding tracking for value properties, and departing from monolithic abstract domains.

Once an abstraction has been defined for memory states, it is natural to extend it with value properties, so as to let the analysis infer constraints over both the structure of data and their values. A straightforward way to achieve this, and to add interval constraints over values is to extend the definition of abstract elements by m ::

= . . . | m ∧ α ≤ n | m ∧ n ≤ α | .
. .. However, this implies the abstract operations (post-condition operators, join and widening) have to be extended so as to deal with both structures and value properties, at the same time: therefore abstract operations are bound to become overly complex. Moreover, this approach is awkward, as it does not build upon existing abstract operations of value abstractions such as intervals [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF] or octagons [START_REF] Miné | The octagon abstract domain[END_REF], which means it will not easily benefit from the efficient algorithms designed to infer such properties (the same also applies to the memory abstraction). Besides, it makes it harder to switch from one value abstraction to another at a later point, hence reducing the flexibility of the analysis.

In the following, we advocate a modular abstract domain design, which: separates concerns in the abstract domain designs; reuses existing abstract domains algorithms; allows one to tune distinct parts of the abstractions independently. Such design has been extensively used in the ASTR ÉE static analyzer [START_REF] Blanchet | A static analyzer for large safety-critical software[END_REF], which makes intensive use of reduced product [START_REF] Cousot | Systematic design of program analysis frameworks[END_REF] among other abstract domain combination techniques [START_REF] Cousot | Combination of abstractions in the astrée static analyzer[END_REF]. This design contributed not only to the precision and efficiency of the analysis, but also to making it easier to extend [START_REF] Cousot | Combination of abstractions in the astrée static analyzer[END_REF].

Abstraction of value properties, and combined abstract domain. To achieve a modular abstract domain design, we set up a different abstract domain V that will only track value properties (and not memory layout as the previously defined M does), and define a new abstract domain S for states that combines both:

m(∈ M) ::= . . . defined as before v(∈ V) ::= true | v ∧ v | α ≤ n | n ≤ α value predicates s(∈ S) ::= m ∧ v conjunction of sub-properties
In essence, S defines a reduced product [START_REF] Cousot | Systematic design of program analysis frameworks[END_REF] of the memory abstraction M and value abstraction V. As such, it completely separates memory and value abstraction concerns, which makes the abstract domain fully modular [START_REF] Toubhans | An abstract domain combinator for separately conjoining memory abstractions[END_REF]. Indeed, both sub-components can be implemented in distinct ML modules, and S is defined as a ML functor. In practice, this functor should ensure that the symbolic variables used in the value abstraction are consistent with the memory cell contents and addresses symbols defined in the memory abstraction (thus it implements a co-fibered abstract domain [START_REF] Venet | Abstract cofibered domains: Application to the alias analysis of untyped programs[END_REF], which essentially generalizes the notion of reduced product).

Both concrete states of Figure 1 can be abstracted by

α → α 0 * α 0 • n → α 1 * α 0 • d → α ′ 0 * lpos(α 1 ) ∧ α = &x ∧ -10 ≤ α ′ 0 ∧ α ′ 0 ≤ 0,
where inductive definition lpos describes all lists of positive numbers.

Separate combination of memory abstractions. So far, we combined abstract domains capturing distinct sets of properties. Yet, this abstract domain decomposition approach can be pushed further. As an example, ASTR ÉE [START_REF] Blanchet | A static analyzer for large safety-critical software[END_REF] relies on a decomposition of the numerical abstract domain into simpler abstractions that handle specific sets of properties. Likewise, a similar approach can be applied to the memory abstraction part. One approach to do this is to split concrete heaps and apply distinct memory abstractions to disjoint regions [START_REF] Toubhans | An abstract domain combinator for separately conjoining memory abstractions[END_REF]:

m(∈ M) ::= m 0 * m 1 where m 0 ∈ M 0 ∧ m 1 ∈ M 1 m 0 (∈ M 0 ) ::= . . .
defines a 1st memory abstract domain, e.g., for lists m 1 (∈ M 1 ) ::= . . . defines a 2nd memory abstract domain, e.g., for arrays This construction allows one to apply parsimoniously expensive memory abstractions to the memory regions that require them, while lighter weight abstractions can be used for simpler structures. This results in better control of the analysis complexity. A cost is that the analyzer now has to resolve memory fragments across sub-domains, and to also select which memory fragment is the most adequate to account for each memory allocation.

Reduced product of memory abstractions. Likewise, one can design a reduced product [START_REF] Cousot | Systematic design of program analysis frameworks[END_REF] of memory abstract domains [START_REF] Toubhans | Reduced product combination of abstract domains for shapes[END_REF]:

m(∈ M) ::= m 0 ∧ m 1 where m 0 ∈ M 0 ∧ m 1 ∈ M 1
Such a composed abstraction is adequate when considering overlaid data structures [START_REF] Lee | Program analysis for overlaid data structures[END_REF] (such as lists or trees of objects with a common field pointing to class methods) and separates the concerns of analyzing each aspects of the structures. In turn, it imposes on the analysis the burden to let logical predicates represented in one sub-domain be usable to refine the computations done in the other sub-domain.

Modular abstract domain design. A modular abstract domain significantly simplifies the design of static analyzers while offering additional flexibility and control. The cost for this benefit is the innovation needed to design these more complex and general abstract domain combinators, but this cost is quickly amortized with the ability to reuse these combinators to realize arbitrary static analyzer configurations.

Fig. 1 .

 1 Fig. 1. Heterogeneous property abstraction

⋆ The research leading to these results has received funding from the European Research Council under the FP7 grant agreement 278673, Project MemCAD, from the ARTEMIS Joint Undertaking under agreement no 269335 (ARTEMIS Project MBAT) (See Article II.9 of the Joint Undertaking Agreement), and the United States National Science Foundation under grant CCF-1055066.