APE is a tool for automatically proving the equivalence of programs using modular program verification technology. It show cases an approach to proving the equivalence of programs that differ in the order and amount of dynamic memory allocation. It supports a simple recursive language called L. Underlying APE are the tools Boogie and Z3.
Details of the tool can be found in Tim Wood's Phd Thesis, including a formal proof of the soundness of the methodology. The rest of this document illustrates the capabilities of APE by giving examples, that APE can verify, and commentary on the examples.
- Automatic Procedure Equivalence Tool
The tool was evaluated against a number of micro-test cases and also against several larger examples. In order to illuminate the tool's capabilities we describe here the most important test cases and explain why they are interesting. The code for all 30+ tests cases and the associated generated boogie code is also available. The test cases are tabulated at the end of this document.
In the following test case two objects are allocated and assigned to fields of the procedure parameter. APE ignores garbage so assigning the new objects into fields prevents them from being ignored. In version 0 (v0) the object allocated first is assigned into the field f and the second is assigned into the field g. In version 1 (v1) the first object allocate is assigned into the field g and the second into the field f. Despite this change in allocation order, APE proves the procedure are equivalent by proving that the final stores of the procedures are isomorphic modulo garbage for all initial stores.
VERSION 0
procedure DoubleAllocation(x) {
t := new();
u := new();
x.f := t;
x.g := u;
}
VERSION 1
procedure DoubleAllocation(x) {
t := new();
u := new();
x.g := t;
x.f := u;
}
In the following test case v1 allocates a single object, whereas v2 allocates no objects. APE uses a definition of equivalence that is insensitive to the amount of garbage. APE proves that these procedures always result in isomorphic final stores despite the different numbers of allocations.
VERSION 0
procedure SingleGarbageAllocation(x) {
t := new();
}
VERSION 1
procedure SingleGarbageAllocation(x) {
}
In the following test case v0 allocates more memory that v1. APE proves that the procedures are equivalent because the extra memory that v0 allocates is garbage by the end of the procedure. It is interesting to note that:
- some of the memory that is garbage at the end of the procedure is made reachable during execution of v0
- the garbage from v0 has different shape than the garbage from v1
- the procedure parameter is reachable from the garbage at the end of v0
VERSION 0
procedure DifferentShapedGarbage(x) {
t := new();
u := new();
t.f := x;
x.f := x;
x.g := t;
x.g := new();
}
VERSION 1
procedure DifferentShapedGarbage(x) {
t := new();
x.f := x;
x.g := new();
}
APE is a modular verification tool. It proves the equivalence of pairs of similarly named procedures by assuming that calls to similarly named procedures behave equivalently. If it can verify the equivalence of all such pairs of procedures then the assumptions are justified and the equivalence proof is sound.
The following example shows a pair of procedures that make a single call to another procedure. APE proves that they are equivalent by proving that the versions of Caller are equivalent (under the assumption that the versions of Callee are equivalent) and then proving that the versions of Callee are equivalent.
VERSION 0
procedure Caller(x) {
call Callee(x);
}
procedure Callee(x) {
...
}
VERSION 1
procedure Caller(x) {
call Callee(x);
}
procedure Callee(x) {
...
}
Allocations may occur before a procedure call. In the following example the order of the allocations differ between v0 and v1.
VERSION 0
procedure Caller(x)
{
t := new();
u := new();
call Callee(x);
x.f := t;
x.g := u;
}
procedure Callee(x)
{
...
}
VERSION 1
procedure Caller(x)
{
u := new();
t := new();
call Callee(x);
x.f := t;
x.g := u;
}
procedure Callee(x)
{
...
}
In order to establish the equivalence of a pair of procedure calls APE attempts to find an isomorphism between the part of the heap reachable from their procedure parameters. In the following example the order of the allocations is reversed between v0 and v1. Note that the result of calling Callee is made reachable from the parameter of Caller.
VERSION 0
procedure Caller(x)
{
t := new();
u := new();
call Callee(x,t);
x.f := t.v;
x.g := u;
}
procedure Callee(x,y)
{
}
VERSION 1
procedure Caller(x)
{
t := new();
u := new();
call Callee(x, u);
x.f := u.v;
x.g := t;
}
procedure Callee(x,y)
{
}
APE can deduce that procedures have equivalent effects even when the pre-stores of the calls are not isomorphic. Instead of checking for isomorphism of the whole store it only checks that the parts of the stores reachable from the call parameters are isomorphic. The following test cases illustrate this.
Allocations may be moved past calls, provided they are not reachable from the call parameters. In the following example an object is allocated before the call in v0 but after it in v1. Since the allocate memory is not reachable from the call parameter x in v0, APE is still able to prove equivalence.
Note that knowledge that the shape of the memory pointed to by t in v0 is the same as the shape of the memory pointed to by t in v1 persists over the v0 call to Callee. This is possible due to the frame axioms automatically used by APE and described in Tim's thesis.
VERSION 0
procedure Caller(x) {
t := new();
call Callee(x);
x.f := t;
}
procedure Callee(x) {
...
}
VERSION 1
procedure Caller(x) {
call Callee(x);
t := new();
x.f := t;
}
procedure Callee(x) {
...
}
In the following test case the order of the recursive calls is reversed. APE uses an encoding of mutual summaries to allow it to search for equivalences between procedure calls, please see Tim's thesis for further details. This test case also shows how APE takes advantage of procedure specifications that are available. Here the postcondition annotation modifies {r} is present and helps APE to prove that the procedures are equivalent. APE also checks that such annotations are correct.
VERSION 0
procedure Caller(x, r)
modifies {r};
{
if(x != null) {
r0 := new();
r1 := new();
t0 := x.f;
call Caller(t0, r0);
t1 := x.g;
call Caller(t1, r1);
r.f := r0.v;
r.g := r1.v;
}
}
VERSION 1
procedure Caller(x, r)
modifies {r};
{
if(x != null) {
r0 := new();
r1 := new();
t0 := x.g;
call Caller(t0, r0);
t1 := x.f;
call Caller(t1, r1);
r.g := r0.v;
r.f := r1.v;
}
}
The following examples copies a cyclic data structure. The versions vary in several ways:
- the nodes of the ring are allocated in the reverse order
- version 0 allocates an extra garbage element in the base case
- the sense and order of the conditional is reversed
- the order of several other instructions differ
The verification time is ~4s
VERSION 0
procedure CopyRing(head,r) {
if(head!=null) {
head' := new();
next := head.next;
call CopyRingUntil(next,head,head',r);
}
}
procedure CopyRingUntil(node,until,head',r) {
node' := new();
if(node==until) {
r.v := head';
} else {
next := node.next;
r' := new();
call CopyRingUntil(next,until,head',r');
node'.next := r'.v;
r.v := node';
}
}
VERSION 1
procedure CopyRing(head,r) {
if(head!=null) {
head' := new();
next := head.next;
call CopyRingUntil(next,head,head',r);
}
}
procedure CopyRingUntil(node,until,head',r) {
if(node!=until) {
r' := new();
next := node.next;
call CopyRingUntil(next,until,head',r');
node' := new();
r.v := node';
node'.next := r'.v;
} else {
r.v := head';
}
}
The following test case inserts a key/value pair into a table, replacing any existing occurrence of the key. The versions vary in several ways:
- In v1 the new row is always allocated at the start, and becomes garbage when the procedure eventually returns. Thus v1 sometimes allocates much more memory than v0.
- The order of several other instructions differ.
Verification time ~31s
VERSION 0
procedure Put(table,key,value,r) {
if(table!=null) {
if(table.key == key) {
r.v := table.value;
table.value := value;
} else {
l := new();
next := table.next;
call Last(next,l);
if(l.v != null) {
table.next := new();
table.next.key := key;
table.next.value := value;
} else {
call Put(next,key,value,r);
}
}
}
}
procedure Last(table,r)
{
if(table == null) {
r.v := new();
}
}
VERSION 1
procedure Put(table,key,value,r) {
row := new();
row.key := key;
row.value := value;
if(table!=null) {
next := table.next;
if(table.key == key) {
r.v := table.value;
table.value := value;
} else {
l := new();
call Last(next,l);
if(l.v != null) {
table.next := row;
} else {
call Put(next,key,value,r);
}
}
}
}
procedure Last(table,r)
{
if(table == null) {
r.v := new();
}
}
The following test case copies a list. The versions vary in several ways:
- The order of the allocations is reversed.
- v1 allocates the new node under different conditions to v0. This causes extra garbage for some executions of v1.
- An allocation that happens before the recursive call in v1 happens after in v0.
- The conditions for some instructions and the order of some assignments vary
Verification time ~7s
VERSION 0
procedure CopyList(x,y)
{
if(x!=null)
{
if(y!=null)
{
r := new();
xn := x.n;
call CopyList(xn, r);
t := new();
// copy head data here
t.n := r.v;
y.v := t;
}
}
}
VERSION 1
procedure CopyList(x,y)
{
if(x!=null)
{
t := new();
// copy head data here
xn := x.n;
if(y!=null)
{
r := new();
call CopyList(xn, r);
y.v := t;
t.n := r.v;
}
}
}
The following test case recursively copies a tree. The versions vary in several ways:
- The order of the recursive calls is reversed; v0 copies the left side of the tree first whereas v1 copies the right side first. APE uses an encoding of mutual summaries to allow it to search for equivalences between procedure calls, please see Tim Wood's Phd Thesis for further details.
- This test case also shows how APE takes advantage of procedure specifications that are available. In this case, the postcondition annotation
modifies {r}is present and helps APE to prove that the procedures are equivalent. APE also checks that such annotations are correct.
Verification time ~130s
VERSION 0
procedure CopyTree(x, r)
modifies {r};
{
if(x!=null) {
if(r!= null) {
r0 := new();
r1 := new();
n := new();
t0 := x.f;
call CopyTree(t0, r0);
t1 := x.g;
call CopyTree(t1, r1);
n.f := r0.v;
n.g := r1.v;
r.v := n;
}
}
}
VERSION 1
procedure CopyTree(x, r)
modifies {r};
{
if(x!=null) {
if(r!= null) {
r0 := new();
r1 := new();
t0 := x.g;
call CopyTree(t0, r1);
t1 := x.f;
call CopyTree(t1, r0);
n := new();
n.f := r0.v;
n.g := r1.v;
r.v := n;
}
}
}
Here we tabulate the other micro-benchmarks and test cases with a brief explaination of what each one shows
| Description | Reason | Case |
|---|---|---|
| Allocation moves past a call | Testing framing of unreachable allocations | AllocationMovesPastCall.bl |
| Allocations passed to call out of order | Testing procedure parameter isomorphism | AllocationsPassedToCall.bl |
| A procedure with a call | Testing modular verification | Call001.bl |
| A procedure with several calls | Testing modular verification | Call002.bl |
| A conditional is reversed and some procedures called | Testing solving of conditions | Conditional001.bl |
| Then else branches swapped | Test that non-equivalent conditionals fail to verify | Conditional002.bl |
| Longer example of a cycle | Testing several features together | CopyCycle.bl |
| A procedure is called with non-isomorphic parameters | Check that non-isomorphic parameters cause erification failure | DifferentParameters.bl |
| More garbage allocations in one version | Test that garbage with a complex shape is ignored | DifferInShapeOfGarbage.bl |
| Extra garbage is allocated | Test that garbage is ignored | DifferInSingleGarbageAllocation.bl |
| Memory allocated in different orders is made reachable | Test that allocation order is ignored | DoubleAllocationInDifferentOrders.bl |
| Empty procedures | Test that empty procedures are equivalent | Empty.bl |
| Allocation and call reordering | Test framing axioms | Frame001.bl |
| Memory allocated before a call is made reachable | Test framing axioms | Frame002.bl |
| Memory allocated before a call is modified non-isomorphically afterwards | Test that verification fails for non isomorphic memory when frame axioms are active | Frame003.bl |
| A procedure modifies something not in its modifies clause | Test that incorrect modifies clauses are detected | Frame005.bl |
| Pure procedures are called with non isomorphic parameters | Test that side effect free procedures can be reasoned about | Frame006.bl |
| The results of a procedure are ignored | Check that garbage created by a called procedure is ignored | FramedGarbageOnlyProcedure.bl |
| Side effect free procedures are called | Procedures without side effects are reasoned about | FramedNoopProcedure.bl |
| Procedures assign different values to fields | non-equivalence is detected | |
| Procedures allocate a list of length 4 and length 5 | non-equivalence deeper in the heap is detected | NonEquiv002.bl |
| Procedures create a deep heap structure with a difference | non-equivalence deeper in the heap is detected | NonEquiv003.bl |
| A tree is copied. One version copies the left side first the other the right side | Tests that a complex data structure and out-of-order procedure calls can be verified together | ProcedureReturnsValuesViaFramedTemporary.bl |
| Copies a list | Tests that recursive calls with out-of-order allocation and differences in garbage can be verified together | RecursiveListCopyExample.bl |
| Walks a list recursively | Tests that examples with no allocations verify | RecursivelyWalkList.bl |
| Calls are reordered | Tests that reordered calls can be verified | ReorderCalls.bl |
| Allocations are allocated out of order before a call | Enough information persists over the call to allow verification | ReverseAllocationsBeforeCall.bl |
| A single non-garbage allocation | A single allocation verifies | SingleAllocation.bl |
| Procedure call | A procedure call verifies | SingleCall.bl |
| Calls to different procedures | Calls to different procedure are not equivalent | SingleCallToDifferentProcedures.bl |
| A heap swap vs a stack swap | Tests that allocated memory can be used then discarded as garbage | Swap.bl |
| Inserts a row into a table | Tests that several features can be verified together, particularly that garbage is ignored correctly | TableInsert.bl |