Version bump, decreases clauses with predicates

setup.py

@@ -1,5 +1,5 @@
 """
-Copyright (c) 2019 ETH Zurich
+Copyright (c) 2023 ETH Zurich
 This Source Code Form is subject to the terms of the Mozilla Public
 License, v. 2.0. If a copy of the MPL was not distributed with this
 file, You can obtain one at http://mozilla.org/MPL/2.0/.
@@ -10,7 +10,7 @@
 
 setup(
         name='nagini',
-        version='0.9.0',
+        version='1.0.0',
         author='Viper Team',
         author_email='[email protected]',
         license='MPL-2.0',

src/nagini_translation/lib/errors/messages.py

@@ -86,6 +86,8 @@
         lambda n: 'Function might not terminate.',
     'refute.failed':
         lambda n: 'Refute holds in all cases or could not be reached.',
+    'predicateinstance.no.access':
+        lambda n: 'Predicate access might fail.'
 }
 
 REASONS = {

src/nagini_translation/lib/viper_ast.py

@@ -291,6 +291,10 @@ def DecreasesWildcard(self, condition, position, info):
         condition = self.scala.Some(condition) if condition is not None else self.none
         return self.jvm.viper.silver.plugin.standard.termination.DecreasesWildcard(condition, position, info, self.NoTrafos)
 
+    def PredicateInstance(self, args, pred_name, position, info):
+        args_seq = self.to_seq(args)
+        return self.jvm.viper.silver.plugin.standard.predicateinstance.PredicateInstance(args_seq, pred_name, position, info, self.NoTrafos)
+
     def FullPerm(self, position, info):
         return self.ast.FullPerm(position, info, self.NoTrafos)
 

src/nagini_translation/resources/all.sil

@@ -6,6 +6,7 @@
  */
 
 import <decreases/int.vpr>
+import <decreases/predicate_instance.vpr>
 
 domain SIFDomain[T] {
     function Low(x: T): Bool

src/nagini_translation/sif/resources/all.sil

@@ -6,6 +6,8 @@
  */
 
 import <decreases/int.vpr>
+import <decreases/predicate_instance.vpr>
+
 
 domain SIFDomain[T] {
     function Low(x: T): Bool

src/nagini_translation/translators/method.py

@@ -110,7 +110,15 @@ def _translate_decreases(self, method: PythonMethod,
                 if isinstance(measure_node, ast.NameConstant) and measure_node.value is None:
                     decreases_clause = self.viper.DecreasesWildcard(condition, pos, info)
                 else:
-                    measure_stmt, measure = self.translate_expr(measure_node, ctx, target_type=self.viper.Int)
+                    measure = None
+                    if isinstance(measure_node, ast.Call):
+                        target = self.get_target(measure_node, ctx)
+                        if isinstance(target, PythonMethod) and target.predicate:
+                            measure_stmt, measure_args, _ = self.translate_args(target, measure_node.args,
+                                                                                measure_node.keywords, measure_node, ctx)
+                            measure = self.viper.PredicateInstance(measure_args, target.sil_name, pos, info)
+                    if measure is None:
+                        measure_stmt, measure = self.translate_expr(measure_node, ctx, target_type=self.viper.Int)
                     decreases_clause = self.viper.DecreasesTuple([measure], condition, pos, info)
                     if measure_stmt:
                         raise InvalidProgramException(measure_node, 'purity.violated')

src/nagini_translation/verifier.py

@@ -117,7 +117,9 @@ def __init__(self, jvm: JVM, filename: str, viper_args: List[str], counterexampl
             '--exhaleMode=2',
             '--alternativeFunctionVerificationOrder',
             '--disableDefaultPlugins',
-            '--plugin=viper.silver.plugin.standard.refute.RefutePlugin:viper.silver.plugin.standard.termination.TerminationPlugin',
+            '--plugin=viper.silver.plugin.standard.refute.RefutePlugin:'
+            'viper.silver.plugin.standard.termination.TerminationPlugin:'
+            'viper.silver.plugin.standard.predicateinstance.PredicateInstancePlugin',
             *(['--counterexample=native'] if counterexample else []),
             *viper_args,
         ]
@@ -162,6 +164,10 @@ def __init__(self, jvm: JVM, filename: str, viper_args: List[str]):
             '--assumeInjectivityOnInhale',
             '--boogieExe', config.boogie_path,
             '--z3Exe', config.z3_path,
+            '--disableDefaultPlugins',
+            '--plugin=viper.silver.plugin.standard.refute.RefutePlugin:'
+            'viper.silver.plugin.standard.termination.TerminationPlugin:'
+            'viper.silver.plugin.standard.predicateinstance.PredicateInstancePlugin',
             *viper_args
         ]
         args_seq = list_to_seq(args, jvm, jvm.java.lang.String)

tests/functional/verification/examples/iap_bst.py

@@ -68,6 +68,7 @@ def tree(n : TreeNode) -> bool:
 @Pure
 def sorted(n: TreeNode, upper: Optional[int], lower: Optional[int]) -> bool:
     Requires(tree(n))
+    Decreases(tree(n))
     return (Unfolding(tree(n),
             Implies(upper is not None, n.key < upper) and
             Implies(lower is not None, n.key > lower) and

tests/functional/verification/test_decreases.py

@@ -2,6 +2,7 @@
 # http://creativecommons.org/publicdomain/zero/1.0/
 
 from nagini_contracts.contracts import *
+from typing import Optional
 
 @Pure
 def fac1(i: int) -> int:
@@ -80,4 +81,36 @@ def fac5pre(i: int) -> int:
         return fac5pre(i)
     if i <= 1:
         return 1
-    return i * fac5pre(i - 1)
+    return i * fac5pre(i - 1)
+
+
+class Node:
+    def __init__(self) -> None:
+        self.value = 0
+        self.next : Optional[Node] = None
+
+
+@Predicate
+def tree(n: Node) -> bool:
+    return (
+        Acc(n.next) and Acc(n.value) and Implies(n.next is not None, tree(n.next))
+    )
+
+
+@Pure
+def size1(n: Node) -> int:
+    Requires(tree(n))
+    Decreases(tree(n))
+    if Unfolding(tree(n), n.next) is None:
+        return 1
+    return 1 + Unfolding(tree(n), size1(n.next))
+
+
+@Pure
+def size2(n: Node) -> int:
+    Requires(tree(n))
+    Decreases(tree(n))
+    if Unfolding(tree(n), n.next) is None:
+        return 1
+    #:: ExpectedOutput(termination.failed:tuple.false)
+    return 1 + size2(n)