Apparatus and method for analyzing source code using path analysis and Boolean satisfiability
View Patent ↗A computer readable storage medium includes executable instructions to identify a path in target source code. Constraints associated with the path are extracted. The constraints are converted to a Boolean expression. The Boolean expression is processed with a Boolean satisfiability engine to identify either a feasible path or an infeasible path. A feasible path is statically analyzed, while an infeasible path is not statically analyzed.
1. A non-transitory computer readable storage medium, comprising executable instructions to:
identify a path in target source code of a program, wherein the path is a potential sequence of operations carried out when the program is executed;
extract constraints associated with the path;
convert the constraints to a Boolean expression;
process the Boolean expression with a Boolean satisfiability engine to identify either a feasible path or an infeasible path, wherein the infeasible path is a sequence of operations that is never carried out when the program is executed and a feasible path is a sequence of operations that is carried out when the program is executed;
perform a static analysis of a feasible path to report any bugs in the feasible path and omit static analysis of an infeasible path; and
executable instructions to bit width limit the input to the Boolean satisfiability engine.
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 parse the target source code.
4. The computer readable storage medium of claim 3 further comprising executable instructions to build a model of the target source code.
5. The computer readable storage medium of claim 4 further comprising executable instructions to identify a plurality of paths in the target source code.
6. A method comprising:
identifying a path in target source code of a program, wherein the path is a potential sequence of operations carried out when the program is executed;
extracting constraints associated with the path;
converting the constraints to a Boolean expression;
processing by a processor the Boolean expression with a Boolean satisfiability engine to identify either a feasible path or an infeasible path, wherein the infeasible path is a sequence of operations that is never carried out when the program is executed and a feasible path is a sequence of operations that is carried out when the program is executed; and
performing a static analysis of a feasible path to report any bugs in the feasible path and omit static analysis of an infeasible path.
7. The method of claim 6 , comprising:
limiting a bit width of the Boolean expression input to the Boolean satisfiablility engine.
8. The method of claim 6 , wherein the Boolean expression is expressed in Conjunctive Normal Form.
9. The method of claim 6 comprising:
parsing the target source code to identify the path.
10. The method of claim 6 , comprising:
building a model of the target source code to identify the path.
11. The method of claim 6 , comprising:
identifying a plurality of paths in the target source code, wherein either the feasible path or the infeasible path is identified from at least one of the plurality of paths.
12. A computer system comprising:
a hardware device to identify a path in target source code of a program, wherein the path is a potential sequence of operations carried out when the program is executed,
to extract constraints associated with the path,
to convert the constraints to a Boolean expression,
to process the Boolean expression with a Boolean satisfiability engine to identify either a feasible path or an infeasible path, wherein the infeasible path is a sequence of operations that is never carried out when the program is executed and a feasible path is a sequence of operations that is carried out when the program is executed, and
to perform a static analysis of a feasible path to report any bugs in the feasible path and omit static analysis of an infeasible path.
13. The computer system of claim 12 , wherein the hardware device is to limit a bit width the Boolean expression input to the Boolean satisfiablility engine.
14. The computer system of claim 12 , wherein the Boolean expression is expressed in Conjunctive Normal Form.
15. The computer system of claim 12 , wherein the hardware device is to parse the target source code to identify the path.
16. The The computer system of claim 12 , wherein the hardware device is to build a model of the target source code to identify the path.
17. The computer system of claim 12 , wherein the hardware device is to identify a plurality of paths in the target source code, wherein either the feasible path or the infeasible path is identified from at least one of the plurality of paths.