Merge pull request #163 from marcoeilers/abstract_predicates

Abstract predicates

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

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)

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

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)

tests/functional/translation/test_abstract_pred_2.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
+
+def huhFunc(mc: MyClass) -> int:
+    Requires(huh(mc))
+    Ensures(Result() > 0)
+    #:: ExpectedOutput(invalid.program:abstract.predicate.fold)
+    Unfold(huh(mc))
+    return 3

tests/functional/translation/test_abstract_pred_3.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:
+    Ensures(Result() > 0)
+    #:: ExpectedOutput(invalid.program:abstract.predicate.fold)
+    Fold(huh(mc))
+    return 4

tests/functional/translation/test_abstract_pred_4.py

@@ -0,0 +1,17 @@
+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)
+    Fold(mc.huh())
+    return 4

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
+

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)