* (13) Chalupa, M., Jašek, T., Tomovič, L., Hruška, M., Šoková, V., Ayaziová, P., Strejček, J., Vojnar, T.:  Symbiotic 7: Integration of Predator and More (Competition Contribution).  In Proc. of TACAS’20, vol. 12079 of LNCS, pp. 413–417. Springer (2020)
  * (14) Chang, B.-Y. E., Rival, X., Necula, G.C.:  Shape analysis with structural invariant checkers.  In: Proc. of SAS’07, vol. 4634 of LNCS, pp. 384–401. Springer (2007)
  * (15) Cox, A., Chang, B.-Y. E., Li, H., Rival, X.:  Abstract Domains and Solvers for Sets Reasoning.  In: Proc. of LPAR’15, vol. 9450 of LNCS, pp. 356–371. Springer (2015)
  * (16) Dudka, K., Holík, L., Peringer, P., Trtík, M., Vojnar, T.:  From Low-Level Pointers to High-Level Containers.  In: Proc. of VMCAI’16, vol. 9583 of LNCS, pp. 431–452. Springer (2016)
  * (17) Dudka, K., Peringer, P., Vojnar, T.:  An Easy to Use Infrastructure for Building Static Analysis Tools.  In: Proc. of EUROCAST’11, vol. 6927 of LNCS, pp. 527–534. Springer (2012)
  * (18) Dudka, K., Peringer, P., Vojnar, T.:  Predator: A Practical Tool for Checking Manipulation of Dynamic Data Structures Using Separation Logic.  In: Proc. of CAV’11, vol. 6806 of LNCS, pp. 372–378. Springer (2011)
  * (19) Dudka, K., Peringer, P., Vojnar, T.:  Predator: Byte-Precise Verification of Low-Level List Manipulation.  In: Proc. of SAS’13, vol. 7935 of LNCS, pp. 214–237. Springer (2013)
  * (20) Habermehl, P., Holík, L., Rogalewicz, A., Šimáček, J., Vojnar, T.:  Forest Automata for Verification of Heap Manipulation.  Formal Methods in System Design, 41(1), Springer (2012)
  * (21) Heizmann, M. et al.:  Ultimate Automizer with an On-Demand Construction of Floyd-Hoare Automata.  In: Proc. of TACAS’17, vol. 10206 of LNCS, pp. 394–398. Springer (2017)
  * (22) Holík, L., Kotoun, M., Peringer, P., Šoková, V., Trtík, M., Vojnar, T.:  Predator Shape Analysis Tool Suite.  In: Proc. of HVC’16, vol. 10028 of LNCS, pp. 202–209. Springer (2016)
  * (23) Kreiker, J., Seidl, H., Vojdani, V.:  Shape Analysis of Low-Level C with Overlapping Structures.  In: Proc. of VMCAI’10, vol. 5944 of LNCS, pp. 214–230. Springer (2010)
  * (24) Laviron, V., Chang, BY.E., Rival, X.:  Separating Shape Graphs.  In: Proc. of ESOP’10, vol. 6012 of LNCS, pp. 387–406. Springer (2010)
  * (25) Le, Q.L., Gherghina, C., Qin, S., Chin, W.-N.:  Shape Analysis via Second-Order Bi-Abduction.  In: Proc. of CAV’15, vol. 9206 of LNCS, pp. 52–68. Springer (2015)
  * (26) Löwe, S., Mandrykin, M.U., Wendler, P.:  CPAchecker with Sequential Combination of Explicit-Value Analyses and Predicate Analyses (Competition Contribution).  In Proc. of TACAS’14, vol. 8413 of LNCS, pp. 392–394. Springer (2014)
  * (27) Malík, V., Martiček, Š., Schrammel, P., Srivas, M.K., Vojnar, T., Wahlang, J.:  2LS: Memory Safety and Non-termination (Competition Contribution).  In Proc. of TACAS’18, vol. 10806 of LNCS, pp. 417–421. Springer (2018)
  * (28) Malík, V., Hruška, M., Schrammel, P., Vojnar, T.:  Template-Based Verification of Heap-Manipulating Programs.  In Proc. of FMCAD’18. IEEE (2018)
  * (29) Marron, M., Hermenegildo, M., Kapur, D., Stefanovic, D.:  Efficient Context-Sensitive Shape Analysis with Graph Based Heap Models.  In: Proc. of CC’08, vol. 4959 of LNCS, pp. 245–259. Springer (2008)
  * (30) Muller, P., Peringer, P., Vojnar, T.:  Predator Hunting Party (Competition Contribution).  In: Proc. of TACAS’15, vol. 9035 of LNCS, pp. 443–446. Springer (2015)
  * (31) Muller, P., Vojnar, T.:  CPAlien: Shape Analyzer for CPAChecker (Competition Contribution).  In Proc. of TACAS’14, vol. 8413 of LNCS, pp. 395–397. Springer (2014)
  * (32) Peringer, P., Šoková, V., Vojnar, T.:  PredatorHP Revamped (Not Only) for Interval-Sized Memory Regions and Memory Reallocation (Competition Contribution).  In Proc. of TACAS’20, vol. 12079 of LNCS, pp. 408–412. Springer (2020)
  * (33) Reps, T., Horwitz, S., Sagiv, M.:  Precise Interprocedural Dataflow Analysis via Graph Reachability.  In: Proc. of POPL’95, pp. 49–61. ACM Press (1995)
  * (34) Rival, X., et al.:  The MemCAD Analyzer.  Available at https://www.di.ens.fr/~rival/memcad.html. (2016)
  * (35) Sagiv, M., Reps, T., Wilhelm, R.:  Parametric shape analysis via 3-valued logic.  ACM Transactions on Programming Languages and Systems (TOPLAS), 24(3), ACM (2002)
  * (36) Tuch, H.:  Formal Verification of C Systems Code.  Journal of Automated Reasoning, 42(2–4), Springer (2009)
  * (37) Yang, H., Lee, O., Calcagno, C., Distefano, D., O’Hearn, P.W.:  On Scalable Shape Analysis.  Technical report RR-07-10, Queen Mary, University of London (2007)
  * (38) Yang, H., Lee, O., Berdine, J., Calcagno, C., Cook, B., Distefano, D., O’Hearn, P.W.:  Scalable Shape Analysis for Systems Code.  In: Proc. of CAV’08, vol. 5123 of LNCS, pp. 385–398. Springer (2008)

## Appendix

##  0.8 Data Reinterpretation of Nullified Blocks

In this appendix, we present a detailed description of the algorithms for read
and write reinterpretation of nullified blocks, which were briefly introduced
in Section 0.3.1. Given an SMG $G=(O,V,\Lambda,H,P)$, we define
$H_{ov}(o,o\\!f,t)$ as the set of all has-value edges leading from $o$ whose
fields overlap with the field $(o\\!f,t)$, i.e.:

$H_{ov}(o,o\\!f,t)=\\{(o\raisebox{-1.29167pt}{$\xrightarrow{\smash{\raisebox{-0.43057pt}{$\scriptstyle
o\\!f^{\prime},t^{\prime}$}}}$}v)\in H\mid
I(o\\!f,t)\;\cap\;I(o\\!f^{\prime},t^{\prime})\;\neq\;\emptyset\\}.$

Further, we define $H_{zr}(o,o\\!f,t)$ as the subset of $H_{ov}(o,o\\!f,t)$
containing all its edges leading to $0$, i.e.:

$H_{zr}(o,o\\!f,t)=\\{(o\raisebox{-1.29167pt}{$\xrightarrow{\smash{\raisebox{-0.43057pt}{$\scriptstyle
o\\!f^{\prime},t^{\prime}$}}}$}0)\in H_{ov}(o,o\\!f,t)\\}.$

###  0.8.1 Read Reinterpretation of Nullified Blocks

Algorithm 1 gives the algorithm of read reinterpretation instantiated for
dealing with nullified blocks of memory as precisely as possible.

Algorithm 1 $\mathit{readValue}(G,o,o\\!f,t)$

Input:

  * •

An SMG $G=(O,V,\Lambda,H,P)$.

  * •

An object $o\in O$.

  * •

A field $(o\\!f,t)$ within $o$, i.e.,
$o\\!f+\textit{size}(t)\leq\textit{size}(o)$.

Output:

  * •

A tuple $(G^{\prime},v)$ that is the result of read reinterpretation of $G$
wrt the object $o$ and the field $(o\\!f,t)$ such that fields representing
nullified memory are read as precisely as the notion of SMGs allows (i.e., the
operator recognises that the field to be read is nullified iff the input SMG
guarantees that each byte of the field is indeed zero).

Method:

  1. 1.

Let $v:=H(o,o\\!f,t)$.

  2. 2.

If $v\neq\bot$, return $(G,v)$.

  3. 3.

If the field to be read is covered by nullified blocks, i.e., if $\forall
o\\!f\leq i<o\\!f+\textit{size}(t)~{}\exists e\in H_{zr}(o,o\\!f,t):~{}i\in
I(e)$, let $v:=0$. Otherwise, extend $V$ by a fresh value node $v$.

  4. 4.

Extend $H$ by the has-value edge
$o\raisebox{-1.29167pt}{$\xrightarrow{\smash{\raisebox{-0.43057pt}{$\scriptstyle
o\\!f,t$}}}$}v$ and return $(G,v)$ based on the obtained SMG $G$.

###  0.8.2 Write Reinterpretation of Nullified Blocks

Algorithm 2 gives the algorithm of write reinterpretation instantiated for
dealing with nullified blocks of memory as precisely as possible. An
illustration of how the algorithm works can be found in Fig. 12.

Figure 12: An illustration of write reinterpretation: (a) an initial SMG $G$,
(b) the SMG $G^{\prime}$ obtained by $\mathit{writeValue}(G,r,3,ptr,a_{1})$,
and (c) the SMG $G^{\prime\prime}$ obtained by
$\mathit{writeValue}(G^{\prime},r,7,ptr,a_{2})$. Note that $G^{\prime\prime}$
contains an undefined value in a field of size of 4 bytes at offset 3.
Algorithm 2 $\mathit{writeValue}(G,o,o\\!f,t,v)$

Input:

  * •

An SMG $G=(O,V,\Lambda,H,P)$.

  * •

An object $o\in O$.

  * •

A field $(o\\!f,t)$ within $o$, i.e.,
$o\\!f+\textit{size}(t)\leq\textit{size}(o)$.

  * •

A value $v$ such that $v\not\in O$ (needed so that $v$ can be safely added
into $V$).

Output:

  * •

An SMG $G^{\prime}$ that is the result of write reinterpretation of $G$ wrt
the object $o$, the field $(o\\!f,t)$, and the value $v$ such that as much
information on nullified memory as is allowed by the notion of SMGs is
preserved (i.e., each byte that is nullified in the input SMG will stay
nullified in the output SMG unless it is overwritten by a possibly non-zero
value).

Method:

  1. 1.

If $H(o,o\\!f,t)=v$, return $G$.

  2. 2.

Let $V:=V\cup\\{v\\}$.

  3. 3.

Remove from $H$ all edges leading from $o$ to non-zero values whose fields
overlap with the given field, i.e., the edges in $H_{ov}(o,o\\!f,t)\setminus
H_{zr}(o,o\\!f,t)$.

  4. 4.

If $v\neq 0$, then for each edge
$(e_{z}:o\raisebox{-1.29167pt}{$\xrightarrow{\smash{\raisebox{-0.43057pt}{$\scriptstyle
o\\!f_{z},t_{z}$}}}$}0)\in H_{zr}(o,o\\!f,t)$ do:

    1. (a)

Remove the edge $e_{z}$ from $H$.

    2. (b)

Let $o\\!f^{\prime}:=o\\!f+\textit{size}(t)$ and
$o\\!f^{\prime}_{z}:=o\\!f_{z}+\textit{size}(t_{z})$.

    3. (c)

If $o\\!f_{z}<o\\!f$, extend $H$ by the edge
$o\raisebox{-1.29167pt}{$\xrightarrow{\smash{\raisebox{-0.43057pt}{$\scriptstyle
o\\!f_{z},\mathtt{char[}o\\!f-o\\!f_{z}\mathtt{]}$}}}$}0$.

    4. (d)

If $o\\!f^{\prime}<o\\!f^{\prime}_{z}$, extend $H$ by the edge
$o\raisebox{-1.29167pt}{$\xrightarrow{\smash{\raisebox{-0.43057pt}{$\scriptstyle
o\\!f^{\prime},\mathtt{char[}o\\!f^{\prime}_{z}-o\\!f^{\prime}\mathtt{]}$}}}$}0$.

  5. 5.

Extend $H$ by the has-value edge
$o\raisebox{-1.29167pt}{$\xrightarrow{\smash{\raisebox{-0.43057pt}{$\scriptstyle
o\\!f,t$}}}$}v$ and return the obtained SMG.

##  0.9 The Join Algorithms

This appendix provides a detailed description of the join algorithms
introduced in Section 0.3.2. We first describe the $\mathit{joinSubSMGs}$
function, which implements the core functionality on top of which both joining
garbage-free SPCs (to reduce the number of SPCs obtained from different paths
through the program) as well as merging a pair of neighbouring objects of a
doubly-linked list into a single DLS within abstraction are built.
Subsequently, we describe the functions $\mathit{joinValues}$,
$\mathit{joinTargetObjects}$, and
$\mathit{insertLeftDlsAndJoin}\,/\,\mathit{insertRightDlsAndJoin}$ on which
$\mathit{joinSubSMGs}$ is based. In fact, $\mathit{joinSubSMGs}$ calls
$\mathit{joinValues}$ on pairs of corresponding values that appear below the
roots of the sub-SMGs to be joined, $\mathit{joinValues}$ then calls
$\mathit{joinTargetObjects}$ on pairs of objects that are the target of value
nodes representing addresses, and the $\mathit{joinTargetObjects}$ algorithm
recursively calls $\mathit{joinSubSMGs}$ to join the sub-SMGs of the objects
to be joined. The $\mathit{insertLeft}$($\mathit{Right}$)$\mathit{DlsAndJoin}$
functions are called from $\mathit{joinValues}$ when the given pair of
addresses cannot be joined since their target objects are incompatible, and an
attempt to save the join from failing is done by trying to compensate a DLS
missing in one of the SMGs by inserting it with the minimum length being 0
(which is possible since a 0+ DLS is a possibly empty list segment). Finally,
we describe the $\mathit{joinSPCs}$ and $\mathit{mergeSubSMGs}$ functions
implemented on top of the generic $\mathit{joinSubSMGs}$ function. The
$\mathit{joinSPCs}$ function joins garbage-free SPCs into a single SPC that
semantically covers both. The $\mathit{mergeSubSMGs}$ function merges a pair
of objects during abstraction into a single DLS while the non-shared part of
the sub-SMGs rooted at them is joined into the nested sub-SMG of the resulting
DLS.

