sl_prove
sl_prove
is an automatic entailment prover for separation logic with inductive definitions.
The theory/design behind sl_prove
appears in [APLAS12].
Compiling
If you are simply looking for the latest version of sl_prove
, have a look at Installation.
The original version of sl_prove
in [APLAS12] is not stored on GitHub. To try the closest possible,
you can checkout a very early commit.
git clone https://github.com/ngorogiannis/cyclist.git cyclist
cd cyclist
git checkout b289f39a6a46b4f57da3585aa7fd71f3ca8601fc
Then consult the README included, which contains building instructions relevant to that version.
Example
Here is an example. A linked-list segment from address x
to address y
can be defined as follows:
ls {
x=y => ls(x,y) |
x!=y * x->x' * ls(x',y) => ls(x,y)
}
This means that either the list segment is empty (hence x=y
) or it is not
empty (x!=y
) and there is a cell allocated at x
containing some value x'
(x->x'
) from which there is a list segment up to y
(ls(x',y)
).
Now we can ask whether, for instance, a chain of two segments from x
through y
to nil
(nil
is a special, always non-allocatable address, much like C’s’ NULL
)
forms a proper list segment from x
to nil
. This is how we pose the query
and the output we obtain:
$ ./sl_prove.native -S "ls(x,y) * ls(y,nil) |- ls(x,nil)"
Proved: ls^1(x, y) * ls^2(y, nil) |- ls^3(x, nil)
This means sl_prove
found a proof for the above sequent. Let’s inspect this proof.
$ ./sl_prove.native -S "ls(x,y)*ls(y,nil) |- ls(x,nil)" -p
0: ls^1(x, y) * ls^2(y, nil) |- ls^3(x, nil) (ls L.Unf./Simplify) [1, 2]
1: ls^2(x, nil) |- ls^3(x, nil) (Pred Intro) [3]
3: emp |- emp (Id)
2: nil!=x * y!=x * x->z * ls^2(y, nil) * ls^3(z, y) |- ls^3(x, nil) (ls R.Unf./Simplify) [4]
4: nil!=x * y!=x * x->z * ls^2(y, nil) * ls^3(z, y) |- x->y' * ls^1(y', nil) (Pto Intro/Simplify) [5]
5: nil!=x * y!=x * ls^2(y, nil) * ls^3(z, y) |- ls^1(z, nil) (Weaken) [6]
6: ls^2(y, nil) * ls^3(z, y) |- ls^3(z, nil) (Subst) [7]
7: ls^2(y, nil) * ls^3(x, y) |- ls^3(x, nil) (Backl) [0] <pre={(2, 2), (3, 1)}>
The -p
argument lets us see the proof found. This proof is cyclic (node 7 is a back-link to node 0).
There are several other options, which are listed when sl_prove
is run without arguments.
Benchmarks in [APLAS12]
To run a fixed set of entailment queries (including the sequents appearing in [APLAS12]), run
$ make sl-tests
SL grammar
The grammar for SL sequents is roughly as follows.
sequent ::= form "|-" form
form ::= heap | heap "\/" form
heap ::= atomic | atomic "*" heap
atomic ::= "emp" | eq | deq | pointsto | pred
eq ::= term "=" term
deq ::= term "!=" term
pointsto ::= var "->" termlist
termlist ::= term | term "," termlist
term ::= var | "nil"
pred ::= identifier "(" termlist ")"
where var matches any word over letters and numbers possibly postfixed by a quote ‘, and identifier matches any word over letters and numbers. Variables ending in a quote are implicitly existentially quantified.