Deciding Memory Safety for Single-Pass Heap-Manipulating Programs

TL;DR

This paper presents a decision procedure for verifying memory safety in heap-manipulating programs that process forest data-structures in a single pass, demonstrating efficiency and practical applicability.

Contribution

It extends decidability results to alias-aware programs with map updates and develops algorithms for verifying memory safety in single-pass heap programs.

Findings

Decidable when initial heap is a forest and programs are streaming-coherent.

Verification algorithms are efficient for common single-pass data-structure algorithms.

Experimental results confirm practical applicability on library routines.

Abstract

We investigate the decidability of automatic program verification for programs that manipulate heaps, and in particular, decision procedures for proving memory safety for them. We extend recent work that identified a decidable subclass of uninterpreted programs to a class of alias-aware programs that can update maps. We apply this theory to develop verification algorithms for memory safety--- determining if a heap-manipulating program that allocates and frees memory locations and manipulates heap pointers does not dereference an unallocated memory location. We show that this problem is decidable when the initial allocated heap forms a forest data-structure and when programs are streaming-coherent, which intuitively restricts programs to make a single pass over a data-structure. Our experimental evaluation on a set of library routines that manipulate forest data-structures shows that common single-pass algorithms on data-structures often fall in the decidable class, and that our decision procedure is efficient in verifying them.

Tables

Table 1. Table 1 . Evaluation of tool for proving memory safety and finding memory safety errors

Program	LOC	Streaming-	Found	# States	Time
		coherent?	Safe		(ms)
Verification of Memory Safe Programs
sll-append-safe	19	yes	✓	4	4
sll-copy-all-safe	27	yes	✓	6	3
sll-delete-all-safe	56	yes	✓	58	9
sll-deletebetween-safe	42	yes	✓	53	8
sll-find-safe	16	yes	✓	4	3
sll-insert-back-safe	20	yes	✓	3	3
sll-insert-front-safe	8	yes	✓	1	3
sll-insert-safe	50	yes	✓	12	4
sll-reverse-safe	12	yes	✓	3	3
sll-sorted-concat-safe	17	yes	✓	4	3
sll-sorted-insert-safe	50	yes	✓	12	4
sll-sorted-merge-safe	74	yes	✓	62	8
bst-find-safe	23	yes	✓	21	4
bst-insert-safe	45	yes	✓	29	6
bst-remove-root-safe	52	yes	✓	12	4
avl-balance-safe	190	yes	✓	48	12
tree-rotate-left-safe	25	yes	✓	3	3
Finding Errors in Memory-unsafe Programs
sll-append-unsafe	20	yes	✗	—	3
sll-copy-all-unsafe	29	yes	✗	—	4
sll-delete-all-unsafe	58	yes	✗	—	5
sll-deletebetween-unsafe	44	yes	✗	—	4
sll-find-unsafe	18	yes	✗	—	3
sll-insert-back-unsafe	20	yes	✗	—	3
sll-insert-front-unsafe	9	yes	✗	—	3
sll-insert-unsafe	50	yes	✗	—	3
sll-reverse-unsafe	12	yes	✗	—	3
sll-sorted-concat-unsafe	17	yes	✗	—	3
sll-sorted-insert-unsafe	50	yes	✗	—	3
sll-sorted-merge-unsafe-1	69	yes	✗	—	4
sll-sorted-merge-unsafe-2	63	yes	✗	—	3
bst-find-unsafe	25	yes	✗	—	4
bst-insert-unsafe	49	yes	✗	—	6
bst-remove-root-unsafe	54	yes	✗	—	3
avl-balance-unsafe	111	yes	✗	—	3
tree-rotate-left-unsafe	20	yes	✗	—	3
Detecting Programs are not
streaming-coherent
sll-sorted-merge-non-streaming-coherent	75	no	—	—	4
bst-remove-root-non-streaming-coherent	55	no	—	—	3

Equations

$$⟨stmt⟩::=$$

$$\mid a:=b\mid a:=f(\mathbf{c})\mid \text{assume}(⟨cond⟩)\mid ⟨stmt⟩;⟨stmt⟩$$

$$\mid \text{if}(⟨cond⟩)\text{then}⟨stmt⟩\text{else}⟨stmt⟩\mid \text{while}(⟨cond⟩)⟨stmt⟩$$

$$⟨cond⟩::=$$

$$\Pi =\{\text{“}x:=y\text{”},\text{“}x:=y\cdot p\text{”},\text{“}y\cdot p:=x\text{”},\text{“}a:=y\cdot d\text{”},\text{“}y\cdot d:=a\text{”},\text{“}\text{alloc}(x)\text{”},\text{“}\text{free}(x)\text{”},\text{“}a:=b\text{”},$$

$$\text{“}a:=f(\mathbf{c})\text{”},\text{“}\text{assume}(x=y)\text{”},\text{“}\text{assume}(x\ne y)\text{”},\text{“}\text{assume}(a=b)\text{”},\text{“}\text{assume}(a\ne b)\text{”}$$

$$\mid x,y\in V_{\mathsf{Loc}},p\in {\mathsf{Flds}}_{\mathsf{Loc}},d\in {\mathsf{Flds}}_{\mathsf{Data}},f\in {\mathcal{F}}_{\mathsf{Data}}a,b\in V_{\mathsf{Data}},\text{ and }\mathbf{c}\text{ a tuple over }{V}_{\mathsf{Data}}\}.$$

$$\displaystyle\begin{array}[]{rcll}\textsf{Exec}(\textbf{skip})&=&\epsilon&\\ \textsf{Exec}(a)&=&a&\text{if }a\in\Pi\\ \textsf{Exec}(\textbf{assume}(c_{1}\lor c_{2}))&=&\textsf{Exec}(\textbf{assume}(c_{1}))+\textsf{Exec}(\textbf{assume}(c_{2}))&c_{1},c_{2}\in\langle cond\rangle\\ \textsf{Exec}(\textbf{assume}(c_{1}\land c_{2}))&=&\textsf{Exec}(\textbf{assume}(c_{1}))\cdot\textsf{Exec}(\textbf{assume}(c_{2}))&c_{1},c_{2}\in\langle cond\rangle\\ \textsf{Exec}(\textbf{if}\,(c)\,\textbf{then}\,s_{1}\,\textbf{else}\,s_{2})&=&\begin{aligned} &\textsf{Exec}(\textbf{assume}(c))\cdot\textsf{Exec}(s_{1})\\ &+\,\textsf{Exec}(\textbf{assume}(\neg c))\cdot\textsf{Exec}(s_{2})\end{aligned}&\begin{aligned} &c\in\langle cond\rangle,\\ &s_{1},s_{2}\in\langle stmt\rangle\end{aligned}\\ \textsf{Exec}(\textbf{while}\,(c)\,s)&=&\begin{aligned} &(\textsf{Exec}(\textbf{assume}(c))\cdot\textsf{Exec}(s))^{*}\\ &\cdot\,\textsf{Exec}(\textbf{assume}(\neg c))\end{aligned}&\begin{aligned} &c\in\langle cond\rangle,\\ &s\in\langle stmt\rangle\end{aligned}\\ \textsf{Exec}(s_{1};s_{2})&=&\textsf{Exec}(s_{1})\cdot\textsf{Exec}(s_{2})&s_{1},s_{2}\in\langle stmt\rangle\\ \end{array}$$

$$\displaystyle\begin{array}[]{rcl}\mathsf{Val}^{\mathcal{M}}_{\mathsf{Loc}}(\varepsilon,u)&=&\mathcal{I}(\widehat{u})\\ \mathsf{Val}^{\mathcal{M}}_{\mathsf{Loc}}(\sigma\cdot s,u)&=&\begin{cases}\mathsf{Val}^{\mathcal{M}}_{\mathsf{Loc}}(\sigma,y)&\text{if }s=\text{``}x:=y\text{''}\text{ and }u=x\\ e_{i-1}&\text{if }s=\text{``}\textbf{alloc}(x)\text{''},i=\mathsf{allocations}(\sigma)\\ &\text{ and }u=x\\ \mathsf{Flds}\mathsf{Val}^{\mathcal{M}}_{\mathsf{Loc}}(\sigma,p)(\mathsf{Val}^{\mathcal{M}}_{\mathsf{Loc}}(\sigma,y))&\text{if }s=\text{``}x:=y{\cdot}p\text{''}\text{ and }u=x\\ \mathsf{Val}^{\mathcal{M}}_{\mathsf{Loc}}(\sigma,u)&\text{otherwise}\end{cases}\end{array}$$

$$\displaystyle\begin{array}[]{rcl}\mathsf{Val}^{\mathcal{M}}_{\mathsf{Data}}(\varepsilon,v)&=&\mathcal{I}(\widehat{v})\\ \mathsf{Val}^{\mathcal{M}}_{\mathsf{Data}}(\sigma\cdot s,v)&=&\begin{cases}\mathsf{Val}^{\mathcal{M}}_{\mathsf{Data}}(\sigma,b)&\text{if }s=\text{``}a:=b\text{''}\text{ and }v=a\\ \mathcal{I}(f)(\mathsf{Val}^{\mathcal{M}}_{\mathsf{Data}}(\sigma,c_{1}),\ldots,\mathsf{Val}^{\mathcal{M}}_{\mathsf{Data}}(\sigma,c_{r}))&\text{if }s=\text{``}a:=f(c_{1},\ldots,c_{r})\text{''}\\ &\text{ and }v=a\\ \mathsf{Flds}\mathsf{Val}^{\mathcal{M}}_{\mathsf{Data}}(\sigma,d)(\mathsf{Val}^{\mathcal{M}}_{\mathsf{Loc}}(\sigma,y))&\text{if }s=\text{``}a:=y{\cdot}d\text{''}\text{ and }v=a\\ \mathsf{Val}^{\mathcal{M}}_{\mathsf{Data}}(\sigma,v)&\text{otherwise}\end{cases}\end{array}$$

$$\displaystyle\begin{array}[]{rcl}\mathsf{Flds}\mathsf{Val}^{\mathcal{M}}_{\mathsf{Loc}}(\varepsilon,p)&=&\mathcal{I}(\widehat{p})\\ \mathsf{Flds}\mathsf{Val}^{\mathcal{M}}_{\mathsf{Loc}}(\sigma\cdot s,p)&=&\begin{cases}\mathsf{Flds}\mathsf{Val}^{\mathcal{M}}_{\mathsf{Loc}}(\sigma,q)[\mathsf{Val}^{\mathcal{M}}_{\mathsf{Loc}}(\sigma,y)\mapsto\mathsf{Val}^{\mathcal{M}}_{\mathsf{Loc}}(\sigma,x)]&\text{ if }s=\text{``}y{\cdot}q:=x\text{''}\\ &\text{ and }p=q\\ \mathsf{Flds}\mathsf{Val}^{\mathcal{M}}_{\mathsf{Loc}}(\sigma,p)&\text{otherwise}\end{cases}\end{array}$$

$$\displaystyle\begin{array}[]{rcl}\mathsf{Flds}\mathsf{Val}^{\mathcal{M}}_{\mathsf{Data}}(\varepsilon,d)&=&\mathcal{I}(\widehat{d})\\ \mathsf{Flds}\mathsf{Val}^{\mathcal{M}}_{\mathsf{Data}}(\sigma\cdot s,d)&=&\begin{cases}\mathsf{Flds}\mathsf{Val}^{\mathcal{M}}_{\mathsf{Data}}(\sigma,h)[\mathsf{Val}^{\mathcal{M}}_{\mathsf{Loc}}(\sigma,y)\mapsto\mathsf{Val}^{\mathcal{M}}_{\mathsf{Data}}(\sigma,a)]&\text{ if }s=\text{``}y{\cdot}h:=a\text{''}\\ &\text{ and }d=h\\ \mathsf{Flds}\mathsf{Val}^{\mathcal{M}}_{\mathsf{Data}}(\sigma,d)&\text{otherwise}\end{cases}\end{array}$$

$${\pi }_1\stackrel{\Delta }{=}{\text{z}}_1:=\text{x}\cdot \text{next}\cdot \text{assume}({\text{z}}_1\ne {\text{z}}_2)\cdot \text{y}\cdot \text{next}:={\text{z}}_2\cdot {\text{z}}_3:=\text{x}\cdot \text{next}$$

$${\pi }_2\stackrel{\Delta }{=}{\pi }_1\cdot \text{assume}({\text{z}}_2={\text{z}}_3){\pi }_3\stackrel{\Delta }{=}{\pi }_1\cdot \text{assume}({\text{z}}_2\ne {\text{z}}_3)$$

$${\pi }_4^{\prime }\stackrel{\Delta }{=}$$

$$\cdot {\text{z}}_3:=\text{x}\cdot \text{next}\cdot {\text{k}}_1:=\text{x}\cdot \text{key}\cdot {\text{k}}_2:=\text{y}\cdot \text{key}\cdot \underset{n}{\underbrace{{\text{k}}_1:=\text{f}({\text{k}}_1)\cdot {\text{k}}_2:=\text{f}({\text{k}}_2)\cdots {\text{k}}_1:=\text{f}({\text{k}}_1)\cdot {\text{k}}_2:=\text{f}({\text{k}}_2)}}$$

$$\cdot \text{assume}({\text{z}}_2={\text{z}}_3)\cdot \text{assume}({\text{k}}_1={\text{k}}_2)$$

$$\displaystyle\begin{array}[]{rcl}\textsf{Comp}(\varepsilon,u)&=&\widehat{u}\\ \textsf{Comp}(\sigma\cdot s,u)&=&\begin{cases}\textsf{Comp}(\sigma,y)&\text{if }s=\text{``}x:=y\text{''}\text{ and }u=x\\ \mathsf{f}_{\mathsf{dynamic}}^{i}(\mathsf{c}_{\mathsf{dynamic}})&\begin{aligned} &\text{if }s=\text{``}\textbf{alloc}(x)\text{''},\\ &i=\mathsf{allocations}(\sigma),\text{ and }u=x\end{aligned}\\ \mathsf{Flds}\textsf{Comp}(\sigma,h,y)&\text{if }s=\text{``}x:=y{\cdot}h\text{''}\text{ and }u=x\\ f(\textsf{Comp}(\sigma,z_{1}),\ldots,\textsf{Comp}(\sigma,z_{r}))&\text{if }s=\text{``}x:=f(z_{1},\ldots,z_{r})\text{''}\text{ and }u=x\\ \textsf{Comp}(\sigma,u)&\text{otherwise}\end{cases}\end{array}$$

$$\displaystyle\begin{array}[]{rcl}\mathsf{Flds}\textsf{Comp}(\varepsilon,h,z)&=&\widehat{h}(\widehat{z})\\ \mathsf{Flds}\textsf{Comp}(\sigma\cdot s,h,z)&=&\begin{cases}\textsf{Comp}(\sigma,x)&\begin{aligned} \begin{array}[]{l}\text{ if }s=\text{``}y{\cdot}h:=x\text{''}\\ \text{ and }\textsf{Comp}(\sigma,z)\cong_{\alpha(\sigma)}\textsf{Comp}(\sigma,y)\end{array}\end{aligned}\\ \mathsf{Flds}\textsf{Comp}(\sigma,h,z)&\text{otherwise}\end{cases}\end{array}$$

$$\displaystyle\begin{array}[]{rcl}\alpha(\varepsilon)&=&\varnothing\\ \alpha(\sigma\cdot s)&=&\begin{cases}\alpha(\sigma)\cup\{(\textsf{Comp}(\sigma,x),\textsf{Comp}(\sigma,y))\}&\text{if }s=\text{``}\textbf{assume}(x=y)\text{''}\\ \alpha(\sigma)&\text{otherwise}\end{cases}\end{array}$$

$${\pi }_5\stackrel{\Delta }{=}\text{assume}(\text{x}=\text{y})\cdot \text{x}\cdot \text{p}:={\text{z}}_1\cdot {\text{z}}_2:=\text{y}\cdot \text{p}\cdot \text{assume}({\text{z}}_1\ne {\text{z}}_2)$$

$${\pi }_6\stackrel{\Delta }{=}\text{x}\cdot \text{p}:={\text{z}}_1\cdot {\text{z}}_2:=\text{y}\cdot \text{p}\cdot \text{assume}(\text{x}=\text{y})\cdot \text{assume}({\text{z}}_1\ne {\text{z}}_2)$$

