Optimizing libraries for validating C++ programs using symbolic execution

1. A method comprising: by one or more computing devices,

using a source code-to-source code rewrite to optimize a C++ function comprising one or more loops for symbolic execution, comprising:

for a first loop of the one or more loops, the first loop comprising a first branching condition, performing semantics preserving source code-to-source code rewrite to convert the first loop to move the first branching condition outside the loop; and

for a second loop of the one or more loops, the second loop comprising a second branching condition, rewriting the second loop to include a symbolic variable representing a return value and to replace the second loop with an equivalent logical formula relating the symbolic variable with inputs of the C++ function; and

wherein:

the C++ function comprises a C++ library function,

the C++ function further comprises one or more conditional branches,

using the source code-to-source code rewrite to optimize the C++ function comprises using a hack-in function to access the symbolic executor to move the exploration of the multiple paths from within the symbolic executor to within the solver, and

using the source code-to-source code rewrite for the first loop and the second loop moves the exploration of multiple paths from within a symbolic executor to within a solver.

2. The method of claim 1 , wherein the C++ function further comprises one or more execution paths, and the method further comprises:

for each execution path, reducing a symbolic expression obtained for the execution path by implementing a decision procedure into source code of the C++ function.

3. The method of claim 1 , wherein the C++ function further comprises one or more conditional branches, and the method further comprises:

for each conditional branch, constructing a symbolic expression using an intermediate language to delay interpretation of the C++ function to the conditional branch.

4. The method of claim 1 , wherein moving the exploration of multiple paths from within the symbolic executor to within a solver comprises implementing a string solver by purely modifying the source code.

5. A system comprising:

a memory comprising instructions executable by one or more processors; and

the one or more processors coupled to the memory and operable to execute the instructions, the one or more processors being operable when executing the instructions to:

use a source code-to-source code rewrite to optimize a C++ function comprising one or more loops for symbolic execution by:

for a first loop of the one or more loops, the first loop comprising a first branching condition, performing semantics preserving source code-to-source code rewrite to convert the first loop to move the first branching condition outside the loop; and

for a second loop of the one or more loops, the second loop comprising a second branching condition, rewriting the second loop to include a symbolic variable representing a return value and to replace the second loop with an equivalent logical formula relating the symbolic variable with inputs of the C++ function; and

wherein:

the C++ function comprises a C++ library function,

the C++ function further comprises one or more conditional branches,

using the source code-to-source code rewrite to optimize the C++ function comprises using a hack-in function to access the symbolic executor to move the exploration of the multiple paths from within the symbolic executor to within the solver, and

using the source code-to-source code rewrite for the first loop and the second loop moves the exploration of multiple paths from within a symbolic executor to within a solver.

6. The system of claim 5 , wherein the C++ function further comprises one or more execution paths, and the one or more processors are further operable when executing the instructions to:

for each execution path, reduce a symbolic expression obtained for the execution path by implementing a decision procedure into source code of the C++ function.

7. The system of claim 5 , wherein the C++ function further comprises one or more conditional branches, and the one or more processors are further operable when executing the instructions to:

for each conditional branch, construct a symbolic expression using an intermediate language to delay interpretation of the C++ function to the conditional branch.

8. The system of claim 5 , wherein moving the exploration of multiple paths from within the symbolic executor to within a solver comprises implementing a string solver by purely modifying the source code.

9. One or more computer-readable non-transitory storage media embodying software operable when executed by one or more computer systems to:

use a source code-to-source code rewrite to optimize a C++ function comprising one or more loops for symbolic execution by:

for a first loop of the one or more loops, the first loop comprising a first branching condition, performing semantics preserving source code-to-source code rewrite to convert the first loop to move the first branching condition outside the loop; and

for a second loop of the one or more loops, the second loop comprising a second branching condition, rewriting the second loop to include a symbolic variable representing a return value and to replace the second loop with an equivalent logical formula relating the symbolic variable with inputs of the C++ function; and

wherein:

the C++ function comprises a C++ library function,

the C++ function further comprises one or more conditional branches,

using the source code-to-source code rewrite to optimize the C++ function comprises using a hack-in function to access the symbolic executor to move the exploration of the multiple paths from within the symbolic executor to within the solver, and

using the source code-to-source code rewrite for the first loop and the second loop moves the exploration of multiple paths from within a symbolic executor to within a solver.

10. The computer-readable non-transitory storage media of claim 9 , wherein the C++ function further comprises one or more execution paths, and the software is further operable when executed by one or more computer systems to:

for each execution path, reduce a symbolic expression obtained for the execution path by implementing a decision procedure into source code of the C++ function.

11. The computer-readable non-transitory storage media of claim 9 , wherein the C++ function further comprises one or more conditional branches, and the software is further operable when executed by one or more computer systems to:

for each conditional branch, construct a symbolic expression using an intermediate language to delay interpretation of the C++ function to the conditional branch.

12. The computer-readable non-transitory storage media of claim 9 , wherein moving the exploration of multiple paths from within the symbolic executor to within a solver comprises implementing a string solver by purely modifying the source code.

13. A system comprising:

means for using a source code-to-source code rewrite to optimize a C++ function comprising one or more loops for symbolic execution, comprising:

for a first loop of the one or more loops, the first loop comprising a first branching condition, means for performing semantics preserving source code-to-source code rewrite to convert the first loop to move the first branching condition outside the loop; and

for a second loop of the one or more loops, the second loop comprising a second branching condition, means for rewriting the second loop to include a symbolic variable representing a return value and means for replacing the second loop with an equivalent logical formula relating the symbolic variable with inputs of the C++ function; and

wherein:

the C++ function comprises a C++ library function,

the C++ function further comprises one or more conditional branches,

using the source code-to-source code rewrite to optimize the C++ function comprises using a hack-in function to access the symbolic executor to move the exploration of the multiple paths from within the symbolic executor to within the solver, and

using the source code-to-source code rewrite for the first loop and the second loop moves an exploration of multiple paths from within a symbolic executor to within a solver.

14. The system of claim 13 , wherein moving the exploration of multiple paths from within the symbolic executor to within a solver comprises implementing a string solver by purely modifying the source code.