# An Abstract Separation Logic for Interlinked Extensible Records

Martin Bodin, Thomas Jensen, Alan Schmitt

► To cite this version:

Martin Bodin, Thomas Jensen, Alan Schmitt. An Abstract Separation Logic for Interlinked Extensible Records. Vingt-septièmes Journées Francophones des Langages Applicatifs (JFLA 2016), Jan 2016, Saint-Malo, France. hal-01333600

HAL Id: hal-01333600

https://hal.science/hal-01333600

Submitted on 15 Sep 2016

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# An Abstract Separation Logic for Interlinked Extensible Records

Martin Bodin, Thomas Jensen & Alan Schmitt

Inria, France

## Résumé

The memory manipulated by JAVASCRIPT programs can be seen as a heap of extensible records storing values and pointers. We define a separation logic for describing such structures. In order to scale up to full-fledged languages such as JAVASCRIPT, this logic must be integrated with existing abstract domains from abstract interpretation. However, the frame rule—which is a central notion in separation logic—does not easily mix with abstract interpretation. We present a domain of heaps of interlinked extensible records based on both separation logic and abstract interpretation. The domain features spatial conjunction and uses summary nodes from shape analyses. We show how this domain can accommodate an abstract interpretation including a frame rule.

## 1. Introduction

The memory of a JAVASCRIPT program is a dynamic and complex heap of extensible records storing values and pointers. Fields can be added and removed from records dynamically, and their presence can be tested. Moreover, records are not constrained by a static type structure, which further complicates the analysis of the shapes that these interlinked objects may form. Obtaining a good approximation of the memory structure of a JAVASCRIPT program is a challenge for static analysis, even if we restrict other features of the language such as computed field names and dynamic code generation.

In this paper, we present a solution to this challenge, by mixing elements of separation logic and shape analysis, and integrating them into an abstract interpretation framework. Separation logic in itself is not adequate for describing the inter-connected heaps of JAVASCRIPT. First, separation logic is based on some additional structures, such as lists or trees. For JAVASCRIPT, such structures can be difficult to identify, as illustrated by Gardner et al. [?]. Second, JAVASCRIPT native structures tend to not separate nicely. Gardner et al. propose to remedy this through a *partial separation operator* $\bowtie$ (“seppish”). The formula $P \bowtie Q$ describes a heap which can be split in two heaps, one satisfying P and the other Q; but these two heaps do not need to be disjoint. Here, we pursue this idea, but instead of introducing a new operator in separation logic, we inject ideas from shape analyses, and use summary nodes for modelling the portion of memory that may be shared. In this way, we move the approximation into the shape structures while keeping a precise separation operator $\star$.

The work described here is part of a larger project on certified static analyses in which static analysis tools are developed and proved correct based on a mechanised formalisation of the semantics of the underlying language. More precisely, the aim is to build on the JSCERT [?] semantics for JAVASCRIPT, a pretty-big step operational semantics [?] entirely written in Coq. The size of the JAVASCRIPT's semantics imposes that we take an approach that is both principled and mechanisable. We base the development on the theory of abstract interpretation. Abstract interpretation [?] provides a powerful theory for finding and proving loop invariants within a program, assuming minimal structure on the

<footnote>This research was partially supported by the French ANR-10-LABX-07-01 Laboratoire d'excellence CominLabs and ANR-14-CE28-0008 project Ajacs.</footnote>
space of abstract domains. For the mechanisation, certification in proof assistants such as Coq is
needed. We have previously built a Coq library [?] providing the building blocks for constructing
an abstract interpretation from a pretty-big step operational semantics, following initial ideas of
Schmidt [?]. In that paper, we showed how to derive abstract rules from concrete ones in such a way
that abstract derivations are correct by construction. Here, we show how to extend this approach
with abstractions of heaps using techniques from both separation logic and shape analysis, in order
to give reasonable results for JAVASCRIPT.

The abstract domains arising from separation logic do not have the rich structure of lattices
encountered in many abstract interpretations. The theory of abstract interpretation, however, does
generalise to the setting where the underlying structure is that of only a subset of a pre-order. We
shall hence use this more general framework, which provides the same correctness guarantees but does
not explain how to compute a best analysis result.

Separation logic provides useful notions for the analysis of heap-manipulating programs. In separation logic, abstract rules are only given locally: they only state what is changed by a given program, assuming that everything not mentioned is left unchanged. The frame rule then allows to add an unchanged partial heap to the analysed result. This mechanism is very powerful to locally reason about programs. However JAVASCRIPT introduces some new issues about the frame rule: Reynolds [?, Section 3.5] stated that the frame rule can not be applied as-is if the language allows constructions similar to JAVASCRIPT's *delete* operator. We address this issue using a special value ⌜?⌝.

The main contributions of this paper are as follows.

* A combination of separation logic and shape analysis, which allows to use the separation ⋆ for disjoint domains, and shapes for complex domains with potential sharing.

* An alternative to the ⌜?⌝ operator that better fits the frame rule.

* An integration of separation logic into an abstract interpretation framework based on pre-orders and big-step operational semantics, extending our previous work [?].

The paper is organised as follows. We first present our toy language *OWHILE*. Our logic is presented in two steps: first, a logic over abstract domains is built in Section ??; its structure should not be surprising to a reader familiar with separation logic. A crucial step of the approach is the addition of membranes, in Section ??, to deal with the frame rule. Second, we add the summary nodes from shape analyses to the domain in Section ???. Section ?? presents how we build our program logic for *OWHILE*, leading in Section ?? to the correctness of our abstract semantics. Section ?? examines related work and Section ?? concludes.

## 2. The OWhile Language

We define our analyses on a small imperative language with interlinked records, called *OWHILE*. This language is inspired from JAVASCRIPT's memory model but we shall disregard all aspects related to prototype inheritance or type conversion. We can create new records (which we call *objects*), and read, write, and delete their fields (also called *properties* in JAVASCRIPT). Records are *interlinked* because their fields may contain pointers to other objects.

The syntax of our language is presented in Figure ???. A detailed version of the concrete semantics can be found in Appendix ??, but it comes with no surprises for a pretty-big-step semantics [?]. There are only numbers in the language, so for the purpose of branching (instructions *if* and *while*), the number 0 behaves as *false*, and any other number as *true*. The operation ? non-deterministically returns a number. Fresh objects are created by the {} expression. We can access the field *f* of an object computed by *e* through *e.f*. We can check the presence or absence of a given field *f* in an
<figure><img src="image_2.png" /><figcaption>(a) Statements</figcaption></figure>

<caption>(b) Expressions</caption>

<caption>Figure 1: The syntax of the OWHILE language</caption>

object computed by *e* through *f* in *e*, which returns 1 if the field is present and 0 otherwise. As in JAVASCRIPT, writing to the field *f* of an object adds the field if it is not already present, and deleting an object's field succeeds even if the field is absent. There is no explicit declaration of variables: as for fields, writing a variable which is not defined creates it. A program may abort for the following reasons: explicitly running *throw*, reading a variable or a field that is not assigned, or accessing the field of a value that is not an object. The state *S* of a program is composed of two components.

* An environment (also called *store* in JAVASCRIPT parlance) *E* : *Var* → *Val*, where *Var* is the set of variable names and *Val* is the set of values. A value *v* ∈ *Val* can either be a location *l*<sup>*i*</sup> (including the special null location *l*<sup>0</sup>, always out of the domain of *S*), or a basic value *n* ∈ ℤ.

* A heap $H : \mathit{Loc} \to \mathfrak{F} \to \mathit{Val}$, where $\mathit{Loc} = \{l^i | i \in \mathbb{N}^*\}$ is the set of non-null locations, and $\mathfrak{F}$ the set of field names. We assume $\mathfrak{F}$ to be infinite.

We define dom(*S*) to be dom(*E*) ∪ dom(*H*) where *E* and *H* are the respective environment and heap of *S*. The function *fresh* takes a state *S* and returns a location fresh in *S*, i.e., *l*<sup>*j*</sup> ∉ dom(*H*).

3. Abstract Domains

3.1. Abstract State Formulae

In this section we build a separation logic over an abstract domain of base values. There are various
ways of representing separation logic; our logic is based on the work of [?]. Abstract state formulae
$\phi \in \mathit{State}^{\sharp}$ model pairs of concrete heaps and stores. These formulae are defined as follows.

$$
\phi ::= \mathit{emp} \mid \phi_1 \star \phi_2 \mid \mathbf{x} \doteqdot \mathbf{v}^\sharp \mid l \mapsto \{o\}
$$

$$
o ::= \mathbf{f} : v^{\sharp}, o | \_ : v^{\sharp}
$$

These formulae make use of abstract locations *l* ∈ *LLoc*<sup>‡</sup>. These locations are identifiers which are meant to represent one concrete (non-null) location. In the concretisation of formulae, abstract locations are related to concrete locations by a valuation *ρ* : *LLoc*<sup>‡</sup> →<sub>*inj*</sub> *Loc* (where →<sub>*inj*</sub> denotes a partial injection). Concrete locations in *Loc* are written with an exponent *l*<sup>*i*</sup> whilst abstract locations use indexes or primes: *l*, *l*<sub>*i*</sub>, or *l*'<sub>*</sub>

The structure of the abstract domain for values $v^{\sharp} \in Val^{\sharp}$ is described in detail in Section ???. For now, we just note that this abstract domain contains abstract locations (detailed below) and abstract properties of numeric values (sign, parity, intervals, ...). The concretisation function $\gamma_{\rho}$ of abstract values relates them to sets of concrete values.

