typpete's Issues
Quick Start instructions missing
README.md
file should contain the instructions how to build the project and how to use it. Ideally it should contain:
- Instructions how to build from source.
- Instructions how install as a Python package.
Failing Tests
In the 'adventure' branch some tests are failing.
Annotated assign is unsatisfiable
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
Limitation with classes order?
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
Variable name in except clause is not added to context
In a try-except block, with code like except Exception as e: ...
, the variable e
is unknown in the except block.
Accessing attribute with the name `count` throws error
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
Bug with classes
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
Add support for abstract methods
- Ignore the body of abstract methods
- Enforce subclasses to override methods which have
@abstarctmethod
decorator which appear in their super class(es).
Allow mutually recursive functions
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
Elements being inferred (/constraints being added) multiple times for the same elements?
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.
SyntaxError when running Typpete with Python 3.7
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
Bug with importing classes
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.
Scoping issues when inheriting methods
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.
Segmentation fault
Why I always get a Segmentation fault even for an empty file when runnig the typpete on Ubuntu 18.04 and Python3.6?
Differentiate between instance methods and callable objects attached as instance variables
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.
Wrong return type inferred for constructors
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.
Crash when using soft constraints
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
ICemu Test Missing
The ICemu test is missing from the master branch.
Results for imported modules
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).
argparse, logging and inplace update
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:
Support for fixed width integers
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
But I'm running into an error on this line:
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.
Unsafe typing due to having None as subtype of all types
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.
Differences between versions of imp-interpreter and ICemu
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.
Use typeshed in lieu of custom type stubs?
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?
Incorrect function override checking for methods with default arguments
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
Support __call__
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__
.
Cannot access imported function (crash)
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)".
Possible optimizations
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 ofB
, that usually (i.e. in other OO languages) means that nothing in the definition ofB
may depend onA
. I don't know if we want to be quite that strict, but USUALLY, if in classB
, something could have either typeA
or typeB
, we want it to have typeB
. 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 typeB
are always also possible on one of typeA
. 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.
Stub methods should not need type annotation for receiver parameter ("self")
Problem with static methods inference
Static methods still expect the first argument to be the receiver.
Will work on this.
Function overloading
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.
Docstrings messed up in annotated files
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.
'''
Handling type aliases
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.
Crash when explicitly mentioning "object" base class
Wrong inferred type for values of dictionary
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
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. ๐๐๐
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google โค๏ธ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.