Hugo Illous

Matthieu Lemerre

Xavier Rival

Interprocedural Shape Analysis Using Separation Logic-based Transformer Summaries

Shape analyses aim at inferring semantic invariants related to the data-structures that programs manipulate. To achieve that, they typically abstract the set of reachable states. By contrast, abstractions for transformation relations between input states and output states not only provide a finer description of program executions but also enable the composition of the effect of program fragments so as to make the analysis modular. However, few logics can efficiently capture such transformation relations. In this paper, we propose to use connectors inspired by separation logic to describe memory state transformations and to represent procedure summaries. Based on this abstraction, we design a top-down interprocedural analysis using shape transformation relations as procedure summaries. Finally, we report on implementation and evaluation.

Introduction

Static analyses based on abstractions of sets of states (or for short, state analyses) compute an over-approximation of the states that a program may reach, so as to answer questions related, e.g., to safety (absence of errors or structural invariant violations). By contrast, one may also design static analyses that discover relations between program initial states and output states. In this paper, we refer to such static analyses as transformation analyses. A transformation relation between the initial state and the output state of a given execution can provide an answer to questions related to the functional correctness of a program (i.e., does it compute a correct result when it does not crash and terminates). Another application of such a transformation relation is to let the analysis reuse multiple times the result obtained for a given code fragment (e.g., a procedure), provided the analysis can compose transformation relations. The great advantage of this approach is to reduce the analysis cost, by avoiding to recalculate the effect, e.g., of a procedure in multiple calling contexts. This is known as the relational approach to interprocedural analysis [START_REF] Sharir | Two approaches to interprocedural data flow analysis[END_REF].

However, a major difficulty is to find an accurate and lightweight representation of the input-output transformation relation of each procedure. A first solution is to resort to tables of abstract pre-and post-conditions that are all expressed in a given state abstract domain [START_REF] Cousot | Modular static program analysis[END_REF][START_REF] Calcagno | Footprint analysis : A shape analysis that discovers preconditions[END_REF][START_REF] Bhargav S Gulavani | Bottom-up shape analysis[END_REF][START_REF] Loc | Shape analysis via second-order bi-abduction[END_REF]. However, this generally makes composition imprecise unless very large tables can be computed. A second solution is to build upon a relational abstract domain, namely, an abstract domain that can capture relations across distinct program variables. The transformation between states is then expressed using "primed" and "non-primed" variables where the former describe the input state and the latter the output state [START_REF] Manna | Axiomatic approach to total correctness of programs[END_REF][START_REF] Müller | Precise interprocedural analysis through linear algebra[END_REF][START_REF] Popeea | Inferring disjunctive postconditions[END_REF]. As an example, we consider a procedure that computes the absolute value of input x and stores it into y (for the sake of simplicity we assume mathematical integers):

-Using the intervals abstract domain [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF], we can provide the table [((x ∈ [-5, -1], y ∈]-∞, +∞[) → (x ∈ [-5, -1], y ∈ [START_REF] Bourdoncle | Abstract interpretation by dynamic partitioning[END_REF][START_REF] Bor-Yuh | Relational inductive shape analysis[END_REF])); ((x ∈ [-1, 10], y ∈ ]-∞, +∞[) → (x ∈ [-1, 10], y ∈ [0, 10]))] (this table is obviously not unique); -Using the relational abstract domain of polyhedra [START_REF] Cousot | Automatic discovery of linear restraints among variables of a program[END_REF], we can construct the transformation relation (x = x ∧ y ≥ x ∧ y ≥ -x). We note that, while the expressiveness of the two is not comparable, the latter option is more adapted to compositional reasoning. For instance, given pre-condition -10 ≤ x ≤ -5, the analysis based on a table either returns a very imprecise answer or requires enriching the table whereas the analysis with a relational domain can immediately derive x = x ∈ [-10, -5] (x has not changed) and y ≥ 5.

Such reasoning becomes more complex when considering non-numerical facts, such as memory shape properties. Many works rely on the tabulation approach, using a conventional shape state abstraction [START_REF] Calcagno | Footprint analysis : A shape analysis that discovers preconditions[END_REF][START_REF] Bhargav S Gulavani | Bottom-up shape analysis[END_REF][START_REF] Loc | Shape analysis via second-order bi-abduction[END_REF]. In general, the tabulation approach restricts the ability to precisely relate procedure input and output states and may require large tables of pairs of formulas for a good level of precision. The approach based on a relational domain with primed and non-primed variables has been implemented by [START_REF] Jeannet | A relational approach to interprocedural shape analysis[END_REF][START_REF] Jeannet | A relational approach to interprocedural shape analysis[END_REF] in the TVLA shape analysis framework [START_REF] Sagiv | Solving shape-analysis problems in languages with destructive updating[END_REF]. However, it is more difficult to extend shape analyses that are based on separation logic [START_REF] Reynolds | Separation logic: A logic for shared mutable data structures[END_REF] since a separation logic formula describes a region of a given heap; thus, it does not naturally constrain fragments of two different states. To solve this issue, a first approach is to modify the semantics of separation logic connectors to pairs of states [START_REF] Schaefer | Local reasoning for termination[END_REF]. A more radical solution is to construct novel logical connectors over state transformation relations that are inspired by separation logic [START_REF] Illous | A relational shape abstract domain[END_REF]. These transformations can describe the effect of a program and express facts such as "memory region A is left untouched whereas a single element is inserted into the list stored inside memory region B and the rest of that list is not modified". The analysis of [START_REF] Illous | A relational shape abstract domain[END_REF] is designed as a forward abstract interpretation which produces abstract transformation relations. Therefore, it can describe tranfsormations precisely using separation logic predicates and without accumulating tables of input and output abstract states.

However, this analysis still lacks several important components to actually make interprocedural analysis modular. In particular, it lacks a composition algorithm over abstract transformation relations. Modular interprocedural analysis also needs to synchronize two distinct processes that respectively aim at computing procedure summaries and at instantiating them at a call-site. In this paper, we propose a top-down analysis based on shape summaries and make the following contributions:

in Section 2, we demonstrate the use of abstract shape transformations; -in Section 3 and Section 4, we formalize transformation summaries based on separation logic (intraprocedural analysis is presented in Section 5); -in Section 6, we build a composition algorithm over transformation summaries; in Section 7, we formalize a modular interprocedural analysis; -in Section 8, we report on implementation and evaluation.

Overview

In this section, we study a restricted example to highlight some issues in interprocedural analysis. We consider a recursive implementation of C linked lists, with a couple of procedures shown in Figure 1. The function append takes two lists as arguments and assumes the first one non-empty, it traverses the first list, and mutates the pointer field of the last element. The function double_append takes three lists as arguments (the first one is assumed non-empty) and concatenates all three by calling append. The topic of our discussion is only the invariants underlying this code and their discovery, not the efficiency of the code itself.

