Path-sensitive static analysis
A method may include obtaining, from one of the rules of a static analysis, a built-in path relation describing a path constraint on a path variable, generating, using the rules, a transfer function that updates a property vector while analyzing code, generating an evaluation function that determines, using the updated property vector, whether the static analysis is satisfied, and determining whether the code includes a defect by executing the static analysis on the code using the path constraint, the transfer function, and the evaluation function.
1. A method, comprising:
obtaining, from a rule of a plurality of rules of a static analysis, a built-in path relation describing a path constraint on a path variable, wherein the built-in path relation comprises a path condition;
generating, using the plurality of rules, a transfer function that updates a property vector while analyzing code;
generating an evaluation function that determines, using the updated property vector, whether the static analysis is satisfied; and
determining whether the code comprises a defect by executing the static analysis on the code using the path constraint, the transfer function, and the evaluation function, wherein executing the static analysis comprises determining whether a branch condition of the code satisfies the path condition.
2. The method of claim 1 , further comprising:
generating a report comprising a path satisfying the path constraint, wherein the path comprises a series of instructions in the code, and wherein the path corresponds to the defect.
3. The method of claim 1 , further comprising:
generating an imperative instruction that updates the property vector, wherein the transfer function comprises the imperative instruction.
4. The method of claim 1 , further comprising:
inlining one or more user-defined relations comprising the path variable until each relation comprising the path variable is a built-in path relation, wherein the relation is in a body of a rule of the plurality of rules.
5. A system, comprising:
a memory coupled to a computer processor;
a repository configured to store code, a property vector, and a static analysis comprising a plurality of rules;
a code analyzer, executing on the computer processor and using the memory, configured to:
obtain, from a rule of the plurality of rules, a built-in path relation describing a path constraint on a path variable, wherein the built-in path relation comprises a path condition,
generate, using the plurality of rules, a transfer function that updates the property vector while analyzing the code, and
generate an evaluation function that determines, using the updated property vector, whether the static analysis is satisfied; and
a dataflow engine, executing on the computer processor and using the memory, configured to determine whether the code comprises a defect by executing the static analysis on the code using the path constraint, the transfer function, and the evaluation function, wherein executing the static analysis comprises determining whether a branch condition of the code satisfies the path condition.
6. The system of claim 5 , wherein the code analyzer is further configured to:
generate a report comprising a path satisfying the path constraint, wherein the path comprises a series of instructions in the code, and wherein the path corresponds to the defect.
7. The system of claim 5 , wherein the code analyzer is further configured to:
generate an imperative instruction that updates the property vector, wherein the transfer function comprises the imperative instruction.
8. A non-transitory computer readable medium comprising instructions that, when executed by a computer processor, perform:
obtaining, from a rule of a plurality of rules of a static analysis, a built-in path relation describing a path constraint on a path variable, wherein the built-in path relation comprises a path condition;
generating, using the plurality of rules, a transfer function that updates a property vector while analyzing code;
generating an evaluation function that determines, using the updated property vector, whether the static analysis is satisfied; and
determining whether the code comprises a defect by executing the static analysis on the code using the path constraint, the transfer function, and the evaluation function, wherein executing the static analysis comprises determining whether a branch condition of the code satisfies the path condition.
9. The non-transitory computer readable medium of claim 8 , further comprising instructions that perform:
generating a report comprising a path satisfying the path constraint, wherein the path comprises a series of instructions in the code, and wherein the path corresponds to the defect.
10. The non-transitory computer readable medium of claim 8 , further comprising instructions that perform:
generating an imperative instruction that updates the property vector, wherein the transfer function comprises the imperative instruction.
11. A method, comprising:
obtaining, from a rule of a plurality of rules of a static analysis, a built-in path relation describing a path constraint on a path variable;
identifying a correlated variable comprised by a subset of the plurality of rules;
generating a property vector by creating a flag for an expression that defines a value of the correlated variable;
generating, using the plurality of rules, a transfer function that updates the property vector while analyzing code;
generating an evaluation function that determines, using the updated property vector, whether the static analysis is satisfied; and
determining whether the code comprises a defect by executing the static analysis on the code using the path constraint, the transfer function, and the evaluation function.
12. The method of claim 11 , further comprising:
prioritizing the subset, wherein the property vector is generated, based on the prioritizing, using a rule in the subset.
13. The method of claim 11 , wherein the property vector is further generated by creating a flag for an independent instruction.
14. A system, comprising:
a memory coupled to a computer processor;
a repository configured to store code, a property vector, and a static analysis comprising a plurality of rules;
a code analyzer, executing on the computer processor and using the memory, configured to:
obtain, from a rule of the plurality of rules, a built-in path relation describing a path constraint on a path variable,
identify a correlated variable comprised by a subset of the plurality of rules,
generate a property vector by creating a flag for an expression that defines a value of the correlated variable,
generate, using the plurality of rules, a transfer function that updates the property vector while analyzing the code, and
generate an evaluation function that determines, using the updated property vector, whether the static analysis is satisfied; and
a dataflow engine, executing on the computer processor and using the memory, configured to determine whether the code comprises a defect by executing the static analysis on the code using the path constraint, the transfer function, and the evaluation function.
15. The system of claim 14 , wherein the code analyzer is further configured to:
prioritize the subset, wherein the property vector is generated, based on the prioritizing, using a rule in the subset.
16. The system of claim 14 , wherein the property vector is further generated by creating a flag for an independent instruction.
17. A non-transitory computer readable medium comprising instructions that, when executed by a computer processor, perform:
obtaining, from a rule of a plurality of rules of a static analysis, a built-in path relation describing a path constraint on a path variable;
identifying a correlated variable comprised by a subset of the plurality of rules;
generating a property vector by creating a flag for an expression that defines a value of the correlated variable;
generating, using the plurality of rules, a transfer function that updates the property vector while analyzing code;
generating an evaluation function that determines, using the updated property vector, whether the static analysis is satisfied; and
determining whether the code comprises a defect by executing the static analysis on the code using the path constraint, the transfer function, and the evaluation function.
18. The non-transitory computer readable medium of claim 17 , further comprising instructions that perform:
prioritizing the subset, wherein the property vector is generated, based on the prioritizing, using a rule in the subset.
19. The non-transitory computer readable medium of claim 17 , wherein the property vector is further generated by creating a flag for an independent instruction.