System and method for overflow detection using symbolic analysis
A method for demand-driven symbolic analysis involves obtaining a section of code comprising an instruction from a source code file and determining a critical variable in the section of code and data dependencies related to the critical variable. The method further involves iteratively computing a symbolic value representing a range of values of the critical variable according to the data dependencies, determining a set of control predicates relevant to the critical variable at the instruction, refining the range of values according to the set of control predicates to generate a second range of values for the symbolic value, and reporting an error when the second range of values exceeds a predetermined value.
1. A method for demand-driven symbolic analysis for detecting overflow comprising:
obtaining, using a processor, a section of code comprising a first instruction from a source code file;
determining, using the processor, a critical variable in the section of code;
determining, using the processor, data dependencies related to the critical variable;
iteratively computing, using the processor, a symbolic value representing a first range of potential values of the critical variable at the first instruction according to the data dependencies, wherein the first instruction represents a point within the section of code where the symbolic value will be computed;
determining, using the processor, a first set of control predicates relevant to the critical variable at the first instruction;
refining, using the processor, the first range of potential values according to the first set of control predicates to generate a second range of potential values for the symbolic value; and
reporting, using the processor, an error when the second range of potential values exceeds a predetermined value.
2. The method of claim 1 , wherein iteratively computing the symbolic value comprises:
setting the symbolic value to an initial value; and
computing the symbolic value based on each operand defining the critical variable to obtain the first range of potential values.
3. The method of claim 2 , further comprising:
updating a plurality of symbolic ranges dependent on the symbolic value in response to computing the first range of potential values.
4. The method of claim 2 , further comprising:
storing the symbolic value in response to computing the first range of potential values.
5. The method of claim 1 , wherein the refining of the first range of potential values is path-sensitive.
6. The method of claim 1 , wherein the refining of the first range of potential values continues until a fixed point is reached.
7. The method of claim 1 , wherein the error comprises an integer overflow.
8. A system for demand-driven symbolic analysis for detecting overflow comprising:
a memory; and
a processor, operatively connected to the memory and having functionality to execute instructions for:
obtaining a section of code, comprising a first instruction, from a source code file;
determining a critical variable in the section of code;
determining data dependencies related to the critical variable;
iteratively computing a symbolic value representing a first range of potential values of the critical variable at the first instruction according to the data dependencies, wherein the first instruction represents a point within the section of code where the symbolic value will be computed;
determining a first set of control predicates relevant to the critical variable at the first instruction;
refining the first range of potential values according to the first set of control predicates to generate a second range of potential values for the symbolic value; and
reporting an error when the second range of potential values exceeds a predetermined value.
9. The system of claim 8 , wherein iteratively computing the symbolic value comprises:
setting the symbolic value to an initial value; and
computing the symbolic value based on each operand defining the critical variable to obtain the first range of potential values.
10. The system of claim 9 , further comprising functionality to execute instructions for:
updating a plurality of symbolic ranges dependent on the symbolic value in response to computing the first range of potential values.
11. The system of claim 9 , further comprising functionality to execute instructions for:
storing the symbolic value in response to computing the first range of potential values.
12. The system of claim 8 , wherein the refining of the first range of potential values is path-sensitive.
13. The system of claim 8 , wherein the refining of the first range of potential values continues until a fixed point is reached.
14. The system of claim 8 , wherein the error comprises an integer overflow.
15. A non-transitory computer readable storage medium storing instructions for demand-driven symbolic analysis for detecting overflow, the instructions with functionality to:
obtain a section of code, comprising a first instruction, from a source code file;
determine a critical variable in the section of code;
determine data dependencies related to the critical variable;
iteratively compute a symbolic value representing a first range of potential values of the critical variable at the first instruction according to the data dependencies, wherein the first instruction represents a point within the section of code where the symbolic value will be computed;
determine a first set of control predicates relevant to the critical variable at the first instruction;
refine the first range of potential values according to the first set of control predicates to generate a second range of potential values for the symbolic value; and
report an error when the second range of potential values exceeds a predetermined value.
16. The non-transitory computer readable storage medium of claim 15 , wherein iteratively computing the symbolic value comprises:
setting the symbolic value to an initial value; and
computing the symbolic value based on each operand defining the critical variable to obtain the first range of potential values.
17. The non-transitory computer readable storage medium of claim 16 , the instructions further comprising functionality to:
update a plurality of symbolic ranges dependent on the symbolic value in response to computing the first range of potential values.
18. The non-transitory computer readable storage medium of claim 16 , the instructions further comprising functionality to:
store the symbolic value in response to computing the first range of potential values.
19. The non-transitory computer readable storage medium of claim 15 , wherein the refining of the first range of potential values is path-sensitive.
20. The non-transitory computer readable storage medium of claim 15 , wherein the refining of the first range of potential values continues until a fixed point is reached.