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
  • Test Cases and Examples
    • Changing the order of allocations
    • Changing the amount allocated
    • Procedure Calls
      • Modular Verification
      • Allocations before a call
      • Isomorphism of heap region reachable from call parameters
      • Equivalent calls from non-isomorphic stores
        • Allocations may move past calls
        • Recursive calls may be reordered
    • Larger Examples
      • Recursively copying a cyclic data structure
      • Recursively inserting a row into a table
      • Recursively copy a list
      • Copy the sides of a tree in different orders
    • Tabulation of Testcases

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:

1. some of the memory that is garbage at the end of the procedure is made reachable during execution of v0
2. the garbage from v0 has different shape than the garbage from v1
3. 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:

1. the nodes of the ring are allocated in the reverse order
2. version 0 allocates an extra garbage element in the base case
3. the sense and order of the conditional is reversed
4. 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:

1. 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.
2. 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:

1. The order of the allocations is reversed.
2. v1 allocates the new node under different conditions to v0. This causes extra garbage for some executions of v1.
3. An allocation that happens before the recursive call in v1 happens after in v0.
4. 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:

1. 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.
2. 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