Effective Static Debugging via Compential Set-Based Analysis

[摘要] Sophisticated software systems are inherently complex. Understanding, debuggingand maintaining such systems requires inferring high-level characteristics of thesystem's behavior from a myriad of low-level details. For large systems, this quicklybecomes an extremely difficult task.MrSpidey is a static debugger that augments the programmers ability to dealwith such complex systems. It statically analyzes the program and uses the resultsof the analysis to identify and highlight any program operation may cause a run-timefault. The programmer can then investigate each potential fault site and, using thegraphical explanation facilities of MrSpidey, determine if the fault will really happenor whether the corresponding correctness proof is beyond the analysis's capabilities.In practice, MrSpidey has proven to be an effective tool for debugging program underdevelopment and understanding existing programs.The key technology underlying MrSpidey is componential set-based analysis. Thisis a constraint-based, whole-program analysis for object-oriented and functional programs.The analysis first processes each program component (eg. module or package)independently, generating and simplifying a constraint system describing the dataflow behavior of that component. The analysis then combines and solves these simplifiedconstraint systems to yield invariants characterizing the run-time behavior ofthe entire program. This component-wise approach yields an analysis that handlessignificantly larger programs than previous analyses of comparable accuracy.The simplification of constraint systems raises a number of questions. In particular,we need to ensure that simplification preserves the observable behavior, orsolution space, of a constraint system. This dissertation provides a complete proof-theoreticand algorithmic characterization of the observable behavior of constraintsystems, and establishes a close connection between the observable equivalence ofconstraint systems and the equivalence of regular tree grammars. We exploit thisconnection to develop a complete algorithm for deciding the observable equivalenceof constraint systems, and to adapt a variety of algorithms for simplifying regulartree grammars to the problem of simplifying constraint systems. The resulting constraintsimplification algorithms yield an order of magnitude reduction in the size ofconstraint systems for typical program expressions.

[发布机构] Rice University

[效力级别] software