Symbolic Execution Equivalence of Heap Modifying Programs

Abstract

Equivalence check of two programs (or two versions of a program) is the problem of deciding if the two programs produce the same values as output for the same input. Symbolic execution is a program analysis technique that executes the programs under analysis using symbolic values. Several approaches and tools utilize symbolic execution to check equivalence. Existing symbolic execution implementations face multiple difficulties including scalability and limited support for language constructs. Current equivalence check approaches and implementations focus primarily on the scalability issue, often by abstracting unchanged parts of the programs under check. Despite the existence of several extensions to symbolic execution that deal with complex data types, current equivalence check implementations are incapable of performing equivalence checks for programs that deal with non-primitive data types. We present an equivalence checker that can check Java programs with non-primitive method parameters, fields, and return types., including parameterized types. The checker tracks input and output variables (e.g., instance and static fields, parameters, and returns) for changes throughout the symbolic execution of the program, and collects the transformations of those variables. The checker relies on a symbolic execution extension known as Lazy Initialization, to handle non-primitive data types, and extends the technique to further deal with parameterized types by utilizing type signatures. By supporting non-primitive types and more input and output variables, the checker extends the space of possible programs that we can check for equivalence.