11institutetext: École Normale Supérieure,
PSL Research University, Paris, France 22institutetext: AdaCore, Paris, France
33institutetext: Laboratoire de Recherche en Informatique,
Université Paris-Sud, CNRS, Orsay, F-91405 44institutetext: Inria Saclay,
Université Paris Saclay, Palaiseau, F-91120

# Borrowing Safe Pointers from Rust in SPARK

Georges-Axel Jaloyan This work is partly supported by the Joint Laboratory
ProofInUse (ANR-13-LAB3-0007) and project VECOLIB (ANR-14-CE28-0018) of the
French National Research Agency (ANR).11 Yannick Moy 22 Andrei Paskevich 3344

###### Abstract

In the field of deductive software verification, programs with pointers
present a major challenge due to pointer aliasing. In this paper, we introduce
pointers to SPARK, a well-defined subset of the Ada language, intended for
formal verification of mission-critical software. Our solution uses a
permission-based static alias analysis method inspired by Rust’s _borrow-
checker_ and _affine types_ , and enforces the Concurrent Read, Exclusive
Write policy. This analysis has been implemented in the GNAT Ada compiler and
tested against a number of challenging examples. In the paper, we give a
formal presentation of the analysis rules for a miniature version of SPARK and
prove their soundness. We discuss the implementation and compare our solution
with Rust.

##  1 Introduction

SPARK [1] is a subset of the Ada programming language targeted at safety- and
security-critical applications. SPARK restrictions ensure that the behavior of
a SPARK program is unambiguously defined, and simple enough that formal
verification tools can perform an automatic diagnosis of conformance between a
program specification and its implementation.

As a consequence of SPARK’s focus on automation and usability, it forbids the
use of programming language features that either prevent automatic proof, or
make it possible only at the expense of extensive user effort in annotating
the program. The lack of support for pointers in SPARK is the main example of
this choice. While it is possible to exclude parts of the programs that
manipulate pointers from analysis, it would be preferable to support pointers
when their use does not prevent formal verification.

Among the various problems related to the use of pointers in the context of
formal program verification, the most difficult problem is the possibility
that two names refer to overlapping memory locations, a.k.a. aliasing. Formal
verification platforms that support pointer aliasing like Frama-C [2] require
users to annotate programs to specify when pointers are not aliased. This can
take the form of inequalities between pointers when a typed memory model is
used, or the form of separation predicates between memory zones when an
untyped memory model is used. In both cases, the annotation burden is
acceptable for leaf functions which manipulate single-level pointers, and
quickly becomes overwhelming for functions that manipulate pointer-rich data
structures. In parallel to the increased cost of annotations, the benefits of
automation decrease, as automatic provers have difficulties reasoning
explicitly with these inequalities and separation predicates.

Programs often rely on non-aliasing in general for correctness, when such
aliasing would introduce interferences between two unrelated names. We call
such aliasing _potentially harmful_ when a memory location modified through
one name could be read through another name, within the scope of a
verification condition. Otherwise, the aliasing is _benign_ , when the memory
location is only read through both names. A reasonable restriction for formal
program verification is thus to forbid potentially harmful aliasing of names.
The difficulty is then to guarantee the absence of potentially harmful
aliasing. The following code shows an example where we want analysis to be
able to rely on the non-aliasing of parameters `X` and `Y` to prove the
postcondition of the procedure `Assign_Incr`:

⬇

procedure Assign_Incr (X, Y : in out Integer_Pointer)

with Post => Y.all = X.all + 1

is

begin

Y.all := X.all + 1;

end Assign_Incr;

In this work, we present the first step for the inclusion of pointers in the
Ada language subset supported in SPARK. As our main contribution, we show that
it is possible to borrow and adapt the ideas underlying the safe support for
pointers in permission-based languages like Rust, to safely restrict the use
of pointers in usual imperative languages like Ada. This adaptation is based
on a possible division of work between a permission-based anti-aliasing
analysis, lifetime management by typing, and the use of a formal verification
platform for checking non-nullity of accessed pointers. For example, these
rules prevent aliasing between parameters `X` and `Y` in the code of procedure
`Assign_Incr` above, which makes it possible to treat pointers in proof like
records with a single field corresponding to the type of the object pointed
to. Thus, the verification condition corresponding to the postcondition of
procedure `Assign_Incr` has a form (using `get`/`set` to access the field
`all` of variables `X` and `Y`) that can readily be proved by automatic
provers:

     hypothesis: Y’ = set(Y, all, get(X, all) + 1)
     goal:       get(Y’, all) = get(X, all) + 1

In Section 2, we present a formalization of the non-aliasing rules enforced by
the permission-based analysis, including proof of non-aliasing guarantees. In
Section 3, we describe a concrete implementation of the analysis inside the
open-source GNAT compiler for Ada which is part of GCC. We survey related
works in Section 4, in particular with respect to Rust.

##  2 Alias Analysis

In Ada/SPARK code, the access to memory areas is given through _paths_ that
start with an identifier (a variable name) and follow through record fields,
array indices, or through a special field all, which corresponds to pointer
dereferencing. In this paper, we only consider record and pointer types, and
discuss the treatment of arrays in Section 3.

As an example, we use the following Ada type, describing singly linked lists
where each node carries a boolean flag and a pointer to a shared integer
value.

⬇

type List is record

Flag : Boolean;

Key : access Integer;

Next : access List;

end record;

Given a variable A : List, the paths A.Flag, A.Key.all, A.Next.all.Key are
valid and their respective types are Boolean, Integer, and access Integer (a
pointer to an Integer). The important difference between pointers and records
in Ada is that—similarly to C—assignment of a record copies the values of
fields, whereas assignment of a pointer only copies the address and creates an
alias.

The alias analysis procedure runs after the type checking. The idea is to
associate one of the four permissions—$\mathsf{RW}$, $\mathsf{R}$,
$\mathsf{W}$ or $\mathsf{NO}$—to each possible path (starting from the
available variables) at each sequence point in the program.

The _read-only_ permission $\mathsf{R}$ allows us to read any value accessible
from the path: use it in a computation, or pass it as an in parameter in a
procedure call. As a consequence, if a given path has the $\mathsf{R}$
permission, then each valid extension of this path also has it.

The _write-only_ permission $\mathsf{W}$ allows us to modify memory occupied
by the value: use it on the left-hand side in an assignment or pass it as an
out parameter in a procedure call. For example, having a write permission for
a path of type List allows us to modify the Flag field or to change the
addresses stored in the pointer fields Key and Next. However, this does not
necessarily give us the permission to modify memory accessible from those
pointers. Indeed, to dereference a pointer, we must read the address stored in
it, which requires the read permission. Thus, the $\mathsf{W}$ permission only
propagates to path extensions that do not dereference pointers, i.e., do not
contain additional all fields.

The _read-write_ permission $\mathsf{RW}$ combines the properties of the
$\mathsf{R}$ and $\mathsf{W}$ permissions and grants the full ownership of the
path and every value accessible from it. In particular, the $\mathsf{RW}$
permission propagates to all valid path extensions including those that
dereference pointers. The $\mathsf{RW}$ permission is required to pass a value
as an in-out parameter in a procedure call.

Execution of program statements changes permissions. For example, allocating a
new non-initialised memory area assigns the $\mathsf{W}$ permission to every
value stored in this area. Thus, after the statement P := new List, the paths
P, P.all, P.all.Flag, P.all.Key, and P.all.Next have permission $\mathsf{W}$.
All strict extensions of P.all.Key and P.all.Next receive permission
$\mathsf{NO}$, that is, no permission. Indeed, since the pointers P.all.Key
and P.all.Next are not initialised, neither reads nor writes under them make
any sense. Another simple example of permission change is the procedure call:
all out parameters must be assigned by the callee and receive the
$\mathsf{RW}$ permission after the call.

The assignment statement is more complicated and several cases must be
considered. If we assign a value that does not contain pointers (say, an
integer or a pointer-free record), the whole value is copied into the left-
hand side, and we only need to check that we have the appropriate permissions:
$\mathsf{W}$ or $\mathsf{RW}$ for the left-hand side and $\mathsf{R}$ or
$\mathsf{RW}$ for the right-hand side. However, whenever we copy a pointer, an
alias is created. We want to make the left-hand side the new full owner of the
value (i.e., give it the $\mathsf{RW}$ permission), and therefore, after the
permission checks, we must revoke the permissions from the right-hand side, to
avoid potentially harmful aliasing. The permission checks are also slightly
different in this case, as we require the right-hand side to have the
$\mathsf{RW}$ permission in order to move it to the left-hand side.

Let us now consider several simple programs and see how the permission checks
allow us to detect potentially harmful aliasing.

⬇

procedure P1

(A,B: in out List) is

begin

A := B;

B.Flag := True;

B.Key.all := 42;

end P1;

⬇

procedure P2

(A,B: in out Integer_Pointer) is

begin

while B.all > 0 loop

A.all := A.all + 1;

B.all := B.all - 1;

A := B;

end loop;

end P2;

Figure 1: Examples of potentially harmful aliasing.

Procedure P1 in Fig. 1 receives two in-out parameters A and B of type List. At
the start of the procedure, all in-out parameters assume permission
$\mathsf{RW}$. In particular, this implies that each in-out parameter is
separated from all other parameters (in fact, only the in parameters may alias
each other). The first assignment copies the structure B into A. Thus, the
paths A.Flag, A.Key, and A.Next are separated, respectively, from B.Flag,
B.Key, and B.Next. However, the paths A.Key.all and B.Key.all are aliased, and
A.Next.all and B.Next.all are aliased as well.