The formula *emp* describes the empty heap and empty environment. The spatial conjunction $\phi_1 \star \phi_2$
describes the set of all heaps and environments which we can separate into two smaller heaps and
environments, each respecting one of the two sub-formulae $\phi_1$ and $\phi_2$. The $\star$ operator is commutative,
associative, and has *emp* as neutral element. The formula $\mathbf{x} \doteqdot v^{\sharp}$ states that the value of the variable
x satisfies the property $v^\sharp$. We follow the tracks of [?] and do not consider this formula pure. As we are not interested in concurrency in this paper, we use a simpler version than [?] where we either have full permission over x if $x \doteq v^\sharp$ is present, and no permission otherwise. The construction $l \mapsto \{o\}$ describes the set of heaps whose only defined location $\rho(l)$ points to an object abstracted by $\{o\}$.

Objects are abstracted as a list associating fields to abstract values, with an additional default abstract value for the other fields present in the object.<fnref n="1" /> All the specified field names of an object are supposed to be different. An abstract object $\{f_1 : v_1^\sharp, \dots, f_n : v_n^\sharp, \dots : v_r^\sharp\}$ represents the set of objects whose respective fields $f_1, \dots, f_n$ are abstracted by respectively $v_1^\sharp, \dots, v_n^\sharp$, and all the other fields are abstracted by $v_r^\sharp$. Abstract values also include the possibility to state that a field is undefined. This is expressed through the special value $\boxtimes$. The abstract object $\{f : \boxtimes, g : v^\sharp, \dots : \top\}$ thus describes the set of objects such that each object has no field $f$ and its field $g$ can be abstracted by $v^\sharp$. Similarly, $\{\_ : \boxtimes\}$ describes the singleton of the empty object, which is returned by $\{\}$.

An alternative approach to model heaps and objects is to allow the separation of fields themselves, as in $l \stackrel{f}{\mapsto} v_1^\sharp \star l \stackrel{g}{\mapsto} v_2^\sharp$, in a way similar to [?]. We experimented with this approach and discovered that it results in complex interactions with the frame rule. We thus follow a simpler approach here.

## 3.2. Abstract Values and Abstract Object

Our separation logic formulae are parameterized over an abstract domain describing the base values which variables and fields can contain. In line with the dynamic typing of JAVASCRIPT, we shall consider an abstract domain containing both numerical values and locations. Hence, a variable may contain both types of values depending on the flow of control, and the abstract domain has to be able to join such values together.

In addition, when analyzing JAVASCRIPT's heap, we must take into account expressions like `f in e` whose result depends on the absence of a field. We thus have to track whether fields can be undefined.<fnref n="2" /> To this mean, we attach a boolean to the abstract values to indicate whether the concrete value can be undefined, as illustrated before with the value $\boxtimes$. We use this boolean at two different places: to indicate that a field is possibly undefined, but also to indicate that a variable is possibly undefined.

Suppose a lattice domain $Z^\sharp$ carrying abstract properties of numeric, or basic, values (sign, parity, intervals, ...). Such a domain must store information about the different instances of values: basic values, locations, the possibility of being the special location $l^0$, and the possibility of being undefined. We define abstract values to be tuples of the form $(n^\sharp, nil^?, L, d)$, where $n^\sharp \in Z^\sharp$ denotes the possible basic values which can be represented by this abstract value; $nil^?$ is a boolean stating whether the value can be $l^0$ (denoted by `nil`) or not (denoted by $\overline{nil}$); $L \in \mathcal{P}_f(LLoc^\sharp)^\top$ denotes the possible location values $(\mathcal{P}_f(LLoc^\sharp)^\top)$ denotes the set of finite subsets of $LLoc^\sharp$ augmented with a $\top$ element); and the boolean $d \in \{\boxtimes, \Box\}$ denotes whether the value can be undefined (denoted by $\boxtimes$) or can not (denoted by $\Box$). Each part of these tuples carries the information about a kind of value.

For the sake of readability, we will identify the projections of an abstract value $v^\sharp$ with $v^\sharp$ itself if all the other projections are bottoms elements of their respective lattice. For instance we will write $n^\sharp$ to mean $(n^\sharp, \overline{nil}, \emptyset, \Box)$, `nil` to mean $(\bot, \overline{nil}, \emptyset, \Box)$, and $\boxtimes$ to mean $(\bot, \overline{nil}, \emptyset, \boxtimes)$. We will also identify $l$ with $(\bot, \overline{nil}, \{l\}, \Box)$. To avoid the cumbersome tuple notation, we will use the natural join operation on this domain and write values such as $l \sqcup \boxtimes$.

The order on the tuple is the usual product order: a tuple is less than another if all its projections are less than the others. Sets of locations are ordered using the usual set lattice. The definition part

<footnote n="1">¹This default field is sometimes called a *summary node* in the literature; we do not use this name as summary nodes denote a different concept in this paper.</footnote>

<footnote n="2">²This abstract value is different from the JAVASCRIPT value `undefined`.</footnote>
d is ordered by □ ⊑ ⊗ as □ forces the value to be defined while ⊗ allows (without forcing) it to be undefined. We similarly define $\overline{nil} \sqsubseteq nil$. We use the symbol $\sqsubseteq$ to denote the order within a lattice, that is over abstract values and abstract objects.

We can now define an order on abstract objects as follows: two objects are ordered, {$o_1$} $\sqsubseteq$ {$o_2$} if all the fields of {$o_1$} are associated with a value which is smaller than the value of the same field in {$o_2$}. To check the order relation between two objects, we rely on the default value for all fields not explicitly mentioned in the object. With this value, we can rewrite the two objects so that they refer to the same fields, using the following rewriting equality,

$$ \{ \mathbf{f}_1 : v_1^\sharp, \dots, \mathbf{f}_n : v_n^\sharp, \dots : v_r^\sharp \} = \{ \mathbf{f}_1 : v_1^\sharp, \dots, \mathbf{f}_n : v_n^\sharp, \dots : v_r^\sharp \} $$

which holds provided that $g$ is not one of the $\mathbf{f}_1, \dots, \mathbf{f}_n$. This order equips abstract objects with a lattice structure, with $\sqcup$ and $\sqcap$ computing the abstract object whose fields are associated to the results of the corresponding operator $\sqcup$ or $\sqcap$ applied on the corresponding fields of the two operands (completed such that they have the same fields):

$$ \begin{aligned} & \{ \mathbf{f}_1 : v_1^\sharp, \dots, \mathbf{f}_n : v_n^\sharp, \dots : v_r^\sharp \} \sqcup \{ \mathbf{f}_1 : v_1'^\sharp, \dots, \mathbf{f}_n : v_n'^\sharp, \dots : v_r'^\sharp \} \\ & = \{ \mathbf{f}_1 : v_1^\sharp \sqcup v_1'^\sharp, \dots, \mathbf{f}_n : v_n^\sharp \sqcup v_n'^\sharp, \dots : v_r^\sharp \sqcup v_r'^\sharp \end{aligned} $$

## 4. The Frame Rule

Our main contribution deals with the interaction between formulae and the frame rule. In order to introduce it, we first detail how this rule typically works. The frame rule defines how to extend Hoare triples using the separation operator $\star$. A Hoare triple $\phi_1, t \Downarrow^\sharp \phi_2$ states that the term $t$ changes any heap that satisfies formula $\phi_1$ in a heap that satisfies formula $\phi_2$. In our setting, a heap satisfies a formula if it belongs to its concretisation. A heap $h$ belongs to the concretisation of a formula $\phi_1 \star \phi_2$ if it can be split in disjoint heaps $h_1$ and $h_2$ such that $h_1$ satisfies $\phi_1$ and $h_2$ satisfies $\phi_2$.

$$ \frac{\frac{\text{FRAME}}{\phi_1, t \Downarrow^\sharp \phi_2}}{\phi_1 \star \phi_c, t \Downarrow^\sharp \phi_2 \star \phi_c} $$

For the frame rule to be correct, it is crucial that if $\phi_1 \star \phi_c$ is defined (the set of concrete heaps it denotes is not empty), then $\phi_2 \star \phi_c$ is defined. In our setting, this may not be the case when new abstract locations are introduced in $\phi_2$. For instance, consider the abstract rule NEWOBJ, which builds the Hoare triple emp, {} $\Downarrow^\sharp l \mapsto \{\_ : \boxtimes\}$. The result contains an additional location $l$ which we would like to keep fresh from the initial abstract heap emp. However, the frame rule applied as-is can add a new fact about $l$ and generate the Hoare triple $l \mapsto \{\_ : \boxtimes\}, \{\} \Downarrow^\sharp l \mapsto \{\_ : \boxtimes\} \star l \mapsto \{\_ : \boxtimes\}$, which is wrong as the result formula has an empty concretisation (because $l$ is not separated) whilst a concrete derivation tree can easily be derived. This problem also occurs when renaming abstract locations, as is described in Section ??.

To ensure the soundness of the frame rule, we have to introduce scopes for identifiers in a formula. For instance, the scope of a newly created location $l$ should be restricted to the result formula, as in emp, {} $\Downarrow^\sharp (\nu l | l \mapsto \{\_ : \boxtimes\})$: this states that any mention of $l$ outside the formula is actually a different identifier. Since we not only need to restrict the scope of identifiers, but also relate names inside a scope to names outside the scope, we introduce the notion of membrane. A membrane M traces the links between these two scopes. Each context added by the frame rule has to be converted when entering a membrane. Membranes behave like substitutions: we can compose them through $\circ$ and apply them to a formula $\phi$ to update its identifiers. Our version of the frame rule, defined in below, relies on membranes for its soundness.
## 4.1. Membranes

Membranes $M$ are defined as a set of scope changes $m$, which can be caused either because a location has been renamed, or because a new location has been allocated. The abstraction $\Phi$ of heap and environment is now a couple of a formula $\phi$ and a rewriting membrane $M$, written $(M|\phi)$. We call the simple formulae $\phi$ inner formulae and the membraned formulae $\Phi$ formulae.

$$m \in \mathfrak{M} ::= l \to l' | \nu l$$

$$\Phi ::= (M|\phi)$$

$$M \in \mathcal{P}_f(\mathfrak{M})$$

We impose left-hand sides of scope changes to only appear once in a given membrane. We also impose that in a formula $\Phi = (M|\phi)$, any location $l$ in $\phi$ is present on the right-hand side of a scope change or as a new name $\nu l$ in $M$. We define the domain $dom(M)$ of a membrane $M$ as the set of left-hand sides of its rewritings, and the codomain $codom(M)$ as the union of the set of right-hand sides of its rewritings and the set of newly allocated locations. The interface interface($\Phi$) of a formula $\Phi = (M|\phi)$ is the domain of its membrane $dom(M)$: these locations are accessible from the outside of the formula. The substitution $M(\phi)$ applied to inner formulae works as expected: it renames every abstract locations either as values or as memory cells. Trivial rewritings such as $l \to l$ are allowed and sometimes required: an abstract location $l$ may be unchanged by the membrane, but it still has to be in the interface; the domain names of the inner and scope scopes are independent.

Let us consider a simple example: $\Phi = (l_0 \to l | \mathbf{x} \doteq l \star l \mapsto \{\mathbf{f} : l, \_ : \boxtimes\})$. The membrane $\{l_0 \to l\}$ renames the outer location identifier $l_0$ to the inner location $l$. If the frame rule introduces a context $\phi_c = l_1 \mapsto \{\mathbf{f} : l_0, \_ : \boxtimes\}$ referring to $l_0$, the integration of $\phi_c$ in the membrane leads to the renaming of $l_0$ into $l$ for a final formula $(l_0 \to l | \mathbf{x} \doteq l \star l \mapsto \{\mathbf{f} : l, \_ : \boxtimes\} \star l_1 \mapsto \{\mathbf{f} : l, \_ : \boxtimes\})$. On the other hand, if the frame rule introduces a context with a $l$ such as $\phi_c = l_1 \mapsto \{\mathbf{f} : l, \_ : \boxtimes\}$, this $l$ is actually different from the one in $\Phi$. In this case, $\Phi$ is $\alpha$-renamed, for instance to $\Phi = (l_0 \to l' | \mathbf{x} \doteq l' \star l' \mapsto \{\mathbf{f} : l', \_ : \boxtimes\})$, to avoid the capture of $l$ when $\phi_c$ enters the membrane. Note that $\alpha$-renaming does not change the interface of a formula: only its codomain is modified.

