Performs differential testing using the KLEE symbolic execution tool extended with symbolic memory and lazy initialization to enable under-constrained symbolic execution (see ramos:sec:2015).
They demonstrate that differential symbolic execution (see person:fse:2008) can be used to compare different implementations of the same library API (NewLib vs. ucLibC), different versions of the same library (ucLibC), different compiler optimization levels (cf. yang:pldi:2011), and to find bugs in the tool itself.
In addition to (the substantial tasks of) adding symbolic memory and lazy initialization to KLEE, the main change was extending the KLEE API with the ability
- to take a snapshot of the address space;
- to restore the address space;
- to explicitly invoke the KLEE evaluator on a statement capturing any errors (I think this includes errors like division by zero or null pointer dereference);
- to compare errors; and
- to compare objects in memory.
Comparing objects in memory is challenging because the objects may have been allocated in different orders, at different addresses, etc. A mark-sweep algorithm is used to compare the structure of the heap rather than the concrete addresses.
As in their later work (ramos:sec:2015) but unlike the original lazy initialization work (khurshid:tacas:2003), the lazy initialization implementation does not explore object sharing so doubly linked lists or overlapping arguments to memcpy would not be explored.
Determining the size of objects is also hard: when an array of unknown size is generated, they initially guess a size of 8 and then keep doubling it if that fails.
They cap the number of objects allocated by lazy initialization.
Their evaluation showed that this was very effective at finding bugs and differences.
Papers related to Practical, low-effort equivalence verification of real code
- Under-constrained symbolic execution: Correctness checking for real code [ramos:sec:2015]