The first assignment does not change the permissions of A and its extensions:
they retain the $\mathsf{RW}$ permission and keep the full ownership of their
respective memory areas, even if the areas themselves have changed. The paths
under B, however, must relinquish (some of) their permissions. The paths
B.Key.all and B.Next.all as well as all their extensions get the $\mathsf{NO}$
permission, that is, lose both read and write permissions. This is necessary,
as the ownership over their memory areas is transferred to the corresponding
paths under A. The paths B, B.Key, and B.Next lose the read permission but
keep the write-only $\mathsf{W}$ permission. Indeed, we forbid reading from
memory that can be altered through a concurrent path. However, it is allowed
to “redirect” the pointers B.Key and B.Next, either by assigning those fields
directly or by copying some different record into B. The field B.Flag is not
aliased, nor has it aliased extensions, and thus retains the initial
$\mathsf{RW}$ permission. This $\mathsf{RW}$ permission allows us to perform
the assignment B.Flag := True on the next line.

The third assignment, however, is now illegal, since B.Key.all does not have
the write permission anymore. What is more, at the end of the procedure the
in-out parameters A and B are not separated. This is forbidden, as the caller
assumes that all out and in-out parameters are separated after the call just
as they were before.

Procedure P2 in Fig. 1 receives two pointers A and B, and manipulates them
inside a while loop. Since the permissions are assigned statically, we must
ensure that at the end of a single iteration, we did not lose the permissions
necessary for the next iteration. This requirement is violated in the example:
after the last assignment A := B, the path B receives permission $\mathsf{W}$
and the path B.all, permission $\mathsf{NO}$, as B.all is now an alias of
A.all. The new permissions for B and B.all are thus weaker than the original
ones ($\mathsf{RW}$ for both), and the procedure is rejected. Should it be
accepted, we would have conflicting memory modifications from two aliased
paths at the beginning of the next iteration.

###  2.1 $\mu$SPARK language

For the purposes of formal presentation, we introduce $\mu$SPARK, a small
subset of SPARK featuring pointers, records, loops, and procedure calls. We
present the syntax and semantics of $\mu$SPARK, and define the rules for
static analysis of alias safety.

The data types of $\mu$SPARK are as follows:

$\begin{array}[]{rclcl}type&\>::=&\texttt{Integer}\>\>|\>\>\texttt{Real}\>\>|\>\>\texttt{Boolean}&&\text{scalar
type}\\\ &|&\texttt{access}\>\>type&&\text{access type (pointer)}\\\
&|&ident&&\text{record type}\end{array}$

Every $\mu$SPARK program starts with a list of record type declarations:

$\begin{array}[]{rcl}record&\>::=&\texttt{type}\>\>ident\>\>\texttt{is}\>\>\texttt{record}\>\>field^{\star}_{\texttt{;}}\>\>\texttt{end}\\\\[4.30554pt]
field&\>::=&ident\>\>\texttt{:}\>\>type\end{array}$

We require all field names to be distinct. The field types must not refer to
the record types declared later in the list. Recursive record types are
allowed: a field of a record type $R$ can contain pointers to $R$ (written
access $R$). We discuss the handling of array types in Section 3.

The syntax of $\mu$SPARK statements is defined by the following rules:

$\begin{array}[]{rclcl}path&\>::=&ident&&\text{variable}\\\
&|&path\,\texttt{.}\,ident&&\text{record field}\\\
&|&path\,\texttt{.}\,\texttt{all}&&\text{pointer dereference}\\\\[8.61108pt]
expr&\>::=&path&&\text{l-value}\\\
&|&\texttt{42}\;|\;\texttt{3.14}\;|\;\texttt{True}\;|\;\texttt{False}\;|\;\ldots&&\text{scalar
value}\\\
&|&expr\>\>(\,\texttt{+}\,|\,\texttt{-}\,|\,\texttt{<}\,|\,\texttt{=}\,|\,\ldots\,)\>\>expr&&\text{binary
operator}\\\ &|&path\texttt{'Access}&&\text{address of an l-value}\\\
&|&\texttt{null}&&\text{null pointer}\\\\[8.61108pt]
stmt&\>\>::=&path\>\>\texttt{:=}\;\;expr&&\text{assignment}\\\
&|&path\>\>\texttt{:=}\;\;\texttt{new}\>\>type&&\text{allocation}\\\
&|&\texttt{if}\>\>expr\>\>\texttt{then}\>\>stmt^{\star}_{\texttt{;}}\>\>\texttt{else}\>\>stmt^{\star}_{\texttt{;}}\>\>\texttt{end}&&\text{conditional}\\\
&|&\texttt{while}\>\>expr\>\>\texttt{loop}\>\>stmt^{\star}_{\texttt{;}}\>\>\texttt{end}&&\text{``while''
loop}\\\
&|&ident\>\>\texttt{(}\>\>{expr}^{\star}_{\texttt{,}}\>\>\texttt{)}&&\text{procedure
call}\end{array}$

Following the record type declarations, a $\mu$SPARK program contains a set of
mutually recursive procedure declarations:

$\begin{array}[]{rcl}procedure&\>::=&\texttt{procedure}\>\>ident\>\>\texttt{(}\>\>param^{\star}_{\texttt{;}}\>\>\texttt{)}\>\>\texttt{is}\>\>local^{\star}_{\texttt{;}}\>\>\texttt{begin}\>\>stmt^{\star}_{\texttt{;}}\>\>\texttt{end}\\\\[4.30554pt]
param&\>::=&ident\>\>\texttt{:}\>\>(\,\texttt{in}\>|\>\texttt{in-
out}\>|\>\texttt{out}\,)\>\>type\\\\[4.30554pt]
local&\>::=&ident\>\>\texttt{:}\>\>type\end{array}$

We require all formal parameters and local variables in a procedure to have
distinct names. A procedure call can only pass left-values (i.e., paths) for
in-out and out parameters. The execution starts from a procedure named Main
with the empty parameter list.

The type system for $\mu$SPARK is rather standard and we do not present it
here in full. We assume that binary operators only operate on scalar types.
The null pointer can have any pointer type access $\tau$. The dereference
operator .all converts a pointer type access $\tau$ to $\tau$. The access
operator ’Access applied to an l-value of type $\tau$ returns the
corresponding pointer type access $\tau$. The allocation statement $p$ := new
$\tau$ requires the path $p$ to have type access $\tau$. In what follows, we
only consider well-typed $\mu$SPARK programs.

On the semantic level, we need to distinguish the units of allocation, such as
whole records, from the units of access, such as individual record fields. We
use the term _location_ to refer to the memory area occupied by an allocated
value. We treat locations as elements of an abstract infinite set, and denote
them with letter $\ell$. We use the term _address_ to designate either a
location, denoted $\ell$, or a specific component inside the location of a
record, denoted $\ell.f.g$, where $f$ and $g$ are field names (assuming that
at $\ell$ we have a record whose field $f$ is itself a record with a field
$g$). A _value_ is either a scalar, an address, a null pointer or a record,
that is, a finite mapping from field names to values.

A $\mu$SPARK program is executed in the context defined by a _binding_
$\Upsilon$ that maps variable names to addresses and a _store_ $\Sigma$ that
maps locations to values. By a slight abuse of notation, we apply $\Sigma$ to
arbitrary addresses, so that $\Sigma(\ell.f)$ is $\Sigma(\ell)(f)$, the value
of the field $f$ of the record value stored in $\Sigma$ at $\ell$. Similarly,
we write $\Sigma[\ell.f\mapsto v]$ to denote an update of a single field in a
record, that is, $\Sigma[\ell\mapsto\Sigma(\ell)[f\mapsto v]]$.

We use big-step operational semantics and write $\Upsilon\cdot\Sigma\cdot
s\Downarrow\Sigma^{\prime}$ to denote that $\mu$SPARK statement $s$, when
evaluated under binding $\Upsilon$ and store $\Sigma$, terminates with the
state of the store $\Sigma^{\prime}$. We extend this notation to sequences of
statements $\bar{s}$ in an obvious way. In this paper, we do not consider
diverging statements.

The evaluation of expressions is effect-free and is denoted $\llbracket
e\rrbracket^{\Upsilon}_{\Sigma}$. We also need to evaluate l-values to the
corresponding addresses in the store, written $\langle
p\rangle^{\Upsilon}_{\Sigma}$, where $p$ is the evaluated path. Illicit
operations, such as dereferencing a null pointer, cannot be evaluated and
stall the execution (_blocking semantics_). In the formal rules below, $c$
stands for a scalar constant and $\odot$, for a binary operator:

$\displaystyle\langle x\rangle^{\Upsilon}_{\Sigma}$
$\displaystyle=\Upsilon(x)$ $\displaystyle\langle
p.f\rangle^{\Upsilon}_{\Sigma}$ $\displaystyle=\langle
p\rangle^{\Upsilon}_{\Sigma}.f$ $\displaystyle\langle
p.\texttt{all}\rangle^{\Upsilon}_{\Sigma}$ $\displaystyle=\llbracket
p\rrbracket^{\Upsilon}_{\Sigma}$ $\displaystyle\llbracket
c\rrbracket^{\Upsilon}_{\Sigma}$ $\displaystyle=c$ $\displaystyle\llbracket
p\rrbracket^{\Upsilon}_{\Sigma}$ $\displaystyle=\Sigma(\langle
p\rangle^{\Upsilon}_{\Sigma})$ $\displaystyle\llbracket
p\texttt{'Access}\rrbracket^{\Upsilon}_{\Sigma}$ $\displaystyle=\langle
p\rangle^{\Upsilon}_{\Sigma}$ $\displaystyle\llbracket e_{1}\odot
e_{2}\rrbracket^{\Upsilon}_{\Sigma}$ $\displaystyle=\llbracket
e_{1}\rrbracket^{\Upsilon}_{\Sigma}\odot\llbracket
e_{2}\rrbracket^{\Upsilon}_{\Sigma}$
$\displaystyle\llbracket\texttt{null}\rrbracket^{\Upsilon}_{\Sigma}$
$\displaystyle=\texttt{null}$

Allocation adds a fresh address to the store, mapping it to a default value
for the corresponding type: 0 for Integer, False for Boolean, null for the
access types, and for the record types, a record value where each field has
the default value. Notice that since pointers are initialised to null, there
is no deep allocation. We write $\Box_{\tau}$ to denote the default value of
type $\tau$.

The evaluation rules are given in Figure 2. In the (E-call) rule, we evaluate
the procedure body in the dedicated context $\Upsilon_{P}\cdot\Sigma_{P}$.
This context binds the in parameters to fresh locations containing the values
of the respective expression arguments, binds the in-out and out parameters to
the addresses of the respective l-value arguments, and allocates memory for
the local variables. For simplicity, we do not reclaim memory on return from a
procedure call, and thus avoid dangling pointers. In Ada and SPARK, this issue
is handled separately, using scope-based memory pools, and does not need to be
addressed by our analysis procedure.

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\llbracket
e\rrbracket^{\Upsilon}_{\Sigma}=v\end{array}}{\begin{array}[]{@{}c@{}}\Upsilon\cdot\Sigma\cdot
p\,\texttt{:=}\,e\>\Downarrow\>\Sigma[\,\langle
p\rangle^{\Upsilon}_{\Sigma}\mapsto v\,]\end{array}}$ (E-assign)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\ell\not\in
dom\>\Sigma\end{array}}{\begin{array}[]{@{}c@{}}\Upsilon\cdot\Sigma\cdot
p\,\texttt{:=}\,\texttt{new}\,\tau\>\Downarrow\>\Sigma[\,\langle
p\rangle^{\Upsilon}_{\Sigma}\mapsto\ell,\,\ell\mapsto\Box_{\tau}\,]\end{array}}$
(E-alloc)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\llbracket
e\rrbracket^{\Upsilon}_{\Sigma}=\texttt{True}\qquad\Upsilon\cdot\Sigma\cdot\bar{s}_{1}\>\Downarrow\>\Sigma^{\prime}\end{array}}{\begin{array}[]{@{}c@{}}\Upsilon\cdot\Sigma\cdot\text{{if
$e$ then $\bar{s}_{1}$ else
$\bar{s}_{2}$}}\>\Downarrow\>\Sigma^{\prime}\end{array}}$ (E-ifTrue)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\llbracket
e\rrbracket^{\Upsilon}_{\Sigma}=\texttt{False}\qquad\Upsilon\cdot\Sigma\cdot\bar{s}_{2}\>\Downarrow\>\Sigma^{\prime}\end{array}}{\begin{array}[]{@{}c@{}}\Upsilon\cdot\Sigma\cdot\text{{if
$e$ then $\bar{s}_{1}$ else
$\bar{s}_{2}$}}\>\Downarrow\>\Sigma^{\prime}\end{array}}$ (E-ifFalse)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\llbracket
e\rrbracket^{\Upsilon}_{\Sigma}=\texttt{True}\qquad\Upsilon\cdot\Sigma\cdot(\text{{$\bar{s}$
; while $e$ loop $\bar{s}$
end}})\>\Downarrow\>\Sigma^{\prime}\end{array}}{\begin{array}[]{@{}c@{}}\Upsilon\cdot\Sigma\cdot\text{{while
$e$ loop $\bar{s}$ end}}\>\Downarrow\>\Sigma^{\prime}\end{array}}$
(E-whileTrue)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\llbracket
e\rrbracket^{\Upsilon}_{\Sigma}=\texttt{False}\end{array}}{\begin{array}[]{@{}c@{}}\Upsilon\cdot\Sigma\cdot\text{{while
$e$ loop $\bar{s}$ end}}\>\Downarrow\>\Sigma\end{array}}$ (E-whileFalse)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\texttt{procedure}\>P\>\texttt{(}\,a_{1}\,\texttt{:}\,\texttt{in}\>\tau_{a_{1}}\texttt{;}\ldots\texttt{;}\,b_{1}\,\texttt{:}\,\texttt{in-
out}\>\tau_{b_{1}}\texttt{;}\ldots\texttt{;}\,c_{1}\,\texttt{:}\,\texttt{out}\>\tau_{c_{1}}\texttt{;}\ldots\texttt{)}\\\
\text{~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}}\texttt{is}\;d_{1}\,\texttt{:}\,\tau_{d_{1}}\texttt{;}\ldots\>\texttt{begin}\;\bar{s}\;\texttt{end}\text{~{}~{}is
declared in the program}\\\\[4.30554pt]
\ell_{a_{1}},\ldots,\ell_{d_{1}},\ldots\not\in
dom\>\Sigma\qquad\qquad\llbracket
e_{a_{1}}\rrbracket^{\Upsilon}_{\Sigma},\ldots=v_{a_{1}},\ldots\\\\[4.30554pt]
\Upsilon_{P}=[\,a_{1}\mapsto\ell_{a_{1}},\ldots,b_{1}\mapsto\langle
p_{b_{1}}\rangle^{\Upsilon}_{\Sigma},\ldots,c_{1}\mapsto\langle
q_{c_{1}}\rangle^{\Upsilon}_{\Sigma},\ldots,d_{1}\mapsto\ell_{d_{1}},\ldots\,]\\\\[4.30554pt]
\Sigma_{P}=\Sigma[\,\ell_{a_{1}}\mapsto
v_{a_{1}},\ldots,\ell_{d_{1}}\mapsto\Box_{\tau_{d_{1}}},\ldots\,]\qquad\qquad\Upsilon_{P}\cdot\Sigma_{P}\cdot\bar{s}\>\Downarrow\>\Sigma^{\prime}\end{array}}{\begin{array}[]{@{}c@{}}\Upsilon\cdot\Sigma\cdot
P(e_{a_{1}},\ldots,p_{b_{1}},\ldots,q_{c_{1}},\ldots)\Downarrow\Sigma^{\prime}\end{array}}$
(E-call)

