Research And Implementation Of Instrumentation Based On Symbolic Execution

With the proposal of “Internet Plus”, computer technology is gradually applied into traditional industry, which provides a chance for the modernization of these traditional enterprises. However, during the process of development, new requirements for the update of computer technology are generating with the progress in traditional industry. The quality and security of computer software has always been an important issue in the process of software development, especially in the field of national defense, finance, healthcare and so on. Software testing is a commonly used method to protect the quality and security of the software, and the development of software inevitably accompanies with repeated testing process, so software testing is particularly important for the developers. The process of software testing consists of constructing test cases, running the program, comparing the output value with the expected, modifying the program, and repeats these procedures in sequence. The preceding steps seem ordinary but have some defects, because the test cases which constructed by developers are not very perfect. Critical path in the program may be missed or defective path cannot be triggered when using these test cases to execute the under-test programs, thus the existing problems can be omitted.Although it is almost impossible to get all the paths by method of manual exhaustion, the program can achieve this goal. For instance, automatic test cases generation based on dynamic symbolic execution theory can solve the above problem effectively. Using dynamic symbolic execution techniques to generate test cases can achieve full path coverage, which provides theoretical foundation for the method of manual exhaustion. Our research group uses dynamic symbolic execution technology and develops a tool which automatically generates test cases for unit testing of C language on Linux platform. The main contribution of this thesis is the instrumentation part of the tool. That is analyzing the LLVM IR(LLVM Intermediate Presentation) code of a C program by LLVM compiler framework, and inserting additional instructions(stub function) in the relative position of LLVM IR, and then simulating the principle of stack machine to implement the stub function. When the instrumented program being executed, the symbolic execution process is triggered by these stub functions, and it will automatic generate test cases. Although this type of tools has applied in the actual project, there are still many places to be improved in dynamic symbolic execution, such as the path explosion, external function calls, and floating-point processing etc. This thesis presents a new idea to deal with floating-point problem.In order to verify the correctness of the test case automatic generation tool, this thesis adopts two small programs and a big program in benchmark of program analysis to test the tool. Firstly, this thesis introduces the testing procedures are introduced by simple programs, and explains the files and data obtained during the test. The final experimental results validate the rightness of instrumentation part and floating-point solution. Then the effectiveness of this tool is testified by having a complete testing for the tool with big program in benchmark.