Formulae are used to abstract states (environment and heap), but there are places in our semantics where additional values are carried. In pretty-big-step, we use intermediate terms along the execution, which require to carry additional values. For example, the assignment $\mathbf{x} := e$ involves two steps (evaluating the expression and updating the state) so we introduce an intermediate term $\mathbf{x} :=_1$ whose semantic context consists of a state and a value to assign to $\mathbf{x}$ and whose result is the update state. These values can contain locations and must be placed inside membranes: we shall thus sometimes manipulate formulae of the form $(M|l \mapsto \{o\}, l \sqcup l')$ where the value $l \sqcup l'$ represents the value of the intermediate semantic context. All operations defined on usual formulae can be extended to extended formulae. We do not show the details here for space reasons.

## 4.2. Separating Formulae

To express the frame rule in our formalism, the frame has to manipulate membranes; we define the operator $\boxtimes$ (read “in frame”) taking two formulae $\Phi_o = (M_o|\phi_o)$ and $\Phi_i = (M_i|\phi_i)$—i stands for “inner” and $o$ for “outer”—which intuitively builds $(M_o|\phi_o \star (\phi_i|M_i))$ (this formula does not fit the grammar of formulae as-is): the inner formula is considered in the context of the outer one. This operation is associative, but not commutative. It performs an $\alpha$-renaming of the inner identifiers of $\phi_i$ to prevent conflicts with $M_i$, then pushes $\phi_o$ through the membrane $M_i$. For instance for $\Phi_o = (l_0 \to l, k_0 \to k | k \mapsto \{\mathbf{g} : k, \mathbf{h} : l, \_ : \boxtimes\})$ and $\Phi_i = (l \to k | k \mapsto \{\mathbf{f} : k \sqcup nil, \_ : \boxtimes\})$, the identifier $k$ is used both in $\phi_i$ and in $\phi_o$, but because of the membranes, it represent a different set of
concrete locations in both formulae. We thus α-rename $k$ into $k'$ to avoid name conflict:

$$ 
\begin{align*}
(l_0 \to l, k_0 \to k | k &\mapsto \{g : k, h : l, \_ : \boxtimes\}) \boxplus (l \to k | k \mapsto \{f : k \sqcup nil, \_ : \boxtimes\}) \\
&= (l_0 \to l, k_0 \to k | k \mapsto \{g : k, h : l, \_ : \boxtimes\}) \boxplus (l \to k' | k' \mapsto \{f : k' \sqcup nil, \_ : \boxtimes\}) \\
&= (l_0 \to k', k_0 \to k | k \mapsto \{g : k, h : k', \_ : \boxtimes\} \star k' \mapsto \{f : k' \sqcup nil, \_ : \boxtimes\})
\end{align*}
$$

Because of the composition of membranes, $l$, which was an identifier introduced by $M_o$ but substituted by $M_i$, was removed. Membranes are meant to be composed by the $\boxplus$ operator, and the domain of the inner membrane should thus be in the codomain of the outer one: $dom(M_i) \subseteq codom(M_o)$.

We define $\boxplus$ as follows. Given and $\Phi_o = (M_o|\phi_o) \Phi_i = (M_i|\phi_i)$ such that $dom(M_i) \subseteq codom(M_o)$, we α-rename $\Phi_i$ into $\Phi'_i = (M'_i|\phi'_i)$ such that $codom(M'_i) \cap codom(M_o) = \emptyset$. We then make the formula $\phi_o$ enter the membrane $M_i$:

$$ \Phi_o \boxplus \Phi_i = \Phi_o \boxplus \Phi'_i = (M'_i \circ M_o | M'_i(\phi_o) \star \phi'_i) $$

We are now ready to state our frame rule.

$$ \frac{\text{FRAME} \qquad \Phi, t \Downarrow^{\sharp} \Phi'}{\Phi_c \boxplus \Phi, t \Downarrow^{\sharp} \Phi_c \boxplus \Phi'} $$

Although our program logic is not introduced until Section ??, here is an example of how the frame rule can be used. Consider the program *if? skip* (*x* := ?) where the branch is chosen randomly, one branch does nothing while the other assigns a random value to *x*. The empty branch of the *if* can be given the Hoare triple *emp*, *skip* $\Downarrow^{\sharp} *emp*$, and the other branch the Hoare triple *x* = $\boxtimes$, *x* := ? $\Downarrow^{\sharp} *x* \doteq \top_Z$. The first branch can then be extended using the frame rule to the triple *x* = $\boxtimes$, *skip* $\Downarrow^{\sharp} *x* \doteq \boxtimes$. Since both branches now have the same assumption, they may be merged together for the whole conditional: *x* = $\boxtimes$, *if? skip* (*x* := ?) $\Downarrow^{\sharp} *x* \doteq \boxtimes \sqcup \top_Z$.

## 5. Adding Summary Nodes

Up to this point, the formulae which we have defined reflect precisely the structure of the concrete heap. However, this approach is not viable in the presence of loops. We need a way to forget about some information of the structure, in particular its size. To this end, we reuse the idea of summary nodes from shape analysis, by adding a new kind of abstract locations $k \in KLoc^\sharp$ which represent a set (finite and possibly empty) of concrete locations. We call them *summary locations*. As with $LLoc^\sharp$, this new set of abstract locations $KLoc^\sharp$ is supposed to be a new, infinite, set of identifiers. We note abstract locations as $h \in KLoc^\sharp \sqcup LLoc^\sharp$.

Abstract values have been defined in Section ?? as tuples $(n^\sharp, nil^?, L, d)$, where $L \in \mathcal{P}_f(\mathit{LLoc}^\sharp)^\top$. We update them to track summary nodes by changing their projection $L$ to $L \in \mathcal{P}_f(\mathit{LLoc}^\sharp \sqcup KLoc^\sharp)^\top$. Values are thus abstracted by $Val^\ell = Z^\ell \times \{\overline{nil}, nil\} \times \mathcal{P}_f(\mathit{LLoc}^\sharp \sqcup KLoc^\sharp)^\top \times \{\Box, \boxtimes\}$.

In formulae, summary locations may occur on the left-hand side of heaps $k \mapsto \{o\}$, denoting heaps where every concrete location in the concretion of $k$ maps to a concretion of $o$. When $k$ occurs as a value, its concretion is any single location denoted by $k$. Note the asymmetry in $k \mapsto \{f : k, \_ : \boxtimes\}$, which means that every concrete location represented by $k$ has a field $f$ pointing to a concrete location in the set represented by $k$, but there is no relation between these two concrete locations. In particular, they need not be the same.

The set of formulae with summary nodes is defined as follows.
<figure><img src="image_3.png" /><figcaption>Figure 2: Picturisation of membrane operations</figcaption></figure>

$$
\begin{array}{l@{\qquad}l@{\qquad}l}
\phi ::= \mathit{emp} | \phi_1 \star \phi_2 & h ::= l | k & m \in \mathfrak{M} ::= h \to h_1 + \dots + h_n \\
| x \doteq v^{\sharp} & o ::= \mathfrak{f} : v^{\sharp}, o & | \nu h \\
| h \mapsto \{o\} & | \_ : v^{\sharp} & \Phi ::= (M | \phi) \qquad M \in \mathcal{P}_f(\mathfrak{M})
\end{array}
$$

Abstract values $v^{\sharp}$ can now contain basic values, abstract locations $h$ (which can be summary nodes $k$ or precise abstract locations $l$), the special *nil*, and the special abstraction $\boxtimes$. We update the definition of domain and codomain of membranes as expected:

