Bor-Yuh Evan Chang

Xavier Rival
email: rival@di.ens.fr

Modular Construction of Shape-Numeric Analyzers

The aim of static analysis is to infer invariants about programs that are precise enough to establish semantic properties, such as the absence of run-time errors. Broadly speaking, there are two major branches of static analysis for imperative programs. Pointer and shape analyses focus on inferring properties of pointers, dynamically-allocated memory, and recursive data structures, while numeric analyses seek to derive invariants on numeric values. Although simultaneous inference of shapenumeric invariants is often needed, this case is especially challenging and is not particularly well explored. Notably, simultaneous shape-numeric inference raises complex issues in the design of the static analyzer itself.

In this paper, we study the construction of such shape-numeric, static analyzers. We set up an abstract interpretation framework that allows us to reason about simultaneous shape-numeric properties by combining shape and numeric abstractions into a modular, expressive abstract domain. Such a modular structure is highly desirable to make its formalization and implementation easier to do and get correct. To achieve this, we choose a concrete semantics that can be abstracted step-by-step, while preserving a high level of expressiveness. The structure of abstract operations (i.e., transfer, join, and comparison) follows the structure of this semantics. The advantage of this construction is to divide the analyzer in modules and functors that implement abstractions of distinct features.

Introduction

The static analysis of programs written in real-world imperative languages like C or Java are challenging because of the mix of programming features that the analyzer must handle effectively. On one hand, there are pointer values (i.e., memory addresses) that can be used to create dynamically-allocated recursive data structures. On the other hand, there are numeric data values (e.g., integer and floating-point values) that are integral to the behavior of the program. While it is desirable to use distinct abstract domains to handle such different families of properties, precise analyses require these abstract domains to exchange information because the pointer and numeric values are often interdependent. Setting up the structure of the implementation of such a shape-numeric analyzer can be quite difficult. While maintaining separate modules with clearly defined interfaces is a cornerstone of software engineering, such boundaries also impede the easy exchange of semantic information.

In this manuscript, we contribute a modular construction of an abstract domain [START_REF] Cousot | Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints[END_REF] that layers a numeric abstraction on a shape abstraction of memory. The construction that we present is parametric in the numeric abstraction, as well as the shape abstraction. For example, the numeric abstraction may be instantiated with an abstract domain such such as polyhedra [START_REF] Cousot | Automatic discovery of linear restraints among variables of a program[END_REF] or octagons [START_REF] Miné | The octagon abstract domain[END_REF], while the shape abstraction may be instantiated with domains such as Xisa [START_REF] Chang | End-User Program Analysis[END_REF][START_REF] Chang | Relational inductive shape analysis[END_REF] or TVLA [START_REF] Sagiv | Parametric shape analysis via 3-valued logic[END_REF]. Note that the focus of this paper is on describing the formalization and construction of the abstract domain. Empirical evaluation of implementations based on this construction are given elsewhere [START_REF] Chang | End-User Program Analysis[END_REF][START_REF] Chang | Relational inductive shape analysis[END_REF][START_REF] Chang | Shape Analysis with Structural Invariant Checkers[END_REF][START_REF] Laviron | Separating Shape Graphs[END_REF][START_REF] Rival | Calling context abstraction with shapes[END_REF][START_REF] Sotin | Hierarchical Shape Abstraction of Dynamic Structures in Static Blocks[END_REF][START_REF] Toubhans | Reduced Product Combination of Abstract Domains for Shapes[END_REF].

We describe our construction in four steps:

1. We define a concrete program semantics for a generic imperative programming language focusing on the concrete model of mutable memory (Section 2). 2. We describe a step-by-step abstraction of program states as a cofibered construction of a numeric abstraction layer on top of a shape abstraction layer (Section 3). In particular, we characterize a shape abstraction as a combination of an exact abstraction of memory cells along with a summarization operation. Then, we describe how a value abstraction can be applied both globally on materialized memory locations and locally within summarized regions. 3. We detail the abstract operators necessary to implement an abstract program semantics in terms of interfaces that a shape abstraction and a value abstraction must implement (Section 4). 4. We overview a modular construction of a shape-numeric static analyzer based on our abstract operators (Section 5).

A concrete semantics

We first define a concrete program semantics for a generic imperative programming language.

Concrete memory states

We define a "bare metal" model of machine memory. A concrete store is a partial function σ ∈ H = A ⇀ fin V from addresses to values. An address a ∈ A is also considered a value v ∈ V, that is, we assume that A ⊆ V. For simplicity, we assume that all cells of any store σ have the same size (i.e., word-sized) and that all addresses are aligned (i.e., word-aligned). For example, we can imagine a standard 32-bit architecture where all values are 4-bytes and all addresses are 4-byte-aligned. We write for dom(σ ) the set of addresses at which σ is defined, and we let σ [a ← v] denote the heap obtained after updating the cell at address a with value v. A concrete environment E ∈ E = X → A maps program variables to their addresses. That is, we consider all program variables as mutable cells in the concrete store-the concrete environment E indicates where each variable is allocated. A concrete memory state m simply pairs a concrete environment and a concrete store: (E, σ ). Thus, the set of memory states M = E × H is the product of the set of concrete environments and the set of concrete stores.

Figure 1(c) shows an example concrete memory state at the return point of the procedure f in (a). The environment E has two bindings for the variables x and y that are in scope. For concreteness, we show the concrete store for this example laid out using 32-bit addresses and a C-style layout for struct s. The figure shown in (b) shows the concrete store as an informal box diagram.

Related work and discussion. Observe that we do not make the distinction between stack and heap space in a concrete store σ (as in a C-style model), nor have we partitioned a heap on field names (as in Java-style model). We have intentionally chosen this rather low-level definition of concrete memory states-essentially an assembly-level model of memory-and leave any abstraction to the definition of abstract memory states. An advantage of this approach is the ability to use a common concrete model for combining abstractions that make different choices about the details they wish to expose or hide [START_REF] Laviron | Separating Shape Graphs[END_REF]. For example, Laviron et al. [START_REF] Laviron | Separating Shape Graphs[END_REF] defines an abstract domain that treats precisely C-style aggregates: both structs and unions with sized-fields and pointer arithmetic. Another abstract domain [START_REF] Sotin | Hierarchical Shape Abstraction of Dynamic Structures in Static Blocks[END_REF] abstracts nested structures using a hierarchical abstraction. Rival and Chang [START_REF] Rival | Calling context abstraction with shapes[END_REF] defines an abstraction that simultaneously summarizes the stack of activation records and the heap data structures (with a slightly extended notion of concrete environments), which is useful for analyzing recursive procedures.

Concrete program semantics

For the most part, we can be agnostic about the particulars of the imperative programming language of interest. To separate concerns between abstracting memory and control points on which abstract interpretation collects, all we assume is that a concrete execution state consists of a control state and a concrete memory state. A shape-numeric abstract domain as we define in Section 3 abstracts the concrete memory state component.

Definition 1 (Execution states

). An execution state s ∈ S consists of a triple (ℓ, E, σ ) where ℓ ∈ L is a control state, E ∈ E is an concrete environment, and σ ∈ H is a concrete store. The memory component of an execution state is the pair (E, σ ) ∈ M.

Thus, the set of execution states S = L × E × H ≡ L × M. A program execution is described by a finite trace, that is, a finite sequence of states s 0 , . . . , s n . We let T = S ⋆ denote the set of finite traces over S.

To make our examples more concrete, we consider a C-like programming language whose syntax is shown in Figure 2. A location expression loc names a memory cell, which can be a program variable x, a field offset from another memory location loc 1 • f, or the memory location named by a pointer value ⋆exp. We write f ∈ F for a field name and implicitly read any field as an offset, that is, we write a + f for the address a ′ ∈ A obtained by offsetting an address a with field f. To emphasize that we mean C-style field offset as opposed to Java-style field dereference, we write x • f for what is normally written as x.f in C. As in C, we write exp -> f for Java-style field dereference, which is a shorthand for (⋆exp) • f. An expression exp can be a memory location expression loc, an address of a memory location &loc, or any value literal v, some other n-ary operator ⊕(exp). Like in C, a memory location expression loc used as an expression (i.e., "r-value") refers to the contents of the named memory cell, while the &loc converts the location's address (i.e., "l-value") into a pointer "r-value." We leave the value literals v (e.g., 1) and expression operators ⊕ (e.g., !, +, ==) unspecified.

An operational semantics: Given a program p, we assume its execution is described by a transition relation → p ⊆ S × S. This relation defines a small-step operational semantics, which can be defined as a structured operational semantics judgment s → p s ′ . Such a definition is completely standard for our language, so we do not detail it here.

loc (∈ L X ) ::= x (x ∈ X) | loc 1 • f (loc 1 ∈ L X ; f ∈ F) | ⋆exp (exp ∈ E X ) exp (∈ E X ) ::= loc (loc ∈ L X ) | &loc (loc ∈ L X ) | v (v ∈ V) | ⊕(exp) (exp ∈ E X ) ⊕ ::= • • • p (∈ P X ) ::= loc = exp (loc ∈ L X ; exp ∈ E X ) assignment | loc = malloc({f 1 , . . . , f n }) (loc ∈ L X ; [f 1 , . . . , f n ] ∈ F * ) memory allocation | free(loc) (loc ∈ L X ) memory deallocation | p 1 ; p 2 (p 1 , p 2 ∈ P X ) sequence | if (exp) p 1 else p 1 (exp ∈ E X ; p 1 , p 2 ∈ P X ) condition test | while (exp) p 1 (exp ∈ E X ; p 1 ∈ P X ) loop
Figure 2: Abstract syntax for a C-like imperative programming language. A program p consists of assignment, dynamic memory allocation and deallocation, sequences, condition tests, and loops. An assignment is specified by a location expression loc that names a memory cell to update and an expression exp that is evaluated to yield the new contents for the cell. For simplicity, we specify allocation with a list of field names (i.e., malloc({f 1 , . . . ,

f n })). DOASSIGNMENT (ℓ pre , E, σ ) → loc = exp (ℓ post , E, σ [L loc (E, σ ) ← E exp (E, σ )]) L x (E, σ ) def = E(x) L ⋆exp def = E exp E loc (E, σ ) def = σ • L loc (E, σ ) E &loc def = L loc L loc • f (E, σ ) def = L loc (E, σ ) + f
Figure 3: A small-step operational semantics for programs.

