Resolving and applying constraint queries on context-sensitive analyses

ABSTRACT

A context-sensitive analysis is an analysis in which program elements are assigned sets of properties that depend upon the context in which they occur. For analyses on imperative languages, this often refers to considering the behavior of statements in a called procedure with respect to the call-stack that generated the procedure invocation. Algorithms for performing or approximating these types of analyses make up the core of interprocedural program analysis and are pervasive; having applications in program comprehension, optimization, and verification. However, for many of these applications what is of interest is the solution to the dual problem: given a vertex and a desirable set of properties, what is the set of potential stack-contexts leading to that vertex that results in the desirable property set? Many techniques, such as procedure cloning, have been developed to approximately partition the set of stack-contexts leading to a vertex according to such a condition. This paper introduces a broad generalization of this problem referred to as a constraint query on the analysis. This generalization allows sophisticated constraints to be placed on both the desirable property set as well as the set of interesting stack-contexts. From these constraints, a novel technique based on manipulating regular languages is introduced that efficiently produces a concise representation of the exact set of stack-contexts solving this dual problem subject to the constraints. This technique is applied to a pair of emerging software engineering challenges - resolving program comprehension queries over aggregate collections of properties and statically modifying code to enforce a safety policy decidable by the analysis. Practical examples of both applications are presented along with empirical results.

REFERENCES

• 1: Joshua E. Barnes, A modified tree code: don't laugh; it runs, Journal of Computational Physics, v.87 n.1, p.161-170, March 1990 [doi>10.1016/0021-9991(90)90232-P]
• 2: Mary Wolcott Hall, Managing interprocedural optimization, Rice University, Houston, TX, 1992
• 3: T. W. Reps, S. Schwoon, and S. Jha. Weighted pushdown systems and their application to interprocedural dataflow analysis. In 10th International Symposium on Static Analysis, pages 189---213, June 2003.
• 4: Fred B. Schneider, Enforceable security policies, ACM Transactions on Information and System Security (TISSEC), v.3 n.1, p.30-50, Feb. 2000 [doi>10.1145/353323.353382]
• 5: U. Shankar, K. Talwar, J. S. Foster, and D. Wagner. Detecting format string vulnerabilities with type qualifiers. In 10th USENIX Security Symposium, pages 201--220, 2001.
• 6: M. Sharir and A. Pnueli. Two approaches to interprocedural data flow analysis. In S. Muchnick and N. Jones, editors, Program Flow Analysis: Theory and Applications, chapter 7, pages 189--233. Prentice-Hall, 1981.
• 7: William E. Weihl, Interprocedural data flow analysis in the presence of pointers, procedure variables, and label variables, Proceedings of the 7th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.83-94, January 28-30, 1980, Las Vegas, Nevada [doi>10.1145/567446.567455]

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Program analysis

General Terms:
Languages, Theory

Keywords:
context-sensitive analysis, static analysis