$$
\begin{align*}
\operatorname{dom}(h \rightarrow h_1 + \dots + h_n) &= \{h\} & \operatorname{codom}(h \rightarrow h_1 + \dots + h_n) &= \{h_1, \dots, h_n\} \\
\operatorname{dom}(\nu h) &= \emptyset & \operatorname{codom}(\nu h) &= \{h\} \\
\operatorname{dom}(M) &= \bigcup_{m \in M} \operatorname{dom}(m) & \operatorname{codom}(M) &= \bigcup_{m \in M} \operatorname{codom}(m)
\end{align*}
$$

As renamings can now map an abstract location to several abstract locations, substitutions $M(\phi)$ can
now duplicate memory cells: $\{k \to k_1 + k_2\} (k \mapsto \{o\}) = k_1 \mapsto \{o[k_1 \sqcup k_2/k]\} \star k_2 \mapsto \{o[k_1 \sqcup k_2/k]\}$.

There are two basic operations on summary locations: summarizations and materializations. These
two operations rename abstract locations, thus changing the scope of formulae: membranes are a
crucial point for their soundness in accordance to their interaction with the frame rule. Let us first
only consider an inner formula $\phi$.

The summarization consists in merging abstract locations $h_1, \dots, h_n$ into a single new summary
node $k$. Figures ?? and ?? picture two examples of summarizations, respectively of two summary
nodes, and of an abstract location. It allows to loose information about the structure of $h_1, \dots,
h_n$; typically to get a loop invariant. In order to perform a summarization, we need to have in the
considered inner formula $\phi$ the explicit definition of all these abstract locations: it is not possible
to summarize $l$ and $l'$ in the formula $l \mapsto \{\mathfrak{f} : l', \_ : \boxtimes\}$ as we do not have access to the resource
$l'$. Let us thus suppose that the formula $\phi$ is of the form $h_1 \mapsto \{o_1\} \star \dots \star h_n \mapsto \{o_n\} \star \phi'$. The
summarization of $h_1, \dots, h_n$ into $k$, provided that $k$ does not appear in $\phi$, is the following formula.

$$
(h_1 \to k, \dots, h_n \to k | (k \mapsto \{o_1\} \sqcup \dots \sqcup \{o_n\} \star \phi') [k/h_1] \dots [k/h_n])
$$

We have merged all the statements about $h_1, \dots, h_n$, replaced in the current context $\phi'$ and the
merged abstract object these abstract locations by $k$, and left a notice in the form of a membrane for
additionnal contexts added by the frame rule about the operation which took place.

The materialization follows the same scheme, pictured in figure ??. Given an entry point to a
summary node k—either on the form of a variable x = k or a location l = {f : k, ...}—we can
rewrite a summary location into a single location (pointed by the entry point) and another summary
node, representing the rest of the concrete locations previously present. Indeed, we know that k
cannot represent an empty set of locations, and we would like to split it into the exact location
l' accessed by our entry point, and the rest k' of the other locations. This operation allows to
perform strong updates on these precise values. The materialization of k into l' and k' through
l.f (or a variable x) transforms an inner formula of the form $k \mapsto \{o\} \star l \mapsto \{f : k, ...\} \star \phi'$ into the formula $(k \to l' + k' | (l' \mapsto \{o\} \star k' \mapsto \{o\} \star l \mapsto \{f : l', ...\} \star \phi') [l' \sqcup k'/k])$: the entry point have been replaced by the precise location l' at the cost of replacing every occurence of k by l' $\sqcup$ k'. The membrane is for now only partial as there might be uncaught locations in $\phi'$ or in $\{o\}$. The materialization can only be performed if the entry point is precise: to perform a materialization over $x \doteq l \sqcup k$ for instance, we would have to first summarize l and k into the same summary node. Note that materialization can always be reversed using a well-chosen summarization.

These two processes of summarization and materialization have been shown on inner formulae. For formulae, we have to merge the new rewriting to the membrane. For instance, let us consider a summarization of l and k to k' on the following formula:

$$ \Phi = (k_0 \to k, l_0 \to l | x \doteq l \star l \mapsto \{f : k, \_, \_ : \Box\} \star k \mapsto \{g : k, \_, \_ : \Box\}) $$

We first forget about the membrane and perform the summarization on its inner formula, getting a new inner formula and the partial membrane $\{k \to k', l \to k'\}$; we then compose this partial membrane with the old membrane to get $\Phi'$: $\{k \to k', l \to k'\} \circ \{k_0 \to k, l_0 \to l\} = \{k_0 \to k', l_0 \to k'\}$.

$$ \Phi' = (k_0 \to k', l_0 \to k' | x \doteq k' \star k' \mapsto \{f : k' \sqcup \Box, g : k' \sqcup \Box, \_, \_ : \Box\}) $$

For the sake of example, let us continue by materializing $k'$ in $\Phi'$ through x. As before, we focus on the inner formula, then compose the generated rewriting $k' \to l'' + k''$ to the membrane to get $\Phi''$: $\{k' \to l'' + k''\} \circ \{k_0 \to k', l_0 \to k'\} = \{k_0 \to l'' + k'', l_0 \to l'' + k''\}$.

$$ \begin{aligned} \Phi'' = (k_0 \to l'' + k'', l_0 \to l'' + k'' | x \doteq l'' \star l'' \mapsto & \{f : l'' \sqcup k'' \sqcup \Box, g : l'' \sqcup k'' \sqcup \Box, \_, \_ : \Box\} \\ & \star k'' \mapsto \{f : l'' \sqcup k'' \sqcup \Box, g : l'' \sqcup k'' \sqcup \Box, \_, \_ : \Box\}) \end{aligned} $$

These transformations are permitted by a relation $\ll$ compatible with them: if $\Phi$ becomes $\Phi'$ through one of these transformations, then $\Phi \ll \Phi'$. Intuitively, $\Phi \ll \Phi'$ means that $\Phi$ is more precise than $\Phi'$. The soundness of these transformations is then implied by the soundness of $\ll$. In contrary to usual abstract interpretation, the relation $\ll$ is not required to form a lattice, but only to be sound with respect to the concretisation in any context, as shown in Section ?? . The pre-order $\ll$ is defined in Appendix ?? , but understanding its heavy definition is not needed to follow the rest of this paper.

Materializations and summarizations are the usual manipulations defined in shape analysis, but our formalism allows to define other similar operations. For instance, we could define a filtering op- eration which partitions locations depending on the values of their fields: the filtering of k relative to field f and the values $l_1$ and $l_2$ in the formula $(k_0 \to k + l_1 + l_2 | k \to \{f : l_1 \sqcup l_2, \_, \_ : \Box\} \star x \doteq k)$ is $(k_0 \to k_1 + k_2 + l_1 + l_2 | k_1 \to \{f : l_1, \_, \_ : \Box\} \star k_2 \to \{f : l_2, \_, \_ : \Box\} \star x \doteq k_1 \sqcup k_2)$; we have sepa- rated the summary node k into two nodes depending on the value of f. To add this operation into the formalism, the relation $\ll$ would have to be updated, as well as its correctness proof.

# 6. A Program Logic for OWhile

Given the abstract domain of formulae defined in the previous sections, we define a program logic for OWHILE to reason about these. We shall derive the program logic in a systematic fashion from the concrete semantics, extending an abstraction technique developed by the authors [?] to cover spatial conjunctions and the frame rule. We explain this technique in Section ?? , then present how to abstract rules in Section ?? . Section ?? presents the changes to accommodate the frame rule.

## 6.1. Abstract Interpretation of Pretty-big-step Semantics

Motivated by the JSCERT operational semantics for JAVASCRIPT, we have defined an abstract interpretation framework for semantics written in pretty-big-step style [?]. Pretty-big-step semantics [?].
is a particular form of big-step semantics where intermediate evaluation steps are brought out explicitly via intermediate terms that mix syntax and semantics. Following a proposal by Schmidt [?] for abstract interpretation of big-step semantics, we have shown how the inference rules in JSCERT can each be interpreted over an abstract domain such that the ensuing derivations are correct analyses of the original program. More precisely, we have exactly one abstract rule for each concrete rule, and the correctness proof is simplified to proving that each concrete and abstract rules are related in a one-to-one manner. For example, the abstract versions of the rules ADD2 and IF (e, s₁, s₂) follow.

$$ \frac{\text{ADD2}}{(v_1^\sharp, va^\sharp v_2^\sharp), +_2 \Downarrow^\sharp \text{add}^\sharp (v_1^\sharp, v_2^\sharp)} \qquad \frac{\text{IF}(e, s_1, s_2) \qquad \begin{array}{l} \Phi, e \Downarrow^\sharp \Phi' \\ \Phi', if_1 s_1 s_2 \Downarrow^\sharp \Phi'' \end{array}}{\Phi, ife s_1 s_2 \Downarrow^\sharp \Phi''} $$

However, as explained in [?], this approach implies that the abstract rules can no longer be interpreted inductively. Each rule describes how to build a new Hoare triple $\Phi, t \Downarrow^\sharp \Phi'$ given a semantic relation $\Downarrow_0^\sharp$ but such a triple is not correct by itself. Instead, we must consider all the applicable rules, i.e., rules $i$ that match the term ($t = l_i$) and may be applied according to the semantic context ($\text{cond}_i^\sharp(\Phi)$ holds), and merge their results in order to obtain a valid result. Formally, the abstract evaluation relation $\Downarrow^\sharp$ is defined as in Schmidt as the greatest fixed point of the iterator $\mathcal{F}^\sharp$; the relation $\mathcal{F}^\sharp(\Downarrow_0^\sharp)$ extends the relation $\Downarrow_0^\sharp$ by adding the triples $(\Phi_\sigma, t, \Phi_r)$ valid for all applicable rules. It uses the function $\text{glue}_i^\sharp(\Downarrow_0^\sharp)$ which computes all triples obtainable from the application of the $i$th rule:

$$ \mathcal{F}^{\sharp}(\Downarrow_0^{\sharp}) = \{ (\Phi_{\sigma}, t, \Phi_r) \mid \forall i. t = l_i \Rightarrow \text{cond}_i^{\sharp}(\Phi_{\sigma}) \Rightarrow (\Phi_{\sigma}, t, \Phi_r) \in \text{glue}_i^{\sharp}(\Downarrow_0^{\sharp}) \} $$

