marcoeilers / nagini

Nagini is a static verifier for Python 3, based on the Viper verification infrastructure.
Mozilla Public License 2.0
233 stars 8 forks source link

Does not compile with Python 3.5 #139

Closed ldanilek closed 5 years ago

ldanilek commented 5 years ago

The README says that Nagini works with python 3.5 and later.

Trying to run Nagini with python 3.5.2 throws an exception (see below). This exception does not appear in python 3.6 or later.

As you can see from the stacktrace, this is an error in the python 3.5 typing code running on line 90 of contracts.py, which can be reproduced with this small example (crashes python 3.5, works in python 3.6)

from typing import (
    Type,
    TypeVar,
    Union,
)

T = TypeVar('T')

def Forall(domain: Union[str, Type[T]]) -> bool:
    return True

Here is the exception:

ldanilek@ldanilek-dbx:~/src/nagini_sandbox$ ./env/bin/nagini bst.py 
Traceback (most recent call last):
  File "./env/bin/nagini", line 6, in <module>
    from nagini_translation.main import main
  File "/home/ldanilek/src/nagini_sandbox/env/lib/python3.5/site-packages/nagini_translation/main.py", line 24, in <module>
    from nagini_translation.analyzer import Analyzer
  File "/home/ldanilek/src/nagini_sandbox/env/lib/python3.5/site-packages/nagini_translation/analyzer.py", line 11, in <module>
    import nagini_contracts.io_builtins
  File "/home/ldanilek/src/nagini_sandbox/env/lib/python3.5/site-packages/nagini_contracts/io_builtins.py", line 15, in <module>
    from nagini_contracts.contracts import (
  File "/home/ldanilek/src/nagini_sandbox/env/lib/python3.5/site-packages/nagini_contracts/contracts.py", line 90, in <module>
    def Forall(domain: Union[Iterable[T], Type[T]],
  File "/usr/lib/python3.5/typing.py", line 552, in __getitem__
    dict(self.__dict__), parameters, _root=True)
  File "/usr/lib/python3.5/typing.py", line 512, in __new__
    for t2 in all_params - {t1} if not isinstance(t2, TypeVar)):
  File "/usr/lib/python3.5/typing.py", line 512, in <genexpr>
    for t2 in all_params - {t1} if not isinstance(t2, TypeVar)):
  File "/usr/lib/python3.5/typing.py", line 1077, in __subclasscheck__
    if super().__subclasscheck__(cls):
  File "/home/ldanilek/src/nagini_sandbox/env/lib/python3.5/abc.py", line 225, in __subclasscheck__
    for scls in cls.__subclasses__():
TypeError: descriptor '__subclasses__' of 'type' object needs an argument

Given that the documentation says Nagini works with python 3.5, the code should be modified to not throw exceptions when run with python 3.5.

marcoeilers commented 5 years ago

Thanks, fixed with commit db6850262545f833b4cd4e652298dd3fdf739a63.