Floating-Point Exception Detection Based On Symbolic Execution And Interval Arithmetic

At present, the floating point arithmetic is widely used in the modern computer science, application fields such as military, aerospace, scientific research, finance, signal processing are involved. However, floating point operations may produce exceptions due to the limited precision of floating point number and the range of expression of computer, such as overflow, under overflow, zero and invalid. Floating point exceptions will lead to the failure of the calculation program and cost millions of economic losses and even the price of life.How to ensure the trustworthiness of the floating point program needs to be solved urgently. It is particularly important to detect floating-point exception which is one of the most prominent issues in trusted compute field. Considering the considerable proportion of applications of C language in various fields, this article aims to study the methods of the floating-point exception detection of C language program, and help programmers and the scientific researchers who have related work with floating point arithmetic.These can be practical valuable for scientific computing. The main work of this paper are as follows.1. Floating point exceptions under the standard of IEEE 754 are studied. The conditions of floating point exceptions of C language is analyzed based on the study of the causes of exceptions. Constraints are constructed and then sample points of exceptions are obtained combined with the theory of symbolic execution and constraint solving, thus the potential exceptions are excavated.2. For programs whose inputs are given, combined with the exception marking functions of C standard library and the theory of interval arithmetic, whether an exact input will trigger an exception as well as the exception situation of a program in a range of input values are respectively detected. When detecting the exceptions of a range of inputs, the LOC-ECP algorithm based on branch and bound is designed. We can locate the exact sample point in a given range.3. The corresponding C-oriented program analysis and rewriting tool CPART (C program analysis and rewriting tool) is developed combined with the method of floating point exception detection. The tool can be used to analyze the grammatical structure of the target program and embed the corresponding detection method in the appropriate position so as to rewrite the program.4. The floating point exceptions of the functions of an Aerospace Engineering and GNU Scientific Library (GSL) are detected and captured using the tool and methods mentioned in the article. The experimental results show that our tool can effectively analyze and rewrite the program and the detection methods are scientific and effective.