Figure 2: Semantics of $\mu$SPARK (terminating statements).

###  2.2 Access policies, transformers, and alias safety rules

We denote paths with letters $p$ and $q$. We write $p\sqsubset q$ to denote
that $p$ is a strict _prefix_ of $q$ or, equivalently, $q$ is a strict
_extension_ of $p$. In what follows, we always mean strict prefixes and
extensions, unless explicitly said otherwise.

In the typing context of a given procedure, a well-typed path is said to be
_deep_ if it has an extension of an access type, otherwise it is called
_shallow_. We extend these notions to types: a type $\tau$ is deep (resp.
shallow) if and only if a $\tau$-typed path is deep (resp. shallow). In other
words, a path or a type is deep if a pointer can be reached from it, and
shallow otherwise. For example, the List type in Section 2 is a deep type, and
so is access Integer, whereas any scalar type or any record with scalar fields
only is shallow.

An extension $q$ of a path $p$ is called a _near extension_ if it has as many
pointer dereferences as $p$, otherwise it is a _far extension_. For instance,
given a variable A of type List, the paths A.Flag, A.Key, and A.Next are the
near extensions of A, whereas A.Key.all, A.Next.all, and their extensions are
far extensions, since they all create an additional pointer dereference by
passing through all.

We say that _sequence points_ are the program points before or after a given
statement. For each sequence point in a given $\mu$SPARK program, we
statically compute an _access policy_ : a partial function that maps each
well-typed path to one of the four _permissions_ : $\mathsf{RW}$,
$\mathsf{R}$, $\mathsf{W}$, and $\mathsf{NO}$, which form a diamond lattice:
$\mathsf{RW}>\mathsf{R}|\mathsf{W}>\mathsf{NO}$. We denote permissions with
$\pi$ and access policies with $\Pi$.

Permission transformers modify policies at a given path, as well as its
prefixes and extensions. Symbolically, we write
$\Pi\xrightarrow{T}_{p}\Pi^{\prime}$ to denote that policy $\Pi^{\prime}$
results from application of transformer $T$ to $\Pi$ at path $p$. We write
$\Pi\xrightarrow{T_{1}\fatsemi\,T_{2}}_{p}\Pi^{\prime}$ as an abbreviation for
$\Pi\xrightarrow{T_{1}}_{p}\fatsemi\xrightarrow{T_{2}}_{p}\Pi^{\prime}$ (that
is, for some $\Pi^{\prime\prime}$,
$\Pi\xrightarrow{T_{1}}_{p}\Pi^{\prime\prime}\xrightarrow{T_{2}}_{p}\Pi^{\prime}$).
We write $\Pi\xrightarrow{T}_{p,q}\Pi^{\prime}$ as an abbreviation for
$\Pi\xrightarrow{T}_{p}\fatsemi\xrightarrow{T}_{q}\Pi^{\prime}$.

