From addf50042dd0448f48f156dfb96fcde0e76944eb Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Laurent=20Th=C3=A9venoux?= Date: Tue, 12 Sep 2023 15:51:44 +0200 Subject: [PATCH] Fix `is_spark` property configuration pragma handling This change fixes a bug in the `is_spark` property where configuration pragmas were not handled correctly: a `SPARK_Mode` configuration pragma in a package specification only applies to the package specification and does not affect the body (and vice-versa). --- ada/ast.py | 26 ++++++++++++++----- .../is_spark/configuration_pragma_5/test.adb | 3 +++ .../is_spark/configuration_pragma_5/test.ads | 5 ++++ .../is_spark/configuration_pragma_5/test.out | 6 +++++ .../is_spark/configuration_pragma_5/test.py | 22 ++++++++++++++++ .../is_spark/configuration_pragma_5/test.yaml | 1 + .../configuration_pragma_5/test2-p.adb | 5 ++++ .../is_spark/configuration_pragma_5/test2.adb | 5 ++++ .../is_spark/configuration_pragma_5/test2.ads | 5 ++++ user_manual/changes/libadalang/1073.yaml | 8 ++++++ 10 files changed, 80 insertions(+), 6 deletions(-) create mode 100644 testsuite/tests/properties/is_spark/configuration_pragma_5/test.adb create mode 100644 testsuite/tests/properties/is_spark/configuration_pragma_5/test.ads create mode 100644 testsuite/tests/properties/is_spark/configuration_pragma_5/test.out create mode 100644 testsuite/tests/properties/is_spark/configuration_pragma_5/test.py create mode 100644 testsuite/tests/properties/is_spark/configuration_pragma_5/test.yaml create mode 100644 testsuite/tests/properties/is_spark/configuration_pragma_5/test2-p.adb create mode 100644 testsuite/tests/properties/is_spark/configuration_pragma_5/test2.adb create mode 100644 testsuite/tests/properties/is_spark/configuration_pragma_5/test2.ads create mode 100644 user_manual/changes/libadalang/1073.yaml diff --git a/ada/ast.py b/ada/ast.py index c6361dddf..c32405440 100644 --- a/ada/ast.py +++ b/ada/ast.py @@ -20347,7 +20347,7 @@ def local_config_pragmas(): ) @langkit_property(return_type=T.Pragma.array) - def sources_config_pragmas(): + def sources_config_pragmas(include_other_part=(Bool, True)): """ Return the list of configuration pragmas defined in Ada sources and which apply to the current unit. @@ -20360,13 +20360,14 @@ def sources_config_pragmas(): Cond( # If Self is a spec, we need to look at its body, and # conversely. - Self.body.is_a(T.LibraryItem), + include_other_part & Self.body.is_a(T.LibraryItem), Self.other_part._.local_config_pragmas, # If Self is a sub-unit, we need to look at all subunits up in # the chain, the root body, and the corresponding spec. Self.body.is_a(T.Subunit), - Self.body.cast(Subunit).root_unit._.sources_config_pragmas, + Self.body.cast(Subunit).root_unit + ._.sources_config_pragmas(include_other_part), No(T.Pragma.array), ) @@ -20385,6 +20386,21 @@ def all_config_pragmas(): .map(lambda n: n.as_bare_entity) ) + @langkit_property(return_type=T.Pragma.entity) + def spark_config_pragma(): + """ + Return the ``SPARK_Mode`` configuration pragma that applies to the + current unit. + """ + return ( + Self.external_config_pragmas.concat( + Self.sources_config_pragmas(include_other_part=False) + ).filtermap( + lambda n: n.as_bare_entity, + lambda n: n.id.name_is("SPARK_Mode") + ).at(-1) + ) + @langkit_property(return_type=T.Pragma.entity.array, public=True) def config_pragmas(name=T.Symbol): """ @@ -20735,9 +20751,7 @@ def is_spark(include_skip_proof_annotations=(T.Bool, True)): # Finally, check for configuration pragmas. This configuration # pragma is of the form `pragma SPARK_Mode [On|Off|Auto]`. - Entity.enclosing_compilation_unit.all_config_pragmas.filter( - lambda p: p.id.name_is("SPARK_Mode") - ).at(0).then( + Entity.enclosing_compilation_unit.spark_config_pragma.then( lambda p: p.spark_mode_is_on, # No configuration pragma were found default_val=False diff --git a/testsuite/tests/properties/is_spark/configuration_pragma_5/test.adb b/testsuite/tests/properties/is_spark/configuration_pragma_5/test.adb new file mode 100644 index 000000000..7e7b21455 --- /dev/null +++ b/testsuite/tests/properties/is_spark/configuration_pragma_5/test.adb @@ -0,0 +1,3 @@ +package body Test is + procedure P is null; -- Off +end Test; diff --git a/testsuite/tests/properties/is_spark/configuration_pragma_5/test.ads b/testsuite/tests/properties/is_spark/configuration_pragma_5/test.ads new file mode 100644 index 000000000..94e483ed0 --- /dev/null +++ b/testsuite/tests/properties/is_spark/configuration_pragma_5/test.ads @@ -0,0 +1,5 @@ +pragma SPARK_Mode (On); + +package Test is + procedure P; +end Test; diff --git a/testsuite/tests/properties/is_spark/configuration_pragma_5/test.out b/testsuite/tests/properties/is_spark/configuration_pragma_5/test.out new file mode 100644 index 000000000..b0c10c7e0 --- /dev/null +++ b/testsuite/tests/properties/is_spark/configuration_pragma_5/test.out @@ -0,0 +1,6 @@ +=== Analysing unit: """ +Subprogram is skipped + +=== Analysing unit: """ +Subprogram is analyzed + diff --git a/testsuite/tests/properties/is_spark/configuration_pragma_5/test.py b/testsuite/tests/properties/is_spark/configuration_pragma_5/test.py new file mode 100644 index 000000000..a00ee4482 --- /dev/null +++ b/testsuite/tests/properties/is_spark/configuration_pragma_5/test.py @@ -0,0 +1,22 @@ +""" +This test checks that calling get_aspect/has_aspect/get_pragma/is_spark on a +subprogram body node works as expected. +""" +import glob +import libadalang as lal + + +context = lal.AnalysisContext() +context.set_config_pragmas_mapping(None, {}) + +for filename in sorted(glob.glob('*.ad[bs]')): + unit = context.get_from_file(filename) + subprograms = unit.root.findall(lal.BaseSubpBody) + if subprograms: + print('=== Analysing unit: ', unit, '"""') + for subprogram in subprograms: + print("Subprogram {} is {}".format( + subprogram, + "analyzed" if subprogram.p_is_spark() else "skipped" + )) + print('') diff --git a/testsuite/tests/properties/is_spark/configuration_pragma_5/test.yaml b/testsuite/tests/properties/is_spark/configuration_pragma_5/test.yaml new file mode 100644 index 000000000..30423a038 --- /dev/null +++ b/testsuite/tests/properties/is_spark/configuration_pragma_5/test.yaml @@ -0,0 +1 @@ +driver: python diff --git a/testsuite/tests/properties/is_spark/configuration_pragma_5/test2-p.adb b/testsuite/tests/properties/is_spark/configuration_pragma_5/test2-p.adb new file mode 100644 index 000000000..91dab827f --- /dev/null +++ b/testsuite/tests/properties/is_spark/configuration_pragma_5/test2-p.adb @@ -0,0 +1,5 @@ +separate (Test2) +procedure P is +begin + null; +end P; diff --git a/testsuite/tests/properties/is_spark/configuration_pragma_5/test2.adb b/testsuite/tests/properties/is_spark/configuration_pragma_5/test2.adb new file mode 100644 index 000000000..a074fa344 --- /dev/null +++ b/testsuite/tests/properties/is_spark/configuration_pragma_5/test2.adb @@ -0,0 +1,5 @@ +pragma SPARK_Mode; + +package body Test2 is + procedure P is separate; +end Test2; diff --git a/testsuite/tests/properties/is_spark/configuration_pragma_5/test2.ads b/testsuite/tests/properties/is_spark/configuration_pragma_5/test2.ads new file mode 100644 index 000000000..3c045411f --- /dev/null +++ b/testsuite/tests/properties/is_spark/configuration_pragma_5/test2.ads @@ -0,0 +1,5 @@ +pragma SPARK_Mode; + +package Test2 is + procedure P; +end Test2; diff --git a/user_manual/changes/libadalang/1073.yaml b/user_manual/changes/libadalang/1073.yaml new file mode 100644 index 000000000..1a6cc82e4 --- /dev/null +++ b/user_manual/changes/libadalang/1073.yaml @@ -0,0 +1,8 @@ +type: bugfix +title: Fix `p_is_spark` configuration pragma handling +description: | + This change fixes a bug in the `is_spark` property where configuration + pragmas were not handled correctly: a `SPARK_Mode` configuration pragma in a + package specification only applies to the package specification and does not + affect the body (and vice-versa). +date: 2023-09-12