covered and the number of programmers served. Static analysis with SL has
matured to the point where it has been
applied industrially in the Facebook
Infer program analyzer, an open source
tool used at Facebook, Mozilla, Spotify,
Amazon Web Services, and other companies ( www.fbinfer.com).
The purpose of this article is to describe the basic ideas of SL as well as
these and other developments.
Mathematical semantics has been
critical to the discovery and further SL
development, but many of the main
points can be gleaned from “picture
semantics.” Consider the first picture
in Figure 1. We read the formula at
the top of this figure as “x points to
y and separately y points to x.” Going down the middle of the diagram
is a line that represents a heap partitioning: a separating conjunction
asks for a partitioning that divides
the heap into parts, heaplets, satisfying its two conjuncts. At the bottom
of the first picture is an example of
a concrete memory description that
corresponds to the diagram. There,
x and y have values 10 and 42 (in the
“environment,” or “register bank”),
and 10 and 42 are themselves locations with the indicated contents (in
the “heaplet,” or even “RAM”).
The indicated separating conjunction here is true of the pictured
memory because the parts satisfy the
conjuncts, as indicated in the second
picture. The meaning of “x points to
y and yet to nothing” is precisely disambiguated in the RAM description
below the diagram: x and y denote values ( 10 and 42), x’s value is an allocated memory address which contains
y’s value, but y’s value is not allocated.
The separating conjunction splits the
heap/RAM, but it does not split the association of variables to values.
Generally speaking, the separating
conjunction P Q is true of a heap if it
can be split into two heaplets, one of
which makes P true and the other of
which makes Q true. A distinction between and Boolean conjunction ∧ is
that P P ≠ P where P ∧ P = P. In particular, x v x v is always false: there is
no way to divide any heap in such a way
that a cell x goes to both partitions.
is often used with linked structures. If list (x, y) describes an acyclic
linked list running from x to y, then we
can describes a structure with a list segment, followed by a single pointer, followed by a further list running up to 0
(null), as follows:
This is the kind of structure you
might need to consider when deleting
an element from a list, or inserting one
There is a further connective, the separating implication or “magic wand.”
P –* Q says that whenever the current
heaplet is extended with a separate
heaplet satisfying P, the resulting combined heaplet will satisfy Q. For example, (x –) ((x 3) –*Q) says that x is
allocated in the current heap, and that if
you mutate its contents to 3 then Q will
hold. This describes the “weakest precondition” for the mutation [x] = 3 with
postcondition Q. 26
Finally, there is an assertion emp
which says “the heaplet is empty,” emp
is the unit of *, so that P = emp P = P *
emp. Also, –* and fit together is a way
similarly to how implication ⇒ and conjunction ∧ do in standard logic. For example, the entailment
(where reads “entails”) is a SL relative
of “modus ponens.”
Although we will concentrate on the
informal picture semantics in this ar-
ticle, for the theoretically inclined we
have included a glimpse of the formal
semantics in Figure 2.
Rules for Program Proof
Figure 3 contains a selection of proof
rules of SL. The rules are divided into
axioms for basic mutation commands
(the “small axioms”) and inference
rules for modular reasoning. An inference rule says “if you can derive what
is above the line, then so can you what
is below,” and the axioms are derivable true statements that are given.
The small axioms are for a programming language with load and store
instructions similar to an assembly
language. If we vary the programming
language the small axioms change.
The concurrency rule uses a composition operator || for running two processes in parallel, derived from Dijkstra’s parbegin/parend. 16
The first small axiom just says that if
x points to something beforehand, then
it points to v afterward, and it says this
for a small portion of the state in which x
is the only active cell.
Figure 3. Separation logic proof system (a selection).