From 2ab30058c4a967032fb990ec51b4d9c4a18a35e5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Rapha=C3=ABl=20AMIARD?= Date: Thu, 14 Sep 2023 10:39:32 +0200 Subject: [PATCH] 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. --- ada/ast.py | 118 +++++++++++------- .../tests/properties/is_spark/aspect/test.py | 2 +- .../is_spark/configuration_pragma_1/test.out | 2 +- .../is_spark/configuration_pragma_1/test.py | 6 +- .../is_spark/configuration_pragma_2/test.py | 2 +- .../is_spark/configuration_pragma_3/test.py | 2 +- .../is_spark/configuration_pragma_4/test.py | 2 +- .../is_spark/configuration_pragma_5/test.py | 2 +- .../is_spark/mixed_pragma_and_aspect/test.py | 2 +- .../is_spark/pkg_private_and_body/test.py | 2 +- .../is_spark/pkg_private_and_body/test2.adb | 2 +- .../tests/properties/is_spark/pragma/test.py | 2 +- .../is_spark/skip_flow_and_proof/test.py | 2 +- .../properties/is_spark/skip_proof/test.py | 2 +- .../skip_proof_library_level_subp/test.adb | 2 +- .../skip_proof_library_level_subp/test.out | 2 +- user_manual/changes/libadalang/1016.yaml | 27 +++- 17 files changed, 115 insertions(+), 64 deletions(-) diff --git a/ada/ast.py b/ada/ast.py index 940d63ba7..1c3c72d2b 100644 --- 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 index b2c577b35..b9fc629fb 100644 --- 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 index 135d885a8..14fb72bb3 100644 --- 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 is skipped Subprogram is skipped Subprogram is analyzed -=== Re-analysing unit (ignoring Skip_Proof annotations): === +=== Re-analysing unit calling has_spark_mode: === Subprogram is analyzed Subprogram is analyzed Subprogram 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 index 700152bf3..654c506d7 100644 --- 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 index 5c641fcbf..8c6ef896b 100644 --- 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 index 5c641fcbf..8c6ef896b 100644 --- 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 index b2c577b35..b9fc629fb 100644 --- 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 index a00ee4482..4d67cef34 100644 --- 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 index b2c577b35..b9fc629fb 100644 --- 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 index 6a8f9bdfa..b58748f02 100644 --- 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 index 1b55bd142..96779169e 100644 --- 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 index b2c577b35..b9fc629fb 100644 --- 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 index b2c577b35..b9fc629fb 100644 --- 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 index b2c577b35..b9fc629fb 100644 --- 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 index ad211722e..42fd655c1 100644 --- 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 index 0f2118aac..3ce7370cc 100644 --- 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 ===================================================== -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 index 732c22866..125ef071a 100644 --- 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