Many small updates

.github/workflows/test.yml

@@ -19,7 +19,7 @@ jobs:
         python-version: 3.8
     - name: Install Boogie
       run: |
-        dotnet tool install --global Boogie --version 2.4.21
+        dotnet tool install --global Boogie --version 2.15.9
     - name: Install Nagini
       run: |
         python -m pip install --upgrade pip

setup.py

@@ -36,6 +36,7 @@
         entry_points = {
              'console_scripts': [
                  'nagini = nagini_translation.main:main',
+                 'nagini_client = nagini_translation.client:main',
                  ]
              },
         url='http://www.pm.inf.ethz.ch/research/nagini.html',

src/nagini_contracts/contracts.py

@@ -12,7 +12,8 @@
     Generic,
     Iterable,
     Iterator,
-    List, Set,
+    List,
+    Optional,
     Sized,
     Tuple,
     Type,
@@ -23,21 +24,21 @@
 
 GHOST_PREFIX = "_gh_"
 
-CONTRACT_WRAPPER_FUNCS = ['Requires', 'Ensures', 'Exsures', 'Invariant']
+CONTRACT_WRAPPER_FUNCS = ['Requires', 'Ensures', 'Exsures', 'Invariant', 'Decreases']
 
-CONTRACT_FUNCS = ['Assume', 'Assert', 'Old', 'Result', 'Implies', 'Forall', 'IOForall',
+CONTRACT_FUNCS = ['Assume', 'Assert', 'Old', 'Result', 'Implies', 'Forall', 'IOForall', 'Forall2', 'Forall3', 'Forall6',
                   'Exists', 'Low', 'LowVal', 'LowEvent', 'Declassify', 'TerminatesSif',
                   'Acc', 'Rd', 'Wildcard', 'Fold', 'Unfold', 'Unfolding', 'Previous',
-                  'RaisedException', 'PSeq', 'PSet', 'ToSeq', 'MaySet', 'MayCreate',
+                  'RaisedException', 'PSeq', 'PSet', 'ToSeq', 'ToMS', 'MaySet', 'MayCreate',
                   'getMethod', 'getArg', 'getOld', 'arg', 'Joinable', 'MayStart', 'Let',
-                  'PMultiset', 'LowExit', 'SplitOn']
+                  'PMultiset', 'LowExit', 'Refute']
 
 T = TypeVar('T')
 V = TypeVar('V')
-
-
-def SplitOn(expr: bool, trueSplit: bool = True, falseSplit: bool = True) -> bool:
-    pass
+U = TypeVar('U')
+U2 = TypeVar('U2')
+U3 = TypeVar('U3')
+U4 = TypeVar('U4')
 
 
 def Requires(expr: bool) -> bool:
@@ -56,6 +57,10 @@ def Invariant(expr: bool) -> bool:
     pass
 
 
+def Decreases(expr: Optional[int], condition: bool = True) -> bool:
+    pass
+
+
 def Assume(expr: bool) -> None:
     pass
 
@@ -64,6 +69,10 @@ def Assert(expr: bool) -> bool:
     pass
 
 
+def Refute(expr: bool) -> bool:
+    pass
+
+
 def Old(expr: T) -> T:
     pass
 
