Abstract
Modern languages are equipped with static type checking/inference that helps programmers to keep a clean programming style and to reduce errors. However, the ever-growing size of programs and their continuous evolution require building fast and efficient analysers. A promising solution is incrementality, aiming at only re-typing the diffs, i.e. those parts of the program that change or are inserted, rather than the entire codebase. We propose an algorithmic schema that drives an incremental usage of existing, standard typing algorithms with no changes. Ours is a grey-box approach: just the shape of the input, that of the results and some domain-specific knowledge are needed to instantiate our schema. Here, we present the foundations of our approach and the conditions for its correctness. We show it at work to derive two different incremental typing algorithms. The first type checks an imperative language to detect information flow and non-interference, and the second infers types for a functional language. We assessed our proposal on a prototypical implementation of an incremental type checker. Our experiments show that using the type checker incrementally is (almost) always rewarding.
The first two authors have been partially supported by U. Pisa project PRA_2018_66 DECLware: Declarative methodologies for designing and deploying applications. The last author is supported by IMT project PAI VeriOSS.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
Available at https://github.com/mcaos/incremental-mincaml.
- 2.
Instead with the axiom \(\varGamma '[x \mapsto \tau ] \vdash _\mathcal {A} x : \tau \) one has \(\mathbb {I}_x = \emptyset \) and the same \( checkJoin _x\), where \(\varGamma = \varGamma '[x \mapsto \tau ]\).
- 3.
Available at https://github.com/mcaos/incremental-mincaml.
- 4.
Available at https://github.com/Chris00/ocaml-benchmark.
- 5.
As measured by the Landmarks library https://github.com/LexiFi/landmarks.
References
Aditya, S., Nikhil, R.S.: Incremental polymorphism. In: Hughes, J. (ed.) FPCA 1991. LNCS, vol. 523, pp. 379–405. Springer, Heidelberg (1991). https://doi.org/10.1007/3540543961_19
Blackshear, S., Di Stefano, D., Luca, M., O’Hearn, P., Villard, J.: Finding inter-procedural bugs at scale with infer static analyzer, September 2017. https://code.facebook.com/posts/1537144479682247/finding-inter-procedural-bugs-at-scale-with-infer-static-analyzer/
Busi, M., Degano, P., Galletta, L.: Using standard typing algorithms incrementally. Extended Version http://arxiv.org/abs/1808.00225
Calcagno, C., et al.: Moving fast with software verification. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 3–11. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-17524-9_1
Erdweg, S., Bracevac, O., Kuci, E., Krebs, M., Mezini, M.: A co-contextual formulation of type rules and its application to incremental type checking. In: Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, pp. 880–897 (2015)
Facebook: Pyre - a performant type-checker for Python 3. https://pyre-check.org/
Harman, M., O’Hearn, P.: From start-ups to scale-ups: opportunities and open problems for static and dynamic program analysis. In: IEEE International Working Conference on Source Code Analysis and Manipulation (2018)
Infer, F.: Infer static analyzer. http://fbinfer.com/
Johnson, G.F., Walz, J.A.: A maximum-flow approach to anomaly isolation in unification-based incremental type inference. In: Proceedings of the 13th Symposium on Principles of Programming Languages, pp. 44–57. ACM (1986)
Lauterburg, S., Sobeih, A., Marinov, D., Viswanathan, M.: Incremental state-space exploration for programs with dynamically allocated data. In: 30th International Conference on Software Engineering, ICSE 2008, pp. 291–300 (2008)
Leino, K.R.M., Wüstholz, V.: Fine-grained caching of verification results. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 380–397. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21690-4_22
McPeak, S., Gros, C., Ramanathan, M.K.: Scalable and incremental software bug detection. In: Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, ESEC/FSE 2013, pp. 554–564 (2013)
Meertens, L.G.L.T.: Incremental polymorphic type checking in B. In: Wright, J.R., Landweber, L., Demers, A.J., Teitelbaum, T. (eds.) Proceedings of the 10th ACM Symposium on Principles of Programming Languages, pp. 265–275. ACM (1983)
Miao, W., Siek, J.G.: Incremental type-checking for type-reflective metaprograms. In: Visser, E., Järvi, J. (eds.) Proceedings of the Ninth International Conference on Generative Programming and Component Engineering, pp. 167–176. ACM (2010)
Mudduluru, R., Ramanathan, M.K.: Efficient incremental static analysis using path abstraction. In: Gnesi, S., Rensink, A. (eds.) FASE 2014. LNCS, vol. 8411, pp. 125–139. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54804-8_9
Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer, Heidelberg (1999). https://doi.org/10.1007/978-3-662-03811-6
Qiu, R., Yang, G., Pasareanu, C.S., Khurshid, S.: Compositional symbolic execution with memoized replay. In: 37th IEEE/ACM International Conference on Software Engineering, ICSE 2015, vol. 1, pp. 632–642 (2015)
Ryder, B.G., Paull, M.C.: Incremental data-flow analysis. ACM Trans. Program. Lang. Syst. 10(1), 1–50 (1988)
Smith, G.: Principles of secure information flow analysis. In: Christodorescu, M., Jha, S., Maughan, D., Song, D., Wang, C. (eds.) Malware Detection, vol. 27, pp. 291–307. Springer, Boston (2007). https://doi.org/10.1007/978-0-387-44599-1_13
Sumii, E.: MinCaml: a simple and efficient compiler for a minimal functional language. In: Findler, R.B., Hanus, M., Thompson, S. (eds.) Proceedings of the 2005 Workshop on Functional and Declarative Programming in Education, pp. 27–38. ACM (2005)
Szabó, T., Erdweg, S., Voelter, M.: IncA: a DSL for the definition of incremental program analyses. In: Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering, pp. 320–331 (2016)
Volpano, D.M., Irvine, C.E., Smith, G.: A sound type system for secure flow analysis. J. Comput. Secur. 4(2/3), 167–188 (1996)
Wachsmuth, G.H., Konat, G.D.P., Vergu, V.A., Groenewegen, D.M., Visser, E.: A language independent task engine for incremental name and type analysis. In: Erwig, M., Paige, R.F., Van Wyk, E. (eds.) SLE 2013. LNCS, vol. 8225, pp. 260–280. Springer, Cham (2013). https://doi.org/10.1007/978-3-319-02654-1_15
Yang, G., Dwyer, M.B., Rothermel, G.: Regression model checking. In: 25th IEEE International Conference on Software Maintenance, ICSM 2009, pp. 115–124 (2009)
Yang, G., Person, S., Rungta, N., Khurshid, S.: Directed incremental symbolic execution. ACM Trans. Softw. Eng. Methodol. 24(1), 3:1–3:42 (2014)
Yur, J., Ryder, B.G., Landi, W.: An incremental flow- and context-sensitive pointer aliasing analysis. In: Proceedings of the 1999 International Conference on Software Engineering, pp. 442–451 (1999)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
Busi, M., Degano, P., Galletta, L. (2019). Using Standard Typing Algorithms Incrementally. In: Badger, J., Rozier, K. (eds) NASA Formal Methods. NFM 2019. Lecture Notes in Computer Science(), vol 11460. Springer, Cham. https://doi.org/10.1007/978-3-030-20652-9_7
Download citation
DOI: https://doi.org/10.1007/978-3-030-20652-9_7
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-20651-2
Online ISBN: 978-3-030-20652-9
eBook Packages: Computer ScienceComputer Science (R0)