As an example rule, consider the case for an assignment loc = exp where ℓ pre and ℓ post are the control points before and after the assignment, respectively. We assume that the semantics of a location expression L loc is a function from memory states to addresses M → A and that the semantics of an expression E exp is a function from memory states to values M → V. Then, the transition relation for assignment simply updates the input store σ at the address given by loc with the value given by exp as shown in Figure 3. The evaluation of locations loc and expressions exp, that is, L loc (E, σ ) and E exp (E, σ ), respectively, can be defined by induction on their structure. The environment E is used to lookup the allocated address for program variables in L x . The value for a memory location E loc is obtained by looking up the contents in the store σ . Dereference ⋆exp and &loc mediate between address and value evaluation, while field offset loc • f is simply an address computation. The evaluation of the remaining expression forms is completely standard. Example 1 (Evaluating an assignment). Using the concrete memory state (E, σ ) shown in Figure 1, the evaluation of the assignment x -> a -> b = y • c proceeds as follows. First, the right-hand side gets evaluated by noting that E(y) = 0x...b0 and following

E y • c (E, σ ) = σ (L y • c (E, σ )) = σ (L y (E, σ ) + c) = σ (E(y) + c) = σ (0x...b8) = 178 .
Second, the left-hand side gets evaluated by noting that E(x) = 0x...a0 and then following the location evaluation

L x -> a -> b (E, σ ) = σ (σ (0x...a0) + a) + b) = σ (0x...b0 + a) + b = 0x...c0 + b = 0x...c4.
Finally, the store is updated at address 0x...c4 with the value 178 with σ [0x...c4 ← 178].

Concrete program semantical definitions:

Several notions of program semantics can be used as a basis for static analysis, which each depend on the desired properties and the kinds of invariants needed to establish them. A semantical definition expressed as the least fixed-point of a continuous function F over a concrete, complete lattice is particularly well-suited to the design of abstract interpreters [START_REF] Cousot | Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints[END_REF]. Following this analysis design methodology, an abstract interpretation consists of (1) choosing an abstraction of the concrete lattice (Section 3), (2) designing abstract operators that over-approximate the effect of the transition relation → p and concrete joins ∪ (Section 4), and (3) applying abstract operators to over-approximate F using widening (Section 5).

Definition 2 (A concrete domain). Let us fix a form for our concrete domains D to be the powerset of some set of concrete objects O, that is, let D = P(O). Domain D form a complete lattice with subset containment ⊆ as the partial order. Hence, concrete joins are simply set union ∪.

For a program p, let ℓ pre be its entry point (i.e., its initial control state). A standard definition of interest is the set of reachable states, which is sufficient for reasoning about safety properties.

Example 2 (Reachable states). We write p r for the set of reachable states of program p, that is,

p r def = {s | (ℓ pre , E, σ ) → ⋆ p s for some E ∈ E and σ ∈ H}
where → ⋆ p is the reflexive-transitive closure of the single-step transition relation →. Alternatively, p r can be defined as lfp F r , the least-fixed point of F r , where F r : P(S) → P(S) is as follows:

F r (S) def = {(ℓ pre , E, σ ) | E ∈ E and σ ∈ H} ∪ {s ′ | s ∈ S and s → p s ′ for some s ′ ∈ S} .
Note that we have let the concrete objects O be the execution states S in this example.

We can also describe the reachable states denotationally [START_REF] Schmidt | Abstract Interpretation From a Denotational-semantics Perspective[END_REF]-

p d (E, σ ) def = {s | (ℓ pre , E, σ ) → ⋆
p s}that enables a compositional way to reason about programs. Here, we let the set of concrete objects be functions from memory states to sets of states (i.e., M → P(S)).

Related work and discussion. For additional precision or for richer properties, it may be critical to retain some information about the history of program executions (i.e., how a state can be reached) [START_REF] Mauborgne | The trace partitioning abstract domain[END_REF]. In this case, we might choose a trace semantics as a concrete semantics where the concrete objects O are chosen to be traces T. For instance, the finite prefix traces semantics is defined by p t def = { s 0 , . . . , s n | s 0 : (ℓ pre , E 0 , σ 0 ) and s i → p s i+1 for some E 0 ∈ E, σ 0 ∈ H and for all 0 ≤ i < n}. Or we may to choose to define a trace semantics denotationally p dh : M → P(T) that maps input memory states into traces starting from them.

In this section, we have left the definition of a control state essentially abstract. A control state is simply a member of a set of labels on which an interpreter visits. In the intraprocedural setting, the control state is usually a point in the program text corresponding to a program counter. Since the set of program points is finite, the control state can be left unabstracted yielding a flow-sensitive analysis. Meanwhile, richer notions of control states are often needed for interprocedural analysis [START_REF] Milanova | Parameterized object sensitivity for points-to analysis for Java[END_REF][START_REF] Sharir | Two approaches to interprocedural data flow analysis[END_REF].

Abstraction of memory states

In this section, we discuss the abstraction of memory states, including environments and stores, as well as the values stored in them. A shape abstraction typically abstracts entire stores but only the pointer values (i.e., addresses) in them. In contrast, a numeric abstraction is typically applied only to the data values stored in program variables (i.e., the part of the store containing the global and local variables). We defer the abstraction of program executions to Section 5.

Following the abstract interpretation framework [START_REF] Cousot | Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints[END_REF], an abstraction or abstract domain is a set of abstract properties D ♯ together with a concretization function and sound abstract operators. Definition 3 (Concretization). A concretization function γ : D ♯ → D defines the meaning of D ♯ in terms of a concrete domain D = P(O) for some set of concrete objects O. An abstract inclusion

d ♯ 1 ⊑ d ♯ 2 for abstract elements d ♯ 1 , d ♯ 2 ∈ D ♯ should be sound with respect to concrete inclusion: γ(d ♯ 1 ) ⊆ γ(d ♯ 2 )
, and γ should be monotone. For each concrete operation f , we expect a sound abstract counterpart f ♯ ; for example, an abstract operation f ♯ : D ♯ → D ♯ is sound with respect to a concrete operation f :

D → D if and only if γ(d ♯ ) ⊆ γ • f ♯ (d ♯ ) for all d ♯ ∈ D ♯ .
In this section, we focus on the abstract domains and concretization functions, while the construction of abstract operations are detailed in Section 4.

An exact store abstraction based on separating shape graphs

An abstract heap σ ♯ ∈ H ♯ should over-approximate a set of concrete heaps with a compact representation. This set of abstract heaps H ♯ form the domain of abstract heaps (or the shape abstract domain). For simplicity, we first consider an exact abstraction of heaps with no unbounded dynamic data structures. That is, such an abstraction explicitly enumerates a finite number of memory cells and performs no summarization. Summarization is considered in Section 3.3.

A heap can be viewed as a set of disjoint cells (cf., Figure 1). At the abstract level, it is convenient to make disjointness explicit and describe disjoint cells independently. Thus, we write σ ♯ 0 * σ ♯ 1 for the abstract heap element that denotes all that can be partitioned into a sub-heap satisfying σ ♯ 0 and another disjoint sub-heap satisfying σ ♯ 1 . This observation about disjointness underlies separation logic [START_REF] Reynolds | Separation Logic: A Logic for Shared Mutable Data Structures[END_REF] and thus we borrow the separating conjunction operator * from there. An individual cell is described by an exact points-to predicate of the form α • f → β where α, β are symbolic variables (or, abstract values) drawn from a set V ♯ . The symbolic variable α denotes an address, while β represents the contents at the memory cell with address α • f (i.e., α offset by a field f). An exact heap abstraction is thus a separating conjunction of a set of exact points-to predicates. Such abstract heap predicates can be represented using separating shape graphs [START_REF] Chang | Shape Analysis with Structural Invariant Checkers[END_REF][START_REF] Laviron | Separating Shape Graphs[END_REF] where nodes are symbolic variables and edges represent heap predicates. An exact points-to predicate α • f → β is denoted by an edge from node α to node β with a label for the field offset f. For example, β a denotes the value corresponding to the C expression y • a.

The concretization γ H of a separating shape graph must account for symbolic variables that denote some concrete values, so it also must yield an instantiation or a valuation ν : V ♯ → V. Thus, this concretization has type γ H : H ♯ → P(H × (V ♯ → V)) and is defined as follows (by induction on the structure σ ♯ ):

