From fabb8dc72717a7d48690bad50713f42f3038c22a Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Thu, 25 Jan 2024 06:52:08 -0500 Subject: [PATCH 1/2] Abstract predicates --- .../translators/contract.py | 6 +++ .../translators/predicate.py | 37 ++++++++++++------- .../translation/test_abstract_pred_1.py | 17 +++++++++ .../translation/test_abstract_pred_2.py | 16 ++++++++ .../translation/test_abstract_pred_3.py | 15 ++++++++ .../translation/test_abstract_pred_4.py | 16 ++++++++ .../translation/test_abstract_pred_5.py | 19 ++++++++++ .../verification/test_predicate_abstract.py | 33 +++++++++++++++++ 8 files changed, 145 insertions(+), 14 deletions(-) create mode 100644 tests/functional/translation/test_abstract_pred_1.py create mode 100644 tests/functional/translation/test_abstract_pred_2.py create mode 100644 tests/functional/translation/test_abstract_pred_3.py create mode 100644 tests/functional/translation/test_abstract_pred_4.py create mode 100644 tests/functional/translation/test_abstract_pred_5.py create mode 100644 tests/functional/verification/test_predicate_abstract.py diff --git a/src/nagini_translation/translators/contract.py b/src/nagini_translation/translators/contract.py index 42f08a0f..455f00d3 100644 --- a/src/nagini_translation/translators/contract.py +++ b/src/nagini_translation/translators/contract.py @@ -414,6 +414,8 @@ def translate_fold(self, node: ast.Call, ctx: Context) -> StmtsAndExpr: if (target_pred and (not isinstance(target_pred, PythonMethod) or not target_pred.predicate)): raise InvalidProgramException(node, 'invalid.contract.call') + if target_pred and target_pred.contract_only: + raise InvalidProgramException(node, 'abstract.predicate.fold') pred_stmt, pred = self.translate_expr(node.args[0], ctx, self.viper.Bool, True) if self._is_family_fold(node): @@ -473,6 +475,8 @@ def translate_unfold(self, node: ast.Call, ctx: Context) -> StmtsAndExpr: if (target_pred and (not isinstance(target_pred, PythonMethod) or not target_pred.predicate)): raise InvalidProgramException(node, 'invalid.contract.call') + if target_pred and target_pred.contract_only: + raise InvalidProgramException(node, 'abstract.predicate.fold') pred_stmt, pred = self.translate_expr(node.args[0], ctx, self.viper.Bool, True) if self._is_family_fold(node): @@ -502,6 +506,8 @@ def translate_unfolding(self, node: ast.Call, ctx: Context, if (target_pred and (not isinstance(target_pred, PythonMethod) or not target_pred.predicate)): raise InvalidProgramException(node, 'invalid.contract.call') + if target_pred and target_pred.contract_only: + raise InvalidProgramException(node, 'abstract.predicate.fold') pred_stmt, pred = self.translate_expr(node.args[0], ctx, self.viper.Bool, True) diff --git a/src/nagini_translation/translators/predicate.py b/src/nagini_translation/translators/predicate.py index b56fe2e3..62a09315 100644 --- a/src/nagini_translation/translators/predicate.py +++ b/src/nagini_translation/translators/predicate.py @@ -41,18 +41,21 @@ def translate_predicate(self, pred: PythonMethod, raise InvalidProgramException(pred.node, 'invalid.predicate') - content = pred.node.body[0] - if isinstance(content, ast.Return): - content = content.value - stmt, body = self.translate_expr( - content, - ctx, impure=True, - target_type=self.viper.Bool) - if stmt: - raise InvalidProgramException(pred.node, - 'invalid.predicate') - body = self.viper.And(arg_types, body, self.no_position(ctx), - self.no_info(ctx)) + if pred.contract_only: + body = None + else: + content = pred.node.body[0] + if isinstance(content, ast.Return): + content = content.value + stmt, body = self.translate_expr( + content, + ctx, impure=True, + target_type=self.viper.Bool) + if stmt: + raise InvalidProgramException(pred.node, + 'invalid.predicate') + body = self.viper.And(arg_types, body, self.no_position(ctx), + self.no_info(ctx)) ctx.current_function = None return self.viper.Predicate(pred.sil_name, args, body, self.to_position(pred.node, ctx), @@ -70,6 +73,8 @@ def translate_predicate_family(self, root: PythonMethod, for pred in preds: value = {pred.overrides} if pred.overrides else set() dependencies[pred] = value + if pred.contract_only != root.contract_only: + raise InvalidProgramException(pred.node, 'partially.abstract.predicate.family') sorted = toposort_flatten(dependencies, False) name = root.sil_name @@ -90,6 +95,9 @@ def translate_predicate_family(self, root: PythonMethod, body = None assert not ctx.var_aliases for instance in sorted: + if root.contract_only: + # do not generate any body + continue ctx.var_aliases = {} assert not ctx.current_function if instance.type.name != BOOL_TYPE: @@ -155,7 +163,7 @@ def translate_predicate_family(self, root: PythonMethod, self.viper.MethodCall(self_frame_method_name, [], [], self.to_position(root.node, ctx), no_info) root_pos = self.to_position(root.node, ctx) all_preds = [] - if not (root.name == 'invariant' and root.cls.name == 'Lock'): + if not root.contract_only and not (root.name == 'invariant' and root.cls.name == 'Lock'): root_pos_with_rule = self.to_position(root.node, ctx, rules=rules.PRED_FAM_FOLD_UNKNOWN_RECEIVER) rest_pred_name = root.module.get_fresh_name(root.name + '_abstract_rest') rest_pred = self.viper.Predicate(rest_pred_name, args, None, root_pos, no_info) @@ -169,7 +177,8 @@ def translate_predicate_family(self, root: PythonMethod, root_pos_with_rule, no_info), root_pos_with_rule, no_info) ctx.var_aliases = {} - body = self.viper.And(arg_types, body, root_pos, no_info) + if not root.contract_only: + body = self.viper.And(arg_types, body, root_pos, no_info) family_pred = self.viper.Predicate(name, args, body, root_pos, no_info) all_preds.append(family_pred) return all_preds, self_framing_check_methods diff --git a/tests/functional/translation/test_abstract_pred_1.py b/tests/functional/translation/test_abstract_pred_1.py new file mode 100644 index 00000000..5b9cd6ce --- /dev/null +++ b/tests/functional/translation/test_abstract_pred_1.py @@ -0,0 +1,17 @@ +from nagini_contracts.contracts import * + +class MyClass: + def __init__(self) -> None: + pass + +@Predicate +@ContractOnly +def huh(mc: MyClass) -> bool: + return True + +@Pure +def huhFunc(mc: MyClass) -> int: + Requires(huh(mc)) + Ensures(Result() > 0) + #:: ExpectedOutput(invalid.program:abstract.predicate.fold) + return Unfolding(huh(mc), 6) diff --git a/tests/functional/translation/test_abstract_pred_2.py b/tests/functional/translation/test_abstract_pred_2.py new file mode 100644 index 00000000..871b30c7 --- /dev/null +++ b/tests/functional/translation/test_abstract_pred_2.py @@ -0,0 +1,16 @@ +from nagini_contracts.contracts import * + +class MyClass: + def __init__(self) -> None: + pass + +@Predicate +@ContractOnly +def huh(mc: MyClass) -> bool: + return True + +def huhFunc(mc: MyClass) -> int: + Requires(huh(mc)) + Ensures(Result() > 0) + #:: ExpectedOutput(invalid.program:abstract.predicate.fold) + return Unfold(huh(mc)) diff --git a/tests/functional/translation/test_abstract_pred_3.py b/tests/functional/translation/test_abstract_pred_3.py new file mode 100644 index 00000000..f6f41fef --- /dev/null +++ b/tests/functional/translation/test_abstract_pred_3.py @@ -0,0 +1,15 @@ +from nagini_contracts.contracts import * + +class MyClass: + def __init__(self) -> None: + pass + +@Predicate +@ContractOnly +def huh(mc: MyClass) -> bool: + return True + +def huhFunc(mc: MyClass) -> int: + Ensures(Result() > 0) + #:: ExpectedOutput(invalid.program:abstract.predicate.fold) + return Fold(huh(mc)) diff --git a/tests/functional/translation/test_abstract_pred_4.py b/tests/functional/translation/test_abstract_pred_4.py new file mode 100644 index 00000000..b2d3a6d0 --- /dev/null +++ b/tests/functional/translation/test_abstract_pred_4.py @@ -0,0 +1,16 @@ +from nagini_contracts.contracts import * + +class MyClass: + def __init__(self) -> None: + pass + + @Predicate + @ContractOnly + def huh(self) -> bool: + return True + + +def huhFunc(mc: MyClass) -> int: + Ensures(Result() > 0) + #:: ExpectedOutput(invalid.program:abstract.predicate.fold) + return Fold(mc.huh()) diff --git a/tests/functional/translation/test_abstract_pred_5.py b/tests/functional/translation/test_abstract_pred_5.py new file mode 100644 index 00000000..b0a17426 --- /dev/null +++ b/tests/functional/translation/test_abstract_pred_5.py @@ -0,0 +1,19 @@ +from nagini_contracts.contracts import * + + +class MyClass: + def __init__(self) -> None: + self.x = 1 + + @Predicate + @ContractOnly + def myHuh(self) -> bool: + return self.x > 2 + + +class MySubClass(MyClass): + + @Predicate #:: ExpectedOutput(invalid.program:partially.abstract.predicate.family) + def myHuh(self) -> bool: + return self.x > 4 + diff --git a/tests/functional/verification/test_predicate_abstract.py b/tests/functional/verification/test_predicate_abstract.py new file mode 100644 index 00000000..f6f7794e --- /dev/null +++ b/tests/functional/verification/test_predicate_abstract.py @@ -0,0 +1,33 @@ +from nagini_contracts.contracts import * + + +class MyClass: + def __init__(self) -> None: + self.x = 1 + + @Predicate + @ContractOnly + def myHuh(self) -> bool: + return self.x > 2 + + +class MySubClass(MyClass): + + @Predicate + @ContractOnly + def myHuh(self) -> bool: + return self.x > 4 + + +@Predicate +@ContractOnly +def huh(mc: MyClass) -> bool: + return mc.x > 6 + + +@Pure +@ContractOnly +def huhFunc(mc: MyClass) -> int: + Requires(huh(mc)) + Ensures(Result() > 0) + return Unfolding(huh(mc), 6) From 12f52b96fe1c2dc98368e965a89c326a1422e42d Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Thu, 25 Jan 2024 08:03:46 -0500 Subject: [PATCH 2/2] Fixing tests --- src/nagini_translation/analyzer.py | 2 ++ tests/functional/translation/test_abstract_pred_2.py | 3 ++- tests/functional/translation/test_abstract_pred_3.py | 3 ++- tests/functional/translation/test_abstract_pred_4.py | 3 ++- 4 files changed, 8 insertions(+), 3 deletions(-) diff --git a/src/nagini_translation/analyzer.py b/src/nagini_translation/analyzer.py index b5c6f064..fe4e054c 100644 --- a/src/nagini_translation/analyzer.py +++ b/src/nagini_translation/analyzer.py @@ -674,6 +674,8 @@ def visit_FunctionDef(self, node: ast.FunctionDef) -> None: func.method_type = MethodType.class_method self.current_class._has_classmethod = True func.predicate = self.is_predicate(node) + if func.predicate: + func.contract_only = self.is_declared_contract_only(node) if self.is_all_low(node): self.has_all_low = True func.all_low = True diff --git a/tests/functional/translation/test_abstract_pred_2.py b/tests/functional/translation/test_abstract_pred_2.py index 871b30c7..54adc5f9 100644 --- a/tests/functional/translation/test_abstract_pred_2.py +++ b/tests/functional/translation/test_abstract_pred_2.py @@ -13,4 +13,5 @@ def huhFunc(mc: MyClass) -> int: Requires(huh(mc)) Ensures(Result() > 0) #:: ExpectedOutput(invalid.program:abstract.predicate.fold) - return Unfold(huh(mc)) + Unfold(huh(mc)) + return 3 diff --git a/tests/functional/translation/test_abstract_pred_3.py b/tests/functional/translation/test_abstract_pred_3.py index f6f41fef..61954aec 100644 --- a/tests/functional/translation/test_abstract_pred_3.py +++ b/tests/functional/translation/test_abstract_pred_3.py @@ -12,4 +12,5 @@ def huh(mc: MyClass) -> bool: def huhFunc(mc: MyClass) -> int: Ensures(Result() > 0) #:: ExpectedOutput(invalid.program:abstract.predicate.fold) - return Fold(huh(mc)) + Fold(huh(mc)) + return 4 diff --git a/tests/functional/translation/test_abstract_pred_4.py b/tests/functional/translation/test_abstract_pred_4.py index b2d3a6d0..d5b4ac44 100644 --- a/tests/functional/translation/test_abstract_pred_4.py +++ b/tests/functional/translation/test_abstract_pred_4.py @@ -13,4 +13,5 @@ def huh(self) -> bool: def huhFunc(mc: MyClass) -> int: Ensures(Result() > 0) #:: ExpectedOutput(invalid.program:abstract.predicate.fold) - return Fold(mc.huh()) + Fold(mc.huh()) + return 4