AbstractThe concepts of value and control flow graphs are important for program analysis of imperative programs. An imperative value flow graph can be constructed by a single pass over the program text. No similar concepts exist for higher-order languages: we propose a method for constructing value flow graphs for typed higher-order functional languages. A higher-order value flow graph is constructed by a single pass over an explicitly typed program. By using standard methods, single-source and single-use value flow problems can be answered in linear time and all-sources-all-uses can be answered in quadratic time (in the size of the flow graph, which is equivalent to the size of the explicitly typed program). On simply typed programs, the precision of the resulting analysis is equivalent to closure analysis. In practice, it is a reasonable assumption that typed programs are only bigger than their untyped equivalent by a constant factor, hence this is an asymptotic improvement over previous algorithms.
We extend the analysis to handle polymorphism, sum types and recursive types. As a consequence, the analysis can handle (explicit) dynamically typed programs. The analysis is polyvariant for polymorphic definitions.
Categories and Subject Descriptors: D.3.4 [Programming Languages]: Processors; F.3.3 [Logics and Meanings of Programs]: Studies of Program Constructs; F.4.1 [Mathematical Logic and Formal Languages]: Mathematical Logic
Additional Key Words and Phrases: program analysis, type system, efficiency, polymorphism, recursive types, polyvariance
Selected references
- Fritz Henglein. Dynamic typing: syntax and proof theory. Science of Computer Programming, 22(3):197-230, June 1994.
- Thomas W. Reps, Susan Horwitz, and Mooly Sagiv. Precise interprocedural dataflow analysis via graph reachability. In Conference Record of POPL '95: 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 49-61, San Francisco, California, January 1995.