Small optimization for messages with single field

Ref. eng/recordflux/RecordFlux#1761
AdaCore · Aug 27, 2024 · 90454fe · 90454fe
1 parent d2e047a
commit 90454fe
Show file tree

Hide file tree

Showing 6 changed files with 27 additions and 16 deletions.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -5,6 +5,12 @@ All notable changes to this project will be documented in this file.
 The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/),
 and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html).
 
+## [Unreleased]
+
+### Changed
+
+- Improve generation of predicate for single-field messages (eng/recordflux/RecordFlux#1761)
+
 ## [0.23.0] - 2024-08-23
 
 ### Changed
@@ -554,6 +560,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ## [0.1.0] - 2019-05-14
 
+[Unreleased]: https://github.com/AdaCore/RecordFlux/compare/v0.23.0...HEAD
 [0.23.0]: https://github.com/AdaCore/RecordFlux/compare/v0.22.0...v0.23.0
 [0.22.0]: https://github.com/AdaCore/RecordFlux/compare/v0.21.0...v0.22.0
 [0.21.0]: https://github.com/AdaCore/RecordFlux/compare/v0.20.0...v0.21.0

diff --git a/rflx/generator/message.py b/rflx/generator/message.py
@@ -1203,6 +1203,21 @@ def create_initialized_function(prefix: str, message: Message) -> UnitPart:
     specification = FunctionSpecification("Initialized", "Boolean", [Parameter(["Ctx"], "Context")])
     first_field = message.fields[0]
 
+    def all_fields_invalid() -> Expr:
+        if len(message.fields) == 1:
+            return Call(
+                "Invalid",
+                [Variable("Ctx"), Variable(message.fields[0].affixed_name)],
+            )
+        return ForAllIn(
+            "F",
+            Variable("Field"),
+            Call(
+                "Invalid",
+                [Variable("Ctx"), Variable("F")],
+            ),
+        )
+
     return UnitPart(
         [
             # Eng/RecordFlux/Workarounds#47
@@ -1246,14 +1261,7 @@ def create_initialized_function(prefix: str, message: Message) -> UnitPart:
                             Number(1),
                         ),
                     ),
-                    ForAllIn(
-                        "F",
-                        Variable("Field"),
-                        Call(
-                            "Invalid",
-                            [Variable("Ctx"), Variable("F")],
-                        ),
-                    ),
+                    all_fields_invalid(),
                 ),
             ),
         ],

diff --git a/tests/feature/messages_with_single_opaque_field/generated/rflx-test-message.ads b/tests/feature/messages_with_single_opaque_field/generated/rflx-test-message.ads
@@ -696,8 +696,7 @@ private
       and then Valid_Next (Ctx, F_Data)
       and then RFLX.Test.Message.Field_First (Ctx, RFLX.Test.Message.F_Data) rem RFLX_Types.Byte'Size = 1
       and then Available_Space (Ctx, F_Data) = Ctx.Last - Ctx.First + 1
-      and then (for all F in Field =>
-                   Invalid (Ctx, F)));
+      and then Invalid (Ctx, F_Data));
 
    function Read (Ctx : Context) return RFLX_Types.Bytes is
      (Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Verified_Last)));

diff --git a/tests/feature/session_case_expression_numeric/generated/rflx-test-message.ads b/tests/feature/session_case_expression_numeric/generated/rflx-test-message.ads
@@ -633,8 +633,7 @@ private
       and then Valid_Next (Ctx, F_Value)
       and then RFLX.Test.Message.Field_First (Ctx, RFLX.Test.Message.F_Value) rem RFLX_Types.Byte'Size = 1
       and then Available_Space (Ctx, F_Value) = Ctx.Last - Ctx.First + 1
-      and then (for all F in Field =>
-                   Invalid (Ctx, F)));
+      and then Invalid (Ctx, F_Value));
 
    function Read (Ctx : Context) return RFLX_Types.Bytes is
      (Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Verified_Last)));

diff --git a/tests/spark/generated/rflx-enumeration-message.ads b/tests/spark/generated/rflx-enumeration-message.ads
@@ -633,8 +633,7 @@ private
       and then Valid_Next (Ctx, F_Priority)
       and then RFLX.Enumeration.Message.Field_First (Ctx, RFLX.Enumeration.Message.F_Priority) rem RFLX_Types.Byte'Size = 1
       and then Available_Space (Ctx, F_Priority) = Ctx.Last - Ctx.First + 1
-      and then (for all F in Field =>
-                   Invalid (Ctx, F)));
+      and then Invalid (Ctx, F_Priority));
 
    function Read (Ctx : Context) return RFLX_Types.Bytes is
      (Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Verified_Last)));

diff --git a/tests/spark/generated/rflx-expression-message.ads b/tests/spark/generated/rflx-expression-message.ads
@@ -705,8 +705,7 @@ private
       and then Valid_Next (Ctx, F_Payload)
       and then RFLX.Expression.Message.Field_First (Ctx, RFLX.Expression.Message.F_Payload) rem RFLX_Types.Byte'Size = 1
       and then Available_Space (Ctx, F_Payload) = Ctx.Last - Ctx.First + 1
-      and then (for all F in Field =>
-                   Invalid (Ctx, F)));
+      and then Invalid (Ctx, F_Payload));
 
    function Read (Ctx : Context) return RFLX_Types.Bytes is
      (Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Verified_Last)));