$s_{1}\backslash s_{2}$ | $\simeq$ | $\sqsupset$ | $\sqsubset$ | $\Join$
---|---|---|---|---
$\simeq$ | $\simeq$ | $\sqsupset$ | $\sqsubset$ | $\Join$
$\sqsupset$ | $\sqsupset$ | $\sqsupset$ | $\Join$ | $\Join$
$\sqsubset$ | $\sqsubset$ | $\Join$ | $\sqsubset$ | $\Join$
$\Join$ | $\Join$ | $\Join$ | $\Join$ | $\Join$

As mentioned in Section 0.3.2, the join algorithm computes on the fly the so-
called _join status_ which compares the semantics of the SMGs being joined
(with the semantics being either equal, in an entailment relation, or
incomparable). For the purpose of maintaining the join status, the table shown
on the right defines the function
$\mathit{updateJoinStatus}:\mathbb{J}\times\mathbb{J}\longrightarrow\mathbb{J}$
that combines the current join status $s_{1}$, obtained from joining the so-
far explored parts of the SMGs being joined, with a status
$s_{2}\in\mathbb{J}$ comparing the semantics of the objects/values being
currently joined. Note that the function is monotone in that once the status,
which is initially $\simeq$, becomes $\sqsupset$ or $\sqsubset$, it can never
get back to $\simeq$, and once the status becomes $\Join$, it cannot change
any more.

In case of the $\mathit{joinSPCs}$ function, $\mathit{joinSubSMGs}$ needs to
be called multiple times for a single pair of SPCs (starting from different
program variables), and it is necessary to keep certain state information
between the calls. Besides the join status mentioned above, the algorithm
maintains a mapping of values and objects between the source SMGs and the
destination SMG. This is needed in order to identify potentially conflicting
mappings arising when starting the join from different program variables as
well as to identify parts of SMGs that have already been processed. The
mapping is encoded as a pair of partial injective functions
$m_{1}:(O_{1}\rightharpoonup O)\cup(V_{1}\rightharpoonup V)$ and
$m_{2}:(O_{2}\rightharpoonup O)\cup(V_{2}\rightharpoonup V)$. Additionally, we
assume that the $\\#$ object and the $0$ address, which have their pre-defined
unique roles in all SMGs, never appear in the ranges of $m_{1},m_{2}$. In case
of the $\mathit{mergeSubSMGs}$ function, the mapping of objects and values is
used to obtain the sets of nodes recognized as nested data structures.

In the following, we write $\textit{kind}_{1}$, $\textit{size}_{1}$,
$\textit{level}_{1}$, $\textit{len}_{1}$, $\textit{valid}_{1}$,
$\textit{nfo}_{1}$, $\textit{pfo}_{1}$, and $\textit{hfo}_{1}$ to denote kind,
size, level, len, valid, nfo, pfo, and hfo from $\Lambda_{1}$, i.e., the
labelling function of the first SMG being joined. Likewise for $\Lambda_{2}$.
We further define $\textit{len}^{\prime}$ as a wrapper function of len such
that $\textit{len}^{\prime}(o)=\textit{len}(o)$ if
$\textit{kind}(o)=\mathtt{dls}$, and $\textit{len}^{\prime}(o)=1$ if
$\textit{kind}(o)=\mathtt{reg}$.

###  0.9.1 Join Reinterpretation

The read and write reinterpretations described in Section 0.3.1 operate on a
single object of a single SMG. However, when joining a pair of SMGs, we need
to compare pairs of their objects, figure out what they have semantically in
common, and modify their sets of fields such that they become the same (even
if for the price of loosing some information), allowing one to subsequently
attempt to join their corresponding sub-SMGs. For that purpose, we introduce
_join reinterpretation_.

A join reinterpretation operator inputs a pair of SMGs $G_{1}$ and $G_{2}$,
whose sets of objects are $O_{1}$ and $O_{2}$, respectively, and a pair of
objects $o_{1}\in O_{1}$ and $o_{2}\in O_{2}$ such that
$\textit{size}_{1}(o_{1})=\textit{size}_{2}(o_{2})$. The operator returns a
triple $(s,G^{\prime}_{1},G^{\prime}_{2})$ where $s\in\mathbb{J}$ is a join
status, and $G_{1}^{\prime}$, $G_{2}^{\prime}$ are two SMGs with sets of has-
value edges $H^{\prime}_{1}$, $H^{\prime}_{2}$, respectively,

$s$ | semantics of $G^{\prime}_{1}$ | semantics of $G^{\prime}_{2}$
---|---|---
$\simeq$ | $\textit{MI}(G_{1})=\textit{MI}(G^{\prime}_{1})$ | $\textit{MI}(G_{2})=\textit{MI}(G^{\prime}_{2})$
$\sqsupset$ | $\textit{MI}(G_{1})=\textit{MI}(G^{\prime}_{1})$ | $\textit{MI}(G_{2})\subset\textit{MI}(G^{\prime}_{2})$
$\sqsubset$ | $\textit{MI}(G_{1})\subset\textit{MI}(G^{\prime}_{1})$ | $\textit{MI}(G_{2})=\textit{MI}(G^{\prime}_{2})$
$\Join$ | $\textit{MI}(G_{1})\subset\textit{MI}(G^{\prime}_{1})$ | $\textit{MI}(G_{2})\subset\textit{MI}(G^{\prime}_{2})$

such that: (1) The sets of fields of $o_{1}$ and $o_{2}$ are the same, i.e.,
$\forall o\\!f\in\mathbb{N}~{}\forall
t\in\mathbb{T}:~{}H^{\prime}_{1}(o_{1},o\\!f,t)\neq\bot\Leftrightarrow
H^{\prime}_{2}(o_{2},o\\!f,t)\neq\bot$. (2) The status $s$ and the semantics
of $G^{\prime}_{1}$ and $G^{\prime}_{2}$ are defined according to the table
shown on the right. Intuitively, the status $\sqsupset$ means that some
aspects of $G_{1}$ are less restrictive than those of $G_{2}$, implying a need
to lift these restrictions in $G_{2}$ to keep chance for its successful join
with $G_{1}$, which enlarges the semantics of $G_{2}$ while that of $G_{1}$
stays the same. Likewise for the other symbols of $\mathbb{J}$.

Algorithm 3 $joinFields(G_{1},G_{2},o_{1},o_{2})$

Input:

  * •

SMGs $G_{1}=(O_{1},V_{1},\Lambda_{1},H_{1},P_{1})$ and
$G_{2}=(O_{2},V_{2},\Lambda_{2},$ $H_{2},P_{2})$ with sets of addresses
$A_{1}$ and $A_{2}$, respectively.

  * •

Objects $o_{1}\in O_{1}$ and $o_{2}\in O_{2}$, s.t.
$\textit{size}_{1}(o_{1})=\textit{size}_{2}(o_{2})$.

Output:

  * •

A tuple $(s^{\prime},G_{1}^{\prime},G_{2}^{\prime})$ consisting of a join
status and two SMGs that is the result of join reinterpretation of $G_{1}$ and
$G_{2}$ wrt $o_{1}$ and $o_{2}$ which reorganizes the nullified fields of
$o_{1}$ and $o_{2}$ with the aim of obtaining the smallest possible number of
nullified fields such that either (a) each byte of such fields is nullified in
both $G_{1}$ and $G_{2}$, or (b) the field is nullified in one of them, and in
the other, it contains a non-null address.

Method:

  1. 1.

Let $H_{1}^{\prime}:=H_{1}$, $H_{2}^{\prime}:=H_{2}$.

  2. 2.

Process the set
$H_{1,0}=\\{o_{1}\raisebox{-1.29167pt}{$\xrightarrow{\smash{\raisebox{-0.43057pt}{$\scriptstyle
o\\!f,t$}}}$}0\in H_{1}^{\prime}\\}$ of edges leading from $o_{1}$ to $0$ in
$G_{1}$ as follows:

    1. (a)

Remove the edges that are in $H_{1,0}$ from $H_{1}^{\prime}$.

    2. (b)

Extend $H_{1}^{\prime}$ by the smallest set of edges $H^{\prime}_{1,0}$ in
which for each $0\leq i<\textit{size}_{1}(o_{1})$ there is an edge
$o_{1}\raisebox{-1.29167pt}{$\xrightarrow{\smash{\raisebox{-0.43057pt}{$\scriptstyle
o\\!f^{\prime},t^{\prime}$}}}$}0\in H^{\prime}_{1,0}$ such that $i\in
I(o\\!f^{\prime},t^{\prime})$ where $t^{\prime}=\mathtt{char[}n\mathtt{]}$ for
some $n>0$ iff
$\exists(o_{1}\raisebox{-1.29167pt}{$\xrightarrow{\smash{\raisebox{-0.43057pt}{$\scriptstyle
o\\!f_{1},t_{1}$}}}$}0)\in
H_{1,0}~{}\exists(o_{2}\raisebox{-1.29167pt}{$\xrightarrow{\smash{\raisebox{-0.43057pt}{$\scriptstyle
o\\!f_{2},t_{2}$}}}$}0)\in H_{2}^{\prime}:~{}i\in I(o\\!f_{1},t_{1})\cap
I(o\\!f_{2},t_{2})$.

    3. (c)

For each address $a_{2}\in A_{2}\setminus\\{0\\}$ and each edge
$(o_{2}\raisebox{-1.29167pt}{$\xrightarrow{\smash{\raisebox{-0.43057pt}{$\scriptstyle
o\\!f,\mathtt{ptr}$}}}$}a_{2})\in H_{2}^{\prime}$ for which there is no
$a_{1}\in A_{1}\setminus\\{0\\}$ such that
$(o_{1}\raisebox{-1.29167pt}{$\xrightarrow{\smash{\raisebox{-0.43057pt}{$\scriptstyle
o\\!f,\mathtt{ptr}$}}}$}a_{1})\in H_{1}^{\prime}$, but
$I(o\\!f,\mathtt{ptr})\subseteq\bigcup_{e\in H_{1,0}}I(e)$, extend
$H_{1}^{\prime}$ by the edge
$o_{1}\raisebox{-1.29167pt}{$\xrightarrow{\smash{\raisebox{-0.43057pt}{$\scriptstyle
o\\!f,\mathtt{ptr}$}}}$}0$.

Then do the same for $o_{2}$ with swapped sets of edges $H_{1}^{\prime}$ and
$H_{2}^{\prime}$, using $A_{1}$ instead of $A_{2}$, and $H_{2,0}$ and
$H^{\prime}_{2,0}$ instead of $H_{1,0}$ and $H^{\prime}_{1,0}$, respectively.

  3. 3.

Let $s:=\;\simeq$.

  4. 4.

For each $0\leq i<\textit{size}_{1}(o_{1})$:

     * •

If
$\exists(e:\;o_{1}\raisebox{-1.29167pt}{$\xrightarrow{\smash{\raisebox{-0.43057pt}{$\scriptstyle
o\\!f,t$}}}$}0)\in H_{1}$ such that $i\in I(e)$ and
$\forall(e^{\prime}:o_{1}\raisebox{-1.29167pt}{$\xrightarrow{\smash{\raisebox{-0.43057pt}{$\scriptstyle
o\\!f^{\prime},t^{\prime}$}}}$}0)\in H_{1}^{\prime}:i\notin I(e^{\prime})$,
let $s:=\mathit{updateJoinStatus}(s,\sqsubset)$.

     * •

If
$\exists(e:\;o_{2}\raisebox{-1.29167pt}{$\xrightarrow{\smash{\raisebox{-0.43057pt}{$\scriptstyle
o\\!f,t$}}}$}0)\in H_{2}$ such that $i\in I(e)$ and
$\forall(e^{\prime}:o_{2}\raisebox{-1.29167pt}{$\xrightarrow{\smash{\raisebox{-0.43057pt}{$\scriptstyle
o\\!f^{\prime},t^{\prime}$}}}$}0)\in H_{2}^{\prime}:i\notin I(e^{\prime})$,
let $s:=\mathit{updateJoinStatus}(s,\sqsupset)$.

  5. 5.

For all fields $(o\\!f,t)$ such that
$H_{1}^{\prime}(o_{1},o\\!f,t)\neq\bot~{}\wedge~{}H_{2}^{\prime}(o_{2},o\\!f,t)=\bot$,
extend $H_{2}^{\prime}$ such that $H_{2}^{\prime}(o_{2},o\\!f,t)=v$ for some
fresh $v$ added into $V_{2}$. Proceed likewise for non-nullified fields of
$o_{2}$ not defined in $o_{1}$.

  6. 6.

Return $(s,G_{1},G_{2})$ where
$G_{1}=(O_{1},V_{1},\Lambda_{1},H_{1}^{\prime},P_{1})$ and
$G_{2}=(O_{2},V_{2},\Lambda_{2},H_{2}^{\prime},P_{2})$.

