Abstract interpretation with a congruence abstract domain and/or a heap succession abstract domain

• US 7,559,054 B2
• Filed: 04/19/2005
• Issued: 07/07/2009
• Est. Priority Date: 04/19/2005
• Status: Active Grant

• Current Assignee: Microsoft Technology Licensing LLC (Microsoft Corporation)
• Original Assignee: Microsoft Corporation
• Inventors: Chang, Bor-Yuh Evan, Leino, K. Rustan M.
• Primary Examiner(s): Zhen; Wei Y
• Assistant Examiner(s): DENG, ANNA CHEN
• Application Number:
  US11/110,108
• Publication Number:
  US 20060236311A1
• Time in Patent Office: 1,540 Days
• Field of Search: 717/126, 717140-146
• US Class Current: 717/126
• CPC Class Codes: G06F 11/3608 using formal methods, e.g. model checking, abstract interpretation theorem proving G06N5/013

Abstract

Techniques and tools are described for analyzing software. For example, an analysis tool performs abstract interpretation with a congruence abstract domain and/or a heap succession abstract domain. For the congruence abstract domain, the tool tracks equivalence classes between alien expressions and base domain variables. For the heap succession abstract domain, the tool tracks updates to a heap. In either case, to preserve information after updates, the tool may identify an expression having an unreachable value then determine an equivalent expression that lacks the unreachable value.

Claims

1. A computer system comprising:

computer memory and a central processing unit; and

a tool stored in the computer memory and executable by the central processing unit, wherein the tool comprises;

plural base domains comprising respective pluralities of base domain variables, wherein at least one of the plural base domains supports analysis of different functions than an other of the plural base domains; and

a congruence domain parameterized by the plural base domains, wherein the congruence domain is configured to infer symmetric relationships, reflexive relationships, transitive relationships, and whether expressions evaluate to a same base domain value;

wherein the tool further comprises at least one equivalence graph mapping alien expressions to the base domain variables, and wherein the equivalence graph tracks equalities between terms and maps equal expressions to a same value, wherein the expressions comprise program text variables or program functions; and

wherein the tool implementing the congruence domain operates in conjunction with the plural base domains to query the plural base domains for a replacement expression for a given expression, wherein the replacement expression does not mention a particular variable.

2. The computer system of claim 1 wherein the plural base domains include a heap succession domain that facilitates tracking of heap updates.

3. The computer system of claim 1 wherein the tool implementing the congruence domain operates in conjunction with the plural base domains to query each of the plural base domains about what expression information is understandable by each of the plural base domains, and to receive from each of the plural base domains information about what expression information is understandable within each of the plural base domains.

4. The computer system of claim 3 wherein the expression information is a function or relation symbol and its argument expressions.

5. The computer system of claim 1 wherein the tool also facilitates replacement of plural expressions having garbage values with plural equivalent expressions lacking the garbage values.

6. The computer system of claim 1 wherein, when adding constraints, the tool operates in conjunction with one or more base domains to identify the alien expressions based at least in part upon which of plural functions and/or relation symbols of a client computer program are supported in the one or more base domains.

7. The computer system of claim 1 wherein the tool operates in conjunction with one or more of the plural base domains to determine garbage values and to perform garbage collection for the determined garbage values.

13. The computer system of claim 3 wherein if query results indicate that a given expression is not supported, the tool replaces the given unsupported expression with a base domain variable.

14. The computer system of claim 13 wherein the tool tracks a mapping of the given unsupported expression to a base domain variable in one of the plural base domains.

8. A computer-implemented method comprising:

in a computer, representing plural base domains comprising respective pluralities of base domain variables, wherein at least one of the plural base domains supports analysis of different functions than an other of base domains of the plural base domains;

in the computer, implementing a congruence domain parameterized by the plural base domains, wherein the implementing comprises inferring symmetric relationships, inferring reflexive relationships, inferring transitive relationships, and inferring whether expressions evaluate to a same base domain value; and

in the computer, representing at least one equivalence graph mapping alien expressions to the base domain variables, wherein the representing comprises tracking equalities between terms and mapping equal expressions to a same value, wherein the expressions comprise program text variables or program functions;

identifying, for one of the base domains, an expression having one or more unreachable values;

determining an equivalent expression that lacks the one or more unreachable values;

requesting the equivalent expression from another base domain for use in the determining the equivalent expression;

if available via the requesting, receiving the requested equivalent expression, and replacing the expression of the one of the base domains that has the one or more unreachable values with the requested equivalent expression; and

otherwise, removing mapping with the one or more unreachable values from the equivalence graph, and eliminating the one or more unreachable values from the one of the base domains.

9. The method of claim 8 wherein software implementing the base domain provides information about what expression information is understandable within the base domain.

10. A computer-implemented method comprising:

in a computer, representing plural base domains comprising respective pluralities of base domain variables, wherein one or more of the plural base domains supports analysis of different functions than an other of the plural base domains;

in the computer, implementing a congruence domain parameterized by the plural base domains, wherein the implementing comprises inferring symmetric relationships, inferring reflexive relationships, inferring transitive relationships, and inferring whether expressions evaluate to a same base domain value; and

in the computer, representing at least one equivalence graph mapping alien expressions to the base domain variables, wherein the representing comprises tracking equalities between terms and mapping equal expressions to a same value, wherein the expressions comprise program text variables or program functions;

in at least one of the plural base domains, tracking one or more updates to a memory pool, wherein software implementing the at least one of the plural base domains facilitates replacement of expressions having one or more unreachable values; and

for an unreachable heap;

if a heap successor exists, providing the heap successor for replacement of the unreachable heap; and

otherwise, eliminating the unreachable heap;

wherein the at least one of the plural base domains includes one or more succession predicates for the tracking, and wherein each of the one or more succession predicates indicates one of the one or more updates.

11. The method of claim 10 wherein the one or more updates include a change for a field of an object of an object-oriented computer program, for an element of an array, or for a field of a record.

12. The method of claim 10 wherein the software implementing the at least one of the plural base domains also provides information about what symbols are understandable within the at least one of the plural base domains.

15. One or more computer-readable storage media having encoded thereon computer-executable instruction causing a computer to perform a method comprising:

in the computer, representing plural base domains comprising respective pluralities of base domain variables, wherein at least one of the plural base domains supports analysis of different functions than an other of the plural base domains;

in the computer, implementing a congruence domain parameterized by the plural base domains, wherein the implementing comprises inferring symmetric relationships, inferring reflexive relationships, inferring transitive relationships, and inferring whether expressions evaluate to a same base domain value; and

in the computer, representing at least one equivalence graph mapping alien expressions to the base domain variables, wherein the representing comprises tracking equalities between terms and mapping equal expressions to a same value, wherein the expressions comprise program text variables or program functions;

wherein at least one of the plural base domains comprises a heap succession abstract domain configured to track updates to a heap; and

wherein the heap succession abstract domain performs a method comprising;

for an unreachable heap;

if a heap successor exists, providing a heap successor for replacement of the unreachable heap; and

otherwise, eliminating the unreachable heap.

16. The method of claim 15 wherein the congruence domain introduces variables for use in a given base domain to stand for sub-expressions that are alien to the given base domain.