Permission transformers can also apply to expressions, which consists in
updating the policy for every path in the expression. This only includes paths
that occur as sub-expressions: in an expression X.f.g + Y.h, only the paths
X.f.g and Y.h are concerned, whereas X, X.f and Y are not. The order in which
the individual paths are treated must not affect the final result.

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Pi\xrightarrow{\mathrm{move}}_{e}\fatsemi\xrightarrow{\mathrm{check}\>\mathsf{W}\>\fatsemi\>\mathrm{fresh}\>\mathsf{RW}\>\fatsemi\>\mathrm{lift}}_{p}\Pi^{\prime}\end{array}}{\begin{array}[]{@{}c@{}}\Pi\cdot
p\,\texttt{:=}\,e\rightarrow\Pi^{\prime}\end{array}}$ (P-assign)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Pi\xrightarrow{\mathrm{check}\>\mathsf{W}}_{p}\fatsemi\xrightarrow{\mathrm{fresh}\>\mathsf{W}\>\fatsemi\>\mathrm{cut}\>\fatsemi\>\mathrm{block}}_{p.\texttt{all}}\Pi^{\prime}\end{array}}{\begin{array}[]{@{}c@{}}\Pi\cdot
p\,\texttt{:=}\,\texttt{new}\>\>\tau\rightarrow\Pi^{\prime}\end{array}}$
(P-alloc)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Pi\xrightarrow{\mathrm{check}\>\mathsf{R}}_{e}\Pi\quad\quad\Pi\cdot\bar{s}_{1}\rightarrow\Pi_{1}\quad\quad\Pi\cdot\bar{s}_{2}\rightarrow\Pi_{2}\quad\quad\forall
p.\,\Pi^{\prime}(p)=\Pi_{1}(p)\land\Pi_{2}(p)\end{array}}{\begin{array}[]{@{}c@{}}\Pi\cdot\texttt{if}\;e\,\>\texttt{then}\;\bar{s}_{1}\;\texttt{else}\;\bar{s}_{2}\;\texttt{end}\rightarrow\Pi^{\prime}\end{array}}$
(P-if)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Pi\xrightarrow{\mathrm{check}\>\mathsf{R}}_{e}\Pi\quad\quad\Pi\cdot\bar{s}\rightarrow\Pi^{\prime}\quad\quad\forall\pi.\,\Pi^{\prime}(\pi)\geqslant\Pi(\pi)\end{array}}{\begin{array}[]{@{}c@{}}\Pi\cdot\texttt{while}\;e\,\>\texttt{loop}\;\bar{s}\;\texttt{end}\rightarrow\Pi\end{array}}$
(P-while)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\texttt{procedure}\>P\>\texttt{(}\,a_{1}\,\texttt{:}\,\texttt{in}\>\tau_{a_{1}}\texttt{;}\ldots\texttt{;}\,b_{1}\,\texttt{:}\,\texttt{in-
out}\>\tau_{b_{1}}\texttt{;}\ldots\texttt{;}\,c_{1}\,\texttt{:}\,\texttt{out}\>\tau_{c_{1}}\texttt{;}\ldots\texttt{)}\\\
\text{~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}}\texttt{is}\;\cdots\>\texttt{begin}\;\bar{s}\;\texttt{end}\text{~{}~{}is
declared in the program}\\\\[4.30554pt]
\Pi\xrightarrow{\mathrm{check}\>\mathsf{R}\>\fatsemi\>\mathrm{observe}}_{e_{a_{1}},\ldots}\fatsemi\xrightarrow{\mathrm{check}\>\mathsf{RW}\>\fatsemi\>\mathrm{borrow}}_{p_{b_{1}},\ldots}\fatsemi\xrightarrow{\mathrm{check}\>\mathsf{W}\>\fatsemi\>\mathrm{borrow}}_{q_{c_{1}},\ldots}\Pi^{\prime\prime}\\\
\Pi\xrightarrow{\mathrm{fresh}\>\mathsf{RW}\>\fatsemi\>\mathrm{lift}}_{p_{b_{1}},\ldots,q_{c_{1}},\ldots}\Pi^{\prime}\end{array}}{\begin{array}[]{@{}c@{}}\Pi\cdot
P(e_{a_{1}},\ldots,p_{b_{1}},\ldots,q_{c_{1}},\ldots)\rightarrow\Pi^{\prime}\end{array}}$
(P-call)

Figure 3: Alias safety rules for statements.

We define the rules of alias safety for $\mu$SPARK statements in the context
of a current access policy. An _alias-safe_ statement yields an updated policy
which is used to check the subsequent statement. We write $\Pi\cdot
s\rightarrow\Pi^{\prime}$ to denote that statement $s$ is safe with respect to
policy $\Pi$ and yields the updated policy $\Pi^{\prime}$. We extend this
notation to sequences of statements $\bar{s}$ in an obvious way. The rules for
checking the alias safety of statements are given in Fig. 3. These rules use a
number of permission transformers such as ‘fresh’, ‘check’, ‘move’, ‘observe’,
and ‘borrow’, which we define and explain below.

Let us start with the (P-assign) rule. Assignments grant the full ownership
over the copied value to the left-hand side. If we copy a value of a shallow
type, we merely have to ensure that the right-hand side has the read
permission. Whenever we copy a deep-typed value, aliases may be created, and
we must check that the right-hand side is initially the sole owner of the
copied value (that is, possesses the $\mathsf{RW}$ permission) and revoke the
ownership from it.

To define the ‘${\mathrm{move}}$’ transformer that handles permissions for the
right-hand side of an assignment, we need to introduce several simpler
transformers.

###### Definition 1

Permission transformer $\mathrm{check}\>~{}\pi$ does not modify the access
policy and only verifies that a given path $p$ has permission $\pi$ or
greater. In other words,
$\Pi\xrightarrow{\mathrm{check}\>\pi}_{p}\Pi^{\prime}$ if and only if
$\Pi(p)\geqslant\pi$ and $\Pi=\Pi^{\prime}$. This transformer also applies to
expressions: $\Pi\xrightarrow{\mathrm{check}\>\pi}_{e}\Pi^{\prime}$ states
that $\Pi\xrightarrow{\mathrm{check}\>\pi}_{p}\Pi^{\prime}(=\Pi)$ for every
path $p$ occurring in $e$.

###### Definition 2

Permission transformer $\mathrm{fresh}\>\pi$ assigns permission $\pi$ to a
given path $p$ and all its extensions.

###### Definition 3

Permission transformer $\mathrm{cut}$ assigns restricted permissions to a deep
path $p$ and its extensions: the path $p$ and its near deep extensions receive
permission $\mathsf{W}$, the near shallow extensions keep their current
permissions, and the far extensions receive permission $\mathsf{NO}$.

Going back to the procedure P1 in Fig. 1, the change of permissions on the
right-hand side after the assignment A := B corresponds to the definition of
‘$\mathrm{cut}$’. In the case where the right-hand side of an assignment is
not simply a variable, but a deep path or a ’Access expression, we also need
to change permissions of the prefixes, to reflect the ownership transfer.

###### Definition 4

Permission transformer $\mathrm{block}$ propagates the loss of the read
permission from a given path to all its prefixes. Formally, it is defined by
the following rules, where $x$ stands for a variable and $f$ for a field name:

$\begin{array}[]{ccc}\dfrac{}{\Pi\xrightarrow{\mathrm{block}}_{x}\Pi}&&\dfrac{\Pi[p\mapsto\mathsf{W}]\\!\xrightarrow{\mathrm{block}}_{p}\\!\Pi^{\prime}}{\Pi\xrightarrow{\mathrm{block}}_{p.\textnormal{{all}}}\Pi^{\prime}}\\\\[17.22217pt]
\dfrac{\Pi(p)=\mathsf{NO}}{\Pi\xrightarrow{\mathrm{block}}_{p.f}\Pi}&&\dfrac{\Pi(p)\geqslant\mathsf{W}\quad\Pi[p\mapsto\mathsf{W}]\\!\xrightarrow{\mathrm{block}}_{p}\\!\Pi^{\prime}}{\Pi\xrightarrow{\mathrm{block}}_{p.f}\Pi^{\prime}}\end{array}$

###### Definition 5

Permission transformer $\mathrm{drop}$ propagates the loss of both read and
write permissions from a given path to its prefixes up to the first pointer,
and propagates the loss of the read permission afterwards:

$\begin{array}[]{c}\dfrac{}{\Pi\xrightarrow{\mathrm{drop}}_{x}\Pi}\qquad\quad\dfrac{\Pi[p\mapsto\mathsf{W}]\\!\xrightarrow{\mathrm{block}}_{p}\\!\Pi^{\prime}}{\Pi\xrightarrow{\mathrm{drop}}_{p.\textnormal{{all}}}\Pi^{\prime}}\qquad\quad\dfrac{\Pi[p\mapsto\mathsf{NO}]\\!\xrightarrow{\mathrm{drop}}_{p}\\!\Pi^{\prime}}{\Pi\xrightarrow{\mathrm{drop}}_{p.f}\Pi^{\prime}}\end{array}$

###### Definition 6

Permission transformer $\mathrm{move}$ applies to expressions:

  * •

if $e$ has a shallow type, then
$\Pi\xrightarrow{\mathrm{move}}_{e}\Pi^{\prime}\,\Leftrightarrow\,\Pi\xrightarrow{\mathrm{check}\>\mathsf{R}}_{e}\Pi^{\prime}$;

  * •

if $e$ is a deep path $p$, then
$\Pi\xrightarrow{\mathrm{move}}_{e}\Pi^{\prime}\,\Leftrightarrow\,\Pi\xrightarrow{\mathrm{check}\>\mathsf{RW}\>\fatsemi\>\mathrm{cut}\>\fatsemi\>\mathrm{block}}_{p}\Pi^{\prime}$;

  * •