For the particular case of dealing with nullified memory, we implement the
join reinterpretation as follows (cf. Algorithm 3). First, nullified fields
are shortened, split, and/or composed in each of the objects with the aim of
obtaining the smallest possible number of nullified fields such that either
(1) each byte of such fields is nullified in both original SMGs, or (2) the
field is nullified in one SMG, and, in the other, it contains a non-null
address. The former is motivated by preserving as much information about
nullified memory as possible when joining two objects. The latter is motivated
by the fact that a null pointer may be interpreted as a special case of a
null-terminated 0+ DLS and hence possibly joined with an address in the other
SMG if its target is a DLS. Finally, whenever a field $(o\\!f,t)$ remains
defined in $o_{1}$ but not in $o_{2}$ after the described transformations,
i.e., if $H_{1}(o_{1},o\\!f,t)\neq\bot$ and $H_{2}(o_{2},o\\!f,t)=\bot$,
$H_{2}$ is extended such that $H_{2}(o_{2},o\\!f,t)=v^{\prime}$ for some fresh
$v^{\prime}$ (and likewise the other way around). Note that the join status is
not updated since it will be updated later on when joining the appropriate
values.

###  0.9.2 Join of Sub-SMGs

The $\mathit{joinSubSMGs}$ function (cf. Alg. 4) is responsible for joining a
pair of sub-SMGs rooted at a given pair of objects and for constructing the
resulting sub-SMG within the given destination SMG. The function inputs a
triple of SMGs $G_{1}$, $G_{2}$, $G$ (two source SMGs and one destination SMG)
and a triple of equally-sized objects $o_{1}$, $o_{2}$, $o$ from the SMGs
$G_{1}$, $G_{2}$, $G$, respectively. If the $\mathit{joinSubSMGs}$ function
fails in joining the given sub-SMGs, it returns $\bot$. Otherwise, it returns
a triple of SMGs $G_{1}^{\prime}$, $G_{2}^{\prime}$, $G^{\prime}$ such that:

  * •

$\textit{MI}(G_{1})\subseteq\textit{MI}(G_{1}^{\prime})$ and
$\textit{MI}(G_{2})\subseteq\textit{MI}(G_{2}^{\prime})$ where $G_{1}$ and
$G_{2}$ can differ from $G^{\prime}_{1}$ and $G^{\prime}_{2}$, respectively,
due to an application of join reinterpretation on some of the pairs of objects
being joined only.

  * •

The sub-SMGs $G_{1}^{\prime\prime}$ and $G_{2}^{\prime\prime}$ of
$G_{1}^{\prime}$ and $G_{2}^{\prime}$ rooted at $o_{1}$ and $o_{2}$,
respectively, are joined into the sub-SMG $G^{\prime\prime}$ of $G^{\prime}$
rooted at $o$, i.e., it is required that
$\textit{MI}(G_{1}^{\prime\prime})\subseteq\textit{MI}(G^{\prime\prime})\supseteq\textit{MI}(G_{2}^{\prime\prime})$.

  * •

The sub-SMG $G^{\prime}\setminus G^{\prime\prime}$ is exactly the sub-SMG of
$G$ that consists of objects and values that are not removed in Step 10 of the
$\mathit{joinTargetObjects}$ function due to using the principle of delayed
join of sub-SMGs described in Section 0.9.6 (which will take care of the fact
that some sub-SMG may be reachable along some access path in one of the SMGs
$G_{1}$/$G_{2}$ only, due to some optional nested sub-heap missing in the
other SMG, in which, however, it may be reachable via some other access path
and may thus be discovered and joined later on).

The $\mathit{joinSubSMGs}$ function first applies the join reinterpretation
operator (denoted $joinFields$) on $G_{1}$, $G_{2}$ and $o_{1}$, $o_{2}$,
which ensures that the sets of fields of $o_{1}$ and $o_{2}$ are identical.
The function then iterates over the set of fields of these objects, and for
each field $(o\\!f,t)$ does the following:

  * •

finds the pair of values $v_{1}$ and $v_{2}$ which the has-value edges of
$o_{1}$ and $o_{2}$ labelled by $(o\\!f,t)$ lead to,

  * •

calls the $\mathit{joinValues}$ function for $v_{1}$ and $v_{2}$, which is
responsible for recursively joining the remaining parts of the sub-SMGs rooted
at them (before the call, the nesting level difference between $G_{1}$ and
$G_{2}$ is possibly updated as described below), and

  * •

extends the set of edges of $G$ by
$o\raisebox{-1.29167pt}{$\xrightarrow{\smash{\raisebox{-0.43057pt}{$\scriptstyle
o\\!f,t$}}}$}v$ where $v$ is the value returned by the $\mathit{joinValues}$
function.

#### Adjusting the Nesting Level Difference

In Section 0.3.2, it is said that the levels of the objects being joined can
differ since the objects may sometimes appear below a DLS and sometimes below
a region (and while an object that appears below a DLS may be considered
nested—provided that each node of the segment has a separate copy of such an
object—there is no notion of nesting below regions since for regions which
represent concrete objects there is no need to distinguish private and shared
sub-SMGs). The functionality of $\mathit{joinSubSMGs}$ therefore includes
tracking of the difference in levels (denoted $l_{diff}$) at which objects and
values to be joined within some sub-SMG can appear. When objects $o_{1}$ and
$o_{2}$ are being joined, the difference is computed as follows: If $o_{1}$ is
a DLS and $o_{2}$ is a region, the current value of $l_{diff}$ is increased by
one. Symmetrically, if $o_{1}$ is a region and $o_{2}$ is a DLS, the value of
$l_{diff}$ is decreased by one. Note that when going to sub-heaps in both
$G_{1}$ and $G_{2}$, the change of the difference is 0. The new difference is
then used when joining the values of the fields of $o_{1}$ and $o_{2}$ (apart
from the next and prev fields of course).

Algorithm 4 $\mathit{joinSubSMGs}$($s$, $G_{1}$, $G_{2}$, $G$, $m_{1}$,
$m_{2}$, $o_{1}$, $o_{2}$, $o$, $l_{diff}$)

Input:

  * •

Initial join status $s\in\mathbb{J}$.

  * •

SMGs $G_{1}=(O_{1},V_{1},\Lambda_{1},H_{1},P_{1})$,
$G_{2}=(O_{2},V_{2},\Lambda_{2},$ $H_{2},P_{2})$, and $G=(O,V,\Lambda,H,P)$.

  * •

Injective partial mappings of nodes $m_{1},m_{2}$ as defined in Section 0.9.

  * •

Objects $o_{1}\in O_{1}$, $o_{2}\in O_{2}$, $o\in O$.

  * •

Nesting level difference $l_{diff}\in\mathbb{Z}$.

Output:

  * •

$\bot$ in case the sub-SMGs of $G_{1}$ and $G_{2}$ rooted at $o_{1}$ and
$o_{2}$ cannot be joined.

  * •

Otherwise, a tuple
$(s^{\prime},G_{1}^{\prime},G_{2}^{\prime},G^{\prime},m_{1}^{\prime},m_{2}^{\prime})$
where:

    * –

$s^{\prime}\in\mathbb{J}$ is the resulting join status.

    * –

$G_{1}^{\prime},G_{2}^{\prime},G^{\prime}$ are SMGs as defined in Section
0.9.2.

    * –

$m_{1}^{\prime}$, $m_{2}^{\prime}$ are the resulting injective partial
mappings of nodes.

Method:

  1. 1.

Let $res:=joinFields(G_{1},G_{2},o_{1},o_{2})$. If $res=\bot$, return $\bot$.
Otherwise let
$(s^{\prime},G_{1},G_{2}):=res$ and
$s:=\mathit{updateJoinStatus}(s,s^{\prime})$.

  2. 2.

Collect the set $F$ of all pairs $(o\\!f,t)$ occurring in has-value edges
leading from $o_{1}$ or $o_{2}$.

  3. 3.

For each field $(o\\!f,t)\in F$ do:

     * •

Let $v_{1}=H_{1}(o_{1},o\\!f,t)$, $v_{2}=H_{2}(o_{2},o\\!f,t)$, and
$l_{diff}^{\prime}:=l_{diff}$.

     * •

If $\textit{kind}_{1}(o_{1})=\mathtt{dls}$ and $(o\\!f,t)$ is not the
next/prev field of $o_{1}$, let $l_{diff}^{\prime}:=l_{diff}^{\prime}+1$.

     * •

If $\textit{kind}_{2}(o_{2})=\mathtt{dls}$ and $(o\\!f,t)$ is not the
next/prev field of $o_{2}$, let $l_{diff}^{\prime}:=l_{diff}^{\prime}-1$.

     * •

Let
$res:=\mathit{joinValues}(s,G_{1},G_{2},G,m_{1},m_{2},v_{1},v_{2},l_{diff}^{\prime})$.
If $res=\bot$, return $\bot$. Otherwise, let
$(s,G_{1},G_{2},G,m_{1},m_{2},v):=res$.

     * •

Introduce a new has-value edge
$o\raisebox{-1.29167pt}{$\xrightarrow{\smash{\raisebox{-0.43057pt}{$\scriptstyle
o\\!f,t$}}}$}v$ in $H$.

  4. 4.

Return $(s,G_{1},G_{2},G,m_{1},m_{2})$.

###  0.9.3 Join of Values

The $\mathit{joinValues}$ function (cf. Alg. 5) joins a pair of sub-SMGs
rooted at a given pair of values and returns a single value node that
represents both the input values in the destination SMG. The function inputs a
triple of SMGs $G_{1}$, $G_{2}$, $G$ (two source SMGs and one destination SMG)
and a pair of values $v_{1}$ and $v_{2}$ from $G_{1}$ and $G_{2}$,
respectively. If the function fails in joining the given values, it returns
$\bot$. Otherwise, it returns a triple of SMGs $G_{1}^{\prime}$,
$G_{2}^{\prime}$, $G^{\prime}$, and a value $v$ from $G^{\prime}$ such that:

  * •

$\textit{MI}(G_{1})\subseteq\textit{MI}(G_{1}^{\prime})$ and
$\textit{MI}(G_{2})\subseteq\textit{MI}(G_{2}^{\prime})$ where $G_{1}$ and
$G_{2}$ can differ from $G^{\prime}_{1}$ and $G^{\prime}_{2}$, respectively,
due to an application of join reinterpretation on some of the pairs of objects
being joined only.

  * •

The sub-SMGs $G_{1}^{\prime\prime}$ and $G_{2}^{\prime\prime}$ of
$G_{1}^{\prime}$ and $G_{2}^{\prime}$ rooted at $v_{1}$ and $v_{2}$,
respectively, are joined into the sub-SMG $G^{\prime\prime}$ of $G^{\prime}$
rooted at $v$, i.e., it is required that
$\textit{MI}(G_{1}^{\prime\prime})\subseteq\textit{MI}(G^{\prime\prime})\supseteq\textit{MI}(G_{2}^{\prime\prime})$.

  * •

The sub-SMG $G^{\prime}\setminus G^{\prime\prime}$ is exactly the sub-SMG of
$G$ that consists of objects and values that are not removed in Step 10 of the
$\mathit{joinTargetObjects}$ function due to using the principle of delayed
join of sub-SMGs described in Section 0.9.6.

Algorithm 5 $\mathit{joinValues}$($s$, $G_{1}$, $G_{2}$, $G$, $m_{1}$,
$m_{2}$, $v_{1}$, $v_{2}$, $l_{diff}$)

Input:

  * •

Initial join status $s\in\mathbb{J}$.

  * •

SMGs $G_{1}=(O_{1},V_{1},\Lambda_{1},H_{1},P_{1})$,
$G_{2}=(O_{2},V_{2},\Lambda_{2},H_{2},P_{2})$, and $G=(O,V,\Lambda,H,P)$.

  * •

Injective partial mappings of nodes $m_{1},m_{2}$ as defined in Section 0.9.

  * •

Values $v_{1}\in V_{1}$ and $v_{2}\in V_{2}$.

  * •

Nesting level difference $l_{diff}\in\mathbb{Z}$.

Output:

  * •

$\bot$ in case the sub-SMGs of $G_{1}$ and $G_{2}$ rooted at $v_{1}$ and
$v_{2}$ cannot be joined.

  * •

Otherwise, a tuple
$(s^{\prime},G_{1}^{\prime},G_{2}^{\prime},G^{\prime},m_{1}^{\prime},m_{2}^{\prime},v^{\prime})$
where:

    * –

$s^{\prime}\in\mathbb{J}$ is the resulting join status.

    * –

$G_{1}^{\prime},G_{2}^{\prime},G^{\prime}$ are SMGs as defined in Section
0.9.3.

    * –

$m_{1}^{\prime}$, $m_{2}^{\prime}$ are the resulting injective partial
mappings of nodes.

    * –

$v^{\prime}$ is a value in $G^{\prime}$ satisfying the conditions stated in
Section 0.9.3.

Method:

  1. 1.

If $v_{1}=v_{2}$, return $(s,G_{1},G_{2},G,m_{1},m_{2},v_{1})$. In this case,
the given pair of values matches trivially, which happens whenever a shared
value is reached during abstraction.

  2. 2.

If $m_{1}(v_{1})=m_{2}(v_{2})=v\neq\bot$, return
$(s,G_{1},G_{2},G,m_{1},m_{2},v)$. In this case, the pair of values is already
joined.

  3. 3.

If both $v_{1}$ and $v_{2}$ are non-address values, i.e., $P_{1}(v_{1})=\bot$
and $P_{2}(v_{2})=\bot$, then:

     * •

If $m_{1}(v_{1})\neq\bot$ or $m_{2}(v_{2})\neq\bot$, return $\bot$.

     * •

Create a new value node $v\in V$ such that
$\textit{level}(v)=max(\textit{level}_{1}(v_{1}),\textit{level}_{2}(v_{2}))$.

     * •

Extend the mapping of nodes such that $m_{1}(v_{1})=m_{2}(v_{2})=v$.

     * •

If $\textit{level}_{1}(v_{1})-\textit{level}_{2}(v_{2})<l_{diff}$, let
$s:=\mathit{updateJoinStatus}(s,\sqsubset)$.

     * •

If $\textit{level}_{1}(v_{1})-\textit{level}_{2}(v_{2})>l_{diff}$, let
$s:=\mathit{updateJoinStatus}(s,\sqsupset)$.

     * •

