Software architecture for validating C++ programs using symbolic execution

摘要

Particular embodiment compile a C++ program having one or more input variables to obtain bytecode of the C++ program; compile a C++ library to obtain bytecode of the C++ library; symbolically execute the bytecode of the C++ program and the bytecode of the C++ library, comprising assign a symbolic input to each input variable of the C++ program; determine one or more execution paths in the C++ program; and for each execution path, construct a symbolic expression that if satisfied, causes the C++ program to proceed down the execution path; and generate one or more test cases for the C++ program by solving the symbolic expressions.

主权项

1. A method comprising: by one or more computing devices,
compiling a C++ program having one or more input variables to obtain bytecode of the C++ program; modifying a standard C++ library associated with the C++ program to create an optimized C++ library, the optimized C++ library used for symbolic execution and the standard C++ library used for concrete execution, wherein modifying the standard C++ library comprises rewriting one or more classes defined in the standard C++ library to result in fewer execution paths; compiling the optimized C++ library to obtain bytecode of the optimized C++ library; symbolically executing the bytecode of the C++ program and the bytecode of the optimized C++ library, comprising:
assigning a symbolic input to each input variable of the C++ program;determining one or more execution paths in the C++ program; andfor each execution path, constructing a symbolic expression that if satisfied, causes the C++ program to proceed down the execution path; generating one or more test cases for the C++ program by solving each of the symbolic expressions, the one or more test cases indicating values that satisfy a feasible execution path of the C++ program with respect to the symbolic input; and testing the C++ program by compiling the C++ program to obtain machine code and applying the test cases as input to the machine code.