if $e$ is $p\texttt{'Access}$, then
$\Pi\xrightarrow{\mathrm{move}}_{e}\Pi^{\prime}\,\Leftrightarrow\,\Pi\xrightarrow{\mathrm{check}\>\mathsf{RW}\>\fatsemi\>\mathrm{fresh}\>\mathsf{NO}\>\fatsemi\>\mathrm{drop}}_{p}\Pi^{\prime}$;

  * •

if $e$ is null, then
$\Pi\xrightarrow{\mathrm{move}}_{e}\Pi^{\prime}\,\Leftrightarrow\,\Pi^{\prime}=\Pi$.

To further illustrate the ‘$\mathrm{move}$’ transformer, let us consider two
variables P and Q of type access List and an assignment P := Q.all.Next. We
assume that Q and all its extensions have full ownership ($\mathsf{RW}$)
before the assignment. We apply the second case in the definition of
‘$\mathrm{move}$’ to the deep path Q.all.Next. The
‘$\mathrm{check}\>\mathsf{RW}$’ condition is verified, and the
‘$\mathrm{cut}$’ transformer sets the permission for Q.all.Next to
$\mathsf{W}$ and the permission for Q.all.Next.all and all its extensions to
$\mathsf{NO}$. Indeed, P.all becomes an alias of Q.all.Next.all and steals the
full ownership for this memory area. However, we still can reassign Q.all.Next
to a different address. Moreover, we still can write some new values into
Q.all or Q, without compromising safety. This is enforced by the application
of the ‘$\mathrm{block}$’ transformer at the end. We cannot keep the read
permission for Q or Q.all, since it implies the read access to the data under
Q.all.Next.all.

Now, let a variable R have type access Boolean and consider the assignment R
:= Q.all.Flag’Access. We apply the third case in the definition of
‘$\mathrm{move}$’. Assuming once again that Q has full ownership over its
value, the ‘$\mathrm{check}\>\mathsf{RW}$’ condition for Q.all.Flag is
verified. Since the ownership of this Boolean value is now transferred to
R.all, we must revoke all permissions from Q.all.Flag (and its extensions, if
it had any), which is enforced by ‘$\mathrm{fresh}\>\mathsf{NO}$’. Moreover,
since writing into the record Q.all overwrites the Flag field, we must also
revoke all permissions from Q.all. This is done by the ‘$\mathrm{drop}$’
transformer. Notice that the permissions for Q.all.Key and Q.all.Next are not
affected: we can still read and modify those fields, as they are not aliased
with other paths. Furthermore, modifying the pointer Q itself is allowed,
which is why ‘$\mathrm{drop}$’ becomes ‘$\mathrm{block}$’ after rising past
all.

Finally, we need to describe the change of permissions on the left-hand side
of an assignment, in order to reflect the gain of the full ownership. The idea
is that as soon as we have the full ownership for each field of a record, we
can assume the full ownership of the whole record, and similarly for pointers.

###### Definition 7

Permission transformer $\mathrm{lift}$ propagates the $\mathsf{RW}$ permission
from a given path to its prefixes, wherever possible:

$\begin{array}[]{ccc}\dfrac{}{\Pi\xrightarrow{\mathrm{lift}}_{x}\Pi}&&\dfrac{\Pi[p\mapsto\mathsf{RW}]\\!\xrightarrow{\mathrm{lift}}_{p}\\!\Pi^{\prime}}{\Pi\xrightarrow{\mathrm{lift}}_{p.\textnormal{{all}}}\Pi^{\prime}}\\\\[17.22217pt]
\dfrac{\forall q\sqsupset
p.\,\Pi(q)=\mathsf{RW}\quad\Pi[p\mapsto\mathsf{RW}]\\!\xrightarrow{\mathrm{lift}}_{p}\\!\Pi^{\prime}}{\Pi\xrightarrow{\mathrm{lift}}_{p.f}\Pi^{\prime}}&&\dfrac{\exists
q\sqsupset
p.\,\Pi(q)\neq\mathsf{RW}}{\Pi\xrightarrow{\mathrm{lift}}_{p.f}\Pi}\end{array}$

In the (P-assign) rule, we revoke the permissions from the right-hand side of
an assignment before granting the ownership to the left-hand side. This is
done in order to prevent creation of circular data structures. Consider an
assignment A.Next := A’Access, where A has type List. According to the
definition of ‘$\mathrm{move}$’, path A and all its extensions receive
permission $\mathsf{NO}$. This makes the left-hand side A.Next fail the write
permission check.

Allocations p := new $\tau$ are handled by the (P-alloc) rule. As long as the
memory area under the pointer p is not explicitly initialised by the program
code, no read permission is granted for p, nor its extensions and prefixes.
Moreover, since the pointer fields (if any) in the allocated memory are not
accessible yet, no permission at all can be given for the far extensions of p.
This is enforced by the ‘$\mathrm{cut}$’ transformer.

In a conditional statement, the policies at the end of the two branches are
merged selecting the most restrictive permission for each path. Loops require
that no permissions are lost at the end of a loop iteration, compared to the
entry, as explained above for procedure P2 in Fig. 1.

Procedure calls guarantee to the callee that every argument with mode in, in-
out, or out has at least permission $\mathsf{R}$, $\mathsf{RW}$ or
$\mathsf{W}$, respectively. To ensure the absence of potentially harmful
aliasing, we revoke the necessary permissions using the ‘$\mathrm{observe}$’
and ‘$\mathrm{borrow}$’ transformers.

###### Definition 8

Permission transformer $\mathrm{borrow}$ assigns permission $\mathsf{NO}$ to a
given path $p$ and all its prefixes and extensions.

###### Definition 9

Permission transformer $\mathrm{freeze}$ removes the write permission from a
given path $p$ and all its prefixes and extensions. In other words,
$\mathrm{freeze}$ assigns to each path $q$ comparable to $p$ the minimum
permission $\Pi(q)\land\mathsf{R}$.

###### Definition 10

Permission transformer $\mathrm{observe}$ applies to expressions:

  * •

if $e$ has a shallow type, then
$\Pi\xrightarrow{\mathrm{observe}}_{e}\Pi^{\prime}\,\Leftrightarrow\,\Pi^{\prime}=\Pi$;

  * •

if $e$ is a deep path $p$, then
$\Pi\xrightarrow{\mathrm{observe}}_{e}\Pi^{\prime}\,\Leftrightarrow\,\Pi\xrightarrow{\mathrm{freeze}}_{p}\Pi^{\prime}$;

  * •

if $e$ is $p\texttt{'Access}$, then
$\Pi\xrightarrow{\mathrm{observe}}_{e}\Pi^{\prime}\,\Leftrightarrow\,\Pi\xrightarrow{\mathrm{freeze}}_{p}\Pi^{\prime}$;

  * •

if $e$ is null, then
$\Pi\xrightarrow{\mathrm{observe}}_{e}\Pi^{\prime}\,\Leftrightarrow\,\Pi^{\prime}=\Pi$.

We remove the write permission from the deep-typed in parameters using the
‘$\mathrm{observe}$’ transformer, in order to allow aliasing between the read-
only paths. As for the in-out and out parameters, we transfer the full
ownership over them to the callee, which is reflected by dropping every
permission on the caller’s side using ‘$\mathrm{borrow}$’.

In the (P-call) rule, we revoke permissions right after checking them for each
parameter. In this way, we cannot pass, for example, the same path as an in
and in-out parameter in the same call. Indeed, the ‘$\mathrm{observe}$’
transformer will remove the write permission, which is required by
‘$\mathrm{check}\>\mathsf{RW}$’ later in the transformer chain. At the end of
the call, the callee transfers to the caller the full ownership over each in-
out and out parameter.

We apply our alias safety analysis to each procedure declaration. We start
with an empty access policy, denoted $\varnothing$. Then we fill the policy
with the permissions for the formal parameters and the local variables and
check the procedure body. At the end, we verify that every in-out and out
parameter has the $\mathsf{RW}$ permission. Formally, this is expressed with
the following rule:

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\varnothing\xrightarrow{\mathrm{fresh}\>\mathsf{R}}_{a_{1},\ldots}\fatsemi\xrightarrow{\mathrm{fresh}\>\mathsf{RW}}_{b_{1},\ldots}\fatsemi\xrightarrow{\mathrm{fresh}\>\mathsf{W}\>\fatsemi\>\mathrm{cut}}_{c_{1},\ldots}\fatsemi\xrightarrow{\mathrm{fresh}\>\mathsf{W}\>\fatsemi\>\mathrm{cut}}_{d_{1},\ldots}\Pi^{\prime}\\\\[3.01385pt]
\Pi^{\prime}\cdot\bar{s}\rightarrow\Pi^{\prime\prime}\quad\quad\Pi^{\prime\prime}(b_{1})=\cdots=\Pi^{\prime\prime}(c_{1})=\cdots=\mathsf{RW}\end{array}}{\begin{array}[]{@{}c@{}}\texttt{procedure}\>P\>\texttt{(}\,a_{1}\,\texttt{:}\,\texttt{in}\>\tau_{a_{1}}\texttt{;}\ldots\texttt{;}\,b_{1}\,\texttt{:}\,\texttt{in-
out}\>\tau_{b_{1}}\texttt{;}\ldots\texttt{;}\,c_{1}\,\texttt{:}\,\texttt{out}\>\tau_{c_{1}}\texttt{;}\ldots\texttt{)}\\\
\text{~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}}\texttt{is}\;d_{1}\,\texttt{:}\,\tau_{d_{1}}\texttt{;}\ldots\>\texttt{begin}\;\bar{s}\;\texttt{end}\text{~{}~{}~{}is
alias-safe}\end{array}}$

We say that a $\mu$SPARK program is _alias-safe_ if all its procedures are.

###  2.3 Soundness

As the end of the analysis, an alias-safe program has an access policy
associated to each sequence point in it. We say that an access policy $\Pi$ is
_consistent_ whenever it satisfies the following conditions for all valid
paths $\pi$, $\pi.f$, $\pi.\texttt{all}$:

$\displaystyle\Pi(\pi)=\mathsf{RW}$
$\displaystyle\Longrightarrow\Pi(\pi.f)=\mathsf{RW}$
$\displaystyle\Pi(\pi)=\mathsf{RW}$
$\displaystyle\Longrightarrow\Pi(\pi.\textnormal{{all}})=\mathsf{RW}$ (1)
$\displaystyle\Pi(\pi)=\mathsf{R}$
$\displaystyle\Longrightarrow\Pi(\pi.f)=\mathsf{R}$
$\displaystyle\Pi(\pi)=\mathsf{R}$
$\displaystyle\Longrightarrow\Pi(\pi.\textnormal{{all}})=\mathsf{R}$ (2)
$\displaystyle\Pi(\pi)=\mathsf{W}$
$\displaystyle\Longrightarrow\Pi(\pi.f)\geq\mathsf{W}$ (3)

These invariants correspond to the informal explanations given in Section 2.
Invariant (1) states that the full ownership over a value propagates to all
values reachable from it. Invariant (2) states that the read-only permission
must also propagate to all extensions. Indeed, a modification of a reachable
component can be observed from any prefix. Invariant (3) states that write
permission over a record value implies a write permission over each of its
fields. However, the write permission does not necessarily propagate across
pointer dereference.

######  Lemma 1 (Policy consistency)

