Hi! First off, this seems like a very promising project, I'm curious to see how far it can be taken. I was thinking it could be useful to use typeshed stubs instead of the custom builtin definitions, as typeshed is much more complete.

I expect there are things in typeshed that may cause issues?

When a function is inherited, it's copied into the class that inherits it. If that inheriting class is in a different module, the inference will apparently run a second time on the inherited version. But that inherited version will now be treated as if it was in the module of the class that inherited it. If the method relies on some imports that are present in its own module, but not the module of the inheriting class, this leads to errors.

From @caterinaurban on July 27, 2017 15:56

It seems that the inference cannot handle such program:

class Parser:
    def _add_(self, other):
        return Concat(self, other)

class Concat(Parser):
    def _init_(self, left, right):
        self.left = left
        self.right = right

Can we maybe preprocess the classes in some way to handle this?

Copied from original issue: caterinaurban/Lyra#56

Currently, any attribute call adds the instance as a first argument for the receiver, accordingly, the following doesn't work.

class A:
    def __init__(self, f):
        self.f = f
    def g(self):
        return self.f()

def f():
    pass

x = A(f)

because the call self.f() in method g is considered a method call, so it as the instance self as an argument, whereas function f doesn't expect any arguments.

I've made some usability improvements in the fork at:

https://github.com/adsharma/Typpete

A few questions:

• Are these improvements interesting?
• If not and if you'd prefer that I maintain them in a fork, would you like me to use a different name for the project or Typpete is ok?

Some context on how I'm trying to incorporate this work into py2many:

py2many/py2many#440

In the 'adventure' branch some tests are failing.

From @caterinaurban on July 28, 2017 13:35

The type inferred for env in the following program is wrong:

class Aexp:
    def eval(self, env):
        return 0

class IntAexp(Aexp):
    def __init__(self, i):
        self.i = i

    def eval(self, env):
        return self.i

class BinopAexp(Aexp):
    def __init__(self, op, left, right):
        self.op = op
        self.left = left
        self.right = right

    def eval(self, env):
        left_value = self.left.eval(env)
        right_value = self.right.eval(env)
        if self.op == '/':
            value = left_value / right_value
            return value
        else:
            raise RuntimeError('unknown operator: ' + self.op)

class Statement:
    def eval(self, env):
        pass

class AssignStatement(Statement):
    def __init__(self, name, aexp):
        self.name = name
        self.aexp = aexp

    def eval(self, env):
        value = self.aexp.eval(env)
        env[self.name] = value

"""
x = 0
x = 1 / 2
"""

env = dict()
i = AssignStatement('x', IntAexp(0))
d = BinopAexp('/', IntAexp(1), IntAexp(2))
f = d.eval(env)
a = AssignStatement('x', d)
a.eval(env)
print(env)

The type should be Dict[str, float] but Dict[str, int] is inferred instead.

Copied from original issue: caterinaurban/Lyra#59

• Ignore the body of abstract methods
• Enforce subclasses to override methods which have @abstarctmethod decorator which appear in their super class(es).

When a class has an instance attribute with the name count, a type error is thrown.
For example, this throws an error:

class A:
    def __init__(self):
        self.count = 1

But this one doesn't:

class A:
    def __init__(self):
        self.count2 = 1

https://mypy.readthedocs.io/en/stable/more_types.html#function-overloading

was introduced in py38, a couple of years ago.

Looks like it could help solvers like typpete.

When running Typpete with Python 3.7 and the following example file I get an SyntaxError: invalid syntax

Example file:

from abc import ABCMeta, abstractmethod

class Item (metaclass=ABCMeta):
    @abstractmethod
    def compete(self, item):
        pass

    def evalEven(self, item):
        return "WIN"

    def evalOdd(self, item):
        return "LOSE"


class Even(Item):
    def compete(self, item):
        return item.evalEven(self)


class Odd(Item):
    def compete(self, item):
        return item.evalOdd(self)


def match(item1, item2):
    return item1.compete(item2)