State abstraction and analysis. We consider an abstraction based on separation logic [START_REF] Reynolds | Separation logic: A logic for shared mutable data structures[END_REF], as shown, e.g., in [START_REF] Distefano | A local shape analysis based on separation logic[END_REF][START_REF] Chang | Shape analysis with structural invariant checkers[END_REF]. To describe sets of states, we assume a predicate lseg(α 0 , α 1 ) that represents heap regions that consist of a list segment starting at some address represented by the symbolic variable α 0 and such that the last element points to some address represented by α 1 . Such a segment may be empty. For short, we note list(α) for the instance lseg(α, 0x0), which denotes a complete singly-linked list (as the last element contains a null next link). A single list element writes down α 0 • n → α 1 where n denotes the next field offset (we elide other fields). More generally, α 0 → α 1 denotes a single memory cell of address α 0 and content α 1 . Thus &x → α expresses that variable x stores a value α (which may be either a base value or the address of a memory cell). Predicates lseg and list are summary predicates as they describe unbounded memory regions; their denotation is naturally defined by induction. As usual, separating conjunction * conjoins predicates over disjoint heap regions.

Assuming the abstract precondition

&l0 → α 0 * lseg(α 0 , α 1 ) * α 1 • n → 0x0 * &l1 → α 2 * list(α 2 )
, existing state shape analyses [13,6] can derive the post-condition &l0 → α 0 * lseg(α 0 , α 1 ) * α 1 • n → α 2 * &l1 → α 2 * list(α 2 ) by a standard forward abstract interpretation [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF] of the body of append. The analysis proceeds by abstract interpretation of basic statements, unfolds summaries when analyzing reads or writes into the regions that they represent, and folds basic predicates into summaries at loop heads. The convergence of the loop analysis takes a few iterations and involves widening which is often a rather costly operation. The analysis of double_append by inlining follows similar steps. One important note though is that it analyses the body of append twice, namely once per calling context, and thus also the loop inside append. In turn, if double_append is called in several contexts in a larger program, or inside a loop, its body will also be analyzed multiple times, which increases even more the overall analysis cost.

Transformation analysis. Unlike state analyses, transformation analyses compute abstractions of the input-output relation of a program fragment. As an example, given the above abstract pre-condition, the analysis of [START_REF] Illous | A relational shape abstract domain[END_REF] infers relations as shown in Figure 2(a). This graphical view states that the procedure append keeps both summary predicates unchanged and only modifies the middle list element so as to append the two lists. This transformation is formally represented using three basic kinds of relational predicates that respectively state that one region is preserved, that one region is "transformed" into another one, and that two transformations are conjoined at the transformation level. To stress the difference, we write * T for the latter, instead of just * . Although it uses transformation predicates, the analysis follows similar abstract interpretation steps as [START_REF] Distefano | A local shape analysis based on separation logic[END_REF][START_REF] Chang | Shape analysis with structural invariant checkers[END_REF].

Towards modular analysis: composition of transformation abstractions. The first advantage of transformation predicates such as Figure 2(a) is that they can be applied to state predicates in the abstract, as a function would be in the concrete. Indeed, if we apply this abstract transformation to the abstract pre-condition given above, we can match each component of the abstract transformation of Figure 2(a), and derive its post-condition. In this example, the body of each summary is left unchanged, whereas the last element of the first list is updated. The result is shown in Figure 2(b) and it can be derived without reanalyzing the body of append.

While these steps produce a state analysis of the body of double_append, we may want to summarize the effect of this function too, as it may be called somewhere else in a larger program. To achieve this, we need not only to apply an abstract transformation to an abstract state, but to compose two abstract transformations together. Intuitively, this composition should proceed in a similar way as the application that we sketched above. In the case of double_append, the analysis requires case splits depending on whether k1 is empty or not. For brevity, we show only the case where this list is non-empty in Figure 2(c). In general, the composition of two transformations requires to match the post-condition of the first and the pre-condition of the second, and to refine them, using some kind of intersection as shown in Section 6. Another important issue is the summary computation process. Bottom-up analyses strive for general summaries whatever the calling context. However, a procedure may behave differently when applied to other structures (e.g., a binary tree or a doubly linked list), thus the top-down approach which provides information about the calling contexts before they are analyzed seems more natural. However, this means that the analysis should infer summaries and apply them simultaneously, and that the discovery of new calling contexts may require for more general summaries. We describe this in Section 7.

Abstraction of sets of states and state transformations

In the following sections, we restrict ourselves to a small imperative language that is sufficient to study procedure transformation summaries, although our implementation described in Section 8 supports a larger fragment of C. We also only consider basic singly linked lists in the formalization although the implementation supports a large range of list or tree-like inductive data-structures.

Concrete states, programs, and semantics. We write X for the set of program variables and V for the set of values, which include memory addresses. The address of a variable x is assumed fixed and noted &x. Structure fields are viewed both as names and as offsets; they include the null offset (basic pointer) and n, the "next" field of a list element. We let a memory state σ ∈ M be a partial function from variable addresses and heap addresses to values. We write dom(σ) for the domain of σ, that is the set of elements for which it is defined. Additionally, if σ 0 , σ 1 are such that dom(σ 0 ) ∩ dom(σ 1 ) = ∅, we let σ 0 σ 1 be the memory state obtained by appending σ 1 to σ 0 (its domain is dom(σ 0 ) ∪ dom(σ 1 )). If a is an address and v a value, we write [a → v] for the memory state σ such that dom(σ) = {a} and σ(a) = v. A command C is either an assignment, a local variable declaration or a loop (we omit tests and memory allocation out as our procedure summary analysis handles them in a very standard way). A procedure P is defined by a list of arguments and a body (we let function returns be encoded via parameter passing by reference). A program is made of a series of procedures including a main. All variables are local. The syntax of programs is defined by the grammar below: We let the semantics of a command C be a function C T : P(M) → P(M) that maps a set of input states into a set of output states. We do not detail the definition of this semantics as it is standard. In the following, we formalize two abstractions, that respectively describe sets of states and relations over states.