The alias safety rules in Fig. 3 preserve policy consistency.

When, during an execution, we arrive at a given sequence point with the set of
variable bindings $\Upsilon$, store $\Sigma$, and statically computed and
consistent access policy $\Pi$, we say that the state of the execution
respects the Concurrent Read, Exclusive Write condition (CREW), if and only if
for any two distinct valid paths $p$ and $q$, $\langle
p\rangle^{\Upsilon}_{\Sigma}=\langle
q\rangle^{\Upsilon}_{\Sigma}\land\Pi(p)\geq\mathsf{W}\Longrightarrow\Pi(q)=\mathsf{NO}$.

The main result about the soundness of our approach is as follows:

######  Theorem 2.1 (Soundness)

A terminating evaluation of a well-typed alias-safe $\mu$SPARK program
respects the CREW condition at every sequence point.

The full proof, for a slightly different definition of $\mu$SPARK, is given in
[3]. The argument proceeds by induction on the evaluation derivation,
following the rules in Figure 2. The only difficult cases are assignment,
where the required permission withdrawal is ensured by the ‘$\mathrm{move}$’
transformer, and procedure call, where the chain of ‘$\mathrm{observe}$’ and
‘$\mathrm{borrow}$’ transformers, together with the corresponding checks, on
the caller’s side, ensures that the CREW condition is respected at the
beginning of the callee.

##  3 Implementation

We have implemented the permission rules in the GNAT compiler for Ada, which
is part of GCC. The implementation consists in 3700 lines in Ada. The analysis
is triggered by using the debug switch -gnatdF and setting the context for
formal verification of SPARK code with switch -gnatd.F and aspect SPARK_Mode.

Access policies are infinitely big in presence of recursive types, which we
took into account in our implementation with a lazy implementation of
permission trees. Permission trees start with a depth of one, and are expanded
on demand.

The permission rules presented in Section 2 only address a subset of SPARK.
Complete SPARK differs from $\mu$SPARK on several points, which have been
taken into account when designing the full set of rules. For arrays,
permission rules are adapted to apply to all elements, without taking into
account the exact index of that element, which may not be known statically in
general. Besides procedures, SPARK has functions, which return values and
cannot perform side-effects. Functions take only parameters of mode in and can
be called inside expressions. Our permission rules are augmented with an
implicit $\mathrm{move}$ of the values returned by functions, which allows us
to support constructors.

In our formalization, we considered that every shallow in parameter is passed
by-copy, which is not the case in SPARK. In our implementation, we correctly
distinguish parameters of by-copy types (typically scalars) and parameters
which may be passed by-copy or by-reference, which we treat as deep parameters
(except for function in parameters, as functions cannot have side effects, and
in particular cannot write in their parameters even under dereference).

Loops in SPARK also differ on two accounts from the loops in our
formalization: besides ‘while’ loops, SPARK also defines ‘for’ loops and plain
loops (with no exit condition), and exit statements inside a loop allow
exiting any enclosing loop. In our implementation, we take these into account
to create the correct merged context for analyzing the code after the loop.

The analysis has been tested on four test suites, including the regression
testsuite of the GNAT compiler (17041 tests [4]) and the regression testsuite
of the SPARK product (2087 tests), which detected 30 regressions, most of them
related to object oriented features that the current analysis is not able to
handle. We also wrote a dedicated testsuite [5] containing 20 tests inspired
by the examples given in the Rust borrow-checker documentation [6].

##  4 Related Works

###  4.1 Comparison with Rust

The following section compares Rust and SPARK on some features and constructs
that seem relevant to the authors. Both prevent harmful aliasing in the source
code, whereas different design choices affect their respective expressiveness.
In SPARK, an additional limitation was the choice not to add any annotation or
keyword to the language.

The main differences come from the fact that SPARK uses other compiler passes
to handle many safety features, whereas they are handled directly by Rust’s
borrow-checker and type-checker. A benefit of our work is that it
unambiguously defines the rules for SPARK while there exists no official
document specifying Rust’s borrow-checker, in all details, especially as Rust
continues to go through significant evolutions, such as non-lexical lifetimes
[7]. We must note, however, a significant recent effort to provide a rigorous
formal description of the foundations of Rust [8].

In SPARK, the duration of borrows is limited to the duration of procedure
calls. The mechanism of _renaming_ in SPARK can be used to shorten long paths,
and thus it is less important to be able to create several local copies of the
same deep variable. It turns out, however, that this restriction forbids
traversing a linked data structure with only $\mathsf{R}$ permission, and that
even with $\mathsf{RW}$ permission the structure needs to be reconstructed
after traversal. We are working on the rules for local application of borrow
and observe inside a block to allow these.

Rust has sophisticated lifetime checks, allowing to precisely control the
duration of a borrowed pointer. In SPARK, similar checks are implemented as a
separate analysis pass of GNAT compiler, with their own set of rules that are
less expressive: the lifetime of a pointer is limited to the block in which
its type has been declared.

There are no null pointers in Rust, whereas they are allowed in SPARK.
Dereferencing a null pointer is a runtime error, and the null-pointer safety
must be proved by a separate analysis by the SPARK verification tools [9].

Another difference is that mutable borrows in Rust guarantee the ownership of
the underlying memory at any time, whereas in SPARK borrow guarantees
ownership only at the entry and exit of the procedure. In particular, it is
not possible in Rust to move out a borrowed variable without assigning it in
the same statement. In SPARK, any borrowed variable can be moved as long as it
is assigned before the end of the procedure, which grants it the $\mathsf{RW}$
permission. This allows us to directly implement the swap procedure in SPARK,
whereas the Rust implementation relies on unsafe operations:

⬇

procedure Swap (X, Y : in out T) is

Temp : T := Y; \-- Move Y. X:RW, Y:W, Temp:RW

begin

Y := X; \-- Move X. X:W, Y:RW, Temp:RW

X := Temp; \-- Move Temp. X:RW, Y:RW, Temp:W

end Swap; \-- Both arguments X and Y are RW.

Finally, it is impossible to implement cycling constructs in SPARK (the right-
hand side of an assignment cannot be an ancestor of the left-hand side). Rust
has a similar limitation and requires some workarounds like reference counting
to implement structures like graphs [10]. Nevertheless, both Rust and SPARK
allow compiling with parts of code written in an unsafe superset of the
language. This is the case for some standard library containers (hash tables,
iterators, smart pointers, etc.) that have an interface specified in SPARK and
Rust, and can be called safely from safe Rust/SPARK.

###  4.2 Other Related Works

Permission-based programming languages generalize the issue of avoiding
harmful aliasing to the more general problem of preventing harmful sharing of
resources (memory, but also network connections, files, etc.). Cyclone and
Rust achieve absence of harmful aliasing by enforcing an ownership type system
on the memory pointed to by objects [11, 12].

Dafny associates each object with its _dynamic frame_ , the set of pointers
that it owns [13]. This dynamic version of ownership is enforced by modeling
the ownership of pointers in logic, generating verification conditions to
detect violations of the single-owner model, and proving them using SMT
provers. In Spec#, ownership is similarly enforced by proof, to detect
violations of the so-called Boogie methodology [14].

Separation logic [15] is an extension of Hoare-Floyd logic that allows
reasoning about pointers. In general, it is difficult to integrate into
automated deductive verification: in particular, it is not directly supported
by SMT provers.

In our work, we use a permission-based mechanism for detecting potentially
harmful aliasing, in order to make the presence of pointers transparent for
automated provers. In addition, our approach does not require additional user
annotations, that are required in some of the previously mentioned techniques.
We thus expect to achieve high automation and usability, which was our goal
for supporting pointers in SPARK.

##  5 Conclusion

In this paper, we have presented anti-aliasing rules that allow supporting
pointers in SPARK. We showed a systematic analysis that allows a wide range of
use cases with pointers and dynamic allocation. To the best of our knowledge,
this is a novel approach for controlling aliasing introduced by arbitrary
pointers in a programming language supported by proof. Our approach does not
require user annotations or proof of verification conditions, which makes it
much simpler to adopt. Moreover, we provided a formalization of our rules on a
subset of SPARK in order to mathematically prove the safety of our analysis.
Finally, we compared our method to the Rust language which provides a similar
analysis.

More work needs to be done to fully support pointers in SPARK. Both flow
analysis and proof need to be adapted to account for the presence of pointers.
This work has started and is expected to be completed by the end of 2018. This
will make it possible to use formal verification with SPARK on industrial
programs with pointers, something that was long believed to be impossible.

We also need to extend our formalism and proof to non-terminating executions.
For that purpose, we can provide a co-inductive definition of the big-step
semantics and perform a similar co-inductive soundness proof, as described by
Leroy and Grall [16].

The formal study of the constructs that can be implemented using this borrow-
checker has not been discussed in this paper. Such a study could allow a
formalization of anti-aliasing analyses through classes of expressiveness.
Another long-term goal would be extending our analysis so that it could handle
automatic reclamation, parallelism, initialization and lifetime checks,
instead of relying on external checks.

The proposed anti-aliasing rules are being discussed by the Ada Rapporteur
Group for inclusion in the next version of Ada [17].

