KeyError in `res_strict.graph` in Translator when using external library (`numpy`)

[ifndefJOSH]

This may be an issue with mypy and not Nagini, but I discovered an issue when attempting to verify the following minimal Numpy program:

 import numpy as np

from nagini_contracts.contracts import *

def matmult(A : np.matrix, B : np.matrix) -> np.matrix:
	Requires(A.size == B.size)
	Ensures(Result().size == A.size)
	return A * B

The following KeyError is produced in Nagini

Traceback (most recent call last):
  File "/home/josh/.pyenv/versions/3.8.18/bin/nagini", line 8, in <module>
    sys.exit(main())
  File "/home/josh/.pyenv/versions/3.8.18/lib/python3.8/site-packages/nagini_translation/main.py", line 352, in main
    translate_and_verify(args.python_file, jvm, args, arp=args.arp, base_dir=args.base_dir)
  File "/home/josh/.pyenv/versions/3.8.18/lib/python3.8/site-packages/nagini_translation/main.py", line 359, in translate_and_verify
    modules, prog = translate(python_file, jvm, selected=selected, sif=args.sif, base_dir=base_dir,
  File "/home/josh/.pyenv/versions/3.8.18/lib/python3.8/site-packages/nagini_translation/main.py", line 110, in translate
    type_correct = types.check(path, base_dir)
  File "/home/josh/.pyenv/versions/3.8.18/lib/python3.8/site-packages/nagini_translation/lib/typeinfo.py", line 339, in check
    for dep_name in res_strict.graph[name].dep_line_map:
KeyError: 'numpy.core._multiarray_umath'

Notes

• I was unable to reproduce this with other libraries, such as pillow (because of insufficient type annotations)
• This happens on any numpy program I attempt to verify
• numpy.core._multiarray_umath is not a type but rather a module within numpy.
• I've tried this with several versions of numpy, with no difference

My thoughts (as an outsider to your project)

Digging around in your source code, it is evident that res_strict is built by mypy, and name (the variable causing the KeyError) is produced using each of all elements in relevant_files which is directly defined from [next(iter(res_strict.graph))]. This causes the KeyError to be especially confusing, as these are all supposed to be keys from res_strict.graph. Spitballing, it could be related to #37 but honestly it seems like an issue with mypy's Dict (since that's the type of res_strict.graph as you can see here).

[marcoeilers]

I'm not sure why this is happening, but: a) Nagini uses a really old version of mypy, so it's possible that there's a bug in that version that was fixed long ago; b) the NumPy type stubs use a bunch of features Nagini doesn't support yet, so even if this bug did not exist, there would certainly be other issues later.

We're just in the process of starting a project whose goal is, among other things, to make Nagini NumPy compatible. So I hope this will work in a couple of months, but until then, you unfortunately won't be able to verify NumPy client code using Nagini.

[PascalDevenoge]

Apparently the problem seems that the numpy.core._multiarray_umath module is a native C extension module and mypy ignores these (See this among many other issues on mypy python/mypy#8575 (comment)). I guess they don't want to have to deal with extracting type information from C code, which seems fair.

Nagini tries to follow import statements to transitively find all Python files it should care about. The Graph datastructure returned by mypy contains all import statements of all processed modules, but if one of them includes a C extension, then that module itself doesn't have its own entry in the graph, hence the KeyError.

def check(self, filename: str, base_dir: str = None) -> bool:
       ...
           
            # Contains file names of imports found so far
            relevant_files = [next(iter(res_strict.graph))]

            i = 0
            while i < len(relevant_files):
                name = relevant_files[i]
                # The graphs keys only include files processed by mypy, but a files dep_line_map contains _all_ its imports, including those for ignored modules
                for dep_name in res_strict.graph[name].dep_line_map:
                    if dep_name in IGNORED_IMPORTS:
                        continue
                    if dep_name not in relevant_files:
                        # All imports found (including ignored ones) are added to the list and then queried from the dict
                        relevant_files.append(dep_name)
                i += 1

        ...

I've been able to reproduce the exact same error with mypy version 1.0.0, so that behaviour doesn't seem to have changed in recent versions.

Just a guess, but I think we could just skip over these "native" modules. No idea if the missing type information would be a problem in itself though.

[Magikaaarp]

We're just in the process of starting a project whose goal is, among other things, to make Nagini NumPy compatible. So I hope this will work in a couple of months, but until then, you unfortunately won't be able to verify NumPy client code using Nagini.

May I ask how this project is currently progressing? The third-party library I am verifying uses a lot of np.ndarray, which fortunately involves almost no numerical calculations. Perhaps I can wait for this project to be completed.