C ::= x = y | x = v | x -> n = y | x = y -> n | C; C | while(x = 0x0){C} | decl x; | f(x 0 , . . . , x k ) P ::= proc f(p 0 , . . . , p k ){C} R ::= P 0 . . . P l proc main(){C} n(∈ N) ::= α (α ∈ A) | &x (x ∈ X) c ::= n 0x0 ( ∈ {=, =}) | n = n h (∈ H) ::= emp | n • f → n | lseg(α, α ) | list(α) | h * S h | h ∧ c (a) Abstract states syntax γH(n • f → n ) = {([ν(n) + f → ν(n )], ν)} γH(emp) = {([], ν)} γH(h 0 * S h 1 ) = {(σ0 σ1, ν) | (σ0, ν) ∈ γH(h 0 ) ∧ (σ1, ν) ∈ γH(h 1 )} γH(h ∧ c ) = {(σ, ν) | (σ, ν) ∈ γH(h ) ∧ ν ∈ γC(c )} (
Abstract states and transformations. The syntax of abstract heaps h ∈ H is shown in Figure 3(a). We let A = {α, α , . . .} denote a set of symbolic variables that abstract heap addresses and values. A symbolic name n ∈ N is either a variable address &x or a symbolic value α. Numerical constraints c describe predicates over symbolic names. An abstract heap (or state) h ∈ H is the (possibly) separating conjunction of region predicates that abstract separate regions [START_REF] Reynolds | Separation logic: A logic for shared mutable data structures[END_REF], which consist either of an empty region emp, or of a basic memory block (described by a points-to predicate n • f → n ), or inductive summaries, and may include some numerical constraints (that do not represent any memory region and only constrain symbolic names). We note * S for separating conjunction over states. The abstract states defined in Figure 3(a) are of a comparable level of expressiveness as the abstractions used in common shape analysis tools such as [START_REF] Distefano | A local shape analysis based on separation logic[END_REF][START_REF] Chang | Shape analysis with structural invariant checkers[END_REF][START_REF] Calcagno | Footprint analysis : A shape analysis that discovers preconditions[END_REF][START_REF] Dudka | Predator: A practical tool for checking manipulation of dynamic data structures using separation logic[END_REF] to verify properties such as the absence of memory errors or the preservation of structural invariants. The concretization of abstract states is shown in Figure 3(b). It uses valuations to tie the abstract names and the value they denote. A valuation consists of a function ν : N → V. We assume the concretization γ C (c ) of a numeric constraint c returns the set of valuations that meet this constraint. Abstract heaps are concretized into sets of pairs made of a heap and of the valuation that realizes this heap. The concretization of summary predicates list and lseg is defined recursively, by unfolding. Indeed, we let γ

H (h 0 ) = {γ H (h 1 ) | h 0 → U h 1 }
, where → U is defined by (cases for list are similar):

lseg(α 0 , α 1 ) → U emp ∧ α 0 = α 1 lseg(α 0 , α 1 ) → U α 0 • n → α 2 * S lseg(α 2 , α 1 ) ∧ α 0 = α 1
Example 1 (Abstract state). The abstract state in Figure 2(b) writes down as:

&l0 → α 0 * S &l1 → α 2 * S lseg(α 0 , α 1 ) * S α 1 • n → α 2 * S list(α 2 )
Assuming both lseg(α 0 , α 1 ) and list(α 2 ) unfold to structures of length one, it concretizes in the same way as: Abstract transformations. Abstract transformations are defined on top of abstract states and rely on specific logical connectors. Their syntax is defined in Figure 4(a). A heap transformation is either the identity Id(h ), which denotes physical equality over pairs of states that are both described by h , a state transformation [h i h o ] which captures input/output pairs of states respectively defined by h i and by h o , or a separating conjunction of transformations t 0 * T t 1 (we write * T to stress the distinction with the state separating conjunction * S). The concretization of transformations is shown in Figure 4(b). It is built upon the previously defined γ H and also utilizes valuations. The most interesting case is that of * T: this connector imposes disjointness not only of the sub-heaps in both the pre-and post-state, but also across them. In this paper, we study only a basic form of the transformation predicate * T although it may be strengthened with additional constraints [16], e.g., to assert that the footprint has not changed or that only specific fields may have been modified. We leave out such constraints as their goal is orthogonal to the focus of this paper. Finally, the analysis uses finite disjunctions of transformations.

&l0 → α 0 * S &l1 → α 2 * S α 0 • n → α 1 * S α 1 • n → α 2 * S α 2 • n → α 3 ∧ α 3 = 0 t (∈ T) ::= Id(h ) | [h h ] | t * T t | t ∧ c (a) Abstract transformations syntax γT(Id(h )) = {(σ, σ, ν) | (σ, ν) ∈ γH(h )} γT([h i h o ]) = {(σi, σo, ν) | (σi, ν) ∈ γH(h i ) ∧ (σo, ν) ∈ γH(h o )} γT(t 0 * T t 1 ) = {(σ0,i σ1,i, σ0,o σ1,o, ν) | (σ0,i, σ0,o, ν) ∈ γT(t 0 ) ∧ dom(σ0,i) ∩ dom(σ1,o) = ∅ ∧ (σ1,i, σ1,o, ν) ∈ γT(t 1 ) ∧ dom(σ1,i) ∩ dom(σ0,o) = ∅} γT(t ∧ c ) = {(σi, σo, ν) ∈ γT(t ) | ν ∈ γC(c )} (
Example 2 (Abstract transformation). The transformation informally described in Figure 2(a) is captured by the abstract transformation below:

t = Id (&l0 → α 0 * S &l1 → α 2 * S lseg(α 0 , α 1 ) * S list(α 2 )) * T [(α 1 • n → 0x0) (α 1 • n → α 2 )]
In the following, we write h 0 → U h 1 when h 0 may be rewritten into h 1 by applying → U to any of its sub-terms. We use this notation for both heaps and transformations. Last, we let → U[α] denote unfolding of a list(α) or lseg(α, . . .) predicate.

4 Procedure summarization.

The semantics of a procedure boils down to a relation between its input states and its output states, thus our first attempt at summaries over-approximates the input-output relation of the procedure. To express this, we introduce the following notation. If f :

P(A) → P(B) is a function and R ⊆ A × B is a relation, we note f R if and only if ∀X ⊆ A, X × f (X) ⊆ R.
Definition 1 (Global transformation summary). A sound global transformation summary (or, for short, global summary) of procedure proc f(. . .){C} is an abstract transformation t that over-approximates C T in the sense that:

C T {(σ i , σ o ) | ∃ν, (σ i , σ o , ν) ∈ γ T (t )}
For example, function append (Figure 1) can be described using a global procedure summary (noted t in Example 2). While this notion of summary may account for the effect of a procedure, it is not adequate to describe intermediate analysis results. As an example, a procedure f is likely to be called in multiple contexts. In that case, when the analysis reaches a first context, it computes a summary t , that accounts for the effect of the procedure in that context, for a given set of procedure input states. When it reaches a second context, it should be able to decide whether t also covers the states that reach the procedure in that second context. Observe that the pre-state of t does not suffice since t may have been computed for some very specific context. Moreover, the left projection of t may not account for some call states encountered so far when these lead to non-termination or to an error in the body of f. To overcome this issue, an over-approximation of the procedure input states observed so far should be adjoined to the global summary:

Definition 2 (Context transformation summary). A sound context transformation summary (or, for short, context summary) of procedure proc f(. . .){C} is a pair (h f , t f ) such that the following holds:

(λ(M ⊆ {σ | ∃ν, (σ, ν) ∈ γ H (h f )})• C T (M )) {(σ i , σ o ) | ∃ν, (σ i , σ o , ν) ∈ γ T (t f )}
Intuitively, Definition 2 asserts that (h f , t f ) captures all the functions such that their restriction to states in h f can be over-approximated by relation t f . Although we do not follow this approach here, the h f component may be used in order to augment summaries with context sensitivity. We note that h f accounts for all states found to enter the body of f so far, even though they may lead to no output state in t f (e.g., if the evaluation of the body of f from them does not terminate or fails due to an error, as shown in Example 4).

Example 3 (Context summary).

We let h = &l0 → α 0 * S lseg(α 0 , α 1 ) * S α 1 • n → 0x0 * S &l1 → α 2 * S list(α 2 ) and assume that t is defined as in Example 2. Then, (h , t ) defines a valid context summary for append (Figure 1).

Example 4 (Role of the pre-condition approximation in context summaries). We consider the function below and assume it is always called in a state where l0 is a valid pointer and l1 points to a well-formed, but possibly empty, singly-linked list:

1 void getnext ( list * * l0 , list * l1 ) { * l0 = l1->n ; }
Obviously, this function will crash when the list is empty, i.e., when l0 is the null pointer. However, the pair (h f , t f ) below defines a valid transformation summary for this procedure:

h f = &l0 → α 0 * S α 0 → α 1 * S &l1 → α 2 * S list(α 2 ) t f = Id(&l0 → α 0 * S &l1 → α 2 * S α 2 • n → α 3 * S list(α 3 )) * T [α 0 → α 1 α 0 → α 3 ]
We observe that the h f component describes not only states for which the procedure returns but also states for which it crashes since the list pointer cl1 is null. The former are not part of the concretization of the transformation component h f .

The above example shows the importance of the first component of the transformation summary: it conveys the fact that a set of states have been considered by the analysis as a pre-condition for a program fragment, even when the program fragment may not produce any post-condition for these states hereby they can be omitted from the transformation part.

Intraprocedural analysis

The analysis performs a forward abstract interpretation [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF] over abstract transformations (rather than on abstract states). More precisely, the abstract semantics C T of a command C inputs a transformation describing the entire computation so far, before executing C, and outputs a new transformation that reflects the effect of C on top of that computation. Intuitively, the input of C T may be viewed the dual of a continuation. Formally, the analysis is designed so as to meet the following soundness statement, for any transformation t :

∀(σ 0 , σ 1 , ν) ∈ γ T (t ), σ 2 ∈ M, (σ 1 , σ 2 ) ∈ C T =⇒ (σ 0 , σ 2 , ν) ∈ γ T ( C T (t )) (1)
The analysis of assignments and loops follows from [START_REF] Illous | A relational shape abstract domain[END_REF]. It may require finite disjunctions of transformations although we do not formalize this aspect since it is orthogonal to the goal of this paper. We recall the main aspects of their algorithms in this section and refer the reader to [START_REF] Illous | A relational shape abstract domain[END_REF] for a full description.

Post-conditions for assignment. We consider an assignment command x -> n = y (the analysis of other kinds of commands is similar), and a pre-transformation t , and we discuss the computation of x -> n = y T (t ). To do this, the analysis should first localize both x -> n and y in the post-state of t , by rewriting t into an expression of the form Id(&x → α 0 * S &y → α 1 ) * T t 0 or [(. . .) (&x → α 0 * S &y → α 1 )] * T t 0 , and searching for α 0 in t 0 . Two main cases may arise:

-if t 0 contains a term of the form Id(α 0 • n → α 2 ) or [(. . .) (α 0 • n → α 2 )
], the post-transformation is derived by a mutation over the pointer cell, which produces a term of the form [(. . .)

(α 0 • n → α 1 )]; -if t 0 contains a term Id(h 0 ) or [(. . .)
h 0 ] where h 0 is either list(α 0 ) or lseg(α 0 , . . .), the summary should be unfolded so that the modified cell can be resolved as in the previous case; this step relies on relation → U (Section 3).

It is also possible that the localization of x -> n fails, which typically indicates that the program being analyzed may dereference an invalid pointer. Besides assignment, the analysis also supports other such operations; for instance, we write newV T [x 0 , . . . , x n ] (resp., delV T [x 0 , . . . , x n ]) for the operation that adds (resp., removes) variables x 0 , . . . , x n to the output state of the current transformation. They over-approximate concrete operations noted newV and delV.

Weakening. The analysis of loop statements proceeds by abstract iteration over the loop body with widening. Intuitively, the widening t 0 T t 1 of transformations t 0 , t 1 returns a new transformation t , such that γ T (t i ) ⊆ γ T (t ) for all i ∈ {0, 1}. In the state level, widening replaces basic blocks with summaries (effectively inversing → U ). In the transformation level, widening commutes with Id and * T whenever their arguments can be widened as above, and weakens them into [ ] transformations otherwise. Furthermore, this transformation introduces summary predicates so as to ensure termination of all widening sequences [START_REF] Illous | A relational shape abstract domain[END_REF]. Similarly, t 0 T t 1 conservatively decides inclusion test (if t 0 T t 1 holds, then γ T (t 0 ) ⊆ γ T (t 1 )).

Example 5 (Analysis of the loop of append). In this example, we consider the loop at line 4 in the append function (Figure 1) and only present the part of the memory reachable from c. The analysis of the loop starts with the transformation Id(&l0 → α * S &c → α * S list(α)) ∧ α = 0. The analysis of the assignment inside the loop body forces the unfolding of list, and produces Id(&l0

→ α * S α • n → α * S list(α )) * T [(&c → α) (&c → α )] ∧ α = 0. The widening of these two transformations produces Id(&l0 → α * S lseg(α, α ) * S list(α )) * T [(&c → α) (&c → α )] ∧ α = 0
, which also turns out to be the loop invariant.

Abstract composition

In this section, we set up the abstract operations that are required to rely on transformations for modular analysis. In Section 2, we mentioned application and composition. We remark that the application of a transformation t to an abstract state h boils down to the abstract composition of t with Id(h ), since the latter represents exactly the set of pairs (σ, σ) where σ is described by h . Moreover, we observed in Section 2 that composition requires to reason over intersection of abstract states. Thus, we only define intersection and composition in this section.

Abstract intersection. In this paragraph, we set up an abstract operator inter , which inputs two abstract states and returns a disjunctive abstract state that overapproximates their intersection. The computation over abstract heaps is guided by a set of rewriting rules that are shown in Figure 5. The predicate h 0 h 1 H means that the computation of the intersection of h 0 and h 1 may produce the disjunction of abstract heaps H (there may exist several solutions for a given pair of arguments). We remark that the definition of γ H lets symbolic variables be existentially quantified, thus they may be renamed without changing the concretization, following usual α-equivalence. Therefore, the rules of Figure 5 assume that both

h 0,0 h 1,0 H0 h 0,1 h 1,1 H1 (h 0,0 * S h 0,1 ) (h 1,0 * S h 1,1 ) {h 0 * S h 1 | h 0 ∈ H0 ∧ h 1 ∈ H1} * S h is either emp, or n • f → n , or list(α), or lseg(α, α ) h h {h } = list(α1) h 1 H list(α0) (lseg(α0, α1) * S h 1 ) {lseg(α0, α1) * S h | h ∈ H} [l, s] lseg(α1, α2) h 1 H α2 = α1 lseg(α0, α2) (lseg(α0, α1) * S h 1 ) {lseg(α0, α1) * S h | h ∈ H} [s, s]
h 0 contains a list(α0) or lseg(α0, α1) term α0 carries no summary in h 1 arguments follow a consistent naming, although the implementation should perform α-equivalence whenever needed and maintain a correspondence of symbolic variables [START_REF] Bor-Yuh | Relational inductive shape analysis[END_REF]. Rule * S states that intersection can be computed locally. Rule = expresses that intersection behaves like identity when both of its arguments are the same basic term. Rules [l, s] and [s, s] implement structural reasoning over summaries. Finally, rule u unfolds one argument so as to consider all subsequent cases. The result may differ depending on the order of application or even on the way each rule is applied. As an example, * S may produce different results depending on the way both arguments are split into h i,0 and h i,1 , which may affect precision. Therefore, our implementation follows a carefully designed application strategy that attempts to maximize the use of = . We omit the numerical predicate intersection (handled by a numerical domain intersection operator). Given two abstract heaps h 0 , h 1 , the computation of inter (h 0 , h 1 ) proceeds by proof search following the rules of Figure 5 up-to commutativity (standard rule, not shown). In case this system fails to infer a solution, returning either argument provides a sound result.

h 0 h 1 {h | ∃h 0,u , H, (h 0 → U[α 0 ] h 0,u ) ∧ (h 0,u h 1 H) ∧ h ∈ H} u

Definition 3 (Abstract intersection algorithm).

The operator inter is a partial function that inputs two abstract heaps h 0 , h 1 and returns a disjunction of abstract heaps H such that h 0 h 1 H following Figure 5.

Theorem 1 (Soundness of abstract intersection). Abstract intersection is sound in the sense that, for all h

0 , h 1 , γ H (h 0 ) ∩ γ H (h 1 ) ⊆ γ H (inter (h 0 , h 1 )).

Example 6 (Abstract intersection). Let us consider:

-

h 0 = &x → α 0 * S &y → α 2 * S lseg(α 0 , α 2 ) * S α 2 • n → α 3 * S list(α 3 ) and -h 1 = &x → α 0 * S &y → α 2 * S lseg(α 0 , α 1 ) * S α 1 • n → α 2 * S list(α 2 ). Then, inter (h 0 , h 1 ) returns &x → α 0 * S &y → α 2 * S lseg(α 0 , α 1 ) * S α 1 • n → α 2 * S α 2 • n → α 3 * S list(α 3 )
. Note that the computation involves the structural t 0,0 t 1,0 T0 t 0,1 t 1,1 T1

(t 0,0 * T t 0,1 ) (t 1,0 * T t 1,1 )

{t 0 * T t 1 | t 0 ∈ T0 ∧ t 1 ∈ T1} * T h 0 h 1 H Id(h 0 ) Id(h 1 ) {Id(h ) | h ∈ H} Id h 0,o h 1,i H H = ∅ [h 0,i h 0,o ] [h 1,i h 1,o ] [h 0,i h 1,o ] h 0 h 1,i H Id(h 0 ) [h 1,i h 1,o ] {[h i h 1,o ] | h i ∈ H} Id, ,l [(h 0 * S h 0,i ) (h 0 * S h 0,o )] t 1 T (Id(h 0 ) * T [h 0,i h 0,o ]) t 1 T weak,Id,l ([(h 0,i * S h 1,i ) (h 0,o * S h 1,o )] * T t 2 ) t 3 T ([h 0,i h 0,o ] * T [h 1,i h 1,o ] * T t 2 ) t 3
T weak, * T,l t 0 contains an list(α0) or lseg(α0, α1) term

t 0 t 1 {t | ∃t 0,u , (t 0 → U[α 0 ] t 0,u ) ∧ (t 0,u t 1 T ) ∧ t ∈ T } unf,l
Fig. 6. Abstract composition rewriting rules (rules Id, ,r , weak,Id,r , weak, * T,r , and unf,r which are right versions of rules Id, ,l , weak,Id,l , weak, * T,l , and unf,l , can be systematically derived by symmetry, and are omitted for the sake of brevity).

rule [s, s] and the unfolding rule to derive this result, where both the segment between x and y and the list pointed to by y are non-empty. This result is exact (no precision is lost) and the result is effectively more precise than both arguments.

Composition of abstract transformations. We now study the composition of abstract transformations. Again, the computation is based on a rewriting system, that gradually processes two input transformations into an abstraction of their composition. The rules are provided in Figure 6. The predicate t 0 t 1 T means that the effect of applying transformation t 0 and then transformation t 1 can be described by the union of the transformations in T . Rule * T enables local reasoning over composition, at the transformation level. Rules Id and respectively compose matching identity transformations and matching modifying transformations. Similarly, Id, ,l composes an identity followed by a modifying transformation with a consistent support (this rule, as the following, has a corresponding right version that we omit for the sake of brevity). Rule weak,Id,l implements a weakening based on the inclusion γ T (Id(t )) ⊆ γ T ([t t ]) (the inclusion is proved in [START_REF] Illous | A relational shape abstract domain[END_REF]). Similarly, rule weak, * T ,l weakens [h 0,i

h 0,o ] * T [h 1,i h 1,o ] into [(h 0,i * S h 1,i ) (h 0,o * S h 1,o )].
Finally, rule unf,l unfolds a summary to enable composition. The abstract composition operation performs a proof search. Just as for intersection, the composition operator may produce different results depending on the application order; our implementation relies on a strategy designed to improve precision by maximizing the use of Id .

Definition 4 (Abstract composition algorithm). The operator comp is a partial function that inputs two abstract transformations t 0 , t 1 and returns a set of abstract transformations T such that t 0 t 1 T following Figure 6.

Theorem 2 (Soundness of abstract composition). Let t 0 , t 1 be two transformations, h 0 , h 1 , h 2 be abstract heaps and ν be a valuation. We assume that comp (t 0 , t 1 ) evaluates to the set of transformations T . Then:

(σ 0 , σ 1 , ν) ∈ γ T (t 0 ) ∧ (σ 1 , σ 2 , ν) ∈ γ T (t 1 ) =⇒ ∃t ∈ T, (σ 0 , σ 2 , ν) ∈ γ T (t )
Example 7 (Abstract composition and analysis compositionality). In this example, we study the classical case of an in-place list reverse code snippet:

1 // l points to a list

2 list * c = l ; list * x = 0 ; 3 while ( l != NULL ) { c = l->n ; l->n = x ; x = l ; l = c ; }
The effects of c = l->n and of l->n = x can be described by the abstract transformations t 0 and t 1 :

t 0 = Id(&l → α 0 * S α 0 • n → α 1 * S &x → α 2 * S list(α 1 ) * S list(α 2 )) * T [(&c → α 3 ) (&c → α 1 )] t 1 = Id(&l → α 0 * S &x → α 2 * S &c → α 1 * S list(α 1 ) * S list(α 2 )) * T [(α 0 • n → α 1 ) (α 0 • n → α 2 )]
The composition of these two transformations needs to apply the weakening rules to match terms that are under the Id constructors. The result is the following transformation t 0 t 1 :

Id(&l → α 0 * S &x → α 2 * S list(α 1 ) * S list(α 2 )) * T [(&c → α 3 ) (&c → α 1 )] * T [(α 0 • n → α 1 ) (α 0 • n → α 2 )]
This description is actually a very precise account for the effect of the sequence of these two assignment commands. This example shows that composition may be used not only for interprocedural analysis (as we show in the next section), but also to supersede some operations of the intraprocedural analysis of Section 5.

Example 8 (Abstract application)

. As observed at the beginning of the section, composition may also be used as a means to analyze the application of a transformation to an abstract state. We consider the composition of the transformation t corresponding to function append (shown in Example 2 and Figure 1) and the

abstract pre-state h = &l0 → α 0 * S &l1 → α 2 * S lseg(α 0 , α 1 ) * S α 1 • n → α 3 * S list(α 2 ) ∧ α 3 = 0x0.
Then, the composition Id(h ) t returns:

&l0 → α 0 * S &l1 → α 2 * S lseg(α 0 , α 1 ) * S α 1 • n → α 2 * S list(α 2 )
7 Interprocedural analysis based on function summaries

In this section, we study two mutually dependent aspects: the application of summaries at call-sites and their inference by static analysis in a top down manner.

We first focus on non-recursive calls and discuss recursive calls at the end of the section. The analysis maintains a context summary (h f , t f ) for each procedure f. Initially, this context summary is set to (⊥, ⊥). When the analysis reaches a call to procedure f it should attempt to utilize the existing summary (Section 7.1).

When the existing summary does not account for all the states that may reach the current context, a new summary needs to be computed first (Section 7.2).

Analysis of a call site using an existing summary

We assume a procedure proc f (p 0 , . . . , p k ){C} and a sound context summary (h f , t f ). We consider the analysis f(x 0 , . . . , x k ) T of a call to this procedure, with transformation t pre as a pre-transformation. To analyze the call, the analysis should (1) process parameter passing, (2) detect which part of t pre may be modified by f, (3) check whether the context summary covers this context, and (4) apply the summary, if (3) succeeds (the case where it fails is studied in Section 7.2).

Parameter passing. Parameter passing boils down to creating the variables p 0 , . . . , p k using transfer function newV T and then to analyzing assignment statements p 0 = x 0 , . . . , p k = x k . These operations can all be done using the transfer functions defined in Section 5:

t pars = ( p k = x k T • . . . • p 0 = x 0 T • newV T [p 0 , . . . , p k ])(t pre )
Procedure footprint. To identify the fragment of the abstract heap that f can view and may modify, the analysis should first extract from t pars an abstraction of the set of states that enter the body of f. This is the goal of function O : T → H:

O(Id(h )) = h O(t 0 * T t 1 ) = O(t 0 ) * S O(t 1 ) O([h 0 h 1 ]) = h 1 O(t ∧ c ) = O(t ) ∧ c
Intuitively, O projects the "output" part of a transformation. Thus O(t pars ) overapproximates the set of states that enter C. However, only the fragment of O(t pars ) that is reachable from the parameters of f is relevant. Given an abstract heap h , we can compute the set of symbolic names R[h ] that are relevant based on the following rules:

(&p i ) ∈ R[h ] n ∈ R[h ] h contains a term n • f → n or lseg(n, n ) n ∈ R[h ]
The slice R[p 0 , . . . , p k ](h ) of h with respect to p 0 , . . . , p k retains only the terms of h that contain only names in R[h ] defined as the least solution of the above rules. Similarly, we let I[p 0 , . . . , p k ](h ) be the abstract heap made of the remaining terms. Therefore, we have the equality h = R[p 0 , . . . , p k ](h ) * S I[p 0 , . . . , p k ](h ).

Data: Existing context summary (h f , t f ) for proc f (p 0 , . . . , p k ){C} Data: Input transformation t pre (computation before the call) Result: Output transformation t post (computation before the call + body of f) Result: Update of the context summary if it does not cover the context of t pre

1 t pars ← p k = x k T • . . . • p 0 = x0 T • newVT [p 0 , . . . , p k ](t pre ) ; 2 h in,f = R[p 0 , . . . , p k ](O(t pars )) ; 3 h rem = I[p 0 , . . . , p k ](O(t pars )) ; 4 if ¬(h in,f H h f ) then 5 h f ← h f H h in,f ; 6 t f ← C T (Id(h f )) 7 end 8 t post ← delVT [p 0 , . . . p k ](comp (t pars , t f * T Id(h rem )))
Fig. 7. Interprocedural analysis: algorithm for the analysis of a procedure call.

Summary computation. The computation of a new context summary should take into account a context that is general enough to encompass both h f and h in,f :

the new abstract context is h f H h in,f using abstract state widening H [START_REF] Chang | Shape analysis with structural invariant checkers[END_REF]; -the new summary related to this abstract context is derived by analysis of the body of f, thus by updating t f with C T (Id(h f T h in,f )). Then, the context summary for f is updated with this new context summary.

Application. Once a new summary has been computed, by definition, it satisfies the inclusion h in,f H h f , thus it can be applied so as to compute an abstract transformation after the call to f as shown in Section 7.1.

The overall procedure call analysis algorithm is displayed in Figure 7. The case examined in this subsection corresponds to the case where the if branch at lines 5-6 is taken. We observe that it necessarily occurs whenever a procedure is analyzed for the first time, as context summaries are initially set to (⊥, ⊥). Moreover, we note that the application of the summary after its update is done as in Section 7.1.

The following result formalizes the soundness of Figure 7, under the assumption that there is no recursive call.

Theorem 3 (Soundness of the analysis of a procedure call using a context summary). We consider the call to f with the abstract transformation t pre as input, and the post-condition t post returned by the algorithm of Figure 7. We denote by (h f , t f ) the context summary for f after the analysis of the call. We let

(σ 0 , σ 1 , ν) ∈ γ T (t pre ), σ 1 ∈ p 0 = x 0 T • . . . • p k = x k T • newV[p 0 , . . . p k ]({σ 1 }), σ 2 ∈ C T ({σ 1 }), and σ 2 ∈ delV[p 0 , . . . , p k ]({σ 2 }) (i.e., σ 2 ∈ f(x 0 , . . . , x k ) T ({σ 1 })).
Then, the following property holds:

(σ 0 , σ 2 , ν) ∈ γ T (t post ) ∧ (σ 1 , ν) ∈ γ H (h f ) ∧ (σ 1 , σ 2 , ν) ∈ γ T (t f )
This result means that not only the transformation t post over-approximates the state after the call, but also the new context summary accounts for this call. This entails that context summaries account for all the calls that are encountered in the analysis of a complete interprocedural program. Moreover, Theorem 3 entails Equation 1 for procedure calls.

Example 10 (Context summary computation). In this example, we consider the function append again, but assume that the analysis starts with the (⊥, ⊥) context summary for it. We study the code append(a, b); append(a, c); where a, b, and c are initially lists of length 1. Then:

the first call results in the update of the summary with a context summary (h , t ) where h assumes that the first argument is a single list element, i.e., is of the form &l0 → α 0 * S α 0 • n → 0x0 * S &l1 → α 1 * S . . .;

when the second call is encountered this first summary does not cover the second context (at this point, the argument a has length 2), thus a new context summary needs to be calculated; this new summary (h , t ) is such that h only assumes that the first argument may be a list of any length (as derived by widening), i.e., it is of the form &l0 → α 0 * S lseg(α 0 , α 1 ) * S α 1 • n → 0x0 * S &l1 → α 1 * S . . .. This last summary may still not be as general as the summary shown in Example 9, and may thus be generalized even more at subsequent call points.

Analysis of recursive calls. So far, we have focused on the case where there are no recursive calls. Actually, the presence of recursive calls changes relatively little to the principle of our analysis (although the formalization would be significantly heavier and is left out). Indeed, it only requires to extend the algorithm of Figure 7 with a fixpoint computation over context summaries, so as to determine an overapproximation of both components of the procedure context summary.

when a recursive call is encountered and when the calling context is not accounted for in the current context summary (Figure 7, condition at line 4 evaluated to false), the h f component should be widened and the current t f should be used directly; -at the end of the analysis of the procedure body, the t f component should be widened with the previously known transformation, and the analysis of the procedure body iterated until this transformation stabilizes. Convergence is ensured by widening both on abstract states and transformations.

Experimental evaluation

In this section, we report on the evaluation of the interprocedural analysis based on function summaries, with respect to the following questions:

1. Is it able to infer precise invariants? 2. Does it scale better than a classical call-string-based analysis? 3. How effective are context summaries, i.e., do they often have to be recomputed?

We have implemented the interprocedural analysis based on context summaries for a large fragment of the C language. Our tool is a plugin for Frama-C [START_REF] Kirchner | Frama-c: A software analysis perspective[END_REF]. It supports conventional control flow structures of C and can be parameterized by the inductive definition of the structure to consider, as in [START_REF] Bor-Yuh | Relational inductive shape analysis[END_REF]. However, it leaves out non-recursive structures and data-types that are not immediately related to the analysis principle (strings, arrays, numeric types). Furthermore, we have also implemented as another extension of Frama-C an analysis relying on the call-string approach, i.e., that inlines procedures at call sites.

Experiments and raw data. We did two experiments. First, we ran the two analyses on a fragment of the GNU Emacs 25.3 editor. This fragment comprises 22 functions of the Fx_show_tip feature and is implemented in C. It manipulates descriptions of Lisp objects including lists built as Cons pairs. The analyzed code corresponds to about 3 kLOC. Analyses were ran on an Intel Core i7 laptop at 2.3 GHz with 16Gb of RAM. The raw data are provided in Appendix A and the following paragraphs discuss the main points related to the above questions. Second, we analyzed a set of basic recursive functions on trees and lists to validate the recursive call analysis.

Precision. We compared the result of the analysis of the body of each procedure. More precisely, we checked whether the transformation computed for the whole procedure body for its entry abstract state (the first component of context summaries) is at least as precise as the post-condition produced by the state analysis. For 15 functions, the body contains nested calls and the result is as precise. The remaining 7 functions do not contain any call, thus are not relevant to validate the absence of precision loss at call sites.

Scalability. The total measured analysis time was 14.20s for the transformationbased analysis against 877.12s for the state analysis, which shows a high overall speedup. Secondly, we show the average analysis time of the body of each function in Figure 8 (these values are average analysis times, and not total time spent analyzing each function, as the effectiveness of summary reuse is the topic of the next paragraph). We observe that for some functions the speedup is low or even negative. These functions mostly correspond to low analysis times. Upon inspection, they all occupy a low position in the call tree: they call few functions, and the transformation analysis overhead is not compensated by a high gain from many summary applications to avoid the analysis of down calls. Conversely functions at the top of the call graph (such as the entry point) show a very high gain.

Effectiveness. Finally, we assessed the effectiveness of the summary reuse, which depends not only on the call graph shape (functions that are called at a single site offer no gain opportunity) but also on the function behavior and the analysis (depending on the contexts that are encountered, some procedure may need to be reanalyzed multiple times or not). We observed that only one procedure needed to be reanalyzed (Fcons was reanalyzed 3 times). All other summaries were computed only once (i.e., the branch at lines 4-6 in Figure 7 is taken only once). For functions called at a single point (11 of the total) summaries could not be reused, but for 8 functions, summaries were reused multiple times (3 to 44 times). By contrast, the state analysis had to reanalyze most functions several times: in particular 11 functions were reanalyzed 15 times or more (up to 296 times). Therefore, the summary-based analysis provides significant gain even for small functions.

Recursive calls. We ran the analysis on a series of recursive implementations of classical functions on lists and binary trees, including size, allocation, deallocation, insertion, search and deep copy, and also list concatenation and filter. For all these functions, the expected invariants could be inferred in under 5ms (Appendix A).

Related works and conclusion

Since Sharir and Pnueli's seminal paper [START_REF] Sharir | Two approaches to interprocedural data flow analysis[END_REF], many works have studied approaches to interprocedural analyses. The relational approach strives for modularity, which has been a concern in static analysis even beyond interprocedural code [START_REF] Cousot | Modular static program analysis[END_REF][START_REF] Codish | Compositional analysis of modular logic programs[END_REF]. A major advantage of modular approaches is to avoid the reanalysis of program fragments that are called repeatedly. However, it is generally difficult to apply as it requires an accurate and efficient representation for summaries. While relational numerical abstract domains [START_REF] Cousot | Automatic discovery of linear restraints among variables of a program[END_REF] naturally provide a way to capture numerical input/output relations [START_REF] Müller | Precise interprocedural analysis through linear algebra[END_REF][START_REF] Popeea | Inferring disjunctive postconditions[END_REF], this is harder to achieve when considering memory abstractions. The TVLA framework [START_REF] Sagiv | Solving shape-analysis problems in languages with destructive updating[END_REF] supports such relation using the classical "primed variables" technique [START_REF] Jeannet | A relational approach to interprocedural shape analysis[END_REF][START_REF] Jeannet | A relational approach to interprocedural shape analysis[END_REF] where input and output variables are distinguished using prime symbols. Some pointer analyses such as [START_REF] Dillig | Precise and compact modular procedure summaries for heap manipulating programs[END_REF] rely on specific classes of procedure summaries to enable modular analysis. However, separation logic [START_REF] Reynolds | Separation logic: A logic for shared mutable data structures[END_REF] does not naturally support this since formulas describe regions of a given heap. The classical solution involves the tabulation of pairs of separation logic formulas [START_REF] Calcagno | Footprint analysis : A shape analysis that discovers preconditions[END_REF][START_REF] Bhargav S Gulavani | Bottom-up shape analysis[END_REF][START_REF] Loc | Shape analysis via second-order bi-abduction[END_REF], but this approach does not allow to relate the description of heap regions in a fine manner. To circumvent this, we use transformations introduced in [START_REF] Illous | A relational shape abstract domain[END_REF], which are built on connectors inspired by separation logic. The advantage is twofold: it enables not only a more concise representation of transformations (since tables of pairs may need to grow large to precisely characterize the effect of procedures) but also a more local description of the relation between procedure input and output states. Our graph representation of abstract states and transformations opens the way to a resolution of the frame problem [START_REF] Rinetzky | A semantics for procedure local heaps and its abstractions[END_REF][START_REF] Rinetzky | Interprocedural shape analysis for cutpoint-free programs[END_REF] using intersection operation. The results of our top-down, context summary-based analysis confirm that this approach brings a gain in analysis scalability once the upfront cost of summaries is amortized.

Many pointer analyses and weak forms of shape analyses have introduced specific techniques in order to construct and compute procedure summaries [START_REF] Lattner | Making context-sensitive points-to analysis with heap cloning practical for the real world[END_REF][START_REF] Marron | Efficient context-sensitive shape analysis with graph based heap models[END_REF][START_REF] Lei | Fast and precise handling of positive weight cycles for field-sensitive pointer analysis[END_REF]. These works typically rely on some notion of graph that describes both knowledge about memory entities and procedure calls, therefore the interprocedural analysis reduces to graph algorithms. Moreover, context sensitivity information may be embedded into these graphs. Our approach differs in that it relies on a specific algebra of summaries, although we may also augment our summaries with context information. Another difference is that the summary predicates our abstract domain is based on allow a very high level of precision and that the abstract procedure call analysis algorithm (with intersection and composition) aims at preserving this precision. We believe that two interesting avenues for future works would consider the combination of various levels of context sensitivity and of less less expressive summaries with our analysis framework.

A very wide range of techniques have been developed to better cope with interprocedural analysis, many of which could be combined with context summaries. First, we do not consider tabulation of procedure summaries [START_REF] Cousot | Modular static program analysis[END_REF], however, we could introduce this technique together with some amount of context sensitivity [START_REF] Bourdoncle | Abstract interpretation by dynamic partitioning[END_REF]. Indeed, while relations reduce the need for tables of abstract pre-and post-conditions, combining context summaries and finer context abstraction may result in increased precision [START_REF] Chatterjee | Relevant context inference[END_REF]. Bi-abduction [START_REF] Calcagno | Compositional shape analysis by means of bi-abduction[END_REF] has been proposed as a technique to infer relevant abstract pre-conditions of procedures. In [START_REF] Calcagno | Compositional shape analysis by means of bi-abduction[END_REF], this process was implemented on a state abstract domain, but the core principle of the technique is orthogonal to that choice, thus bi-abduction could also be applied to abstract transformations. Moreover, while our analysis proceeds top-down, it would be interesting to consider the combination with a bottom-up inference of summaries for some procedures [START_REF] Castelnuovo | Modularity in lattices: A case study on the correspondence between top-down and bottom-up analysis[END_REF]. Last, many works have considered the abstraction of the stack-frame and of the relations between the stack frame structure and the heap structures manipulated by procedures [START_REF] Rinetzky | Interprocedural shape analysis for recursive programs[END_REF][START_REF] Rival | Calling context abstraction with shapes[END_REF]. The notion of cut-points has been proposed in [START_REF] Rinetzky | A semantics for procedure local heaps and its abstractions[END_REF][START_REF] Rinetzky | Interprocedural shape analysis for cutpoint-free programs[END_REF] to describe structures tightly intertwined with the stack. An advantage of our technique is that the use of an abstraction based on transformations which can express that a region of the heap is preserved reduces the need to reason over cutpoints.

A Raw experimental data

Analysis of Fx_show_tip. The table below lists the per call average analysis times of each procedure, whether the summary analysis is as precise as the state analysis ("as precise" means the results are at least as precise; "irrel." means the measure is irrelevant as the function body does not contain any call) and the depth in the call graph. The table below lists the number of times the body of a procedure is reanalyzed:

column #state counts reanalyses by the state analysis; -column #total counts the number of times a call site to this procedure is encountered by the summary analysis; -column #recomp counts the number of times the summary based analysis needs to reanalyze the body of this procedure to come up with more general summary; -column #reuse counts the number of times a summary is reused without recomputation.

1Fig. 1 .

 1 Fig. 1. Simple and double list append procedures.

Fig. 2 .

 2 Fig. 2. A shape transformation procedure summary and composition.

Fig. 3 .

 3 Fig. 3. Syntax and concretization of the abstract states.

Fig. 4 .

 4 Fig. 4. Syntax and concretization of abstract transformations.

Fig. 5 .

 5 Fig. 5. Abstract intersection rewriting rules.

Fig. 8 .

 8 Fig. 8. Per-function comparison of analysis runtime (times in seconds)

  Analysis of recursive list and tree classical algorithms. The table below lists the analysis times of a series of classical functions over lists and trees.

	Function name		#state #total #recomp #reuse
	Fcons		296	47	3	44
	list2		12	2	1	1
	list4		24	4	1	3
	Fassq		64	16	1	15
	Fcar		24	1	1	0
	Fcdr		12	4	1	3
	Fnthcdr		24	1	1	0
	Fnth		24	8	1	7
	make_monitor_attribute_list	6	2	1	1
	check_x_display_info		3	1	1	0
	Fx_display_monitor_attributes_list	3	1	1	0
	x_get_monitor_for_frame		6	2	1	1
	x_make_monitor_attribute_list	3	1	1	0
	x_get_monitor_attributes_fallback	3	1	1	0
	x_get_monitor_attributes		3	1	1	0
	x_get_arg		19	5	1	4
	x_frame_get_arg		15	1	1	0
	x_default_parameter		15	15	1	14
	compute_tip_xy		3	3	1	2
	x_default_font_parameter		1	1	1	0
	x_create_tip_frame		1	1	1	0
	Fx_show_tip		1	1	1	0
	Structure function time (ms)
	List	length	1.256
	List	get_n	2.179
	List	alloc	1.139
	List	dealloc	0.842
	List	concat	1.833
	List	map	0.904
	List	deep_copy 1.540
	List	filter	3.357
	Tree	visit	1.078
	Tree	size	1.951
	Tree	search	3.818
	Tree	dealloc	1.391
	Tree	insert	5.083
	Tree	deep_copy 2.603

Acknowledgments. We would like to thank the anonymous reviewers for their suggestions that helped greatly improve the quality of this paper. This work has received support from the French ANR as part of the VeriAMOS grant.

Context summary coverage test. Based on the above, the set of states that reach the body of f under the calling context defined by t pre can be over-approximated by h in,f = R[p 0 , . . . , p k ](O(t pars )). We let h rem = I[p 0 , . . . , p k ](O(t pars )) be the remainder part. The context summary (h f , t f ) covers h in,f if and only if h in,f H h f holds where H is a sound abstract state inclusion test as defined in, e.g., [START_REF] Distefano | A local shape analysis based on separation logic[END_REF][START_REF] Chang | Shape analysis with structural invariant checkers[END_REF]. When this condition does not hold, the context summary should be re-computed with a more general pre-condition (this point is discussed in Section 7.2). Summary application. Given the above notation, the effect of the procedure (described by t f ) should be applied to h in,f whereas h rem should be preserved. To do this, the following transformation should be composed with the abstract transformation t f * T Id(h rem ) (note that the identity part is applied to the part of the pre-transformation that is not relevant to the execution of the body of f). Thus, the transformation that accounts for the computation from the program entry point till the return point of f is:

Example 9 (Context summary coverage and application). In this example, we assume the context summary defined in Example 3 for procedure append:

Moreover, we consider the call append(a,b) with the abstract transformation below as a pre-condition (note that variable c is not accessed by append):

After parameter passing, computation of the heap fragment f may view, and projection of the output, we obtain the abstract state &l0 → α 0 * S α 0 •n → 0x0 * S &l1 → α 1 * S α 1 • n → 0x0, which is obviously included in h . The composition with the summary of the procedure produces the abstract transformation below:

The whole algorithm is shown in Figure 7. It implements the steps described above and in Section 7.2. The case considered in this subsection (when h in,f H h f holds) corresponds to the case where the if branch at lines 5-6 is not taken.

Inference of a new context summary

We now discuss the case where the previously existing context summary of f does not cover the executions corresponding to t . As mentioned above, this corresponds to the case where the abstract inclusion h in,f H h f does not hold.