## References

  * [1] McCormick, J.W., Chapin, P.C.:  Building High-Integrity Applications with SPARK.  Cambridge University Press (2015)
  * [2] Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.:  Frama-C: A software analysis perspective.  Formal Aspects of Computing 27(3) (May 2015) 573–609
  * [3] Jaloyan, G.A.:  Safe pointers in SPARK 2014 (2017) https://arxiv.org/abs/1710.07047.
  * [4] ACATS:  Test suite.  http://www.ada-auth.org/acats-files/4.1/ACATS41.ZIP
  * [5] Georges-Axel Jaloyan:  SPARK aliasing test suite.  https://github.com/GAJaloyan/SPARKtestsuite
  * [6] Rust community:  Documentation for Rust’s borrow-checker.  https://github.com/rust-lang/rust/blob/master/src/librustc_borrowck/borrowck/README.md
  * [7] Rust community:  Non-lexical lifetimes.  https://github.com/rust-lang/rfcs/pull/2094
  * [8] Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, Derek Dreyer:  RustBelt: Securing the foundations of the Rust programming language.  2(Issue POPL, 66) (2018)
  * [9] AdaCore, Thales:  Implementation Guidance for the Adoption of SPARK, http://www.adacore.com/uploads/technical-papers/ePDF-ImplementationGuidanceSPARK.pdf
  * [10] Rust:  Graphs and arena allocation.  https://github.com/nrc/r4cppp/blob/master/graphs/README.md
  * [11] Grossman, D., Morrisett, G., Jim, T., Hicks, M., Wang, Y., Cheney, J.:  Region-based memory management in Cyclone.  SIGPLAN Not. 37(5) (May 2002) 282–293
  * [12] Balasubramanian, A., Baranowski, M.S., Burtsev, A., Panda, A., Rakamarić, Z., Ryzhyk, L.:  System programming in Rust: Beyond safety.  SIGOPS Oper. Syst. Rev. 51(1) (September 2017) 94–99
  * [13] Leino, K.R.M.  In: Dafny: An Automatic Program Verifier for Functional Correctness. Springer Berlin Heidelberg, Berlin, Heidelberg (2010) 348–370
  * [14] Barnett, M., Chang, B.Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.  In: Boogie: A Modular Reusable Verifier for Object-Oriented Programs. Springer Berlin Heidelberg, Berlin, Heidelberg (2006) 364–387
  * [15] Reynolds, J.C.:  Separation logic: A logic for shared mutable data structures.  In: Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science. LICS ’02, Washington, DC, USA, IEEE Computer Society (2002) 55–74
  * [16] Leroy, X., Grall, H.:  Coinductive big-step operational semantics.  Information and Computation 207(2) (Feb 2009) 284–304
  * [17] AdaCore:  Access value ownership and parameter aliasing (2018) http://www.ada-auth.org/cgi-bin/cvsweb.cgi/ai12s/ai12-0240-1.txt.


# FinRED: A Dataset for Relation Extraction in Financial Domain

Soumya Sharma<EMAIL_ADDRESS>IIT KharagpurIndia ,  Tapas Nayak
<EMAIL_ADDRESS>IIT KharagpurIndia ,  Arusarka Bose<EMAIL_ADDRESS>IIT KharagpurIndia ,  Ajay Kumar Meena<EMAIL_ADDRESS>IIT
KharagpurIndia ,  Koustuv Dasgupta<EMAIL_ADDRESS>Goldman
SachsIndia ,  Niloy Ganguly<EMAIL_ADDRESS>IIT Kharagpur, IndiaLU,
Hannover and  Pawan Goyal<EMAIL_ADDRESS>IIT KharagpurIndia

(2022)

###### Abstract.

Relation extraction models trained on a source domain cannot be applied on a
different target domain due to the mismatch between relation sets. In the
current literature, there is no extensive open-source relation extraction
dataset specific to the finance domain. In this paper, we release FinRED, a
relation extraction dataset curated from financial news and earning call
transcripts containing relations from the finance domain. FinRED has been
created by mapping Wikidata triplets using distance supervision method. We
manually annotate the test data to ensure proper evaluation. We also
experiment with various state-of-the-art relation extraction models on this
dataset to create the benchmark. We see a significant drop in their
performance on FinRED compared to the general relation extraction datasets
which tells that we need better models for financial relation extraction.

financial information extraction, financial relation extraction, financial
dataset

* Equal contribution

††journalyear: 2022††copyright: acmcopyright††conference: Companion
Proceedings of the Web Conference 2022; April 25–29, 2022; Virtual Event,
Lyon, France.††booktitle: Companion Proceedings of the Web Conference 2022
(WWW ’22 Companion), April 25–29, 2022, Virtual Event, Lyon, France††price:
15.00††doi: 10.1145/3487553.3524637††isbn: 978-1-4503-9130-6/22/04††ccs: Deep
learning Span extraction††ccs: Natural language processing Information
extraction, Relation Extraction††ccs: Domain Financial

##  1\. Introduction

The task of relation extraction (RE) is defined as identifying triplets from
text. Recently joint entity and relation extraction models (Nayak and Ng,
2020; Sui et al., 2020; Wang et al., 2020) have been proposed to eliminate the
dependency on an external NER module. These models have achieved remarkable
performance in this task. Freebase-New York Times dataset (FB-NYT) (Hoffmann
et al., 2011) is obtained by mapping relational triplets from Freebase
(Bollacker et al., 2008), WebNLG (Gardent et al., 2017) is a natural language
generation dataset created semi-automatically from DBPedia (Bizer et al.,
2009) triplets. Although KBs such as Freebase, Wikidata, DBpedia contain a lot
of relational triplets from different domains such as finance, material
science, legal, but that is not reflected in the existing RE datasets as they
very generic sources of text corpus. There have been some efforts to create
datasets for particular domain-specific relation extraction such as legal
(Andrew, 2018), biomedical (Gu et al., 2016; Li et al., 2017; Choi, 2018;
Thillaisundaram and Togia, 2019), scientific articles (Luan et al., 2017; Jain
et al., 2020). There have been some efforts to create datasets in the
financial domain (Vela and Declerck, 2009; Wu et al., 2020; Jabbari et al.,
2020), however to the best of our knowledge, there is currently no standard
dataset in English to understand financial relations. There has been some work
on financial numeral understanding (Chen and Huang, 2019; Chen et al., 2019),
however, our paper focuses on textual relations and not numerical. To bridge
this gap, we create a finance domain-specific distance supervised relation
extraction dataset. We obtain the finance relations from Wikidata KB and use
text from the finance domain to create the FinRED dataset.

##  2\. Dataset Sources and Creation

The FinRED dataset 111Repository https://github.com/soummyaah/FinRED/ has been
created using two sets of documents: 1) Webhose Financial News, and 2) Earning
Call Transcript (ECT).

Webhose Financial News:  For the financial news articles, we use the freely
available dataset curated by Webhose. It contains 47,851 English financial
news articles crawled from July 2015 - October 2015.

Earning Call Transcripts (ECT):  We collect 4,713 ECTs dated from June 2019 to
September 2019 from seekingalpha.com. A typical ECT contains a presentation
from the company participants followed by a questionnaire section containing
questions asked by audience answered by company participants. We term the
presentation portion and the answers as monologues. We use the presentation as
well as the questionnaire portion of the transcript and remove monologues with
less than 200 characters. In the ECT corpus, we have about 200K monologues,
1.8M sentences with an average of 7.19 sentences per monologue. In total, we
have 152K tokens in the corpus.

Table 1. Comparison between different RE datasets. Dataset Name | Train | Test | #Relations | #Financial Relations
---|---|---|---|---
FB-NYT | 56,196 | 5,000 | 24 | 4
WebNLG | 5,519 | 703 | 216 | 12
FinRED (Ours) | 5,699 | 1,068 | 29 | 29
Table 2. Examples in the dataset Sentence | Head | Relation | Tail
---|---|---|---
Antony Jenkins has been |  | chief |
sacked as chief executive | Anthony | executive |
officer of Barclays Plc. | Jenkins | officer | Barclays
MEXICO CITY — State-owned |  | product or |
Mexican oil company Pemex |  | material |
is reporting second quarter | Pemex | produced | petroleum
losses of $\$$US5.2 billion |  |  |
($\$$A7.16 billion) due mainly |  | headquarters | Mexico
to lower petroleum prices | Pemex | location | City

Knowledge Base (KB):  We use a subset of the Wikidata KB as a source of
relational triplets for financial domain containing manually filtered 29
financial relations. Using the idea of distance supervision (Mintz et al.,
2009), we align the relational triplets to the text corpus.

Dataset:  In total we obtain about 21,000 sentences using the distance
supervision method, however a lot of these sentences are noisy. Eg: “Delhi-
based National Housing Bank (NHB) is working to set up more than 80 new
housing finance companies (HFCs), with a special emphasis on those that will
focus on financing affordable houses.” where the tuple is (More Than,
industry, finance) since in Wikidata, “More Than“ is listed as an insurance
company of the financial industry. We study a small representation of the data
in detail and remove datapoints with incorrect entities such as “More Than“
and “industry“. After reduction, we get 7,775 sentences which we divide into
the train, dev, and test dataset. We observe that this dataset only contains
920 sentences from the earnings call transcript and we attribute this to the
earning call transcripts containing primarily conversational data which often
does not contain a triplet in a sentence. A comparison of FinRED with FB-NYT
(Hoffmann et al., 2011) and WebNLG (Gardent et al., 2017) along with a few
examples from the dataset has been showcased in Table 1.

Annotation of test data:  We annotate the dataset with the help of 2 non-
native fluent English speakers annotators, who go through the dataset twice,
and all incorrect triplets are removed. All triplets marked as incorrect by
both the annotators are removed from the dataset. The Cohen $\kappa$ between
the annotators is 82.1%.

##  3\. Experiments

To avoid the use of external NER module, we choose 3 joint entity and relation
extraction models, namely, SPN (Sui et al., 2020), TPLinker (Wang et al.,
2020), and CasRel (Wei et al., 2020) for our experiments. These models
achieved state-of-the-art performance on standard relation extraction datasets
Freebase-New York Times (Hoffmann et al., 2011) and WebNLG (Gardent et al.,
2017). We report precision, recall and F1 score for triplet extraction based
on exact entity matching criterion and report the results in Table 3.

From Table 3, we can observe a drop of $\sim$4% for SPN and $\sim$25-30% for
TPLinker and Casrel models in F1 as compared to FB-NYT and WebNLG datasets.
Drop in the performance showcases that more research is required to better
capture performance. For the SPN model, we observe that the relation F1 value
is 88.37% and the entity F1 value is 96.36% showcasing that while the model
can predict the entity properly, the lower model performance can be attributed
to incorrect relation classification. We see similar trends in the performance
of TPLinker and CasRel.

