ABSTRACT
In previous work, we introduced scope graphs as a formalism for describing program binding structure and performing name resolution in an AST-independent way. In this paper, we show how to use scope graphs to build static semantic analyzers. We use constraints extracted from the AST to specify facts about binding, typing, and initialization. We treat name and type resolution as separate building blocks, but our approach can handle language constructs---such as record field access---for which binding and typing are mutually dependent. We also refine and extend our previous scope graph theory to address practical concerns including ambiguity checking and support for a wider range of scope relationships. We describe the details of constraint generation for a model language that illustrates many of the interesting static analysis issues associated with modules and records.
- F. Baader and T. Nipkow. Term rewriting and all that. Cambridge University Press, 1998. Google ScholarDigital Library
- J. A. Brzozowski. Derivatives of regular expressions. JACM, 11(4):481–494, 1964. Google ScholarDigital Library
- T. Ekman and G. Hedin. Modular name analysis for Java using JastAdd. In GTTSE, pages 422–436, 2006. Google ScholarDigital Library
- T. Ekman and G. Hedin. The JastAdd extensible Java compiler. In OOPSLA, pages 1–18, 2007. Google ScholarDigital Library
- S. Erdweg, O. Bracevac, E. Kuci, M. Krebs, and M. Mezini. A cocontextual formulation of type rules and its application to incremental type checking. In OOPSLA, pages 880–897, 2015. Google ScholarDigital Library
- S. Erdweg, T. van der Storm, M. Völter, L. Tratt, et al. Evaluating and comparing language workbenches: Existing results and benchmarks for the future. Computer Languages, Systems & Structures, 44:24–– 47, 2015. Google ScholarDigital Library
- G. Hedin. Reference attributed grammars. informaticaSI, 24(3), 2000.Google Scholar
- B. Heeren, J. Hage, and S. D. Swierstra. Scripting the type inference process. In ICFP, pages 3–13, 2003. Google ScholarDigital Library
- U. Kastens and W. M. Waite. An abstract data type for name analysis. ACTA, 28(6):539–558, 1991. Google ScholarDigital Library
- L. C. L. Kats and E. Visser. The Spoofax language workbench: rules for declarative specification of languages and IDEs. In OOPSLA, pages 444–463, 2010. Google ScholarDigital Library
- D. E. Knuth. Semantics of context-free languages. mst, 2(2):127–145, 1968.Google Scholar
- G. D. P. Konat, L. C. L. Kats, G. Wachsmuth, and E. Visser. Declarative name binding and scope rules. In SLE, pages 311–331, 2012.Google Scholar
- R. Milner. A theory of type polymorphism in programming. jcss, 17(3):348–375, 1978.Google Scholar
- P. Neron, A. P. Tolmach, E. Visser, and G. Wachsmuth. A theory of name resolution. In ESOP, pages 205–231, 2015.Google ScholarCross Ref
- J. Palsberg and M. I. Schwartzbach. Object-oriented type inference. In OOPSLA, pages 146–161, 1991. Google ScholarDigital Library
- J. Palsberg and M. I. Schwartzbach. Object-oriented type systems. Wiley professional computing. Wiley, 1994. Google ScholarDigital Library
- H. van Antwerpen, P. Neron, A. P. Tolmach, E. Visser, and G. Wachsmuth. A constraint language for static semantic analysis based on scope graphs with proofs. Technical Report TUD-SERG-2015-012, Software Engineering Research Group, Delft University of Technology, 2015. Available at http://swerl.tudelft.nl/twiki/pub/ Main/TechnicalReports/TUD-SERG-2015-012.pdf.Google Scholar
- E. Visser, G. Wachsmuth, A. P. Tolmach, P. Neron, V. A. Vergu, A. Passalaqua, and G. D. P. Konat. A language designer’s workbench: A one-stop-shop for implementation and verification of language designs. In OOPSLA, pages 95–111, 2014. Google ScholarDigital Library
- G. Wachsmuth, G. D. P. Konat, V. A. Vergu, D. M. Groenewegen, and E. Visser. A language independent task engine for incremental name and type analysis. In SLE, pages 260–280, 2013.Google ScholarCross Ref
- D. Zhang and A. C. Myers. Toward general diagnosis of static errors. In POPL, pages 569–582, 2014. Google ScholarDigital Library
- D. Zhang, A. C. Myers, D. Vytiniotis, and S. L. P. Jones. Diagnosing type errors with class. In PLDI, pages 12–21, 2015. Google ScholarDigital Library
Index Terms
- A constraint language for static semantic analysis based on scope graphs
Recommendations
A Language Designer's Workbench: A One-Stop-Shop for Implementation and Verification of Language Designs
Onward! 2014: Proceedings of the 2014 ACM International Symposium on New Ideas, New Paradigms, and Reflections on Programming & SoftwareThe realization of a language design requires multiple artifacts that redundantly encode the same information. This entails significant effort for language implementors, and often results in late detection of errors in language definitions. In this ...
The spoofax name binding language
SPLASH '12: Proceedings of the 3rd annual conference on Systems, programming, and applications: software for humanityIn textual software languages, names are used to identify program elements such as variables, methods, and classes. Name analysis algorithms resolve names in order to establish references between definitions and uses of names. In this poster, we present ...
Binders unbound
ICFP '11: Proceedings of the 16th ACM SIGPLAN international conference on Functional programmingImplementors of compilers, program refactorers, theorem provers, proof checkers, and other systems that manipulate syntax know that dealing with name binding is difficult to do well. Operations such as α-equivalence and capture-avoiding substitution ...
Comments