Terminating polymorphic type inference program analysis

• US 6,014,518 A
• Filed: 06/26/1997
• Issued: 01/11/2000
• Est. Priority Date: 06/26/1997
• Status: Expired due to Term

• Current Assignee: Microsoft Technology Licensing LLC (Microsoft Corporation)
• Original Assignee: Microsoft Corporation
• Inventors: Steensgaard, Bjarne
• Primary Examiner(s): Voeltz, Emanuel Todd
• Assistant Examiner(s): Chaki, Kakali
• Application Number:
  US08/882,746
• Time in Patent Office: 929 Days
• Field of Search: 395/705, 395/706, 395/707, 395/708, 395/709
• US Class Current: 717/154
• CPC Class Codes: G06F 8/437 Type checking

Abstract

A terminating polymorphic type inference program analysis helps to better optimize, understand, and/or browse computer programs. The analysis represents parameter values for each function call in the program with separate types and modifies the types to comply with typing constraints. The analysis also determines whether a potential non-terminating loop has been entered. If so, the analysis modifies the types such that the types comply with the typing constraints and such that the type inference analysis will terminate. In this manner, the analysis will generate a usable finite set of types for programs regardless of whether the principal typing for the program is infinite in size.

Claims

1. A method for performing a polymorphic type inference analysis for a program with a data processing system, the program comprising at least one function call, the method comprising the steps of:

a) representing parameter values for each function call in the program with separate types; and

b) modifying the types to comply with typing constraints, wherein the modifying step (b) comprises the steps of;

i) determining whether a potential non-terminating loop has been entered, and

ii) if a potential non-terminating loop has been entered, modifying the types such that the types comply with the typing constraints and such that the type inference analysis will terminate.

2. The method of claim 1, wherein the representing step (a) comprises the steps of representing a parameter variable for a function in the program with a generic type and representing a value for the parameter variable at a call site of the function with a substitution type for the generic type.

3. The method of claim 2, wherein the modifying step (b) comprises the step of defining a substitution type for a generic type having a generic type component such that the substitution type has a substitution type component for the generic type component.

4. The method of claim 2, wherein the modifying step (b) comprises the step of defining a first substitution type for a first generic type representing a potential pointer to a first location represented by a second generic type to represent a potential pointer to a second location represented by a second substitution type for the second generic type, wherein the first and second substitution types represent values for a same call site of a function.

5. The method of claim 2, wherein the modifying step (b) comprises the step of propagating constraints from generic types to substitution types;

and

wherein the determining step (b)(i) comprises the step of determining whether the propagation of a constraint from a generic type to a substitution type triggers another propagation of a constraint from a generic type to a substitution type.

6. The method of claim 2, wherein the determining step (b)(i) comprises the steps of identifying a first generic type having a type component and determining whether the type component is a substitution type reachable along a substitution path from a second generic type within a same function.

7. The method of claim 6, wherein the first generic type represents a potential pointer to a location represented by the type component.

8. The method of claim 6, wherein the modifying step (b)(ii) comprises the step of unifying the second generic type with the substitution type reachable along the substitution path from the second generic type.

9. The method of claim 6, wherein the modifying step (b)(ii) comprises the step of defining the substitution type reachable along the substitution path as a generic type for all substitution types for the second generic type.

10. The method of claim 6, wherein the modifying step (b) comprises the step of propagating constraints from generic types to substitution types;

and

wherein the determining step (b)(i) comprises the step of determining whether the substitution type reachable along the substitution path was created in propagating a constraint to the first generic type as a substitution type for a generic type having the constraint.

11. The method of claim 1, wherein the modifying step (b) comprises the step of prioritizing the modification of types for one function of the program over the modification of types for another function of the program.

12. The method of claim 1, comprising the step of representing globally accessible locations for the program with global types.

13. The method of claim 1, wherein each type is represented by a type variable and an associated type constructor.

14. The method of claim 1, wherein the method performs a pointer analysis using the polymorphic type inference analysis.

15. The method of claim 14, wherein the method performs the pointer analysis while compiling the program for execution by a data processing system.

16. A method for performing a polymorphic type inference pointer analysis for a program with a data processing system, the program comprising at least one function call, the method comprising the steps of:

