On Modular Pluggable Analyses Using Set Interfaces

paper ps   
We present a technique that enables the focused application of multiple analyses to different modules in the same program. Our research has two goals: 1) to address the scalability limitations of precise analyses by focusing the analysis on only those parts of the program that are relevant to the properties that the analysis is designed to verify, and 2) to enable the application of specialized analyses that verify properties of specific classes of data structures to programs that simultaneously manipulate several different kinds of data structures. In our approach, each module encapsulates a data structure and uses membership in abstract sets to characterize how objects participate in its data structure. Each analysis verifies that the implementation of the module 1) preserves important internal data structure representation invariants and 2) conforms to a specification that uses formulas in a set algebra to characterize the effects of operations on the data structure. The analyses use the common set abstraction to 1) characterize how objects participate in multiple data structures and to 2) enable the inter-analysis communication required to verify properties that depend on multiple modules analyzed by different analyses. We characterize the key soundness property that an analysis plugin must satisfy to successfully participate in our system and present several analysis plugins that satisfy this property: a flag plugin that analyzes modules in which abstract set membership is determined by a flag field in each object, and a graph types plugin that analyzes modules in which abstract set membership is determined by reachability properties of objects stored in tree-like data structures.

Citation

Patrick Lam, Viktor Kuncak, and Martin Rinard. On modular pluggable analyses using set interfaces. Technical Report 933, MIT CSAIL, December 2003.

BibTex Entry

@techreport{LamETAL03OnModularPluggableAnalysesUsingSetInterfaces,
  author = {Patrick Lam and Viktor Kuncak and Martin Rinard},
  title = {On Modular Pluggable Analyses Using Set Interfaces},
  institution = {MIT CSAIL},
  month = {December},
  number = {933},
  year = 2003,
  abstract = {
We present a technique that enables the focused application
of multiple analyses to different modules in the same
program.  Our research has two goals: 1) to address the
scalability limitations of precise analyses by focusing the
analysis on only those parts of the program that are
relevant to the properties that the analysis is designed to
verify, and 2) to enable the application of specialized
analyses that verify properties of specific classes of data
structures to programs that simultaneously manipulate
several different kinds of data structures.

In our approach, each module encapsulates a data structure
and uses membership in abstract sets to characterize how
objects participate in its data structure.  Each analysis
verifies that the implementation of the module 1) preserves
important internal data structure representation invariants
and 2) conforms to a specification that uses formulas in a
set algebra to characterize the effects of operations on the
data structure. The analyses use the common set abstraction
to 1) characterize how objects participate in multiple data
structures and to 2) enable the inter-analysis communication
required to verify properties that depend on multiple
modules analyzed by different analyses.

We characterize the key soundness property that an analysis
plugin must satisfy to successfully participate in our
system and present several analysis plugins that satisfy
this property: a flag plugin that analyzes modules in which
abstract set membership is determined by a flag field in
each object, and a graph types plugin that analyzes modules
in which abstract set membership is determined by
reachability properties of objects stored in tree-like data
structures.
}
}