Optimizing libraries for validating C++ programs using symbolic execution

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.

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.

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.