[Python-Dev] Static checker for common Python programming errors

[Stefan Bucur]

Thanks for the pointer! There seem indeed to be more formal analysis tools
for JavaScript than for Python (e.g., the most recent one for JS I know of
is the Jalangi framework [1]). I assume the main reason is that JavaScript
is standardized and somewhat simpler, so it's easier to construct formal
specs for all language features than it is for Python, which is also
evolving faster and relies on a lot of hard-to-model native functionality.

That's why I'm planning to reuse as much as possible the "implicit specs"
of the interpreter implementation, instead of re-stating them in an
explicit model.

We already have an execution engine that uses the interpreter to
automatically explore multiple paths through a piece of Python code (you
can read here [2] the academic paper, with case studies for Python and
Lua). In turn, we could use that engine to discover paths, while checking
program properties along each path.

Guido's suggestion for a type checker raises some interesting applications
of this multi-path analysis. For instance, we could examine the type of the
objects assigned to a static variable across all discovered execution paths
and determine its consistency. This analysis could either start with no
type annotations and output suggested types, or take existing annotations
and check them against the actual types.

Thanks again,
Stefan

[1] https://github.com/SRA-SiliconValley/jalangi
[2] http://dslab.epfl.ch/pubs/chef.pdf

On Mon Nov 17 2014 at 8:50:21 PM Francis Giraldeau <
francis.giraldeau at gmail.com> wrote:

> If I may, there are prior work on JavaScript that may be worth
> investigating. Formal verification of dynamically typed software is a
> challenging endeavour, but it is very valuable to avoid errors at runtime,
> providing benefits from strongly type language without the rigidity.
>
> http://cs.au.dk/~amoeller/papers/tajs/
>
> Good luck!
>
> Francis
>
> 2014-11-17 9:49 GMT-05:00 Stefan Bucur <stefan.bucur at gmail.com>:
>
>> I'm developing a Python static analysis tool that flags common
>> programming errors in Python programs. The tool is meant to complement
>> other tools like Pylint (which perform checks at lexical and syntactic
>> level) by going deeper with the code analysis and keeping track of the
>> possible control flow paths in the program (path-sensitive analysis).
>>
>> For instance, a path-sensitive analysis detects that the following
>> snippet of code would raise an AttributeError exception:
>>
>> if object is None: # If the True branch is taken, we know the object is
>> None
>>   object.doSomething() # ... so this statement would always fail
>>
>> I'm writing first to the Python developers themselves to ask, in their
>> experience, what common pitfalls in the language & its standard library
>> such a static checker should look for. For instance, here [1] is a list of
>> static checks for the C++ language, as part of the Clang static analyzer
>> project.
>>
>> My preliminary list of Python checks is quite rudimentary, but maybe
>> could serve as a discussion starter:
>>
>> * Proper Unicode handling (for 2.x)
>>   - encode() is not called on str object
>>   - decode() is not called on unicode object
>> * Check for integer division by zero
>> * Check for None object dereferences
>>
>> Thanks a lot,
>> Stefan Bucur
>>
>> [1] http://clang-analyzer.llvm.org/available_checks.html
>>
>>
>> _______________________________________________
>> Python-Dev mailing list
>> Python-Dev at python.org
>> https://mail.python.org/mailman/listinfo/python-dev
>>
> Unsubscribe:
>> https://mail.python.org/mailman/options/python-dev/francis.giraldeau%40gmail.com
>>
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.python.org/pipermail/python-dev/attachments/20141118/bdc576ac/attachment.html>