PET: Partial Evaluation-based Test Case Generator for Bytecode

CLP Heap Solver

One of the main challenges to software testing today is to efficiently handle heap-manipulating programs. These programs often build complex, dynamically allocated data structures during execution and, to ensure reliability, the testing process needs to consider all possible shapes these data structures can take. This creates scalability issues since high (often exponential) numbers of shapes may be built due to the aliasing of references.

We have developed a novel CLP heap solver for the test case generation of heap-manipulating programs that is more scalable than previous proposals (e.g. lazy initialization), thanks to the treatment of reference aliasing by means of disjunction, and to the use of advanced back-propagation of heap related constraints. In addition, the heap solver supports the use of heap assumptions to avoid aliasing of data that, though legal, should not be provided as input.

Using our CLP Heap Solver

The CLP Heap Solver is available as a standalone Prolog program. Some basic examples are provided and the user can also write up heap-manipulating programs manually. Please read the README file for a guide to the use of the heap solver.

Download CLP Heap Solver v1.0 (tar file) (updated June 24, 2013)

Experimental Evaluation

The CLP Heap Solver has been integrated in the web interface of PET. The following table allows the user to run a set of benchmarks and compare the results obtained by the standard execution of PET with no aliasing, the execution of PET considering aliasing explicitly and the execution of PET using the CLP Heap Solver.

Benchmark PET Standard PET+Aliasing CLP Heap Solver
DoublyLinkedList.add
Run
Run
Run
NodeSequence.removeAt
Run
Run
Run
NodeSequence.replaceAt
Run
Run
Run
SortedListPriorityQueue.insert
Run
Run
Run
SortedListPriorityQueue.remove
Run
Run
Run
BinarySearchTree.addAll
Run
Run
Run
BinarySearchTree.find
Run
Run
Run
BinarySearchTree.findAll
Run
Run
Run
BinarySearchTree.insert
Run
Run
Run
BinarySearchTree.remove
Run
Run
Run
HeapPriorityQueue.insert
Run
Run
Run
HeapPriorityQueue.remove
Run
Run
Run