Return $(s,G_{1},G_{2},G,m_{1},m_{2},v_{1})$.

  4. 4.

If $P_{1}(v_{1})=\bot$ or $P_{2}(v_{2})=\bot$, return $\bot$.

  5. 5.

Let
$res:=\mathit{joinTargetObjects}(s,G_{1},G_{2},G,m_{1},m_{2},v_{1},v_{2},l_{diff})$.
If $res=\bot$, return $\bot$. If $res\neq\;\hookleftarrow$, then return $res$.

  6. 6.

Let $o_{1}:=o(P_{1}(v_{1}))$ and $o_{2}:=o(P_{2}(v_{2}))$.

  7. 7.

If $\textit{kind}_{1}(o_{1})=\mathtt{dls}$, let
$res=\mathit{insertLeftDlsAndJoin}(s,G_{1},G_{2},G,m_{1},m_{2},v_{1},v_{2},l_{diff})$.
If $res=\bot$, return $\bot$. If $res\neq\;\hookleftarrow$, then return $res$.

  8. 8.

If $\textit{kind}_{2}(o_{2})=\mathtt{dls}$, let
$res=\mathit{insertRightDlsAndJoin}(s,G_{1},G_{2},G,m_{1},m_{2},v_{1},v_{2},l_{diff})$.
If $res\in\\{\bot,\hookleftarrow\\}$, return $\bot$. Otherwise, return $res$.

If the input values are identical ($v_{1}=v_{2}$), the resulting value $v$ is
the same identical value, say $v_{1}$, which prevents shared nodes from being
processed as nested data structures during abstraction. If both values are
mapped to the same value node in the destination SMG, i.e.,
$m_{1}(v_{1})=m_{2}(v_{2})$, the node $m_{1}(v_{1})$ (or, equivalently,
$m_{2}(v_{2})$) to which they are mapped is returned since such a pair of
values has already been successfully joined before. A pair of non-address
values visited for the first time, i.e., a pair of values for which
$m_{1}(v_{1})=\bot=m_{2}(v_{2})$, is joined by creating a fresh value node $v$
in $G^{\prime}$ with the appropriate nesting level262626In case the difference
of $\textit{level}_{1}(v_{1})$ and $\textit{level}_{2}(v_{2})$ differs from
$l_{diff}$, the join status is appropriately updated. This reflects the fact
that, e.g., a single unknown (or interval) abstract value that is used as the
value of multiple fields of some region (for instance, an array) that is more
nested than the region may concretise to _different_ concrete values for each
of the fields while it must concretise to the _same_ concrete value if the
abstract value is on the same level as the given region., and the mapping of
nodes is extended such that $m_{1}(v_{1})=m_{2}(v_{2})=v$. Non-address values
are never joined with addresses—if such a situation occurs, the whole join
operation fails.272727Note that the handling of non-address values is kept
simple since the basic notion of SMGs does not distinguish any special kinds
of non-address values (numbers, intervals, etc.), but there is still room for
improvement, especially in conjunction with the extensions described in
Section 0.4. For addresses seen for the first time, the algorithm tries to
join their targets with each other with three possible outcomes:

  1. 1.

The join succeeds, and $\mathit{joinValues}$ then succeeds too.

  2. 2.

The join fails in a recoverable way (denoted by the result being
$\hookleftarrow$). Intuitively, this happens when trying to join addresses
that are found to be obviously different, i.e., addresses that are found to be
different without going deeper into the sub-SMGs rooted at them—e.g., due to
they point to some object with different offsets, different target specifiers,
incompatible levels, size, validity, linking fields (for DLSs), or when the
objects they point to are already mapped to some other objects. In case of the
recoverable failure, if at least one of the target objects is a DLS, the
algorithm tries to virtually _insert a DLS_ in one of the SMGs, which allows
it to create a $0+$ DLS in the destination SMG and continue by joining the
appropriate successor values. If this fails too, the whole join operation
fails.282828As mentioned already in Section 0.3.2, the recovery could be tried
even when the impossibility of joining two addresses is discovered much later
during joining the sub-SMGs rooted at the given addresses. Then, however,
back-tracking would be necessary, which we try to avoid for efficiency
reasons.

  3. 3.

The join fails in an irrecoverable way (denoted by the result being $\bot$) in
which case $\mathit{joinValues}$ fails too.

###  0.9.4 Join of Target Objects

Algorithm 6 $\mathit{joinTargetObjects}$($s$, $G_{1}$, $G_{2}$, $G$, $m_{1}$,
$m_{2}$, $a_{1}$, $a_{2}$, $l_{diff}$)

Input:

  * •

Initial join status $s\in\mathbb{J}$.

  * •

SMGs $G_{1}=(O_{1},V_{1},\Lambda_{1},H_{1},P_{1})$,
$G_{2}=(O_{2},V_{2},\Lambda_{2},H_{2},P_{2})$, and $G=(O,V,\Lambda,H,P)$.

  * •

Injective partial mappings of nodes $m_{1},m_{2}$ as defined in Section 0.9.

  * •

Addresses $a_{1}\in V_{1}$ and $a_{2}\in V_{2}$.

  * •

Nesting level difference $l_{diff}\in\mathbb{Z}$.

Output:

  * •

$\bot$ in case of an irrecoverable failure.

  * •

$\hookleftarrow$ in case of a recoverable failure.

  * •

Otherwise, a tuple
$(s^{\prime},G_{1}^{\prime},G_{2}^{\prime},G^{\prime},m_{1}^{\prime},m_{2}^{\prime},a^{\prime})$
where:

    * –

$s^{\prime}\in\mathbb{J}$ is the resulting join status.

    * –

$G_{1}^{\prime},G_{2}^{\prime},G^{\prime}$ are SMGs as defined in Section
0.9.4.

    * –

$m_{1}^{\prime}$, $m_{2}^{\prime}$ are the resulting injective partial
mappings of nodes.

    * –

$a^{\prime}$ is an address in $G^{\prime}$ satisfying the conditions stated in
Section 0.9.4.

Method:

  1. 1.

If $o\\!f(P_{1}(a_{1}))\neq o\\!f(P_{2}(a_{2}))$ or
$\textit{level}_{1}(a_{1})-\textit{level}_{2}(a_{2})\neq l_{diff}$, return
$\hookleftarrow$.

  2. 2.

Let $o_{1}:=o(P_{1}(a_{1}))$ and $o_{2}:=o(P_{2}(a_{2}))$.

  3. 3.

If $\textit{kind}_{1}(o_{1})=\textit{kind}_{2}(o_{2})$ and
$\textit{tg}(P_{1}(a_{1}))\neq\textit{tg}(P_{2}(a_{2}))$, return
$\hookleftarrow$.

  4. 4.

If $o_{1}=\\#=o_{2}$ or $m_{1}(o_{1})=m_{2}(o_{2})\neq\bot$,
let
$(G,m_{1},m_{2},a):=mapTargetAddress(G_{1},G_{2},G,m_{1},m_{2},a_{1},a_{2})$
and return $(s,G_{1},G_{2},G,m_{1},m_{2},a)$. In this case, the targets are
already joined, and we need to create a new address for the corresponding
object $o\in O$.

  5. 5.

Let $s:=matchObjects(s,G_{1},G_{2},m_{1},m_{2},o_{1},o_{2})$. If $s=\bot$,
return $\hookleftarrow$.

  6. 6.

Create a new object $o\in O$.

  7. 7.

Initialize the labelling of $o$ to match the labelling of $o_{1}$ if
$\textit{kind}_{1}(o_{1})=\mathtt{dls}$, or to match the labelling of $o_{2}$
if $\textit{kind}_{2}(o_{2})=\mathtt{dls}$, otherwise take the labelling from
any of them since both $o_{1}$ and $o_{2}$ are equally labelled regions.

  8. 8.

If $\textit{kind}_{1}(o_{1})=\mathtt{dls}$ or
$\textit{kind}_{2}(o_{2})=\mathtt{dls}$, let
$\textit{len}(o):=min(\textit{len}_{1}(o_{1}),\textit{len}_{2}(o_{2}))$.

  9. 9.

Let
$\textit{level}(o):=max(\textit{level}_{1}(o_{1}),\textit{level}_{2}(o_{2}))$.

  10. 10.

If $m_{1}(o_{1})\neq\bot$, replace each edge leading to $m_{1}(o_{1})$ by an
equally labelled edge leading to $o$, remove $m_{1}(o_{1})$ together with all
nodes and edges of $G$ that are reachable via $m_{1}(o_{1})$ only, and remove
the items of $m_{1}$ whose target nodes were removed. Likewise for $m_{2}$ and
$o_{2}$. Note that this mechanism is called a _delayed join of sub-SMGs_ and
explained in Section 0.9.6.

  11. 11.

Extend the mapping of nodes such that $m_{1}(o_{1})=m_{2}(o_{2})=o$.

  12. 12.

Let
$(G,m_{1},m_{2},a):=mapTargetAddress(G_{1},G_{2},G,m_{1},m_{2},a_{1},a_{2})$.

  13. 13.

Let
$res:=\mathit{joinSubSMGs}(s,G_{1},G_{2},G,m_{1},m_{2},o_{1},o_{2},o,l_{diff})$.
If $res=\bot$, return $\bot$. Otherwise return
$(s,G_{1},G_{2},G,m_{1},m_{2},a)$.

The $\mathit{joinTargetObjects}$ function (cf. Alg. 6) joins a pair of sub-
SMGs rooted at the given pair of addresses and returns a single address node
that represents both the input addresses in the destination SMG. The function
inputs a triple of SMGs $G_{1}$, $G_{2}$, $G$ (two source SMGs and one
destination SMG) and a pair of addresses $a_{1}$ and $a_{2}$ from $G_{1}$ and
$G_{2}$, respectively. If the function fails in joining the given addresses,
it returns $\bot$ in case of an irrecoverable failure and $\hookleftarrow$ in
case of a recoverable failure (intuitively, for efficiency reasons, this
happens when the offsets, target specifiers, nesting levels, the kinds of the
target objects, their sizes, or validity are found incompatible without going
deeper in the sub-SMGs rooted at the given addresses). If the function
succeeds, it returns a triple of SMGs $G_{1}^{\prime}$, $G_{2}^{\prime}$,
$G^{\prime}$ and an address $a$ from $G^{\prime}$ such that:

  * •

$\textit{MI}(G_{1})\subseteq\textit{MI}(G_{1}^{\prime})$ and
$\textit{MI}(G_{2})\subseteq\textit{MI}(G_{2}^{\prime})$ where $G_{1}$ and
$G_{2}$ can differ from $G^{\prime}_{1}$ and $G^{\prime}_{2}$, respectively,
due to an application of join reinterpretation on some of the pairs of objects
being joined only.

  * •

The sub-SMGs $G_{1}^{\prime\prime}$ and $G_{2}^{\prime\prime}$ of
$G_{1}^{\prime}$ and $G_{2}^{\prime}$ rooted at $a_{1}$ and $a_{2}$,
respectively, are joined as the sub-SMG $G^{\prime\prime}$ of $G^{\prime}$
rooted at $a$, i.e., it is required that
$\textit{MI}(G_{1}^{\prime\prime})\subseteq\textit{MI}(G^{\prime\prime})\supseteq\textit{MI}(G_{2}^{\prime\prime})$.

  * •

The sub-SMG $G^{\prime}\setminus G^{\prime\prime}$ is exactly the sub-SMG of
$G$ that consists of objects and values that are not removed in Step 10 of the
function due to using the principle of delayed join of sub-SMGs described in
Section 0.9.6.

The algorithm first checks compatibility of the offsets that the points-to
edges leading from $a_{1}$ and $a_{2}$ are labelled with and checks whether
the difference in the nesting depth is appropriate. Then, provided that the
target objects $o_{1}=o(P_{1}(a_{1}))$ and $o_{2}=o(P_{2}(a_{2}))$ are of the
same kind, the algorithm checks whether they are reached via the same target
specifiers (when one is a DLS and one a region, the specifiers may differ
since the target specifier is not important for the region). If these tests do
not pass, the algorithm fails in a recoverable way.

Next, if both $o_{1}$ and $o_{2}$ are null or if they have already been joined
with each other (and they are now reached through a different pair of
addresses only), the function $mapTargetAddress$ (cf. Alg. 7) is used to join
the addresses $a_{1}$ and $a_{2}$ into a fresh address $a\in A$ (so that
$m_{1}(a_{1})=m_{2}(a_{2})=a$) and to create a points-to edge from $a$ to the
join of $o_{1}$ and $o_{2}$, i.e., the object $m_{1}(o_{1})=m_{2}(o_{2})$. If
the objects $o_{1}$ and $o_{2}$ have not been joined so far, the algorithm
checks through the $matchObjects$ function (Alg. 8 discussed below) whether
$o_{1}$ and $o_{2}$ can be safely joined (based on their labels, labels of
their outgoing edges, and the state of their mapping so far). If so, a fresh
object $o$ in $G$ is created that is intended to semantically cover both
$o_{1}$ and $o_{2}$.

We allow DLSs to be joined with regions as well as with DLSs of a different
minimal length, which requires the minimal length of the object $o$ to be
adjusted so that it covers both cases, i.e.,
$\textit{len}(o):=min(\textit{len}_{1}(o_{1}),\textit{len}_{2}(o_{2}))$. The
nesting level must also be properly chosen: the larger value is chosen since a
path through more DLSs is more abstract and hence more general (covering the
more concrete path through less DLSs).

Line 10 now solves the case when exactly one of the mappings $m_{1}(o_{1})$ or
$m_{2}(o_{2})$ is already defined—the situation when both of them are already
defined is handled on line 4 and in function $matchObjects$. This case can
occur as a consequence of the DLS insertion algorithm described in Section
0.9.5, and it is further discussed in Section 0.9.6. For now, it is enough to
note that line 10 eliminates the impact of the DLS insertion algorithm on
$o_{1}$ or $o_{2}$ (depending on which of them was mapped within the DLS
insertion) as well as on their sub-SMGs, so that they can subsequently be
merged as though both of them were encountered for the first time.

