From d95e0dadcf9cf3b0f6b19660b0462982db607b19 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Sun, 27 Aug 2023 12:39:15 +0200 Subject: [PATCH] Version bump, decreases clauses with predicates --- setup.py | 4 +-- src/nagini_translation/lib/errors/messages.py | 2 ++ src/nagini_translation/lib/viper_ast.py | 4 +++ src/nagini_translation/resources/all.sil | 1 + src/nagini_translation/sif/resources/all.sil | 2 ++ src/nagini_translation/translators/method.py | 10 +++++- src/nagini_translation/verifier.py | 8 ++++- .../verification/examples/iap_bst.py | 1 + .../functional/verification/test_decreases.py | 35 ++++++++++++++++++- 9 files changed, 62 insertions(+), 5 deletions(-) diff --git a/setup.py b/setup.py index 77c45ff29..07b13729a 100644 --- a/setup.py +++ b/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='viper@inf.ethz.ch', license='MPL-2.0', diff --git a/src/nagini_translation/lib/errors/messages.py b/src/nagini_translation/lib/errors/messages.py index 22afb9190..74220a5d8 100644 --- a/src/nagini_translation/lib/errors/messages.py +++ b/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 = { diff --git a/src/nagini_translation/lib/viper_ast.py b/src/nagini_translation/lib/viper_ast.py index 28f42842c..96b17fd7b 100644 --- a/src/nagini_translation/lib/viper_ast.py +++ b/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) diff --git a/src/nagini_translation/resources/all.sil b/src/nagini_translation/resources/all.sil index a61f76d7f..402499295 100644 --- a/src/nagini_translation/resources/all.sil +++ b/src/nagini_translation/resources/all.sil @@ -6,6 +6,7 @@ */ import +import domain SIFDomain[T] { function Low(x: T): Bool diff --git a/src/nagini_translation/sif/resources/all.sil b/src/nagini_translation/sif/resources/all.sil index 58d47c9de..bfda3a221 100644 --- a/src/nagini_translation/sif/resources/all.sil +++ b/src/nagini_translation/sif/resources/all.sil @@ -6,6 +6,8 @@ */ import +import + domain SIFDomain[T] { function Low(x: T): Bool diff --git a/src/nagini_translation/translators/method.py b/src/nagini_translation/translators/method.py index 7f9f8a0a2..4ad734907 100644 --- a/src/nagini_translation/translators/method.py +++ b/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') diff --git a/src/nagini_translation/verifier.py b/src/nagini_translation/verifier.py index a90a5e33d..abfa64009 100644 --- a/src/nagini_translation/verifier.py +++ b/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) diff --git a/tests/functional/verification/examples/iap_bst.py b/tests/functional/verification/examples/iap_bst.py index 345348248..d727bfe83 100644 --- a/tests/functional/verification/examples/iap_bst.py +++ b/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 diff --git a/tests/functional/verification/test_decreases.py b/tests/functional/verification/test_decreases.py index 05e1874f3..95027f0ea 100644 --- a/tests/functional/verification/test_decreases.py +++ b/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) \ No newline at end of file + 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)