γ H (α • f → β ) def = {([ν(α) + f → ν(β )], ν) | ν ∈ V ♯ → V} γ H (σ ♯ 0 * σ ♯ 1 ) def = {(σ 0 ⊎ σ 1 , ν) | (σ 0 , ν) ∈ γ H (σ ♯ 0 ) and (σ 1 , ν) ∈ γ H (σ ♯ 1 ) and dom(σ 0 ) ∩ dom(σ 1 ) = / 0} .
That is, an exact points-to predicate corresponds to a single cell concrete store under a valuation ν, and a separating conjunction of abstract heaps is a concrete store composed of disjoint sub-stores that are individually abstracted by the conjuncts under the same instantiation (as in separation logic [START_REF] Reynolds | Separation Logic: A Logic for Shared Mutable Data Structures[END_REF]). Symbolic variables can be viewed as existentially-quantified variables that are bound at the top-level of the abstraction. The valuation makes this explicit and thus is a bit similar to a concrete environment E.

Related work and discussion. Separating conjunction manifests itself in separating shape graphs as simply distinct edges. In other words, distinct edges denote disjoint heap regions. Separating shape graphs are visually quite similar to classical shape and points-to graphs [START_REF] Chase | Analysis of Pointers and Structures[END_REF][START_REF] Sagiv | Parametric shape analysis via 3-valued logic[END_REF] but are actually quite different semantically. In classical shape and points-to graphs, the nodes represent memory cells, and typically, a node corresponds to one-or-more concrete cells. Distinct nodes represent disjoint memory memory regions, and edges express variants of may or must points-to relations between two sets of cells. In contrast, it is the edges in separating shape graphs that correspond to disjoint memory cells, while the nodes simply represent values. We have found two main advantages of this approach. First, because there is no a priori requirement that two nodes be distinct values, we do not need to case split simply to speak about the contents of cells (e.g., consider two pointer variables x and y and representing to which objects they point; a classic shape graph must consider two cases where x and y are aliases or not, while a separating shape graph does not). Limiting case splits is critical to getting good analysis performance [START_REF] Chang | End-User Program Analysis[END_REF]. Second, a separating shape graph is agnostic to the type of values that nodes represent. Nodes may represent addresses, but they can just as easily represent non-address values, such as integer, Boolean, or floating-point values. We take advantage of this observation to interface with numeric abstract domains [START_REF] Chang | Relational inductive shape analysis[END_REF], which we discuss further next in Section 3.2.

Enriching shapes with a numeric abstraction

From Section 3.1, we have an exact heap abstraction based on a separating shape graph with a finite number of exact points-to edges. Intuitively, this abstraction is quite weak, as we have simply enumerated the memory cells of interest. We have, however, given names to all values-both addresses and contents-of potential interest. Here, we enrich the abstraction with information about the values contained in data structures, not just the pointer shape. We focus on scalar numeric values, such as integers or floatingpoint values, but other types of values could be handled similarly. A separating shape graph defines a set of symbolic variables corresponding to values, so we can abstract the values those symbolic variables represent. First, we consider a simple example, shown in Figure 5. In Figure 5, we show four concrete stores such that 0 ≤ x • a ≤ 10 and x • a ≤ 2(x • b) + 1. The separating shape graph on the right clearly abstracts the shape of the four stores (i.e., two fields a and b off a struct at variable x). The symbolic variables β a and β b represent the contents of cells x • a and x • b, respectively, so the numeric property specified above can expressed simply by using a logical formula involving β a and β b (as shown).

In general, a separating shape graph σ ♯ is defined over a set of symbolic variables

V ♯ [σ ♯ ] where V ♯ [σ ♯ ] ⊆ V ♯ .
The properties of the values stored in heaps described by σ ♯ can be characterized by

σ ♯ 0 σ ♯ 1 σ ♯ 2 σ ♯ 3 σ ♯ 4 D num σ ♯ 0 D num σ ♯ 1 D num σ ♯ 2 D num σ ♯ 3 D num σ ♯ 4 Figure 6:
The combined shape-numeric abstract domain is a cofibered layering of a numeric abstract domain on a shape abstract domain. logical formulas over V ♯ [σ ♯ ]. Such logical formulas expressing numeric properties can be represented using a numeric abstract domain

D num V ♯ [σ ♯ ] that abstracts functions from V ♯ [σ ♯ ] to V, that is, it comes with concretization function parametrized by a set of symbolic values V ♯ [σ ♯ ] of the following type: γ num V ♯ [σ ♯ ] : D num V ♯ [σ ♯ ] → P(V ♯ [σ ♯ ] → V).
For example, the numeric property mentioned in Figure 5 could be expressed using the convex polyhedra abstract domain [START_REF] Cousot | Automatic discovery of linear restraints among variables of a program[END_REF]. As a shape graph concretizes into a set of pairs composed of a heap σ and a valuation ν : V ♯ [σ ♯ ] → V, such numeric constraints simply restrict the set of admissible valuations.

The need to combine a shape graph with a numeric constraint suggests using a product abstraction [START_REF] Cousot | Systematic Design of Program Analysis Frameworks[END_REF] of a shape abstract domain H ♯ and a numeric abstract domain D num -. However, note that the numeric abstract domain that needs to be used depends on the separating shape graph, as the set of dimensions is equal to the set of nodes in the separating shape graph. Therefore, the conventional notion of a symmetric reduced product does not apply here. Instead, we use a different construction known as a cofibered abstract domain [START_REF] Venet | Abstract Cofibered Domains: Application to the Alias Analysis of Untyped Programs[END_REF] (in reference with the categorical notion underlying this construction). Definition 4 (Combined shape-numeric abstract domain). Given a shape domain H ♯ and a numeric domain D numparametrized by a set of symbolic variables. We let N ♯ denote the set of numeric abstract values corresponding to any shape graph (i.e., N

♯ def = {D num V | V ⊆ V ♯ })
, and we define the combined shape-numeric abstract domain H ♯ ⇒ N ♯ and its concretization γ

H ♯ ⇒N ♯ : (H ♯ ⇒ N ♯ ) → P(H×(V ♯ → V))
as follows:

H ♯ ⇒ N ♯ def = {(σ ♯ , ν ♯ ) | σ ♯ ∈ H ♯ and ν ♯ ∈ D num V ♯ [σ ♯ ] } γ H ♯ ⇒N ♯ (σ ♯ , ν ♯ ) def = {(σ , ν) | (σ , ν) ∈ γ H (σ ♯ ) and ν ∈ γ num V ♯ [σ ♯ ] (ν ♯ )}
This product is clearly asymmetric, as the left member defines the abstract lattice to which the right member belongs. We illustrate this structure in Figure 6. The left part depicts the lattice of abstract heaps, while the right part illustrates a lattice of numeric lattices. Each element of the lattice of lattices is an instance of the numeric abstract domain over the symbolic variables defined by the abstract heap, that is, it is the image of the function σ

♯ → D num V ♯ [σ ♯ ] .
This dependence is not simply theoretical but has practical implications on both the representation of abstract values and the design of abstract operations in the combined abstract domain. For instance, Figure 7 shows two separating shape graphs together with numerical invariants that represent the same set of concrete stores even though they use two different sets of symbolic variables (even up to α-renaming). Both of these combined shape-numeric abstract domain elements represent a store with two fields x • a and x • b such that x • a = x • b. In the right abstract domain element, the contents of both fields are associated with distinct nodes, and the values denoted by those nodes are constrained to be equal by the numeric domain. In the left graph, the contents of both fields are associated to the same node, which implies that they must be equal (without any constraint in the numeric domain). Now, with respect to the design of abstract operations in the combined abstract domain, the set of nodes in the shape graph will in general change during the course of the analysis. For instance, the analysis of an assignment of the value contained into field a to field b from the abstract state shown in the left produces the one in the right in Figure 8. After this transformation takes place, node δ becomes "garbage" or irrelevant, as it is not linked anywhere in the shape graph, and no numeric property is attached to it. This symbolic variable δ should thus be removed or projected from the numeric abstract domain. Other operations can cause new symbolic variables to be added, and this issue is only magnified with summaries (cf., Section 3.3). Thus, the combined abstract domain must take great care in ensuring the consistency of the numeric abstract values with the shape graphs, as well as dealing with graphs with different sets of nodes. Considering again the diagram in Figure 6, whenever two shape graphs are ordered σ ♯ 0 ⊑ σ ♯ 1 , there exists a symbolic variable renaming function

Φ σ ♯ 0 , σ ♯ 1 : V ♯ [σ ♯ 1 ] → V ♯ [σ ♯ 0 ]
that expresses a renaming of the symbolic variables from the weaker shape graph σ ♯ 1 to the stronger one σ ♯ 0 . For example, the symbolic renaming function Φ for the shape graphs shown in Figure 7 is

[α x → α x , β 1 → β 0 , δ 1 → β 0 ].
Related work and discussion. In practice, the implementation of the shape abstract domain takes the form of a functor (in the ML programming sense) that takes as input a module implementing a numeric domain interface (e.g., a wrapper on top of the APRON library [START_REF] Jeannet | Apron: A Library of Numerical Abstract Domains for Static Analysis[END_REF]) and outputs another module that implements the memory abstract domain interface. The construction that we have shown in this section is general to analyses where the set of symbolic variables is dynamic during the course of the analysis and where the inference of this set is bound to the inference of cell contents. In other words, it is wellsuited to applying shape analyses for summarizing memory cells and then reasoning about their contents with another domain. This construction has been used not only in Xisa [START_REF] Chang | Relational inductive shape analysis[END_REF] but also in a TVLA-based setup [START_REF] Mccloskey | Statically Inferring Complex Heap, Array, and Numeric Invariants[END_REF] and one based on a history of heap updates [START_REF] Chang | Abstract Interpretation with Alien Expressions and Heap Structures[END_REF].

