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.