Next, the mapping of nodes is extended such that
$m_{1}(o_{1})=m_{2}(o_{2})=o$, followed by using the function
$mapTargetAddress$ to map the addresses $a_{1}$ and $a_{2}$ to a new address
$a\in A$ and to create a points-to edge from $a$ to $o$ (as we have already
seen above). Finally, the $\mathit{joinSubSMGs}$ function is called
recursively for the triple $o_{1},o_{2},o$.

While we believe that Alg. 7 is self-explaining, we provide some more
intuition to Alg. 8 that performs a local check whether objects $o_{1}$,
$o_{2}$ from SMGs $G_{1}$ and $G_{2}$, can be joined under the current
mappings $m_{1}$ and $m_{2}$, respectively, possibly for the price of updating
the current joint status $s$. The algorithm assumes that at least one of the
objects is non-null (the case of both them being null is handled in Alg. 6).
Under this assumption, if one of the objects is null, the algorithm fails
since null can be joined with null only.

The algorithm also fails if both $o_{1}$ and $o_{2}$ are mapped but not to
each other. Next, even if $o_{2}$ is not mapped, but $o_{1}$ is mapped to some
other object $o^{\prime}_{2}\in O_{2}\setminus\\{o_{2}\\}$, a failure happens
(and symmetrically with the roles of $o_{1}$ and $o_{2}$ swapped). The reason
for the failures based on the mappings is that at most two objects can be
mapped together. The only case when the join can succeed with one of the
objects mapped is when the other is not mapped—this scenario is a consequence
of the further discussed DLS insertion and will be handled by cancelling the
mapping of the object that has already been mapped and by mapping $o_{1}$ and
$o_{2}$ to each other.

Subsequently, the algorithm checks whether the sizes of $o_{1}$ and $o_{2}$
are equal and whether they have the same validity status. In case the objects
are DLSs, their defining offsets are checked for equality too. Then, the
algorithm checks for all fields that appear in both objects and whose values
are already mapped whether their values are mapped to each other. If some of
the tests does not pass, the algorithm fails.

Finally, the algorithm checks whether the lengths of the objects or their
kinds imply a need to update the join status (joining a more concrete object
with a more abstract one). If so, the join status is updated accordingly.

Algorithm 7 $mapTargetAddress$($G_{1}$, $G_{2}$, $G$, $m_{1}$, $m_{2}$,
$a_{1}$, $a_{2}$)

Input:

  * •

SMGs $G_{1}=(O_{1},V_{1},\Lambda_{1},H_{1},P_{1})$,
$G_{2}=(O_{2},V_{2},\Lambda_{2},H_{2},P_{2})$, and $G=(O,V,\Lambda,H,P)$ with
the corresponding sets of addresses $A_{1},A_{2},A$.

  * •

Injective partial mappings of nodes $m_{1},m_{2}$ as defined in Section 0.9.

  * •

Addresses $a_{1}\in A_{1}$, $a_{2}\in A_{2}$ referring with the same offset
$o\\!f=o\\!f(P_{1}(a_{1}))=o\\!f(P_{2}(a_{2}))$ to objects
$o_{1}=o(P_{1}(a_{1}))$, $o_{2}=o(P_{2}(a_{2}))$, respectively, which are
already joined into an object $o=m_{1}(o_{1})=m_{2}(o_{2})$ and which are
accessible via target specifiers such that
$\textit{kind}_{1}(o_{1})=\textit{kind}_{2}(o_{2})\Rightarrow\textit{tg}(P_{1}(a_{1}))=\textit{tg}(P_{2}(a_{2}))$.

Output:

  * •

A tuple $(G^{\prime},m_{1}^{\prime},m_{2}^{\prime},a)$ where:

    * –

$G^{\prime}$ is an SMG obtained from $G$ by extending its set of addresses by
an address $a$ representing the join of $a_{1}$ and $a_{2}$ (unless $G$
already contains this address) together with a points-to edge from $a$ to $o$
representing the join of the points-to edges between $a_{1}$, $a_{2}$ and
$o_{1}$, $o_{2}$, respectively.

    * –

$m_{1}^{\prime}$ and $m_{2}^{\prime}$ are the resulting injective partial
mappings of nodes that are either identical to $m_{1}$ and $m_{2}$ (if $a$
already exists in $G$) or obtained from $m_{1}$ and $m_{2}$ by extending them
such that $m_{1}^{\prime}(a_{1})=m_{2}^{\prime}(a_{2})=a$.

Method:

  1. 1.

Let $o_{1}:=o(P_{1}(a_{1}))$, $o\\!f:=o\\!f(P_{1}(a_{1}))$.

  2. 2.

If $o_{1}=\\#$, let $o:=\\#$. Otherwise, let $o:=m_{1}(o_{1})$.

  3. 3.

If $\textit{kind}_{1}(o_{1})=\mathtt{dls}$, let
$\textit{tg}:=\textit{tg}(P_{1}(a_{1}))$. Otherwise, let
$\textit{tg}:=\textit{tg}(P_{2}(a_{2}))$.

  4. 4.

If there is an address $a\in A$ such that $P(a)=(o\\!f,\textit{tg},o)$, return
$(G,m_{1},m_{2},a)$.

  5. 5.

Extend $A$ by a fresh address $a$, then extend $P$ by a new points-to edge
$a\raisebox{-1.29167pt}{$\xrightarrow{\smash{\raisebox{-0.43057pt}{$\scriptstyle
o\\!f,\textit{tg}$}}}$}o$.

  6. 6.

Extend the mapping of nodes such that $m_{1}(a_{1})=m_{2}(a_{2})=a$.

  7. 7.

Return $(G,m_{1},m_{2},a)$.

Algorithm 8 $matchObjects$($s$, $G_{1}$, $G_{2}$, $m_{1}$, $m_{2}$, $o_{1}$,
$o_{2}$)

Input:

  * •

Initial join status $s\in\mathbb{J}$.

  * •

SMGs $G_{1}=(O_{1},V_{1},\Lambda_{1},H_{1},P_{1})$ and
$G_{2}=(O_{2},V_{2},\Lambda_{2},H_{2},P_{2})$.

  * •

Injective partial mappings of nodes $m_{1},m_{2}$ as defined in Section 0.9.

  * •

Objects $o_{1}\in O_{1}$ and $o_{2}\in O_{2}$ such that $o_{1}\neq\\#\vee
o_{2}\neq\\#$.

Output:

  * •

$\bot$ in case $o_{1}$ and $o_{2}$ cannot be joined.

  * •

Otherwise, $s\in\mathbb{J}$ reflecting the impact of the labels of $o_{1}$ and
$o_{2}$ on the relation of the semantics of $G_{1}$ and $G_{2}$.

Method:

  1. 1.

If $o_{1}=\\#$ or $o_{2}=\\#$, return $\bot$.

  2. 2.

If $m_{1}(o_{1})\neq\bot\neq m_{2}(o_{2})$ and $m_{1}(o_{1})\neq
m_{2}(o_{2})$, return $\bot$.

  3. 3.

If $m_{1}(o_{1})\neq\bot$ and $\exists o_{2}^{\prime}\in
O_{2}:\;m_{1}(o_{1})=m_{2}(o_{2}^{\prime})$, return $\bot$.

  4. 4.

If $m_{2}(o_{2})\neq\bot$ and $\exists o_{1}^{\prime}\in
O_{1}:\;m_{1}(o_{1}^{\prime})=m_{2}(o_{2})$, return $\bot$.

  5. 5.

If $\textit{size}_{1}(o_{1})\neq\textit{size}_{2}(o_{2})$ or
$\textit{valid}_{1}(o_{1})\neq\textit{valid}_{2}(o_{2})$, return $\bot$.

  6. 6.

If $\textit{kind}_{1}(o_{1})=\textit{kind}_{2}(o_{2})=\mathtt{dls}$, then:

     * •

If $\textit{nfo}_{1}(o_{1})\neq\textit{nfo}_{2}(o_{2})$,
$\textit{pfo}_{1}(o_{1})\neq\textit{pfo}_{2}(o_{2})$, or
$\textit{hfo}_{1}(o_{1})\neq\textit{hfo}_{2}(o_{2})$, return $\bot$.

  7. 7.

Collect the set $F$ of all pairs $(o\\!f,t)$ occurring in has-value edges
leading from $o_{1}$ or $o_{2}$.

  8. 8.

For each field $(o\\!f,t)\in F$ do:

     * •

Let $v_{1}=H_{1}(o_{1},o\\!f,t)$ and $v_{2}=H_{2}(o_{2},o\\!f,t)$.

     * •

If $v_{1}\neq\bot\neq v_{2}$ and $m_{1}(v_{1})\neq\bot\neq m_{2}(v_{2})$ and
$m_{1}(v_{1})\neq m_{2}(v_{2})$, return $\bot$.

  9. 9.

If $\textit{len}_{1}^{\prime}(o_{1})<\textit{len}_{2}^{\prime}(o_{2})\;\;$ or
$\;\;\textit{kind}_{1}(o_{1})=\mathtt{dls}\;\wedge\;\textit{kind}_{2}(o_{2})=\mathtt{reg}$,
let $s:=\mathit{updateJoinStatus}(s,\sqsupset)$.

  10. 10.

If $\textit{len}_{1}^{\prime}(o_{1})>\textit{len}_{2}^{\prime}(o_{2})\;\;$ or
$\;\;\textit{kind}_{1}(o_{1})=\mathtt{reg}\;\wedge\;\textit{kind}_{2}(o_{2})=\mathtt{dls}$,
let $s:=\mathit{updateJoinStatus}(s,\sqsubset)$.

  11. 11.

Return $s$.

###  0.9.5 DLS Insertion

Assume that a pair of addresses $a_{1}$ and $a_{2}$ from SMGs $G_{1}$ and
$G_{2}$ is to be joined in order to allow $G_{1}$ and $G_{2}$ to be joined
into an SMG $G$. Further, assume that the objects that the addresses refer to
cannot be joined, but at least one of them is a DLS—in particular, assume that
it is the object with the address $a_{1}$, denote it $d_{1}$, and denote the
other object $o_{2}$ (the other possibility being symmetric). As mentioned
already at the beginning of Section 0.9, in such a case, we proceed as though
$a_{2}$ pointed to a $0+$ DLS $d_{2}$ preceding $o_{2}$ and labelled equally
as $d_{1}$ up to its length. We then join $d_{1}$ and $d_{2}$ into a single 0+
DLS $d$ in $G$ and continue by joining the addresses $a_{next}$ and $a_{2}$
where $a_{next}$ is the value stored in the next/prev pointer of $d_{1}$
(depending on whether we came to $d_{1}$ via the $\mathtt{fst}$ or
$\mathtt{lst}$ target specifier, respectively). We call this mechanism a _DLS
insertion_ because it can be seen as if the join of objects was preceded by a
virtual insertion of a DLS from one of the SMGs into the other SMG. This
extension is possible since the semantics of a 0+ DLS includes the empty list,
which can be safely assumed to appear anywhere, compensating a missing object
in one of the SMGs.

Algorithm 9 implements the DLS insertion. The algorithm first checks whether
the DLS $d_{1}$ from $G_{1}$ that we would like to virtually insert into
$G_{2}$ has not been processed by the join algorithm already in the past. If
this is the case and there is some object $o$ in $G_{2}$ that has been joined
with $d_{1}$ into $d$, the join fails since the $d_{2}$ segment (possibly
represented by a region as its concrete instance) is not missing, but it is
not connected to the rest of the SMG in a way compatible with $d_{1}$ (at
least not for the current way $G_{1}$ and $G_{2}$ are being joined). If no
such object $o$ exists, the DLS $d$ to which $d_{1}$ is mapped in $G$ is used
as the result of joining $d_{1}$ with the virtually added segment $d_{2}$, and
unless even the address $a_{1}$ has already been processed, the join continues
by the addresses $a_{next}$ and $a_{2}$. Intuitively, this case arises when
inserting a single missing segment that should be reachable through several
paths in the SMG. Note that such a situation is, in fact, quite usual since a
DLS can be reached both forward and backward. The algorithm, however, has to
insert a single virtual segment $d_{2}$ for all such paths.

If $d_{1}$ has not yet been processed, the algorithm checks whether there is
some hope that the virtual insertion of $d_{2}$ could help (or whether it is
better to try to proceed with the join in some other way: e.g., try to insert
a DLS from $G_{2}$ into $G_{1}$ in case both of the addresses $a_{1}$ and
$a_{2}$ point to DLSs or fall-back to introducing a 0/1 abstract object as
mentioned in Section 0.4). However, unlike in the function
$\mathit{joinTargetObjects}$, if we do not want to go deeper in the SMGs
(which we do not want for efficiency reasons), there is not so many properties
to check since we do not have two objects whose labelling we could compare,
but the single DLS $d_{1}$ whose counterpart we want to virtually insert into
$G_{2}$ only. So, we at least check that there is no conflict of the successor
addresses $a_{next}$ and $a_{2}$ according to the current mapping of nodes,
i.e., we require
$m_{1}(a_{next})=\bot\;\vee\;m_{2}(a_{2})=\bot\;\vee\;m_{1}(a_{next})=m_{2}(a_{2})$.

If the above checks pass, the DLS insertion proceeds as follows: Let $F$ be
the set of the linking fields of $d_{1}$ that are oriented forward wrt the
direction of the traversal. In particular, let
$F=\\{\textit{nfo}_{1}(d_{1})\\}$ if $\textit{tg}(P_{1}(a_{1}))=\mathtt{fst}$,
and $F=\\{\textit{pfo}_{1}(d_{1})\\}$ if
$\textit{tg}(P_{1}(a_{1}))=\mathtt{lst}$. First, the DLS $d$ representing the
join of $d_{1}$ and the virtually inserted $d_{2}$ is created in the
destination SMG with the same labelling as that of $d_{1}$ up to
$\textit{len}(d)=0$. Together with basically copying the DLS $d_{1}$ from
$G_{1}$ to $G$, we also copy the $F$-restricted sub-SMG rooted at it from
$G_{1}$ into $G$, excluding the nodes for which $m_{1}$ is already defined
(these were already reached through some other paths in the past, and the
newly copied part of the $F$-restricted sub-SMG rooted at $d_{1}$ is just
linked to them). Subsequently, the algorithm extends the mapping $m_{1}$ for
the nodes newly inserted to $G$, creates the appropriate address node $a\in A$
as well as the points-to edge leading from $a$ to $d$, and extends the mapping
of addresses such that $m_{1}(a_{1})=a$. The algorithm then continues by
joining the pair of successor values $a_{next}$ and $a_{2}$.

