The GENSAT Technology

Static analysis of programs is a fundamental technique used in a variety of language processing tasks--from compilation to migration and re-engineering tools. A language processor typically uses different kinds of static analyses to support its activities. Efficiency and reliability of static analysis are key issues in this context, along with the lead times for design, implementation and verification of static analysers. In the absence of good generative tools, experimentation with the use of static analysers is severely hampered by the complexity of developing a static analyser. This, in turn, affects the process of selecting the static analyses to include in a language processing tool.

GENSAT, a generator for static analysis and transformation (SAT) programs, overcomes the practical difficulties involved in selecting a set of static analyses to support the language processing activities. It provides a non-procedural declarative interface to specify the static analysis to be performed and the program transformations to be applied depending on its results.

GENSAT provides the following advantages

  1. Ease of specification.
  2. Reduced lead times.
  3. Use of a comprehensive generalized theory of data flow analysis (Based on the paper "A generalized theory of bit-vector data flow analysis", by U.P.Khedker and D.M.Dhamdhere, ACM Transactions on Programming Languages & Systems, 1994.) guarantees correctness of analyses.
  4. Code sharing across different static analyses to be performed.
  5. Efficiency of data flow analysis through an appropriate choice of the solution technology.
  6. Applicability to unidirectional and bi-directional data flows.
  7. Easy adaptibility to different intermediate representations of programs.