Refactor is_spark's API

Split into two public properties, `has_spark_mode_on` and `is_subject_to_proof`. Because we deemed that the initial API was misleading.
AdaCore · Sep 14, 2023 · 2ab3005 · 2ab3005
1 parent c81b39f
commit 2ab3005
Show file tree

Hide file tree

Showing 17 changed files with 115 additions and 64 deletions.
diff --git a/ada/ast.py b/ada/ast.py
@@ -1889,6 +1889,57 @@ class BasicDecl(AdaNode):
     associates a name with a language entity, for example a type or a variable.
     """
 
+    @langkit_property(return_type=Bool, memoized=True)
+    def is_spark_impl(include_skip_proof_annotations=T.Bool):
+        """
+        Main implementation for the properties ``has_spark_mode_on`` and
+        ``is_subject_to_proof``.
+
+        This property will determine if the decl or body has SPARK mode on,
+        with some special paths for bodies.
+
+        It will also, for bodies only, determine whether there are
+        ``Skip_Proof`` annotations, if the parameter
+        ``include_skip_proof_annotations`` is True.
+        """
+        return Cond(
+            # For bodies, and if `include_skip_proof_annotations` is True,
+            # check `Skip_Proof`/`Skip_Flow_And_Proof`.
+            include_skip_proof_annotations & Not(
+                Entity.cast(BaseSubpBody)._.gnatprove_annotations.find(
+                    lambda a: a.cast(Name).name_symbol.any_of(
+                        'Skip_Proof', 'Skip_Flow_And_Proof'
+                    )
+                ).is_null
+            ),
+            False,
+
+            # Check for the `SPARK_Mode` aspect. Only consider explicit `On`
+            Entity.has_aspect("SPARK_Mode"),
+            Entity.get_aspect("SPARK_Mode").value.then(
+                lambda mode: mode.cast(T.Name).name_is("On"),
+                # `SPARK_Mode` without value is `On` by default
+                default_val=True
+            ),
+
+            # If there is no aspect on this subprogram, it's `On` if the
+            # enclosing subprogram or declarative region is `On`.
+            If(
+                Entity.previous_part_for_decl._.is_a(T.BodyStub),
+                Entity.previous_part_for_decl,
+                Entity
+            ).declarative_scope.as_entity._.is_spark,
+            True,
+
+            # Finally, check for configuration pragmas. This configuration
+            # pragma is of the form `pragma SPARK_Mode [On|Off|Auto]`.
+            Entity.enclosing_compilation_unit.spark_config_pragma.then(
+                lambda p: p.spark_mode_is_on,
+                # No configuration pragma were found
+                default_val=False
+            )
+        )
+
     @langkit_property(return_type=Equation, dynamic_vars=[origin])
     def subp_constrain_prefix(prefix=T.Expr):
         """
@@ -9721,6 +9772,17 @@ class BasicSubpDecl(BasicDecl):
         """
     )
 
+    @langkit_property(return_type=Bool, public=True)
+    def has_spark_mode_on():
+        """
+        Returns whether this subprogram has explicitly been set as having
+        ``Spark_Mode`` to ``On``, directly or indirectly.
+
+        Doesn't include subprograms that can be inferred by GNATprove as being
+        SPARK.
+        """
+        return Entity.is_spark_impl(include_skip_proof_annotations=False)
+
     @langkit_property(dynamic_vars=[default_imprecise_fallback()])
     def get_body_in_env(env=T.LexicalEnv):
         elements = Var(
@@ -20715,52 +20777,24 @@ def gnatprove_annotations():
 
         return aspects.concat(pragmas).concat(enclosing_subp_annotations)
 
-    @langkit_property(public=True, return_type=Bool, memoized=True)
-    def is_spark(include_skip_proof_annotations=(T.Bool, True)):
+    @langkit_property(return_type=Bool, public=True)
+    def is_subject_to_proof():
         """
-        Return whether this subprogram body is in SPARK or not, i.e. return
-        whether SPARK proofs will be applied to that subprogram or not.
+        Returns whether this subprogram body is subject to proof in the context
+        of the SPARK/GNATprove tools.
         """
-        return Cond(
-            # If `Skip_Proof` or `Skip_Flow_And_Proof` has been specified, this
-            # is not in SPARK.
-            include_skip_proof_annotations & Not(
-                Entity.gnatprove_annotations.find(
-                    lambda a: a.cast(Name).name_symbol.any_of(
-                        'Skip_Proof', 'Skip_Flow_And_Proof'
-                    )
-                ).is_null
-            ),
-            False,
+        return Entity.is_spark_impl(include_skip_proof_annotations=True)
 
-            # Else, check for the `SPARK_Mode` aspect. For subprogram bodies,
-            # only the mode `On` turns proofs on. Any other values: `Off` and
-            # `Auto` turn them off. Of course, if the aspect isn't specified at
-            # all, the proofs are off too.
-            Entity.has_aspect("SPARK_Mode"),
-            Entity.get_aspect("SPARK_Mode").value.then(
-                lambda mode: mode.cast(T.Name).name_is("On"),
-                # `SPARK_Mode` without value is `On` by default
-                default_val=True
-            ),
-
-            # If there is no aspect on this subprogram, it's `On` if the
-            # enclosing subprogram or declarative region is `On`.
-            If(
-                Entity.subp_previous_part._.is_a(T.BodyStub),
-                Entity.subp_previous_part,
-                Entity
-            ).declarative_scope.as_entity._.is_spark,
-            True,
+    @langkit_property(return_type=Bool, public=True)
+    def has_spark_mode_on():
+        """
+        Returns whether this subprogram has explicitly been set as having
+        ``Spark_Mode`` to ``On``, directly or indirectly.
 