Another approach that avoids this construction by performing a sequence of analyses: first, a shape analysis infers the set of symbolic variables; then, a numeric static analysis relies on this set [START_REF] Magill | Arithmetic Strengthening for Shape Analysis[END_REF][START_REF] Magill | Automatic numeric abstractions for heap-manipulating programs[END_REF]. While less involved, this approach prevents the exchange of information between both analyses, which is often required to achieve a satisfactory level of precision [START_REF] Chang | Relational inductive shape analysis[END_REF]. This sequencing of heap analysis followed by value analysis is similar to the application of a pre-pass pointer analysis followed by model checking over a Boolean abstraction exemplified in SLAM [START_REF] Ball | Automatic Predicate Abstraction of C Programs[END_REF] and BLAST [START_REF] Henzinger | Lazy abstraction[END_REF] 3.3 Enhancing store abstractions with summaries

So far, we have considered very simple abstract heaps described by separating shape graphs where all concrete memory cells are abstracted by exact points-to edges. To support abstracting a potentially unbounded number of concrete memory cells via dynamic memory allocation, we must extend abstract heaps with summarization, that is, a way of providing a compact abstraction for possibly unbounded, possibly non-contiguous memory regions. As an example, consider the concrete stores shown in the left part of Figure 9 consisting of a series of linked lists with 0, 1, and 2 elements. These concrete stores are just instances among infinitely many ones where x stores a reference to a list of arbitrary length. Each of these instances consist of two regions: the cell corresponding to variable x (green) and the list elements (blue). To abstract all of these stores in a compact and precise manner, we need to summarize the second region with a predicate. We can define such a predicate for summarizing such a region using an inductive definition list following the structure of lists:

α • list := (emp ∧ α = 0x0) ∨ (α • a → β 0 * α • b → β 1 * β 0 • list ∧ α = 0x0
). This definition notation is slightly non-standard to match the graphical notation: the predicate name is list and α is the formal induction parameter. A list memory region is empty if the root pointer α of the list is null, or otherwise, there is a head list element with two fields a and b such that the contents of cell α • a called β 0 is itself a pointer to a list. Then, in Figure 9, if variable x contains a pointer value denoted by β , the second region can be summarized by the inductive predicate instance β • list.

Furthermore, the three concrete stores are abstracted by the abstract heap α x → β * β • list (drawn as a graph to the right). The inductive predicate β • list is drawn as the bold, thick edge from node β .

Materialization:

The analyzer must be able to apply transfer functions on summarized regions. However, designing precise transfer functions on arbitrary summaries is extremely difficult. An effective approach is to define direct transfer functions only on exact predicates and then define transfer functions on summaries indirectly via materialization [START_REF] Sagiv | Solving Shape-Analysis Problems in Languages with Destructive Updating[END_REF] of exact predicates from them. In the following, we focus on the case where summaries are derived from inductive predicates [START_REF] Chang | Shape Analysis with Structural Invariant Checkers[END_REF] and thus call the materialization operation unfolding. In practice, unfolding should be guided by a specification of the summarized region where the analyzer needs to perform local reasoning on materialized cells (see Section 4.2). However, from the theoretical point of view, we can let an unfolding operator be defined as some function that replaces one abstract (σ ♯ , ν ♯ ) with a finite set of abstract elements (σ ♯ 0 , ν ♯ 0 ), . . . , (σ ♯ n-1 , ν ♯ n-1 ).

Definition 5 (Materialization). Let us write ⊆ (H ♯ ⇒ N ♯ ) × P fin (H ♯ ⇒ N ♯ ) for the unfolding relation.

Then, any unfolding of an abstract element should be sound with respect to concretization:

If (σ ♯ , ν ♯ ) (σ ♯ 0 , ν ♯ 0 ), . . . , (σ ♯ n-1 , ν ♯ n-1 ) , then γ H ♯ ⇒N ♯ (σ ♯ , ν ♯ ) ⊆ 0≤i<n γ H ♯ ⇒N ♯ (σ ♯ i , ν ♯ i ) .
As seen above, the finite set of abstract elements that results from materialization represents a disjunction of abstract elements (i.e., materialization is a form of case analysis). For precision, we typically want an equality instead of inclusion in the conclusion, which motivates a need to represent a disjunction of abstract elements (cf., Section 3.4).

Example 3 (Unfolding an inductively-defined list). For instance, the abstract element from H ♯ ⇒ N ♯ depicted in Figure 9 can be unfolded to two elements:

(α x → β * β • list, ⊤) (α x → β , β = 0x0), (α x → β * β • a → β 0 * β • b → β 1 * β 0 • list, β = 0x0) ,
which means that the list pointer β is either a null pointer or points to a list element whose a field contains a pointer to another list. Related work and discussion. Historically, the idea of using compact summaries for an unbounded number of concrete memory cells goes back to at least Jones and Muchnick [START_REF] Jones | Flow Analysis and Optimization of LISP-like Structures[END_REF], though the set of abstract locations was fixed a priori before the analysis. Chase et al. [START_REF] Chase | Analysis of Pointers and Structures[END_REF] considered dynamic summarization during analysis, while Sagiv et al. [START_REF] Sagiv | Solving Shape-Analysis Problems in Languages with Destructive Updating[END_REF] introduced materialization. We make note of existing analysis algorithms that make use of summarization-materialization. TVLA summary nodes [START_REF] Sagiv | Parametric shape analysis via 3-valued logic[END_REF] represent unbounded sets of concrete memory cells with predicates that express universal properties of all the concrete cells they denote. The use of three-valued logic enables abstraction beyond a set of exact points-to constraints (i.e., the separating shape graphs in Section 3.1 are akin to two-valued structures in TVLA), and summarization is controlled by instrumentation predicates that limits the compaction done by canonical abstraction. Fixed list segment predicates [START_REF] Berdine | Shape Analysis for Composite Data Structures[END_REF][START_REF] Distefano | A Local Shape Analysis Based on Separation Logic[END_REF] characterize consecutive chains of list elements by its first and last pointers. Thus, a predicate of the form ls(α, α ′ ) denotes all chains of list elements (of any length) starting at α and ending at α ′ . Then, an abstract heap consists of a separating conjunction of points-to predicates (Section 3.1) and list segments. These predicates can be generalized to other structure segments. Inductive predicates [START_REF] Chang | Relational inductive shape analysis[END_REF][START_REF] Chang | Shape Analysis with Structural Invariant Checkers[END_REF] generalize the list segment predicates in several ways. First, the abstract domain may be parametrized by a set of user-supplied inductive definitions. Note that as parameters to the abstract domain and thus the analyzer, the inductive definitions specify possible templates for summarization. A sound analysis can only infer a summary predicate essentially if it exhibits an exact instance of the summary. The "correctness" of such inductive definitions are not assumed, but rather a disconnect between the user's intent and the meaning an inductive predicate could lead to unexpected results. Second, inductive predicates can correspond to complete structures (e.g., a tree that is completely summarized into a single abstract predicate), whereas segments correspond to incomplete structures characterized by a missing sub-structure. Inductive predicates can be generically lifted to unmaterializable segment summaries [START_REF] Chang | Shape Analysis with Structural Invariant Checkers[END_REF] or materializable ones [START_REF] Chang | Relational inductive shape analysis[END_REF]. Independently, array region predicates [START_REF] Gopan | A framework for numeric analysis of array operations[END_REF] have been used to describe the contents of zones in arrays. Some analyses on arrays and containers have used index variables into summaries instead of explicit materialization operations [START_REF] Dillig | Precise reasoning for programs using containers[END_REF][START_REF] Gulwani | Lifting abstract interpreters to quantified logical domains[END_REF][START_REF] Halbwachs | Discovering properties about arrays in simple programs[END_REF].

Lifting store abstractions to disjunctive memory state abstractions

At this point, we have described an abstraction framework for concrete stores σ . To complete an abstraction for memory states m : (E, σ ), we need two things: (1) an abstract counterpart to E and (2) a disjunctive abstraction for when a single abstract heap σ ♯ is insufficient for precisely abstracting the set of possible concrete stores.

Abstract environments: Since the abstract counterpart for addresses are symbolic variables (or nodes) in shape graphs, an abstract environment E ♯ can simply be a function mapping program variables to nodes, that is, E ♯ ∈ E ♯ = X → V ♯ . Now, the memory abstract domain M ♯ is defined by M ♯ = E ♯ × (H ♯ ⇒ N ♯ ), and its concretization γ M : M ♯ → P(E × H) can be defined as follows:

γ M (E ♯ , (σ ♯ , ν ♯ )) def = {(ν • E ♯ , σ ) | (σ , ν) ∈ γ H (σ ♯ ) and ν ∈ γ num V ♯ [σ ♯ ] (ν ♯ )} .
Note that in an abstract memory state m ♯ : (E ♯ , σ ♯ ), the abstract environment E ♯ simply gives the sym- bolic address of program variables, while the abstract heap σ ♯ abstracts all memory cells-just like the concrete model in Section 2.2. We let the abstract environment be depicted by node labels in the graphical representation of abstract heaps. For instance, the concrete memory state shown in Figure 1 can be described by the diagram in Figure 10.

Disjunctive abstraction: Recall that the unfolding operation from Section 3.3 generates a finite disjunction of abstract facts-specifically, combined shape-numeric abstract elements {. . . , (σ ♯ i , ν ♯ i ), . . .} ⊆ H ♯ ⇒ N ♯ . Thus, a disjunctive abstraction layer is required regardless of other analysis reasons (e.g., path-sensitivity). We assume the disjunctive abstraction is defined by an abstract domain M ♯ ∨ and a concretization function γ ∨ : M ♯ ∨ → P(M). We do not prescribe any specific disjunctive abstraction. A simple choice is to apply a disjunctive completion [START_REF] Cousot | Systematic Design of Program Analysis Frameworks[END_REF], but further innovations might be possible by taking advantage of being specific to memory. Example 4 (Disjunctive completion). For a memory abstract domain M ♯ , its disjunctive completion M ♯ ∨ is defined as follows:

