Kirsten L. Solberg Gasser
Abstract
We present a methodology for the systematic realisation of control flow analyses and illustrate it for Concurrent ML. We start with an abstract specification of the analysis that is next proved semantically sound with respect to a traditional small-step operational semantics; this result holds for terminating w well as non-terminating programs. The analysis is defined coinductively and it is shown that all programs have a least analysis result (that is indeed the best one). To realise the analysis we massage the specification in three stages: (i) to explicitly record reachability of subexpressions, (ii) to be defined in a syntax-directed manner, and (iii) to generate a set of constraints that subsequently can be solved by standard techniques. We prove equivalence results between the different versions of the analysis; in particular it follows that the least solution to the constraints generated will be the least analysis result also to the initial specification.
- 1 J.M. Ashley. A practical and flexible flow analysis for higher-order languages. In Proc. 23th POPL, pages 184-195. ACM Press, 1996. Google Scholar
Digital Library
- 2 P. Cousot and R. Cousot. Abstract Interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proc. jth POPL, pages 238-252. ACM Press, 1977. Google Scholar
- 3 P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In Proc. 6th POPL, pages 269- 282. ACM Press, 1979. Google ScholarDigital Library
- 4 P. Cousot and R. Cousot. Formal language, grammar and set-constraint-based program analysis by abstract interpretation. In Proc. FPCA '95, pages 170-181. ACM Press, 1995. Google ScholarDigital Library
- 5 K.-F. Fax~n. Optimizing lazy functional programs using flow inference. In Proc. SAS '95, pages 136-153. SLNCS 983, 1995. Google ScholarDigital Library
- 6 C. Flanagan and M. Felleisen. The semantics of Future and its use in program optimization. In Proc. POPL. ACM Press, 1995. Google ScholarDigital Library
- 7 N. Heintze. Set-based analysis of ML programs. In Proc. Lisp and Functional Programming. ACM Press, 1994. Google ScholarDigital Library
- 8 S. Jagannathan and S. Weeks. Analysing stores and references in a parallel symbolic language. In Proc. Lisp and Functional Programming. ACM Press, 1994. Google ScholarDigital Library
- 9 S. Jagannathan and S. Weeks. A unified treatment of flow analysis in higher-order languages. In Proc. POPL '95. ACM Press, 1995. Google ScholarDigital Library
- 10 S. Jagannathan and A. Wright. Effective flow analysis for avoiding run-time checks. In Proc. SAS '95, pages 207-224. SLNCS 983, 1995. Google ScholarDigital Library
- 11 N.D. Jones and F. Nielson. Abstract Interpretation: a semantics-based tool for program analysis. In Handbook of Logic in Computer Science vol. 4. Oxford University Press, 1995. Google ScholarDigital Library
- 12 R. Milner, M. Tofte and R. Harper. The Definition of Standard ML. The MIT Press, Cambridge, Mass, 1990. Google ScholarDigital Library
- 13 F. Nielson and H.R. Nielson. Infmitary Control Flow Analysis: a Collecting Semantics for Closure Analysis. Proc. POPL, pages 332-345, 1997. Google ScholarDigital Library
- 14 H.R. Nielson and F. Nielson. Higher-order concurrent programs with finite communication topology. In Proc. POPL '9~, pages 84-97. ACM Press, 1994. Google Scholar
- 15 J. Palsberg. Closure analysis in constraint form. ACM TOPLAS, 17 (1):47-62, 1995. Google ScholarDigital Library
- 16 G.D. Plotkin. A structural approach to operational semantics. Technical Report FN-19, DAIMI, Aarhus University, Denmark, 1981.Google Scholar
- 17 J.H. Reppy. Concurrent ML: Design, application and semantics. In Proc. Functional programming, Concurrency, Simulation and Automated Reasoning, pages 165-198. SLNCS 693, 1993. Google ScholarDigital Library
- 18 P. Sestoft. Analysis and efficient implementation of functional programs. Ph.D.-thesis, Department of Computer Science, University of Copenhagen, Denmark, 1991.Google Scholar
- 19 O. Shivers. Control flow analysis in Scheme. In Proc. PLDI'88, pages 164-174. ACM Sigplan Notices 7 (1), 1988. Google ScholarDigital Library
- 20 O. Shivers. The semantics of Scheme control-flow analysis. In Partial Evaluation and Semantics-Based Program Manipulation. ACM SIGPLAN Notices 26 (9), 1991. Google ScholarDigital Library
- 21 M. Wand and P. Steckler. Selective and lightweight closure conversion. In Proc. POPL '9~, pages 435-445. ACM Press, 1994. Google Scholar
Index Terms
- Systematic realisation of control flow analyses for CML
Recommendations
Systematic realisation of control flow analyses for CML
ICFP '97: Proceedings of the second ACM SIGPLAN international conference on Functional programmingWe present a methodology for the systematic realisation of control flow analyses and illustrate it for Concurrent ML. We start with an abstract specification of the analysis that is next proved semantically sound with respect to a traditional small-step ...
Variance analyses from invariance analyses
POPL '07: Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languagesAn invariance assertion for a program location l is a statement that always holds at l during execution of the program. Program invariance analyses infer invariance assertions that can be useful when trying to prove safety properties. We use the term ...
Specifying Dynamic Analyses by Extending Language Semantics
Dynamic analysis is increasingly attracting attention for debugging, profiling, and program comprehension. Ten to twenty years ago, many dynamic analyses investigated only simple method execution traces. Today, in contrast, many sophisticated dynamic ...
Comments