Fix type conflicts in generated code

Ref. #500
AdaCore · Dec 1, 2020 · 4e7bfbc · 4e7bfbc
1 parent 58374e3
commit 4e7bfbc
Show file tree

Hide file tree

Showing 68 changed files with 180 additions and 98 deletions.
diff --git a/rflx/generator/common.py b/rflx/generator/common.py
@@ -1,4 +1,4 @@
-from typing import Callable, Mapping, Sequence
+from typing import Callable, Mapping, Optional, Sequence
 
 import rflx.ada as ada
 import rflx.expression as expr
@@ -24,7 +24,7 @@ def substitution(
     message: Message,
     embedded: bool = False,
     public: bool = False,
-    target_type: ada.ID = const.TYPES_U64,
+    target_type: Optional[ada.ID] = const.TYPES_U64,
 ) -> Callable[[expr.Expr], expr.Expr]:
     facts = substitution_facts(message, embedded, public, target_type)
 
@@ -127,7 +127,7 @@ def substitution_facts(
     message: Message,
     embedded: bool = False,
     public: bool = False,
-    target_type: ada.ID = const.TYPES_U64,
+    target_type: Optional[ada.ID] = const.TYPES_U64,
 ) -> Mapping[expr.Name, expr.Expr]:
     def prefixed(name: str) -> expr.Expr:
         return expr.Variable(expr.ID("Ctx") * name) if not embedded else expr.Variable(name)
@@ -153,86 +153,61 @@ def field_last(field: Field) -> expr.Expr:
     def field_size(field: Field) -> expr.Expr:
         if public:
             return expr.Call(
-                target_type,
-                [
-                    expr.Call(
-                        "Field_Size", [expr.Variable("Ctx"), expr.Variable(field.affixed_name)]
-                    )
-                ],
+                "Field_Size", [expr.Variable("Ctx"), expr.Variable(field.affixed_name)]
             )
