Correct Handling of Floating-Point Computations in Symbolic Execution

Symbolic execution is a program testing technique which evaluates statements with symbolic input data along a selected path of the control flow graph. The process involves the computation of path conditions that tend to be simplified or solved in order either to get test data that sensitize the selected path or to demonstrate infeasibility of the path. In the presence of floating-point computations, the current strategy consists in using a constraint solver based on rationals or reals. Unfortunately, even when the computations conform ANSI/IEEE-754 floating-point arithmetic, this leads not only to approximative results but also to incorrect ones. For example, a path can be labeled as infeasible by using a constraint solver on the rationals although there exist floating-point input data that sensitize it. This paper shows how to evaluate symbolically the expressions when floating-point variables are involved in the computations. The focus is on the design and the implementation of projection functions required to solve path conditions over the floats. The proposed approach handles not only the numeric values of floating-point variables but also the symbolic values, such as infinities and NaNs. A symbolic execution environment of C floating-point computations is currently under development. Some very first experimental results are reported.