From 316e9e7521c1f83f600cfdaf1c2925a56c976d7f Mon Sep 17 00:00:00 2001 From: Tobias Reiher Date: Thu, 22 Sep 2022 18:46:48 +0200 Subject: [PATCH 1/3] Reduce skipping of jobs in tests workflow --- .github/workflows/tests.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml index 6b45149cf..9220d72ca 100644 --- a/.github/workflows/tests.yml +++ b/.github/workflows/tests.yml @@ -99,7 +99,7 @@ jobs: installation: name: Installation needs: skip_check_general - if: ${{ needs.skip_check_python.outputs.should_skip != 'true' }} + if: ${{ needs.skip_check_general.outputs.should_skip != 'true' }} runs-on: ubuntu-20.04 steps: - uses: actions/checkout@v2 @@ -464,7 +464,7 @@ jobs: - id: skip_check uses: fkirc/skip-duplicate-actions@v3.4.0 with: - paths: '[".github/workflows/**", "*.gpr", "tests/spark/**"]' + paths: '[".github/workflows/**", "*.gpr", "rflx/**", "tests/**"]' verification_spark: name: Verification From 3bcc9435dc8740b90e75370f9a81b71bc3f5814f Mon Sep 17 00:00:00 2001 From: Tobias Reiher Date: Thu, 22 Sep 2022 18:57:05 +0200 Subject: [PATCH 2/3] Fix tests Ref. #993 --- .../specification_model_generator_test.py | 49 +++++++++++++------ 1 file changed, 35 insertions(+), 14 deletions(-) diff --git a/tests/integration/specification_model_generator_test.py b/tests/integration/specification_model_generator_test.py index 93417becf..26e2fcd69 100644 --- a/tests/integration/specification_model_generator_test.py +++ b/tests/integration/specification_model_generator_test.py @@ -446,9 +446,7 @@ def test_refinement_with_self(tmp_path: Path) -> None: ) -@pytest.mark.verification -def test_definite_message_with_builtin_type(tmp_path: Path) -> None: - spec = """\ +DEFINITE_MESSAGE_WITH_BUILTIN_TYPE_SPEC = """\ package Test is type Length is range 0 .. 2 ** 7 - 1 with Size => 7; @@ -464,8 +462,17 @@ def test_definite_message_with_builtin_type(tmp_path: Path) -> None: end Test; """ - utils.assert_compilable_code_string(spec, tmp_path) - utils.assert_provable_code_string(spec, tmp_path, units=["rflx-test-message"]) + + +def test_definite_message_with_builtin_type(tmp_path: Path) -> None: + utils.assert_compilable_code_string(DEFINITE_MESSAGE_WITH_BUILTIN_TYPE_SPEC, tmp_path) + + +@pytest.mark.verification +def test_definite_message_with_builtin_type_provability(tmp_path: Path) -> None: + utils.assert_provable_code_string( + DEFINITE_MESSAGE_WITH_BUILTIN_TYPE_SPEC, tmp_path, units=["rflx-test-message"] + ) def test_message_expression_value_outside_type_range(tmp_path: Path) -> None: @@ -538,9 +545,7 @@ def test_feature_integration(tmp_path: Path) -> None: utils.assert_compilable_code_specs([SPEC_DIR / "feature_integration.rflx"], tmp_path) -@pytest.mark.verification -def test_parameterized_message(tmp_path: Path) -> None: - spec = """\ +PARAMETERIZED_MESSAGE_SPEC = """\ package Test is type Length is range 1 .. 2 ** 14 - 1 with Size => 16; @@ -559,13 +564,20 @@ def test_parameterized_message(tmp_path: Path) -> None: end Test; """ - utils.assert_compilable_code_string(spec, tmp_path) - utils.assert_provable_code_string(spec, tmp_path, units=["rflx-test-message"]) + + +def test_parameterized_message(tmp_path: Path) -> None: + utils.assert_compilable_code_string(PARAMETERIZED_MESSAGE_SPEC, tmp_path) @pytest.mark.verification -def test_definite_parameterized_message(tmp_path: Path) -> None: - spec = """\ +def test_parameterized_message_provability(tmp_path: Path) -> None: + utils.assert_provable_code_string( + PARAMETERIZED_MESSAGE_SPEC, tmp_path, units=["rflx-test-message"] + ) + + +DEFINITE_PARAMETERIZED_MESSAGE_SPEC = """\ package Test is type Length is range 1 .. 2 ** 14 - 1 with Size => 16; @@ -578,8 +590,17 @@ def test_definite_parameterized_message(tmp_path: Path) -> None: end Test; """ - utils.assert_compilable_code_string(spec, tmp_path) - utils.assert_provable_code_string(spec, tmp_path, units=["rflx-test-message"]) + + +def test_definite_parameterized_message(tmp_path: Path) -> None: + utils.assert_compilable_code_string(DEFINITE_PARAMETERIZED_MESSAGE_SPEC, tmp_path) + + +@pytest.mark.verification +def test_definite_parameterized_message_provability(tmp_path: Path) -> None: + utils.assert_provable_code_string( + DEFINITE_PARAMETERIZED_MESSAGE_SPEC, tmp_path, units=["rflx-test-message"] + ) def test_session_type_conversion_in_assignment(tmp_path: Path) -> None: From 9aba2cb4f41e188fbf75f38c54858d008034427b Mon Sep 17 00:00:00 2001 From: Tobias Reiher Date: Thu, 22 Sep 2022 19:34:43 +0200 Subject: [PATCH 3/3] Fix generation of SPARK test code Ref. #993 --- tools/generate_spark_test_code.py | 51 ++++++++++++++++++++++++------- 1 file changed, 40 insertions(+), 11 deletions(-) diff --git a/tools/generate_spark_test_code.py b/tools/generate_spark_test_code.py index 05a510ff9..d5907e285 100755 --- a/tools/generate_spark_test_code.py +++ b/tools/generate_spark_test_code.py @@ -2,13 +2,16 @@ """Generate the SPARK code for the test project and all feature tests.""" +from __future__ import annotations + import filecmp import logging -import sys from pathlib import Path +from rflx.common import unique from rflx.generator import Generator from rflx.integration import Integration +from rflx.model import Model, Session, Type from rflx.specification import Parser from tests.const import SPEC_DIR from tests.unit.generator_test import MODELS @@ -35,17 +38,25 @@ ] -def main() -> int: +def main() -> None: + generate_spark_tests() + generate_feature_tests() + + +def generate_spark_tests() -> None: + remove_ada_files(OUTPUT_DIRECTORY) + parser = Parser() parser.parse(*SPECIFICATION_FILES) + model = merge_models([parser.create_model(), *MODELS]) + Generator( + "RFLX", + reproducible=True, + ignore_unsupported_checksum=True, + ).generate(model, Integration(), OUTPUT_DIRECTORY) - for model in [parser.create_model(), *MODELS]: - Generator( - "RFLX", - reproducible=True, - ignore_unsupported_checksum=True, - ).generate(model, Integration(), OUTPUT_DIRECTORY) +def generate_feature_tests() -> None: generate(SHARED_DIRECTORY) shared_files = {f.name: f for f in (SHARED_DIRECTORY / "generated").iterdir()} @@ -56,12 +67,13 @@ def main() -> int: f.unlink() f.symlink_to(f"../../shared/generated/{f.name}") - return 0 - def generate(feature_test: Path) -> None: output_directory = feature_test / "generated" output_directory.mkdir(exist_ok=True) + + remove_ada_files(output_directory) + parser = Parser() parser.parse(feature_test / "test.rflx") Generator( @@ -71,5 +83,22 @@ def generate(feature_test: Path) -> None: ).generate(parser.create_model(), parser.get_integration(), output_directory) +def remove_ada_files(directory: Path) -> None: + for f in directory.glob("*.ad?"): + print(f"Removing {f}") + f.unlink() + + +def merge_models(models: list[Model]) -> Model: + types: list[Type] = [] + sessions: list[Session] = [] + + for m in models: + types.extend(m.types) + sessions.extend(m.sessions) + + return Model(list(unique(types)), list(unique(sessions))) + + if __name__ == "__main__": - sys.exit(main()) + main()