Static Analysis of Python Programs using Abstract Interpretation: An Application to Tensor Shape Analysis

Tensors, an extension of arrays, are widely used in a variety of programming tasks. Tensors are the building blocks of many modern machine learning frameworks and are fundamental in the definition of deep learning models. Linters are indispensable tools for today's developers, as they help the developers to check code before executing it. Despite the popularity of tensors, linters for Python that check and flag code with tensors are nonexistent. Given the tremendous amount of work done in Python with (and without) tensors, it is quite baffling that little work has been done in this regard. Abstract Interpretation is a methodology/framework for statically analysing code. The idea of Abstract Interpretation is to soundly overapproximate the result of running a piece of code over all possible inputs of the program. A sound overapproximation ensures that the Abstract Interpreter will never omit a true negative, i.e.~if a piece of code is not flagged by the Abstract Interpreter, then it can be safely assumed that the code will not fail. The Abstract Interpreter can be modified so that it only outputs true positives, although losing soundness, i.e.~the interpreter can flag which parts of the code are going to fail no matter how the code is run. In this work, we specify a subset of Python with emphasis on tensor operations. Our operational Python semantics is based on The Python Language Reference. We define an Abstract Interpreter and present its implementation. We show how each part of the Abstract Interpreter was built: the Abstract Domains defined and the abstract semantics. We present the structure of Pytropos, the Abstract Interpreter implemented. Pytropos is able to check NumPy array operations taking into account broadcasting and complex NumPy functions as \texttt{array} and \texttt{dot}. We constructed 74 unit test cases checking the capabilities of Pytropos and 20 property test cases checking compliance with the official Python implementation. We show what and how many bugs the Abstract Interpreter was able to find.

• Autores: Cruz Camacho, Elkin Alejandro
• Fecha de publicación: 2019
• Institución: Universidad Nacional de Colombia
• Repositorio: Universidad Nacional de Colombia
• Idioma: spa
• OAI Identifier: oai:repositorio.unal.edu.co:unal/76335
• Acceso en línea: https://repositorio.unal.edu.co/handle/unal/76335; http://bdigital.unal.edu.co/72620/
• Palabra clave: Tensors; Lenguage Python; Programming; Tensores; Lenguaje Python; Programación
• Rights: openAccess
• License: Atribución-NoComercial 4.0 Internacional