Sophisticated software systems are inherently complex. Understanding, debugging
and maintaining such systems requires inferring high-level characteristics of the
system's behavior from a myriad of low-level details. For large systems, this quickly
becomes an extremely difficult task.
MrSpidey is a static debugger that augments the programmers ability to deal
with such complex systems. It statically analyzes the program and uses the results
of the analysis to identify and highlight any program operation may cause a run-time
fault. The programmer can then investigate each potential fault site and, using the
graphical explanation facilities of MrSpidey, determine if the fault will really happen
or whether the corresponding correctness proof is beyond the analysis's capabilities.
In practice, MrSpidey has proven to be an effective tool for debugging program under
development and understanding existing programs.
The key technology underlying MrSpidey is componential set-based analysis. This
is 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 data
flow behavior of that component. The analysis then combines and solves these simplified
constraint systems to yield invariants characterizing the run-time behavior of
the entire program. This component-wise approach yields an analysis that handles
significantly 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, or
solution space, of a constraint system. This dissertation provides a complete proof-theoretic
and algorithmic characterization of the observable behavior of constraint
systems, and establishes a close connection between the observable equivalence of
constraint systems and the equivalence of regular tree grammars. We exploit this
connection to develop a complete algorithm for deciding the observable equivalence
of constraint systems, and to adapt a variety of algorithms for simplifying regular
tree grammars to the problem of simplifying constraint systems. The resulting constraint
simplification algorithms yield an order of magnitude reduction in the size of
constraint systems for typical program expressions.
| Identifer | oai:union.ndltd.org:RICE/oai:scholarship.rice.edu:1911/20475 |
| Date | January 1997 |
| Source Sets | Rice University |
| Language | English |
| Detected Language | English |
| Type | Thesis, Text |
| Format | application/pdf |
Page generated in 0.0021 seconds