-            # Finally, check for configuration pragmas. This configuration
-            # pragma is of the form `pragma SPARK_Mode [On|Off|Auto]`.
-            Entity.enclosing_compilation_unit.spark_config_pragma.then(
-                lambda p: p.spark_mode_is_on,
-                # No configuration pragma were found
-                default_val=False
-            )
-        )
+        Doesn't include subprograms that can be inferred by GNATprove as being
+        SPARK.
+        """
+        return Entity.is_spark_impl(include_skip_proof_annotations=False)
 
 
 class ExprFunction(BaseSubpBody):

diff --git a/testsuite/tests/properties/is_spark/aspect/test.py b/testsuite/tests/properties/is_spark/aspect/test.py
@@ -17,6 +17,6 @@
         for subprogram in subprograms:
             print("Subprogram {} is {}".format(
                 subprogram,
-                "analyzed" if subprogram.p_is_spark() else "skipped"
+                "analyzed" if subprogram.p_is_subject_to_proof else "skipped"
             ))
         print('')
diff --git a/testsuite/tests/properties/is_spark/configuration_pragma_1/test.out b/testsuite/tests/properties/is_spark/configuration_pragma_1/test.out
@@ -6,7 +6,7 @@ Subprogram <NullSubpDecl ["S"] test.adb:5:4-5:24> is skipped
 Subprogram <NullSubpDecl ["T"] test.adb:6:4-6:47> is skipped
 Subprogram <NullSubpDecl ["U"] test.adb:7:4-7:46> is analyzed
 
-=== Re-analysing unit (ignoring Skip_Proof annotations):  <AnalysisUnit 'test.adb'> ===
+=== Re-analysing unit calling has_spark_mode:  <AnalysisUnit 'test.adb'> ===
 Subprogram <NullSubpDecl ["P"] test.adb:2:4-2:24> is analyzed
 Subprogram <NullSubpDecl ["Q"] test.adb:3:4-3:24> is analyzed
 Subprogram <NullSubpDecl ["R"] test.adb:4:4-4:24> is analyzed

diff --git a/testsuite/tests/properties/is_spark/configuration_pragma_1/test.py b/testsuite/tests/properties/is_spark/configuration_pragma_1/test.py
@@ -17,14 +17,14 @@
         for subprogram in subprograms:
             print("Subprogram {} is {}".format(
                 subprogram,
-                "analyzed" if subprogram.p_is_spark() else "skipped"
+                "analyzed" if subprogram.p_is_subject_to_proof else "skipped"
             ))
         print('')
-        print('=== Re-analysing unit (ignoring Skip_Proof annotations): ',
+        print('=== Re-analysing unit calling has_spark_mode: ',
               unit, '===')
         for subprogram in subprograms:
             print("Subprogram {} is {}".format(
                 subprogram,
-                "analyzed" if subprogram.p_is_spark(False) else "skipped"
+                "analyzed" if subprogram.p_has_spark_mode_on else "skipped"
             ))
         print('')
diff --git a/testsuite/tests/properties/is_spark/configuration_pragma_2/test.py b/testsuite/tests/properties/is_spark/configuration_pragma_2/test.py
@@ -17,6 +17,6 @@
         for subprogram in subprograms:
             print("Subprogram {} is {}".format(
                 subprogram,
-                "analyzed" if subprogram.p_is_spark() else "skipped"
+                "analyzed" if subprogram.p_is_subject_to_proof else "skipped"
             ))
         print('')
diff --git a/testsuite/tests/properties/is_spark/configuration_pragma_3/test.py b/testsuite/tests/properties/is_spark/configuration_pragma_3/test.py
@@ -17,6 +17,6 @@
         for subprogram in subprograms:
             print("Subprogram {} is {}".format(
                 subprogram,
-                "analyzed" if subprogram.p_is_spark() else "skipped"
+                "analyzed" if subprogram.p_is_subject_to_proof else "skipped"
             ))
         print('')
diff --git a/testsuite/tests/properties/is_spark/configuration_pragma_4/test.py b/testsuite/tests/properties/is_spark/configuration_pragma_4/test.py
@@ -17,6 +17,6 @@
         for subprogram in subprograms:
             print("Subprogram {} is {}".format(
                 subprogram,
-                "analyzed" if subprogram.p_is_spark() else "skipped"
+                "analyzed" if subprogram.p_is_subject_to_proof else "skipped"
             ))
         print('')
diff --git a/testsuite/tests/properties/is_spark/configuration_pragma_5/test.py b/testsuite/tests/properties/is_spark/configuration_pragma_5/test.py
@@ -17,6 +17,6 @@
         for subprogram in subprograms:
             print("Subprogram {} is {}".format(
                 subprogram,
-                "analyzed" if subprogram.p_is_spark() else "skipped"
+                "analyzed" if subprogram.p_is_subject_to_proof else "skipped"
             ))
         print('')
diff --git a/testsuite/tests/properties/is_spark/mixed_pragma_and_aspect/test.py b/testsuite/tests/properties/is_spark/mixed_pragma_and_aspect/test.py
@@ -17,6 +17,6 @@
         for subprogram in subprograms:
             print("Subprogram {} is {}".format(
                 subprogram,
-                "analyzed" if subprogram.p_is_spark() else "skipped"
+                "analyzed" if subprogram.p_is_subject_to_proof else "skipped"
             ))
         print('')
diff --git a/testsuite/tests/properties/is_spark/pkg_private_and_body/test.py b/testsuite/tests/properties/is_spark/pkg_private_and_body/test.py
@@ -16,6 +16,6 @@
         for subprogram in subprograms:
             print("Subprogram {} is {}".format(
                 subprogram,
-                "analyzed" if subprogram.p_is_spark() else "skipped"
+                "analyzed" if subprogram.p_is_subject_to_proof else "skipped"
             ))
         print('')
diff --git a/testsuite/tests/properties/is_spark/pkg_private_and_body/test2.adb b/testsuite/tests/properties/is_spark/pkg_private_and_body/test2.adb
@@ -4,7 +4,7 @@ package body Test2 is
    pragma SPARK_Mode;
    function F10 return Boolean is (True);
    --% node.p_get_aspect("SPARK_Mode")
-   --% node.p_is_spark
+   --% node.p_is_subject_to_proof
 begin
    pragma SPARK_Mode (Off);
    function F20 return Boolean is (True);

diff --git a/testsuite/tests/properties/is_spark/pragma/test.py b/testsuite/tests/properties/is_spark/pragma/test.py
@@ -17,6 +17,6 @@
         for subprogram in subprograms:
             print("Subprogram {} is {}".format(
                 subprogram,
-                "analyzed" if subprogram.p_is_spark() else "skipped"
+                "analyzed" if subprogram.p_is_subject_to_proof else "skipped"
             ))
         print('')
diff --git a/testsuite/tests/properties/is_spark/skip_flow_and_proof/test.py b/testsuite/tests/properties/is_spark/skip_flow_and_proof/test.py
@@ -17,6 +17,6 @@
         for subprogram in subprograms:
             print("Subprogram {} is {}".format(
                 subprogram,
-                "analyzed" if subprogram.p_is_spark() else "skipped"
+                "analyzed" if subprogram.p_is_subject_to_proof else "skipped"
             ))
         print('')
diff --git a/testsuite/tests/properties/is_spark/skip_proof/test.py b/testsuite/tests/properties/is_spark/skip_proof/test.py
@@ -17,6 +17,6 @@
         for subprogram in subprograms:
             print("Subprogram {} is {}".format(
                 subprogram,
-                "analyzed" if subprogram.p_is_spark() else "skipped"
+                "analyzed" if subprogram.p_is_subject_to_proof else "skipped"
             ))
         print('')
diff --git a/testsuite/tests/properties/is_spark/skip_proof_library_level_subp/test.adb b/testsuite/tests/properties/is_spark/skip_proof_library_level_subp/test.adb
@@ -2,4 +2,4 @@ procedure Test is
 begin
    null;
 end Test;
---% node.p_is_spark()
+--% node.p_is_subject_to_proof
diff --git a/testsuite/tests/properties/is_spark/skip_proof_library_level_subp/test.out b/testsuite/tests/properties/is_spark/skip_proof_library_level_subp/test.out
@@ -1,5 +1,5 @@
 Working on node <SubpBody ["Test"] test.adb:1:1-4:10>
 =====================================================
 
-Eval 'node.p_is_spark()'
+Eval 'node.p_is_subject_to_proof'
 Result: False
diff --git a/user_manual/changes/libadalang/1016.yaml b/user_manual/changes/libadalang/1016.yaml
@@ -1,7 +1,24 @@
 type: new-feature
-title: New `is_spark` property on `BaseSubpBody`
+title: New SPARK related properties on subprograms
 description: |
-  This change introduces a new property on subprogram bodies (`BaseSubpBody`).
-  This property, named `is_spark` allows to determine if a given subprogram is
-  in SPARK or not.
-date: 2023-07-06
+
+  This change introduces new properties on subprogram decls & bodies:
+
+  .. code-block::
+
+     SubpBody.is_subject_to_proof()``:
+     """
+     Returns whether this subprogram body is subject to proof in the context of
+     the SPARK/GNATprove tools.
+     """
+
+     SubpDecl/SubpBody.has_spark_mode_on():
+     """
+     Returns whether this subprogram has explicitly been set as having
+     ``Spark_Mode`` to ``On``, directly or indirectly.
+
+     Doesn't include subprograms that can be inferred by GNATprove as being
+     SPARK.
+     """
+
+date: 2023-09-14