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

• US 20060236311A1
• Filed: 04/19/2005
• Published: 10/19/2006
• Est. Priority Date: 04/19/2005
• Status: Active Grant

• Current Assignee: Microsoft Technology Licensing LLC (Microsoft Corporation)
• Original Assignee: Microsoft Corporation
• Inventors: Leino, K. Rustan M., Chang, Bor-Yuh Evan
• Granted Patent: US 7,559,054 B2
• Time in Patent Office: Days
• US Class Current: 717/151
• 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 tool comprising software for tracking equivalence classes between plural alien expressions and plural base domain variables.

2. The tool of claim 1 wherein the software implements a congruence domain parameterized by plural base domains, and wherein at least one of the plural base domains supports analysis of different functions and/or relation symbols compared to the other base domains of the plural base domains.

3. The tool of claim 2 wherein the plural base domains include a heap succession domain that facilitates tracking of heap updates.

4. The tool of claim 2 wherein the software 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 the base domain.

5. The tool of claim 4 wherein the expression information is a function or relation symbol and its argument expressions.

6. The tool of claim 2 wherein the software implementing the congruence domain operates in conjunction with the plural base domains to query each of the plural base domains for a replacement expression for a given expression, wherein the replacement expression does not mention a particular variable.

7. The tool of claim 1 wherein the software also facilitates replacement of plural expressions having garbage values with plural equivalent expressions lacking the garbage values.

8. The tool of claim 1 wherein the software includes means for processing in a constrain routine, means for processing in a join routine, means for processing in a widen routine, means for processing in a rename routine, and means for processing in an eliminate routine.

9. The tool of claim 1 wherein, when adding constraints, the software operates in conjunction with one or more base domains to identify the plural 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.

10. The tool of claim 1 wherein the software operates in conjunction with one or more base domains to perform garbage collection for garbage values.

11. A method comprising:

identifying for an abstract domain an expression having one or more unreachable values; and

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

12. The method of claim 11 wherein software implementing the abstract domain includes a routine for providing information about equivalent expressions, wherein the identifying includes receiving parameters in an invocation of the routine, and wherein the routine returns the equivalent expression.

13. The method of claim 11 further comprising:

requesting information from another abstract domain for use in the determining the equivalent expression; and

receiving the requested information.

14. The method of claim 11 further comprising receiving in the abstract domain a variable mapped to expression information not understood within the abstract domain.

15. The method of claim 11 wherein software implementing the abstract domain provides information about what expression information is understandable within the abstract domain.

16. A method comprising, in an abstract domain, tracking one or more updates to a memory pool, wherein software implementing the abstract domain facilitates replacement of expressions having one or more unreachable values.

17. The method of claim 16 wherein the abstract domain 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.

18. The method of claim 16 further comprising, 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.

19. The method of claim 16 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.

20. The method of claim 16 wherein the software implementing the abstract domain also provides information about what symbols are understandable within the abstract domain.