Traceback (most recent call last):
  File "venv/bin/typpete", line 7, in <module>
    from typpete.inference_runner import run_inference
  File "~/tmp/Typpete/venv/lib/python3.7/site-packages/typpete/inference_runner.py", line 1, in <module>
    from typpete.src.stmt_inferrer import *
  File "~/tmp/Typpete/venv/lib/python3.7/site-packages/typpete/src/stmt_inferrer.py", line 24, in <module>
    import typpete.src.expr_inferrer as expr
  File "~/tmp/Typpete/venv/lib/python3.7/site-packages/typpete/src/expr_inferrer.py", line 35, in <module>
    import typpete.src.z3_axioms as axioms
  File "~/tmp/Typpete/venv/lib/python3.7/site-packages/typpete/src/z3_axioms.py", line 2, in <module>
    from typpete.src.z3_types import And, Or, Implies, Not
  File "~/tmp/Typpete/venv/lib/python3.7/site-packages/typpete/src/z3_types.py", line 13, in <module>
    from typpete.src.pre_analysis import PreAnalyzer
  File "~/tmp/Typpete/venv/lib/python3.7/site-packages/typpete/src/pre_analysis.py", line 6, in <module>
    from typpete.src.import_handler import ImportHandler
  File "~/tmp/Typpete/venv/lib/python3.7/site-packages/typpete/src/import_handler.py", line 2, in <module>
    import astunparse
  File "~/tmp/Typpete/venv/lib/python3.7/site-packages/astunparse/__init__.py", line 4, in <module>
    from .unparser import Unparser
  File "~/tmp/Typpete/venv/lib/python3.7/site-packages/astunparse/unparser.py", line 331
    def _generic_FunctionDef(self, t, async=False):
                                          ^
SyntaxError: invalid syntax

From @mostafa-abdullah on July 20, 2017 12:58

Example

def f(x):
    if x == 0:
        return 1
    return g(x - 1)

def g(x):
    if x == 0:
        return 2
    return f(x - 1)