Table 3. Performance of the three baseline models on FinRED. | FinRED (Ours) | FB-NYT | WebNLG
---|---|---|---
Model | Prec. | Rec. | F1 | F1 | F1
SPN |  89.22% |  86.42% |  87.80% | 92.30% | 91.80%
TPLinker | 76.59% | 63.45% | 69.40% | 92.00% | 86.70%
CasRel | 69.71% | 55.84% | 62.01% | 89.60% | 93.40%
Table 4. Performance of SPN model on the sentence classes with different number triplets and with type of overlapping triplets in them. Metric | Precision | Recall | F1
---|---|---|---
1 triplet | 76.15% | 86.46% | 80.98%
2 triplets | 86.36% | 88.88% | 87.60%
3 triplets | 93.31% | 85.24% | 89.09%
4+ triplets | 95.79% | 88.61% | 92.06%
NEO | 78.40% | 89.61% | 83.36%
EPO | 93.07% | 85.50% | 89.16%
SEO | 89.86% | 86.18% | 87.98%

Performance of SPN model on the sentence classes with different number of
triplets is reported in Table 4. The performance improves as the number of
triplets increases which showcases that the more the number of triplets(
typically EPO and SEO) , the better assistance the machine has to make better
predictions.

In Table 4 we also report the performance of SPN model on the sentence classes
with the type of overlapping triplets in them. Based on the overlap of
entities, the sentence can be divided into three types: 1) NEO (No entity
overlap) 2) EPO (Entity Pair Overlap) and 3) SEO (Single Entity Overlap).
Here, we can observe that the model shows a slightly higher performance for
SEO (F1: 87.98%) and EPO (F1: 89.16%) as compared to NEO (F1: 83.36%). We
surmise that this is because the entity prediction part of the model performs
well so for multi-label and overlapping triplets, the performance is higher
since it needs to identify less number of entities.

##  4\. Conclusion

In this paper, we propose FinRED, a relation extraction dataset for the
finance domain curated from earning call transcript corpus and financial news
articles. It contains more finance domain-specific relations than the existing
RE datasets. We experimented with three state-of-the-art joint entity and
relation extraction models on this dataset and saw a significant drop in F1
score compare to general domain RE datasets showcasing that more research is
required on the models for FinRED.

###### Acknowledgements.

This research was partially supported by Goldman Sachs sponsored research
grant FTHS. (FinTalk: Research towards creating a platform for highlight
generation and summarization of financial documents while taking into account
user feedback).

## References

  * (1)
  * Andrew (2018) Judith Jeyafreeda Andrew. 2018\.  Automatic Extraction of Entities and Relation from Legal Documents. In _Proceedings of the Seventh Named Entities Workshop_. Association for Computational Linguistics, Melbourne, Australia, 1–8.  https://doi.org/10.18653/v1/W18-2401
  * Bizer et al. (2009) Christian Bizer, Jens Lehmann, Georgi Kobilarov, S. Auer, Christian Becker, Richard Cyganiak, and Sebastian Hellmann. 2009.  DBpedia - A crystallization point for the Web of Data.  _J. Web Semant._ 7 (2009), 154–165.
  * Bollacker et al. (2008) Kurt Bollacker, Colin Evans, Praveen Paritosh, Tim Sturge, and Jamie Taylor. 2008.  Freebase: A collaboratively created graph database for structuring human knowledge.  _Proc. Sigmod_ , 1247–1250.  https://doi.org/10.1145/1376616.1376746
  * Chen and Huang (2019) Chung-Chi Chen and Hen-Hsen Huang. 2019.  Overview of the ntcir-14 finnum task: Fine-grained numeral understanding in financial social media data. In _Proceedings of the 14th NTCIR Conference on Evaluation of Information Access Technologies_.
  * Chen et al. (2019) Chung-Chi Chen, Hen-Hsen Huang, Hiroya Takamura, and Hsin-Hsi Chen. 2019.  Numeracy-600K: Learning Numeracy for Detecting Exaggerated Information in Market Comments. In _Proceedings of the 57th Annual Meeting of the Association for Computational Linguistics_. Association for Computational Linguistics, Florence, Italy, 6307–6313.  https://doi.org/10.18653/v1/P19-1635
  * Choi (2018) Sung-Pil Choi. 2018\.  Extraction of protein–protein interactions (PPIs) from the literature by deep convolutional neural networks with various feature embeddings.  _Journal of Information Science_ 44 (2018), 60 – 73.
  * Gardent et al. (2017) Claire Gardent, Anastasia Shimorina, Shashi Narayan, and Laura Perez-Beltrachini. 2017.  Creating Training Corpora for NLG Micro-Planners. In _Proceedings of the 55th Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers)_. Association for Computational Linguistics, Vancouver, Canada, 179–188.  https://doi.org/10.18653/v1/P17-1017
  * Gu et al. (2016) Jinghang Gu, Longhua Qian, and Guodong Zhou. 2016\.  Chemical-induced disease relation extraction with various linguistic features.  _Database: The Journal of Biological Databases and Curation_ 2016 (2016).
  * Hoffmann et al. (2011) Raphael Hoffmann, Congle Zhang, Xiao Ling, Luke Zettlemoyer, and Daniel S. Weld. 2011.  Knowledge-Based Weak Supervision for Information Extraction of Overlapping Relations. In _Proceedings of the 49th Annual Meeting of the Association for Computational Linguistics: Human Language Technologies_. Association for Computational Linguistics, Portland, Oregon, USA, 541–550.  https://aclanthology.org/P11-1055
  * Jabbari et al. (2020) Ali Jabbari, Olivier Sauvage, Hamada Zeine, and Hamza Chergui. 2020.  A French Corpus and Annotation Schema for Named Entity Recognition and Relation Extraction of Financial News. In _Proceedings of the 12th Language Resources and Evaluation Conference_. European Language Resources Association, Marseille, France, 2293–2299.  https://aclanthology.org/2020.lrec-1.279
  * Jain et al. (2020) Sarthak Jain, Madeleine van Zuylen, Hannaneh Hajishirzi, and Iz Beltagy. 2020.  SciREX: A Challenge Dataset for Document-Level Information Extraction. In _Proceedings of the 58th Annual Meeting of the Association for Computational Linguistics_. Association for Computational Linguistics, Online, 7506–7516.  https://doi.org/10.18653/v1/2020.acl-main.670
  * Li et al. (2017) Fei Li, Meishan Zhang, Guohong Fu, and Dong-Hong Ji. 2017\.  A neural joint model for entity and relation extraction from biomedical text.  _BMC Bioinformatics_ 18 (2017).
  * Luan et al. (2017) Yi Luan, Mari Ostendorf, and Hannaneh Hajishirzi. 2017\.  Scientific Information Extraction with Semi-supervised Neural Tagging. In _Proceedings of the 2017 Conference on Empirical Methods in Natural Language Processing_. Association for Computational Linguistics, Copenhagen, Denmark, 2641–2651.  https://doi.org/10.18653/v1/D17-1279
  * Mintz et al. (2009) Mike Mintz, Steven Bills, Rion Snow, and Daniel Jurafsky. 2009\.  Distant supervision for relation extraction without labeled data. In _Proceedings of the Joint Conference of the 47th Annual Meeting of the ACL and the 4th International Joint Conference on Natural Language Processing of the AFNLP_. Association for Computational Linguistics, Suntec, Singapore, 1003–1011.  https://aclanthology.org/P09-1113
  * Nayak and Ng (2020) Tapas Nayak and Hwee Tou Ng. 2020.  Effective modeling of encoder-decoder architecture for joint entity and relation extraction. In _Proceedings of the AAAI conference on artificial intelligence_ , Vol. 34. 8528–8535.
  * Sui et al. (2020) Dianbo Sui, Yubo Chen, Kang Liu, Jun Zhao, Xiangrong Zeng, and Shengping Liu. 2020\.  Joint entity and relation extraction with set prediction networks.  _arXiv preprint arXiv:2011.01675_ (2020).
  * Thillaisundaram and Togia (2019) Ashok Thillaisundaram and Theodosia Togia. 2019.  Biomedical relation extraction with pre-trained language representations and minimal task-specific architecture. In _Proceedings of The 5th Workshop on BioNLP Open Shared Tasks_. Association for Computational Linguistics, Hong Kong, China, 84–89.  https://doi.org/10.18653/v1/D19-5713
  * Vela and Declerck (2009) Mihaela Vela and Thierry Declerck. 2009.  Concept and Relation Extraction in the Finance Domain. In _Proceedings of the Eight International Conference on Computational Semantics_. Association for Computational Linguistics, Tilburg, The Netherlands, 346–350.  https://aclanthology.org/W09-3741
  * Wang et al. (2020) Yucheng Wang, Bowen Yu, Yueyang Zhang, Tingwen Liu, Hongsong Zhu, and Limin Sun. 2020\.  TPLinker: Single-stage Joint Extraction of Entities and Relations Through Token Pair Linking. In _Proceedings of the 28th International Conference on Computational Linguistics_. International Committee on Computational Linguistics, Barcelona, Spain (Online), 1572–1582.  https://doi.org/10.18653/v1/2020.coling-main.138
  * Wei et al. (2020) Zhepei Wei, Jianlin Su, Yue Wang, Yuan Tian, and Yi Chang. 2020.  A Novel Cascade Binary Tagging Framework for Relational Triple Extraction. In _Proceedings of the 58th Annual Meeting of the Association for Computational Linguistics_. 1476–1488.
  * Wu et al. (2020) Haoyu Wu, Qing Lei, Xinyue Zhang, and Zhengqian Luo. 2020\.  Creating A Large-Scale Financial News Corpus for Relation Extraction.  _2020 3rd International Conference on Artificial Intelligence and Big Data (ICAIBD)_ (2020), 259–263.