×

Inferring complete initialization of arrays. (English) Zbl 1292.68104

Summary: We define an automaton-based abstract interpretation of a trace semantics which identifies loops that definitely initialize all elements of an array to values satisfying a given property, a useful piece of information for the static analysis of Java-like languages. This results in a completely automatic and efficient analysis, that does not use manual code annotations. We give a formal proof of correctness that considers aspects such as side-effects of method calls. We show how the identification of those loops can be lifted to global invariants about the contents of elements of fields of array type, that hold everywhere in the code where those elements are accessed. This makes our work more significant and useful for the static analysis of real programs. The implementation of our analysis inside the Julia analyzer is both efficient and precise.

MSC:

68Q55 Semantics in the theory of computing
68Q45 Formal languages and automata
PDFBibTeX XMLCite
Full Text: DOI

References:

[2] Aho, A. V.; Sethi, R.; Ullman, J. D., Compilers: Principles, Techniques and Tools (1986), Addison-Wesley
[3] Beyer, Dirk; Henzinger, Thomas A.; Majumdar, Rupak; Rybalchenko, Andrey, Path Invariants, (Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation. Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation, PLDI 2007 (2007), ACM), 300-309
[4] Blanchet, B.; Cousot, P.; Cousot, R.; Feret, J.; Mauborgne, L.; Miné, L.; Monniaux, D.; Rival, X., Design and implementation of a special-purpose static program analyzer for safety-critical real-time embedded software, invited chapter, (The Essence of Computation: Complexity, Analysis, Transformation. Essays Dedicated to Neil D. Jones. The Essence of Computation: Complexity, Analysis, Transformation. Essays Dedicated to Neil D. Jones, Lecture Notes in Computer Science, vol. 2566 (2002), Springer), 85-108 · Zbl 1026.68514
[6] Cousot, P.; Cousot, R., Systematic design of program analysis frameworks, (Proceedings of the 6th Symposium on Principles of Programming Languages. Proceedings of the 6th Symposium on Principles of Programming Languages, POPL 1979 (1979), ACM), 269-282
[7] Cousot, P.; Cousot, R., Systematic design of program transformation frameworks by abstract interpretation, (Proceedings of the 29th Symposium on Principles of Programming Languages. Proceedings of the 29th Symposium on Principles of Programming Languages, POPL 2002 (2002), ACM), 178-190 · Zbl 1323.68356
[8] Cousot, Patrick; Cousot, Radhia; Logozzo, Francesco, A parametric segmentation functor for fully automatic and scalable array content analysis, (Proceedings of the 38th Symposium on Principles of Programming Languages. Proceedings of the 38th Symposium on Principles of Programming Languages, POPL 2011 (2011), ACM: ACM New York, NY, USA), 105-118 · Zbl 1284.68210
[9] Flanagan, C.; Qadeer, S., Predicate abstraction for software verification, (Proceedings of the 29th Symposium on Principles of Programming Languages. Proceedings of the 29th Symposium on Principles of Programming Languages, POPL 2002 (2002), ACM), 191-202 · Zbl 1323.68371
[10] Gopan, Denis; Reps, Thomas; Sagiv, Mooly, A framework for numeric analysis of array operations, (Proceedings of the 32nd annual ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages. Proceedings of the 32nd annual ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages, POPL 2005 (2005), ACM: ACM New York, NY, USA), 338-350 · Zbl 1369.68138
[11] Graf, S.; Saïdi, H., Construction of Abstract State Graphs with PVS, (Proceedings of the 9th International Conference on Computer Aided Verification. Proceedings of the 9th International Conference on Computer Aided Verification, CAV 1997. Proceedings of the 9th International Conference on Computer Aided Verification. Proceedings of the 9th International Conference on Computer Aided Verification, CAV 1997, Lecture Notes in Computer Science, vol. 1254 (1997), Springer), 72-83
[12] Habermehl, Peter; Iosif, Radu; Vojnar, Tomás, What else is decidable about integer arrays?, (Proceedings of the 11th International Conference on Foundations of Software Science and Computational Structures. Proceedings of the 11th International Conference on Foundations of Software Science and Computational Structures, FOSSACS 2008. Proceedings of the 11th International Conference on Foundations of Software Science and Computational Structures. Proceedings of the 11th International Conference on Foundations of Software Science and Computational Structures, FOSSACS 2008, Lecture Notes in Computer Science, vol. 4962 (2008), Springer: Springer Budapest, Hungary), 474-489 · Zbl 1139.03007
[13] Halbwachs, Nicolas; Péron, Mathias, Discovering properties about arrays in simple programs, (Proceedings of the 2008 ACM SIGPLAN conference on Programming Language Design and Implementation. Proceedings of the 2008 ACM SIGPLAN conference on Programming Language Design and Implementation, PLDI 2008 (2008), ACM: ACM New York, NY, USA), 339-348
[14] Hoder, Krystof; Kovács, Laura; Voronkov, Andree, Case studies on invariant generation using a saturation theorem prover, (Proceedings of the 10th Mexican International Conference on Artificial Intelligence. Proceedings of the 10th Mexican International Conference on Artificial Intelligence, MICAI 2011. Proceedings of the 10th Mexican International Conference on Artificial Intelligence. Proceedings of the 10th Mexican International Conference on Artificial Intelligence, MICAI 2011, Lecture Notes in Computer Science, vol. 7094 (2011), Springer), 1-15
[15] Kovács, Laura; Voronkov, Andrei, Finding loop invariants for programs over arrays using a theorem prover, (Proceedings of the 12th International Conference on Fundamental Approaches to Software Engineering. Proceedings of the 12th International Conference on Fundamental Approaches to Software Engineering, FASE 2009. Proceedings of the 12th International Conference on Fundamental Approaches to Software Engineering. Proceedings of the 12th International Conference on Fundamental Approaches to Software Engineering, FASE 2009, Lecture Notes in Computer Science, vol. 5503 (2009), Springer), 470-485
[18] Nikolić, Đurica; Spoto, Fausto, Automaton-based array initialization analysis, (Proceedings of the 6th International Conference on Language and Automata Theory and Application, vol. 7183. Proceedings of the 6th International Conference on Language and Automata Theory and Application, vol. 7183, LATA 2012 (2012), Springer), 420-432 · Zbl 1350.68180
[19] Nikolić, Đurica; Spoto, Fausto, Definite expression aliasing analysis for java bytecode, (Proceedings of the 9th International Colloquium on Theoretical Aspects of Computing. Proceedings of the 9th International Colloquium on Theoretical Aspects of Computing, ICTAC 2012. Proceedings of the 9th International Colloquium on Theoretical Aspects of Computing. Proceedings of the 9th International Colloquium on Theoretical Aspects of Computing, ICTAC 2012, Lecture Notes in Computer Science, vol. 7521 (2012), Springer), 74-89 · Zbl 1362.68031
[20] Nikolić, Đurica; Spoto, Fausto, Reachability analysis of program variables, (Proceedings of the 6th International Joint Conference on Automated Reasoning. Proceedings of the 6th International Joint Conference on Automated Reasoning, IJCAR 2012. Proceedings of the 6th International Joint Conference on Automated Reasoning. Proceedings of the 6th International Joint Conference on Automated Reasoning, IJCAR 2012, Lecture Notes in Artificial Intelligence, vol. 7364 (2012), Springer), 423-438 · Zbl 1358.68075
[21] Palsberg, J.; Schwartzbach, M. I., Object-oriented type inference, (Proceedings of Object-Oriented Programming, Systems, Languages & Applications. Proceedings of Object-Oriented Programming, Systems, Languages & Applications, OOPSLA 1991. Proceedings of Object-Oriented Programming, Systems, Languages & Applications. Proceedings of Object-Oriented Programming, Systems, Languages & Applications, OOPSLA 1991, ACM SIGPLAN Notices, vol. 26(11) (1991), ACM), 146-161
[22] Payet, É.; Spoto, F., Static analysis of android programs, Information & Software Technology, 54, 11, 1192-1201 (2012)
[23] Secci, Stefano; Spoto, Fausto, Pair-sharing analysis of object-oriented programs, (Proceedings of the 12th International Static Analysis Symposium. Proceedings of the 12th International Static Analysis Symposium, SAS 2005. Proceedings of the 12th International Static Analysis Symposium. Proceedings of the 12th International Static Analysis Symposium, SAS 2005, Lecture Notes in Computer Science, vol. 3672 (2005), Springer), 320-335 · Zbl 1141.68378
[24] Spoto, F., Precise null-pointer analysis, Software and Systems Modeling, 10, 2, 219-252 (2011)
[25] Spoto, Fausto, The nullness analyser of Julia, (Proceedings of the 16th International Conference on Logic for Programming, Artificial Intelligence and Reasoning — LPAR (Dakar). Proceedings of the 16th International Conference on Logic for Programming, Artificial Intelligence and Reasoning — LPAR (Dakar), Lecture Notes in Computer Science, vol. 6355 (2010), Springer), 405-424
[26] Spoto, Fausto; Jensen, Thomas P., Class analyses as abstract interpretations of trace semantics, ACM Transactions on Programming Languages and Systems, 25, 5, 578-630 (2003)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.