$${\pi }_7\stackrel{\Delta }{=}\text{u}:=\text{f(w)}\cdot \underset{n}{\underbrace{\text{u}:=\text{f(u)}\cdots \text{u}:=\text{f(u)}}}\cdot \text{v}:=\text{f(w)}\cdot \underset{n}{\underbrace{\text{v}:=\text{f(v)}\cdots \text{v}:=\text{f(v)}}}\cdot \text{assume}(\text{u}\ne \text{v})$$

$${\pi }_8\stackrel{\Delta }{=}\text{u}:={\text{u}}_0\cdot \stackrel{n}{\overbrace{\text{u}:=\text{f(u)}\cdots \text{u}:=\text{f(u)}}}\cdot \text{v}:={\text{v}}_0\cdot \stackrel{n}{\overbrace{\text{v}:=\text{f(v)}\cdots \text{v}:=\text{f(v)}}}$$

$$\cdot \text{assume}(\text{u}\ne \text{v})$$

$$⟨stmt{⟩}_{\text{assert}}::=$$

$$\displaystyle\begin{array}[]{rcl}\mathsf{Alloc}(\varepsilon)&=&\mathsf{Reach}_{\varphi}\\ \mathsf{Alloc}(\sigma\cdot s)&=&\begin{cases}\mathsf{Alloc}(\sigma)\cup\{\mathsf{Val}^{\mathcal{M}}_{\mathsf{Loc}}(\sigma\cdot s,x)\}&\text{ if }s=\text{``}\textbf{alloc}(x)\text{''}\\ \mathsf{Alloc}(\sigma)\setminus\{\mathsf{Val}^{\mathcal{M}}_{\mathsf{Loc}}(\sigma,x)\}&\text{ if }s=\text{``}\textbf{free}(x)\text{''}\\ \mathsf{Alloc}(\sigma)&\text{otherwise}\end{cases}\end{array}$$

$${\pi }_2^{\prime }\stackrel{\Delta }{=}\text{assume}(\text{x}\ne \mathtt{NIL})\cdot \text{assume}(\text{y}\ne \mathtt{NIL})\cdot {\text{z}}_1:=\text{x}\cdot \text{next}\cdot \text{assume}({\text{z}}_1\ne {\text{z}}_2)\cdot \text{y}\cdot \text{next}:={\text{z}}_2\cdot$$

$${\text{z}}_3:=\text{x}\cdot \text{next}$$

$$(t_i,t_j)\in {\mathsf{Closure}}^{=}(\phi ,E)⟹\{(t_i,{\mathsf{stop}}_i),(t_j,{\mathsf{stop}}_j)\}\subseteq {\mathsf{Closure}}^{=}(\phi ,E)$$