M ♯ ∨ def = P fin (M ♯ ) γ ∨ (s ♯ ) def = {γ M (m ♯ ) | m ♯ ∈ s ♯ } .
In Figure 11, we sum up the structure of the abstract domain for abstracting memory states M as a stack of layers, which are typically implemented as ML-style functors. Each layer corresponds to the abstraction of a different form of concrete semantics (as shown in the diagram).

Related work and discussion. Trace partitioning [START_REF] Mauborgne | The trace partitioning abstract domain[END_REF] relies on control-flow history to manage disjunctions, which could be used as an alternative to disjunctive completion. However, it is a rather general construction and can be instantiated in multiple ways with a large effect on precision and performance.

Static analysis operations

In this section, we describe the main abstract operations on the memory abstract domain M ♯ and demonstrate how they are computed through the composition of abstract domains discussed in Section 3. Our presentation describes each kind of operation (i.e., transfer functions for commands like assignment, abstract comparison, and abstract join) one by one and shows how unfolding and folding operations are triggered by their application. The end result of this discussion is a description of how these domains implement the interfaces shown in Figure 12. For these interfaces, we let B denote the set of booleans {true, false} and U denote an undefined value for some functions that may fail to produce a result. We write X U for X ⊎ {U} for any set X (i.e., an option type).

shape abstract domain γ H : H ♯ → P(H × (V ♯ → V)) numeric abstract domain γ num V ♯ [σ ♯ ] : D num V ♯ [σ ♯ ] → P(V ♯ [σ ♯ ] → V) combined shape-numeric abstract domain γ H ♯ ⇒N ♯ : (H ♯ ⇒ N ♯ ) → P(H × (V ♯ → V)) memory abstract domain γ M : M ♯ → P(M) M ♯ = E ♯ × (H ♯ ⇒ N ♯ ) disjunctive abstract domain γ ∨ : M ♯ ∨ → P(M)
Figure 11: Layers of abstract domains to yield a disjunctive memory state abstraction. From an implementation perspective, the edges correspond to inputs for ML-style functor instantiations.

Assignment over materialized cells

First, we consider the transfer function for assignment. In this subsection, for simplicity, we focus on the case where none of the locations that appear in either side of the assignment are summarized, and we defer the case of transfer functions over summarized graph regions to Section 4.2. Because of this simplification, the types of the abstract operators mentioned will not exactly match those given in Figure 12.

At the same time, this transfer function captures the essence of the shape-numeric combination.

Recall that loc ∈ L X and exp ∈ E X are location and value expressions, respectively, in our programming language (cf., Figure 2). The transfer function assign mem : L X × E X × M ♯ → M ♯ should compute a sound post-condition for the assignment command loc = exp stated as follows:

Condition 1 (Soundness of assign mem ). If (E, σ ) ∈ γ M (m ♯ ), then (E, σ [L loc (E, σ ) ← E exp (E, σ )]) ∈ γ M (assign mem (loc, exp, m ♯ )) .
Assignments of the form loc = loc ′ . Let us first assume that right hand side of the assignment is a location expression. As an example, consider the assignment shown in Figure 13 and applying assign mem to the pre-condition on the left to yield the post-condition on the right. The essence is that loc dictates an edge that should be updated to point to the node specified by loc ′ .

To compute a post-condition in this case, assign mem should update the abstract heap, that is, the preheap σ ♯ ∈ H ♯ . An assign mem call should eventually forward the assignment to the heap abstract domain via the eval[l] shape operation that evaluates a location expression loc to an edge, eval[e] shape that evaluates a value expression exp to a node, and mutate shape that swings a points-to edge.

The base of a sequence of pointer dereferences is given by a program variable, so the first step consists of replacing the program variables in the assignment with the symbolic names corresponding to their addresses using the abstract environment E ♯ . For our example, this results in the call to assign comb (α 0 -> a • b, α 0 • b, (σ ♯ , ν ♯ )) at the combined shape-numeric layer, which should satisfy a soundness condition similar to that of assign mem (Condition 1). The next step consists of traversing the abstract heap σ ♯ LOCADDRESS

• A shape abstract domain H ♯ eval[l] shape : L V ♯ × H ♯ -→ (V ♯ × F × H ♯ ) U eval[e] shape : E V ♯ × H ♯ -→ (V ♯ × H ♯ ) U mutate shape : V ♯ × F × V ♯ × H ♯ -→ H ♯ U unfold shape : (L V ♯ × F) × H ♯ -→ P fin (H ♯ × E V ♯ ) new shape : V ♯ × H ♯ -→ H ♯ delete[n] shape : V ♯ × H ♯ -→ H ♯ delete[e] shape : V ♯ × F × H ♯ -→ H ♯ compare shape : (V ♯ → V ♯ ) × H ♯ × H ♯ -→ {false} ⊎ {true} × (V ♯ → V ♯ ) join shape : ((V ♯ ) 2 → V ♯ ) × H ♯ × H ♯ -→ H ♯ × (V ♯ → V ♯ ) 2 widen shape : ((V ♯ ) 2 → V ♯ ) × H ♯ × H ♯ -→ H ♯ × (V ♯ → V ♯ ) 2 • A numeric abstract domain over symbolic variables N ♯ assign num : L V ♯ × E V ♯ × N ♯ -→ N ♯ guard num : E V ♯ × N ♯ -→ N ♯ new num : V ♯ × N ♯ -→ N ♯ delete[n] num : V ♯ × N ♯ -→ N ♯ rename num : (V ♯ → V ♯ ) × N ♯ -→ N ♯ compare num : N ♯ × N ♯ -→ B join num : N ♯ × N ♯ -→ N ♯ widen num : N ♯ × N ♯ -→ N ♯ • A combined shape-numeric abstract domain H ♯ ⇒ N ♯ assign comb : L V ♯ × E V ♯ × H ♯ ⇒ N ♯ -→ P fin (H ♯ ⇒ N ♯ ) U guard comb : E V ♯ × (H ♯ ⇒ N ♯ ) -→ P fin (H ♯ ⇒ N ♯ ) U unfold comb : L V ♯ × H ♯ ⇒ N ♯ -→ P fin (H ♯ ⇒ N ♯ ) U alloc comb : L V ♯ × F * × (H ♯ ⇒ N ♯ ) -→ P fin (H ♯ ⇒ N ♯ ) U free comb : L V ♯ × F * × (H ♯ ⇒ N ♯ ) -→ P fin (H ♯ ⇒ N ♯ ) U compare comb : (V ♯ → V ♯ ) × (H ♯ ⇒ N ♯ ) × (H ♯ ⇒ N ♯ ) -→ {false} ⊎ {true} × (V ♯ → V ♯ ) join comb : ((V ♯ ) 2 → V ♯ ) × (H ♯ ⇒ N ♯ ) × (H ♯ ⇒ N ♯ ) -→ (H ♯ ⇒ N ♯ ) widen comb : ((V ♯ ) 2 → V ♯ ) × (H ♯ ⇒ N ♯ ) × (H ♯ ⇒ N ♯ ) -→ (H ♯ ⇒ N ♯ ) • A memory abstract domain M ♯ assign mem : L X × E X × M ♯ -→ P fin (M ♯ ) U guard mem : E X × M ♯ -→ P fin (M ♯ ) U alloc mem : L X × F * × M ♯ -→ P fin (M ♯ ) U free mem : L X × F * × M ♯ -→ P fin (M ♯ ) U compare mem : M ♯ × M ♯ -→ B join mem : M ♯ × M ♯ -→ M ♯ widen mem : M ♯ × M ♯ -→ M ♯
eval[l] shape (α, σ ♯ ) = (α, / 0) LOCFIELD eval[l] shape (loc, σ ♯ ) = (α, f) eval[l] shape (loc • g, σ ♯ ) = (α, f + g) VALDEREFERENCE eval[l] shape (loc, σ ♯ ) = (α, f) σ ♯ = σ ♯ 0 * α • f → β eval[e] shape (loc, σ ♯ ) = β LOCVAL eval[e] shape (exp, σ ♯ ) = α eval[l] shape (⋆exp, σ ♯ ) = (α, / 0) VALLOC eval[l] shape (loc, σ ♯ ) = (α, / 0)
eval[e] shape (&loc, σ ♯ ) = α according to the location expression and the value expression of the assignment. As mentioned above, this evaluation is performed using the location evaluation function eval[l] shape that yields an edge and the value expression evaluation function eval[e] shape that yields a node.

Condition 2 (Soundness of eval[l] shape and eval[e] shape ). Let (σ , ν) ∈ γ H (σ ♯ ). Then,

If eval[l] shape (loc, σ ♯ ) = (α, f) , then L loc (σ ) = ν(α) + f . If eval[e] shape (loc, σ ♯ ) = β , then E loc (σ ) = ν(β ) .
In Figure 14, we define eval[l] shape and eval[e] shape following the syntax of location and value expressions (over symbolic variables). We write / 0 for a designated 0-offset field. This abstract evaluation corresponds directly to the concrete evaluation defined in Figure 3. Note that abstract evaluation is not necessarily defined for all expressions. For example, an points-to edge may simply not exist for the computed address in VALDEREFERENCE. The edge may need to be materialized by unfolding (cf., Section 4.2) or otherwise is a potential memory error.

