Modular verification of equivalence for memory allocating procedures

Abstract

Verifying the equivalence of programs has been applied in many situations: for example, proving the correctness of bug-fixes, refactorings, compilation, and optimisation, proving program continuity, proving non-interference in secure information flow, proving abstraction and refinement relationships between programs, and proving that programs conform to differential privacy policies. Verifying the equivalence of heap manipulating procedures where the order and amount of memory allocations differ is challenging for state-of-the-art equivalence verifiers. We describe a fully automatic program equivalence tool, and propose a verification methodology, for such dynamically allocating programs.

Recent years have seen significant progress toward fully automatic program equivalence verification, with the release of several tools taking a variety of approaches. Two main approaches are to use a weakest-precondition based program verifier or a bounded model checker. One such tool has built in support for programs that differ in the order of memory allocation, it uses a bounded model checker to discharge some proof obligations and restricts the allowable shapes of heap data structures to trees.

We describe a fully automatic program equivalence verification tool for a simple object oriented language. It has a notion of procedure equivalence that is powerful enough to allow procedures with different orders and amounts of memory allocation or garbage creation to be considered equivalent, with no restrictions on heap shapes. Our tool establishes equivalence by verifying that procedures result in isomorphic heaps. The tool is built on top of an off-the-shelf weakest-precondition based verifier which itself uses an SMT solver to discharge proof obligations.

A naive encoding of procedure equivalence would require the verification tool to produce a witness to the heap isomorphism before and after procedure calls, which SMT based tools are not very good at. Instead we propose a modular verification methodology, called RIE, that allows us to soundly establish heap isomorphism by checking that an approximation preserves heap equality. RIE then allows us to assume that: whenever we can establish an isomorphism between parts of stores that these stores are in fact equal, and that whenever equivalent procedures are called in an isomorphic manner their effects are equal. RIE also allows our tool to handle some cases where there is not a simulation between the recursive procedure calls of the programs being compared. We prove, and provide intuitions, that RIE is sound for a simple programming language that includes non-deterministic allocation, unbounded recursion, and unbounded heap updates.