Foralln, toMS, new Viper, counterexamples for generics

src/nagini_contracts/contracts.py

@@ -25,15 +25,19 @@
 
 CONTRACT_WRAPPER_FUNCS = ['Requires', 'Ensures', 'Exsures', 'Invariant']
 
-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']
 
 T = TypeVar('T')
 V = TypeVar('V')
+U = TypeVar('U')
+U2 = TypeVar('U2')
+U3 = TypeVar('U3')
+U4 = TypeVar('U4')
 
 
 def Requires(expr: bool) -> bool:
@@ -95,6 +99,46 @@ def Forall(domain: 'Union[Iterable[T], Type[T]]',
     pass
 
 
+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], bool]) -> bool:
     """
     exists x in domain: predicate(x)
@@ -295,6 +339,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.
 
@@ -461,6 +511,11 @@ def dict_pred(d: object) -> bool:
         'RaisedException',
         'Implies',
         'Forall',
+        'Forall2',
+        'Forall3',
+        'Forall4',
+        'Forall5',
+        'Forall6',
         'Exists',
         'Let',
         'Low',
@@ -491,6 +546,7 @@ def dict_pred(d: object) -> bool:
         'PSet',
         'PMultiset',
         'ToSeq',
+        'ToMS',
         'MaySet',
         'MayCreate',
         ]

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/lib/errors/messages.py

@@ -139,7 +139,7 @@
         lambda n: 'Global dependencies may not be defined.',
     'internal':
         lambda n: 'Internal Viper error.',
-    'receiver.not.injective':
+    'qp.not.injective':
         lambda n: 'Receiver expression of quantified permission is not injective.',
     'wait.level.invalid':
         lambda n: 'Thread level may not be lower than current thread.',

src/nagini_translation/lib/resolver.py

@@ -204,6 +204,8 @@ def _do_get_type(node: ast.AST, containers: List[ContainerInterface],
                 if not isinstance(rec_target, PythonModule):
                     rectype = get_type(node.func.value, containers, container)
                     if target.generic_type != -1:
+                        if target.generic_type == -2:
+                            return rectype
                         return rectype.type_args[target.generic_type]
                     if isinstance(target.type, TypeVar):
                         while rectype.python_class is not target.cls:
@@ -404,6 +406,7 @@ def _get_call_type(node: ast.Call, module: PythonModule,
                 assert ctx.current_contract_exception is not None
                 return ctx.current_contract_exception
             elif node.func.id in ('Acc', 'Rd', 'Read', 'Implies', 'Forall', 'IOForall', 'Exists',
+                                  'Forall2', 'Forall3', 'Forall4', 'Forall5', 'Forall6',
                                   'MayCreate', 'MaySet', 'Low', 'LowVal', 'LowEvent', 'LowExit'):
                 return module.global_module.classes[BOOL_TYPE]
             elif node.func.id == 'Declassify':
@@ -417,6 +420,11 @@ def _get_call_type(node: ast.Call, module: PythonModule,
                 seq_class = module.global_module.classes[PSEQ_TYPE]
                 content_type = _get_iteration_type(arg_type, module, node)
                 return GenericType(seq_class, [content_type])
+            elif node.func.id == 'ToMS':
+                arg_type = get_type(node.args[0], containers, container)
+                ms_class = module.global_module.classes[PMSET_TYPE]
+                content_type = _get_iteration_type(arg_type, module, node)
+                return GenericType(ms_class, [content_type])
             elif node.func.id == 'Previous':
                 arg_type = get_type(node.args[0], containers, container)
                 list_class = module.global_module.classes[PSEQ_TYPE]

src/nagini_translation/lib/viper_ast.py

@@ -187,11 +187,11 @@ def MultisetType(self, element_type):
 
     def Domain(self, name, functions, axioms, typevars, position, info):
         return self.ast.Domain(name, self.to_seq(functions),
-                               self.to_seq(axioms), self.to_seq(typevars),
+                               self.to_seq(axioms), self.to_seq(typevars), self.none,
                                position, info, self.NoTrafos)
 
     def DomainFunc(self, name, args, type, unique, position, info, domain_name):
-        return self.ast.DomainFunc(name, self.to_seq(args), type, unique,
+        return self.ast.DomainFunc(name, self.to_seq(args), type, unique, self.none,
                                    position, info, domain_name, self.NoTrafos)
 
     def DomainAxiom(self, name, expr, position, info, domain_name):