Returning to the example in Figure 13, we get eval[l] shape (α 0 -> a • b, σ ♯ ) = (α 1 , b)-the cell being assigned-to corresponds to the exact points-to edge α 1 • b → α 4 -and eval[e] shape (α 0 • b) = α 2 -the value to assign is abstracted by α 2 . The abstract post-condition returned by assign comb should reflect the swinging of that edge in the shape graph, which is accomplished by the mutate shape function:

mutate shape (α, f, β , (α • f → δ ) * σ ♯ ) = (α • f → β ) * σ ♯ .
This function simply replaces a points-to edge named by the address α and field f with a new one for the updated contents (and fails if such a points-to edge does not exist in the abstract heap σ ♯ ). The effect of this assignment can be completely reflected in the abstract heap since the cell corresponding to the assignment is abstracted by exactly one points-to edge and the new value to store in that cell is also exactly abstracted by one node. We note that node α 4 is no longer reachable in the shape graph, and thus the value that this node denotes is no longer relevant when concretizing the abstract state. As a consequence, it can be safely removed both in H ♯ (using function delete[n] shape ) and in N ♯ (using function Modular Construction of Shape-Numeric Analyzers delete[n] num ). Such an existential projection or "garbage collection" step may be viewed as a conversion operation in the cofibered lattice structure shown in Figure 6.

Assignments of the form loc = exp. In general, the right-hand side of an assignment is not necessarily a location expression. The evaluation of left-hand side loc proceeds as above, but the evaluation of the right-hand side expression exp is extended. As an example, consider the assignment shown in Figure 15.

The evaluation of the location expression down to the abstract heap level works as before where we find that eval[l] shape (α 0 • c, σ ♯ ) = (α 0 , c). For the right-hand-side expression, it is not obvious what eval[e] shape (α 0 •b+ 1, σ ♯ ) should return, as no symbolic node is equal to that value in the concretization of all elements of σ ♯ . It is possible to evaluate sub-expression α 0 • b to α 2 , but then eval[e] shape (α 2 + 1, σ ♯ ) cannot be evaluated any further. The solution is to create a new symbolic variable and constrain it to represent the value of the right-hand-side expression. Therefore, the evaluation of assign comb proceeds as follows: (1) generate a fresh node α 4 ; (2) add α 4 to the abstract heap σ ♯ and the numeric abstract value ν ♯ using the function new shape and new num , respectively; (3) update the numeric abstract value ν ♯ using assign num (α 4 , α 2 + 1, ν ♯ ), which over-approximates constraining α 4 = α 2 + 1; and (4) mutate with mutate shape with the new node α 4 (i.e., mutate shape (α 0 , c, α 4 , σ ♯ )).

Unfolding and assignment over summarized cells

struct list { struct list ⋆ next; int d; }; α • list := (emp ∧ α = 0x0) ∨ (α • next → β 0 * α • d → β 1 * β 0 • list ∧ α = 0x0)
We now consider assign mem in the presence of summary predicates, which intuitively "get in the way" of evaluating location and value expressions in a shape graph. For instance, consider trying to apply the assignment shown in Figure 16. On the left, we have a separating shape graph where α 2 is a list described by the inductive defi- nition shown inset. For clarity, we also show the C-style struct definition that corresponds to the layout of each list element. In applying the assignment, the evaluation of the right-hand-side expression x -> next fails. While x evaluates to node α 2 , there is no points-to edge from α 2 . Thus, eval[e] shape (α 0 -> next) fails. It is clear that the reason for this failure is that the memory cell corresponding to the right-handside expression is summarized as part of the α 2 • list predicate. To materialize this cell, this predicate should be unfolded; then, the assignment can proceed as in the previous section (Section 4.1). We can now describe the transfer function for assignment assign mem (loc, exp, (σ ♯ , ν ♯ )) in general:

1. It should call the underlying assign comb and follow the process described previously in Section 4.1.

If evaluation via eval[l] shape or eval[e] shape fail, then they should return a failure address, which consists of a pair (β , f) corresponding to the node and field offset that does not have a materialized points-to edge. In the example in Figure 16, the failure address is (α 2 , next). Note that the interface for evaluation shown in Figure 16 does not show the contents of the failure case for simplicity. 2. Then, assign comb in the combined domain performs an unfolding of the abstract heap by calling a function unfold shape that implements the unfolding relation with the target points-to edge to materialize (β , f). Condition 3 (Soundness of unfold shape ).

γ H (σ ♯ ) ⊆ {(σ , ν) ∈ γ H (σ ♯ u ) | (σ ♯ u , exp u ) ∈ unfold shape ((β , f), σ ♯ ) and exp u (ν) = true} .
Note that unfolding of an abstract heap returns pairs consisting of an unfolded abstract heap and a numeric constraint as an expression

exp u ∈ E V ♯ [σ ♯ u ]
over the symbolic variables of the unfolded abstract heap. This expression allows a summary to contain constraints not expressible in a shape graph itself. For instance, in the list inductive definition, each case comes with a nullness or nonnullness condition on the head pointer. Or more interestingly, we can imagine an orderedness constraint for an inductive definition describing an ordered list. For the example from Figure 16, unfolding the shape graph at (α 2 , next) generates two disjuncts, but the one corresponding to the empty list can be eliminated due to the constraint that α 2 has to be non-null. 3. The numeric constraints should be evaluated in the numeric abstract domain using a condition test operator guard num . Condition 4 (Soundness of guard num ). Let V ⊆ V ♯ , ν ♯ ∈ D num V , and ν ∈ γ num V (ν ♯ ). Then, If exp (ν) = true , then ν ∈ γ num V (guard num (exp, ν ♯ )) .

Thus, the initial abstract state in the combined domain (σ ♯ , ν ♯ ) ∈ H ♯ ⇒ N ♯ can be over-approximated by the following finite set of abstract states:

unfold comb (loc, (σ ♯ , ν ♯ )) def = {(σ ♯ u , guard num (exp u , ν ♯ )) | (σ ♯ u , exp u ) ∈ unfold shape ((β , f), σ ♯ )} 4.
Finally, assign comb should perform the same set of operations as described in Section 4.1 to reflect the assignment on each unfolded heap. The assign comb returns a finite set of elements because of potential unfolding (and similarly for assign mem ). The soundness condition for assign mem is therefore as follows.

Condition 5 (Soundness of assign mem ). Let (E, σ ) ∈ γ M (m ♯ ). Then,

(E, σ [L loc (E, σ ) ← E exp (E, σ )]) ∈ {γ M (m ♯ u ) | m ♯ u ∈ assign mem (loc, exp, m ♯ )} .
A very similar soundness condition applies to assign comb . Figure 16 shows the resulting abstract state for the assignment after unfolding and mutation on the right. In certain cases, the unfolding process may have to be performed multiple times due to repeated failures of calling eval[l] shape and eval[e] shape as shown in Chang and Rival [START_REF] Chang | Relational inductive shape analysis[END_REF]. This behavior is expected, as unfolding may fail to materialize the correct region, and thus, termination should be enforced with a bound on the number of unfolding steps.

Other transfer functions

Unfolding is also the basis for most other transfer functions. Once the points-to edges in question are materialized, their definition is straightforward as it was for assignment (cf., Section 4.1).

• Condition test. The abstract domain M ♯ should define an operator guard mem that takes an expression (of Boolean type) and an abstract value and then returns an abstract value that has taken into account the effect of the guard expression. Just like with assignment, this function may need to perform an unfolding and thus returns in general a finite set of abstract states. Condition 6 (Soundness of guard mem ). Let m ∈ γ M (m ♯ ). Then,

If exp (m) = true , then m ∈ {γ H (σ ♯ u ) | σ ♯ u ∈ γ M (guard mem (exp, m ♯ ))} .
It applies the transfer function assign num provided by N ♯ satisfying a similar soundness condition, which is fairly standard (e.g., the APRON library provides such a function). • Memory allocation. Transfer function alloc mem accounts for the allocation of a fresh memory block, and the assignment of the address of this block to a given location. Given abstract precondition σ ♯ , the abstract allocation function alloc mem (loc, [f 1 , . . . , f n ], σ ♯ ) returns a sound abstract post-condition for the statement loc = malloc({f 1 , . . . , f n }). • Memory deallocation. Similarly, transfer function free mem accounts for freeing the block pointed to by an instruction such as free. It takes as argument a location pointing to the block being freed, a list of fields, and the abstract pre-condition. It may also need to perform unfolding to materialize the location. It calls free comb in the H ♯ ⇒ N ♯ level, which then materializes pointsto edges corresponding to the block to remove and deletes them from the graph using function delete[e] shape defined by delete[e] shape (α, f, α

• f → β * σ ♯ 0 ) = σ ♯ 0 .
After removing these edges, some symbolic nodes may become unreachable in the graph and should be removed using delete[n] shape and delete[n] num . The analysis of a more full featured programming language would require additional classical transfer functions, such as support for variable creation and deletion, though this can be supported completely at the memory abstract domain M ♯ layer with the abstract environment E ♯ .

As an example of a condition test, consider applying guard mem in Figure 17. In the same way as for the example assignment of Figure 16, the first attempt to compute guard comb (α 2 -> next = 0x0, σ ♯ ) fails, as there is no points-to edge labeled with next starting from node α 2 . Thus guard comb must first call unfold comb . The unfolding returns a pair of abstract elements, yet the one corresponding to the case where the list is empty does not need to be considered any further due to the numerical constraint α 2 = 0x0. Therefore, only the second abstract elements remains, which corresponds to a list with the first element materialized. At this stage, expression α 2 -> next can be evaluated. Finally, the condition test is reflected by applying guard num in the numerical abstract domain N ♯ .

