Floating-point Program Symbolic Execution Platform Research

Program analysis technology is mainly divided into static analysis and dynamic analysis.Static analysis is not actual operating procedures,with great extensibility,but a high rate of false positives.The traditional dynamic analysis technology through actual operating procedures to ensure that the low rate of false positives,but fail to effectively cover the state space of the program.Symbolic execution using symbolic values as the inputs of the program which transform the execution of the program into the corresponding symbolic expressions by systematacially traverse routing space to realize the precise analysis of the program behaviors.However,due to the restriction of the path explosion and constraint solving problems,symbolic execution technology is poor scalability.Because of the shortages of the constraint solver support for floating-point operations currently,floating-point program symbolic execution has become a problem to hinder the application of the symbolic execution technology.This paper also implements a floating-point program symbolic execution technology on the open source symbolic execution tool KLEE that through transforming the floating-point operations into the corresponding integer operations at instruction level by introducing an external library.In order to verify the validity of the extension method,this study chosed 151 floating-point programs from the GSL library to test.In addition,this paper implemented a distributed symbolic execution platform which through a scheduling algorithm distributes tasks from master to slaves to realize tasks parallelly execute and reduced the symbolic execution time overhead.Using this platform,firstly,we evaluated the analysis efficiency of the distributed symbolic execution platform based on four groups contrast experiment,then we also analyzed 100 program packages more than 8500 K lines of C code and totally found 64 bugs.