Program logics usually include a rule to weaken results. In our formalism, it would look like this:

$$ \frac{\text{WEAKEN}}{\Phi'_{\sigma} \preceq \Phi_{\sigma}} \qquad \frac{\Phi_{\sigma}, t \Downarrow^{\sharp} \Phi_{r}}{\Phi'_{\sigma}, t \Downarrow^{\sharp} \Phi'_{r}} $$

In our previous work [?], this rule is encoded in the above-mentioned $\text{glue}^\sharp$ function. It allows the analyser to perform some approximations before and after applying rules. The function $\text{glue}_i^\sharp$ was then defined as follows, where $\text{apply}_i(\Downarrow_0^\sharp)$ is the set of all triples that can be directly derived from $\Downarrow_0^\sharp$ by applying rule $i$ once.

$$ \text{glue}_i^\sharp(\Downarrow_0^\sharp) = \{ (\Phi_\sigma, t, \Phi_r) \mid \exists \Phi'_{\sigma}, \Phi'_{r}. \Phi_\sigma \preceq \Phi'_{\sigma} \wedge \Phi'_{r} \preceq \Phi_r \wedge (\Phi'_{\sigma}, t, \Phi'_{r}) \in \text{apply}_i(\Downarrow_0^\sharp) \} $$

## 6.2. Abstract Rules

Rules give semantics to expressions, statements, and intermediate terms of the OWHILE language. Each concrete rule is translated into exactly one abstract rule. Due to this one-to-one concrete-abstract rule correspondence, abstract and concrete rules share the same names.

In general, the rules fall into four informal categories, measuring the difficulty to abstract them:

* Administrative rules, which push states around; their abstract translation is straightforward.

* Condition rules, which are similar to administrative rules, but with non-trivial side conditions (cond). When translating them into the abstract world, their side condition has to be updated (cond'). Such a translation usually do not give further difficulties.

* Error rules, like condition rules, have a non-trivial side condition. Their result is always an error: they require in practise the same amount of work than condition rules to translate.
* Computational rules, where results are produced. The language operations (summing numbers, writing a variable, creating a field, etc.) take place in these rules and their abstract translations are usually more complex.

Figure ?? in Appendix ?? classifies the different rules of `OWHILE`. As can be seen, very few rules fall into the computational category, which is the category yielding most of the abstraction effort. These categories are arbitrary and debatable as they just serve as a rough estimate on the amount of work needed to build the abstract semantics; for instance the third category of error rules has been added because a lot of rule falls into it, but they require the same amount of work to abstract than the condition rules. For instance, let us consider the two concrete rules for assignments:

$$ \frac{\begin{array}{c} \text{ASGN}(x, e) \\ S, e \Downarrow r \quad r, x :=_1 \Downarrow r' \end{array}}{S, x := e \Downarrow r'} \qquad \frac{\text{ASGN1}(x)}{(S, v), x :=_1 \Downarrow \text{write}(S, x, v)} $$

The first rule `ASGN` $(x, e)$ is an administrative rule: its definition does not depend on the implementation of states and its abstract version is identical. On the other hand, the rule `ASGN1` $(x)$ uses the concrete `write` operation, which does not straightforwardly translate into the abstract world: we do so by exhibiting its footprint. This leads to the following two abstract rules for assignment. In contrary to [?], we only give a local version of the rules: the abstract rules work with the frame rule (see next section). Note how compact the rule `ASGN1` $(x)$ is, its context being implicit. Also note that although the concrete rule `ASGN1` $(x)$ applies even if $x$ is not defined in the state, we require it to be present in the abstract formula—eventually with the value $\boxtimes$. This solves the problem stated by Reynolds [?, Section 3.5], as the frame rule can no longer interfere with the resource $x$.

$$ \frac{\begin{array}{c} \text{ASGN}(x, e) \\ \Phi, e \Downarrow^{\sharp} \Phi' \quad \Phi', x :=_1 \Downarrow^{\sharp} \Phi'' \end{array}}{\Phi, x := e \Downarrow^{\sharp} \Phi''} \qquad \frac{\text{ASGN1}(x)}{(M \mid x \doteq v_0^{\sharp}, v^{\sharp}), x :=_1 \Downarrow^{\sharp} (M \mid x \doteq v^{\sharp})} $$

The only abstract rule of `OWHILE` whose footprint updates the membrane is the rule `NEWOBJ`, whose concrete and abstract rules follow. The concrete rule exhibit a fresh concrete location which has no associated reference $l^{fresh(S)}$. In the current state $S$. In the abstract rule, we create a new location $l$ and declare it as fresh in the membrane: this ensures it to be different from anything present in the context. We also claim that we have write permission over this new location $l$ by adding a memory cell into the formula, leaving its fields undefined as in the concrete rule.

$$ \frac{\text{NEWOBJ}}{S, \{\}\Downarrow(S, l^{fresh(S)})} \qquad \frac{\text{NEWOBJ}}{(\emptyset | \text{emp}), \{\}\Downarrow(\nu l | l \mapsto \{\_ : \boxtimes\}, l)} $$

## 6.3. Interfering with the Frame Rule

The version of the frame rule which we use is recalled below.

$$ \frac{\begin{array}{c} \text{FRAME} \\ \Phi, t \Downarrow^{\sharp} \Phi' \end{array}}{\Phi_c \boxplus \Phi, t \Downarrow^{\sharp} \Phi_c \boxplus \Phi'} $$

To make sense, the abstract semantics has to keep `interface` $(\Phi)$ constant along the derivation. It would otherwise be possible to exhibit a context $\Phi_c$ with a different behaviour in both sides. For instance, although $\Phi_1 = (l \to l | l \mapsto \{\_ : \boxtimes\})$ and $\Phi_2 = (l' \to l | l \mapsto \{\_ : \boxtimes\})$ represent the same concrete states (they have the same concretisation), in the context of $\Phi_c = (k \to l + l' | l \mapsto \{\_ : \boxtimes\})$,
## 6.4. Correctness

The correctness relies on the concretisation $\gamma$ of formulae. Concretisation of formula is defined through a predicate $\models$ shown in Figure ??; this predicate is parametrized by a valuation $\rho: LLoc^\sharp \to Loc \wedge KLoc^\sharp \to \mathcal{P}(Loc)$ of abstract locations to concrete locations. The difficult part stands in the concretisation of objects, where abstract values $v^\sharp$ can represent an undefined concrete value if $\boxtimes \sqsubseteq v^\sharp$. We do not show the definition of the concretisation function of objects, but it comes with no surprise. The set $R$ is used to store the reserved variables: $x \doteq \boxtimes$ states that the variable $x$ is not in the environment, but it still reserves the resource $x$ to be sound with the frame rule; this fact is stored by $R$. The concretisation $\gamma(\Phi)$ of a formula $\Phi$ is then a projection of this predicate:

$$ (E, H) \in \gamma((M | \phi)) \iff \exists \rho, R. (E, R, H) \models_{\rho} \phi $$

$$ \begin{align*} (E, R, H) \models_{\rho} \mathit{emp} &\iff E = R = H = \emptyset \\ (E, R, H) \models_{\rho} \phi_1 \star \phi_2 &\iff \exists E_1, R_1, H_1, E_2, R_2, H_2. E = E_1 \uplus E_2 \wedge R = R_1 \uplus R_2 \\ &\qquad \wedge \mathit{dom}(E_1), \mathit{dom}(E_2), R_1, \text{ and } R_2 \text{ are disjoint pairwise} \\ &\qquad \wedge H = H_1 \uplus H_2 \wedge \mathit{dom}(H_1) \cap \mathit{dom}(H_2) = \emptyset \\ &\qquad \wedge \forall i. (E_i, R_i, H_i) \models_{\rho} \phi_i \end{align*} $$

$$ (E, R, H) \models_{\rho} x \doteq v^\sharp \iff H = \emptyset \wedge (\boxtimes \sqsubseteq v^\sharp \wedge E = \emptyset \wedge R = \{x\}) \\ \phantom{(E, R, H) \models_{\rho} x \doteq v^\sharp \iff} \vee \exists v \in \gamma_{\rho}(v^\sharp) \wedge E = \{(x, v)\} \wedge R = \emptyset $$

$$ (E, R, H) \models_{\rho} l \mapsto \{o\} \iff E = R = \emptyset \wedge \exists o_0 \in \gamma_{\rho}(\{o\}) . H = \{(\rho(l), \mathbf{f}, o_0)\} $$

$$ (E, R, H) \models_{\rho} k \mapsto \{o\} \iff E = R = \emptyset \wedge \exists (o_i) \in (\gamma_{\rho}(\{o\}))^{\rho(k)}. H = \bigcup_{l^i \in \rho(k)} \{(\rho(l), \mathbf{f}, o_i)\} $$

<caption>Figure 3: Definition of the entailment predicate $\models_{\rho}$.</caption>

The approach for correctness is the same than in [?]: we require every abstract rule to be locally correct, i.e., their transfer functions (noted for axioms $ax$ and $ax^\sharp$ in the respective concrete and abstract semantics) and side conditions (noted $cond$ and $cond^\sharp$) follow the corresponding concrete rules, taking into account a potential context. The local correctness conditions over transfer functions and side conditions of axiom rules follow—the correctness of other types of rule is very similar. Because of the context in the side condition, it is possible to have a rule whose side condition holds, but whose semantic context does not match the transfer function: this amounts to say that the construction of a derivation can be blocked if some resources are lacking in the original semantic context. We shall not extend on this technical matter. We can infer from these local properties the global correctness.

$$ \begin{align*} \forall S, \Phi, \Phi_c. S \in \gamma(\Phi_c \boxplus \Phi) &\implies ax(S) \in \gamma(\Phi_c \boxplus ax^\sharp(\Phi)) \\ \forall i, S, \Phi, \Phi_c. S \in \gamma(\Phi_c \boxplus \Phi) &\implies cond_i(S) \implies cond_i^\sharp(\Phi) \end{align*} $$

**Property 1 (Global Correctness)** Let $t$ be a term, $S$ and $S'$ be states, and $\Phi$ and $\Phi'$ formulae. Given the local correctness, if $S \in \gamma(\Phi)$, $S, t \Downarrow S'$, and $\Phi, t \Downarrow^\sharp \Phi'$ then $S' \in \gamma(\Phi')$.

In other words, abstract derivations can not miss concrete executions: our abstract semantics is sound.

## 7. Related Work

This work directly follows from [?], which only focussed on abstract interpretation and how to make a Coq development scale up to big operational semantics such as JAVASCRIPT's. This previous work
came with a Coq development containing some generic analysers, while the current work only focuses at building an abstract domain compatible with the frame rule. There have been works aiming at providing formally verified analysers on languages other than JAVASCRIPT such as [?], but these involve a lot of Coq development and we hope to get to a comparatively lighter development for JAVASCRIPT. We aim at diving the work of [?] to a fully Coq-verified abstract interpreter.

There have been some work about mixing abstract interpretation and separation logic, such as [?] or [?], but few provide an abstract semantics compatible with the frame rule able to express the abstractions of shape analysis. The lattices constructed by these works are based on a disjunctive completion of a formula order, which can easily explode in size. Our mechanism provides a protection against these explosions through summarizations, with the cost of potentially big imprecision.

The logic of [?] is very close to this work; their domain is a disjunctive completion of formulae separated at the field level of objects as we did. Locations and fields are both abstracted by either singletons or summary nodes. However, the frame rule is not mentioned, which removes the need of membranes. They carry a set of formulae storing information about the respective inclusion of the concretisations of summary nodes. Their domain is ordered and equipped with a join and a widening operator with an algorithm compatible with the concretisation function.

The same authors previously developped [?] based on separation logic; this work focusses on inductively defined shapes and is able to express and analyse complex structures such as red-black trees. To increase the efficiency of the analyse, they developed a way to change the point of view of these shapes: for instance, a doubly linked list can be defined either by following *next* or *previous* fields. As with this work, the order relation, are defined through an algorithm compatible with the concretisation function, and they similarly defined joins and widenings by an algorithm.

Inductively defined structures have also been examined in [?], which uses abduction to determine the weakest precondition wielding safety or termination of the analysed program. They provide heuristics to infer how to generalize predicates, as well as a running tool. However, their heuristics rely on the syntax of their toy language (comparable to OWHILE): scaling such an analyser up to JAVASCRIPT might require to look for much complex heuristics, and we think that an approach guided directly by the language semantics can reduce the amount of work to get a certified analyser.

## 8. Conclusion and Future Works

We have presented a program logic for JAVASCRIPT heaps, based on separation logic and integrating ideas from shape analysis. We have expressed this logic within a framework of certified abstract interpretation. The goal is to scale up the logic to the size of JAVASCRIPT's semantics, resulting in an abstract semantics for JAVASCRIPT of reasonable size, and eventually certified analysers for JAVASCRIPT. The particular problem addressed in this paper is that of integrating the frame rule to existing abstract interpretation framework, which is known to be a difficult problem.

Our approach is precise enough to get interesting results on real-world programs, whilst being simple enough to be able to scale it up to a certified abstract semantics of JAVASCRIPT. This work is part of a larger project which aims at building certified static analyses based on the JSCERT [?] formal semantics of JAVASCRIPT.

We have focussed on how to build an abstract semantics, and not on how to build analysers. The abstract domains that arise from our logic are less structured than usual abstract domains, which means that an analyser will be less guided by the abstract interpretation framework. There is thus room for further research into the construction of efficient join and widening operators for abstract domains combining separation and summarization. Furthermore, the frame rule allows to individually analyse functions or recurrent programs; it is thus natural to look for strategies to choose and separately analyse these programs. We have observed that analysing a program without starting from the right resources can lead to big approximations, or to the inability to analyse. Techniques
$$
\begin{array}{l@{\hspace{2em}}l@{\hspace{2em}}l@{\hspace{2em}}l@{\hspace{2em}}l@{\hspace{2em}}l}
s ::= & \mathit{skip} & | s_1; s_2 & | \mathit{ife} s_1 s_2 & e ::= & n \in \mathbb{Z} & | ? & | x \in \mathit{Var} & | \mathit{nil} \\
| \mathit{while} e s & | \mathit{throw} & | x := e & | \{\} & | e.f & | \mathit{f} \mathit{in} e & | \neg e \\
| e_1.f := e_2 & | \mathit{delete} e.f & | & | = e_1 e_2 & | \bowtie e_1 e_2 & (\bowtie \in \{>, +, -\})
\end{array}
$$

(a) Statements

(b) Expressions

$$
\begin{array}{l@{\hspace{2em}}l@{\hspace{2em}}l@{\hspace{2em}}l@{\hspace{2em}}l@{\hspace{2em}}l}
s_e ::= & ;_1 s_2 & | \mathit{if}_1 s_1 s_2 & | \mathit{while}_1 e s & e_e ::= & .f & | \mathbf{f} \mathbf{in}_1 & | \bowtie_1 e_2 \\
         & | \mathit{while}_2 e s & | x :=_1 & | .f :=_1 e_2 & | \bowtie_2 & | \neg_1 & | =_1 e_2 \\
         & | .f :=_2 & | \mathit{delete}_1 .f & & | =_2 & &
\end{array}
$$

(c) Extended statements

(d) Extended expressions

<caption>Figure 4: Complete syntax of the OWHILE language</caption>

like bi-abduction may be relevant to build efficient oracles for our certified analysers.

A. Concrete Semantics

Figure ?? presents the complete syntax of OWHILE, which includes extended terms. These extended
terms carry intermediary results, and are thus associated with specific kinds of extended semantic
contexts, carrying additional values. The concrete rules follow. These rules makes use of functions
such as *read* and *write* which perform some semantic manipulation; their semantics is usual and we do
not explicit them. Section ?? categorizes rules into four different kinds of categories; Figure ?? shows
where all the rules of this semantics fall. As can be seen, the categories are more or less identical in
size, with the notable exception of the computational rules, which are the most difficult to abstract.

$$
\frac{\text{ABORTEXTEXPR}(e_e)}{\sigma, e_e \Downarrow Err} \qquad \sigma = Err
$$

$$
\frac{\text{ABORTEXTSTAT}(s_e)}{\sigma, s_e \Downarrow Err} \qquad \sigma = Err
$$

$$
\frac{\text{CST}(n)}{S, n \Downarrow (S, n)}
$$

$$
\frac{\text{RANDOM}(n)}{S, ? \Downarrow (S, n)}
$$

$$
\frac{\text{VAR}(\mathbf{x})}{S, \mathbf{x} \Downarrow (S, \text{read}(S, \mathbf{x}))} \qquad \mathbf{x} \in \text{dom}(S)
$$

$$
\frac{\text{VARUNDEF}(\mathbf{x})}{S, \mathbf{x} \Downarrow \text{Err}} \quad \mathbf{x} \notin \text{dom}(S)
$$
NIL
$S, nil \Downarrow (S, l^0)$

NEWOBJ
$S, \{\} \Downarrow (S, l^{fresh(S)})$

PROPERTY1(f)
$(S, l^i), .f \Downarrow (S, read(S, l^i .f))$ $l^i .f \in dom(S)$

PROPERTY1UNDEF(f)
$(S, l^i), .f \Downarrow Err$ $l^i .f \notin dom(S)$

IN1TRUE(f)
$(S, l^i), f \text{ in } l^1 \Downarrow (S, 1)$ $l^i .f \in dom(S)$

IN1FALSE(f)
$(S, l^i), f \text{ in } l^1 \Downarrow (S, 0)$ $l^i .f \notin dom(S)$

OP(⊠, e₁, e₂)
$\frac{S, e_1 \Downarrow r \quad r, \bowtie_1 e_2 \Downarrow r'}{S, \bowtie e_1 e_2 \Downarrow r'}$

OP1(⊠, e₂)
$\frac{S, e_2 \Downarrow r \quad (n_1, r), \bowtie_2 r'}{(S, n_1), \bowtie_1 e_2 \Downarrow r'}$

OP1ERROR(⊠, e₂)
$(S, l^i), \bowtie_1 e_2 \Downarrow Err$

OP2ERROR(⊠)
$(n_1, (S, l^j)), \bowtie_2 \Downarrow Err$

ADD2
$(n_1, (S, n_2)), +_2 \Downarrow (S, n_1 + n_2)$

SUB2
$(n_1, (S, n_2)), -_2 \Downarrow (S, n_1 - n_2)$

GREATER2GREATER
$(n_1, (S, n_2)), >_2 \Downarrow (S, 1)$

$n_1 > n_2$

GREATER2LESSEREQ
$(n_1, (S, n_2)), >_2 \Downarrow (S, 0)$

$n_1 \le n_2$

NOT(e)
$\frac{S, e \Downarrow r \quad r, \neg_1 \Downarrow r'}{S, \neg e \Downarrow r'}$

NOT1TRUE
$(S, n), \neg_1 \Downarrow (S, 0)$ $n \ne 0$

NOT1FALSE
$(S, n), \neg_1 \Downarrow (S, 1)$ $n = 0$

NOT1ERROR
$(S, l), \neg_1 \Downarrow Err$

EQ(e₁, e₂)
$\frac{S, e_1 \Downarrow r \quad r, =_1 e_2 \Downarrow r'}{S, =_1 e_2 \Downarrow r'}$

EQ1(e₂)
$\frac{S, e_2 \Downarrow r \quad (v_1, r), =_2 \Downarrow r'}{(S, v_1), =_1 e_2 \Downarrow r'}$

EQ2BASICVALEQ
$(n_1, (S, n_2)), =_2 \Downarrow (S, 1)$ $n_1 = n_2$

EQ2BASICVALNEQ
$(n_1, (S, n_2)), =_2 \Downarrow (S, 0)$

$n_1 \ne n_2$

EQ2LOCEQ
$(l^i, (S, l^j)), =_2 \Downarrow (S, 1)$ $l^i = l^j$

EQ2LOCNEQ
$(l^i, (S, l^j)), =_2 \Downarrow (S, 0)$

$l^i \ne l^j$

EQ2MISTYPEBASICVALLOC
$(n_1, (S, l^j)), =_2 \Downarrow Err$

EQ2MISTYPELOCBASICVAL
$(l^i, (S, n_2)), =_2 \Downarrow Err$

SKIP
$S, skip \Downarrow S$

SEQ(s₁, s₂)
$\frac{S, s_1 \Downarrow r \quad r, ;_1 s_2 \Downarrow r'}{S, s_1; s_2 \Downarrow r'}$

SEQ1(s₂)
$\frac{S, s_2 \Downarrow r}{S, ;_1 s_2 \Downarrow r}$

THROW
$S, throw \Downarrow Err$
<table><caption>Figure 5: Categories of rules</caption><thead><tr><th>Administrative</th><th>Conditions</th><th>Error</th><th>Computational</th></tr></thead><tbody><tr><td>Property (e, f)</td><td>AbortExtExpr (e<sub>e</sub>)</td><td>VarUndef(x)</td><td></td></tr><tr><td>In (f, e)</td><td>AbortExtStat (s<sub>e</sub>)</td><td>Property1NoLoc (f)</td><td>Cst(n)</td></tr><tr><td>Op (⊠, e<sub>1</sub>, e<sub>2</sub>)</td><td>In1True (f)</td><td>Property1Undef (f)</td><td>Random(n)</td></tr><tr><td>Op1 (⊠, e<sub>2</sub>)</td><td>In1False (f)</td><td>In1NoLoc (f)</td><td>Var (x)</td></tr><tr><td>Not (e)</td><td>Greater2Greater</td><td>Op1Error (⊠, e<sub>2</sub>)</td><td>Nil</td></tr><tr><td>Eq (e<sub>1</sub>, e<sub>2</sub>)</td><td>Greater2LesserEq</td><td>Op2Error (⊠)</td><td>NewObj</td></tr><tr><td>Eq1 (e<sub>2</sub>)</td><td>Not1True</td><td>Not1Error</td><td>Property1 (f)</td></tr><tr><td>Skip</td><td>Eq2BasicValEq</td><td>Eq2MistypeBasicValLoc</td><td>Add2</td></tr><tr><td>Seq (s<sub>1</sub>, s<sub>2</sub>)</td><td>Eq2BasicValNeq</td><td>Eq2MistypeLocBasicVal</td><td>Sub2</td></tr><tr><td>Seq1 (s<sub>2</sub>)</td><td>Eq2LocEq</td><td>If1Error (s<sub>1</sub>, s<sub>2</sub>)</td><td>Asgn1 (x)</td></tr><tr><td>If (e, s<sub>1</sub>, s<sub>2</sub>)</td><td>Eq2LocNeq</td><td>While2Error (e, s)</td><td>PropertyAsgn2 (f)</td></tr><tr><td>While (e, s)</td><td>If1True (s<sub>1</sub>, s<sub>2</sub>)</td><td>Throw</td><td>Delete1 (f)</td></tr><tr><td>While1 (e, s)</td><td>If1False (s<sub>1</sub>, s<sub>2</sub>)</td><td>PropertyAsgn1Error (f, e<sub>2</sub>)</td><td></td></tr><tr><td>Asgn (x, e)</td><td>While2True (e, s)</td><td>PropertyAsgn1Nil (f, e<sub>2</sub>)</td><td></td></tr><tr><td>PropertyAsgn (e<sub>1</sub>, f, e<sub>2</sub>)</td><td>While2False (e, s)</td><td>Delete1Error (f)</td><td></td></tr><tr><td>Delete (e, f)</td><td>PropertyAsgn1 (f, e<sub>2</sub>)</td><td></td><td></td></tr><tr><td></td><td>Delete1Nil (f)</td><td></td><td></td></tr></tbody></table>

Our algorithm starts by splitting $\Phi_1$ to remove disjunctions in the values of variables and abstract locations $l$. In the example $x \doteq l \sqcup k$ can be split into $x \doteq l$ and $x \doteq k$ to get the two formulae $\Phi_{1,a}$ and $\Phi_{1,b}$ below. This is sound as the disjunction $\sqcup$ we chose for values does not lose precision: $\forall \Phi_c. \gamma (\Phi_c \triangleright \Phi_1) = \gamma (\Phi_c \triangleright \Phi_{1,a}) \cup \gamma (\Phi_c \triangleright \Phi_{1,b})$.

$$ \Phi_{1,a} = (k_0 \to k, l_0 \to l | x \doteq l \star k \mapsto \{f : \perp, g : l, \_, \_ : \boxtimes\} \star l \mapsto \{f : l \sqcup k, \_, \_ : \boxtimes\}) $$

$$ \Phi_{1,b} = (k_0 \to k, l_0 \to l | x \doteq k \star k \mapsto \{f : \perp, g : l, \_, \_ : \boxtimes\} \star l \mapsto \{f : l \sqcup k, \_, \_ : \boxtimes\}) $$

Let us focus on $\Phi_{1,a}$. We look for a function $\psi$ translating identifiers of the formula $\Phi_{1,a}$ to those of $\Phi_2$ in order to match $\Phi_{1,a}$ with $\Phi_2$. Here the function $\psi$ mapping $l$ to $l'$ and $k$ to $k'$ is enough. Applying the rewriting $\psi$ over $\Phi_{1,a}$ follows the same rules as the $\alpha$-renaming and the summarization presented in Sections ?? and ??—which is why summarizations are compatible with this pre-order:

$$ \psi (\Phi_{1,a}) = (k_0 \to k', l_0 \to l' | x \doteq l' \star k' \mapsto \{f : \perp, g : l, \_, \_ : \boxtimes\} \star l' \mapsto \{f : l' \sqcup k', \_, \_ : \boxtimes\}) $$

The summary node $k$ has an incoherence: every concrete location represented by $k$ is supposed to have a field $f$ represented by $\perp$, which is not possible: the only possible concretisation of $k$ is the empty set. We can thus safely remove $k$ from the formula:

$$ \Phi'_{1,a} = (k_0 \to \emptyset, l_0 \to l' | x \doteq l' \star l' \mapsto \{f : l', \_, \_ : \boxtimes\}) $$

At this point, we compare the inner scope of $\Phi_{1,a}$ with the one of $\Phi_2$: the latter has an additional summary node $k'$. We can easily ignore such a summary node as it can represent an empty set of concrete locations; we thus rewrite $k'$ into $\emptyset$ in $\Phi_2$ to get $\Phi'_2 = (k_0 \to l', l_0 \to l' | x \doteq l' \star l' \mapsto \{f : l' \sqcup nil, \_, \_ : \boxtimes\})$. We now compare the values in the membrane, the variables, and the objects; which we can check are greater in $\Phi'_2$ for any corresponding in $\Phi'_{1,a}$. We have successfully found a $\psi$ leading to the conclusion $\forall \Phi_c. \gamma (\Phi_c \triangleright \Phi_{1,a}) \subseteq \gamma (\Phi_c \triangleright \Phi_2)$.

In the case of $\Phi_{1,b}$ we can perform a materialization, as the have an entry point to a summary node $x \doteq k$. But this generates a subformula $l' \mapsto \{f : \perp, g : l, \_, \_ : \boxtimes\}$, which has an empty concretisation as the reference $l'$. $f$ should be $\perp$. We can conclude that $\Phi_{1,b}$ has an empty concretisation, and thus $\Phi_{1,b} \prec \Phi_2$. Overall, as both $\Phi_{1,a}$ and $\Phi_{1,b}$ are below $\Phi_2$ by the pre-order $\prec$, we have $\Phi_1 \prec \Phi_2$.
## B.2. General Procedure

As we want to be able to perform summarizations and materializations, our algorithm has to take these operations into account. Algorithm ?? shows its pseudo-code; it proceeds through two nested loops. The first one splits the first formula $\Phi_1$ into more precise formulae $\Phi'_1$ through materializations. The second tries to match the more precise $\Phi'_1$ with $\Phi_2$ by performing summarizations. We then look for incoherences, then compare the variables and the objects of the two formulae. The two loops could be removed without causing problems for the final theorem; however they are necessary to make materializations and summarizations hold. Formulae with different interfaces are rejected, even if they have the same concretisation in every context: the relation $\prec$ does not have to be complete.

The first step consists in splitting the formula $\Phi_1$ to remove the presence of join operators $\cup$ in the abstract values; as for the formulae $\Phi_{1,a}$ and $\Phi_{1,b}$ of the example above. Because of the way we defined abstract values, we can split values of the form $n^\sharp \cup nil^? \cup l_1 \cup \dots \cup l_n \cup d$ to their different components without missing any concrete value. This splitting can only be done if the considered abstract value represents only one concrete value; which is neither the case of the default abstract values of objects$^3$, as in the object $\{\_ : nil \cup \Box\}$, nor of a field value pointed by a summary node $k$.

The splitting part also takes into account the materializations in $\Phi_1$. This explodes the number of considered formulae $\Phi'_1$ as this amounts to look for all possible aliases of $\Phi_1$. These materializations are performed for each entry point to a summary node and performed as described in Section ??.
Unfortunately, this part can loop. For instance, consider the inner formula $x \doteq k \star k \mapsto \{f : k, \_ : \top\}$: we can materialize $x$ to get $x \doteq l_1 \star l_1 \mapsto \{f : l_1 \cup k, \_ : \top\} \star k \mapsto \{f : l_1 \cup k, \_ : \top\}$, which splits into $x \doteq l_1 \star l_1 \mapsto \{f : k, \_ : \top\} \star k \mapsto \{f : l_1 \cup k, \_ : \top\}$, which keeps materializing/splitting. But do we need to split it indefinitely? The only goal of this algorithm is to compare the current formula with $\Phi_2$: unfolding up to the size of $\Phi_2$ is enough. Unfoldings can significantly increase the complexity of this algorithm; however, its correction still holds if we limit this unfolding to a given depth—at the cost of the transitivity of $\prec$. This is the reason we say that $\prec$ is only the subset of a pre-order: it is possible to compute it completely and get a complete pre-order, with the cost of efficiency.

This first step makes us consider every possible shape structure. The next step is run on each of these exploded formulae $\Phi'_1$ and succeeds if it succeeded for all instances (universal search). This step accepts a formula $\Phi'_1$ if it can prove that $\forall \Phi_c. \gamma(\Phi_c \oplus \Phi'_1) \subseteq \gamma(\Phi_c \oplus \Phi_2)$. As $\forall \Phi_c. \gamma(\Phi_c \oplus \Phi_1) = \cup \gamma(\Phi_c \oplus \Phi'_1)$, an acceptance yields the requested property $\forall \Phi_c. \gamma(\Phi_c \oplus \Phi_1) \subseteq \gamma(\Phi_c \oplus \Phi_2)$.

For each of these exploded formulae $\Phi'_1$, we look for two functions $\psi_l : LLoc^\sharp \to (LLoc^\sharp \cup KLoc^\sharp)$ and $\psi_k : KLoc^\sharp \to KLoc^\sharp$ translating identifiers of the formula $\Phi'_1$ to those of $\Phi_2$; which we shall note both $\psi$. The goal is to find a translation matching $\Phi'_1$ with $\Phi_2$. Some restrictions applies to $\psi$:

* Only identifiers present in $\Phi'_1$ and $\Phi_2$ can appear in $\psi$. This makes this step a finite search.

* For an abstract location $l$, at most one $l_0$ reaches $l$: $\forall l, l_1, l_2. \psi(l_1) = \psi(l_2) = l \Rightarrow l_1 = l_2$.

We rewrite $\Phi'_1$ into the formula $\Phi_1'' = \psi(\Phi'_1) = (\psi | emp) \oplus \Phi'_1$ where $\psi$ has been identified with its graph. If two or more abstract locations are mapped through $\psi$ to the same summary node $k$, then all their objects are merged; this step fails if one abstract location lacks a memory property in $\Phi'_1$. For instance, if $\psi(l) = \psi(k) = k'$ and that $\Phi'_1 = (k_0 \to k, l_0 \to l | l \mapsto \{o_1\} \star k \mapsto \{o_2\})$, then $\Phi_1'' = (k_0 \to k', l_0 \to k' | k' \mapsto \{o'_1\} \cup \{o'_2\})$ where $\{o'_1\}$ and $\{o'_2\}$ received the renaming process of $\psi$. However, the same choice of $\psi$ fails if only $l \mapsto \{o\}$ appears in $\Phi'_1$.

We execute the last step for all those $\psi$ and return true if at least one of these make the following step returns true (existential choice). The research of a working $\psi$ can probably be performed more

<footnote>$^3$The default abstract value of the objects can actually be split to make the fields appearing in $\Phi_2$ appear, then perform nevertheless splittings and later on materializations. For readability reasons, we shall not go into details about this as the subset of pre-order we get if we do not make this step is still enough to get a correct abstract semantics.</footnote>
**Data:** Two abstract heaps $\Phi_1$ and $\Phi_2$.

**Result:** true iff $\Phi_1 \preceq \Phi_2$.

if *interface*($\Phi_1$) ≠ *interface*($\Phi_2$) then
| return false; // Formulae with different interfaces are immediately rejected.

end

for $\Phi'_1$ be a split/materialization of $\Phi_1$ do // Universal branching

for $\psi$ well-formed do // Existential choice

$\Phi'_1 \leftarrow \psi(\Phi'_1);$