@@ -99,7 +108,47 @@ def Forall(domain: 'Union[Iterable[T], Type[T]]',
     pass
 
 
-def Exists(domain: 'Union[Iterable[T], Type[T]]', predicate: Callable[[T], bool]) -> bool:
+def Forall2(domain1: 'Type[T]', domain2: Type[V],
+           predicate: Callable[[T, V], Union[bool, Tuple[bool, List[List[Any]]]]]) -> bool:
+    """
+    forall x in domain1, y in domain2: predicate(x, y)
+    """
+    pass
+
+
+def Forall3(domain1: 'Type[T]', domain2: Type[V], domain3: Type[U],
+           predicate: Callable[[T, V, U], Union[bool, Tuple[bool, List[List[Any]]]]]) -> bool:
+    """
+    forall x in domain1, y in domain2, z in domain3: predicate(x, y, z)
+    """
+    pass
+
+
+def Forall4(domain1: 'Type[T]', domain2: Type[V], domain3: Type[U], domain4: Type[U2],
+            predicate: Callable[[T, V, U, U2], Union[bool, Tuple[bool, List[List[Any]]]]]) -> bool:
+    """
+    forall x in domain1, y in domain2, z in domain3, ...: predicate(x, y, z, ...)
+    """
+    pass
+
+
+def Forall5(domain1: 'Type[T]', domain2: Type[V], domain3: Type[U], domain4: Type[U2], domain5: Type[U3],
+            predicate: Callable[[T, V, U, U2, U3], Union[bool, Tuple[bool, List[List[Any]]]]]) -> bool:
+    """
+    forall x in domain1, y in domain2, z in domain3, ...: predicate(x, y, z, ...)
+    """
+    pass
+
+
+def Forall6(domain1: 'Type[T]', domain2: Type[V], domain3: Type[U], domain4: Type[U2], domain5: Type[U3], domain6: Type[U4],
+            predicate: Callable[[T, V, U, U2, U3, U4], Union[bool, Tuple[bool, List[List[Any]]]]]) -> bool:
+    """
+    forall x in domain1, y in domain2, z in domain3, ...: predicate(x, y, z, ...)
+    """
+    pass
+
+
+def Exists(domain: 'Union[Iterable[T], Type[T]]', predicate: Callable[[T], Union[bool, Tuple[bool, List[List[Any]]]]]) -> bool:
     """
     exists x in domain: predicate(x)
     """
@@ -299,6 +348,12 @@ def ToSeq(l: Iterable[T]) -> PSeq[T]:
     """
 
 
+def ToMS(s: PSeq[T]) -> PMultiset[T]:
+    """
+    Multiset view of the given sequence.
+    """
+
+
 # The following annotations have no runtime semantics. They are only used for
 # the Python to Viper translation.
 
@@ -456,15 +511,22 @@ def dict_pred(d: object) -> bool:
         'Requires',
         'Ensures',
         'Exsures',
+        'Decreases',
         'Invariant',
         'Previous',
         'Assume',
         'Assert',
+        'Refute',
         'Old',
         'Result',
         'RaisedException',
         'Implies',
         'Forall',
+        'Forall2',
+        'Forall3',
+        'Forall4',
+        'Forall5',
+        'Forall6',
         'Exists',
         'Let',
         'Low',
@@ -495,7 +557,7 @@ def dict_pred(d: object) -> bool:
         'PSet',
         'PMultiset',
         'ToSeq',
+        'ToMS',
         'MaySet',
         'MayCreate',
-        'SplitOn',
         ]

src/nagini_translation/analyzer.py

@@ -351,7 +351,7 @@ def visit_module(self, module: PythonModule) -> None:
     def visit_Module(self, node: ast.Module) -> None:
         for stmt in node.body:
             if isinstance(stmt, (ast.ClassDef, ast.FunctionDef, ast.Import,
-                                 ast.ImportFrom, ast.Assign)):
+                                 ast.ImportFrom, ast.Assign, ast.AnnAssign)):
                 continue
             if (isinstance(stmt, ast.Expr) and
                     isinstance(stmt.value, ast.Str)):
@@ -728,33 +728,57 @@ def visit_While(self, node: ast.While) -> None:
     def visit_For(self, node: ast.While) -> None:
         self.visit_loop(node)
 
+    def _visit_single_name_assign(self, name: ast.Name, node: ast.Assign) -> Tuple[bool, bool]:
+        is_alias = False
+        is_type_var = False
+        actual_prefix = []
+        if self.module.type_prefix:
+            actual_prefix = self.module.type_prefix.split('.')
+        actual_prefix.append(name.id)
+        lhs_name = tuple(actual_prefix)
+        # If it's a type alias marked by mypy
+        if lhs_name in self.types.type_aliases:
+            type_name = self.types.type_aliases[lhs_name]
+            aliased_type = self.convert_type(type_name, node)
+            self.module.classes[name.id] = aliased_type
+            is_alias = True
+        # If it's a type variable marked by mypy
+        elif lhs_name in self.types.type_vars:
+            var = self.types.type_vars[lhs_name]
+            self.module.type_vars[name.id] = var
+            is_type_var = True
+        # Could still be a type alias if RHS refers to class
+        elif not isinstance(node.value, ast.Call):
+            target = self.get_target(node.value, self.module)
+            if isinstance(target, PythonType):
+                self.module.classes[name.id] = target
+                is_alias = True
+        return is_alias, is_type_var
+
     def visit_Assign(self, node: ast.Assign) -> None:
         is_alias = False
         is_type_var = False
         # Check if this is a type alias
         if len(node.targets) == 1 and isinstance(node.targets[0], ast.Name):
-            actual_prefix = []
-            if self.module.type_prefix:
-                actual_prefix = self.module.type_prefix.split('.')
-            actual_prefix.append(node.targets[0].id)
-            lhs_name = tuple(actual_prefix)
-            # If it's a type alias marked by mypy
-            if lhs_name in self.types.type_aliases:
-                type_name = self.types.type_aliases[lhs_name]
-                aliased_type = self.convert_type(type_name, node)
-                self.module.classes[node.targets[0].id] = aliased_type
-                is_alias = True
-            # If it's a type variable marked by mypy
-            elif lhs_name in self.types.type_vars:
-                var = self.types.type_vars[lhs_name]
-                self.module.type_vars[node.targets[0].id] = var
-                is_type_var = True
-            # Could still be a type alias if RHS refers to class
-            elif not isinstance(node.value, ast.Call):
-                target = self.get_target(node.value, self.module)
-                if isinstance(target, PythonType):
-                    self.module.classes[node.targets[0].id] = target
-                    is_alias = True
+            is_alias, is_type_var = self._visit_single_name_assign(node.targets[0], node)
+
+        # Nothing else to do for type aliases and type vars, for all other
+        # cases proceed as usual.
+        if is_alias:
+            if self.current_function or self.current_class:
+                raise InvalidProgramException(node, 'local.type.alias')
+        elif is_type_var:
+            if self.current_function or self.current_class:
+                raise InvalidProgramException(node, 'local.typevar')
+        else:
+            self.visit_default(node)
+
+    def visit_AnnAssign(self, node: ast.AnnAssign) -> None:
+        is_alias = False
+        is_type_var = False
+        # Check if this is a type alias
+        if isinstance(node.target, ast.Name):
+            is_alias, is_type_var = self._visit_single_name_assign(node.target, node)
 
         # Nothing else to do for type aliases and type vars, for all other
         # cases proceed as usual.
@@ -896,6 +920,11 @@ def visit_Call(self, node: ast.Call) -> None:
             elif node.func.id == 'Ensures':
                 self.stmt_container.postcondition.append(
                     (node.args[0], self._aliases.copy()))
+            elif node.func.id == 'Decreases':
+                if not (isinstance(self.stmt_container, PythonMethod) and self.stmt_container.pure):
+                    raise InvalidProgramException(node, 'invalid.contract.position')
+                self.stmt_container.decreases_clauses.append(
+                    (node.args, self._aliases.copy()))
             elif node.func.id == 'Exsures':
                 exception = self.get_target(node.args[0], self.module)
                 if exception not in self.current_function.declared_exceptions:
@@ -1009,7 +1038,7 @@ def visit_Name(self, node: ast.Name) -> None:
                         var = self.node_factory.create_python_global_var(
                             node.id, node, cls, self.module)
                     assign = node._parent
-                    if isinstance(assign, ast.Assign) and len(assign.targets) == 1:
+                    if (isinstance(assign, ast.Assign) and len(assign.targets) == 1) or isinstance(assign, ast.AnnAssign):
                         var.value = assign.value
                     self.module.global_vars[node.id] = var
                 current_module = self.module

src/nagini_translation/analyzer_io.py

@@ -309,7 +309,8 @@ def visit_Call(self, node: ast.Call) -> None:
                 self.visit(arg)
             self._in_property = False
             return
-        elif isinstance(node.func, ast.Name) and node.func.id in ('IOForall', 'Forall', 'Exists'):
+        elif isinstance(node.func, ast.Name) and node.func.id in ('IOForall', 'Forall', 'Forall2', 'Forall3', 'Forall4',
+                                                                  'Forall5', 'Forall6', 'Exists'):
             operation = self._current_io_operation
             assert len(node.args[1].args.args) == 1
             arg_type = self._parent.get_target(node.args[0], operation.module)

src/nagini_translation/client.py

@@ -10,20 +10,23 @@
 
 from nagini_translation.lib.constants import DEFAULT_CLIENT_SOCKET
 
+def main():
+        context = zmq.Context()
 
-context = zmq.Context()
+        socket = context.socket(zmq.REQ)
+        socket.connect(DEFAULT_CLIENT_SOCKET)
 
-socket = context.socket(zmq.REQ)
-socket.connect(DEFAULT_CLIENT_SOCKET)
+        parser = argparse.ArgumentParser()
+        parser.add_argument(
+                'python_file',
+                help='Python file to verify')
 
-parser = argparse.ArgumentParser()
-parser.add_argument(
-        'python_file',
-        help='Python file to verify')
+        args = parser.parse_args()
 
-args = parser.parse_args()
+        socket.send_string(args.python_file)
+        response = socket.recv_string()
 
-socket.send_string(args.python_file)
-response = socket.recv_string()
+        print(response)
 
-print(response)
+if __name__ == '__main__':
+    main()

src/nagini_translation/conftest.py

@@ -212,7 +212,7 @@ def pytest_configure(config: 'pytest.config.Config'):
         if jvm.is_known_class(jvm.viper.carbon.Carbon):
             verifiers.append('carbon')
         if not verifiers:
-            pytest.exit('No backend verifiers avaliable on the classpath.')
+            pytest.exit('No backend verifiers available on the classpath.')
         for verifier in verifiers:
             _pytest_config.add_verifier(verifier)
 

src/nagini_translation/lib/constants.py

@@ -201,7 +201,10 @@
     'none',
     'epsilon',
     'perm',
-    'unique']
+    'unique',
+    'range',
+    'domain',
+    'Map']
 
 LEGAL_MAGIC_METHODS = {
     '__eq__',

src/nagini_translation/lib/errors/manager.py

@@ -128,9 +128,10 @@ def _convert_error(
             rules = {}
         error_item = self._get_item(position)
 
-        if error_item is not None and original_error.counterexample().isDefined() and isinstance(error_item.py_node, PythonMethod):
+        if (error_item is not None and original_error.failureContexts().nonEmpty() and
+                original_error.failureContexts().head().counterExample().isDefined() and isinstance(error_item.py_node, PythonMethod)):
             pymethod = error_item.py_node
-            ce = original_error.counterexample().get()
+            ce = original_error.failureContexts().head().counterExample().get()
             if sif:
                 ce = getattr(jvm.viper.silicon.sif, 'CounterexampleSIFTransformerO').transformCounterexample(ce, pymethod.sil_name)
             inputs = Extractor().extract_counterexample(jvm, pymethod, ce, modules)