From 084f874ce09cc0370c79364f691458b2f3da6b3a Mon Sep 17 00:00:00 2001 From: AlexShefY Date: Wed, 18 Sep 2024 23:05:26 +0200 Subject: [PATCH] in case --- tests/test_nagini.py | 110 +++++++++++++++++- verified_cogen/experiments/incremental_run.py | 7 ++ verified_cogen/runners/languages/nagini.py | 3 +- verified_cogen/tools/verifier.py | 2 + 4 files changed, 120 insertions(+), 2 deletions(-) diff --git a/tests/test_nagini.py b/tests/test_nagini.py index 013a611..742a1b7 100644 --- a/tests/test_nagini.py +++ b/tests/test_nagini.py @@ -12,8 +12,10 @@ def test_nagini_generate(): def main(value: int) -> int: Requires(value >= 10) Ensures(Result() >= 20) + # impl-start Assert(value * 2 >= 20) # assert-line - return value * 2""" + return value * 2 + # impl-end""" ) assert nagini_lang.generate_validators(code) == dedent( """\ @@ -136,3 +138,109 @@ def is_prime(k : int) -> bool: d_2_i_ = (d_2_i_) + (1) return result""" ) + + +def test_nagini_generate1(): + nagini_lang = LanguageDatabase().get("nagini") + + code = dedent( + """\ + from typing import cast, List, Dict, Set, Optional, Union + from nagini_contracts.contracts import * + + @Pure + def lower(c : int) -> bool : + # impl-start + return ((0) <= (c)) and ((c) <= (25)) + # impl-end + + @Pure + def upper(c : int) -> bool : + # impl-start + return ((26) <= (c)) and ((c) <= (51)) + # impl-end + + @Pure + def alpha(c : int) -> bool : + # impl-start + return (lower(c)) or (upper(c)) + # impl-end + + @Pure + def flip__char(c : int) -> int : + # pre-conditions-start + Ensures(lower(c) == upper(Result())) + Ensures(upper(c) == lower(Result())) + # pre-conditions-end + + # impl-start + if lower(c): + return ((c) - (0)) + (26) + elif upper(c): + return ((c) + (0)) - (26) + elif True: + return c + # impl-end + + def flip__case(s : List[int]) -> List[int] : + # pre-conditions-start + Requires(Acc(list_pred(s))) + # pre-conditions-end + # post-conditions-start + Ensures(Acc(list_pred(s))) + Ensures(Acc(list_pred(Result()))) + Ensures((len(Result())) == (len(s))) + Ensures(Forall(int, lambda d_0_i_: (Implies(((0) <= (d_0_i_)) and ((d_0_i_) < (len(s))), lower((s)[d_0_i_]) == upper((Result())[d_0_i_]))))) + Ensures(Forall(int, lambda d_0_i_: (Implies(((0) <= (d_0_i_)) and ((d_0_i_) < (len(s))), upper((s)[d_0_i_]) == lower((Result())[d_0_i_]))))) + # post-conditions-end + + # impl-start + res = list([int(0)] * len(s)) # type : List[int] + i = int(0) # type : int + while i < len(s): + # invariants-start + Invariant(Acc(list_pred(s))) + Invariant(Acc(list_pred(res))) + Invariant(((0) <= (i)) and ((i) <= (len(s)))) + Invariant((len(res)) == (len(s))) + Invariant(Forall(int, lambda d_0_i_: (Implies(((0) <= (d_0_i_)) and ((d_0_i_) < (i)), lower((s)[d_0_i_]) == upper((res)[d_0_i_]))))) + Invariant(Forall(int, lambda d_0_i_: (Implies(((0) <= (d_0_i_)) and ((d_0_i_) < (i)), upper((s)[d_0_i_]) == lower((res)[d_0_i_]))))) + # invariants-end + res[i] = flip__char(s[i]) + i = i + 1 + return res + # impl-end +""" + ) + assert nagini_lang.generate_validators(code) == dedent( + """\ + def lower_valid(c : int) -> bool : + ret = lower(c) + return ret + def upper_valid(c : int) -> bool : + ret = upper(c) + return ret + def alpha_valid(c : int) -> bool : + ret = alpha(c) + return ret + def flip__char_valid(c : int) -> int : + # pre-conditions-start + Ensures(lower(c) == upper(Result())) + Ensures(upper(c) == lower(Result())) + # pre-conditions-end + ret = flip__char(c) + return ret + def flip__case_valid(s : List[int]) -> List[int] : + # pre-conditions-start + Requires(Acc(list_pred(s))) + # pre-conditions-end + # post-conditions-start + Ensures(Acc(list_pred(s))) + Ensures(Acc(list_pred(Result()))) + Ensures((len(Result())) == (len(s))) + Ensures(Forall(int, lambda d_0_i_: (Implies(((0) <= (d_0_i_)) and ((d_0_i_) < (len(s))), lower((s)[d_0_i_]) == upper((Result())[d_0_i_]))))) + Ensures(Forall(int, lambda d_0_i_: (Implies(((0) <= (d_0_i_)) and ((d_0_i_) < (len(s))), upper((s)[d_0_i_]) == lower((Result())[d_0_i_]))))) + # post-conditions-end + ret = flip__case(s) + return ret""" + ) \ No newline at end of file diff --git a/verified_cogen/experiments/incremental_run.py b/verified_cogen/experiments/incremental_run.py index ad2b2d8..eca5197 100644 --- a/verified_cogen/experiments/incremental_run.py +++ b/verified_cogen/experiments/incremental_run.py @@ -12,7 +12,14 @@ from verified_cogen.tools.modes import Mode from verified_cogen.tools.verifier import Verifier +import sys + logger = logging.getLogger(__name__) +handler = logging.StreamHandler(sys.stdout) + +formatter = logging.Formatter('%(asctime)s - %(levelname)s - %(message)s') +handler.setFormatter(formatter) +logger.addHandler(handler) def main(): diff --git a/verified_cogen/runners/languages/nagini.py b/verified_cogen/runners/languages/nagini.py index 76d3f03..e139e4d 100644 --- a/verified_cogen/runners/languages/nagini.py +++ b/verified_cogen/runners/languages/nagini.py @@ -16,7 +16,8 @@ class NaginiLanguage(GenericLanguage): def __init__(self): super().__init__( re.compile( - r"def\s+(\w+)\s*\((.*?)\)\s*->\s*(.*?):((?:\r\n|\r|\n) *(?:Requires|Ensures)\(.*\)(?:\r\n|\r|\n))*", + # r"def\s+(\w+)\s*\((.*?)\)\s*->\s*(.*?):((?:\r\n|\r|\n) *(?:Requires|Ensures)\(.*\)(?:\r\n|\r|\n))*", + r"def\s+(\w+)\s*\((.*?)\)\s*->\s*(.*?):(.*?(\r\n|\r|\n))\s+# impl-start", re.DOTALL, ), NAGINI_VALIDATOR_TEMPLATE, diff --git a/verified_cogen/tools/verifier.py b/verified_cogen/tools/verifier.py index 1873d13..dbe2011 100644 --- a/verified_cogen/tools/verifier.py +++ b/verified_cogen/tools/verifier.py @@ -2,6 +2,7 @@ import subprocess from pathlib import Path from typing import Optional +import os log = logging.getLogger(__name__) @@ -23,6 +24,7 @@ def verify(self, file_path: Path) -> Optional[tuple[bool, str, str]]: timeout=self.timeout, ) except subprocess.TimeoutExpired: + os.system("killall z3") return None return ( res.returncode == 0,