Remove incoherent summary nodes from $\Phi'_1$;

Let $\Phi'_2$ be $\Phi_2$ where every summary node not present in $\Phi'_1$ has been removed;

if $\Phi'_1$ incoherent then

// The current $\psi$ is enough to show that $\Phi'_1 \preceq \Phi_2$.

Continue on the next split $\Phi'_1$ of $\Phi_1$;

end

if $\Phi'_2$ incoherent then

| Try another $\psi$;

end

for $h \to h_1 + \dots + h_n$ present in $\Phi'_2$ and $h \to h'_1 + \dots + h'_m$ in $\Phi''_1$ do

| if $\{h'_1, \dots, h'_m\} \not\subseteq \{h_1, \dots, h_n\}$ then

| Try another $\psi$;

end

end

for $x \doteq v_2^\sharp$ present in $\Phi'_2$ and $x \doteq v_1^\sharp$ present in $\Phi''_1$ do

| if $v_1^\sharp \not\supseteq v_2^\sharp$ then

| Try another $\psi$;

end

end

for $h \mapsto \{o_2\}$ present in $\Phi'_2$ and $h \mapsto \{o_1\}$ present in $\Phi''_1$ do

| if $\{o_1\} \not\supseteq \{o_2\}$ then

| Try another $\psi$;