a) representing locations for the program with separate types, wherein the representing step (a) comprises the step of representing parameter values for each function call in the program with separate types;

b) identifying a store usage for at least one location for the program;

c) determining whether at least one type representing the at least one location for the identified store usage complies with a typing constraint;

d) if the at least one type for the identified store usage does not comply with the typing constraint, modifying the at least one type to comply with the typing constraint; and

e) modifying types that represent locations for functions in the program and that are affected by the modifying step (d) to comply with typing constraints, wherein the modifying step (e) comprises the steps of;

i) determining whether a potential non-terminating loop has been entered, and

ii) if a potential non-terminating loop has been entered, modifying types such that the types comply with typing constraints and such that the type inference analysis will terminate.

17. The method of claim 16, wherein the representing step (a) comprises the steps of representing a parameter variable for a function in the program with a generic type and representing a value for the parameter variable at a call site of the function with a substitution type for the generic type.

18. The method of claim 17, wherein the modifying step (e) comprises the step of defining a first substitution type for a first generic type representing a potential pointer to a first location represented by a second generic type to represent a potential pointer to a second location represented by a second substitution type for the second generic type, wherein the first and second substitution types represent values for a same call site of a function.

19. The method of claim 17, wherein the modifying step (e) comprises the step of propagating constraints from generic types to substitution types;

and

wherein the determining step (e)(i) comprises the step of determining whether the propagation of a constraint from a generic type to a substitution type during the modifying step (e) triggers another propagation of a constraint from a generic type to a substitution type during the modifying step (e).

20. The method of claim 17, wherein the determining step (e)(i) comprises the steps of identifying a first generic type representing a potential pointer to a location and determining whether the location is represented by a substitution type reachable along a substitution path from a second generic type within a same function.

21. The method of claim 20, wherein the modifying step (e)(ii) comprises the step of unifying the second generic type with the substitution type reachable along the substitution path from the second generic type.

22. The method of claim 20, wherein the modifying step (e)(ii) comprises the step of defining the substitution type reachable along the substitution path as a generic type for all substitution types for the second generic type.

23. The method of claim 20, wherein the modifying step (e) comprises the step of propagating constraints from generic types to substitution types;

and

wherein the determining step (e)(i) comprises the step of determining whether the substitution type reachable along the substitution path was created during the modifying step (e) in propagating a points-to constraint to the first generic type as a substitution type for a generic type representing a potential pointer.

24. The method of claim 16, wherein the modifying step (e) comprises the step of prioritizing the modification of types for one function of the program over the modification of types for another function of the program.

25. The method of claim 16, wherein the representing step (a) comprises the step of representing globally accessible locations for the program with global types.

26. The method of claim 16, wherein each type is represented by a type variable and an associated type constructor.

27. The method of claim 26, wherein the method performs the pointer analysis while compiling the program for execution by a data processing system.

28. A memory for storing software for execution by a data processing system to perform a polymorphic type inference analysis for a program comprising at least one function call, the memory comprising:

a) program code stored by the memory for representing parameter values for each function call in the program with separate types; and

b) program code stored by the memory for modifying the types to comply with typing constraints, wherein the program code (b) comprises;

i) program code for determining whether a potential non-terminating loop has been entered, and

ii) program code for modifying the types such that the types comply with the typing constraints and such that the type inference analysis will terminate if a potential non-terminating loop has been entered.

29. The memory of claim 28, wherein the program code (a) comprises program code for representing a parameter variable for a function in the program with a generic type and for representing a value for the parameter variable at a call site of the function with a substitution type for the generic type.

30. The memory of claim 29, wherein the program code (b) comprises program code for defining a substitution type for a generic type having a generic type component such that the substitution type has a substitution type component for the generic type component.

31. The memory of claim 29, wherein the program code (b) comprises program code for defining a first substitution type for a first generic type representing a potential pointer to a first location represented by a second generic type to represent a potential pointer to a second location represented by a second substitution type for the second generic type, wherein the first and second substitution types represent values for a same call site of a function.

32. The memory of claim 29, wherein the program code (b) comprises program code for propagating constraints from generic types to substitution types;

and