m ♯ 0 : (E ♯ 0 , (σ ♯ 0 , ν ♯ 0 )) α0 x α2 α4 α5 α6 α7 α1 y α3 next d next d list ∧ α 3 ≤ α 5 ∧ α 5 ≤ α 7 ⊑ m ♯ 1 : (E ♯ 1 , (σ ♯ 1 , ν ♯ 1 )) α ′ 0 x α ′ 2 α ′ 4 α ′ 5 α ′ 1 y α ′ 3 next d list ∧ α ′ 3 ≤ α ′ 5
Figure 18: An abstract inclusion that holds and shows the need for a node relation Φ. In both abstract heaps, variable x points to a list and y points to a number. On the left, the abstract heap describes a list with at least two elements, while on the right, it describes one with at least one element. The number pointed to by y is less than or equal to the data field d of the first element in both abstract heaps. The data field of the first element is less than or equal to the data field of the second in the left abstract heap.

Abstract comparison

Abstract interpreters make use of inclusion testing operations in many situations, such as checking that an abstract post-fixed point has been reached in a loop invariant computation or that some, for example, user-supplied post-condition can be verified with the analysis results. As inclusion is often not decidable, the comparison function is not required to be complete but should meet a soundness condition:

Condition 7 (Soundness of compare mem ). If compare mem (m ♯ 0 , m ♯ 1 ) = true, then γ M (m ♯ 0 ) ⊆ γ M (m ♯ 1 )
The implementation of such an operator is complicated by the fact that the underlying abstract heaps may have distinct sets of symbolic nodes. This issue is a manifestation of the the cofibered abstract domain construction (Section 3.2). The concretizations of all abstract domains below H ♯ ⇒ N ♯ make use of valuations, and thus the inclusion checking operator needs to account for a relation between the symbolic nodes of the graphs. This relation between nodes in two graphs Φ is computed step-by-step during the course of the inclusion checking.

The example in Figure 18 illustrates these difficulties. It is quite intuitive that any state in the concretization of m ♯ 0 is also in the concretization of m ♯ 1 . To see the role of the node relation Φ, let us consider concretizations of m ♯ 0 and m ♯ 1 . Clearly, if concrete state (E, σ ) is in the concretization of m ♯ 0 and in the concretization of m ♯ 1 , then node α 0 in m ♯ 0 and α ′ 0 denotes the address of x. Thus α 0 and α ′ 0 denote the same value, that is, valuations used as part of the concretization should map those two nodes to the same value. The Φ should relate these two nodes akin to a unification substitution. Similarly, α 2 and α ′ 2 both denote the value stored in variable x, thus should be related in Φ. On the other hand, node α 6 of abstract state m ♯ 0 has no counterpart in m ♯ 1 -it corresponds to a null or non-null address in the region summarized by the inductive edge.

We notice Φ can be viewed as a map from nodes in m ♯ 1 to nodes of m ♯ 0 and in this example, defined by Φ(α ′ i ) = α i for 0 ≤ i ≤ 5. Also, we notice that mapping Φ can be derived step-by-step, starting from the abstract environments. Thus, compare shape and compare comb each take as a parameter a set of pairs of symbolic nodes that should be related in Φ. We call this initial set the roots, as they are used as a starting point in the computation of Φ.

We can now describe the steps of computing compare mem (m ♯ 0 :

(E ♯ 0 , (σ ♯ 0 , ν ♯ 0 )), m ♯ 1 : (E ♯ 1 , (σ ♯ 1 , ν ♯ 1 ))): 1. First, an initial node mapping Φ : V ♯ [σ ♯ 1 ] → V ♯ [σ ♯ 0 ] is derived from the abstract environments: Φ def = E ♯ 0 •(E ♯ 1 ) -1
. This definition states that the addresses of the program variables in m ♯ 1 correspond to the respective addresses of the program variables in m ♯ 0 . It is well-defined, as two distinct Recall from Sections 3.3 and 4.2 that unfolding returns a finite set of abstract elements interpreted disjunctively and thus justifies the need for a disjunctive abstraction layer-independent of other possible reasons like a desire for path-sensitivity. In this subsection, we describe the interface for a disjunctive abstraction layer M ♯ ∨ shown in Figure 20 that sits above the memory layer M ♯ .

m ♯ 0 : (E ♯ 0 , (σ ♯ 0 , ν ♯ 0 )) α0 x α2 α4 α5 α1 y α3 next d list list ⊔ m ♯ 1 : (E ♯ 1 , (σ ♯ 1 , ν ♯ 1 )) α ′ 0 x α ′ 2 α ′ 1 y α ′ 3 α ′ 4 α ′ 5 next d list list =⇒ m ♯ ⊔ : (E ♯ ⊔ , (σ ♯ ⊔ , ν ♯ ⊔ )) α ′′ 0 x α ′′ 2 α ′′ 1 y α ′′ 4.6 Disjunctive abstract domain interface partition ∨ : C × P fin (M ♯ ∨ ) -→ M ♯ ∨ collapse ∨ : C × M ♯ ∨ -→ M ♯ ∨ assign ∨ : C × L X × E X × M ♯ ∨ -→ M ♯ ∨ guard ∨ : C × E X × M ♯ ∨ -→ M ♯ ∨ alloc ∨ : C × L X × N × M ♯ ∨ -→ M ♯ ∨ free ∨ : C × L X × N × M ♯ ∨ -→ M ♯ ∨ compare ∨ : M ♯ ∨ × M ♯ ∨ -→ B join ∨ : M ♯ ∨ × M ♯ ∨ -→ M ♯ ∨ widen ∨ : M ♯ ∨ × M ♯ ∨ -→ M ♯ ∨
The following discussion completes the picture of the abstract domain interfaces (cf., Figure 11). There are two main differences in the interface as compared to the one for M ♯ . First, the disjunctive abstract domain should provide two additional operations partition ∨ and collapse ∨ that create and collapse partitions, respectively. A partition represents a disjunctive set of base domain elements. Second, the transfer functions take an additional context information parameter c ∈ C that can be used in M ♯ ∨ to tag each disjunct with how it arose in the course of the abstract interpretation. Condition 10 (Soundness of partition ∨ and collapse ∨ ). Let s ♯ : M ♯ ∨ and S ♯ : P fin (M ♯ ∨ ).

{γ ∨ (s ♯ ) | s ♯ ∈ S ♯ } ⊆ γ ∨ (partition ∨ (c, S ♯ )) γ ∨ (s ♯ ) ⊆ γ ∨ (collapse ∨ (c, s ♯ ))

Note that contexts play no role in the concretization, but operations can use them, for example, to decide which disjuncts to merge using join mem and which disjuncts to preserve. Transfer functions assign ∨ , guard ∨ , alloc ∨ , and free ∨ all follow the same structure. They first call the underlying operation on the memory abstract domain M ♯ and then apply the partition ∨ partition on the output. For instance, assign ∨ is defined as follows while satisfying the expected soundness condition: (soundness)

Inclusion (compare ∨ ), join, and widening operations should satisfy the usual soundness conditions. The collapse ∨ operator may be used to avoid generating too many disjuncts (and termination of the analysis).

A compositional abstract interpreter

In this section, we assemble an abstract interpreter for the language defined in Section 2 using the abstraction set up in Section 3 and the interface of abstract operations described in Section 4.

The abstract semantics of a program p is a function p ♯ : M ♯ ∨ → M ♯ ∨ , which takes an abstract precondition as input and produces an abstract post-condition as output. Based on an abstract interpretation of the denotational semantics of programs [START_REF] Schmidt | Denotational semantics: a methodology for language development[END_REF][START_REF] Schmidt | Abstract Interpretation From a Denotational-semantics Perspective[END_REF], we can define the abstract semantics by induction over the syntax of programs as shown in Figure 21 in a completely standard manner. We let C [. . .] stand for computing some context information based on, for example, the control state ℓ and/or the branch taken. This context information may be used, for instance, by the disjunctive domain M ♯ ∨ to guide trace partitioning [START_REF] Mauborgne | The trace partitioning abstract domain[END_REF]. The abstract transitions for sequencing, assignment, dynamic memory allocation, and deallocation are straightforward with the latter three calling the corresponding transfer function in the top-layer abstract domain M ♯ ∨ . For if, the pre-condition is first constrained by the guard condition via guard ∨ to interpret the two branches and then the resulting states are joined via join ∨ . For while, we write lfp ♯ for an abstract post-fixed-point operator. The lfp ♯ operator relies on widen ∨ to terminate and on compare ∨ to verify the stability of the abstract post-fixed point. It may also use join ∨ to increase the level of precision when computing the first iterations. We omit a full definition of lfp ♯ as there are many well-known ways to obtain such an operator. The most simple one consists of applying only widen ∨ until stabilization can be shown by compare ∨ . We simply state its soundness condition:

Condition 11 (Soundness of lfp ♯ ). For all concrete transformers F : P(S) → P(S) monotone, all abstract transformers F ♯ : M ♯ ∨ → M ♯ ∨ , and all abstract states

s ♯ ∈ M ♯ ∨ , if F • γ ∨ ⊆ γ ∨ • F ♯ , then lfp γ ∨ (s ♯ ) F ⊆ γ ∨ (lfp ♯ s ♯ F ♯ ) .
We write lfp S for the least post-fixed point that is at least S and similarly for lfp ♯ s ♯ . Finally, the static analysis is sound in the following sense: Theorem 1 (Soundness of the analysis). Let p be a program, and let s ♯ ∈ M ♯ ∨ be an abstract precondition. Then, the result of the analysis is sound: ∀s ∈ γ ∨ (s ♯ ), p d (s) ⊆ γ ∨ ( p ♯ (s ♯ )) .

