Python 3.9 support and updated jpype

.github/workflows/test.yml

@@ -13,10 +13,10 @@ jobs:
       BOOGIE_EXE: "/home/runner/.dotnet/tools/boogie"
     steps:
     - uses: actions/checkout@v2
-    - name: Set up Python 3.8
+    - name: Set up Python 3.9
       uses: actions/setup-python@v2
       with:
-        python-version: 3.8
+        python-version: 3.9
     - name: Install Boogie
       run: |
         dotnet tool install --global Boogie --version 2.15.9

README.rst

@@ -6,13 +6,13 @@ Our CAV 2018 tool paper describing Nagini can be found `here <http://pm.inf.ethz
 Dependencies (Ubuntu Linux)
 ===================================
 
-Install Java 11 or newer (64 bit) and Python 3.8 (64 bit, newer versions likely *will not work*) and the required libraries.
+Install Java 11 or newer (64 bit) and Python 3.9 (64 bit, other versions likely *will not work*) and the required libraries.
 For usage with Viper's verification condition generation backend Carbon, you will also need to install Boogie (version 2.15.9).
 
 Dependencies (Windows)
 ==========================
 
-1.  Install Java 11 or newer (64 bit) and Python 3.8 (64 bit, newer versions likely *will not work*).
+1.  Install Java 11 or newer (64 bit) and Python 3.9 (64 bit, other versions likely *will not work*).
 
 2.  Install the required version of either Visual C++ Build Tools or Visual Studio. 
 

setup.py

@@ -10,7 +10,7 @@
 
 setup(
         name='nagini',
-        version='1.0.0',
+        version='1.1.0',
         author='Viper Team',
         author_email='viper@inf.ethz.ch',
         license='MPL-2.0',
@@ -26,14 +26,13 @@
         install_requires=[
             'mypy==0.782',
             'toposort==1.5',
-            'jpype1==0.7.0',
+            'jpype1==1.0.1',
             'astunparse==1.6.2',
-            'typed-ast==1.4.0',
             'pytest==4.3.0',
             'pytest-xdist==1.27.0',
             'z3-solver==4.8.7.0'
             ],
-        entry_points = {
+        entry_points={
              'console_scripts': [
                  'nagini = nagini_translation.main:main',
                  'nagini_client = nagini_translation.client:main',
@@ -50,7 +49,7 @@
             'Intended Audience :: Developers',
             'License :: OSI Approved :: Mozilla Public License 2.0 (MPL 2.0)',
             'Operating System :: OS Independent',
-            'Programming Language :: Python :: 3 :: Only',
+            'Programming Language :: Python :: 3.9',
             'Topic :: Software Development',
             ],
         )

src/nagini_translation/analyzer.py

@@ -450,12 +450,12 @@ def find_or_create_target_class(self, node: ast.AST) -> PythonClass:
             return self.find_or_create_class(node.attr, module=ctx)
         elif isinstance(node, ast.Subscript):
             cls = self.find_or_create_target_class(node.value)
-            if isinstance(node.slice.value, ast.Name):
-                ast_args = [node.slice.value]
-            elif isinstance(node.slice.value, ast.Str):
-                ast_args = [node.slice.value]
+            if isinstance(node.slice, ast.Name):
+                ast_args = [node.slice]
+            elif isinstance(node.slice, ast.Str):
+                ast_args = [node.slice]
             else:
-                ast_args = node.slice.value.elts
+                ast_args = node.slice.elts
             args = [self.find_or_create_target_class(arg) for arg in ast_args]
             result = GenericType(cls, args)
             return result
@@ -542,10 +542,10 @@ def visit_ClassDef(self, node: ast.ClassDef) -> None:
         current_index = 0
         for base in node.bases:
             if isinstance(base, ast.Subscript) and base.value.id == 'Generic':
-                if isinstance(base.slice.value, ast.Name):
-                    arg_names = [base.slice.value.id]
+                if isinstance(base.slice, ast.Name):
+                    arg_names = [base.slice.id]
                 else:
-                    arg_names = [elmt.id for elmt in base.slice.value.elts]
+                    arg_names = [elmt.id for elmt in base.slice.elts]
                 for arg_name in arg_names:
                     assert arg_name in self.module.type_vars
                     var_info = self.module.type_vars[arg_name]

src/nagini_translation/conftest.py

@@ -174,7 +174,7 @@ def pytest_configure(config: 'pytest.config.Config'):
         for test in tests:
             _pytest_config.add_test(test)
         if 'sif-true' in tests or 'sif-poss' in tests or 'sif-prob' in tests:
-            if not jvm.is_known_class(jvm.viper.silver.sif.SIFReturnStmt):
+            if not jvm.is_known_class(jvm.viper.silver.sif, 'SIFReturnStmt'):
                 pytest.exit('Viper SIF extension not avaliable on the classpath.')
     elif config.option.single_test:
         _pytest_config.clear_tests()
@@ -183,9 +183,9 @@ def pytest_configure(config: 'pytest.config.Config'):
         # Default: all tests that are available, SIF tests only if the extension is
         # present.
         tests = ['functional', 'io', 'obligations']
-        if jvm.is_known_class(jvm.viper.silver.sif.SIFReturnStmt):
+        if jvm.is_known_class(jvm.viper.silver.sif, 'SIFReturnStmt'):
             tests.extend(['sif-true', 'sif-poss', 'sif-prob'])
-        if jvm.is_known_class(jvm.viper.silver.plugin.ARPPlugin):
+        if jvm.is_known_class(jvm.viper.silver.plugin, 'ARPPlugin'):
             tests.append('arp')
         for test in tests:
             _pytest_config.add_test(test)
@@ -207,9 +207,9 @@ def pytest_configure(config: 'pytest.config.Config'):
     if not _pytest_config.verifiers:
         # Default: all available verifiers.
         verifiers = []
-        if jvm.is_known_class(jvm.viper.silicon.SiliconRunner):
+        if jvm.is_known_class(jvm.viper.silicon, 'SiliconRunner'):
             verifiers.append('silicon')
-        if jvm.is_known_class(jvm.viper.carbon.Carbon):
+        if jvm.is_known_class(jvm.viper.carbon, 'Carbon'):
             verifiers.append('carbon')
         if not verifiers:
             pytest.exit('No backend verifiers available on the classpath.')

src/nagini_translation/lib/jvmaccess.py

@@ -28,5 +28,12 @@ def get_proxy(self, supertype, instance):
     def get_array(self, t, n):
         return jpype.JArray(t)(n)
 
-    def is_known_class(self, class_object) -> bool:
-        return not isinstance(class_object, jpype.JPackage)
+    def is_known_class(self, package_object, class_name) -> bool:
+        return hasattr(package_object, class_name)
+
+
+def getobject(java, package, name):
+    return java.lang.Class.forName(str(package) + "." + name + "$").getDeclaredField('MODULE$').get(None)
+
+def getclass(java, package, name):
+    return jpype.JClass(java.lang.Class.forName(str(package) + "." + name))

src/nagini_translation/lib/resolver.py

@@ -137,28 +137,28 @@ def get_target(node: ast.AST,
             if type_class:
                 fixed_size = True
                 # Look up the type arguments. Also consider string arguments.
-                if isinstance(node.slice.value, ast.Tuple):
-                    if len(node.slice.value.elts) == 2 and isinstance(node.slice.value.elts[1], ast.Ellipsis):
-                        args = [get_target(node.slice.value.elts[0], containers, container, True)]
+                if isinstance(node.slice, ast.Tuple):
+                    if len(node.slice.elts) == 2 and isinstance(node.slice.elts[1], ast.Ellipsis):
+                        args = [get_target(node.slice.elts[0], containers, container, True)]
                         fixed_size = False
                     else:
                         args = [get_target(arg, containers, container, True)
-                                for arg in node.slice.value.elts]
+                                for arg in node.slice.elts]
                 else:
-                    args = [get_target(node.slice.value, containers, container, True)]
+                    args = [get_target(node.slice, containers, container, True)]
                 res = GenericType(type_class, args)
                 res.exact_length = fixed_size
                 return res
             if node.value.id == 'Optional':
-                option = get_target(node.slice.value, containers, container, True)
+                option = get_target(node.slice, containers, container, True)
                 return OptionalType(option)
             if node.value.id == 'Union':
-                if isinstance(node.slice.value, ast.Tuple):
+                if isinstance(node.slice, ast.Tuple):
                     elts = [get_target(e, containers, container, True)
-                            for e in node.slice.value.elts]
+                            for e in node.slice.elts]
                     return UnionType(elts)
                 else:
-                    return get_target(node.slice.value, containers, container, True)
+                    return get_target(node.slice, containers, container, True)
 
     else:
         return None
@@ -563,14 +563,14 @@ def _get_subscript_type(value_type: PythonType, module: PythonModule,
                 raise UnsupportedException(node, 'tuple slicing')
             if len(value_type.type_args) == 1:
                 return value_type.type_args[0]
-            if isinstance(node.slice.value, ast.UnaryOp):
-                if (isinstance(node.slice.value.op, ast.USub) and
-                        isinstance(node.slice.value.operand, ast.Num)):
-                    index = -node.slice.value.operand.n
+            if isinstance(node.slice, ast.UnaryOp):
+                if (isinstance(node.slice.op, ast.USub) and
+                        isinstance(node.slice.operand, ast.Num)):
+                    index = -node.slice.operand.n
                 else:
                     raise UnsupportedException(node, 'dynamic subscript type')
-            elif isinstance(node.slice.value, ast.Num):
-                index = node.slice.value.n
+            elif isinstance(node.slice, ast.Num):
+                index = node.slice.n
             return value_type.type_args[index]
         else:
             return common_supertype(value_type.type_args)

src/nagini_translation/lib/viper_ast.py

@@ -9,10 +9,10 @@
 
 from nagini_translation.lib.constants import FUNCTION_DOMAIN_NAME
 from nagini_translation.lib.errors import error_manager, Rules
-
-
-def getobject(package, name):
-    return getattr(getattr(package, name + '$'), 'MODULE$')
+from nagini_translation.lib.jvmaccess import (
+    getclass,
+    getobject
+)
 
 
 class Function0:
@@ -41,8 +41,8 @@ def __init__(self, jvm, java, scala, viper, sourcefile):
         self.used_names_sets = {}
 
         def getconst(name):
-            return getobject(ast, name)
-        self.QPs = getobject(ast.utility, 'QuantifiedPermissions')
+            return getobject(java, ast, name)
+        self.QPs = getobject(java, ast.utility, 'QuantifiedPermissions')
         self.AddOp = getconst('AddOp')
         self.AndOp = getconst('AndOp')
         self.DivOp = getconst('DivOp')
@@ -69,13 +69,13 @@ def getconst(name):
         self.Ref = getconst('Ref')
         self.Perm = getconst('Perm')
         self.sourcefile = sourcefile
-        self.none = getobject(scala, 'None')
+        self.none = getobject(java, scala, 'None')
 
     def is_available(self) -> bool:
         """
         Checks if the Viper AST is available, i.e., silver is on the Java classpath.
         """
-        return self.jvm.is_known_class(self.ast.Program)
+        return self.jvm.is_known_class(self.ast, 'Program')
 
     def function_domain_type(self):
         return self.DomainType(FUNCTION_DOMAIN_NAME, {}, [])
@@ -131,10 +131,11 @@ def Program(self, domains, fields, functions, predicates, methods, position, inf
 
     def Function(self, name, args, type, pres, posts, body, position, info):
         body = self.scala.Some(body) if body is not None else self.none
-        return self.ast.Function(name, self.to_seq(args), type,
-                                 self.to_seq(pres),
-                                 self.to_seq(posts),
-                                 body, position, info, self.NoTrafos)
+        function = getobject(self.java, self.ast, 'Function')
+        return function.apply(name, self.to_seq(args), type,
+                              self.to_seq(pres),
+                              self.to_seq(posts),
+                              body, position, info, self.NoTrafos)
 
     def Method(self, name, args, returns, pres, posts, locals, body, position,
                info):
@@ -527,7 +528,7 @@ def to_position(self, expr, vias, error_string: str=None,
                     rules: Rules=None, file: str = None, py_node=None):
         if expr is None:
             return self.NoPosition
-        if not hasattr(expr, 'lineno'):
+        if not hasattr(expr, 'lineno') or expr.lineno is None:
             # TODO: this should never happen (because all nodes that the parser
             # creates have this field), but it does, because in the SIF code we
             # create artificial ast.Name objects which don't have it. That
@@ -539,7 +540,8 @@ def to_position(self, expr, vias, error_string: str=None,
         start = self.ast.LineColumnPosition(expr.lineno, expr.col_offset)
         id = error_manager.add_error_information(
             expr, list(vias), error_string, py_node, rules)
-        if hasattr(expr, 'end_lineno') and hasattr(expr, 'end_col_offset'):
+        if (hasattr(expr, 'end_lineno') and hasattr(expr, 'end_col_offset') and
+                expr.end_lineno is not None and expr.end_col_offset is not None):
             end = self.ast.LineColumnPosition(expr.end_lineno,
                                               expr.end_col_offset)
             end = self.scala.Some(end)

src/nagini_translation/main.py

@@ -23,7 +23,11 @@
 from nagini_translation.lib import config
 from nagini_translation.lib.constants import DEFAULT_SERVER_SOCKET
 from nagini_translation.lib.errors import error_manager
-from nagini_translation.lib.jvmaccess import JVM
+from nagini_translation.lib.jvmaccess import (
+    getclass,
+    getobject,
+    JVM
+)
 from nagini_translation.lib.typedefs import Program
 from nagini_translation.lib.typeinfo import TypeException, TypeInfo
 from nagini_translation.lib.util import (
@@ -55,7 +59,7 @@
 
 
 def parse_sil_file(sil_path: str, bv_path: str, bv_size: int, jvm, float_option: str = None):
-    parser = jvm.viper.silver.parser.FastParser()
+    parser = getclass(jvm.java, jvm.viper.silver.parser, "FastParser")()
     tp = jvm.viper.silver.plugin.standard.termination.TerminationPlugin(None, None, None, parser)
     assert parser
     with open(sil_path, 'r') as file:
@@ -69,17 +73,17 @@ def parse_sil_file(sil_path: str, bv_path: str, bv_size: int, jvm, float_option:
     if float_option == "ieee32":
         text = text.replace("float.sil", "float_ieee32.sil")
     path = jvm.java.nio.file.Paths.get(sil_path, [])
-    none = getattr(getattr(jvm.scala, 'None$'), 'MODULE$')
+    none = getobject(jvm.java, jvm.scala, "None")
     tp.beforeParse(text, False)
-    diskloader = getattr(getattr(jvm.viper.silver.ast.utility, "DiskLoader$"), "MODULE$")
+    diskloader = getobject(jvm.java, jvm.viper.silver.ast.utility, "DiskLoader")
     parsed = parser.parse(text, path, none, diskloader)
 
     parse_result = parsed
     parse_result.initProperties()
     resolver = jvm.viper.silver.parser.Resolver(parse_result)
     resolved = resolver.run()
     resolved = resolved.get()
-    translator = jvm.viper.silver.parser.Translator(resolved)
+    translator = getobject(jvm.java, jvm.viper.silver.parser, 'Translator').apply(resolved)
     # Reset messages in global Consistency object. Otherwise, left-over
     # translation errors from previous translations prevent loading of the
     # built-in silver files.
@@ -159,9 +163,9 @@ def translate(path: str, jvm: JVM, bv_size: int, selected: Set[str] = set(), bas
                                      func_opt=True,
                                      all_low=analyzer.has_all_low)
         if counterexample:
-            prog = getattr(jvm.viper.silicon.sif, 'CounterexampleSIFTransformerO').transform(prog, False)
+            prog = getobject(jvm.java, jvm.viper.silicon.sif, 'CounterexampleSIFTransformerO').transform(prog, False)
         else:
-            prog = getattr(getattr(jvm.viper.silver.sif, 'SIFExtendedTransformer$'), 'MODULE$').transform(prog, False)
+            prog = getobject(jvm.java, jvm.viper.silver.sif, 'SIFExtendedTransformer').transform(prog, False)
         if verbose:
             print('Transformation to MPP successful.')
     if arp:

src/nagini_translation/models/converter.py

@@ -6,6 +6,10 @@
 """
 
 from nagini_translation.lib.constants import RESULT_NAME
+from nagini_translation.lib.jvmaccess import (
+    getclass,
+    getobject
+)
 from nagini_translation.lib.program_nodes import PythonMethod, PythonType, GenericType, PythonField, PythonClass, OptionalType, TypeVar
 from nagini_translation.lib.util import int_to_string, UnsupportedException
 from collections import OrderedDict
@@ -129,9 +133,9 @@ def get_parts(jvm, val):
 def translate_sort(jvm, s):
     terms = jvm.viper.silicon.state.terms
     def get_sort_object(name):
-        return getattr(terms, 'sorts$' + name + '$')
+        return getclass(jvm.java, terms, 'sorts$' + name + '$')
     def get_sort_class(name):
-        return getattr(terms, 'sorts$' + name)
+        return getclass(jvm.java, terms, 'sorts$' + name)
 
     if isinstance(s, get_sort_class('Set')):
         return 'Set<{}>'.format(translate_sort(jvm, s.elementsSort()))
@@ -150,11 +154,11 @@ def get_sort_class(name):
 
 
 def evaluate_term(jvm, term, model):
-    if isinstance(term, getattr(jvm.viper.silicon.state.terms, 'Unit$')):
+    if isinstance(term, getclass(jvm.java, jvm.viper.silicon.state.terms, 'Unit$')):
         return '$Snap.unit'
     if isinstance(term, jvm.viper.silicon.state.terms.IntLiteral):
         return str(term)
-    if isinstance(term, getattr(jvm.viper.silicon.state.terms, "Null$")):
+    if isinstance(term, getclass(jvm.java, jvm.viper.silicon.state.terms, 'Null$')):
         return str(model['$Ref.null'])
     if isinstance(term, jvm.viper.silicon.state.terms.Var):
         key = str(term)
@@ -191,8 +195,7 @@ def evaluate_term(jvm, term, model):
         return get_func_value(model, SNAP_TO + from_sort_name + 'To' + to_sort_name, (sub,))
     elif isinstance(term, jvm.viper.silicon.state.terms.PredicateLookup):
         lookup_func_name = '$PSF.lookup_' + term.predname()
-        toSnapTree = getattr(jvm.viper.silicon.state.terms, 'toSnapTree$')
-        obj = getattr(toSnapTree, 'MODULE$')
+        obj = getobject(jvm.java, jvm.viper.silicon.state.terms, 'toSnapTree')
         snap = obj.apply(term.args())
         psf_value = evaluate_term(jvm, term.psf(), model)
         snap_value = evaluate_term(jvm, snap, model)