We present an effective technique for crosschecking an IEEE 754 ﬂoating-point program and its SIMD-vectorized version, implemented in KLEE-FP, an extension to the KLEE symbolic execution tool that supports symbolic reasoning on the equivalence between ﬂoating-point values.
The key insight behind our approach is that floating-point values are only reliably equal if they are essentially built by the same operations. As a result, our technique works by lowering the Intel Streaming SIMD Extension (SSE) instruction set to primitive integer and ﬂoating-point operations, and then using an algorithm based on symbolic expression matching augmented with canonicalization rules.
Under symbolic execution, we have to verify equivalence along every
feasible control-flow path. We reduce the branching factor of this
process by aggressively merging conditionals, if-converting branches
select operations via an aggressive phi-node folding transformation.
We applied KLEE-FP to OpenCV, a popular open source computer vision library. KLEE-FP was able to successfully crosscheck 51 SIMD/SSE implementations against their corresponding scalar versions, proving the bounded equivalence of 41 of them (i.e., on images up to a certain size), and ﬁnding inconsistencies in the other 10.