end

end

// The chosen $\psi$ succeeded in matching $\Phi'_1$ with $\Phi'_2$.

Continue on the next split $\Phi'_1$ of $\Phi$;

end

// No $\psi$ succeeded in matching $\Phi'_1$ with $\Phi'_2$.

return false;

end

// $\Phi_2$ correctly captures all the behaviours of $\Phi_1$.

return true;

**Algorithm 1:** Algorithm comparing formulae.
efficiently, by only considering the possible ones in an iterative algorithm similar to the one of [?]. The last step consists at comparing the exploded and renamed formula $\Phi_1''$ to $\Phi_2'$, by checking for incoherences, then comparing the membranes, variables, and objects defined.

We look for incoherences into the formula $\Phi_1''$. If any is found, then the concretisation of $\Phi_1''$ is empty, and we immediately states that $\Phi_1'' \preceq \Phi_2''$ by returning true. There are two cases of incoherences. First, spatial incoherences, when a location $l$ is referred several times in the formula in a left-hand side; such as in $l \mapsto \{o\} \star l \mapsto \{o\}$. Even if the two objects $\{o\}$ are identical, both sides of the operator $\star$ refer to the same region of space, which is forbidden. Second, when a variable or the field $f$ of an abstract location $l$ has $\perp$ as a value, which has an empty concretisation. Note that $\perp$ found in summary nodes does not trigger incoherences for the whole abstract state. Consider for instance the formula $(k_0 \to k | k \mapsto \{f: \perp, \_, \top\})$: $k$ can represent an empty set of location, which solves the incoherence. Incoherent summary nodes are removed, which can lead to an incoherence later on. For instance $(k_0 \to k | k \mapsto \{f: \perp, \_, \top\} \star x \doteq k)$ leads to $(k_0 \to \emptyset | x \doteq \perp)$, which has an empty concretisation. We also check for spatial incoherences in $\phi_2$: if any, we stop and return false (unless $\phi_1$ already had an incoherence). At this stage, $\Phi_2$ may have more summary nodes than $\Phi_1''$; this is acceptable as summary nodes can represent empty sets of concrete locations. We thus remove these additional summary nodes in $\Phi_2$ to get $\Phi_2'$.