$$P^{\prime }(f)([u_1{]}_{{\equiv }^{\prime }},\dots ,[u_r{]}_{{\equiv }^{\prime }})=\{\begin{array}{ll}[a{]}_{{\equiv }^{\prime }}& \text{if for every 1≤i≤r},[u_i{]}_{\equiv }=[c_i{]}_{\equiv }\text{ and }a\ne u_i\\ [u{]}_{{\equiv }^{\prime }}& \begin{array}{rl}& \text{otherwise if }a\notin \{u,u_1,\dots ,u_r\}\\ & \text{and }[u{]}_{\equiv }=P(f)([u_1{]}_{\equiv },\dots ,[u_r{]}_{\equiv })\end{array}\\ \mathsf{undef}& \text{otherwise}\end{array}$$

Full text

Memory Safety, Program Verification, Aliasing, Decidability, Uninterpreted Programs, Streaming-Coherence, Forest Data-Structures

††copyright: rightsretained††doi: 10.1145/3371103††journalyear: 2020††journal: PACMPL††journalvolume: 4††journalnumber: POPL††article: 35††publicationmonth: 1††ccs: Theory of computation Logic and verification††ccs: Theory of computation Automated reasoning

1. Introduction

The problem of automatic (safety) verification is to ascertain whether a program satisfies its assertions on all inputs and on all executions. The standard technique for proving programs correct involves writing inductive invariants in terms of loop invariants and pre/post conditions, and proving the resulting verification conditions valid (Floyd, 1967; Hoare, 1969). While there has been tremendous progress in identifying decidable fragments for checking validity of verification conditions (Nelson-Oppen combinations of decidable theories realized by efficient SMT solvers (Bradley and Manna, 2007)), decidable program verification without annotations has been elusive. Apart from programs over finite domains, very few natural decidable classes are known.

In a recent paper (Mathur et al., 2019a), a class of uninterpreted programs was identified and shown to have a decidable verification problem. Uninterpreted programs work over arbitrary data domains; the domains give meaning to the constants, relations, and functions in the program, interpreting equality using its natural definition. A program is deemed correct only if it satisfies its assertions in all executions and for all data domains. The authors show that for a class of programs that satisfies a coherence condition, verification is decidable. The decision procedure relies on a streaming congruence closure algorithm realized as automata. The results of (Mathur et al., 2019a) are, however, purely theoretical; there are no general application domains identified where uninterpreted program verification would be useful, nor is there any implementation.

The goal of this paper is to study completely automated verification for heap-manipulating programs. When modeling the heap, we can treat pointers as unary uninterpreted functions; this is a natural modeling choice that does not involve any abstraction (as pointer fields are really arbitrary, unary functions). Thus, it is reasonable to hope that uninterpreted program verification techniques could be useful in this setting.

However, there is a fundamental challenge that we need to overcome: heap-manipulating programs modify heap pointers. With pointers modeled as functions, these programs modify functions/maps. It turns out that the theory of uninterpreted program verification developed in (Mathur et al., 2019a) is severely inadequate for tackling programs that modify maps.

In this paper, we undertake a fundamental study of verification for programs that have updatable maps/functions. We then apply this theory to show that checking memory safety of heap-manipulating programs (where one is given a recursively-described set of allocated locations and asked to check whether a program only dereferences locations that are within this set) is decidable for a subclass of programs, and evaluate the algorithms with an implementation and experiments.

1.1. Alias Awareness and the Notion of Congruence for Programs with Updatable Maps

We can think of uninterpreted programs as computating terms using the function and constants symbols appearing in the code—in the beginning, each variable stores a constant, and after executing an assignment statement of the form $\text{``}x:=f(y)\text{''}$, the term stored in $x$ is $f(t_{y})$, where $t_{y}$ is the term stored in $y$ before executing this statement. As the program executes, in addition to computing terms, it places equality and disequality constraints on the terms it computes (inherited from the conditionals in if-then-else and while constructs).

However, when the program updates maps, this fundamental property, that the program computes terms, is destroyed. Consider an example where there are two locations pointed to by variables $x$ and $y$, but we do not know whether $x$ and $y$ point to the same location or not. If we update a pointer-field on $x$ and then read the same pointer-field from $y$ into a variable $k$, we cannot really associate any term with the variable $k$, as the term crucially depends on whether $x$ and $y$ were aliases to the same location or not.

The above is a fundamental problem that wreaks havoc, making program verification essentially impossible in the presence of updatable maps. The notion of coherence in (Mathur et al., 2019a) fails, as it crucially relies on this notion of terms. And it cannot be repaired, as the semantic meaning of the coherence  condition fundamentally involves not computing the same term multiple times.

The primary observation, which saves the framework, is to note that the entire problem is due to not knowing aliasing relationships. We call a program execution *alias-aware * if, at every point where it updates a function on the element pointed to by a program variable $x$, the precise aliasing relationship between $x$ and all other program variables in scope is determined. More precisely, when the execution modifies a function/pointer-field of $x$, for every other program variable $z$, it must either be the case that $x$ is different from $z$ in any data-model/heap or it must be the case that $x$ is equal to $z$ in all data-models/heaps.

We show that alias-awareness is a panacea for our problems. For alias-aware  programs (programs whose executions are all alias-aware), we show we can associate terms with variables after a computation that updates maps, and further show that the notion of coherence  extends naturally to programs that update maps. We then show that for coherent alias-aware  programs, the verification problem becomes decidable. These results constitute the first main contribution of the paper.

1.2. Application to Verifying Memory Safety

We then study the application of our framework to verifying memory safety. Our key observation is that for programs that manipulate forest data-structures (data-structures consisting of disjoint tree-like structures), programs are naturally alias-aware. Intuitively, when traversing forest data-structures, aliasing information is implicitly present. For instance, if x points to a location of a forest data-structure, we know that the location pointed to by x, the one pointed to by the left child $\texttt{x}{\cdot}\texttt{left}$, and the one pointed to by the right child $\texttt{x}{\cdot}\texttt{right}$ are all different.

In this paper, we define memory safety as follows. A heap-manipulating program starts with a set of allocated heap locations. During its execution, it dereferences pointers on heap locations, and allocates and frees locations. A program is memory safe if it never dereferences a location that is not in the allocated set. The above definition of memory safety captures the usual categories of memory safety errors such as null-pointer dereferences, use after free, use of uninitialized memory, illegal freeing of memory, etc. (Hicks, 2014). However, in this paper, we do not consider allocation of contiguous blocks of arbitrary size of memory (and hence do not handle arrays and buffer overflows of arrays in languages like C, etc.). Rather, we assume that allocation is done in terms of records of fixed size (like structs in C), and we disallow pointer arithmetic in our programs.

Our second main contribution of the paper is a technical result that gives an efficient decision procedure for verifying memory safety for a subclass of imperative heap-manipulating programs, whose *initial * allocated heaps are restricted to forest data-structures.

Handling forest data-structures, i.e., disjoint lists and trees, is useful as they are ubiquitous. Note that we require only the initial heaps to be forest data-structures; the program can execute for an arbitrarily long time and create cycles/merges as it manipulates the structures. We model the primitive types and operations on them using uninterpreted functions and relations, similar in spirit to the way the work in  (Mathur et al., 2019a) handles all data. The key insight here is that this is a reasonable modeling choice, since programs typically do not rely on the semantics of the primitive data domains in order to assure memory safety (we also show this empirically in experiments). The salient aspect of our work is that we model the pointers in the heap precisely using updatable maps, without resorting to any abstraction (classical automatic analysis of heap programs typically uses abstractions for heaps; for instance, shape analysis involves an abstraction of the heap locations to a finite abstract domain (Sagiv et al., 1999)).

We allow the user to specify the initial allocated set as the (unbounded) set of locations reachable from various locations (pointed to by certain program variables) using particular pointer fields, until a specific set of locations is reached. The memory safety problem is then to check whether such a program, starting from an arbitrary heap storing a forest data-structure, an arbitrary model for the primitive types, and with the specified allocated set, dereferences only those locations that are in the (potentially changing) allocated set, on all executions.

The above problem turns out to be undecidable (a direct consequence from (Mathur et al., 2019a), as even programs that do not manipulate heaps and have simple equality assertions yield undecidability). The main result of the paper is that for a class of programs called streaming-coherent programs, memory safety is decidable. Intuitively, these correspond to programs that traverse the forest data-structures in a single-pass.

Technical Challenges.

The primary challenge is dealing with updatable pointers and updatable sets (the latter are needed to model the set of allocated locations, which changes during program execution). As we show in our first set of results, it is crucial for a program to be alias aware. The fact that our initial data-structures are forests implicitly causes streaming-coherent programs to be alias aware. When two variables point to locations obtained using different traversals, we know they cannot alias to each other. Also, for streaming-coherent programs, we can keep track of whether traversals for any pair of variables are the same, and track their precise aliasing relationships.

The culmination of the ideas above is our result that verification of memory safety for streaming-coherent programs over forest data-structures is decidable, and is $\mathsf{PSPACE}$-complete. It is in fact decidable in time that is linear in the size of the program and exponential in the number of variables. We also show that checking whether a given program is streaming-coherent is decidable in $\mathsf{PSPACE}$. Note that even checking reachability in programs with Boolean domains has this complexity, and hence our algorithms are quite efficient.

Evaluation.

We implement a prototype of our automata-based decision procedure. This involves intersecting an automaton that checks whether a given streaming-coherent  execution is memory-safe with an automaton that represents the given program’s executions. Instead of building these automata and checking emptiness of their intersection, we use an approach that constructs the automaton and the intersection on-the-fly, hence not paying the worst case costs upfront. We evaluate our procedure on a class of standard library functions that manipulate forest data-structures, including linked lists and trees, where various other aspects of the data-structures (such as keys, height, etc.) are modeled using an uninterpreted data domain. These are typically single-pass algorithms on such data-structures, that take pointers to forest data-structures as input (and may create non-forest data-structures during computation).

Though we have stringent requirements that programs must meet in order to be in the decidable class, we show in our experiments that most natural single-pass programs on forest data-structures meet our requirements. We also show that our tool is able to check if the program falls in the decidable class, and both verify memory safety and find memory safety errors extremely efficiently.

We emphasize that the novelty of our approach is in building decision procedures for verifying memory safety without the aid of human-given loop invariants, and without abstracting the heap domain (the data domain is, however, abstracted using uninterpreted functions). In contrast, there are several existing techniques that can prove memory safety when given manually written loop invariants or prove memory safety by abstracting the heap (which can lead to false positives). Our results hence carve out new ground in memory safety verification and our experiments show that our approach holds promise for wider applicability and scalability.

In summary, this paper makes the following contributions:

• •

A notion of alias-aware  coherent programs (Section 3), and a result that shows that the assertion-checking problem for such programs is decidable and $\mathsf{PSPACE}$-complete (Section 4).

• •

A notion of streaming-coherence  and forest data-structures ( Section 5) with an efficient decision procedure for verifying memory safety for the class of streaming-coherent programs that dynamically manipulate forest data-structures (Section 6).

• •

An efficient decision procedure determining if programs are streaming-coherent  (Section 6).

• •

An experimental evaluation ( Section 7) showing (a) common library routines that manipulate forest data-structures using single-pass traversals are often streaming-coherent, and (b) that the decision procedures presented in this paper (for checking whether programs satisfy the streaming-coherent requirement and for checking whether streaming-coherent programs are memory safe) are very efficient, both for proving programs correct and finding errors in incorrect programs.

2. Preliminaries

In this section, we define the syntax and semantics of programs that manipulate heaps and other relevant concepts useful for presenting the main results of the paper. These are fairly standard and familiar readers may skip the details.

2.1. Syntax of Heap-Manipulating Programs

The programs we consider are those that manipulate heaps. It is convenient to abstract heap structures as consisting of two sorts of distinct elements — a sort $\mathsf{Loc}$ of memory locations in the heap, and a sort $\mathsf{Data}$ of data values. Field (or map) symbols will model pointers from memory locations to memory locations or data values. Constants and functions over the data domain will be used to construct other data values. In this paper, we will not assume any fixed interpretation for either data values or for functions on data values. In this sense, our programs work over an uninterpreted data domain. Predicates over data values will be modeled by functions capturing the characteristic function of the predicate.

Let $\mathsf{Loc}$ and $\mathsf{Data}$ be the sorts of locations and data respectively. Our vocabulary $\Sigma$ is a tuple of the form $(\mathcal{C}_{\mathsf{Loc}},\mathcal{F}_{\mathsf{Loc}},\mathcal{C}_{\mathsf{Data}},\mathcal{F}_{\mathsf{Data}},\mathcal{F}_{\mathsf{Loc}\to\mathsf{Data}})$, where

• •

$\mathcal{C}_{\mathsf{Loc}}$ is a set of location constant symbols of sort $\mathsf{Loc}$,

• •

$\mathcal{F}_{\mathsf{Loc}}$ is a set of unary location function symbols with sort ‘$\mathsf{Loc},\mathsf{Loc}$’ 111We will use the notation $\sigma,\tau$ to indicate a function whose arguments are from sort $\sigma$ and which returns a value in sort $\tau$. Thus for example ‘$\mathsf{Loc},\mathsf{Loc}$’ is a function with one argument of sort $\mathsf{Loc}$ and which returns an element of sort $\mathsf{Loc}$. On the other hand, ‘$\mathsf{Data}^{r},\mathsf{Data}$’ denotes functions with $r$ arguments each of sort $\mathsf{Data}$ and which returns an element of sort $\mathsf{Data}$., that models pointers between heap locations,

• •

$\mathcal{C}_{\mathsf{Data}}$ denotes the set of data constant symbols of sort $\mathsf{Data}$,

• •

$\mathcal{F}_{\mathsf{Data}}=\bigcup\limits_{i\geq 0}F_{i}$ where $F_{r}$ is a set of data function symbols of arity $r$ and sort ‘$\mathsf{Data}^{r},\mathsf{Data}$’, and

• •

$\mathcal{F}_{\mathsf{Loc}\to\mathsf{Data}}$ is a set of unary location function symbols with sort ‘$\mathsf{Loc},\mathsf{Data}$’, modeling pointers to data values stored in heap locations.

2.1.1. Program Syntax

Programs will use a finite set of variables to store information — heap locations and data values — during a computation. Let us fix $V_{\mathsf{Loc}}=\{u_{1},\ldots,u_{l}\}$ as the set of location variables and $V_{\mathsf{Data}}=\{v_{1},\ldots,v_{m}\}$ as the set of data variables and let $V=V_{\mathsf{Loc}}\uplus V_{\mathsf{Data}}$ 222We use $A\uplus B$ to denote the disjoint union of sets $A$ and $B$. be the set of all variables. In addition, our programs manipulate fields associated with location variables. We will model these fields as second order function variables $\mathsf{Flds}_{\mathsf{Loc}}=\{p_{1},\ldots,p_{r}\}$ (pointers from locations to locations) and $\mathsf{Flds}_{\mathsf{Data}}=\{d_{1},\ldots,d_{s}\}$ (pointers from locations to data), and let $\mathsf{Flds}=\mathsf{Flds}_{\mathsf{Loc}}\cup\mathsf{Flds}_{\mathsf{Data}}$. Taking $x,y\in V_{\mathsf{Loc}}$, $p\in\mathsf{Flds}_{\mathsf{Loc}}$, $d\in\mathsf{Flds}_{\mathsf{Data}}$, $f$ in $\mathcal{F}_{\mathsf{Data}}$, $a,b\in V_{\mathsf{Data}}$, and ${\bf c}$ to be a tuple of variables in $V_{\mathsf{Data}}$, the syntax of programs is given by the following grammar.

[TABLE]

Our programs have well-typed assignments to variables using values stored in other variables ($x:=y$ and $a:=b$) or using pointer dereferences from location variables, either to the data sort ($a:=y{\cdot}d$) or to the location sort ($x:=y{\cdot}p$), or using function computations in the data sort ($a:=f({\bf c})$). Further, programs can update fields ($y{\cdot}d:=a$ or $y{\cdot}p:=x$), and can dynamically allocate ($\textbf{alloc}(x)$) or deallocate ($\textbf{free}(x)$) memory. In addition, they allow the usual constructs of imperative programming — empty statements (skip), conditionals ($\textbf{if}-\textbf{then}-\textbf{else}$) and loops (while). Conditionals in programs can be Boolean combinations of (well-typed) equality atoms over location or data variables.

2.2. Program Executions

Executions of programs over $\Sigma$ and variables $V$ (given by the $\langle stmt\rangle$ grammar) are finite sequences over the alphabet $\Pi$ given below.

[TABLE]

The set of executions of a program $P$, denoted $\textsf{Exec}(P)$ is given by a regular expression, inductively defined below. We assume that conditionals are in negation normal form where $\text{``}\textbf{assume}(\neg(r=s))\text{''}$ translates to $\text{``}\textbf{assume}(r\neq s)\text{''}$ and $\text{``}\textbf{assume}(\neg(r\neq s))\text{''}$ translates to $\text{``}\textbf{assume}(r=s)\text{''}$.

[TABLE]

The set of partial executions of a program $P$, denoted $\textsf{PExec}(P)$, is the set of prefixes of its executions.

2.3. Semantics of Executions

The semantics of a heap-manipulating program is given in terms of the behavior of its executions on heap structures.

2.3.1. Heap Structures

A $\Sigma$-heap structure is a tuple $\mathcal{M}=(U_{\mathsf{Loc}},U_{\mathsf{Data}},\mathcal{I})$, where $U_{\mathsf{Loc}}$ is a universe of locations, $U_{\mathsf{Data}}$ is a universe of data ($U_{\mathsf{Loc}}\cap U_{\mathsf{Data}}=\varnothing$) and $\mathcal{I}$ is some interpretation of the various symbols in $\Sigma$. In order to faithfully model dynamic memory allocation, we assume that the set of locations is the disjoint union of a statically allocated set of locations and a countably infinite set of locations that can be allocated dynamically. That is, we have $U_{\mathsf{Loc}}=U^{\mathsf{static}}_{\mathsf{Loc}}\uplus U^{\mathsf{dynamic}}_{\mathsf{Loc}}$, where $U^{\mathsf{dynamic}}_{\mathsf{Loc}}=\{e_{0},e_{1},\ldots\}$ is an ordered set of distinguished locations indexed by the set of natural numbers $\mathbb{N}$. The interpretation $\mathcal{I}$ maps every constant $c\in\mathcal{C}_{\mathsf{Loc}}$ to an element from $U^{\mathsf{static}}_{\mathsf{Loc}}$, every constant in $\mathcal{C}_{\mathsf{Data}}$ to an element from $U_{\mathsf{Data}}$, every function symbol $f\in\mathcal{F}_{\mathsf{Loc}}$ to an element of $[U_{\mathsf{Loc}}\to U_{\mathsf{Loc}}]$, symbol $f\in\mathcal{F}_{\mathsf{Data}}$ of arity $r$ to an element of $[(U_{\mathsf{Data}})^{r}\to U_{\mathsf{Data}}]$, and, $f\in\mathcal{F}_{\mathsf{Loc}\to\mathsf{Data}}$ to an element of $[U_{\mathsf{Loc}}\to U_{\mathsf{Data}}]$. Further, we assume that the elements in $U^{\mathsf{dynamic}}_{\mathsf{Loc}}$ cannot be accessed from $U^{\mathsf{static}}_{\mathsf{Loc}}$, i.e., for every $f\in\mathcal{F}_{\mathsf{Loc}}$, we have $\forall e\in U^{\mathsf{static}}_{\mathsf{Loc}},\mathcal{I}(f)(e)\in U^{\mathsf{static}}_{\mathsf{Loc}}$. This ensures that the set of locations reachable by any execution cannot access locations in the dynamic universe that have not been allocated by the execution. Moreover, for every $f\in\mathcal{F}_{\mathsf{Loc}}$ and every $e\in U^{\mathsf{dynamic}}_{\mathsf{Loc}}$, we have $f(e)=e$. Finally, we assume in $\Sigma$ the presence of a distinguished constant symbol $\mathsf{c}_{\mathsf{dynamic}}$ and a distinguished function symbol $\mathsf{f}_{\mathsf{dynamic}}$ not used in the syntax $\langle stmt\rangle$ of programs. We require that for every heap structure $\mathcal{M}=(U^{\mathsf{static}}_{\mathsf{Loc}}\uplus U^{\mathsf{dynamic}}_{\mathsf{Loc}},U_{\mathsf{Data}},\mathcal{I})$ the interpretation function $\mathcal{I}$ of $\mathcal{M}$ assigns interpretations to these symbols such that $\mathcal{I}(\mathsf{c}_{\mathsf{dynamic}})=e_{0}$ and $\mathcal{I}(\mathsf{f}_{\mathsf{dynamic}})\in[U^{\mathsf{dynamic}}_{\mathsf{Loc}}\to U^{\mathsf{dynamic}}_{\mathsf{Loc}}]$ with $\mathcal{I}(\mathsf{f}_{\mathsf{dynamic}})(e_{i})=e_{i+1}$ for every $i\in\mathbb{N}$.

2.3.2. Valuation of Variables and Pointers in an Execution.

We assume that corresponding to each program variable $x\in V$, there is a distinguished constant $\widehat{x}\in\mathcal{C}_{\mathsf{Loc}}\uplus\mathcal{C}_{\mathsf{Data}}$ of the appropriate sort denoting the initial value of $x$. Likewise, each field $p\in\mathsf{Flds}_{\mathsf{Loc}}$ (resp. $d\in\mathsf{Flds}_{\mathsf{Data}}$) is also associated with a unary function $\widehat{p}\in\mathcal{F}_{\mathsf{Loc}}$ (resp. $\widehat{d}\in\mathcal{F}_{\mathsf{Loc}\to\mathsf{Data}}$).

Given an execution $\sigma\in\Pi^{*}$ of a program $P\in\langle stmt\rangle$ and a $\Sigma$-heap structure $\mathcal{M}=(U_{\mathsf{Loc}},U_{\mathsf{Data}},\mathcal{I})$, the valuation of the program variables and field pointers at the end of $\sigma$ are defined in terms of valuation functions $\mathsf{Val}^{\mathcal{M}}_{\mathsf{Loc}}:\Pi^{*}\times V_{\mathsf{Loc}}\to U_{\mathsf{Loc}}$, $\mathsf{Val}^{\mathcal{M}}_{\mathsf{Data}}:\Pi^{*}\times V_{\mathsf{Data}}\to U_{\mathsf{Data}}$, $\mathsf{Flds}\mathsf{Val}^{\mathcal{M}}_{\mathsf{Loc}}:\Pi^{*}\times\mathsf{Flds}_{\mathsf{Loc}}\to[U_{\mathsf{Loc}}\to U_{\mathsf{Loc}}]$ and $\mathsf{Flds}\mathsf{Val}^{\mathcal{M}}_{\mathsf{Data}}:\Pi^{*}\times\mathsf{Flds}_{\mathsf{Data}}\to[U_{\mathsf{Loc}}\to U_{\mathsf{Data}}]$, which are presented next. In the following, $\mathsf{allocations}(\sigma)$ denotes the number of occurrences of statements of the form $\text{``}\textbf{alloc}(\cdot)\text{''}$ in $\sigma$.

[TABLE]

[TABLE]

[TABLE]

[TABLE]

where by $f[a\mapsto b]$ we mean the function $g$ defined as $g(a)=b$ and $g(x)=f(x)$ otherwise.

Feasibility.

An execution $\sigma$ is said to be feasible on $\mathcal{M}$ if for every prefix of $\sigma$ of the form $\rho^{\prime}\cdot\text{``}\textbf{assume}(x=y)\text{''}$, we have $\mathsf{Val}^{\mathcal{M}}_{\mathsf{sort}}(\rho^{\prime},x)=\mathsf{Val}^{\mathcal{M}}_{\mathsf{sort}}(\rho^{\prime},y)$, and for every prefix of $\sigma$ of the form $\rho^{\prime}\cdot\text{``}\textbf{assume}(x\neq y)\text{''}$, we have $\mathsf{Val}^{\mathcal{M}}_{\mathsf{sort}}(\rho^{\prime},x)\neq\mathsf{Val}^{\mathcal{M}}_{\mathsf{sort}}(\rho^{\prime},y)$, where $\mathsf{sort}\in\{\mathsf{Loc},\mathsf{Data}\}$ is the sort of both $x$ and $y$.

3. Defining Coherence  For Heap-Manipulating Programs

In this section we discuss some of the challenges involved in coming up with a reasonable extension for the notion of coherence  as defined in (Mathur et al., 2019a). A key problem in defining such an extension, and indeed in generally handling programs with updatable maps, lies in keeping accurate track of aliasing between variables of the location sort. We will first discuss some examples that highlight these challenges and proffer a first solution to the problem. Then we will discuss our solution more formally by introducing relevant notation and define our notion of alias-aware  executions and programs that captures the essence of the aliasing problem. Finally, we will discuss the notion of coherence  adapted to the case of heap-manipulating programs.

3.1. The Importance of Being Alias Aware for Programs Updating Maps

Functions and updatable maps cannot be handled uniformly; in particular, the work of (Mathur et al., 2019a) does not immediately lend itself to handling updatable maps. Let us illustrate this using the following example.

Example 0.

Consider a straight-line program that generates execution $\pi_{1}$, where

[TABLE]

In the execution above we do not, and in fact cannot, know the value stored in the variable $\texttt{z}_{3}$ unless we know whether $\texttt{x}=\texttt{y}$ or $\texttt{x}\neq\texttt{y}$. In the former case, we will have that $\texttt{z}_{3}=\texttt{z}_{2}$, since y aliases x and, therefore, the update of the next pointer on y will have over-written the value of the pointer on x. Similarly, in the latter case we will have that $\texttt{z}_{3}=\texttt{z}_{1}$, since the pointer update on y will have no effect on x.

This is a major difference, since in any heap structure on which $\pi_{1}$ is feasible, it must be that $\texttt{z}_{1}\neq\texttt{z}_{2}$. Therefore, whether x and y are aliases of each other can have a drastic effect on the semantics and feasibility of the execution.

The above example illustrates that aliasing plays a crucial role in the semantics and feasibility of executions. There is, however, a second (related) issue as well.

Example 0.

Consider the executions $\pi_{2}$ and $\pi_{3}$ where

[TABLE]

As discussed earlier, execution $\pi_{2}$ is only feasible in models where $\texttt{x}=\texttt{y}$ and $\pi_{3}$ only in models where $\texttt{x}\neq\texttt{y}$ where at the end of $\pi_{1}$ both kinds of models were feasible. Therefore one can have implied equalities and disequalities between variables that are only known much later in the execution. In general, this is hard to keep track of in a streaming setting (which we wish to do in order to use the underlying ideas in (Mathur et al., 2019a)) and can require an unbounded amount of memory, as can be seen in the following example.

Example 0.

Consider the following execution

[TABLE]

The above execution is feasible, but would require an unbounded amount of memory to reason as such in a streaming fashion. Next we will see a solution to this aliasing problem that will allow us to keep track of relationships between variables and the correct semantics of an execution.

3.2. Alias-Aware Executions and Programs

In Section 3.1, we saw that unlike the work of (Mathur et al., 2019a) we cannot define what term (or value) is computed by a variable. We also observed that the main issue with programs that have updatable maps is aliasing — i.e., when a pointer or data field is updated on a variable, the update may also be true for a different variable that aliases the original variable. In this section we identify a class of executions, called alias-aware executions, which implicitly resolves any aliasing when updating the pointer fields on heap locations.

Below, we formally define alias-aware executions. We denote by $\textsf{Heaps}(\sigma)$ the set of heap structures on which the execution $\sigma$ is feasible.

Definition 0.

Let $\rho\in\Pi^{*}$ be an execution. $\rho$ is said to be alias-aware if for every prefix of $\rho$ of the form $\sigma\cdot\text{``}x{\cdot}h:=u\text{''}$ (the sorts of $u$ and $h$ are compatible), and for every location variable $y\in V_{\mathsf{Loc}}$, one of the following hold

• •

For every heap structure $\mathcal{M}=(U_{\mathsf{Loc}},U_{\mathsf{Data}},\mathcal{I})\in\textsf{Heaps}(\sigma)$, $\mathsf{Val}^{\mathcal{M}}_{\mathsf{Loc}}(\sigma,x)=\mathsf{Val}^{\mathcal{M}}_{\mathsf{Loc}}(\sigma,y)$.

• •

For every heap structure $\mathcal{M}=(U_{\mathsf{Loc}},U_{\mathsf{Data}},\mathcal{I})\in\textsf{Heaps}(\sigma)$, $\mathsf{Val}^{\mathcal{M}}_{\mathsf{Loc}}(\sigma,x)\neq\mathsf{Val}^{\mathcal{M}}_{\mathsf{Loc}}(\sigma,y)$.

Intuitively, the above definition says that for an alias-aware  execution, at a map update we know all the relevant aliasing information (even in the uninterpreted sense), because the variables that alias to the variable on which the update is being performed are the same in every feasible model.

Definition 0 (Alias-Aware  programs).

A program $s\in\langle stmt\rangle$ is said to be alias-aware  if every execution $\rho\in\textsf{Exec}(s)$ is alias-aware.

3.3. Term Computed by a Variable during an Execution

Before we define coherence in our setting, we require the notion of terms that an execution computes. The notion of terms lets us reason about infinitely many heap structures in a symbolic fashion and was crucially exploited in (Mathur et al., 2019a) to define coherence and in arguing the correctness of the decision procedure designed for coherent programs.

We would like to define the term associated with a program variable in an execution. There are two major challenges in our way. The first challenge is that, in order to accurately determine the value pointed to by a variable during an execution on a concrete heap structure, one needs to accurately keep track of the interpretations of pointer fields (that could have, in turn, been updated earlier in the execution). A similar problem needs to be addressed in order to successfully define the notion of terms. The second challenge is that unlike in concrete heap structures where two distinct elements in the heap are known to be unequal, terms do not behave the same way. For the case of terms, we would like to explore the possibility that two terms that might be syntactically different might still be semantically equivalent. While this subtlety can be dealt with easily when none of the functions are updatable, as in (Mathur et al., 2019a), greater care is required in our setting. Let us first formalize some notation and then elaborate these subtleties.

For a set $\mathcal{C}$ of constant symbols and a set $\mathcal{F}$ of function symbols from $\Sigma$, we use $\textsf{Terms}(\mathcal{C},\mathcal{F})$ (or just Terms when the signature is clear) to denote the set of (well-sorted) ground terms constructed using the constants in $\mathcal{C}$ and function symbols in $\mathcal{F}$.

For a binary relation $R\subseteq\textsf{Terms}\times\textsf{Terms}$, the congruence closure of $R$, denoted $\cong_{R}$ is the smallest equivalence relation such that (i) $R\subseteq\cong_{R}$, and (ii) for every function $f$ of sort $w_{1}w_{2}\cdots w_{r},w$ ($w,w_{i}\in\{\mathsf{Loc},\mathsf{Data}\}$) and terms $t_{1},t^{\prime}_{1},t_{2},t^{\prime}_{2},\ldots,t_{r},t^{\prime}_{r}$ of sorts $w_{1},w_{1},w_{2},w_{2},\ldots,w_{r},w_{r}$, we have \Big{(}\bigwedge\limits_{i=1}^{r}(t_{i},t^{\prime}_{i})\in\cong_{R}\Big{)}{\implies}(f(t_{1},\ldots,t_{r}),f(t^{\prime}_{1},\ldots,t^{\prime}_{r}))\in\cong_{R}. We say $t_{1}\cong_{R}t_{2}$ if $(t_{1},t_{2})\in\cong_{R}$, where $t_{1},t_{2}$ are terms.

We now define the terms associated with variables $\textsf{Comp}:\Pi^{*}\times V\to\textsf{Terms}$, the interpretations of updatable maps on terms corresponding to variables $\mathsf{Flds}\textsf{Comp}:\Pi^{*}\times\mathsf{Flds}\times V\to\textsf{Terms}$, and the set of equalities accumulated by the execution $\alpha:\Pi^{*}\to\mathcal{P}(\textsf{Terms}\times\textsf{Terms})$. Recall that, in the following, $\mathsf{c}_{\mathsf{dynamic}}\in\mathcal{C}_{\mathsf{Loc}}$ and $\mathsf{f}_{\mathsf{dynamic}}\in\mathcal{F}_{\mathsf{Loc}}$ are special symbols in our vocabulary.

[TABLE]

[TABLE]

[TABLE]

The set of terms computed by an execution $\sigma$ is the set $\textsf{Terms}(\sigma)=\{\textsf{Comp}(\rho,x)\,\mid\,x\in V,\rho\text{ is a prefix of }\sigma\}$.

Let us discuss some aspects of the above definition here. The effect of some of the commands in the executions is obvious and similar to (Mathur et al., 2019a). At the beginning of an execution, each term $x\in V$ is associated with a unique constant term $\widehat{x}$, each pointer $h$ assigns every term $t$ (of the location sort) to $\widehat{h}(t)$, and the set of equalities accumulated is $\varnothing$. On an assignment $\text{``}x:=y\text{''}$, the term stored in $x$ is updated to be that stored in $y$. On an assignment involving a (non-updatable) function ($x:=f(z_{1},\ldots,z_{r})$), the execution computes the term $f(t_{1},\ldots,t_{r})$, and stores it in $x$, where $t_{i}$ is the term associated with $z_{i}$ before the assignment.

Let us now look at the other commands. Recall that we model our set of dynamically allocated locations as a disjoint set from the set of statically allocated locations. The term associated with $x$ after an $\text{``}\textbf{alloc}(x)\text{''}$ follows this premise. It is built using $n$ applications of a distinct function $\mathsf{f}_{\mathsf{dynamic}}\in\mathcal{F}_{\mathsf{Loc}}$ on a distinct constant $\mathsf{c}_{\mathsf{dynamic}}\in\mathcal{C}_{\mathsf{Loc}}$, where $n$ is the number of allocations performed before this point in the execution. Let us now turn to the most subtle aspect: pointer updates. When the execution encounters a command of the form $\text{``}y{\cdot}h:=x\text{''}$, we need to not only update the term pointed to by $t_{y}{\cdot}h$ (where $t_{y}$ is the term associated with $y$), we also need to update the term pointed to by $t{\cdot}h$, when $t$ can be inferred to be equivalent to $t_{y}$ using the equalities $\alpha(\cdot)$ accumulated so far.

Example 0.

Consider the following execution.

[TABLE]

Here, the terms associated with the pointers $x{\cdot}p$ and $y{\cdot}p$ are $\widehat{p}(\widehat{x})$ and $\widehat{p}(\widehat{y})$ respectively. After the $\text{``}\textbf{assume}(\texttt{x}=\texttt{y})\text{''}$, the locations pointed to by x and y are the same in every heap structure on which this assumption is valid, and thus the terms corresponding to x and y must be deemed equivalent. This means that the pointer update $\texttt{x}{\cdot}\texttt{p}:=\texttt{z}_{1}$ should in fact be reflected in the term associated with the pointer $\texttt{y}{\cdot}\texttt{p}$. The above definition of $\textsf{Comp}(\cdot)$ and $\mathsf{Flds}\textsf{Comp}(\cdot)$ will, in fact, ensure that $\textsf{Comp}(\pi_{5},\texttt{z}_{1})=\textsf{Comp}(\pi_{5},\texttt{z}_{2})$. Not doing so will, in turn, not reflect the contradiction due to the last statement of this execution, which makes it infeasible in every heap structure.

It turns out that the above definition of terms associated with variables is only a best effort, in that, it may not accurately summarize all heap structures in which the execution is feasible. The following example illustrates why this is the case.

Example 0.

Let us consider the following, which is a permutation of the execution in Example 6.

[TABLE]

Similar to the execution in Example 6, the execution $\pi_{6}$ is infeasible in every heap structure. However, in this case, the terms associated with $\texttt{z}_{1}$ and $\texttt{z}_{2}$ will be $\textsf{Comp}(\pi_{6},\texttt{z}_{1})=\widehat{\texttt{z}_{1}}$ and $\textsf{Comp}(\pi_{6},\texttt{z}_{2})=\widehat{\texttt{p}}(\widehat{\texttt{y}})$, which are not equal, even when considering the equivalence induced due to $\alpha(\pi_{6})=\{(\widehat{\texttt{x}},\widehat{\texttt{y}})\}$. As a result, it is hard to conclude that $\pi_{6}$ is an infeasible execution by analyzing the terms associated with variables alone.

However, for the case of an alias-aware execution (Definition 4), the definition of terms above indeed accurately relates the terms associated with each variable to their values in every heap structure that makes the execution feasible. This brings us to the first main result of the paper that motivates the definition of alias-aware executions. It simply states that the interpretation of the terms defined above on a given model coincides with the actual values computed on the model.

Theorem 8**.**

Let $\sigma$ be an alias-aware  execution and let $\mathcal{M}=(U_{\mathsf{Loc}},U_{\mathsf{Data}},\mathcal{I})\in\textsf{Heaps}(\sigma)$ be a heap structure on which $\sigma$ is feasible. Then, $\mathcal{I}(\textsf{Comp}(\sigma,x))=\mathsf{Val}^{\mathcal{M}}_{\mathsf{Loc}}(\sigma,x)$ for every variable $x\in V_{\mathsf{Loc}}$ and $\mathcal{I}(\textsf{Comp}(\sigma,a))=\mathsf{Val}^{\mathcal{M}}_{\mathsf{Data}}(\sigma,a)$ for every $a\in V_{\mathsf{Data}}$.

Moreover, $\mathcal{I}(\mathsf{Flds}\textsf{Comp}(\sigma,h,x))=\mathsf{Flds}\mathsf{Val}^{\mathcal{M}}_{\mathsf{Loc}}(\sigma,h)(\mathsf{Val}^{\mathcal{M}}_{\mathsf{Loc}}(\sigma,x))$ and $\mathcal{I}(\mathsf{Flds}\textsf{Comp}(\sigma,d,x))=\mathsf{Flds}\mathsf{Val}^{\mathcal{M}}_{\mathsf{Data}}(\sigma,d)(\mathsf{Val}^{\mathcal{M}}_{\mathsf{Loc}}(\sigma,x))$ for every $h\in\mathsf{Flds}_{\mathsf{Loc}},d\in\mathsf{Flds}_{\mathsf{Data}}$ and $x\in V_{\mathsf{Loc}}$.

Proof.

The proof proceeds by induction on the length of the execution. The base case and most inductive cases are trivial by the definitions of $\textsf{Comp},\mathsf{Val}^{\mathcal{M}}_{\mathsf{Loc}},\mathsf{Val}^{\mathcal{M}}_{\mathsf{Data}}$, etc. The only nontrivial case is that of map update. Consider an execution of the form $\sigma\cdot\text{``}y{\cdot}h:=x\text{''}$. It is easy to see that definitions of $\mathsf{Flds}\mathsf{Val}^{\mathcal{M}}_{\mathsf{Data}}$ and $\mathsf{Flds}\mathsf{Val}^{\mathcal{M}}_{\mathsf{Loc}}$ update the map on the location pointed to by $y$. However, the definition of Comp updates the appropriate term for the map $h$ only on variables whose terms are equivalent modulo $\alpha(\sigma)$. We simply establish that for alias-aware  executions the equivalence modulo $\alpha(\sigma)$ is sufficient to determine which variables alias $y$. This is owing to the fact that the initial model of terms modulo the congruence closure of $\alpha(\sigma)$ is feasible on $\sigma$. And in that model, the only variables that alias $y$ are those that compute terms equivalent to $\textsf{Comp}(\sigma,y)$ modulo $\alpha(\sigma)$. Since $\sigma$ is alias-aware, we have that in any model the variables that alias to $y$ are the same as those that alias to $y$ in the initial model.

We establish that the initial model of an alias-aware  execution $\sigma$ is a feasible model of $\sigma$, by strong induction on the length of the execution, where we strengthen our inductive hypothesis. We present the stronger inductive hypothesis below, the proof of which is a simple mutual (structural) induction on the execution.

Given an alias-aware  execution $\sigma$ that is feasible (i.e., feasible in some model) and a sub-execution $\rho\leq\sigma$:

• •

$\rho$ is feasible on $\mathcal{M}_{\alpha(\rho)}$, where $\mathcal{M}_{\alpha(\rho)}$ is the initial term modulo the congruence closure of $\alpha(\rho)$.

• •

$\mathsf{Val}^{\mathcal{M}_{\alpha(\rho)}}(\rho,x)=[\textsf{Comp}(\rho,x)]_{\alpha(\rho)}$, where $[]_{\alpha(\rho)}$ represents the equivalence class of terms modulo the congruence defined by $\alpha(\rho)$.

Similarly, $\mathsf{Flds}\mathsf{Val}^{\mathcal{M}_{\alpha(\rho)}}_{\mathsf{Loc}}(\rho,h)(\mathsf{Val}^{\mathcal{M}_{\alpha(\rho)}}_{\mathsf{Loc}}(\rho,x))=[\mathsf{Flds}\textsf{Comp}(\rho,h,x)]_{\alpha(\rho)}$

and $\mathsf{Flds}\mathsf{Val}^{\mathcal{M}_{\alpha(\rho)}}_{\mathsf{Data}}(\rho,d)(\mathsf{Val}^{\mathcal{M}_{\alpha(\rho)}}_{\mathsf{Loc}}(\rho,x))=x[\mathsf{Flds}\textsf{Comp}(\rho,d,x)]_{\alpha(\rho)}$

• •

$\mathcal{M}_{\alpha(\sigma)}$ is feasible on $\rho$.

• •

$\mathsf{Val}^{\mathcal{M}_{\alpha(\sigma)}}(\rho,x)=[\textsf{Comp}(\rho,x)]_{\alpha(\sigma)}$

Similarly, $\mathsf{Flds}\mathsf{Val}^{\mathcal{M}_{\alpha(\sigma)}}_{\mathsf{Loc}}(\rho,h)(\mathsf{Val}^{\mathcal{M}_{\alpha(\sigma)}}_{\mathsf{Loc}}(\rho,x))=[\mathsf{Flds}\textsf{Comp}(\rho,h,x)]_{\alpha(\sigma)}$

and $\mathsf{Flds}\mathsf{Val}^{\mathcal{M}_{\alpha(\sigma)}}_{\mathsf{Data}}(\rho,d)(\mathsf{Val}^{\mathcal{M}_{\alpha(\sigma)}}_{\mathsf{Loc}}(\rho,x))=[\mathsf{Flds}\textsf{Comp}(\rho,d,x)]_{\alpha(\sigma)}$

∎

3.4. Coherent Programs

Having defined the concept of terms associated with variables in an execution, we can now extend the notion of coherence, adapting it from (Mathur et al., 2019a) to accommodate updatable pointers as in the heap-manipulating programs that we study.

In the following, we say that $s$ is a superterm of $t$ modulo some congruence relation $\cong$ if there are terms $s^{\prime}$ and $t^{\prime}$ such that $t\cong t^{\prime}$, $s^{\prime}$ is a superterm of $t^{\prime}$ and $s^{\prime}\cong s$.

Definition 0 (Coherence).

A complete or partial execution $\sigma$ is said to be a coherent  execution if it satisfies the following two conditions.

**Memoizing.: **

Let $\rho$ be a prefix of $\sigma$ such that it is of the form $\rho^{\prime}\cdot\text{``}x:=y{\cdot}h\text{''}$ or $\rho^{\prime}\cdot\text{``}x:=f({\bf y})\text{''}$ and let $t_{x}=\textsf{Comp}(\rho,x)$. If there is a term $t^{\prime}\in\textsf{Terms}(\rho^{\prime})$ such that $t^{\prime}\cong_{\alpha(\rho^{\prime})}t_{x}$, then it must be the case that there is some variable $z\in V$ such that $\textsf{Comp}(\rho^{\prime},z)\cong_{\alpha(\rho^{\prime})}t_{x}$.

**Early Assumes.: **

Let $\rho$ be a prefix of the form $\rho^{\prime}\cdot\text{``}\textbf{assume}(x=y)\text{''}$ and let $t_{x}=\textsf{Comp}(\rho^{\prime},x),t_{y}=\textsf{Comp}(\rho^{\prime},y)$. If there is a term $t\in\textsf{Terms}(\rho^{\prime})$ such that $t$ is a superterm of $t_{x}$ or $t_{y}$ modulo $\cong_{\alpha(\rho^{\prime})}$, then there must be some variable $w\in V$ such that $\textsf{Comp}(\rho^{\prime},w)\cong_{\alpha(\rho^{\prime})}t$.

Note that these conditions are applicable to every sort-sensible combination of symbols.

As mentioned earlier, this definition of coherence  is inspired from the notion of coherence defined previously in (Mathur et al., 2019a). The memoizing restriction is the heart of the notion of coherent executions. Let us illustrate with a simple example.

Example 0.

Let $\pi_{7}$ be the following execution:

[TABLE]

It is easy to see that in the above execution $\pi_{7}$, the values of the variables u and v will be equal after executing all the $2n+2$ assignments, in any heap structure. As a result of the last assumption $\text{``}\textbf{assume}(\texttt{u}\neq\texttt{v})\text{''}$, the execution $\pi_{7}$ will thus be infeasible in all heap structures.

However, in order to accurately determine the relationship $\text{``}\texttt{u}=\texttt{v}\text{''}$ at the end of the execution, one needs to keep track of an unbounded amount of information (as $n$ can be increased unboundedly). This is the crucial insight in the first condition (memoizing), which states that when a term has been computed and dropped (i.e., no variable points to the term), then the execution should not recompute this term. Indeed, the above execution $\pi_{7}$ does not meet this requirement — the execution computed the term $t=\texttt{f}(\widehat{\texttt{w}})$ in its first half and stored it in u, re-assigned this variable u immediately after computing $t$, thereby losing all copies of $t$, and then later recomputed this term again in its second half. In fact, each of the terms $\texttt{f}^{i}(\texttt{w})$ ($1\leq i<n$) have been recomputed without retaining their original copies. Clearly, $\pi_{7}$ is not a coherent execution.

A similar example highlights the importance of the second coherence restriction (early assumes).

Example 0.

Let $\pi_{8}$ be the following execution:

[TABLE]

Observe that this execution is similar to the execution in Example 10. Also observe that, as before, this execution is infeasible in any heap structure. However, any algorithm that would accurately determine this in a streaming fashion would require access to unbounded memory.

Definition 0.

A program is said to be coherent if all its executions are coherent.

4. Assertion Checking for Coherent Alias-Aware  Programs

In this section we discuss our first main result — decidability of assertion checking for programs that are both alias-aware  as well as coherent.

Let us first define the problem of assertion checking. For this, we augment our programs with a special statement ‘assert(false)’, and thus our new syntax is given by the following grammar ($\langle stmt\rangle$ is as defined in Section 2.1.1).

[TABLE]

Observe that more complex assertions (including boolean combinations of equality/disequality assertions) can be expressed by translating them to conditional statements. For example, the assertion ‘$\textbf{assert}(x=y)$’ would translate to the program ‘$\textbf{if}\;(x\neq y)\;\textbf{then}\;\textbf{assert}(\textbf{false})\;\textbf{else}\;\textbf{skip}$’.

The set of executions for programs with assertions consists of sequences over the alphabet $\Pi_{\text{assert}}=\Pi\cup\{\text{``}\textbf{assert}(\textbf{false})\text{''}\}$ and can be defined as in Section 2.2, with the addition of the following rule: $\textsf{Exec}(\textbf{assert}(\textbf{false}))=\textbf{assert}(\textbf{false})$

The functions $\mathsf{Val}^{\mathcal{M}}_{\mathsf{Loc}},\mathsf{Val}^{\mathcal{M}}_{\mathsf{Data}},\mathsf{Flds}\mathsf{Val}^{\mathcal{M}}_{\mathsf{Loc}}$ and $\mathsf{Flds}\mathsf{Val}^{\mathcal{M}}_{\mathsf{Data}}$ in the presence of $\text{``}\textbf{assert}(\textbf{false})\text{''}$ are defined as before for execution prefixes without $\text{``}\textbf{assert}(\textbf{false})\text{''}$, and can be assumed to map all elements in their domain to a special symbol $\bot$ for all executions containing $\text{``}\textbf{assert}(\textbf{false})\text{''}$. The feasibility of a partial execution on the alphabet $\Pi_{\text{assert}}\setminus\{\text{``}\textbf{assert}(\textbf{false})\text{''}\}$ on a heap structure $\mathcal{M}$ is defined as before (Section 2.3) and is undefined otherwise.

Definition 0 (Assertion Checking for Heap-Manipulating Programs).

The problem of assertion checking for a program $s\in\langle stmt\rangle_{\text{assert}}$ is to check whether for every heap structure $\mathcal{M}$ and for every partial execution of $s$ of the form $\sigma\cdot\text{``}\textbf{assert}(\textbf{false})\text{''}$, we have that $\sigma$ is infeasible on $\mathcal{M}$.

We first note that the above problem is undecidable in general, a direct consequence of (Mathur et al., 2019a). Indeed, uninterpreted programs are heap-manipulating programs that do not mention any heap variables.

Theorem 2**.**

Assertion checking for heap-manipulating programs is undecidable.

Finally, we state our first decidability result. In the following, an alias-aware  coherent program is a program that is both coherent and alias-aware.

Theorem 3** (Decidability of Uninterpreted Assertion Checking).**

Assertion checking is decidable for the class of alias-aware coherent  programs and is $\mathsf{PSPACE}$-complete.

The proof of the above result relies on the following observations. First, for alias-aware executions, the terms associated with variables reflect their relationships on all heap structures (Theorem 8). Second, in this case, the streaming congruence closure algorithm for checking feasibility of coherent executions introduced in (Mathur et al., 2019a) can be extended directly to the case of coherent executions of heap-manipulating programs. The $\mathsf{PSPACE}$-hardness follows from the $\mathsf{PSPACE}$-hardness result for uninterpreted programs without updates ((Mathur et al., 2019a)). As a consequence of these observations, we also obtain the following result:

Theorem 4**.**

The problem of checking membership in the class of coherent and alias-aware  programs is decidable and is in $\mathsf{PSPACE}$.

5. Memory Safety, Forest Data-Structures, and Streaming-Coherence

We now tackle the problem of memory safety verification for heap-manipulating programs. The goal here is, given a program and an allocated set of locations (defined using a reachability specification), to check whether the program only dereferences (using pointer fields) locations that are in the (dynamically changing) set of allocated locations. We develop a technique for when the initial heap holds a forest data-structure (disjoint lists and tree-like structures). We define a subclass of programs, called streaming-coherent, for which memory safety is decidable. The key idea is to utilize the fact that the initial heap is a forest data-structure in order to make programs alias aware.

For an execution that works over a forest data-structure, one can accurately infer the aliasing relationship between two program variables by tracking if they point to locations on the heap obtained by traversing the same path (i.e., starting from the same initial location and taking the same pointers at each step). Intuitively, in a forest data-structure, two distinct traversals always lead to different locations. In addition, when the program execution does a single pass over the data-structure, one can keep track of the aliasing relationship between variables (or equivalently, whether the locations pointed to by two variables are same or not) using a streaming algorithm. The notion of streaming-coherence essentially ensures such a single pass. Finally, updatable maps can be used to keep track of the initial allocated set and the allocations/frees performed by the program during its execution. Consequently, memory safety can be reduced to assertion checking.

This section is organized as follows.  Section 5.1 introduces the reachability specifications that specify the initial set of allocated locations, and defines the memory safety problem formally. We also show here that memory safety is undecidable in general, and undecidable even for coherent programs.  Section 5.2 defines the class of forest data-structures, and shows that memory safety remains undecidable for programs that start with a heap that holds a forest data-structure. Section 5.3 defines the notion of streaming-coherent  programs.

5.1. Reachability Specification and Memory Safety

Reachability Specification

Heap-manipulating programs can be annotated by a reachability specification that restricts the allowable nodes that can be accessed by a program. A reachability specification is an indexed set of triples $\varphi=\{\varphi_{k}\}_{k=1}^{n}$ where $\varphi_{i}=(\mathsf{Start}_{i},\mathsf{Pointers}_{i},\mathsf{Stop}_{i})$ is such that $\mathsf{Start}_{k}\subseteq\mathcal{C}_{\mathsf{Loc}}$, $\mathsf{Stop}_{k}\subseteq\mathcal{C}_{\mathsf{Loc}}$ and $\mathsf{Pointers}_{k}\subseteq\mathcal{F}_{\mathsf{Loc}}$. Each triple $\varphi_{i}$ denotes a set of locations $\mathsf{Reach}_{i}$, which is the least set that contains $\mathsf{Start}_{i}$, does not include $\mathsf{Stop}_{i}$ and is closed under repeated applications of pointer fields $\mathsf{Pointers}_{i}$. More formally, given a heap structure $\mathcal{M}$ with interpretation $\mathcal{I}$, $\mathsf{Reach}_{i}$ gives a set of locations, which is the smallest set such that

(a) $\{\mathcal{I}(c)\,\mid\,c\in\mathsf{Start}_{i}\}\setminus\{\mathcal{I}(c)\,\mid\,c\in\mathsf{Stop}_{i}\}\subseteq\mathsf{Reach}_{i}$, and

(b) for every $e\in\mathsf{Reach}_{i}$ and for every $p\in\mathsf{Pointers}_{i}$, if $\mathcal{I}(p)(e)\not\in\{\mathcal{I}(c)\,\mid\,c\in\mathsf{Stop}_{i}\}$, then $\mathcal{I}(p)(e)\in\mathsf{Reach}_{i}$.

We let $\mathsf{Reach}_{\varphi}=\bigcup\limits_{i=1}^{n}\mathsf{Reach}_{i}$. Often the heap structure $\mathcal{M}$ will be implicit and we will omit mentioning it.

Allocated Nodes

Starting with a reachability specification $\varphi$ on a given heap structure $\mathcal{M}$, an execution $\sigma$ defines a set of allocated nodes, which we denote as $\mathsf{Alloc}(\sigma)$ and define as follows.

[TABLE]

Memory Safety

An execution $\sigma$ is said to violate memory safety over a heap structure $\mathcal{M}$ with respect to a reachability specification $\varphi$ if there is a prefix $\rho^{\prime}=\rho\cdot s$ of $\sigma$ such that $\rho$ is feasible over $\mathcal{M}$ and one of the following holds.

1. (1)

$s$ dereferences a location that was not allocated. That is, $s$ is of the form $\text{``}w:=y{\cdot}h\text{''}$ or $\text{``}y{\cdot}h:=w\text{''}$, $y\in V_{\mathsf{Loc}}$ and $w$ and $h$ are variables and pointer fields of appropriate sorts, such that $\mathsf{Val}^{\mathcal{M}}_{\mathsf{Loc}}(\rho,y)\not\in\mathsf{Alloc}(\rho)$. 2. (2)

$s$ frees an unallocated location. That is, $s$ is of the form $\textbf{free}(x)$ and $\mathsf{Val}^{\mathcal{M}}_{\mathsf{Loc}}(\rho,x)\not\in\mathsf{Alloc}(\rho)$.

An execution $\sigma$ is memory safe over $\mathcal{M}$ with respect to $\varphi$ if it does not violate memory safety over $\mathcal{M}$ with respect to $\varphi$. With this, we can now define the memory safety verification problem. In the following, we fix our signature $\Sigma$.

Definition 0 (Memory Safety Verification).

The memory safety verification problem asks, given a program $P\in\langle stmt\rangle$ and a reachability specification $\varphi$, whether for all heap structures $\mathcal{M}$, each execution $\sigma\in\textsf{Exec}(P)$ is memory safe over $\mathcal{M}$ with respect to $\varphi$.

We show, unsurprisingly, that checking memory safety is undecidable in general.

Theorem 2** (Undecidability of Memory Safety).**

Memory safety verification is undecidable.

Proof.

In (Mathur et al., 2019a), the authors consider uninterpreted programs, which are programs that have variables taking values in a data domain that is uninterpreted; programs in (Mathur et al., 2019a) don’t have heap variables, and do not modify heaps. It was shown (Theorem 11 in (Mathur et al., 2019a)) that given an uninterpreted program $P$, the problem of determining if there is a data domain $\mathcal{M}$ and an execution $\rho$ of $P$, such that $\rho$ is feasible in $\mathcal{M}$, is undecidable. Our result here can be proved by a simple reduction from that problem. Let $P$ be an uninterpreted program. Consider the reachability specification $\varphi=(\{\widehat{x}\},\{p\},\{\widehat{x}\})$ such that $x\in V_{\mathsf{Loc}}$ is a new variable. Consider program $P^{\prime}=P;y=x{\cdot}p$. Observe that $P^{\prime}$ is memory safe with respect to $\varphi$ if and only if $P$ does not have a feasible execution with respect to some data model. ∎

Given the undecidability result in Theorem 2, we need to identify a restricted subclass of programs and initial heap structures for which the problem of verifying memory safety is decidable. This leads us to the notions of forest data-structures and streaming-coherent programs. In some sense, forest data-structures are natural classes of heap structures where the alias-aware  restrictions become very minimal. We combine these remaining restrictions with our usual notion of coherence  to introduce a new notion of streaming-coherent  programs. We define these below.

5.2. Forest Data-Structures

Let us now define our characterization of heap structures that will be amenable to our decidability result. The main restriction is stated in bullet (3) below and intuitively disallows two different paths to the same location on the heap.

Definition 0 (Forest Data-structures).

A heap structure $\mathcal{M}=(U_{\mathsf{Loc}},U_{\mathsf{Data}},\mathcal{I})$ over a signature $\Sigma$ is said to be a forest data-structure with respect to a reachability specification $\varphi=\{\varphi_{k}\}_{k=1}^{n}$ if

1. (1)

for every $1\leq i\leq n$, each set of stopping locations is a singleton set of the form $\mathsf{Stop}_{i}=\{\mathsf{stop}_{i}\}$, 2. (2)

for every $c\in\bigcup\limits_{k=1}^{n}\mathsf{Stop}_{k}$, and for every $f\in\mathcal{F}_{\mathsf{Loc}}$, we have that $\mathcal{I}(f(c))=\mathcal{I}(c)$, and 3. (3)

for every $t_{i}\in\textsf{Terms}(\mathsf{Start}_{i},\mathsf{Pointers}_{i})\cup\mathsf{Stop}_{i}$ and $t_{j}\in\textsf{Terms}(\mathsf{Start}_{j},\mathsf{Pointers}_{j})\cup\mathsf{Stop}_{j}$ we have, if $\mathcal{I}(t_{i})=\mathcal{I}(t_{j})$, then either $t_{i}=t_{j}\in\mathsf{Start}_{i}\cap\mathsf{Start}_{j}$, or $\mathcal{I}(t_{i})=\mathcal{I}(t_{j})=\mathcal{I}(\mathsf{stop}_{i})=\mathcal{I}(\mathsf{stop}_{j})$.

Intuitively, a heap structure is a forest data-structure with respect to $\varphi$, if the subgraph $G_{i}$ induced by the set of nodes (excluding $\mathsf{Stop}_{i}$) reachable from $\mathsf{Start}_{i}$, using any number of pointers from $\mathsf{Pointers}_{i}$ forms a tree, and further, any two subgraphs $G_{i}$ and $G_{j}$ do not have a node in common (except possibly for the starting locations). Notice that Definition 3 do not impose any restrictions on the elements of the data sort of a heap structure.

Our notion of forest data-structures handles the aliasing problem while still being able to express many practical reachability specifications. Consider the following example similar to our pathological example from Section 3.1.

Example 0.

$\pi_{2}=\pi^{\prime}_{2}\cdot\textbf{assume}(\texttt{z}_{2}=\texttt{z}_{3})$ where

[TABLE]

With respect to forest data-structures the above pathological execution $\pi_{2}$ is, in fact, infeasible. To understand this, observe that for a forest data-structure, if two different locations (x and y in the execution $\pi_{2}$ for instance) are not equal to the stopping location ($\texttt{x}\neq\mathtt{NIL}$ and $\texttt{y}\neq\mathtt{NIL}$), then these locations are also different from each other (and thus $\texttt{x}\neq\texttt{y}$). This means that in the execution $\pi_{2}$, the update $\text{``}\texttt{y}{\cdot}\texttt{next}:=\texttt{z}_{2}\text{''}$ will not affect the value of $\text{``}\texttt{x}{\cdot}\texttt{next}\text{''}$. Now, when the execution reads the value of $\text{``}\texttt{x}{\cdot}\texttt{next}\text{''}$ in $\texttt{z}_{3}$, it is expected to be the same as earlier (i.e., some location as pointed to by $\texttt{z}_{1}$), but since $\texttt{z}_{1}\neq\texttt{z}_{2}$, we must have $\texttt{z}_{3}\neq\texttt{z}_{2}$. This means that the last assume $\textbf{assume}(\texttt{z}_{2}=\texttt{z}_{3})$ makes the execution infeasible.

However, the notion of forest data-structures, by itself, is not enough to ensure decidability, as is shown by the following result.

Theorem 5**.**

The memory safety verification problem for forest data-structures is undecidable.

Proof.

Follows trivially from Theorem 2 because the reachability specification $\varphi$ used in the proof of Theorem 2 is such that $\mathsf{Reach}_{\varphi}$ is the empty set. ∎

Next, we introduce a class of programs called streaming-coherent programs that, in conjunction with forest data-structures results in a $\mathsf{PSPACE}$ decision procedure. We will discuss the decision procedure in Section 6.

5.3. Streaming-Coherent Executions and Programs

In this section, we identify the class of streaming-coherent programs and executions, for which we show decidability. It is analogous to the notion of coherence (Definition 9), except that it uses a different notion of equivalence (for terms) instead of ${\equiv}_{\alpha(\cdot)}$. We define this new notion of equivalence (forest equality closure) below. Intuitively, this notion characterizes the behavior of executions on the class of forest data-structures and allows us to adapt the algorithm used for assertion checking of alias-aware coherent programs (Theorem 3).

Definition 0 (Forest Equality Closure).

Let $\varphi=\{\varphi_{i}\}_{i=1}^{n}$ be a reachability specification, with $\varphi_{i}=(\mathsf{Start}_{i},\mathsf{Pointers}_{i},\mathsf{Stop}_{i})$. Let $\textsf{Terms}_{i}=\textsf{Terms}(\mathsf{Start}_{i},\mathsf{Pointers}_{i})$ ($1\leq i\leq n$). Let $E\subseteq\textsf{Terms}\times\textsf{Terms}$ be an equality relation on terms. The forest equality closure of $E$ with respect to $\varphi$, denoted $\mathsf{Closure}^{=}(\varphi,E)\subseteq\textsf{Terms}\times\textsf{Terms}$ is the smallest congruence relation that satisfies the following.

• •

$E\subseteq\mathsf{Closure}^{=}(\varphi,E)$.

• •

For every $t_{i}\in\textsf{Terms}_{i}$ and $t_{j}\in\textsf{Terms}_{j}$ such that $t_{i}\neq t_{j}$, we have

[TABLE]

We will now define the notion of streaming-coherent  programs with respect to a given reach specification $\varphi$. To do this, we first need the notion of streaming-coherent  executions. This notion is very similar to the notion of coherence (Definition 9) and requires that terms are not recomputed and that assumes over the data sort are early.

Definition 0 (Streaming-Coherence).

Let $\sigma$ be a complete or partial execution. $\sigma$ is said to be streaming-coherent if it satisfies the following two conditions.

**Memoizing.: **

Let $\rho$ be a prefix of $\sigma$ of the form $\rho^{\prime}\cdot\text{``}x:=y{\cdot}h\text{''}$ or $\rho^{\prime}\cdot\text{``}x:=f({\bf y})\text{''}$ and let $t=\textsf{Comp}(\rho,x)$. If there is a term $t^{\prime}\in\textsf{Terms}(\rho^{\prime})$ such that $t\cong_{\mathsf{Closure}^{=}(\varphi,\alpha(\rho^{\prime}))}t^{\prime}$, then it must be the case that there is some variable $z\in V$ such that $\textsf{Comp}(\rho^{\prime},z)\cong_{\mathsf{Closure}^{=}(\varphi,\alpha(\rho^{\prime}))}t$. This condition is applicable to every sort-sensible combination of symbols.

**Early Assumes.: **

Let $\rho$ be a prefix of the form $\rho^{\prime}\cdot\text{``}\textbf{assume}(u=v)\text{''}$ where $u,v\in V_{\mathsf{Data}}$ and $t_{u}=\textsf{Comp}(\rho^{\prime},u),t_{v}=\textsf{Comp}(\rho^{\prime},v)$. If there is a term $t\in\textsf{Terms}(\rho^{\prime})$ such that $t$ is a superterm of $t_{u}$ or $t_{v}$ modulo $\cong_{\mathsf{Closure}^{=}(\varphi,\alpha(\rho^{\prime}))}$, then there must be some variable $w\in V_{\mathsf{Data}}$ such that $\textsf{Comp}(\rho^{\prime},w)\cong_{\mathsf{Closure}^{=}(\varphi,\alpha(\rho^{\prime}))}t$.

Observe that the above definition is close the definition of coherence (Definition 9), but nevertheless there are important differences. First, the early assumes requirement does not apply to variables of the $\mathsf{Loc}$ sort because forest data-structures simplify that requirement. Second, the congruence with respect to which equalities are demanded in the above definition is not one of the congruence closure defined by the equalities accumulated by the execution (which is the congruence used in Definition 9), but rather the congruence of forest equality closure.

Definition 0.

A program is said to be streaming-coherent  with respect to $\varphi$ if all its executions are streaming-coherent  with respect to $\varphi$.

We note here that streaming-coherent  programs on forest data-structures are essentially one-pass algorithms. Intuitively, forest data-structures enforce the alias-aware  restriction by mandating that two locations obtained by two different traversals from the set of initial locations (therefore being represented by two different terms) are different (with minor exceptions). Therefore if a streaming-coherent  execution computes a term twice, i.e., visits a location twice, by definition it has to store a pointer to that location in some variable. Since the number of variables is fixed a priori, it is simple to see that a nontrivial, multi-pass algorithm such as linked-list sorting would inherently be non-streaming-coherent (since it is meant to work on lists of arbitrary size).

6. Streaming Congruence Closure for Forest Data-structures

We will now focus on streaming-coherent programs whose initial heap is a forest data-structure. We now present the second main result of our paper.

Theorem 1** (Decidability of Memory Safety for Streaming-Coherent Programs and Forest Data-Structures).**

The memory safety verification problem over forest data-structures for streaming-coherent programs is decidable and is $\mathsf{PSPACE}$-complete.

Given a reachability specification, we present an algorithm for checking memory safety of such programs. This will establish the decidability and the membership of the problem in $\mathsf{PSPACE}$. The hardness follows from the $\mathsf{PSPACE}$-hardness result in (Mathur et al., 2019a).

Our algorithm is automata theoretic— we construct a finite state automaton $\mathcal{A}_{\textsf{MS}}$ such that its language $L(\mathcal{A}_{\textsf{MS}})$ includes all streaming-coherent executions that are memory safe and excludes all streaming-coherent executions that are not memory safe. Finally, in order to determine if a given streaming-coherent program $P$ is memory safe, we simply check if $\textsf{Exec}(P)\subseteq L(\mathcal{A}_{\textsf{MS}})$; since $\textsf{Exec}(P)$ is also a regular language, this reduces to checking intersection of regular languages.

Let us first discuss some intuition for our construction. The state of the automaton has several components which can be categorized into two groups:

(1) those that track feasibility of executions, and

(2) those that are used to check for violations of memory safety.

The first category comprises of three components ${\equiv},d,P$ which keep track of equalities, disequalities, and functional relationships between variables at a given point in the execution. These components are inspired by the work of (Mathur et al., 2019a) in the context of coherent uninterpreted programs, where this information was used to answer questions of assertion checking/feasibility. Our extended and refined notion of streaming-coherent  programs also has this property, and these three components serve the same roles in our setting. Similar to the work in (Mathur et al., 2019a), when an execution is streaming-coherent, these three components ${\equiv},d,P$ can be accurately maintained at every step in the execution by performing local congruence closure.

We now describe the remaining components of the state, namely those that help check for memory safety. We know from our earlier discussion that forest data-structures are implicitly alias aware. This is because such heap structures consist of many disjoint reachability specifications each of which describes a tree. Therefore, nodes obtained by different pointer traversals from the initial locations are different, and each tree in the forest is closed under a given set of pointers. We keep track of locations (for the purpose of memory safety) primarily using three ordered collections which are disjoint:

(a) a collection $Y=\{Y_{i}\}_{i}$ of ‘yes’ sets,

(b) a collection $M=\{M_{i}\}_{i}$ of ‘maybe’ sets and

(c) a ‘no’ set $N$.

Each $Y_{i}$ and $M_{i}$ above correspond to the $i^{th}$ reachability specification $\varphi_{i}$. In the following, we describe each of these.

$N$ is a set of variables that point to locations which, when dereferenced, lead to a memory safety violation. These locations include the stopping locations of any of the reachability specifications, or those locations in the allocated set that have been freed during the execution. Consider the reachability specification $\psi=(\{\texttt{x}\},\{\texttt{next}\},\{\mathtt{NIL}\})$. At the beginning of any execution, the set $N$ for this specification is $\{\mathtt{NIL}\}$. Further, when the execution encounters the statement $\textbf{free}(\texttt{y})$, we update the $N$ component of the state by adding y.

The sets $Y_{i}$ hold a subset of program variables that point to locations obtained by traversing the $i^{\text{th}}$ reachability specification $\varphi_{i}$. In particular, a variable z belongs to $Y_{i}$ when we know that the corresponding location can be dereferenced without causing a memory safety violation in any heap structure. This can happen when the execution establishes that the location pointed to by z is not the stopping location of $\varphi_{i}$ (i.e., $\mathsf{stop}_{i}$). Consider $\psi$ and the single step execution $\sigma_{1}=\textbf{assume}(\texttt{x}\neq\mathtt{NIL})$. At the end of $\sigma_{1}$ we know that in all heap structures in which $\sigma_{1}$ is feasible, it must be that the location pointed to by x can be dereferenced, and therefore we would add x to the corresponding ‘yes’ set.

Lastly, the ‘maybe’ sets $M_{i}$ hold variables that can be obtained by traversing the tree of $\varphi_{i}$, but are neither known to be stopping locations/freed locations, nor known to be in the allocated set in all feasible heap structures. Consider again $\psi$ and the execution $\sigma_{2}=\textbf{assume}(\texttt{x}\neq\mathtt{NIL})\cdot\texttt{y}:=\texttt{x}{\cdot}\texttt{next}$. Recall that x belongs to the ‘yes’ set after the first statement (i.e., the execution $\sigma_{1}$) and we can therefore dereference it. However, at the end of the execution we would include y in the ‘maybe’ set because the location $\texttt{x}{\cdot}\texttt{next}$ is not in the allocated set in all feasible heap structures. In particular, a heap structure defining a list of length one is a feasible structure for this execution but $\texttt{x}{\cdot}\texttt{next}$ would be $\mathtt{NIL}$, which is not in the allocated set. Now consider the execution $\sigma_{3}=\sigma_{2}\cdot\textbf{assume}(\texttt{y}\neq\mathtt{NIL})$. After the last statement in $\sigma_{3}$ we would now shift y from the ‘maybe’ set to the ‘yes’ set.

This is precisely what our automaton does, shifting variables between components and flagging memory safety violations when the execution dereferences (the location pointed to by) a variable that is not in any $Y_{i}$. However, we do this modulo equalities between variables and these sets described above are in fact sets of equivalence classes. Lastly, we also keep track of variables that point to locations allocated by $\text{``}\textbf{alloc}(\cdot)\text{''}$ using a set $A$ of equivalence classes of variables. Of course, we would transfer an equivalence class from $A$ to $N$ if the execution frees this memory, similar to what happens to members of the ‘yes’ sets.

6.1. Formal Description of Construction

We shall now proceed with the formal construction of the automaton $\mathcal{A}_{\textsf{MS}}$, which accepts a streaming-coherent execution iff it is memory safe. Recall that our reachability specification is an indexed set of tuples $\varphi=\{\varphi_{k}\}_{k=1}^{n}$, where $\varphi_{k}=(\mathsf{Start}_{k},\mathsf{Pointers}_{k},\mathsf{Stop}_{k})$. To simplify presentation, we assume that the set of variables $V$ in our programs is such that for every constant $c$ appearing in the reachability specification $\varphi$, there is a variable $v_{c}$ corresponding to $c$. Further, we assume that these variables are never overwritten. We will, therefore, often interchangeably refer to these constants in $\varphi$ by their corresponding variables, and vice versa. These assumptions can be relaxed with a more involved construction.

The automaton is a tuple $\mathcal{A}_{\textsf{MS}}=(Q,q_{0},\delta)$, where $Q$ is the set of states, $q_{0}$ is the initial state and $\delta:Q\times\Pi\to Q$ is the transition function. Recall that executions are strings over $\Pi$, which is also the alphabet of the automaton $\mathcal{A}_{\textsf{MS}}$. We describe each of these components below.

States. The automaton has two distinguished states $q_{\mathsf{infeasible}}$ and $q_{\mathsf{unsafe}}$. All other states are tuples of the form $({\equiv},d,P,Y,M,N,A,X)$, where each component is as follows.

• •

${\equiv}$ is an equivalence relation over $V$ that respects sorts. We will use $[x]_{{\equiv}}$ to denote the set $\{y\,\mid\,(x,y)\in{\equiv}\}$

• •

$d$ is a symmetric set of pairs of the form $(c_{1},c_{2})$, where $c_{1},c_{2}\in V/{\equiv}$ are equivalence classes.

• •

$P$ associates partial mappings to function symbols in $\mathcal{F}_{\mathsf{Data}}$ and pointer field in $\mathsf{Flds}=\mathsf{Flds}_{\mathsf{Loc}}\cup\mathsf{Flds}_{\mathsf{Data}}$. More formally, for every $f\in\mathcal{F}_{\mathsf{Data}}$ of arity $r$, and classes $c_{1},c_{2},\ldots,c_{r}\in V_{\mathsf{Data}}/{\equiv}$, we have $P(f)(c_{1},\ldots,c_{r})\in V_{\mathsf{Data}}/{\equiv}$ (if defined). Similarly, for every $p\in\mathsf{Flds}_{\mathsf{Loc}}$, and every $c\in V_{\mathsf{Loc}}/{\equiv}$, $P(p)(c)\in V_{\mathsf{Loc}}/{\equiv}$, and for every $d\in\mathsf{Flds}_{\mathsf{Data}}$, and every $c\in V_{\mathsf{Loc}}/{\equiv}$, $P(d)(c)\in V_{\mathsf{Data}}/{\equiv}$. We will say $P(h)(c_{1},\ldots,c_{k})=\mathsf{undef}$ when the function/pointer symbol $h$ is not defined on the arguments $c_{1},\ldots,c_{k}$.

• •

$Y=\{Y_{k}\}_{k=1}^{n}$ and $M=\{M_{k}\}_{k=1}^{n}$ are indexed collections of sets such that for every $1\leq i\leq n$, we have $Y_{i},M_{i}\subseteq V_{\mathsf{Loc}}/{\equiv}$.

• •

The sets $N$, $A$ and $X$ are sets of equivalence classes of location variables, i.e., $N,A,X\subseteq V_{\mathsf{Loc}}/{\equiv}$.

Initial State. The initial state $q_{0}$ is the tuple $({\equiv}_{0},d_{0},P_{0},Y_{0},M_{0},N_{0},A_{0},X_{0})$ such that

• •

${\equiv}_{0}$ is the identity relation on the set $V$ of variables,

• •

$P_{0}$ is such that for all functions and pointer fields $f$, the range of $P(f)$ is empty,

• •

each of $d_{0},A_{0}$ and $(Y_{0})_{1},\ldots,(Y_{0})_{n}$ are $\varnothing$ (empty set),

• •

for each $1\leq i\leq n$, $(M_{0})_{i}=\{[v]_{{\equiv}_{0}}\,\mid\,v\in\bigcup_{i=1}^{n}\mathsf{Start}_{i}\}$,

• •

$N_{0}=\{[v]_{{\equiv}_{0}}\,\mid\,v\in\bigcup_{i=1}^{n}\mathsf{Stop}_{i}\}$.

• •

$X_{0}=\{[v]_{{\equiv}_{0}}\,\mid\,v\in V_{\mathsf{Loc}}\}\setminus\left(N_{0}\cup\bigcup_{i=1}^{n}(M_{0})_{i}\right)$.

Transitions. The states $q_{\mathsf{infeasible}}$ and $q_{\mathsf{unsafe}}$ are absorbing states. That is, for every $s\in\Pi$, $\delta(q_{\mathsf{infeasible}},s)=q_{\mathsf{infeasible}}$ and $\delta(q_{\mathsf{unsafe}},s)=q_{\mathsf{unsafe}}$. In the following, we describe the transition function for every other state in $Q$. Let $q\in Q\setminus\{q_{\mathsf{infeasible}},q_{\mathsf{unsafe}}\}$, $s\in\Pi$ and let $q^{\prime}=\delta(q,s)$. Then, $q^{\prime}$ is $q_{\mathsf{infeasible}}$ or $q_{\mathsf{unsafe}}$, or is of the form $q^{\prime}=({\equiv}^{\prime},d^{\prime},P^{\prime},Y^{\prime},M^{\prime},N^{\prime},A^{\prime},X^{\prime})$.

1. (1)

Case $s=\text{``}u:=v\text{''}$, $u,v\in V$.

In this case, we add the variable $u$ into the class of $v$ and appropriately update each of the components. That is, {\equiv}^{\prime}=\big{(}{\equiv}\setminus\{(u,u^{\prime}),(u^{\prime},u)\,\mid\,u\neq u^{\prime},u^{\prime}\in[u]_{{\equiv}}\}\big{)}\cup\{(u,v^{\prime}),(v^{\prime},u)\,\mid\,v^{\prime}\in[v]_{{\equiv}}\}. The other components of the state are the same as in $q$. 2. (2)

Case $s=\text{``}x:=y{\cdot}p\text{''}$, $x,y\in V_{\mathsf{Loc}}$ and $p\in\mathsf{Flds}_{\mathsf{Loc}}$.

In this case, we need to check if the variable $y$ corresponds to a location that can be dereferenced. If not, we have a memory safety violation; otherwise, we establish the relationship $x=p(y)$ in the next state. Formally, if there is no $i$ such that $[y]_{{\equiv}}\in Y_{i}$ and if $[y]_{{\equiv}}\not\in A$, then $q^{\prime}=q_{\mathsf{unsafe}}$. Otherwise we have that $[y]_{{\equiv}}\in A$ or there is a $k$ such that $[y]_{{\equiv}}\in Y_{k}$. In this case we define the tuple $q^{\prime}=({\equiv}^{\prime},d^{\prime},P^{\prime},Y^{\prime},M^{\prime},N^{\prime},A^{\prime},X^{\prime})$ below. Here, we need to consider the following cases.

• •

Case $P(p)([y]_{{\equiv}})$ is defined and equals $[z]_{{\equiv}}$. In this case, $q^{\prime}$ is defined in the same manner as though $s=\text{``}x:=z\text{''}$.

• •

Case $P(p)([y]_{{\equiv}})=\mathsf{undef}$. Here, for streaming-coherent programs it must be the case that $[y]_{{\equiv}}\in Y_{k}$ for some $k$. Here, we create a new singleton equivalence class containing $x$ and set the value of the $p$ map, on $y$ to be this new class. We also assert that $[x]_{{\equiv}^{\prime}}$ is not equal to any class in any of the $Y_{i}$s or in $A$. That is,

• –

${\equiv}^{\prime}={\equiv}\setminus\{(x,x^{\prime})\,\mid\,x^{\prime}\neq x\}\cup\{(x,x)\}$.

• –

$d^{\prime}{=}\{([u]_{{\equiv}^{\prime}},[v]_{{\equiv}^{\prime}})\mid u\neq x,v\neq x,([u]_{{\equiv}},[v]_{{\equiv}})\in d\}\cup\{([x]_{{\equiv}^{\prime}},c),(c,[x]_{{\equiv}^{\prime}})\mid c\in A\cup\bigcup\limits_{i=1}^{n}Y_{i}\}$

• –

$P^{\prime}(p)([y]_{{\equiv}^{\prime}})=[x]_{{\equiv}^{\prime}}$. For all other combinations of functions/pointers and arguments, $P^{\prime}$ behaves same as $P$.

• –

One of the sets $M_{k}$ and $X$ are updated depending upon the pointer $p$. If $p\in\mathsf{Pointers}_{k}$, then $M^{\prime}_{k}=\{[z]_{{\equiv}^{\prime}}\mid[z]_{{\equiv}}\in M_{k}\}\cup\{[x]_{{\equiv}^{\prime}}\}$. Otherwise, $X=\{[z]_{{\equiv}^{\prime}}\mid[z]_{{\equiv}}\in X\}\cup\{[x]_{{\equiv}^{\prime}}\}$.

• –

All other components are the same as in $q$. 3. (3)

Case $s=\text{``}a:=y{\cdot}d\text{''}$, $a\in V_{\mathsf{Data}},y\in V_{\mathsf{Loc}}$ and $d\in\mathsf{Flds}_{\mathsf{Data}}$.

As in the previous case, $q^{\prime}=q_{\mathsf{unsafe}}$ if $[y]_{{\equiv}}\not\in\cup_{i=1}^{n}Y_{i}\cup A$. Otherwise, similar to the previous case, we have two cases to consider. As before, if there is a variable $b\in V_{\mathsf{Data}}$ such that $P(d)([y]_{{\equiv}})=[b]_{{\equiv}}$, then we treat this case as that of $\text{``}a:=b\text{''}$. Otherwise, the new equivalence relation ${\equiv}^{\prime}$ is such that ${\equiv}^{\prime}={\equiv}\setminus\{(a,u)\,\mid\,u\neq a\}\cup\{(a,a)\}$, while the other components are the same as in $q.$ 4. (4)

Case $s=\text{``}y{\cdot}h:=u\text{''}$, $y\in V_{\mathsf{Loc}}$.

We uniformly handle the case of $h$ being either a pointer field ($\mathsf{Flds}_{\mathsf{Loc}}$) or a data field ($\mathsf{Flds}_{\mathsf{Data}}$). Here we have $q^{\prime}=q_{\mathsf{unsafe}}$ if $[y]_{{\equiv}}\not\in\cup_{i=1}^{n}Y_{i}\cup A$. Otherwise, we simply change $P$ as follows (while keeping other components the same as in $q$):

• •

$P^{\prime}(f)=P(f)$ for $f\neq h$

• •

$P^{\prime}(h)([y]_{{\equiv}^{\prime}})=[u]_{{\equiv}^{\prime}}$

• •

For $z\in V_{\mathsf{Loc}}$ such that $z\notin[y]_{{\equiv}}$, $P^{\prime}(h)([z]_{{\equiv}^{\prime}})=[w]_{{\equiv}^{\prime}}$ if $P(h)([z]_{{\equiv}})=[w]_{{\equiv}}$ for some variable $w$, and $P^{\prime}(h)([z]_{{\equiv}^{\prime}})=\mathsf{undef}$ if no such variable $w$ exists. 5. (5)

Case $s=\text{``}a:=f(c_{1},\ldots,c_{r})\text{''}$, $a\in V_{\mathsf{Data}}$.

Here, we have two cases to consider again. If there is a variable $b\in V_{\mathsf{Data}}$ such that $P(f)([c_{1}]_{{\equiv}},\ldots,[c_{r}]_{{\equiv}})=[b]_{{\equiv}}$, then we treat this case as that of $\text{``}a:=b\text{''}$. Otherwise, we add a singleton equivalence class containing $a$ and update $P(f)$, while keeping all other components the same (modulo the new equivalence relation). Formally,

• •

${\equiv}^{\prime}={\equiv}\setminus\{(a,u),(u,a)\,\mid\,u\in V_{\mathsf{Data}}\}\cup\{(a,a)\}$.

• •

$P^{\prime}(h)$ is same as in $q$ if $h\neq f$. The evaluation of $P^{\prime}$ on $f$ is described as follows.

[TABLE]

• •

All other components are the same as in $q$. 6. (6)

Case $s=\text{``}\textbf{alloc}(x)\text{''}$.

In this case, we create a new singleton class containing $x$, and add this class to the component $A$. We also assert that this new class is not equal to any other class. Formally,

• •

${\equiv}^{\prime}={\equiv}\setminus\{(x,u)\,\mid\,u\in V_{\mathsf{Loc}}\}\cup\{(x,x)\}$.

• •

$d^{\prime}=\{([u_{1}]_{{\equiv}^{\prime}},[u_{2}]_{{\equiv}^{\prime}})\,\mid\,u_{1}\neq u_{2},([u_{1}]_{{\equiv}},[u_{2}]_{{\equiv}})\in d\text{ or }u_{1}=x\lor u_{2}=x\}$

• •

$A^{\prime}=\{[u]_{{\equiv}^{\prime}}\,\mid\,[u]_{{\equiv}}\in A\}\cup\{[x]_{{\equiv}^{\prime}}\}$.

• •

The component $P$ is updated as follows. For every function symbol $f\in\mathcal{F}_{\mathsf{Data}}$, $P^{\prime}(f)$ is the same as $P(f)$. Further, for every pointer field $h\in\mathsf{Flds}_{\mathsf{Data}}\cup\mathsf{Flds}_{\mathsf{Loc}}$ and for every variable $y\in V_{\mathsf{Loc}}\setminus\{x\}$, we have $P^{\prime}(h)([y]_{{\equiv}^{\prime}})=P(h)([y]_{{\equiv}})$. Finally, the mapping on $x$ is defined as $P(p)([x]_{{\equiv}^{\prime}})=[x]_{{\equiv}^{\prime}}$ for every location pointer $p\in\mathsf{Flds}_{\mathsf{Loc}}$ and $P(d)([x]_{{\equiv}^{\prime}})=\mathsf{undef}$ for every data pointer $d\in\mathsf{Flds}_{\mathsf{Data}}$.

• •

All other components are updated as usual. 7. (7)

Case $s=\text{``}\textbf{free}(x)\text{''}$.

In this case, if $[x]_{{\equiv}}\not\in A\cup\bigcup\limits_{i=1}^{n}Y_{i}$, then $q^{\prime}=q_{\mathsf{unsafe}}$. Otherwise, we remove the class $[x]_{{\equiv}}$ from the sets $A$ or $Y_{1},\ldots,Y_{n}$ and add it to the set $N$. That is,

• •

${\equiv}^{\prime}={\equiv}$

• •

$N^{\prime}=\{[z]_{{\equiv}^{\prime}}\,\mid\,[z]_{{\equiv}}\in N\}\cup\{[x]_{{\equiv}^{\prime}}\}$

• •

for every $1\leq i\leq n$, $Y^{\prime}_{i}=\{[z]_{{\equiv}^{\prime}}\,\mid\,[z]_{{\equiv}}\neq[x]_{{\equiv}},[z]_{{\equiv}}\in Y_{i}\}$

• •

$A=\{[z]_{{\equiv}^{\prime}}\,\mid\,[z]_{{\equiv}}\neq[x]_{{\equiv}},[z]_{{\equiv}}\in A\}$

• •

Other components remain the same. 8. (8)

Case $s=\text{``}\textbf{assume}(x=y)\text{''}$, $x,y\in V_{\mathsf{Loc}}$. In this case, if $[x]_{{\equiv}}=[y]_{{\equiv}}$ then $q^{\prime}=q$. Otherwise we have several cases to consider.

In each of these cases, we construct a new tuple $q^{\prime\prime}=({\equiv}^{\prime\prime},d^{\prime\prime},P^{\prime\prime},Y^{\prime\prime},N^{\prime\prime},M^{\prime\prime},A^{\prime\prime},X^{\prime\prime})$. Finally, we set $q^{\prime}=q^{\prime\prime}$ if $d^{\prime\prime}\cap{\equiv}^{\prime\prime}=\varnothing$; otherwise we have $q^{\prime}=q_{\mathsf{infeasible}}$.

• •

The first case to consider is when $\{[x]_{{\equiv}},[y]_{{\equiv}}\}\cap\bigcup\limits_{i=1}^{n}M_{i}=\varnothing$. In this case, we merge $[x]_{{\equiv}}$ and $[y]_{{\equiv}}$. More formally, ${\equiv}^{\prime\prime}$ is the smallest equivalence relation such that \big{(}{\equiv}\cup\{(x,y)\}\big{)}\subseteq{\equiv}^{\prime\prime}. Further, for every component $C\in\{X,A,N\}\cup\bigcup\limits_{i=1}^{n}\{Y_{i},M_{i}\}$ with the corresponding component in $q^{\prime\prime}$ being $C^{\prime\prime}$, and for every $z\in V_{\mathsf{Loc}}$ such that $z\notin[x]_{{\equiv}}\cup[y]_{{\equiv}}$, we have $[z]_{{\equiv}^{\prime\prime}}\in C^{\prime\prime}$ iff $[z]_{{\equiv}}\in C$. For a variable $z\in[x]_{{\equiv}}\cup[y]_{{\equiv}}$, we have $[z]_{{\equiv}^{\prime\prime}}\in C^{\prime\prime}$ iff $\{[x]_{{\equiv}},[y]_{{\equiv}}\}\cap C\neq\varnothing$. The other components of $q^{\prime\prime}$ are the same as in $q$ (modulo the new equivalence classes).

• •

Otherwise, consider the case when $[x]_{{\equiv}}\in M_{i}$ for some $i$. In this case, in addition to adding $\{(x,y)\}$ we also add the pair $\{(x,\mathsf{stop}_{i})\}$. Similarly if $[y]_{{\equiv}}\in M_{j}$ for some $j$ we add $\{(y,\mathsf{stop}_{j})\}$. Construct the state $q^{\prime\prime}$ with ${\equiv}^{\prime\prime}$ being the smallest equivalence relation including these new pairs (and other components remaining the same). 9. (9)

Case $s=\text{``}\textbf{assume}(x\neq y)\text{''}$, $x,y\in V_{\mathsf{Loc}}$. Similarly as above, in this case when $([x]_{{\equiv}},[y]_{{\equiv}})\in d$ we have $q^{\prime}=q$. If $[x]_{{\equiv}}=[y]_{{\equiv}}$ then $q^{\prime}=q_{\mathsf{infeasible}}$. Otherwise, we have the following cases:

• •

$[x]_{{\equiv}}=[\mathsf{stop}_{i}]_{{\equiv}}$ and $[y]_{{\equiv}}\in M_{i}$ for some $i$ (or vice versa). In this case, we simply put the equivalence class of $y$ into $Y_{i}$ and assert that $[y]_{{\equiv}}$ is unequal to all other classes. More formally, ${\equiv}^{\prime}={\equiv}$, $Y^{\prime}_{i}=Y_{i}\cup\{[y]_{{\equiv}}\}$ $d^{\prime}=d\cup\{([y]_{{\equiv}},[z]_{{\equiv}}),([z]_{{\equiv}},[y]_{{\equiv}})\,\mid\,z\notin[y]_{{\equiv}}\}$. The other components remain the same.

• •

Otherwise, we simply update $d^{\prime}=d\cup\{([x]_{{\equiv}},[y]_{{\equiv}})\}$; all other components are the same. 10. (10)

Case $s=\text{``}\textbf{assume}(a=b)\text{''}$, $a,b\in V_{\mathsf{Data}}$. In this case, we merge equivalence classes repeatedly and perform a ‘local congruence closure’. We construct a state $q^{\prime\prime}$ to determine if the transition must be to $q_{\mathsf{infeasible}}$. More formally, we define the state $q^{\prime\prime}$ with the ${\equiv}^{\prime\prime}$ component as the smallest equivalence relation such that:

(a) ${\equiv}\cup{(a,b)}\subseteq{\equiv}^{\prime\prime}$ (b) If $(u_{i},v_{i})\in{\equiv}$ for $1\leq i\leq r$ and $[w]_{{\equiv}^{\prime\prime}}=f([u_{1}]_{{\equiv}^{\prime\prime}}\ldots,[u_{r}]_{{\equiv}^{\prime\prime}}),[w^{\prime}]_{{\equiv}^{\prime\prime}}=f([v_{1}]_{{\equiv}^{\prime\prime}}\ldots,[v_{r}]_{{\equiv}^{\prime\prime}})$ then $(w,w^{\prime})\in{\equiv}^{\prime\prime}$.

The other components remain the same. In particular, it is correct to retain the $P$ component since the above construction is a congruence relation. Finally, if there exist $u,v\in V_{\mathsf{Data}}$ such that $(u,v)\in{\equiv}^{\prime\prime}$ and $([u]_{{\equiv}^{\prime\prime}},[v]_{{\equiv}^{\prime\prime}})\in d^{\prime\prime}$ then $q^{\prime}=q_{\mathsf{infeasible}}$. Otherwise, $q^{\prime}=q^{\prime\prime}$. 11. (11)

Case $s=\text{``}\textbf{assume}(a\neq b)\text{''}$, $a,b\in V_{\mathsf{Data}}$. Similarly as above, if $[a]_{{\equiv}}=[b]_{{\equiv}}$ then $q^{\prime}=q_{\mathsf{infeasible}}$. Otherwise, we update $d^{\prime}=d\cup\{([a]_{{\equiv}},[b]_{{\equiv}})\}$ and all other components remain the same.

The following theorem states the correctness of the automaton $\mathcal{A}_{\textsf{MS}}$.

Lemma 2.

Let $\sigma$ be a streaming-coherent execution and let $\varphi$ be a reachability specification and let $q$ be the state of the automaton $\mathcal{A}_{\textsf{MS}}$ after reading $\sigma$. Then, $q=q_{\mathsf{unsafe}}$ iff there is a forest data-structure $\mathcal{M}$ (with respect to $\varphi$) such that $\sigma$ violates memory safety on $\mathcal{M}$.

The problem of checking if a streaming-coherent program is memory safe against a given specification is decided as follows. Recall that the set of executions of a given program $P$ constitutes a regular language $\textsf{Exec}(P)$. Let $L(\mathcal{A}_{\textsf{MS}})$ be the set of executions $\sigma\in\Pi^{*}$ that do not go to the state $q_{\mathsf{unsafe}}$. Then, the problem of checking if $P$ is memory safe reduces to checking if $\textsf{Exec}(P)\subseteq L(\mathcal{A}_{\textsf{MS}})$.

Next, we show that the problem of checking streaming-coherence  is also decidable. To address the problem of checking streaming-coherence, we construct an automaton $\mathcal{A}_{\textsf{checkSC}}$ similar to $\mathcal{A}_{\textsf{MS}}$ (similar to the automaton for checking coherence  in (Mathur et al., 2019a)) that keeps track of the following information. For every function/pointer $f$ of arity $r$, and for every tuple $(x_{1},\ldots,x_{r})$ of variables (of appropriate sorts), each state of the automaton $\mathcal{A}_{\textsf{checkSC}}$ maintains a boolean predicate denoting whether or not $f(x_{1},\ldots,x_{r})$ has been computed in any execution that reaches the state. This gives us our next result.

Theorem 3**.**

The problem of checking whether a given program is streaming-coherent with respect to a given reach specification defining a forest data-structure is decidable in $\mathsf{PSPACE}$.

7. Implementation and Evaluation

We implemented a tool (Mathur et al., 2019c) for deciding memory safety of forest data-structures based on the construction from Section 6. The tool is ~2000 lines of Ocaml 4.07.0 code. It takes as input a program from the grammar presented in Section 2.1.1 annotated with a reachability specification, as in Section 5.1. The tool does not explicitly construct the automaton from Section 6. Instead, it implements a fixpoint algorithm, described below, which determines the set of states associated with every program point, and uses this set to check for memory safety.

7.1. Fixpoint Algorithm

Here we give a high-level description of the implementation. First, observe that $\mathcal{A}_{\textsf{MS}}$ has exponentially many states in the number of program variables.We manage this by implementing the transition $\delta$ from Section 6 and only building automaton states as they are encountered. For straight-line programs, each transition results in a single new state. For complex programs that use if-then-else and while statements, we need to keep track of a bag of states. To see this, suppose we are checking the program $\textbf{if}\,(c)\,\textbf{then}\,s_{1}\,\textbf{else}\,s_{2}$. To begin our bag of states contains only the initial state $q_{0}$. In order to process the if-then-else, the initial state needs to make two separate transitions, one for each of the two executions generated by the two branches. The bag of states thus grows to include $s_{\textsf{then}}=\delta(q_{0},\text{``}\textbf{assume}(c)\text{''})$ and $s_{\textsf{else}}=\delta(q_{0},\text{``}\textbf{assume}(\neg c)\text{''})$. The branches can then take transitions starting from $s_{\textsf{then}}$ and $s_{\textsf{else}}$. The union of the reachable states from each branch gives us a new bag of states from which to process the remaining program. The intuition for if-then-else carries over to while. From any state in our bag at the beginning of a while, we collect the bag of states that results from any number of executions of the loop guard and body, starting from that state. The number of states $|\mathcal{A}_{\textsf{MS}}|$ is finite, and thus a fixed point is guaranteed. For the benchmarks considered here, the number of states explored by the tool is significantly smaller than the worst case.

If at any point the tool detects a memory safety violation it halts and reports the error. In addition to memory safety, it also monitors the streaming-coherence property as it processes the input program. To do so, it keeps track of terms that were computed using existing equivalence classes, but which were subsequently dropped. If the program attempts to compute the same term using the same classes, the implementation flags a failure of streaming-coherence and halts. For example, to process $\text{``}a:=f(c)\text{''}$, the tool checks that $f$ was not previously applied to $[c]_{{\equiv}}$ and later dropped. In general, this information can be maintained by remembering the equivalence classes $[c_{1}]_{{\equiv}},\ldots,[c_{r}]_{{\equiv}}$ on which any function $f$ (of arity $r$) has been computed.

The algorithm implemented by the tool is more general than we have described thus far. It can output the set of states reached at the head of a loop. By interpreting individual states as conjunctions of equality and disequality, and the set of states as a disjunction of such conjuncts, we can obtain an inductive invariant that proves memory safety (when the program is memory safe). Any assertion in the form of a Boolean combination of equality statements on program variables can also be checked. This can be accomplished by appending the negated assertion to the end of the program and checking that all reachable states are infeasible.

7.2. Benchmarks

We seek to answer the following basic questions about streaming-coherent programs and our algorithm. First, is it the case that the most natural way to write heap-manipulating single-pass programs on lists and trees results in streaming-coherence? Second, for streaming-coherent programs with and without memory safety violations, is the algorithm able to verify memory safety or find violations of it in the corresponding uninterpreted program? Third, how fast is the algorithm? Note that since we do abstract the primitive types and functions/relations on real programs, it is not clear that the tool will be able to prove memory safe programs as so.

To answer the first and second questions, we wrote natural heap-manipulating programs over singly-linked lists (sorted and unsorted) and tree data-structures (binary search trees, AVL trees, rotations of trees) in our input language, and evaluated the tool on them to determine if they were streaming-coherentand to test for memory safety.

The first column of Table 1 gives the set of programs in our benchmark. These are typically single-pass algorithms over an input data-structure. For example, finding a key in a binary search tree or in-place reversal of a linked list are single pass algorithms.

The names of the programs indicate whether or not the program truly contains an unsafe memory access (i.e., the ground truth). Programs whose names end in ‘unsafe’ were obtained by introducing one of two possible memory safety errors into their ‘safe’ counterparts: (i) attempts to read or write to a location that is unallocated, and (ii) freeing unallocated memory locations.

One example of the first kind is illustrated in sll-copy-all, which copies the contents of a linked list into a freshly allocated list. In this example, the program steps through the input list in a loop until it reaches $\mathtt{NIL}$. In each iteration, a new node is allocated, initialized with the contents of the current node, and connected to the end of the new list. The program relies on the invariant that the new list has a next node to step to whenever the old list does. Thus, it does not perform a $\mathtt{NIL}$ check when advancing along the next pointer for the new list. The sll-copy-all-unsafe fails to maintain the invariant by incorrectly adding the freshly allocated node to the new list. An example for errors of the second kind (freeing memory locations that may not be allocated) can be found in sll-deletebetween-unsafe. In this example, the task is to delete all nodes in a linked list that have key values in a certain range. The mistake in this example happens when the program has found a node to delete, but, instead of saving the next node and deleting the current node, it instead frees the next node, which may be unallocated.

7.3. Discussion of Results

Table 1 shows the results for the evaluation, which was performed on a machine running Ubuntu 18.04 with an Intel i7 processor at 2.6 GHz. Columns 3-6 pertain to the operation of the algorithm on the benchmarks. Column 3 indicates whether or not the benchmark fails the streaming-coherence condition. Our tool terminates and identifies memory safety and violation of memory safety on all streaming-coherent programs. Column 4 depicts whether or not an unsafe memory access was detected. Column 5 gives the total number of states that are reachable at the end of the program. Note that non-streaming-coherence and violation of memory safety preclude each other in the table. Upon detecting either, the algorithm halts (and we do not report the number of reachable states). Column 6 gives the total running time of the tool on each benchmark, which is negligible in all cases. Note that the number of reachable states for each example is also quite small relative to the total number of possible states, which grows faster than the Bell numbers. That our algorithm only examines a small fraction of the total state space is encouraging, and suggests that it may scale well for much larger and more complex programs.

8. Related Work

Memory safety errors have attracted a lot of attention because they are serious security vulnerabilities that have been exploited to attack systems (Nagarakatte et al., 2015; Szekeres et al., 2013); they are one of the most common causes of security bugs (Microsoft, 2019). Memory safety concerns have even led to new programming languages, such as Rust (The Rust Team, 2019), that statically assure memory safety (while being efficient). Memory safety vulnerabilities of programs written in C/C++ are still of great concern, and, consequently, identifying fundamental techniques that establish decidability of the problem even for restricted classes of programs is interesting.

There is a rich literature of preventing memory safety errors at runtime by instrumenting code with runtime checks, or at compile time (see (Nagarakatte et al., 2015) and references therein, SafeC (Safe-C, 2019), CCured (Necula et al., 2002; Austin et al., 1994; Necula et al., 2005; Condit et al., 2003), Cyclone (Jim et al., 2002), SVA (Criswell et al., 2007), etc.). Static checking for memory safety is certainly possible when it is part of language design (for instance, using type systems as in Rust (Matsakis and Klock, 2014)). Dynamic analysis techniques as in (Nethercote and Seward, 2007; Rosu et al., 2009; Serebryany et al., 2012) instrument program executables and report errors as they occur during program execution. Recently, there has also been emerging interest in enforcing runtime memory safety using hardware and software support for tagged memory (Oleksenko et al., 2018; Joannou et al., 2017; lowRISC, 2019; Watson et al., 2015; Serebryany et al., 2018).

This work stems from the recent decidability result on uninterpreted coherent programs (Mathur et al., 2019a), which has also been extended to incorporate reasoning modulo theories including associativity and commutativity of functions over the data domain and ordering relations on the data domain (Mathur et al., 2019b). In our work we use automata-theoretic techniques that, over the data domain, reason about equality and function computation over the data elements. Further, for checking memory safety, our procedure tracks a subset of the allocated nodes, namely, the frontier nodes. While a considerable portion of the literature on assertion checking and memory safety for heap-manipulating programs is devoted to techniques that compromise on either soundness, completeness, or decidability, there has been some work that aims at decidable reasoning, while still preserving some form of soundness and completeness.

The work in (Alur and Černý, 2011) reduces assertion checking of single-pass list-processing programs to questions on data string transducers that work over sequences of tagged data values. The decidablity is mainly a consequence of the fact that there is a single variable that advances in a single-pass fashion. In contrast, our work defines a more general notion of single-pass programs using the streaming-coherence restriction that still allows for multiple variables to support pointer updates. Further, the work in (Alur and Černý, 2011) does not directly apply to verifying memory safety of programs as it does not explicitly handle freeing of memory locations, and the operations of the transducer cannot effect changes to the shape of the heap. Another key difference is that streaming data string transducers only allow reasoning about ordering and equality over data but cannot support more complex reasoning such as the congruence arising from function computation.

The work in (Bouajjani et al., 2006) proposes a class of list programs for which verification is decidable, and crucially relies on the idea of representing fragments of the allocated heap by a bounded number of segments and summaries about them, which is one among many other works (Sagiv et al., 1999; Bardin et al., 2004; Balaban et al., 2005; Berdine et al., 2004; Manevich et al., 2005; Dor et al., 2000) that employ a similar approach. These works can handle limited reasoning with data such as total orders on the data domain, but again, do not support predicates like equality on data or function congruences resulting from equalities, and further, often address questions specific to lists. Our work, on the other hand, tackles the more general problem of the verification of uninterpreted heap programs and instantiates the alias-aware  condition to the class of forest data-structures. The key idea of tracking the frontier heap locations, which we use for obtaining decidability of streaming-coherent  programs, appears orthogonal to this line of work.

The work in (Bozga and Iosif, 2007) differs fundamentally from ours in that pointer updates are forbidden, which is a salient feature of our work. Pointer updates are at the heart of the difficulty in building a theory of uninterpreted programs working over heaps. Additionally, that work forbids nesting of loops as well as conditionals within loops, a restriction also used to obtain decidability in earlier work (Godoy and Tiwari, 2009) on uninterpreted programs; there is no such syntactic restriction on the class of programs we introduce in this paper.

The work in (Bouajjani et al., 2005) over-approximates the set of heap configurations associated with a given program location as a regular language over a finite alphabet. The program transformations are represented by finite state transducers, and the work employs an abstraction refinement approach for verifying heap-manipulating programs. Since such abstraction refinement loops may not always terminate for arbitrary programs, the proposed approach is only a semi-decision procedure. Further, this work does not support reasoning over the data sort. Other notable static analyses that employ abstraction refinement for verifying heap programs include the notable work on shape analysis (Sagiv et al., 1999; Yahav, 2001; Lev-Ami and Sagiv, 2000) and automatic predicate abstraction (Ball et al., 2001). Statically verifying memory safety using such incomplete techniques can of course, and commonly does, result in false positives.

There is a rich literature on program logics for heap verification; in particular separation logics  (O’Hearn et al., 2001; Reynolds, 2002) and FO logics based on the principles of separation logic (Løding et al., 2019). Decidable fragments of such logics have also been studied (Berdine et al., 2004; Piskac et al., 2014b, a, 2013; Navarro Pérez and Rybalchenko, 2013, 2011; Berdine et al., 2006; Cook et al., 2011; Møller and Schwartzbach, 2001). However, typically, these decision procedures are for checking validity of Hoare triples, and the problem of generating loop invariants is often undecidable, as is the problem of completely automatic verification of programs against specifications expressed in these logics. Some invariant generation techniques have been discovered for problems in this domain (Calcagno et al., 2011; Neider et al., 2018), but are, of course, inherently incomplete.

9. Conclusions and Future Work

This paper establishes a foundational result for decidably verifying assertions in programs that update maps for a subclass that is alias-aware and coherent. We have used this general result to develop decidable verification of memory safety for a class of programs, called streaming-coherent programs, working on forest data-structures. We also proved membership of programs in this class is decidable. We showed through a prototype implementation of our decision procedure, and its evaluation on a set of single-pass algorithms, that forest data-structures typically fall in our decidable class, and that we can verify memory safety accurately for them.

The most compelling future direction is to adapt the technique in this paper to provide a memory safety analysis tool for a standard programming language (such as C/C++), handling the rest of the programming language using abstractions (e.g., arrays, allocation of varying blocks of memory, etc.). We believe that our automata-based algorithm will scale well. Realizing the techniques presented herein in a full-fledged memory safety analysis tool would be interesting.

On the theoretical front, there are several interesting directions. First, we could ask how to generalize our results to go beyond streaming-coherent  programs on forest data-structures. Although forest data-structures are fairly common as initial heaps for many programs, finding a natural class of heap structures beyond forest data-structures where alias-awareness can be easily established seems an interesting, challenging problem. We believe that data-structures such as doubly-linked lists and trees with parent pointers, and more generally, data-structures that have bounded tree-width with uniform tree decompositions may be amenable to our technique. Tackling multi-pass algorithms on forest data-structures is also an interesting open direction. We believe the best way to look at our work in a larger verification context is that single-pass streaming-coherent programs are the new basic blocks that can be completely automatically analyzed, despite the fact that they contain loops. Putting these blocks together to handle programs with multiple passes over data-structures, even in an incomplete fashion, is an interesting future direction.

Another dimension for exploration is to consider more general post-conditions that can be proved automatically and that go beyond simple assertions. One of the limitations of our work is that, though we have an implicit precondition that demands that data-structures are forests, we do not establish that the data-structure in the post state is also a forest. The ability to establish such a property will allow us to maintain the forest property of data-structures as an invariant across multiple calls from clients that manipulate a data-structure using a library of methods, by showing that each of the methods provably maintains this invariant.

Acknowledgements.

We thank the anonymous reviewers of POPL for several comments that helped improve the paper. Umang Mathur is partially supported by a Google PhD Fellowship. This material is based upon work supported by the National Science Foundation under Grants NSF CCF 1901069 and NSF CCF 1527395.