Algorithm 9 $\mathit{insertLeftDlsAndJoin}$($s$, $G_{1}$, $G_{2}$, $G$,
$m_{1}$, $m_{2}$, $a_{1}$, $a_{2}$, $l_{diff}$)

Input:

  * •

Initial join status $s\in\mathbb{J}$.

  * •

SMGs $G_{1}=(O_{1},V_{1},\Lambda_{1},H_{1},P_{1})$,
$G_{2}=(O_{2},V_{2},\Lambda_{2},H_{2},P_{2})$, and $G=(O,V,\Lambda,H,P)$.

  * •

Injective partial mappings of nodes $m_{1},m_{2}$ as defined in Section 0.9.

  * •

Values $a_{1}\in V_{1}$ such that
$\textit{kind}_{1}(o(P_{1}(a_{1})))=\mathtt{dls}$ and $a_{2}\in V_{2}$.

  * •

Nesting level difference $l_{diff}\in\mathbb{Z}$.

Output:

  * •

$\bot$ in case of an unrecoverable failure.

  * •

$\hookleftarrow$ in case of a recoverable failure.

  * •

Otherwise, a tuple
$(s^{\prime},G_{1}^{\prime},G_{2}^{\prime},G^{\prime},m_{1}^{\prime},m_{2}^{\prime},a^{\prime})$
where:

    * –

$s^{\prime}\in\mathbb{J}$ is the resulting join status.

    * –

$G_{1}^{\prime},G_{2}^{\prime},G^{\prime}$ are SMGs as defined in Section
0.9.4.

    * –

$m_{1}^{\prime}$, $m_{2}^{\prime}$ are the resulting injective partial
mappings of nodes.

    * –

$a^{\prime}$ is an address in $G^{\prime}$ satisfying the conditions stated in
Section 0.9.4.

Method:

  1. 1.

Let $(d_{1},o\\!f,\textit{tg}):=P_{1}(a_{1})$.

  2. 2.

If $\textit{tg}=\mathtt{fst}$, let $nf:=\textit{nfo}_{1}(d_{1})$; if
$\textit{tg}=\mathtt{lst}$, let $nf:=\textit{pfo}_{1}(d_{1})$; otherwise
return $\hookleftarrow$.

  3. 3.

Let $a_{next}:=H_{1}(d_{1},nf,\mathtt{ptr})$.

  4. 4.

If $m_{1}(d_{1})\neq\bot$, then:

     * •

Let $d:=m_{1}(d_{1})$.

     * •

If $\exists o\in O:\;m_{2}(o)=d$, return $\hookleftarrow$.

     * •

If $m_{1}(a_{1})=\bot$, create a new value node $a\in V$ and a new edge
$a\raisebox{-1.29167pt}{$\xrightarrow{\smash{\raisebox{-0.43057pt}{$\scriptstyle
o\\!f,\textit{tg}$}}}$}d$ in $P$, and extend the mapping of nodes such that
$m_{1}(a_{1})=a$. Otherwise let $a:=m_{1}(a_{1})$ and return
$(s,G_{1},G_{2},G,m_{1},m_{2},a)$.

     * •

Let
$res:=\mathit{joinValues}(s,G_{1},G_{2},G,m_{1},m_{2},a_{next},a_{2},l_{diff})$.
If $res=\bot$, return $\bot$. Otherwise, let
$(s,G_{1},G_{2},G,m_{1},m_{2},a):=res$.

  5. 5.

If $m_{1}(a_{next})\neq\bot$ and $m_{2}(a_{2})\neq\bot$ and
$m_{1}(a_{next})\neq m_{2}(a_{2})$, return $\hookleftarrow$.

  6. 6.

Let $s^{\prime}:=(\textit{len}_{1}(d_{1})=0)~{}?~{}\sqsupset~{}:~{}\Join$. Let
$s:=\mathit{updateJoinStatus}(s,s^{\prime})$.

  7. 7.

Extend $G$ by a fresh copy of the $\\{nf\\}$-restricted sub-SMG of $G_{1}$
rooted at $d_{1}$, but excluding the nodes that are already mapped in $m_{1}$
such that the copy of $d_{1}$ is a DLS $d$. Then extend the mapping $m_{1}$
such that the newly created nodes in $O\cup V$ are mapped from the
corresponding nodes of $O_{1}\cup V_{1}$.

  8. 8.

Initialize the labelling of $d$ to match the labelling of $d_{1}$ up to the
minimum length, which is fixed to zero, i.e., $\textit{len}(d)=0$.

  9. 9.

Let $a\in V$ be the address such that $P(a)=(o\\!f,\textit{tg},d)$ if such an
address exists in $G$. Otherwise, create a new value node $a\in V$ and a new
edge
$a\raisebox{-1.29167pt}{$\xrightarrow{\smash{\raisebox{-0.43057pt}{$\scriptstyle
o\\!f,\textit{tg}$}}}$}d$ in $P$, and extend the mapping of nodes such that
$m_{1}(a_{1})=a$.

  10. 10.

Let
$res:=\mathit{joinValues}(s,G_{1},G_{2},G,m_{1},m_{2},a_{next},a_{2},l_{diff})$.
If $res=\bot$, return $\bot$. Otherwise let
$(s,G_{1},G_{2},G,m_{1},m_{2},a^{\prime}):=res$.

  11. 11.

Introduce a new has-value edge
$d\raisebox{-1.29167pt}{$\xrightarrow{\smash{\raisebox{-0.43057pt}{$\scriptstyle
nf,\mathtt{ptr}$}}}$}a^{\prime}$ in $H$.

  12. 12.

Return $(s,G_{1},G_{2},G,m_{1},m_{2},a)$.

###  0.9.6 Delayed Join of Sub-SMGs

The mechanism of DLS insertion increases the chances for two SMGs to be
successfully joined, but it brings one complication to be taken care of.
Assume that SMGs $G_{1}$ and $G_{2}$ are being joined into an SMG $G$. When
applying the DLS insertion mechanism on a DLS $d_{1}$ from $G_{1}$, the not
yet traversed sub-SMG $G_{1}^{\prime}$ of $G_{1}$ reachable from $d_{1}$ is
copied into $G$ too (likewise for the symmetric case). However, some nodes of
$G_{1}^{\prime}$ that are inserted into $G_{2}$ may in fact exist in $G_{2}$
and be reachable through some other address than the address at which the DLS
insertion is started. Note that this _may_ but _needs not_ happen, and at the
time when the DLS insertion is run, it is unknown which of the two cases
applies. In theory, a backward traversal through the SMGs could be used here,
but we chose not to use it since we were afraid of its potential bad impact on
the performance. That is why, we always insert a DLS together with the sub-SMG
rooted at it, and as soon as we realize that some DLS $d_{1}$ from $G_{1}$
whose counterpart was inserted into $G_{2}$ does have a real counterpart in
$G_{2}$, the result of the join of $d_{1}$ with the inserted DLS is deleted
(together with all the values and objects reachable from that DLS only) and a
proper join—which we denote as the so-called _delayed join_ —is used instead
(cf. Point 10 of the function $\mathit{joinTargetObjects}$). Note that running
the delayed join is indeed necessary since the insertion of a DLS is
optimistic in that its sub-SMG is either missing too, or if it is not missing,
it is the same as the sub-SMG of the inserted DLS. This needs, however, not to
be the case.

###  0.9.7 Join of SPCs

The $\mathit{joinSPCs}$ function (cf. Alg. 10) is the top-level of the join
algorithm used when reducing the number of SPCs generated for particular basic
blocks of the program being analysed. It inputs a pair of garbage-free SPCs
$C_{1}=(G_{1},\nu_{1})$, $C_{2}=(G_{2},\nu_{2})$ where
$range(\nu_{1})=range(\nu_{2})=\textit{Var}$ is the common set of program
variables, and for each $x\in\textit{Var}$, the objects $\nu_{1}(x)$ and
$\nu_{2}(x)$ are labelled equally (this condition necessarily holds for SPCs
generated for the same program). The algorithm either fails and returns
$\bot$, or it returns the resulting join status and an SPC $C=(G,\nu)$ where
$range(\nu)=\textit{Var}$, and the triple $G_{1}$, $G_{2}$, $G$ satisfies the
assertions about joined SMGs stated in Section 0.3.2.

The function starts by initializing the mappings of nodes $m_{1}$ and $m_{2}$
to the empty set and the join status $s$ to $\simeq$. Then, for each program
variable $x\in\textit{Var}$, a fresh region $r$ is created in $G$, labelled
equally as $r_{1}$ (or $r_{2}$), and the mappings are extended such that
$\nu(x)=m_{1}(r_{1})=m_{2}(r_{2})=r$ where $r_{1}=\nu_{1}(x)$ and
$r_{2}=\nu_{2}(x)$. Next, for each program variable $x\in\textit{Var}$, the
$\mathit{joinSubSMGs}$ function is called with the corresponding triple of
objects $\nu_{1}(x),\nu_{2}(x),\nu(x)$. The value of $m_{1}$, $m_{2}$, and $s$
gets propagated between each pair of subsequent calls. Subsequently, the
$\mathit{joinSPCs}$ function checks whether there was not created any cycle
consisting of 0+ DLSs only in $G$, and if so, the algorithm fails since the
DLS consistency requirement would be broken this way (cf. Section 0.2.3).

Algorithm 10 $\mathit{joinSPCs}(C_{1},C_{2})$

Input:

  * •

Garbage-free SPCs $C_{1}=(G_{1},\nu_{1})$, $C_{2}=(G_{2},\nu_{2})$ with SMGs
$G_{1}=(O_{1},V_{1},\Lambda_{1},H_{1},P_{1})$,
$G_{2}=(O_{2},V_{2},\Lambda_{2},H_{2},P_{2})$
where $range(\nu_{1})=range(\nu_{2})=\textit{Var}$, and for each
$v\in\textit{Var}$,
the labelling of $\nu_{1}(v)$ is equal to the labelling of $\nu_{2}(v)$.

Output:

  * •

$\bot$ in case $C_{1}$ and $C_{2}$ cannot be joined.

  * •

Otherwise, a tuple $(s,C)$ where:

    * –

$s\in\mathbb{J}$ is the resulting join status.

    * –

$C=(G,\nu)$ where $range(\nu)=\textit{Var}$ and the SMG $G$ satisfies the
condition
$\textit{MI}(G_{1})\subseteq\textit{MI}(G)\supseteq\textit{MI}(G_{2})$.

Method:

  1. 1.

Let $G$ be an empty SMG $G$, $\nu:=m_{1}:=m_{2}:=\emptyset$, $s:=\;\simeq$.

  2. 2.

For each program variable $v\in\textit{Var}$:

     * •

Let $r_{1}:=\nu_{1}(v)$ and $r_{2}:=\nu_{2}(v)$.

     * •

Create a fresh region $r\in O$, initialize its labelling to match the
labelling of $r_{1}$.

     * •

Extend the mappings such that $m_{1}(r_{1})=m_{2}(r_{2})=\nu(v)=r$.

  3. 3.

For each program variable $v\in\textit{Var}$:

     * •

Let $r_{1}:=\nu_{1}(v)$, $r_{2}:=\nu_{2}(v)$, and $r:=\nu(v)$.

     * •

Let $res:=\mathit{joinSubSMGs}(s,G_{1},G_{2},G,m_{1},m_{2},r_{1},r_{2},r,0)$.

     * •

If $res=\bot$, return $\bot$. Otherwise, let
$(s,G_{1},G_{2},G,m_{1},m_{2}):=res$.

  4. 4.

If there is any cycle consisting solely of 0+ DLSs in $G$, return $\bot$.

  5. 5.

Return $(s,C)$ where $C=(G,\nu)$.

###  0.9.8 Join of Sub-SMGs within Abstraction

The $joinSubSMGsForAbstraction$ function (cf. Alg. 11) implements the core
functionality of the elementary merge operation used as a part of our
abstraction mechanism (Section 0.3.3). It inputs an SMG $G=(O,V,\Lambda,H,P)$,
a pair of objects $o_{1},o_{2}\in O$, and a triple of binding offsets hfo,
nfo, $\textit{pfo}\in\mathbb{N}$. If it succeeds, it returns an SMG
$G^{\prime}=(O^{\prime},V^{\prime},\Lambda^{\prime},H^{\prime},P^{\prime})$
and a fresh DLS $d\in O^{\prime}$ which represents the merge of $o_{1}$ and
$o_{2}$ in $G^{\prime}$ and which is the entry point of the sub-SMG
representing a join of the sub-SMGs rooted at $o_{1}$ and $o_{2}$. What
remains to be done in the elementary merge operation is the reconnection of
the pointers surrounding $o_{1}$ and $o_{2}$ to $d$ (apart from those related
to their nested sub-SMGs), cf. Section 0.3.3. As an auxiliary result (used in
the algorithm of searching for longest mergeable sequences), the algorithm
returns the join status $s\in\mathbb{J}$ comparing the semantics of the sub-
SMGs rooted at $o_{1}$ and $o_{2}$ as well as the sets $O_{1},O_{2}\subseteq
O^{\prime}$ and $V_{1},V_{2}\subseteq V^{\prime}$ that contain those objects
and values whose join produced the sub-SMG nested below $d$. Note that the
join status returned by $\mathit{mergeSubSMGs}$ is not affected by the kinds
of $o_{1},o_{2}$ and the values in their next/prev fields since the loss of
information due to merging $o_{1}$ and $o_{2}$ into a single list segment is
deliberate.

