Feedback-directed call graph expansion

1. A machine-implemented method for feedback-directed call graph expansion, comprising:

performing symbolic analysis on an interprocedural control flow graph representation of software code;

skipping over a virtual method call in said control flow graph;

using information obtained from said symbolic analysis as feedback to identify a target of said virtual method call; and

iterating said symbolic analysis on a modified version of said control flow graph that associates said target with said virtual method.

2. The method of claim 1 , wherein said information represents a type constraint on said method call that is revealed by said symbolic analysis.

3. The method of claim 1 , wherein said symbolic analysis comprises a backward analysis to determine a weakest precondition at an entry point of said software code based on a desired logical state at some program point of said software code.

4. The method of claim 3 , wherein said virtual method call is skipped by using a special form of symbolic formula that represent constraints on said virtual method call.

5. The method of claim 4 , wherein said special type of symbolic formula contains one or more skolem constants that define said constraints using existential quantifiers.

6. The method of claim 1 , wherein said control flow graph contains more than one virtual method call and said method iterates said symbolic analysis for each of said virtual method calls.

7. A system, comprising:

a CPU;

a memory operatively coupled to said CPU, said memory including a storage medium tangibly embodying a program of instructions executable by said CPU to perform operations for implementing feedback-directed call graph expansion, comprising:

performing symbolic analysis on an interprocedural control flow graph representation of software code;

skipping over a virtual method call in said control flow graph;

using information obtained from said symbolic analysis as feedback to identify a target of said virtual method call; and

iterating said symbolic analysis on a modified version of said control flow graph that associates said target with said virtual method.

8. The system of claim 7 , wherein said information represents a type constraint on said method call that is revealed by said symbolic analysis.

9. The system of claim 7 , wherein said symbolic analysis comprises a backward analysis to determine a weakest precondition at an entry point of said software code based on a desired logical state at some program point of said software code.

10. The system of claim 9 , wherein said virtual method call is skipped by using a special form of symbolic formula that represent constraints on said virtual method call.

11. The system of claim 10 , wherein said special type of symbolic formula contains one or more skolem constants that define said constraints using existential quantifiers.

12. The system of claim 7 , wherein said control flow graph contains more than one virtual method call and said method iterates said symbolic analysis for each of said virtual method calls.

13. A computer program product, comprising:

one or more computer-readable storage media:

program instructions stored on said one or more storage media for programming a CPU to perform operations for implementing feedback-directed call graph expansion, comprising:

performing symbolic analysis on an interprocedural control flow graph representation of software code;

skipping over a virtual method call in said control flow graph;

using information obtained from said symbolic analysis as feedback to identify a target of said virtual method call; and

iterating said symbolic analysis on a modified version of said control flow graph that associates said target with said virtual method.

14. The computer program product of claim 13 , wherein said information represents a type constraint on said method call that is revealed by said symbolic analysis.

15. The computer program product of claim 13 , wherein said symbolic analysis comprises a backward analysis to determine a weakest precondition at an entry point of said software code based on a desired logical state at some program point of said software code.

16. The computer program product method of claim 15 , wherein said virtual method call is skipped by using a special form of symbolic formula that represent constraints on said virtual method call.

17. The computer program product of claim 16 , wherein said special type of symbolic formula contains one or more skolem constants that define said constraints using existential quantifiers.

18. The computer program product of claim 13 , wherein said control flow graph contains more than one virtual method call and said method iterates said symbolic analysis for each of said virtual method calls.

19. A machine-implemented method for feedback-directed call graph expansion, comprising:

performing symbolic analysis on an interprocedural control flow graph representation of software code;

skipping over virtual method calls in said control flow graph;

for each of said virtual method calls:

using information obtained from said symbolic analysis as feedback to identify a target of said virtual method call; and

iterating said symbolic analysis on a modified version of said control flow graph that associates said target with said virtual method.

20. The method of claim 19 , wherein:

said information represents a type constraint on said method call that is revealed by said symbolic analysis;

said symbolic analysis comprises a backward analysis to determine a weakest precondition at an entry point of said software code based on a desired logical state at some program point of said software code;

said virtual method call is skipped by using a special form of symbolic formula that represent constraints on said virtual method call; and

said special type of symbolic formula containing one or more skolem constants that define said constraints using existential quantifiers.