-        return expr.Call(
-            target_type,
-            [
-                expr.Add(
-                    expr.Sub(
-                        expr.Selected(
-                            expr.Indexed(cursors, expr.Variable(field.affixed_name)), "Last"
-                        ),
-                        expr.Selected(
-                            expr.Indexed(cursors, expr.Variable(field.affixed_name)), "First"
-                        ),
-                    ),
-                    expr.Number(1),
-                )
-            ],
+        return expr.Add(
+            expr.Sub(
+                expr.Selected(expr.Indexed(cursors, expr.Variable(field.affixed_name)), "Last"),
+                expr.Selected(expr.Indexed(cursors, expr.Variable(field.affixed_name)), "First"),
+            ),
+            expr.Number(1),
         )
 
     def field_value(field: Field, field_type: Type) -> expr.Expr:
         if isinstance(field_type, Enumeration):
             if public:
                 return expr.Call(
-                    target_type,
-                    [
-                        expr.Call(
-                            "To_Base", [expr.Call(f"Get_{field.name}", [expr.Variable("Ctx")])]
-                        )
-                    ],
+                    "To_Base", [expr.Call(f"Get_{field.name}", [expr.Variable("Ctx")])]
                 )
-            return expr.Call(
-                target_type,
-                [
-                    expr.Selected(
-                        expr.Indexed(cursors, expr.Variable(field.affixed_name)),
-                        expr.ID("Value") * f"{field.name}_Value",
-                    )
-                ],
+            return expr.Selected(
+                expr.Indexed(cursors, expr.Variable(field.affixed_name)),
+                expr.ID("Value") * f"{field.name}_Value",
             )
         if isinstance(field_type, Scalar):
             if public:
-                return expr.Call(
-                    target_type, [expr.Call(f"Get_{field.name}", [expr.Variable("Ctx")])]
-                )
-            return expr.Call(
-                target_type,
-                [
-                    expr.Selected(
-                        expr.Indexed(cursors, expr.Variable(field.affixed_name)),
-                        expr.ID("Value") * f"{field.name}_Value",
-                    )
-                ],
+                return expr.Call(f"Get_{field.name}", [expr.Variable("Ctx")])
+            return expr.Selected(
+                expr.Indexed(cursors, expr.Variable(field.affixed_name)),
+                expr.ID("Value") * f"{field.name}_Value",
             )
         if isinstance(field_type, Composite):
             return expr.Variable(field.name)
 
         assert False, f'unexpected type "{type(field_type).__name__}"'
 
+    def type_conversion(expression: expr.Expr) -> expr.Expr:
+        return expr.Call(target_type, [expression]) if target_type else expression
+
     return {
-        **{expr.First("Message"): first},
-        **{expr.Last("Message"): last},
-        **{expr.Size("Message"): expr.Add(last, -first, expr.Number(1))},
-        **{expr.First(f.name): field_first(f) for f in message.fields},
-        **{expr.Last(f.name): field_last(f) for f in message.fields},
-        **{expr.Size(f.name): field_size(f) for f in message.fields},
-        **{expr.Variable(f.name): field_value(f, t) for f, t in message.types.items()},
+        **{expr.First("Message"): type_conversion(first)},
+        **{expr.Last("Message"): type_conversion(last)},
+        **{expr.Size("Message"): type_conversion(expr.Add(last, -first, expr.Number(1)))},
+        **{expr.First(f.name): type_conversion(field_first(f)) for f in message.fields},
+        **{expr.Last(f.name): type_conversion(field_last(f)) for f in message.fields},
+        **{expr.Size(f.name): type_conversion(field_size(f)) for f in message.fields},
+        **{
+            expr.Variable(f.name): type_conversion(field_value(f, t))
+            for f, t in message.types.items()
+        },
         **{
-            expr.Variable(l): expr.Call(target_type, [expr.Call("To_Base", [expr.Variable(l)])])
+            expr.Variable(l): type_conversion(expr.Call("To_Base", [expr.Variable(l)]))
             for t in message.types.values()
             if isinstance(t, Enumeration)
             for l in t.literals.keys()
         },
         **{
-            expr.Variable(t.package * l): expr.Call(
-                target_type, [expr.Call("To_Base", [expr.Variable(t.package * l)])]
+            expr.Variable(t.package * l): type_conversion(
+                expr.Call("To_Base", [expr.Variable(t.package * l)])
             )
             for t in message.types.values()
             if isinstance(t, Enumeration)
@@ -270,7 +245,9 @@ def prefixed(name: str) -> expr.Expr:
     first = (
         prefixed("First")
         if source == INITIAL
-        else link.first.substituted(substitution(message, embedded))
+        else link.first.substituted(
+            substitution(message, embedded, target_type=const.TYPES_BIT_INDEX)
+        )
         .substituted(
             mapping={
                 expr.UNDEFINED: expr.Add(

diff --git a/rflx/generator/generator.py b/rflx/generator/generator.py
@@ -3,7 +3,7 @@
 import logging
 from datetime import date
 from pathlib import Path
-from typing import Dict, List, Mapping, Sequence, Tuple, cast
+from typing import Dict, List, Mapping, Optional, Sequence, Tuple, cast
 
 import pkg_resources
 
@@ -132,7 +132,11 @@
 
 NULL = Variable("null")
 
-CONFIGURATION_PRAGMAS = [Pragma("Style_Checks", [String("N3aAbcdefhiIklnOprStux")])]
+CONFIGURATION_PRAGMAS = [
+    Pragma("Style_Checks", [String("N3aAbcdefhiIklnOprStux")]),
+    # ISSUE: Componolit/RecordFlux#508
+    Pragma("Warnings", [Variable("Off"), String("redundant conversion")]),
+]
 
 
 class Generator:
@@ -1037,8 +1041,14 @@ def substituted(expression: expr.Expr) -> Expr:
     @staticmethod
     def __create_field_first_function(message: Message) -> UnitPart:
         def first(field: Field, message: Message) -> Expr:
-            def substituted(expression: expr.Expr) -> Expr:
-                return expression.substituted(common.substitution(message)).simplified().ada_expr()
+            def substituted(
+                expression: expr.Expr, target_type: Optional[ID] = const.TYPES_U64
+            ) -> Expr:
+                return (
+                    expression.substituted(common.substitution(message, target_type=target_type))
+                    .simplified()
+                    .ada_expr()
+                )
 
             if field == message.fields[0]:
                 return Variable("Ctx.First")
@@ -1075,7 +1085,8 @@ def substituted(expression: expr.Expr) -> Expr:
                         substituted(
                             l.first.substituted(
                                 lambda x: contiguous_first if x == expr.UNDEFINED else x
-                            )
+                            ),
+                            target_type=None,
                         ),
                     )
                     for l in message.incoming(field)
@@ -1154,8 +1165,16 @@ def condition(field: Field, message: Message) -> Expr:
                 mapping={
                     expr.Size(field.name): expr.Call(const.TYPES_U64, [expr.Variable("Size")]),
                     expr.Last(field.name): expr.Call(
-                        "Field_Last",
-                        [expr.Variable("Ctx"), expr.Variable(field.affixed_name, immutable=True)],
+                        const.TYPES_U64,
+                        [
+                            expr.Call(
+                                "Field_Last",
+                                [
+                                    expr.Variable("Ctx"),
+                                    expr.Variable(field.affixed_name, immutable=True),
+                                ],
+                            )
+                        ],
                     ),
                     # ISSUE: Componolit/RecordFlux#276
                     **{expr.ValidChecksum(f): expr.TRUE for f in message.checksums},

diff --git a/tests/integration/specification_model_generator_test.py b/tests/integration/specification_model_generator_test.py
@@ -205,3 +205,25 @@ def test_size_attribute(tmp_path: Path, aspects: str) -> None:
         """,
         tmp_path,
     )
+
+
+def test_message_size_calculation(tmp_path: Path) -> None:
+    utils.assert_compilable_code_string(
+        """
+           package Test is
+
+              type T is mod 2**16;
+
+              type Message is
+                 message
+                    A : T;
+                    B : T;
+                    C : Opaque
+                       with Size => A * 8
+                       if Message'Size = A * 8 + (B'Last - A'First + 1);
+                 end message;
+
+           end Test;
+        """,
+        tmp_path,
+    )
diff --git a/tests/spark/generated/rflx-arrays-array_size_defined_by_message_size.ads b/tests/spark/generated/rflx-arrays-array_size_defined_by_message_size.ads
@@ -1,4 +1,5 @@
 pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
+pragma Warnings (Off, "redundant conversion");
 pragma SPARK_Mode;
 with RFLX.Arrays.Generic_Array_Size_Defined_By_Message_Size;
 with RFLX.RFLX_Types;

diff --git a/tests/spark/generated/rflx-arrays-av_enumeration_vector.ads b/tests/spark/generated/rflx-arrays-av_enumeration_vector.ads
@@ -1,4 +1,5 @@
 pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
+pragma Warnings (Off, "redundant conversion");
 pragma SPARK_Mode;
 with RFLX.RFLX_Scalar_Sequence;
 with RFLX.Arrays;

diff --git a/tests/spark/generated/rflx-arrays-enumeration_vector.ads b/tests/spark/generated/rflx-arrays-enumeration_vector.ads
@@ -1,4 +1,5 @@
 pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
+pragma Warnings (Off, "redundant conversion");
 pragma SPARK_Mode;
 with RFLX.RFLX_Scalar_Sequence;
 with RFLX.Arrays;

diff --git a/tests/spark/generated/rflx-arrays-generic_array_size_defined_by_message_size.adb b/tests/spark/generated/rflx-arrays-generic_array_size_defined_by_message_size.adb
@@ -1,4 +1,5 @@
 pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
+pragma Warnings (Off, "redundant conversion");
 
 package body RFLX.Arrays.Generic_Array_Size_Defined_By_Message_Size with
   SPARK_Mode
@@ -70,7 +71,7 @@ is
           when F_Header =>
              (case Fld is
                  when F_Vector =>
-                    Ctx.Last - Ctx.First + 1 - Types.Bit_Length (Ctx.Cursors (F_Header).Last - Ctx.Cursors (F_Header).First + 1),
+                    Types.Bit_Length (Ctx.Last - Ctx.First + 1) - Types.Bit_Length (Ctx.Cursors (F_Header).Last - Ctx.Cursors (F_Header).First + 1),
                  when others =>
                     Types.Unreachable_Bit_Length),
           when F_Vector | F_Final =>
@@ -264,7 +265,7 @@ is
                                   and then (if
                                                Structural_Valid (Ctx.Cursors (F_Vector))
                                             then
-                                               Ctx.Cursors (F_Vector).Last - Ctx.Cursors (F_Vector).First + 1 = Ctx.Last - Ctx.First + 1 - Types.Bit_Length (Ctx.Cursors (F_Header).Last - Ctx.Cursors (F_Header).First + 1)
+                                               Ctx.Cursors (F_Vector).Last - Ctx.Cursors (F_Vector).First + 1 = Types.Bit_Length (Ctx.Last - Ctx.First + 1) - Types.Bit_Length (Ctx.Cursors (F_Header).Last - Ctx.Cursors (F_Header).First + 1)
                                                and then Ctx.Cursors (F_Vector).Predecessor = F_Header
                                                and then Ctx.Cursors (F_Vector).First = Ctx.Cursors (F_Header).Last + 1)));
                if Fld = F_Header then
@@ -433,7 +434,7 @@ is
                             and then (if
                                          Structural_Valid (Ctx.Cursors (F_Vector))
                                       then
-                                         Ctx.Cursors (F_Vector).Last - Ctx.Cursors (F_Vector).First + 1 = Ctx.Last - Ctx.First + 1 - Types.Bit_Length (Ctx.Cursors (F_Header).Last - Ctx.Cursors (F_Header).First + 1)
+                                         Ctx.Cursors (F_Vector).Last - Ctx.Cursors (F_Vector).First + 1 = Types.Bit_Length (Ctx.Last - Ctx.First + 1) - Types.Bit_Length (Ctx.Cursors (F_Header).Last - Ctx.Cursors (F_Header).First + 1)
                                          and then Ctx.Cursors (F_Vector).Predecessor = F_Header
                                          and then Ctx.Cursors (F_Vector).First = Ctx.Cursors (F_Header).Last + 1)));
          Ctx.Cursors (F_Vector) := (State => S_Structural_Valid, First => First, Last => Last, Value => (Fld => F_Vector), Predecessor => Ctx.Cursors (F_Vector).Predecessor);

diff --git a/tests/spark/generated/rflx-arrays-generic_array_size_defined_by_message_size.ads b/tests/spark/generated/rflx-arrays-generic_array_size_defined_by_message_size.ads
@@ -1,4 +1,5 @@
 pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
+pragma Warnings (Off, "redundant conversion");
 with RFLX.RFLX_Generic_Types;
 with RFLX.RFLX_Scalar_Sequence;
 
@@ -431,7 +432,7 @@ private
                    and then (if
                                 Structural_Valid (Cursors (F_Vector))
                              then
-                                Cursors (F_Vector).Last - Cursors (F_Vector).First + 1 = Last - First + 1 - Types.Bit_Length (Cursors (F_Header).Last - Cursors (F_Header).First + 1)
+                                Cursors (F_Vector).Last - Cursors (F_Vector).First + 1 = Types.Bit_Length (Last - First + 1) - Types.Bit_Length (Cursors (F_Header).Last - Cursors (F_Header).First + 1)
                                 and then Cursors (F_Vector).Predecessor = F_Header
                                 and then Cursors (F_Vector).First = Cursors (F_Header).Last + 1)));
 

diff --git a/tests/spark/generated/rflx-arrays-generic_inner_message.adb b/tests/spark/generated/rflx-arrays-generic_inner_message.adb
@@ -1,4 +1,5 @@
 pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
+pragma Warnings (Off, "redundant conversion");
 
 package body RFLX.Arrays.Generic_Inner_Message with
   SPARK_Mode

diff --git a/tests/spark/generated/rflx-arrays-generic_inner_message.ads b/tests/spark/generated/rflx-arrays-generic_inner_message.ads
@@ -1,4 +1,5 @@
 pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
+pragma Warnings (Off, "redundant conversion");
 with RFLX.RFLX_Generic_Types;
 
 generic

diff --git a/tests/spark/generated/rflx-arrays-generic_message.adb b/tests/spark/generated/rflx-arrays-generic_message.adb
@@ -1,4 +1,5 @@
 pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
+pragma Warnings (Off, "redundant conversion");
 
 package body RFLX.Arrays.Generic_Message with
   SPARK_Mode

diff --git a/tests/spark/generated/rflx-arrays-generic_message.ads b/tests/spark/generated/rflx-arrays-generic_message.ads
@@ -1,4 +1,5 @@
 pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
+pragma Warnings (Off, "redundant conversion");
 with RFLX.RFLX_Generic_Types;
 with RFLX.RFLX_Scalar_Sequence;
 

diff --git a/tests/spark/generated/rflx-arrays-generic_messages_message.adb b/tests/spark/generated/rflx-arrays-generic_messages_message.adb
@@ -1,4 +1,5 @@
 pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
+pragma Warnings (Off, "redundant conversion");
 
 package body RFLX.Arrays.Generic_Messages_Message with
   SPARK_Mode

diff --git a/tests/spark/generated/rflx-arrays-generic_messages_message.ads b/tests/spark/generated/rflx-arrays-generic_messages_message.ads
@@ -1,4 +1,5 @@
 pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
+pragma Warnings (Off, "redundant conversion");
 with RFLX.RFLX_Generic_Types;
 with RFLX.RFLX_Message_Sequence;
 

diff --git a/tests/spark/generated/rflx-arrays-inner_message.ads b/tests/spark/generated/rflx-arrays-inner_message.ads
@@ -1,4 +1,5 @@
 pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
+pragma Warnings (Off, "redundant conversion");
 pragma SPARK_Mode;
 with RFLX.Arrays.Generic_Inner_Message;
 with RFLX.RFLX_Types;

diff --git a/tests/spark/generated/rflx-arrays-inner_messages.ads b/tests/spark/generated/rflx-arrays-inner_messages.ads
@@ -1,4 +1,5 @@
 pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
+pragma Warnings (Off, "redundant conversion");
 pragma SPARK_Mode;
 with RFLX.RFLX_Message_Sequence;
 with RFLX.Arrays.Inner_Message;

diff --git a/tests/spark/generated/rflx-arrays-message.ads b/tests/spark/generated/rflx-arrays-message.ads
@@ -1,4 +1,5 @@
 pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
+pragma Warnings (Off, "redundant conversion");
 pragma SPARK_Mode;
 with RFLX.Arrays.Generic_Message;
 with RFLX.RFLX_Types;

diff --git a/tests/spark/generated/rflx-arrays-messages_message.ads b/tests/spark/generated/rflx-arrays-messages_message.ads
@@ -1,4 +1,5 @@
 pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
+pragma Warnings (Off, "redundant conversion");
 pragma SPARK_Mode;
 with RFLX.Arrays.Generic_Messages_Message;
 with RFLX.RFLX_Types;

diff --git a/tests/spark/generated/rflx-arrays-modular_vector.ads b/tests/spark/generated/rflx-arrays-modular_vector.ads
@@ -1,4 +1,5 @@
 pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
+pragma Warnings (Off, "redundant conversion");
 pragma SPARK_Mode;
 with RFLX.RFLX_Scalar_Sequence;
 with RFLX.Arrays;

diff --git a/tests/spark/generated/rflx-arrays-range_vector.ads b/tests/spark/generated/rflx-arrays-range_vector.ads
@@ -1,4 +1,5 @@
 pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
+pragma Warnings (Off, "redundant conversion");
 pragma SPARK_Mode;
 with RFLX.RFLX_Scalar_Sequence;
 with RFLX.Arrays;

diff --git a/tests/spark/generated/rflx-arrays.ads b/tests/spark/generated/rflx-arrays.ads
@@ -1,4 +1,5 @@
 pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
+pragma Warnings (Off, "redundant conversion");
 
 package RFLX.Arrays with
   SPARK_Mode

diff --git a/tests/spark/generated/rflx-derivation-message.ads b/tests/spark/generated/rflx-derivation-message.ads
@@ -1,4 +1,5 @@
 pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
+pragma Warnings (Off, "redundant conversion");
 pragma SPARK_Mode;
 with RFLX.TLV.Generic_Message;
 with RFLX.RFLX_Types;