Apparatus and method for analyzing source code using memory operation evaluation and boolean satisfiability
A computer readable storage medium includes executable instructions to identify a memory operation in target source code. A set of constraints associated with the memory operation are developed. The constraints are converted into a Boolean expression. The Boolean expression is processed with a Boolean satisfiability engine to determine whether the memory operation is potentially unsafe.
1. A computer readable storage medium, comprising executable instructions to:
identify a memory operation in target source code;
develop a set of constraints associated with the memory operation, wherein the set of constraints includes base constraints derived from the target source code and additional constraints for forcing the memory operation to be out of bounds;
convert the constraints into a Boolean expression; and
process the Boolean expression with a Boolean satisfiability engine to determine whether the memory operation is potentially unsafe by executing instructions to:
determine whether the memory operation is always safe;
determine whether the memory operation is safe for a number of inputs if the memory operation is determined to be not always safe; and
test boundary conditions for the memory operation if the memory operation is safe for at least some of the number of inputs, wherein the boundary conditions include the base constraints, constraints requiring the memory operation to be within bounds, and constraints for runtime limitations.
2. The computer readable storage medium of claim 1 wherein the Boolean expression is expressed in Conjunctive Normal Form (CNF).
3. The computer readable storage medium of claim 1 further comprising executable instructions to test the boundary conditions to determine if the memory operation is always safe.
4. The computer readable storage medium of claim 3 further comprising executable instructions to determine unsafe operations.
5. The computer readable storage medium of claim 3 further comprising executable instructions to report unsafe operations.
6. The computer readable storage medium of claim 3 further comprising executable instructions to test boundary conditions from base constraints derived from constructs in a memory operation.
7. The computer readable storage medium of claim 3 further comprising executable instructions to test boundary conditions derived from constraints requiring an operation to be within bounds.
8. The computer readable storage medium of claim 3 further comprising executable instructions to test boundary conditions from additional constraints that limit function inputs and global variables to values that will carry during execution.
9. The computer readable storage medium of claim 3 further comprising executable instructions to test boundary conditions from examining branch predicates in a function to infer expected boundary conditions.
10. The computer readable storage medium of claim 3 further comprising executable instructions to test boundary conditions from examining the contexts in which the function is used to determine a set of known possible values for function inputs.
11. The computer readable storage medium of claim 1 further comprising executable instructions to bit width limit the input to the Boolean satisfiability engine.
12. The computer readable storage medium of claim 1 further comprising executable instructions to parse the target source code.
13. The computer readable storage medium of claim 1 further comprising executable instructions to build a model of the target source code.
14. The computer readable storage medium of claim 1 further comprising instructions to develop the set of constraints representing constant values and control structures for the memory operation.
15. The computer readable storage medium of claim 1 further comprising instructions to convert the constraints into the Boolean expression that force the memory operation out of bounds of the memory operation.