Ensure valid conversion between structure and context

Ref. #961
AdaCore · Apr 4, 2022 · 5b63b8e · 5b63b8e
1 parent 9c895fb
commit 5b63b8e
Show file tree

Hide file tree

Showing 160 changed files with 1,331 additions and 751 deletions.
diff --git a/rflx/generator/generator.py b/rflx/generator/generator.py
diff --git a/rflx/generator/parser.py b/rflx/generator/parser.py
@@ -24,7 +24,6 @@
     ForSomeIn,
     FunctionSpecification,
     Ghost,
-    GreaterEqual,
     If,
     IfStatement,
     In,
@@ -931,7 +930,7 @@ def specification(field: Field) -> ProcedureSpecification:
                                     "Valid_Next",
                                     [Variable("Ctx"), Variable(f.affixed_name)],
                                 ),
-                                GreaterEqual(
+                                Equal(
                                     Length("Data"),
                                     Call(
                                         const.TYPES_TO_LENGTH,
@@ -947,7 +946,17 @@ def specification(field: Field) -> ProcedureSpecification:
                                     ),
                                 ),
                             )
-                        )
+                        ),
+                        Postcondition(
+                            Call(
+                                "Equal",
+                                [
+                                    Variable("Ctx"),
+                                    Variable(f.affixed_name),
+                                    Variable("Data"),
+                                ],
+                            )
+                        ),
                     ],
                 )
                 for f in opaque_fields

diff --git a/rflx/generator/serializer.py b/rflx/generator/serializer.py
diff --git a/rflx/generator/session.py b/rflx/generator/session.py
@@ -2717,13 +2717,20 @@ def _assign_to_call(  # pylint: disable = too-many-locals
                 )
             )
             post_call.append(
-                CallStatement(
-                    ID(type_identifier) * "To_Context",
+                self._if(
+                    Call(ID(type_identifier) * "Valid_Structure", [Variable(target_id)]),
                     [
-                        Variable(target_id),
-                        Variable(context_id(target, is_global)),
+                        CallStatement(
+                            ID(type_identifier) * "To_Context",
+                            [
+                                Variable(target_id),
+                                Variable(context_id(target, is_global)),
+                            ],
+                        ),
                     ],
-                ),
+                    f'"{call_expr.identifier}" returned an invalid message',
+                    exception_handler,
+                )
             )
 
         arguments: list[expr.Expr] = []
@@ -3820,7 +3827,7 @@ def _set_opaque_field_to_message_field(  # pylint: disable = too-many-arguments
                         Variable(message_type * f"F_{message_field}"),
                     ],
                 ),