The function proceeds as follows. Using the offsets nfo, pfo, the values of
the next/prev fields of $o_{1}$ and $o_{2}$ are remembered and temporarily
replaced by $0$ (in order for the subsequently started join of sub-SMGs not to
go through these fields). Then a fresh DLS $d$ is created in $O$ and labelled
by the given offsets hfo, nfo, pfo and the minimum length equal to
$\textit{len}_{1}(o_{1})+\textit{len}_{2}(o_{2})$, other labels are taken from
$o_{1}$ (or $o_{2}$ since the other labels are equal). The mapping of objects
is initialized such that $m_{1}(o_{1})=m_{2}(o_{2})=d$ and the nesting level
difference is initialized based on $\textit{kind}(o_{1})$ and
$\textit{kind}(o_{2})$ using the rules stated in Section 0.9.2. The generic
algorithm $\mathit{joinSubSMGs}$ is then called on the triple $o_{1},o_{2},d$.
If it fails or the resulting SMG contains any cycle consisting of 0+ DLSs
only, the algorithm exits unsuccessfully. If it succeeds, the values of the
next/prev fields in $o_{1},o_{2}$, which were temporarily replaced by $0$, are
restored to their original values. If
$\textit{kind}(o_{1})=\textit{kind}(o_{2})=\mathtt{reg}$, the level of each
node that appears in the image of $m_{1}$ (or $m_{2}$) is increased by one
(since these nodes are now recognized as nested), and all points-to edges
leading to $d$ are relabelled by the $\mathtt{all}$ target specifier.

The resulting sets of nodes are computed as follows: $O_{1}:=range(m_{1})\cap
O$, $O_{2}:=range(m_{2})\cap O$, $V_{1}:=range(m_{1})\cap V$, and
$V_{2}=range(m_{2})\cap V$. The resulting join status is the status returned
by $\mathit{joinSubSMGs}$.

Algorithm 11 $\mathit{joinSubSMGsForAbstraction}$($G$, $o_{1}$, $o_{2}$, hfo,
nfo, pfo)

Input:

  * •

SMGs $G=(O,V,\Lambda,H,P)$.

  * •

Objects $o_{1},o_{2}\in O$ that are the roots of the
$\\{\textit{nfo},\textit{pfo}\\}$-restricted sub-SMGs $G_{1}$ and $G_{2}$ of
$G$ that are to be joined and that are such that $level(o_{1})=level(o_{2})$
and $size(o_{1})=size(o_{2})$.

  * •

Candidate DLS offsets $\textit{hfo},\textit{nfo},\textit{pfo}\in\mathbb{N}$.

Output:

  * •

$\bot$ in case $G_{1}$ and $G_{2}$ cannot be joined.

  * •

Otherwise, a tuple $(s,G^{\prime},d,O_{1},V_{1},O_{2},V_{2})$ where:

    * –

$s\in\mathbb{J}$ is the resulting join status (determines the cost of joining
$G_{1}$ and $G_{2}$).

    * –

$G^{\prime}$ is an SMG obtained from the input SMG $G$ by extending it with a
new DLS $d$ below which the join of $G_{1}$ and $G_{2}$ is nested.

    * –

$O_{i}\subseteq O$ and $V_{i}\subseteq V$ for $i=1,2$ are sets of non-shared
objects and values of $G_{1}$ and $G_{2}$, respectively.

Method:

  1. 1.

Let $a_{p}:=H(o_{1},\textit{pfo},\mathtt{ptr})$,
$a_{n}:=H(o_{2},\textit{nfo},\mathtt{ptr})$,
$a_{1}:=H(o_{1},\textit{nfo},\mathtt{ptr})$,
and $a_{2}:=H(o_{2},\textit{pfo},\mathtt{ptr})$.

  2. 2.

Replace each has-value edge of $H$ leading from $o_{1}$ or $o_{2}$ and
labelled by $(\textit{nfo},\mathtt{ptr})$ or $(\textit{pfo},\mathtt{ptr})$ by
a has-value edge leading to $0$ and having the same label.

  3. 3.

Extend $O$ with a fresh valid DLS $d$ and label it with the head, next, and
prev offsets hfo, nfo, and pfo, the minimum length
$\textit{len}(o_{1})+\textit{len}(o_{2})$, level $\textit{level}(o_{1})$, and
the size $\textit{size}(o_{1})$.

  4. 4.

If $\textit{kind}(o_{1})=\textit{kind}(o_{2})$, let $l_{diff}:=0$. Otherwise,
let $l_{diff}:=(\textit{kind}(o_{1})=\mathtt{dls})?1:-1$.

  5. 5.

Let
$res:=\mathit{joinSubSMGs}(\simeq,G_{1},G_{2},G,\\{(o_{1},d)\\},\\{(o_{2},d)\\},o_{1},o_{2},d,l_{diff})$.
If $res=\bot$, return $\bot$. Otherwise let $(s,\\_,\\_,G,m_{1},m_{2}):=res$.

  6. 6.

If $G$ contains any cycle consisting of 0+ DLSs only, return $\bot$.

  7. 7.

Drop the temporarily created has-value edges of $H$ leading from $o_{1}$ and
$o_{2}$ to $0$ and labelled by $(\textit{nfo},\mathtt{ptr})$ or
$(\textit{pfo},\mathtt{ptr})$ and restore the original has-value edges
$o_{1}\raisebox{-1.29167pt}{$\xrightarrow{\smash{\raisebox{-0.43057pt}{$\scriptstyle\textit{pfo},\mathtt{ptr}$}}}$}a_{p}$,
$o_{1}\raisebox{-1.29167pt}{$\xrightarrow{\smash{\raisebox{-0.43057pt}{$\scriptstyle\textit{nfo},\mathtt{ptr}$}}}$}a_{1}$,
$o_{2}\raisebox{-1.29167pt}{$\xrightarrow{\smash{\raisebox{-0.43057pt}{$\scriptstyle\textit{pfo},\mathtt{ptr}$}}}$}a_{2}$,
and
$o_{2}\raisebox{-1.29167pt}{$\xrightarrow{\smash{\raisebox{-0.43057pt}{$\scriptstyle\textit{nfo},\mathtt{ptr}$}}}$}a_{n}$.

  8. 8.

If $\textit{kind}(o_{1})=\textit{kind}(o_{2})=\mathtt{reg}$, increase by one
the level of each object and value that appears in the image of $m_{1}$ or
$m_{2}$, and relabel all points-to edges leading to $d$ by the $\mathtt{all}$
target specifier.

  9. 9.

Return $(s,G,d,O\cap range(m_{1}),V\cap range(m_{1}),O\cap range(m_{2}),V\cap
range(m_{2}))$.

##  0.10 Longest Mergeable Sequences

In this appendix, we formalize the notion of longest mergeable sequences
informally introduced in Section 0.3.3. Assume an SPC $C=(G,\nu)$ where
$G=(O,V,\Lambda,H,P)$ is an SMG with the sets of regions $R$, DLSs $D$, and
addresses $A$. The _longest mergeable sequence_ of objects given by a
candidate DLS entry
$(o_{c},\textit{hfo}_{c},\textit{nfo}_{c},\textit{pfo}_{c})$ where $o_{c}\in
O$ is the longest sequence of distinct valid heap objects of $G$ whose first
object is $o_{c}$; all objects in the sequence are of level $0$; all DLSs that
appear in the sequence have $\textit{hfo}_{c}$, $\textit{nfo}_{c}$, and
$\textit{pfo}_{c}$ as their head, next, and prev offsets; and the following
holds for any two neighbouring objects $o_{1}$ and $o_{2}$ in the sequence:

  1. 1.

The objects $o_{1}$ and $o_{2}$ are doubly-linked, i.e., there are addresses
$a_{1},a_{2}\in A$ such that
$o_{1}\raisebox{-1.29167pt}{$\xrightarrow{\smash{\raisebox{-0.43057pt}{$\scriptstyle\textit{nfo}_{c},\mathtt{ptr}$}}}$}a_{1}\raisebox{-1.29167pt}{$\xrightarrow{\smash{\raisebox{-0.43057pt}{$\scriptstyle\textit{hfo}_{c},\textit{tg}_{2}$}}}$}o_{2}$
for $\textit{tg}_{2}\in\\{\mathtt{fst},\mathtt{reg}\\}$ and
$o_{2}\raisebox{-1.29167pt}{$\xrightarrow{\smash{\raisebox{-0.43057pt}{$\scriptstyle\textit{pfo}_{c},\mathtt{ptr}$}}}$}a_{2}\raisebox{-1.29167pt}{$\xrightarrow{\smash{\raisebox{-0.43057pt}{$\scriptstyle\textit{hfo}_{c},\textit{tg}_{1}$}}}$}o_{1}$
for $\textit{tg}_{1}\in\\{\mathtt{lst},\mathtt{reg}\\}$.

  2. 2.

The $\\{\textit{nfo}_{c},\textit{pfo}_{c}\\}$-restricted sub-SMGs $G_{1}$,
$G_{2}$ of $G$ rooted at $o_{1}$ and $o_{2}$ can be joined using the extended
join algorithm that yields the sub-SMG $G_{1,2}$ to be nested below the join
of $o_{1}$ and $o_{2}$ as well as the sets $O_{1}$, $V_{1}$ and $O_{2}$,
$V_{2}$ of non-shared objects and values of $G_{1}$ and $G_{2}$, respectively,
whose join gives rise to $G_{1,2}$.

  3. 3.

The non-shared objects and values of $G_{1}$ and $G_{2}$ (other than $o_{1}$
and $o_{2}$ themselves) are reachable via $o_{1}$ or $o_{2}$, respectively,
only. This is, $\forall a\in A\setminus V_{1}~{}\forall o^{\prime}\in
O_{1}\setminus\\{o_{1}\\}:o(P(a))\neq o^{\prime},~{}\forall o^{\prime}\in
O\setminus O_{1}~{}\forall v\in V_{1}:~{}v\notin H(o^{\prime})$, and likewise
for $o_{2}$, $V_{2}$, and $O_{2}$. Moreover, the sets $O_{1}$ and $O_{2}$
contain heap objects only.

  4. 4.

The objects $o_{1}$ and $o_{2}$ are a part of an uninterrupted sequence.
Therefore:

    1. (a)

Regions that are not the first nor last in the sequence can be pointed to
their head offset from their predecessor, successor, or from their non-shared
restricted sub-SMG only. Formally, if $o_{1}\in R\setminus\\{o_{c}\\}$, then
$\neg~{}\exists o\in O\setminus(O_{1}\cup\\{o_{2},o^{\prime}\\})$ $\exists
a\in A~{}\exists
o\\!f\in\mathbb{N}:~{}o\raisebox{-1.29167pt}{$\xrightarrow{\smash{\raisebox{-0.43057pt}{$\scriptstyle
o\\!f,ptr$}}}$}a\raisebox{-1.29167pt}{$\xrightarrow{\smash{\raisebox{-0.43057pt}{$\scriptstyle\textit{hfo}_{c},\mathtt{reg}$}}}$}o_{1}$
where the object $o^{\prime}$ is the predecessor of $o_{1}$, i.e.,
$o^{\prime}=o(P(H(o_{1},\textit{pfo}_{c},\mathtt{ptr})))$.292929Note that no
special formal treatment is needed for $o_{2}$ since it will take the role of
$o_{1}$ when checking the next neighbouring pair in the sequence. The above
also implicitly ensures that pointers to the head offset of the last object
are not restricted.

    2. (b)

If $o_{1}$ ($o_{2}$) is a DLS, the only object that can point to its end
(beginning) is $o_{2}$ ($o_{1}$), resp. Formally, $\text{if }o_{1}\in D\text{,
then }\neg~{}\exists o\in O\setminus\\{o_{2}\\}~{}\exists a\in A$ $\exists
o\\!f\in\mathbb{N}:o\raisebox{-1.29167pt}{$\xrightarrow{\smash{\raisebox{-0.43057pt}{$\scriptstyle
o\\!f,\mathtt{ptr}$}}}$}a\raisebox{-1.29167pt}{$\xrightarrow{\smash{\raisebox{-0.43057pt}{$\scriptstyle\textit{hfo}_{c},\mathtt{lst}$}}}$}o_{1}$.
$\text{If }o_{2}\in D\text{, then }\neg~{}\exists o\in
O\setminus\\{o_{1}\\}~{}\exists a\in A$ $\exists
o\\!f\in\mathbb{N}:o\raisebox{-1.29167pt}{$\xrightarrow{\smash{\raisebox{-0.43057pt}{$\scriptstyle
o\\!f,\mathtt{ptr}$}}}$}a\raisebox{-1.29167pt}{$\xrightarrow{\smash{\raisebox{-0.43057pt}{$\scriptstyle\textit{hfo}_{c},\mathtt{fst}$}}}$}o_{2}$.

    3. (c)

Finally, only non-shared objects of $G_{1}$ and $G_{2}$ can point to non-head
offsets of $o_{1}$ and $o_{2}$, respectively. Formally, $\neg~{}\exists o\in
O\setminus O_{1}~{}\exists a\in A$ $\exists
o\\!f,o\\!f^{\prime}\in\mathbb{N}~{}\exists\textit{tg}\in\mathbb{S}:~{}o\raisebox{-1.29167pt}{$\xrightarrow{\smash{\raisebox{-0.43057pt}{$\scriptstyle
o\\!f,\mathtt{ptr}$}}}$}a\raisebox{-1.29167pt}{$\xrightarrow{\smash{\raisebox{-0.43057pt}{$\scriptstyle
o\\!f^{\prime},\textit{tg}$}}}$}o_{1}~{}\wedge~{}o\\!f^{\prime}\neq\textit{hfo}_{c}$,
and likewise for $o_{2}$ and $O_{2}$.

##  0.11 Symbolic Execution of Conditional Statements

