Advertisement

Galois Connections for Recursive Types

  • Ahmad Salim Al-SibahiEmail author
  • Thomas JensenEmail author
  • Rasmus Ejlers Møgelberg
  • Andrzej Wąsowski
Chapter
  • 46 Downloads
Part of the Lecture Notes in Computer Science book series (LNCS, volume 12065)

Abstract

Building a static analyser for a real language involves modeling of large domains capturing the many available data types. To scale domain design and support efficient development of project-specific analyzers, it is desirable to be able to build, extend, and change abstractions in a systematic and modular fashion. We present a framework for modular design of abstract domains for recursive types and higher-order functions, based on the theory of solving recursive domain equations. We show how to relate computable abstract domains to our framework, and illustrate the potential of the construction by modularizing a monolithic domain for regular tree grammars. A prototype implementation in the dependently typed functional language Agda shows how the theoretical solution can be used in practice to construct static analysers.

Supplementary material

References

  1. 1.
    Abbott, M.G., Altenkirch, T., Ghani, N.: Containers: constructing strictly positive types. Theoret. Comput. Sci. 342(1), 3–27 (2005)MathSciNetCrossRefGoogle Scholar
  2. 2.
    Abramsky, S., Jung, A.: Domain theory. In: Abramsky, S., Gabbay, D.M., Maibaum, T.S.E. (eds.) Handbook of Logic in Computer Science, vol. 3, pp. 1–168. Clarendon Press, Oxford (1994)Google Scholar
  3. 3.
    Aiken, A., Murphy, B.R.: Implementing regular tree expressions. In: Hughes, J. (ed.) FPCA 1991. LNCS, vol. 523, pp. 427–447. Springer, Heidelberg (1991).  https://doi.org/10.1007/3540543961_21CrossRefGoogle Scholar
  4. 4.
    Awodey, S.: Category Theory. Oxford University Press, Oxford (2011)zbMATHGoogle Scholar
  5. 5.
    Benton, P.N.: Strictness properties of lazy algebraic datatypes. In: Cousot, P., Falaschi, M., Filé, G., Rauzy, A. (eds.) WSA 1993. LNCS, vol. 724, pp. 206–217. Springer, Heidelberg (1993).  https://doi.org/10.1007/3-540-57264-3_42CrossRefGoogle Scholar
  6. 6.
    Bodin, M., Gardner, P., Jensen, T., Schmitt, A.: Skeletal semantics and their interpretations. PACMPL 3(POPL), 44:1–44:31 (2019)Google Scholar
  7. 7.
    Chang, B.E., Rival, X.: Relational inductive shape analysis. In: Necula, G.C., Wadler, P. (eds.) POPL 2008, pp. 247–260. ACM (2008)Google Scholar
  8. 8.
    Chang, B.-Y.E., Rival, X., Necula, G.C.: Shape analysis with structural invariant checkers. In: Nielson, H.R., Filé, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 384–401. Springer, Heidelberg (2007).  https://doi.org/10.1007/978-3-540-74061-2_24 CrossRefGoogle Scholar
  9. 9.
    Cousot, P.: The calculational design of a generic abstract interpreter. In: Broy, M., Steinbrüggen, R. (eds.) Calculational System Design. NATO ASI Series F. IOS Press, Amsterdam (1999)Google Scholar
  10. 10.
    Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Graham, R.M., Harrison, M.A., Sethi, R. (eds.) POPL 1977, pp. 238–252. ACM (1977)Google Scholar
  11. 11.
    Cousot, P., Cousot, R.: Invited talk: higher order abstract interpretation (and application to comportment analysis generalizing strictness, termination, projection, and PER analysis. In: Bal, H.E. (ed.) Proceedings of the IEEE Computer Society 1994 International Conference on Computer Languages, Toulouse, France, 16–19 May 1994, pp. 95–112. IEEE Computer Society (1994)Google Scholar
  12. 12.
    Cousot, P., Cousot, R.: Formal language, grammar and set-constraint-based program analysis by abstract interpretation. In: FPCA 1995, pp. 170–181. ACM (1995)Google Scholar
  13. 13.
    Cousot, P., Cousot, R.: Modular static program analysis. In: Horspool, R.N. (ed.) CC 2002. LNCS, vol. 2304, pp. 159–179. Springer, Heidelberg (2002).  https://doi.org/10.1007/3-540-45937-5_13CrossRefGoogle Scholar
  14. 14.
    Darais, D., Labich, N., Nguyen, P.C., Horn, D.V.: Abstracting definitional interpreters (functional pearl). PACMPL 1(ICFP), 12:1–12:25 (2017)Google Scholar
  15. 15.
    Jensen, T.P.: Disjunctive program analysis for algebraic data types. ACM Trans. Program. Lang. Syst. 19(5), 751–803 (1997)CrossRefGoogle Scholar
  16. 16.
    Journault, M., Miné, A., Ouadjaout, A.: Modular static analysis of string manipulations in C programs. In: Podelski, A. (ed.) SAS 2018. LNCS, vol. 11002, pp. 243–262. Springer, Cham (2018).  https://doi.org/10.1007/978-3-319-99725-4_16CrossRefGoogle Scholar
  17. 17.
    Keidel, S., Poulsen, C.B., Erdweg, S.: Compositional soundness proofs of abstract interpreters. PACMPL 2(ICFP), 72:1–72:26 (2018)Google Scholar
  18. 18.
    Midtgaard, J., Jensen, T.: A calculational approach to control-flow analysis by abstract interpretation. In: Alpuente, M., Vidal, G. (eds.) SAS 2008. LNCS, vol. 5079, pp. 347–362. Springer, Heidelberg (2008).  https://doi.org/10.1007/978-3-540-69166-2_23CrossRefzbMATHGoogle Scholar
  19. 19.
    Nielson, F., Nielson, H.R.: The tensor product in wadler’s analysis of lists. Sci. Comput. Program. 22(3), 327–354 (1994)MathSciNetCrossRefGoogle Scholar
  20. 20.
    Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer, Heidelberg (1999).  https://doi.org/10.1007/978-3-662-03811-6CrossRefzbMATHGoogle Scholar
  21. 21.
    Norell, U.: Dependently typed programming in agda. In: Koopman, P., Plasmeijer, R., Swierstra, D. (eds.) AFP 2008. LNCS, vol. 5832, pp. 230–266. Springer, Heidelberg (2009).  https://doi.org/10.1007/978-3-642-04652-0_5CrossRefzbMATHGoogle Scholar
  22. 22.
    Rival, X., Toubhans, A., Chang, B.-Y.E.: Construction of abstract domains for heterogeneous properties (position paper). In: Margaria, T., Steffen, B. (eds.) ISoLA 2014. LNCS, vol. 8803, pp. 489–492. Springer, Heidelberg (2014).  https://doi.org/10.1007/978-3-662-45231-8_40CrossRefGoogle Scholar
  23. 23.
    Streicher, T.: Domain-Theoretic Foundations of Functional Programming. World Scientific Publishing Company, Singapore (2006)CrossRefGoogle Scholar
  24. 24.
    Tarski, A.: A lattice-theoretical fixpoint theorem and its applications. Pac. J. Math. 5(2), 285–309 (1955)MathSciNetCrossRefGoogle Scholar
  25. 25.
    Toubhans, A., Chang, B.-Y.E., Rival, X.: Reduced product combination of abstract domains for shapes. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 375–395. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-35873-9_23CrossRefzbMATHGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2020

Authors and Affiliations

  1. 1.University of CopenhagenCopenhagenDenmark
  2. 2.PaperflowCopenhagenDenmark
  3. 3.INRIARennesFrance
  4. 4.IT University of CopenhagenCopenhagenDenmark

Personalised recommendations