Soundness can be proven by induction over the syntax of programs and by composing the local soundness conditions of all abstract operators. Related work and discussion. An advantage of this iteration strategy, is that it leads to an intuitive order of application of the abstract equations corresponding to the program [START_REF] Cousot | Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints[END_REF], eliminating complex iteration strategies [START_REF] Horwitz | An Efficient General Iterative Algorithm for Dataflow Analysis[END_REF]. It also simplifies the choice of widening points [START_REF] Bourdoncle | Abstract Interpretation by Dynamic Partitioning[END_REF], as it applies widening naturally, at loop heads, though it also allows one to make different choices in strategy by, for example, modifying lfp ♯ to unroll loop iterations [START_REF] Blanchet | A static analyzer for large safety-critical software[END_REF].

Conclusion

We have presented a modular construction of a static analysis that is able to reason both about the shape of data structures and their numeric contents simultaneously. Our construction is parametric in the desired numeric abstraction, as well as the shape abstraction, making it possible to continuously substitute improvements for each component or with variants targeted at different classes of programs or even different programming languages. The main advantage of a modular construction is that it allows one to design, prove, and implement each component of the analysis independently. Modular construction is a cornerstone of quality software engineering, and our experience has been that this nice property becomes even more important when dealing with the complexity of creating a static analysis that simultaneously reasons about shape and numeric properties.

Figure 1 :

 1 Figure 1: A concrete memory state consists of an environment E and a store σ shown in (c). This example state corresponds to the informal box diagram shown in (b) and a state at the return point of the C-procedure f in (a).

Figure 4 :

 4 Figure 4: separating shape graph abstraction of σ in Figure 1. Symbolics α x and α y denote the address of x and y, respectively.

1 Figure 5 :

 15 Figure 5: An example separating shape graph enriched with a numeric constraint (right) with four concrete instances (center) for the C type declaration (left).

Figure 7 :

 7 Figure 7: Two abstractions drawn from the combined abstract domain H ♯ ⇒ N ♯ that have equivalent concretizations but with non-isomorphic sets of symbolic variables.

Figure 8 :

 8 Figure8: Applying the transfer function for an assignment on a separating shape graph that changes the set of "live" symbolic variables.

Figure 9 :

 9 Figure 9: Summarizing linked lists with inductive predicate edges in separating shape graphs.

Figure 10 :

 10 Figure 10: Depicting a memory abstraction including the abstract heap from Figure 4 and an abstract environment.

Figure 12 :Figure 13 :

 1213 Figure 12: Interfaces for the abstract domain layers shown in Figure 11 (except the disjunctive abstraction layer).

Figure 14 :

 14 Figure 14: Evaluating dereferences in an abstract heap.

∧ α 3 ≤ α 2 ∧ α 4 = α 2 + 1 Figure 15 :Figure 16 :

 2411516 Figure 15: Applying assign mem to an example assignment of the form loc = exp.

Figure 17 :

 17 Figure 17: Applying the condition test guard mem to an example that affects a summarized region α 2 • list.

Figure 20 :

 20 Figure 20: Disjunctive abstraction interface.

  assign ∨ (c, loc, exp) def = partition ∨ (c, {assign mem (loc, exp, m ♯ ) | m ♯ ∈ s ♯ }) (definition) (E, σ [L loc (E, σ ) ← E exp (E, σ )]) ∈ γ ∨ (assign ∨ (c, loc, exp, s ♯ ))

p 0 ; p 1 ♯ (s ♯ ) def = p 1 ♯♯ 0 -Figure 21 :

 11021 Figure21: A denotational-style abstract interpreter for the programming language defined in Section 2.2.

Acknowledgments We are inspired by Dave Schmidt's continual effort in formalizing the foundations of static analysis, abstract interpretation, and the semantics of programming languages. We would also wish to thank Dave for being a pillar in the static analysis community and supporting the research community with often thankless, behind-the-scenes work.

This work has been supported in part by the European Research Council under the FP7 grant agreement 278673, Project MemCAD and the United States National Science Foundation under grant CCF-1055066.

Modular Construction of Shape-Numeric Analyzers variables cannot be allocated at the same physical address. 2. Then, it calls compare comb (Φ, (σ ♯ 0 , ν ♯ 0 ), (σ ♯ 1 , ν ♯ 1 )) that forwards to a call of compare shape (Φ, σ ♯ 0 , σ ♯ 1 ). 3. The abstract heap comparison function compare shape attempts to match σ ♯ 0 and σ ♯ 1 region-by-region using a set of local rules:

• (Decomposition) Suppose σ ♯ 0 and σ ♯ 1 can be decomposed as σ ♯ 0 = σ ♯ 0,0 * σ ♯ 0,1 and σ ♯ 1 = σ ♯ 1,0 * σ ♯ 1,1 . And if the corresponding sub-regions can be shown to satisfy the inclusions

then the overall inclusion holds-compare shape (Φ, σ ♯ 0 , σ ♯ 1 ) returns (true, Φ ′′ );

1,r and Φ(α 1 ) = α 0 , then we can conclude inclusion holds locally and extend Φ with Φ(β 1 ) = β 0 ;

succeeds and returns (true, Φ ′ ), it means the inclusion holds with respect to the shape. We, however, still need to check for inclusion with respect to the numeric properties. Recall that the base numeric domain elements

have incomparable sets of symbolic variables. An inclusion check in the base numeric domain can only be performed after renaming symbolic names so that they are consistent. The node mapping Φ ′ computed by the above is precisely the renaming that is needed. Thus, the last step to perform to decide inclusion is to compute compare num (ν ♯ 0 , rename num (Φ ′ , ν ♯ 1 )) and return it as a result for

). Note that function rename num should be sound in the following sense:

where Φ(V ) is the set of symbolic variables obtained by applying Φ to set V . 5. If any of the above steps fail, compare mem returns false. To summarize, the soundness conditions of the inclusion tests for the lower-level domains on which compare mem relies are as follows:

Condition 8 (Soundness of inclusion tests).

Returning to the example in Figure 18, after starting with

, the compare shape operation consumes the points-to edges one-by-one extending Φ incrementally, unfolding the inductive edges in the right argument before concluding that inclusion holds in the shape domain. With the final mapping Φ ′ (α ′ i ) = α i for all i, the numeric inclusion simply needs to check that compare num (α

Join and widening

As is standard, the join mem operation should satisfy the following: Condition 9 (Soundness of join mem ). For all m ♯ 0 and m

). Like the comparison operator, the join operator takes two abstract heaps that have distinct sets of symbolic variables as input. Additionally, it generates a new abstract heap, which requires another set of symbolic variables, as it may not be possible to use the same set as either input. The example shown in Figure 19 illustrates this situation. In left input m ♯ 0 , variable x points to a non-empty list and y points to a possibly empty list, whereas right input m ♯ 1 describes the opposite. The most precise over-approximation of m ♯ 0 and m ♯ 1 corresponds to the case where both x and y point to lists of any length (as shown on the right side of the figure). These three elements all have distinct sets of nodes (that cannot be put in a bijection). Thus, the join algorithm uses a slightly different notion of symbolic node mapping Ψ that binds three-tuples of nodes consisting of one node from each parameter and one node in the output abstract heap. Conceptually, the output abstract heap is a kind of product construction, so it is composed of new symbolic variables corresponding to pairs of nodes with one from each input.

Overall, the join algorithm proceeds in a similar way as the inclusion test: the abstract heap join produces a mapping relating symbolic variables along with a new abstract heap. This mapping is then used to rename symbolic variables in the base numeric domain elements consistently to then apply the join in the base domain. Similar to the inclusion test, an initial mapping Ψ is constructed using the abstract environment at the M ♯ level and then extended step-by-step at the H ♯ level. For instance, in Figure 19, the initial mapping is {(α 0 , α ′ 0 , α ′′ 0 ), (α 1 , α ′ 1 , α ′′ 1 )}, and then pairs (α 2 , α ′ 2 , α ′′ 2 ) and (α 3 , α ′ 3 , α ′′ 3 ) are added by join shape . Note that nodes α 3 , α 4 , α ′ 3 , α ′ 4 have no counterpart in the result. The local rules abstract heap join rules used in join shape belong to two main categories: • (Bijection) When two fragments of each input are isomorphic modulo Ψ, they can be joined into another such fragment. In the example, the points-to edges α 0 → α 2 and α ′ 0 → α ′ 2 can both be over-approximated by α ′′ 0 → α ′′ 2 . Applying this rule adds the triple (α 2 , α ′ 2 , α ′′ 2 ) to the mapping Ψ. • (Weakening) When a heap fragment can be shown to be included in a more simple, summary fragment (in terms of their concretizations), we can over-approximate the original fragment with the summary. For instance, fragment α 2 • next → α 3 * α 2 • d → α 4 * α 3 • list can be shown to be included in α 2 • list. The other input can be an effective means for directing the choice of possible summary fragments [START_REF] Chang | Relational inductive shape analysis[END_REF][START_REF] Chang | Shape Analysis with Structural Invariant Checkers[END_REF]. The widening operator widen mem can be defined similarly to join mem . If the heap join rules enforce termination (i.e., join shape can be used as a widening) and join num is replaced with a widening operator widen num , the cofibered domain definition guarantees the resulting operator enforces termination [START_REF] Venet | Abstract Cofibered Domains: Application to the Alias Analysis of Untyped Programs[END_REF].