Static Value Analysis of Python Programs by Abstract Interpretation
| Autor: | Abdelraouf Ouadjaout, Aymeric Fromherz, Antoine Miné |
|---|---|
| Přispěvatelé: | Algorithmes, Programmes et Résolution (APR), LIP6, Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS), Carnegie Mellon University [Pittsburgh] (CMU) |
| Jazyk: | angličtina |
| Předmět: |
[INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL]
Programming language Computer science 020207 software engineering 02 engineering and technology Object system Static analysis Python (programming language) Abstract interpretation computer.software_genre [INFO.INFO-PF]Computer Science [cs]/Performance [cs.PF] Control flow Computer Science::Mathematical Software 0202 electrical engineering electronic engineering information engineering 020201 artificial intelligence & image processing computer computer.programming_language |
| Zdroj: | Lecture Notes in Computer Science Lecture Notes in Computer Science-NASA Formal Methods NASA Formal Methods NASA Formal Methods 10th International Symposium, NFM 2018, Newport News, VA, USA, April 17-19, 2018, Proceedings NFM 2018-10th International Symposium NASA Formal Methods NFM 2018-10th International Symposium NASA Formal Methods, Apr 2018, Newport News, VA, United States. pp.185-202, ⟨10.1007/978-3-319-77935-5_14⟩ Lecture Notes in Computer Science ISBN: 9783319779348 NFM |
| ISSN: | 0302-9743 1611-3349 |
| DOI: | 10.1007/978-3-319-77935-5_14 |
| Popis: | International audience; We propose a static analysis by abstract interpretation for a significant subset of Python to infer variable values, run-time errors, and uncaught exceptions. Python is a high-level language with dynamic typing, a class-based object system, complex control structures such as generators, and a large library of builtin objects. This makes static reasoning on Python programs challenging. The control flow is highly dependent on the type of values, which we thus infer accurately.As Python lacks a formal specification, we first present a concrete collecting semantics of reachable program states. We then propose a non-relational flow-sensitive type and value analysis based on simple abstract domains for each type, and handle non-local control such as exceptions through continuations. We show how to infer relational numeric invariants by leveraging the type information we gather. Finally, we propose a relational abstraction of generators to count the number of available elements and prove that no StopIteration exception is raised.Our prototype implementation is heavily in development; it does not support some Python features, such as recursion nor the compile builtin, and it handles only a small part of the builtin objects and standard library. Nevertheless, we are able to present preliminary experimental results on analyzing actual, if small, Python code from a benchmarking application and a regression test suite. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|