-                GreaterEqual(
+                Equal(
                     Variable("Length"),
                     Call(
                         const.TYPES_TO_LENGTH,
@@ -3883,7 +3890,7 @@ def _set_opaque_field_to_message(
                         Variable(message_context),
                     ],
                 ),
-                GreaterEqual(
+                Equal(
                     Variable("Length"),
                     Call(
                         message_type * "Byte_Size",

diff --git a/rflx/model/message.py b/rflx/model/message.py
@@ -901,18 +901,25 @@ def is_definite(self) -> bool:
         """
         Return true if the message has an explicit size, no optional fields and no parameters.
 
-        Messages with a First or Last attribute in a size aspect are not yet supported and
-        therefore considered as not definite.
+        Messages with a First or Last attribute in a condition or size aspect are not yet supported
+        and therefore considered as not definite. This is also the case for messages containing
+        sequences.
         """
         return (
             len(self.paths(FINAL)) <= 1
             and not self.has_implicit_size
+            and all(
+                not l.condition.findall(lambda x: isinstance(x, (expr.First, expr.Last)))
+                for l in self.structure
+                for v in l.condition.variables()
+            )
             and all(
                 not l.size.findall(lambda x: isinstance(x, (expr.First, expr.Last)))
                 for l in self.structure
                 for v in l.size.variables()
             )
             and not self.parameters
+            and not any(isinstance(t, mty.Sequence) for t in self.types.values())
         )
 
     def size(self, field_values: Mapping[Field, expr.Expr] = None) -> expr.Expr:

diff --git a/tests/data/models.py b/tests/data/models.py
@@ -9,6 +9,7 @@
     Mul,
     NotEqual,
     Number,
+    Or,
     Pow,
     Size,
     Sub,
@@ -475,6 +476,12 @@
         Link(
             Field("Message_Type"),
             Field("Data"),
+            condition=Or(
+                Equal(Variable("Message_Type"), Variable("Universal.MT_Null")),
+                Equal(Variable("Message_Type"), Variable("Universal.MT_Data")),
+                Equal(Variable("Message_Type"), Variable("Universal.MT_Values")),
+                Equal(Variable("Message_Type"), Variable("Universal.MT_Options")),
+            ),
             size=Number(64),
         ),
         Link(
@@ -506,6 +513,10 @@
         Link(
             Field("Message_Type"),
             Field("Data"),
+            condition=Or(
+                Equal(Variable("Message_Type"), Variable("Universal.OT_Null")),
+                Equal(Variable("Message_Type"), Variable("Universal.OT_Data")),
+            ),
             size=Number(24),
         ),
         Link(

diff --git a/tests/integration/messages/config.yml b/tests/integration/messages/config.yml
@@ -0,0 +1,7 @@
+prove:
+  - rflx-universal-contains
+  - rflx-universal-message
+  - rflx-universal-option
+  - rflx-universal-option_types
+  - rflx-universal-options
+  - rflx-universal-values
diff --git a/tests/integration/messages/generated/rflx-universal-contains.adb b/tests/integration/messages/generated/rflx-universal-contains.adb
@@ -24,7 +24,7 @@ is
       pragma Warnings (Off, """Universal_Option_SDU_Context"" is set by ""Take_Buffer"" but not used after the call");
       RFLX.Universal.Option.Take_Buffer (Universal_Option_SDU_Context, Buffer);
       pragma Warnings (On, """Universal_Option_SDU_Context"" is set by ""Take_Buffer"" but not used after the call");
-      RFLX.Universal.Message.Get_Data (Universal_Message_PDU_Context, Buffer.all);
+      RFLX.Universal.Message.Get_Data (Universal_Message_PDU_Context, Buffer.all (Buffer'First .. Buffer'First + RFLX_Types.Index (RFLX_Types.To_Length (Size)) - 1));
       RFLX.Universal.Option.Initialize (Universal_Option_SDU_Context, Buffer, First, First + Size - 1, First + Size - 1);
    end Copy_Data;
 

diff --git a/tests/integration/messages/generated/rflx-universal-message.adb b/tests/integration/messages/generated/rflx-universal-message.adb
@@ -706,12 +706,13 @@ is
    end Initialize_Values;
 
    procedure Set_Data (Ctx : in out Context; Data : RFLX_Types.Bytes) is
-      First : constant RFLX_Types.Bit_Index := Field_First (Ctx, F_Data);
-      Buffer_First : constant RFLX_Types.Index := RFLX_Types.To_Index (First);
+      Buffer_First : constant RFLX_Types.Index := RFLX_Types.To_Index (Field_First (Ctx, F_Data));
       Buffer_Last : constant RFLX_Types.Index := Buffer_First + Data'Length - 1;
    begin
       Initialize_Data_Private (Ctx, Data'Length);
+      pragma Assert (Buffer_Last = RFLX_Types.To_Index (Field_Last (Ctx, F_Data)));
       Ctx.Buffer.all (Buffer_First .. Buffer_Last) := Data;
+      pragma Assert (Ctx.Buffer.all (RFLX_Types.To_Index (Field_First (Ctx, F_Data)) .. RFLX_Types.To_Index (Field_Last (Ctx, F_Data))) = Data);
    end Set_Data;
 
    procedure Generic_Set_Data (Ctx : in out Context; Length : RFLX_Types.Length) is

diff --git a/tests/integration/messages/generated/rflx-universal-message.ads b/tests/integration/messages/generated/rflx-universal-message.ads
@@ -408,7 +408,9 @@ is
        Has_Buffer (Ctx)
        and then Structural_Valid (Ctx, F_Data)
        and then Valid_Next (Ctx, F_Data)
-       and then Data'Length >= RFLX_Types.To_Length (Field_Size (Ctx, F_Data));
+       and then Data'Length = RFLX_Types.To_Length (Field_Size (Ctx, F_Data)),
+     Post =>
+       Equal (Ctx, F_Data, Data);
 
    generic
       with procedure Process_Data (Data : RFLX_Types.Bytes);
@@ -845,6 +847,7 @@ is
        and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0
        and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0
        and then Valid_Length (Ctx, F_Data, Data'Length)
+       and then Available_Space (Ctx, F_Data) >= Data'Length * RFLX_Types.Byte'Size
        and then Field_Condition (Ctx, F_Data, 0),
      Post =>
        Has_Buffer (Ctx)
@@ -860,7 +863,8 @@ is
        and Ctx.Last = Ctx.Last'Old
        and Predecessor (Ctx, F_Data) = Predecessor (Ctx, F_Data)'Old
        and Valid_Next (Ctx, F_Data) = Valid_Next (Ctx, F_Data)'Old
-       and Get_Message_Type (Ctx) = Get_Message_Type (Ctx)'Old;
+       and Get_Message_Type (Ctx) = Get_Message_Type (Ctx)'Old
+       and Equal (Ctx, F_Data, Data);
 
    generic
       with procedure Process_Data (Data : out RFLX_Types.Bytes);

diff --git a/tests/integration/messages/generated/rflx-universal-option.adb b/tests/integration/messages/generated/rflx-universal-option.adb
@@ -403,12 +403,13 @@ is
    end Initialize_Data;
 
    procedure Set_Data (Ctx : in out Context; Data : RFLX_Types.Bytes) is
-      First : constant RFLX_Types.Bit_Index := Field_First (Ctx, F_Data);
-      Buffer_First : constant RFLX_Types.Index := RFLX_Types.To_Index (First);
+      Buffer_First : constant RFLX_Types.Index := RFLX_Types.To_Index (Field_First (Ctx, F_Data));
       Buffer_Last : constant RFLX_Types.Index := Buffer_First + Data'Length - 1;
    begin
       Initialize_Data_Private (Ctx, Data'Length);
+      pragma Assert (Buffer_Last = RFLX_Types.To_Index (Field_Last (Ctx, F_Data)));
       Ctx.Buffer.all (Buffer_First .. Buffer_Last) := Data;
+      pragma Assert (Ctx.Buffer.all (RFLX_Types.To_Index (Field_First (Ctx, F_Data)) .. RFLX_Types.To_Index (Field_Last (Ctx, F_Data))) = Data);
    end Set_Data;
 
    procedure Generic_Set_Data (Ctx : in out Context; Length : RFLX_Types.Length) is

diff --git a/tests/integration/messages/generated/rflx-universal-option.ads b/tests/integration/messages/generated/rflx-universal-option.ads
@@ -401,7 +401,9 @@ is
        Has_Buffer (Ctx)
        and then Structural_Valid (Ctx, F_Data)
        and then Valid_Next (Ctx, F_Data)
-       and then Data'Length >= RFLX_Types.To_Length (Field_Size (Ctx, F_Data));
+       and then Data'Length = RFLX_Types.To_Length (Field_Size (Ctx, F_Data)),
+     Post =>
+       Equal (Ctx, F_Data, Data);
 
    generic
       with procedure Process_Data (Data : RFLX_Types.Bytes);
@@ -528,6 +530,7 @@ is
        and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0
        and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0
        and then Valid_Length (Ctx, F_Data, Data'Length)
+       and then Available_Space (Ctx, F_Data) >= Data'Length * RFLX_Types.Byte'Size
        and then Field_Condition (Ctx, F_Data, 0),
      Post =>
        Has_Buffer (Ctx)
@@ -540,7 +543,8 @@ is
        and Predecessor (Ctx, F_Data) = Predecessor (Ctx, F_Data)'Old
        and Valid_Next (Ctx, F_Data) = Valid_Next (Ctx, F_Data)'Old
        and Get_Option_Type (Ctx) = Get_Option_Type (Ctx)'Old
-       and Get_Length (Ctx) = Get_Length (Ctx)'Old;
+       and Get_Length (Ctx) = Get_Length (Ctx)'Old
+       and Equal (Ctx, F_Data, Data);
 
    generic
       with procedure Process_Data (Data : out RFLX_Types.Bytes);

diff --git a/tests/integration/messages/generated/rflx-universal.ads b/tests/integration/messages/generated/rflx-universal.ads
@@ -11,6 +11,8 @@ is
        8;
    for Message_Type use (MT_Null => 0, MT_Data => 1, MT_Value => 2, MT_Values => 3, MT_Option_Types => 4, MT_Options => 5, MT_Unconstrained_Data => 6, MT_Unconstrained_Options => 7);
 
+   use type RFLX.RFLX_Types.U64;
+
    function Valid_Message_Type (Val : RFLX.RFLX_Types.U64) return Boolean is
      (Val in 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7);
 
@@ -65,8 +67,6 @@ is
      Size =>
        16;
 
-   use type RFLX.RFLX_Types.U64;
-
    function Valid_Length (Val : RFLX.RFLX_Types.U64) return Boolean is
      (Val <= 65535);
 
@@ -110,16 +110,11 @@ is
          end case;
       end record;
 
-   pragma Warnings (Off, "unused variable ""Val""");
-
-   pragma Warnings (Off, "formal parameter ""Val"" is not referenced");
-
    function Valid_Option_Type (Val : RFLX.RFLX_Types.U64) return Boolean is
-     (True);
-
-   pragma Warnings (On, "formal parameter ""Val"" is not referenced");
+     (Val < 2**8);
 
-   pragma Warnings (On, "unused variable ""Val""");
+   function Valid_Option_Type (Val : Option_Type) return Boolean is
+     ((if Val.Known then True else Valid_Option_Type (Val.Raw) and Val.Raw not in 0 | 1));
 
    function To_U64 (Enum : RFLX.Universal.Option_Type_Enum) return RFLX.RFLX_Types.U64 is
      ((case Enum is

diff --git a/tests/integration/messages_with_implict_size/generated/rflx-test-session.adb b/tests/integration/messages_with_implict_size/generated/rflx-test-session.adb
@@ -51,7 +51,7 @@ is
                         function RFLX_Process_Data_Pre (Length : RFLX_Types.Length) return Boolean is
                           (Universal.Message.Has_Buffer (RFLX_Ctx_P_M_R_Ctx_Tmp)
                            and then Universal.Message.Structural_Valid (RFLX_Ctx_P_M_R_Ctx_Tmp, Universal.Message.F_Data)
-                           and then Length >= RFLX_Types.To_Length (Universal.Message.Field_Size (RFLX_Ctx_P_M_R_Ctx_Tmp, Universal.Message.F_Data)));
+                           and then Length = RFLX_Types.To_Length (Universal.Message.Field_Size (RFLX_Ctx_P_M_R_Ctx_Tmp, Universal.Message.F_Data)));
                         procedure RFLX_Process_Data (Data : out RFLX_Types.Bytes) with
                           Pre =>
                             RFLX_Process_Data_Pre (Data'Length)

diff --git a/tests/integration/messages_with_implict_size/generated/rflx-universal-contains.adb b/tests/integration/messages_with_implict_size/generated/rflx-universal-contains.adb
@@ -24,7 +24,7 @@ is
       pragma Warnings (Off, """Universal_Option_SDU_Context"" is set by ""Take_Buffer"" but not used after the call");
       RFLX.Universal.Option.Take_Buffer (Universal_Option_SDU_Context, Buffer);
       pragma Warnings (On, """Universal_Option_SDU_Context"" is set by ""Take_Buffer"" but not used after the call");
-      RFLX.Universal.Message.Get_Data (Universal_Message_PDU_Context, Buffer.all);
+      RFLX.Universal.Message.Get_Data (Universal_Message_PDU_Context, Buffer.all (Buffer'First .. Buffer'First + RFLX_Types.Index (RFLX_Types.To_Length (Size)) - 1));
       RFLX.Universal.Option.Initialize (Universal_Option_SDU_Context, Buffer, First, First + Size - 1, First + Size - 1);
    end Copy_Data;
 

diff --git a/tests/integration/messages_with_implict_size/generated/rflx-universal-message.adb b/tests/integration/messages_with_implict_size/generated/rflx-universal-message.adb
@@ -706,12 +706,13 @@ is
    end Initialize_Values;
 
    procedure Set_Data (Ctx : in out Context; Data : RFLX_Types.Bytes) is
-      First : constant RFLX_Types.Bit_Index := Field_First (Ctx, F_Data);
-      Buffer_First : constant RFLX_Types.Index := RFLX_Types.To_Index (First);
+      Buffer_First : constant RFLX_Types.Index := RFLX_Types.To_Index (Field_First (Ctx, F_Data));
       Buffer_Last : constant RFLX_Types.Index := Buffer_First + Data'Length - 1;
    begin
       Initialize_Data_Private (Ctx, Data'Length);
+      pragma Assert (Buffer_Last = RFLX_Types.To_Index (Field_Last (Ctx, F_Data)));
       Ctx.Buffer.all (Buffer_First .. Buffer_Last) := Data;
+      pragma Assert (Ctx.Buffer.all (RFLX_Types.To_Index (Field_First (Ctx, F_Data)) .. RFLX_Types.To_Index (Field_Last (Ctx, F_Data))) = Data);
    end Set_Data;
 
    procedure Generic_Set_Data (Ctx : in out Context; Length : RFLX_Types.Length) is

diff --git a/tests/integration/messages_with_implict_size/generated/rflx-universal-message.ads b/tests/integration/messages_with_implict_size/generated/rflx-universal-message.ads
@@ -408,7 +408,9 @@ is
        Has_Buffer (Ctx)
        and then Structural_Valid (Ctx, F_Data)
        and then Valid_Next (Ctx, F_Data)
-       and then Data'Length >= RFLX_Types.To_Length (Field_Size (Ctx, F_Data));
+       and then Data'Length = RFLX_Types.To_Length (Field_Size (Ctx, F_Data)),
+     Post =>
+       Equal (Ctx, F_Data, Data);
 
    generic
       with procedure Process_Data (Data : RFLX_Types.Bytes);
@@ -845,6 +847,7 @@ is
        and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0
        and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0
        and then Valid_Length (Ctx, F_Data, Data'Length)
+       and then Available_Space (Ctx, F_Data) >= Data'Length * RFLX_Types.Byte'Size
        and then Field_Condition (Ctx, F_Data, 0),
      Post =>
        Has_Buffer (Ctx)
@@ -860,7 +863,8 @@ is
        and Ctx.Last = Ctx.Last'Old
        and Predecessor (Ctx, F_Data) = Predecessor (Ctx, F_Data)'Old
        and Valid_Next (Ctx, F_Data) = Valid_Next (Ctx, F_Data)'Old
-       and Get_Message_Type (Ctx) = Get_Message_Type (Ctx)'Old;
+       and Get_Message_Type (Ctx) = Get_Message_Type (Ctx)'Old
+       and Equal (Ctx, F_Data, Data);
 
    generic
       with procedure Process_Data (Data : out RFLX_Types.Bytes);

diff --git a/tests/integration/messages_with_implict_size/generated/rflx-universal-option.adb b/tests/integration/messages_with_implict_size/generated/rflx-universal-option.adb
@@ -403,12 +403,13 @@ is
    end Initialize_Data;
 
    procedure Set_Data (Ctx : in out Context; Data : RFLX_Types.Bytes) is
-      First : constant RFLX_Types.Bit_Index := Field_First (Ctx, F_Data);
-      Buffer_First : constant RFLX_Types.Index := RFLX_Types.To_Index (First);
+      Buffer_First : constant RFLX_Types.Index := RFLX_Types.To_Index (Field_First (Ctx, F_Data));
       Buffer_Last : constant RFLX_Types.Index := Buffer_First + Data'Length - 1;
    begin
       Initialize_Data_Private (Ctx, Data'Length);
+      pragma Assert (Buffer_Last = RFLX_Types.To_Index (Field_Last (Ctx, F_Data)));
       Ctx.Buffer.all (Buffer_First .. Buffer_Last) := Data;
+      pragma Assert (Ctx.Buffer.all (RFLX_Types.To_Index (Field_First (Ctx, F_Data)) .. RFLX_Types.To_Index (Field_Last (Ctx, F_Data))) = Data);
    end Set_Data;
 
    procedure Generic_Set_Data (Ctx : in out Context; Length : RFLX_Types.Length) is

diff --git a/tests/integration/messages_with_implict_size/generated/rflx-universal-option.ads b/tests/integration/messages_with_implict_size/generated/rflx-universal-option.ads
@@ -401,7 +401,9 @@ is
        Has_Buffer (Ctx)
        and then Structural_Valid (Ctx, F_Data)
        and then Valid_Next (Ctx, F_Data)
-       and then Data'Length >= RFLX_Types.To_Length (Field_Size (Ctx, F_Data));
+       and then Data'Length = RFLX_Types.To_Length (Field_Size (Ctx, F_Data)),
+     Post =>
+       Equal (Ctx, F_Data, Data);
 
    generic
       with procedure Process_Data (Data : RFLX_Types.Bytes);
@@ -528,6 +530,7 @@ is
        and then Field_Last (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0
        and then Field_Size (Ctx, F_Data) mod RFLX_Types.Byte'Size = 0
        and then Valid_Length (Ctx, F_Data, Data'Length)
+       and then Available_Space (Ctx, F_Data) >= Data'Length * RFLX_Types.Byte'Size
        and then Field_Condition (Ctx, F_Data, 0),
      Post =>
        Has_Buffer (Ctx)
@@ -540,7 +543,8 @@ is
        and Predecessor (Ctx, F_Data) = Predecessor (Ctx, F_Data)'Old
        and Valid_Next (Ctx, F_Data) = Valid_Next (Ctx, F_Data)'Old
        and Get_Option_Type (Ctx) = Get_Option_Type (Ctx)'Old
-       and Get_Length (Ctx) = Get_Length (Ctx)'Old;
+       and Get_Length (Ctx) = Get_Length (Ctx)'Old
+       and Equal (Ctx, F_Data, Data);
 
    generic
       with procedure Process_Data (Data : out RFLX_Types.Bytes);