Checking equality of values is trivial in SMGs since it reduces to identity
checking. To check non-equality, we propose a sound, efficient, but incomplete
approach as mentioned already in Section 0.3.4. This approach is formalized in
the function $proveNeq$ shown as Alg. 12 that contains a number of comments to
make it self-explaining. The algorithm uses the $lookThrough$ function (Alg.
13) for traversing chains of $0+$ DLSs while looking for objects whose
existence is guaranteed and whose unique addresses can serve as a basis for a
non-equality proof. Note that the algorithms do not allow for comparing values
of fields with incompatible types. Hence, we require all type-casts to be
explicitly represented as separate instructions of the intermediate code so
that the fields being compared are always of compatible types.

If neither equality nor inequality of a pair of values $v_{1}$ and $v_{2}$,
which are compared in a conditional statement, can be established, the
symbolic execution must follow both branches of the conditional statement. For
each of the branches, we attempt to reflect the condition allowing the
execution to enter that branch in the SMG $G$ to be processed in the branch,
effectively reducing the semantics of $G$. However, for efficiency reasons, we
do again not reflect all consequences of the branch conditions that could in
theory be reflected, but only the easy to handle ones, which is sound, and it
suffices in all the case studies that we have considered. In particular, we
restrict SMGs according to the branch conditions as follows (if none of the
below described cases applies, the SMGs are not modified):

  * •

If $v_{1}$ and/or $v_{2}$ are non-address values, one of them is replaced by
the other in the $v_{1}=v_{2}$ branch (a non-address value can be replaced by
an address but not vice versa).

  * •

If there is a chain of $0+$ DLSs connected into a doubly-linked list in the
given SMG such that the $\mathtt{fst}$ address of the first DLS is $v_{1}$ and
the last DLS contains $v_{2}$ in its next field (or vice versa), the chain is
removed by calling the DLS removal algorithm repeatedly in the $v_{1}=v_{2}$
branch. In the $v_{1}\neq v_{2}$ branch, the computation is split to as many
cases as the number of $0+$ DLSs in the chain is, and in each of the cases,
the minimum length of one of the DLSs is incremented (reflecting that at least
one of them must be non-empty).

  * •

If $v_{1}$ points to a DLS $d$ with the $\mathtt{fst}$ target specifier and
$v_{2}$ points to $d$ with the $\mathtt{lst}$ target specifier (or vice
versa), it is clear that $\textit{len}(d)<2$ since otherwise $proveNeq$ would
succeed in proving the inequality between $v_{1}$ and $v_{2}$. In this case,
the following two modifications of the encountered SMGs can be applied in the
different branches of the encountered conditional statement:

    * –

In the $v_{1}=v_{2}$ branch, if $\textit{len}(d)=1$, the DLS $d$ is replaced
by an equally labelled region (excluding the DLS-specific labels) since $d$
must consist of exactly one concrete node in this case.

    * –

In the $v_{1}\neq v_{2}$ branch, if $\textit{len}(d)=1$ or the value of the
next address is equal to the value of the prev address, i.e.,
$H(d,\textit{pfo}(d),\mathtt{ptr})=H(d,\textit{nfo}(d),\mathtt{ptr})$, then
the minimum length of $d$ is increased to $2$ since $d$ must consist of at
least two concrete nodes in this case.

Besides equality checking, we also allow for comparisons of addresses using
the _less than_ or _greater than_ operators in case both of the addresses
point to the same (concrete) object—we simply compare the offsets. This
functionality is needed for successful verification of the NSPR-based case
studies mentioned in Section 0.6.

Algorithm 12 $proveNeq(G,v_{1},v_{2})$

Input:

  * •

An SMG $G=(O,V,\Lambda,H,P)$.

  * •

A pair of values $v_{1},v_{2}\in V$ such that
$\textit{level}(v_{1})=\textit{level}(v_{2})=0$.

Output:

  * •

true if the inequality between the given pair of values was proven, false
otherwise.

Method:

  1. 1.

Let $(v_{1},O_{1}):=lookThrough(G,v_{1})$.

  2. 2.

Let $(v_{2},O_{2}):=lookThrough(G,v_{2})$.

  3. 3.

If $v_{1}=v_{2}$ or $O_{1}\cap O_{2}\neq\emptyset$, return false. 6.5cm//
possible sharing of values

  4. 4.

If $v_{1}\notin A$ or $v_{2}\notin A$, return false. 6.5cm// simplified
handling of data values

  5. 5.

Let $o_{1}:=o(P(v_{1}))$ and $o_{2}:=o(P(v_{2}))$.

  6. 6.

If $o_{1}=o_{2}$:

     * •

If $\textit{tg}(P(v_{1}))=\textit{tg}(P(v_{2}))$, return true. 5.9cm// same
object, different offsets

     * •

If $\textit{tg}(P(v_{1}))=\mathtt{fst}$ and
$\textit{tg}(P(v_{2}))=\mathtt{lst}$, return $\textit{len}^{\prime}(o_{1})\geq
2$.

     * •

If $\textit{tg}(P(v_{1}))=\mathtt{lst}$ and
$\textit{tg}(P(v_{2}))=\mathtt{fst}$, return $\textit{len}^{\prime}(o_{1})\geq
2$.

     * •

Otherwise return false.

  7. 7.

If $o\\!f(P(v_{1}))<0$ or $o\\!f(P(v_{2}))<0$, return false. 6.5cm// out of
bounds

  8. 8.

If $v_{1}\neq 0$ and $\textit{size}(o_{1})\leq o\\!f(P(v_{1}))$, return false.
6.5cm// out of bounds

  9. 9.

If $v_{2}\neq 0$ and $\textit{size}(o_{2})\leq o\\!f(P(v_{2}))$, return false.
6.5cm// out of bounds

  10. 10.

If $v_{1}=0$ or $v_{2}=0$, return true. 6.5cm// $0$ and a valid address of an
object

  11. 11.

Return $\textit{valid}(o_{1})\wedge\textit{valid}(o_{2})$. 6.5cm// addresses
of allocated objects

Algorithm 13 $lookThrough(G,v)$

Input:

  * •

An SMG $G=(O,V,\Lambda,H,P)$.

  * •

A value $v\in V$ such that $\textit{level}(v)=0$.

Output:

  * •

A pair $(v^{\prime},Visited)$ where:

    * –

$v^{\prime}\in V$ is the value reached after all 0+ DLSs are traversed.

    * –

$Visited$ is the set of all 0+ DLSs reachable from $v$ in the forward
direction without traversing any other object.

Method:

  1. 1.

Let $Visited:=\emptyset$.

  2. 2.

Let $o:=o(P(v))$.

  3. 3.

If $o\notin\\{\bot,\\#\\}$ and $\textit{len}^{\prime}(o)=0$, then:

     * •

Let $Visited:=Visited\cup\\{o\\}$.

     * •

If $\textit{tg}(P(v))=\mathtt{fst}$, let
$v:=H(o,\textit{nfo}(o),\mathtt{ptr})$ and continue with step 2.

     * •

If $\textit{tg}(P(v))=\mathtt{lst}$, let
$v:=H(o,\textit{pfo}(o),\mathtt{ptr})$ and continue with step 2.

  4. 4.

Return $(v,Visited)$.

##  0.12 Usage of Predator

The simplest way of running Predator is to use either the slgcc or slllvm
scripts as shown below with `SOURCE.c` being the C program that Predator
should analyse:

`/PATH_TO_predator_DIRECTORY/sl/slgcc SOURCE.c`

`/PATH_TO_predator_DIRECTORY/sl/slllvm SOURCE.c`

The run of Predator can be influenced by a number of options summarised in
Table 3. The options can be passed to Predator via the environment variable
`SL_OPTS`). Further settings can then be provided via the config.h file from
the Predator distribution as discussed below.

Predator can also be invoked directly through the chosen compiler. In
particular, one can proceed as follows with the GCC compiler:

`gcc [CFLAGS] -fplugin=LIBSL [SL_OPTS] SOURCE.c`

Here, `LIBSL` represents a path to the Predator plug-in, which always ends
with the .so suffix for GCC. For instance, when starting Predator from its
main directory, `LIBSL` should be replaced by `./sl_build/libsl.so`. When
launching Predator this way, one can use compiler options `CFLAGS`, such as
-m32/-m64, as well as Predator options `SL_OPTS` described in Table 3.

For the Clang/LLVM compiler, one has to first create the bitcode file and then
start the analysis:

`clang [CFLAGS] -Xclang -fsanitize-address-use-after-scope\`

`-g -S -emit-llvm SOURCE.c -o SOURCE.bc`

`opt SOURCE.bc -lowerswitch -load LIBSL -sl [SL_OPTS]`

A further possibility not requiring additional options but available on Linux
only is the following:

`clang -g SOURCE.c -Xclang -load -Xclang LIBSL`

For Clang/LLVM, the Predator plug-in has the .so suffix on Linux and the
.dylib suffix on Darwin.

###  0.12.1 Deeper Configuration of Predator

Apart from using the above described options, one can further configure the
behaviour of Predator using the config.h file from its distribution. After
that, Predator must, of course, be recompiled. Moreover, usage some of the
above described options can be replaced by changing the config.h file.

Via the config.h file, one can control various aspects of the _abstractions_
used in Predator. For instance, one can say whether the abstraction should be
performed at each basic block or at loop points and/or returns from function
calls only, whether abstraction to singly-/doubly-linked list segments is
allowed, what the various abstraction thresholds are, set an additional cost
for introducing list segments by abstraction, or decide whether the
abstraction of SMGs should be applied to longest sequences of SMG nodes that
are amenable to abstraction only or whether it can be applied to shorter
sequences too. One can also decide whether _integer intervals_ may be used to
represent values and/or offsets and whether they can widened.

Table 3: Predator plug-in options. For the GCC-plugin, use with the prefix -fplugin-arg-libsl. Options |  Description
---|---
-help |  Help
-verbose=<uint> |  Turn on verbose mode
-pid-file=<file> |  Write PID of self to ¡file¿
-preserve-ec |  Do not affect the exit code
-dry-run |  Do not run the analysis
-dump-pp[=<file>] |  Dump linearised CL code
-dump-types |  Dump also type info
-gen-dot[=<file>] |  Generate CFGs
-type-dot=<file> |  Generate type graphs
-args=<peer-args> |  Arguments given to the analyser (see below)
Peer arguments |
`track_uninit` |  Report usage of uninitialised values
`oom` |  Simulate possible shortage of memory (malloc can fail)
`no_error_recovery` |  No error recovery, stop the analysis as soon as an error is detected
`memleak_is_error` |  Treat memory leaks as an error
`exit_leaks` |  Report memory leaks while executing a no-return function
`verifier_error_is_error` |  Treat reaching of `__VERIFIER_error()` as an error
`error_label:<string>` |  Treat reaching of the given label as an error
`int_arithmetic_limit:<uint>` |  The highest integer number Predator can count to
`allow_cyclic_trace_graph` |  Create a node with two parents on entailment
`forbid_heap_replace` |  Do not replace a previously tracked node if entailed by a new one
`allow_three_way_join[:<uint>]` |  Using the general join of possibly incomparable SMGs (so-called three-way join)  0 never 1 only when joining nested sub-heaps 2 also when joining SPCs if considered useful 3 always
`join_on_loop_edges_only[:<int>]` |  -1 never join, never check for entailment, always check for isomorphism 0 join SPCs on each basic block entry 1 join only when traversing a loop-closing edge, entailment otherwise 2 join only when traversing a loop-closing edge, isomorphism otherwise 3 same as 2 but skips the isomorphism check if possible
`state_live_ordering[:<uint>]` |  On the fly ordering of SPCs to be processed  0 do not try to optimise the order of heaps 1 reorder heaps when joining 2 reorder heaps when creating their union (list of SMGs) too
`no_plot` |  Do not generate graphs (ignore all calls of `__sl_plot*()` and `__VERIFIER_plot()`)
`dump_fixed_point` |  Dump SPCs of the obtained fixed-point
`detect_containers` |  Detect low-level implementations of high-level list containers and operations over them (such as various initialisers, iterators, etc.) containers16 .

One can enable/disable the _call cache_ implementing a table of summaries and
set its various parameters (e.g., whether matches in the table are sought
using isomorphism or entailment, how the cache should be pruned, etc.). One
can choose the _scheduler_ choosing basic blocks to be explored (corresponding
to a depth-first search, breadth-first search, or a load-driven search
choosing blocks with fewest SPCs waiting to be explored).

One can specify various _limits_ of the analysis such as the maximum call
depth, the maximum integer constant to be tracked, or the maximum integer to
be used as the minimum length of a list segment. One can also control whether
parts of the generated SPCs should be shared using a _copy-on-write_
mechanism. One can control how much Predator should try to _recover_ after a
bug is found. Further, one can also enable/disable a static pre-analysis
trying to detect variables that are _dead_ at certain program locations whose
results may subsequently be used to prune variables tracked by the main
analysis.

The config.h file can be used to activate various _debugging outputs_ too.
Further information about what can be configured and how can be found directly
in the config.h file, which contains many explanatory comments too.

###  0.12.2 Installing and Using PredatorHP

In order to be able to use the Predator Hunting Party (PredatorHP), one has to
download its binary version or source code from
https://www.fit.vutbr.cz/research/groups/verifit/tools/predatorhp. When
building from sources, one has to make sure that git, python, and all
dependencies for Predator itself are installed. In the directory with
PredatorHP, one can use the script `build-all.sh`. To analyse a single program
using PredatorHP, one can use the following script (whose options are
described in Table 4):

`predatorHP.py --propertyfile=<prpfile> [--witness=<file>]`

`[--compiler-options=CFLAGS] SOURCE.c`

Table 4: Options of the Predator Hunting Party. Options |  Description
---|---
`-h, --help` |  Help
`-v, --version` |  Show the program’s version number
`--propertyfile=<prpfile>` |  A ¡prpfile¿ specifying properties to be verified according to SV-COMP rules
`--compiler-options=CFLAGS` |  Specify options given to compiler (e.g. `--compiler-options="-m32 -g"`)
`--witness=<file>` |  Write the witness trace in XML to ¡file¿