The approach I plan to take is to pre-analyze all function definitions and store the corresponding z3 types in the context, so when the inferencer encounters the g function call (whose definition didn't appear yet) it will have its type already in the context.

The problem with this is that it will allow some incorrect programs to type, like the following one:

def f(x):
    if x == 0:
        return 1
    return g(x - 1)

f(1)

def g(x):
    if x == 0:
        return 2
    return f(x - 1)

Because by the time f is called, g wouldn't have appeared yet.

What do you think? Do you think the above example is tolerable? Can we consider it as a normal run-time error that is not type-related?

Copied from original issue: caterinaurban/Lyra#43

If in class Super I have a method which takes one parameter (non-default) in addition to self, I cannot override it with an identical method where the one parameter has a default value? That seems wrong.

TypeError: Method _setup_sockets in subclass Router should have non-default arguments length less thanor equal that in superclass

In a try-except block, with code like except Exception as e: ..., the variable e is unknown in the except block.

The only thing left to completely support IMP interpreter is to support the built in __call__.

This works by adding disjunctions for calls to include instances of classes which implement __call__.

from typing import Union, Dict, List

JsonData = Union[Dict[str, 'JsonData'], List['JsonData'], int, float, bool, None]
a: JsonData = {"foo" : 10}

Fails with

NameError: Name Union is not defined.

x = int
a: x = 10

also fails, but with a different error message.

In the SCION code, when I have a couple of modules, each of which may import some other modules, it seems that many many many identical constraints are added to the SMT problem multiple times. Is it possible that this happens

• when multiple modules import the same other module?
• when methods/... are inherited in one class from another? Do we run the inference separately on the copied version?

I think the inference should run exactly once on each module, no matter how many other modules import it, and once on each method, no matter how often it is inherited. I think especially the former is one of the main reasons why the inference on SCION code is currently slow.

The imported classes for some reason aren't considered in the pre-analysis part which creates a default init method and propagates the inherited attributes to subclasses.

I will put this as a top priority for now and investigate the solution.

From @mostafa-abdullah on July 20, 2017 12:50

The current inference allows class methods to be called as normal calls with passing the first argument as the class instance.

For example, the current is allowed (which shouldn't be)

class A:
    def f(self):
         instance = A()
         return f(instance)

And accordingly, the following is not allowed (Which should be):

def f():
     return 1

class A:
    def f(self):
         return f()

Because the inference confuses the function call f() with the method f(self)

Copied from original issue: caterinaurban/Lyra#42

It seems currently impossible to obtain the result of the type inference for imported modules. Due to this I am unable to see which files of one project (e.g., ICemu) are actually included in a run of the type inference (via imports).

When I have e.g. the import statement "import copy", and the module (in my case it's a stub, not sure if the problem is more general) named copy contains a function "def deepcopy(o: object) -> object: ...", I cannot access this function in a method writing "copy.deepcopy(someObject)".

def f(x, y):
    return x(y)


def a(x: int):
    return x


def b(x: str):
    return x


l = f(a, 1)
m = f(b, "str")

l += 1
m += 1

The type of f is inferred to be Callable[[Callable[[object], None], object], None]
i.e.
x arg is a function which takes an object and returns None
y arg is object
returns None

so variable l is inferred to be any super type of None which may be int, and so is m.

Accordingly the addition operations l += 1, m += 1 pass the type checking.

Static methods still expect the first argument to be the receiver.

Will work on this.

In Mypy, constructor return types are always None (python/mypy#604), but we seem to infer the type of the class as the return type instead? Or maybe we infer arbitrary types and I just happened to get the type of the class as the return type? Either way, it should be None instead.

typpete /tmp/foo.py / --enable_soft_constraints=0

works ok. But the default behavior with --enable_soft_contraints=true results in a core dump inside Z3_optimize_check().

This is on a vanilla ubuntu 20.04 system with python3.8

README.md file should contain the instructions how to build the project and how to use it. Ideally it should contain:

1. Instructions how to build from source.
2. Instructions how install as a Python package.

The ICemu test is missing from the master branch.

The differences between the versions of the imp-interpreter and ICemu projects that we use and the originals are very suspicious. For instance, there are calls completely commented out and replaced by pass, and an index in a comprehension is replaced by a number. Are we sure that we are preserving the original functionality of the code? I seriously doubt it. This needs to be fixed and every single change compared to the original version should be meticulously tracked and clearly justified.

def foo():
    j: float = 200
    return 42

This type checks ok with mypy and pyright. But when run with typpete I get:

Constraints collection took  0.12059378623962402s
Constraints solving took  0.0006952285766601562s
Check: unsat
WARNING: optimization with quantified constraints is not supported
Solving relaxed model took  0.009663581848144531s
Unsat:
Body type in line 1
Writing output to inference_output

The output files we produce that contain the original program with added type annotations has messed up docstrings. For example, we get something like this:

'\n    Flattens a dict of lists, i.e., concatenates all lists for the same keys.\n    '

which presumably lookes like this before:

'''
Flattens a dict of lists, i.e., concatenates all lists for the same keys.
'''

Why I always get a Segmentation fault even for an empty file when runnig the typpete on Ubuntu 18.04 and Python3.6?

I think there are some possibilities to add additional constraints that reduce the search space for Z3 a bit. We could list them here.

At the moment, I have exactly one idea:

• If A is a subclass of B, that usually (i.e. in other OO languages) means that nothing in the definition of B may depend on A. I don't know if we want to be quite that strict, but USUALLY, if in class B, something could have either type A or type B, we want it to have type B. I think it could be worth restricting that, especially since this is a case that may happen a lot, since all operations possible on a variable of type B are always also possible on one of type A. So there might be a lot of disjunctions, and there will usually be no good reason for the SMT solver to choose one over the other. That might lead to performance problems especially when we're doing optimization.

I'm trying to implement the following:

def foo(x, y):
    i: i8 = 200  # should not be satisfiable due to width
    j = 200 # ok

using

adsharma@53feec0

But I'm running into an error on this line:

https://github.com/adsharma/Typpete/blob/53feec072a60675436748d024a988902ae489f33/typpete/src/z3_types.py#L566

TypeError: '<' not supported between instances of 'DatatypeRef' and 'int'

If t was an Int it would have been a valid expression. But it seems to be a DatatypeRef. Any suggestions on how to specify this constraint? Looks like I have to ast-fy the limit to be able to build an expression. Pointers to existing code would be great. I looked at z3_axioms.py but couldn't find one.