Using dynamic analysis to improve model checking

• US 7,962,901 B2
• Filed: 04/17/2006
• Issued: 06/14/2011
• Est. Priority Date: 04/17/2006
• Status: Expired due to Fees

• Current Assignee: Microsoft Technology Licensing LLC (Microsoft Corporation)
• Original Assignee: Microsoft Corporation
• Inventors: McCamant, Stephen, Chilimbi, Trishul
• Primary Examiner(s): Puente; Emerson C
• Assistant Examiner(s): MILLS, PAUL V
• Application Number:
  US11/406,207
• Publication Number:
  US 20070244942A1
• Time in Patent Office: 1,884 Days
• Field of Search: None
• US Class Current: 717/131
• CPC Class Codes: G06F 11/3612 by runtime analysis performance monitoring G06F11/3466

Abstract

Model checking has been used to verify program behavior. However, exploration of the model is often impractical for many general purpose programs due to the complexity of an exploding state space. Instead, a program is instrumented with code that records pointer dereference information. The instrumented program is executed thereby recording pointer dereference frequency information. Then, a model of the program is explored using the pointer dereference frequency information to direct state space exploration of the model.

Claims

1. A computerized method comprising:

instrumenting a program under test with code that records pointer dereference information;

executing the instrumented program comprising recording pointer dereference frequency information;

generating a Boolean program from the program under test; and

exploring a model based at least on the Boolean program comprising using the pointer dereference frequency information and a points-to graph to direct state space exploration of the model for locating one or more bugs in the program under test;

wherein exploring the model of the program further comprises exploring the model in an iteration that limits the points-to graph to at least one highest frequency memory location using the pointer dereference frequency information, then again exploring the model in one or more subsequent iterations until memory locations with corresponding pointer dereference frequency information are explored or until at least a bug is reported, wherein a subsequent iteration explores the model directed in part by limiting the points-to graph to a combination of at least one lower dereference frequency memory location and higher frequency memory locations of a preceding iteration.

2. The method of claim 1 further comprising storing the recorded pointer dereference frequency information in a two level data structure wherein a first level of the data structure indexes the high order bits of the memory location and the second level of the data structure indexes the low order bits of the memory location.

3. The method of claim 1 wherein the model is explored using the pointer dereference frequency information upon a failure of exploring the model using static pointer analysis information.

4. The method of claim 1 wherein the state space exploration of the model locates a bug in the program.

5. The method of claim 1 wherein the pointer dereference frequency information is recorded in a data structure indexed by memory locations, and each pointer dereference provides a unique mapping from a numeric value of a pointer to an object it refers to.

6. The method of claim 1 wherein the code that records pointer dereference frequency information instruments pointers at locations where they are dereferenced for writing.

7. The method of claim 6 wherein the locations where pointers are dereferenced for writing are those binary instructions that load or store via an indirect address.

8. The method of claim 1 wherein instrumenting the program under test with code that records pointer dereference frequency information comprises instrumenting separately for each dereference site.

9. The method of claim 8 wherein instrumenting separately for each dereference site includes logic for sampling at a rate that decreases geometrically.

10. The method of claim 1 exploring the model comprising exploring the model iteratively from highest to lowest pointer dereference frequency.

11. The method of claim 10 wherein after the pointer dereference frequency information is explored, exploring the model further comprises exploring a static points-to set.

12. The method of claim 1 wherein recording pointer dereference frequency information comprises writing memory dereference information to a trace file and automatically evaluating the trace file to identify and count pointer dereferences.

13. The method of claim 1 wherein recording pointer dereference frequency information comprises counting memory locations dereferenced by a pointer as the instrumented program executes.

14. The method of claim 1 wherein instrumenting the program under test with code comprises adding calls to a dynamic linked library and recording pointer dereference frequency information comprises executing identifying and counting logic in the dynamic linked library.

15. The method of claim 1 wherein recording pointer dereference frequency information comprises:

on a first dereference, a pointer identifier is added to a data structure; and

on a subsequent dereference of the pointer identifier, the subsequent dereference is counted.

16. A computer system comprising:

a digital processor; and

digital memory comprising,

a program under test,

an abstractor generating a Boolean program using the program under test as input, and

a binary instrumentor instrumenting the program under test to provide pointer dereference frequency information, and

a model checker for exploring a model built based at least on the Boolean program using the pointer dereference frequency information and a points-to graph to focus a state space exploration for locating one or more bugs in the program under test, wherein the exploring the model comprises focusing the exploration of the model in an iteration that limits the points-to graph to at least one highest frequency memory location using the pointer dereference frequency information, then again exploring the model in one or more subsequent iterations until memory locations with corresponding pointer dereference frequency information are explored or until at least a bug is reported, wherein a subsequent iteration explores the model directed in part by limiting the points-to graph using a combination of at least one lower frequency memory location and higher frequency memory locations of a preceding iteration.

17. A computer-readable storage medium having computer-executable instructions that when executed cause a computer to perform a method, the method comprising:

instrumenting a program under test with code that records pointer dereference information;

executing the instrumented program comprising recording pointer dereference frequency information;

generating a Boolean program from the program under test; and

exploring a model constructed based at least on the Boolean program comprising using the pointer dereference frequency information and a points-to graph to direct state space exploration of the model in order to locate one or more bugs in the program under test;

wherein exploring the model of the program further comprises exploring the model in a first iteration that limits the points-to graph to at least one highest frequency memory location using the pointer dereference frequency information, then again exploring the model in one or more subsequent iterations until memory locations with corresponding pointer dereference frequency information are explored or until at least one bug is reported, wherein a subsequent iteration limits the points-to graph to a combination of at least one lower frequency memory location and higher frequency memory locations of a preceding iteration.

18. The computer-readable storage medium of claim 17 wherein the computer-executable instructions further comprise instructions for instrumenting separately for each dereference site.