From 90d942242d1d91134914f378ce7bd2cd755c3fba Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Tue, 22 Aug 2023 20:14:41 +0200 Subject: [PATCH] Tests for old issues and some small fixes --- .../resources/preamble.index | 3 +- src/nagini_translation/translators/program.py | 7 +++ tests/functional/verification/issues/00024.py | 7 +++ tests/functional/verification/issues/00052.py | 62 +++++++++++++++++++ tests/functional/verification/issues/00074.py | 48 ++++++++++++++ tests/functional/verification/issues/00119.py | 18 ++++++ tests/functional/verification/issues/00150.py | 31 ++++++++++ 7 files changed, 175 insertions(+), 1 deletion(-) create mode 100644 tests/functional/verification/issues/00024.py create mode 100644 tests/functional/verification/issues/00052.py create mode 100644 tests/functional/verification/issues/00074.py create mode 100644 tests/functional/verification/issues/00119.py create mode 100644 tests/functional/verification/issues/00150.py diff --git a/src/nagini_translation/resources/preamble.index b/src/nagini_translation/resources/preamble.index index be03978a..476adc66 100644 --- a/src/nagini_translation/resources/preamble.index +++ b/src/nagini_translation/resources/preamble.index @@ -542,7 +542,8 @@ }, "__len__": { "args": ["tuple"], - "type": "__prim__int" + "type": "__prim__int", + "requires": ["__val__", "args"] }, "__val__": { "args": ["tuple"], diff --git a/src/nagini_translation/translators/program.py b/src/nagini_translation/translators/program.py index 0f096f2b..f2d25da7 100644 --- a/src/nagini_translation/translators/program.py +++ b/src/nagini_translation/translators/program.py @@ -296,6 +296,13 @@ def create_override_check(self, method: PythonMethod, params.append(method.overrides.args[arg].decl) args.append(method.overrides.args[arg].ref()) + if method.overrides.var_arg: + params.append(method.overrides.var_arg.decl) + args.append(method.overrides.var_arg.ref()) + if method.overrides.kw_arg: + params.append(method.overrides.kw_arg.decl) + args.append(method.overrides.kw_arg.ref()) + self.bind_type_vars(method.overrides, ctx) mname = ctx.module.get_fresh_name(method.sil_name + '_override_check') diff --git a/tests/functional/verification/issues/00024.py b/tests/functional/verification/issues/00024.py new file mode 100644 index 00000000..1e8f7957 --- /dev/null +++ b/tests/functional/verification/issues/00024.py @@ -0,0 +1,7 @@ +# Any copyright is dedicated to the Public Domain. +# http://creativecommons.org/publicdomain/zero/1.0/ + + +def bla() -> None: + #:: ExpectedOutput(type.error:Cannot resolve name "a" (possible cyclic definition)) + a = a \ No newline at end of file diff --git a/tests/functional/verification/issues/00052.py b/tests/functional/verification/issues/00052.py new file mode 100644 index 00000000..4f5b1fdd --- /dev/null +++ b/tests/functional/verification/issues/00052.py @@ -0,0 +1,62 @@ +# Any copyright is dedicated to the Public Domain. +# http://creativecommons.org/publicdomain/zero/1.0/ + + +from nagini_contracts.contracts import ( + Acc, + Assert, + Requires, + Invariant, + Implies, + Predicate, + Fold, + Ensures, + Unfold, + Unfolding, +) +from nagini_contracts.obligations import * + + +class Tree: + + @Predicate + def valid(self) -> bool: + return (Acc(self.left) and Acc(self.right) and + Acc(self.height, 1/10) and self.height >= 0 and + Implies( + self.left is not None, + self.left.valid() and Acc(self.left.height, 1/10) and + self.left.height == self.height - 1) and + Implies( + self.right is not None, + self.right.valid() and Acc(self.right.height, 1/10) and + self.right.height == self.height - 1) + ) + + def __init__(self, left: 'Tree', right: 'Tree', height: int) -> None: + Requires(left.valid() and Acc(left.height, 1/10) and + left.height == height-1) + Requires(right.valid() and Acc(right.height, 1/10) and + right.height == height-1) + Requires(height >= 0) + Ensures(self.valid()) + self.left = left # type: Tree + self.right = right # type: Tree + self.height = height # type: int + Fold(self.valid()) + + + def work(self, call_height: int) -> None: + Requires(self.valid()) + Requires(call_height >= 0) + Requires(Unfolding(self.valid(), self.height == call_height)) + Requires(MustTerminate(call_height + 1)) + Ensures(self.valid()) + + if call_height > 0: + Unfold(self.valid()) + if self.left is not None: + self.left.work(call_height - 1) + if self.right is not None: + self.right.work(call_height - 1) + Fold(self.valid()) \ No newline at end of file diff --git a/tests/functional/verification/issues/00074.py b/tests/functional/verification/issues/00074.py new file mode 100644 index 00000000..5496fb73 --- /dev/null +++ b/tests/functional/verification/issues/00074.py @@ -0,0 +1,48 @@ +# Any copyright is dedicated to the Public Domain. +# http://creativecommons.org/publicdomain/zero/1.0/ + + +from typing import Tuple, Dict +from nagini_contracts.contracts import Requires, Ensures, Result + +class Super: + + #:: Label(L1) + def foo(self, *args: Tuple[int]) -> int: + Requires(len(args) > 3) + Ensures(Result() > 2) + return 5 + + #:: Label(L2) + def bar(self, **kwargs: Dict[str, int]) -> int: + Requires(len(kwargs) > 3) + Ensures(Result() > 2) + return 5 + + +class Sub(Super): + + def foo(self, *args: Tuple[int]) -> int: + Requires(len(args) > 2) + Ensures(Result() > 4) + return 5 + + def bar(self, **kwargs: Dict[str, int]) -> int: + Requires(len(kwargs) > 2) + Ensures(Result() > 4) + return 5 + + +class Sub2(Super): + + def foo(self, *args: Tuple[int]) -> int: + Requires(len(args) > 2) + #:: ExpectedOutput(postcondition.violated:assertion.false,L1) + Ensures(Result() > 0) + return 5 + + def bar(self, **kwargs: Dict[str, int]) -> int: + Requires(len(kwargs) > 2) + #:: ExpectedOutput(postcondition.violated:assertion.false,L2) + Ensures(Result() > 0) + return 5 diff --git a/tests/functional/verification/issues/00119.py b/tests/functional/verification/issues/00119.py new file mode 100644 index 00000000..7ec3b7c2 --- /dev/null +++ b/tests/functional/verification/issues/00119.py @@ -0,0 +1,18 @@ +# Any copyright is dedicated to the Public Domain. +# http://creativecommons.org/publicdomain/zero/1.0/ + +from nagini_contracts.contracts import * + +class A: + def __init__(self, value: int) -> None: + self.value = value # type: int + Ensures(Acc(self.value) and self.value is value) + + +def test() -> None: + Assert(A(5).value == 5) + + +def test2() -> None: + #:: ExpectedOutput(assert.failed:assertion.false) + Assert(A(3).value == 5) \ No newline at end of file diff --git a/tests/functional/verification/issues/00150.py b/tests/functional/verification/issues/00150.py new file mode 100644 index 00000000..bc2d4b48 --- /dev/null +++ b/tests/functional/verification/issues/00150.py @@ -0,0 +1,31 @@ +# Any copyright is dedicated to the Public Domain. +# http://creativecommons.org/publicdomain/zero/1.0/ + + +from typing import Optional, List, Tuple +from nagini_contracts.contracts import * + +class Node: + def __init__(self, function_name: str, children:List['Node']) -> None: + self.function_name = function_name # type: str + self.children = children # type: List['Node'] + Ensures(Acc(self.function_name) and self.function_name is function_name and + Acc(self.children) and self.children is children) + +@Pure +def can_node_be_compressed(marked_execution_tree: 'Node') -> int: + """Searches for the longest compression possible. Returns: + - int: number of nodes that can be compressed. 0 if None""" + Requires(Acc(marked_execution_tree.children)) + Requires(Acc(list_pred(marked_execution_tree.children))) + Requires(Forall(int, lambda i: Implies(i >= 0 and i < len(marked_execution_tree.children), + Acc(marked_execution_tree.children[i].function_name)))) + Requires(Acc(marked_execution_tree.function_name)) + #:: ExpectedOutput(postcondition.violdated:assertion.false) + Ensures(Implies(len(marked_execution_tree.children) != 1, Result() == 0)) + Ensures(Result() == 0) + if len(marked_execution_tree.children) != 1: + return 1 + if marked_execution_tree.children[0].function_name != marked_execution_tree.function_name: + return 0 + return can_node_be_compressed(marked_execution_tree.children[0]) + 1 \ No newline at end of file