The last step is a direct comparison between the modified formulae $\Phi_1''$ and $\Phi_2'$. There are three factors to take into account: membranes, environments (expressed through variables), and spatial properties. For membranes, we check that every rewritings in $\Phi_2'$ rewrites abstract locations to more abstract locations than in $\Phi_1''$: these renamings represent the inner abstract locations under which these outer abstract locations “hide”. For variables, we check that every variable has a lesser value in $\Phi_1''$ than in $\Phi_2'$ in the lattice of abstract values. For spatial properties, we check that each abstract locations $h$ of $\Phi_1''$ is associated a lesser object than in $\Phi_2'$. This step concludes the algorithm.

Note how we perform the splitting and materialization step of the formula $\Phi_1$ before trying to match its locations with these of $\Phi_2$ through $\psi$. If we had reversed the order of these two operations, the following comparison would not hold. In other words, we can choose in the following example whether $l'$ represents $l_1$ or $l_2$ after choosing whether the reference $l.f$ points to $l_1$ or $l_2$.

$$ (l_0 \to l, k \to l_1 + l_2 | l \mapsto \{f: l_1 \sqcup l_2, \_, \top\} \star l_1 \mapsto \{a: nil, \_, \top\} \star l_2 \mapsto \{b: nil, \_, \top\}) \\ \preceq (l_0 \to l, k \to l' + l'' | l \mapsto \{f: l', \_, \top\} \star l' \mapsto \{a: nil \sqcup \top, b: nil \sqcup \top, \_, \top\} \star l'' \mapsto \{_, \top\}) $$

This comparison algorithm defines a relation $\preceq$ with the property of being compatible with the transformations we were looking for: $\alpha$-conversion of inner locations, materializations, and summarizations. Indeed, if $\Phi$ becomes $\Phi'$ by one of these transformations, we get $\Phi \preceq \Phi'$, which allows to rewrite from one to the other when passing through the $glue_i^\sharp(\mathcal{U}^\sharp)$ function (see Section ??). We now claim that this comparison algorithm can be used as a valid relation in this work.

**Property 2** *Algorithm ?? defines a suitable relation $\preceq$:*

$$ \forall \Phi_1, \Phi_2. \Phi_1 \preceq \Phi_2 \Rightarrow \forall \Phi_c. \gamma(\Phi_c \triangleright \Phi_1) \subseteq \gamma(\Phi_c \triangleright \Phi_2) $$

This property takes as lemma the similar results for the intermediate parts of the algorithm: it is still valid if we remove the first or the second loop; this will just remove the ability we have to perform materializations and summarizations.