wherein the program code (b)(i) comprises program code for determining whether the propagation of a constraint from a generic type to a substitution type triggers another propagation of a constraint from a generic type to a substitution type.

33. The memory of claim 29, wherein the program code (b)(i) comprises program code for identifying a first generic type having a type component and for determining whether the type component is a substitution type reachable along a substitution path from a second generic type within a same function.

34. The memory of claim 33, wherein the first generic type represents a potential pointer to a location represented by the type component.

35. The memory of claim 33, wherein the program code (b)(ii) comprises program code for unifying the second generic type with the substitution type reachable along the substitution path from the second generic type.

36. The memory of claim 33, wherein the program code (b)(ii) comprises program code for defining the substitution type reachable along the substitution path as a generic type for all substitution types for the second generic type.

37. The memory of claim 33, wherein the program code (b) comprises program code for propagating constraints from generic types to substitution types;

and

wherein the program code (b)(i) comprises program code for determining whether the substitution type reachable along the substitution path was created in propagating a constraint to the first generic type as a substitution type for a generic type having the constraint.

38. The memory of claim 28, wherein the program code (b) comprises program code for prioritizing the modification of types for one function of the program over the modification of types for another function of the program.

39. The memory of claim 28, comprising program code stored by the memory for representing globally accessible locations for the program with global types.

40. The memory of claim 28, comprising program code stored by the memory for representing each type by a type variable and an associated type constructor.

41. The memory of claim 28, comprising program code stored by the memory for performing a pointer analysis using the polymorphic type inference analysis.

42. The memory of claim 41, comprising program code stored by the memory for compiling the program for execution by a data processing system.

43. A data processing system comprising:

a) a translator for translating a program in a first language into code in a second language, wherein the program comprises at least one function call;

b) a pointer analyzer for performing a polymorphic type inference pointer analysis for the program, the pointer analyzer for representing parameter values for each function call in the program with separate types, for modifying the types to comply with typing constraints, for determining whether a potential non-terminating loop has been entered, and for modifying the types such that the types comply with the typing constraints and such that the type inference analysis will terminate if a potential non-terminating loop has been entered;

c) a store model for storing the types for the program; and

d) an optimizer for optimizing the code based on the store model.

44. The data processing system of claim 43, wherein the pointer analyzer represents a parameter variable for a function in the program with a generic type and represents a value for the parameter variable at a call site of the function with a substitution type for the generic type.

45. The data processing system of claim 44, wherein the pointer analyzer modifies types by defining a first substitution type for a first generic type representing a potential pointer to a first location represented by a second generic type to represent a potential pointer to a second location represented by a second substitution type for the second generic type, wherein the first and second substitution types represent values for a same call site of a function.

46. The data processing system of claim 44, wherein the pointer analyzer modifies types by propagating constraints from generic types to substitution types;

and

wherein the pointer analyzer determines a potential non-terminating loop has been entered by determining whether the propagation of a constraint from a generic type to a substitution type triggers another propagation of a constraint from a generic type to a substitution type.

47. The data processing system of claim 44, wherein the pointer analyzer determines a potential non-terminating loop has been entered by identifying a first generic type representing a potential pointer to a location and determining whether the location is represented by a substitution type reachable along a substitution path from a second generic type within a same function.

48. The data processing system of claim 47, wherein the pointer analyzer modifies types such that the types comply with the typing constraints and such that the type inference analysis will terminate by unifying the second generic type with the substitution type reachable along the substitution path from the second generic type.

49. The data processing system of claim 47, wherein the pointer analyzer modifies types such that the types comply with the typing constraints and such that the type inference analysis will terminate by defining the substitution type reachable along the substitution path as a generic type for all substitution types for the second generic type.

50. The data processing system of claim 47, wherein the pointer analyzer determines a potential non-terminating loop has been entered by determining whether the substitution type reachable along the substitution path was created in propagating a points-to constraint to the first generic type as a substitution type for a generic type representing a potential pointer.

51. The data processing system of claim 43, wherein the pointer analyzer prioritizes the modification of types for one function of the program over the modification of types for another function of the program.

52. The data processing system of claim 43, wherein the pointer analyzer represents globally accessible locations for the program with global types.

53. The data processing system of claim 43, wherein each type is represented by a type variable and an associated type constructor.