An effective symbolic execution based technique for crosschecking C and OpenCL applications involving floating point. It has also been called KLEEFP.
Overview
KLEECL implements a symbolic executionbased technique for crosschecking programs accelerated using SIMD or OpenCL against an unaccelerated version, as well as a technique for detecting data races in OpenCL programs. KLEECL supports symbolic reasoning the equivalence between expressions involving both integer and floatingpoint operations.
While the current generation of constraint solvers provide effective support for integer arithmetic, the situation is different for floatingpoint arithmetic, due to the complexity inherent in such computations. The key insight behind our approach is that floatingpoint values are only reliably equal if they are essentially built by the same operations. This allows us to use an algorithm based on symbolic expression matching augmented with canonicalisation rules to determine path equivalence.
Under symbolic execution, we have to verify equivalence along every feasible controlflow path. We reduce the branching factor of this process by aggressively merging conditionals, ifconverting branches into select operations via an aggressive phinode folding transformation.
To support the Intel Streaming SIMD Extension (SSE) instruction set, we lower SSE instructions to equivalent generic vector operations, which in turn are interpreted in terms of primitive integer and floatingpoint operations.
To support OpenCL programs, we symbolically model the OpenCL environment using an OpenCL runtime library targeted to symbolic execution. We detect data races by keeping track of all memory accesses using a memory log, and reporting a race whenever we detect that two accesses conflict. By representing the memory log symbolically, we are also able to detect races associated with symbolicallyindexed accesses of memory objects.
We used KLEECL to prove the bounded equivalence between scalar and dataparallel versions of floatingpoint programs and find a number of issues in a variety of open source projects that use SSE and OpenCL, including mismatches between implementations, memory errors, race conditions and a compiler bug.
Download
KLEECL (also called KLEEFP) is available as open source here.
Research Support
This research project is generously sponsored by the UK EPSRC through through grants EP/I012036/1 and EP/I006761/1.
Publications

Symbolic Crosschecking of DataParallel FloatingPoint Code
Peter Collingbourne, Cristian Cadar, Paul H. J. Kelly
IEEE Transactions on Software Engineering (TSE 2014)

Symbolic Testing of OpenCL Code
Peter Collingbourne, Cristian Cadar, Paul H. J. Kelly
Haifa Verification Conference (HVC 2011)

Symbolic Crosschecking of FloatingPoint and SIMD Code
Peter Collingbourne, Cristian Cadar, Paul H. J. Kelly
European Conference on Computer Systems (EuroSys 2011)