Check preconditions before calling To_Context

Ref. #1054

rflx/generator/message.py

@@ -2924,7 +2924,8 @@ def create_structure(message: Message, prefix: str) -> UnitPart:
     unit += _create_structure_type(message, prefix)
     unit += _create_valid_structure_function(message, prefix)
     unit += _create_to_structure_procedure(message)
-    unit += _create_to_context_procedure(message, prefix)
+    unit += _create_sufficient_buffer_length_function(message, prefix)
+    unit += _create_to_context_procedure(message)
     return unit
 
 
@@ -3032,6 +3033,56 @@ def _create_valid_structure_function(message: Message, prefix: str) -> UnitPart:
     )
 
 
+def _create_sufficient_buffer_length_function(message: Message, prefix: str) -> UnitPart:
+    assert len(message.paths(FINAL)) == 1
+
+    specification = FunctionSpecification(
+        "Sufficient_Buffer_Length",
+        "Boolean",
+        [
+            Parameter(["Ctx"], "Context"),
+            Parameter(["Struct" if not message.has_fixed_size else "Unused_Struct"], "Structure"),
+        ],
+    )
+    message_size = message.size()
+
+    return UnitPart(
+        [
+            SubprogramDeclaration(
+                specification,
+                [],
+            )
+        ],
+        private=[
+            ExpressionFunctionDeclaration(
+                specification,
+                GreaterEqual(
+                    Call(
+                        const.TYPES_U64,
+                        [
+                            Add(
+                                Call(
+                                    const.TYPES * "To_Last_Bit_Index",
+                                    [Variable("Ctx.Buffer_Last")],
+                                ),
+                                -Call(
+                                    const.TYPES * "To_First_Bit_Index",
+                                    [Variable("Ctx.Buffer_First")],
+                                ),
+                                Number(1),
+                            )
+                        ],
+                    ),
+                    message_size.substituted(_struct_substitution(message))
+                    .substituted(common.substitution(message, prefix))
+                    .simplified()
+                    .ada_expr(),
+                ),
+            ),
+        ],
+    )
+
+
 def _create_to_structure_procedure(message: Message) -> UnitPart:
     assert len(message.paths(FINAL)) == 1
 
@@ -3165,7 +3216,7 @@ def func(expression: expr.Expr) -> expr.Expr:
     return func
 
 
-def _create_to_context_procedure(message: Message, prefix: str) -> UnitPart:
+def _create_to_context_procedure(message: Message) -> UnitPart:
     assert len(message.paths(FINAL)) == 1
 
     body: ty.List[Statement] = [CallStatement("Reset", [Variable("Ctx")])]
@@ -3237,7 +3288,6 @@ def _create_to_context_procedure(message: Message, prefix: str) -> UnitPart:
         "To_Context",
         [Parameter(["Struct"], "Structure"), InOutParameter(["Ctx"], "Context")],
     )
-    message_size = message.size()
 
     return UnitPart(
         [
@@ -3246,31 +3296,10 @@ def _create_to_context_procedure(message: Message, prefix: str) -> UnitPart:
                 [
                     Precondition(
                         AndThen(
-                            Call("Valid_Structure", [Variable("Struct")]),
                             Not(Constrained("Ctx")),
                             Call("Has_Buffer", [Variable("Ctx")]),
-                            GreaterEqual(
-                                Call(
-                                    const.TYPES_U64,
-                                    [
-                                        Add(
-                                            Call(
-                                                const.TYPES * "To_Last_Bit_Index",
-                                                [Variable("Ctx.Buffer_Last")],
-                                            ),
-                                            -Call(
-                                                const.TYPES * "To_First_Bit_Index",
-                                                [Variable("Ctx.Buffer_First")],
-                                            ),
-                                            Number(1),
-                                        )
-                                    ],
-                                ),
-                                message_size.substituted(_struct_substitution(message))
-                                .substituted(common.substitution(message, prefix))
-                                .simplified()
-                                .ada_expr(),
-                            ),
+                            Call("Valid_Structure", [Variable("Struct")]),
+                            Call("Sufficient_Buffer_Length", [Variable("Ctx"), Variable("Struct")]),
                         )
                     ),
                     Postcondition(

rflx/generator/session.py

@@ -2782,6 +2782,7 @@ def _assign_to_call(  # pylint: disable = too-many-locals
         post_call = []
         local_declarations = []
         target_id = variable_id(target, is_global)
+        message_id = context_id(target, is_global)
 
         if isinstance(call_expr.type_, rty.Message):
             type_identifier = self._ada_type(call_expr.type_.identifier)
@@ -2795,13 +2796,23 @@ def _assign_to_call(  # pylint: disable = too-many-locals
                 self._if(
                     Call(ID(type_identifier) * "Valid_Structure", [Variable(target_id)]),
                     [
-                        CallStatement(
-                            ID(type_identifier) * "To_Context",
+                        self._if(
+                            Call(
+                                ID(type_identifier) * "Sufficient_Buffer_Length",
+                                [Variable(message_id), Variable(target_id)],
+                            ),
                             [
-                                Variable(target_id),
-                                Variable(context_id(target, is_global)),
+                                CallStatement(
+                                    ID(type_identifier) * "To_Context",
+                                    [
+                                        Variable(target_id),
+                                        Variable(message_id),
+                                    ],
+                                ),
                             ],
-                        ),
+                            f'insufficient space for converting message "{target}"',
+                            exception_handler,
+                        )
                     ],
                     f'"{call_expr.identifier}" returned an invalid message',
                     exception_handler,

tests/integration/session_endianness/generated/rflx-messages-msg.ads

@@ -456,12 +456,14 @@ is
      Post =>
        Valid_Structure (Struct);
 
+   function Sufficient_Buffer_Length (Ctx : Context; Unused_Struct : Structure) return Boolean;
+
    procedure To_Context (Struct : Structure; Ctx : in out Context) with
      Pre =>
-       Valid_Structure (Struct)
-       and then not Ctx'Constrained
+       not Ctx'Constrained
        and then Has_Buffer (Ctx)
-       and then RFLX_Types.U64 (RFLX_Types.To_Last_Bit_Index (Ctx.Buffer_Last) - RFLX_Types.To_First_Bit_Index (Ctx.Buffer_First) + 1) >= 64,
+       and then Valid_Structure (Struct)
+       and then Sufficient_Buffer_Length (Ctx, Struct),
      Post =>
        Has_Buffer (Ctx)
        and Structural_Valid_Message (Ctx)
@@ -695,4 +697,7 @@ private
    function Valid_Structure (Unused_Struct : Structure) return Boolean is
      (True);
 
+   function Sufficient_Buffer_Length (Ctx : Context; Unused_Struct : Structure) return Boolean is
+     (RFLX_Types.U64 (RFLX_Types.To_Last_Bit_Index (Ctx.Buffer_Last) - RFLX_Types.To_First_Bit_Index (Ctx.Buffer_First) + 1) >= 64);
+
 end RFLX.Messages.Msg;

tests/integration/session_endianness/generated/rflx-messages-msg_le.ads

@@ -456,12 +456,14 @@ is
      Post =>
        Valid_Structure (Struct);
 
+   function Sufficient_Buffer_Length (Ctx : Context; Unused_Struct : Structure) return Boolean;
+
    procedure To_Context (Struct : Structure; Ctx : in out Context) with
      Pre =>
-       Valid_Structure (Struct)
-       and then not Ctx'Constrained
+       not Ctx'Constrained
        and then Has_Buffer (Ctx)
-       and then RFLX_Types.U64 (RFLX_Types.To_Last_Bit_Index (Ctx.Buffer_Last) - RFLX_Types.To_First_Bit_Index (Ctx.Buffer_First) + 1) >= 64,
+       and then Valid_Structure (Struct)
+       and then Sufficient_Buffer_Length (Ctx, Struct),
      Post =>
        Has_Buffer (Ctx)
        and Structural_Valid_Message (Ctx)
@@ -695,4 +697,7 @@ private
    function Valid_Structure (Unused_Struct : Structure) return Boolean is
      (True);
 
+   function Sufficient_Buffer_Length (Ctx : Context; Unused_Struct : Structure) return Boolean is
+     (RFLX_Types.U64 (RFLX_Types.To_Last_Bit_Index (Ctx.Buffer_Last) - RFLX_Types.To_First_Bit_Index (Ctx.Buffer_First) + 1) >= 64);
+
 end RFLX.Messages.Msg_LE;

tests/integration/session_endianness/generated/rflx-messages-msg_le_nested.ads

@@ -489,12 +489,14 @@ is
      Post =>
        Valid_Structure (Struct);
 
+   function Sufficient_Buffer_Length (Ctx : Context; Unused_Struct : Structure) return Boolean;
+
    procedure To_Context (Struct : Structure; Ctx : in out Context) with
      Pre =>
-       Valid_Structure (Struct)
-       and then not Ctx'Constrained
+       not Ctx'Constrained
        and then Has_Buffer (Ctx)
-       and then RFLX_Types.U64 (RFLX_Types.To_Last_Bit_Index (Ctx.Buffer_Last) - RFLX_Types.To_First_Bit_Index (Ctx.Buffer_First) + 1) >= 96,
+       and then Valid_Structure (Struct)
+       and then Sufficient_Buffer_Length (Ctx, Struct),
      Post =>
        Has_Buffer (Ctx)
        and Structural_Valid_Message (Ctx)
@@ -746,4 +748,7 @@ private
    function Valid_Structure (Unused_Struct : Structure) return Boolean is
      (True);
 
+   function Sufficient_Buffer_Length (Ctx : Context; Unused_Struct : Structure) return Boolean is
+     (RFLX_Types.U64 (RFLX_Types.To_Last_Bit_Index (Ctx.Buffer_Last) - RFLX_Types.To_First_Bit_Index (Ctx.Buffer_First) + 1) >= 96);
+
 end RFLX.Messages.Msg_LE_Nested;

tests/integration/session_functions/generated/rflx-test-definite_message.ads

@@ -606,12 +606,14 @@ is
      Post =>
        Valid_Structure (Struct);
 
+   function Sufficient_Buffer_Length (Ctx : Context; Struct : Structure) return Boolean;
+
    procedure To_Context (Struct : Structure; Ctx : in out Context) with
      Pre =>
-       Valid_Structure (Struct)
-       and then not Ctx'Constrained
+       not Ctx'Constrained
        and then Has_Buffer (Ctx)
-       and then RFLX_Types.U64 (RFLX_Types.To_Last_Bit_Index (Ctx.Buffer_Last) - RFLX_Types.To_First_Bit_Index (Ctx.Buffer_First) + 1) >= RFLX_Types.U64 (Struct.Length) * 8 + 16,
+       and then Valid_Structure (Struct)
+       and then Sufficient_Buffer_Length (Ctx, Struct),
      Post =>
        Has_Buffer (Ctx)
        and Structural_Valid_Message (Ctx)
@@ -864,4 +866,7 @@ private
    function Valid_Structure (Struct : Structure) return Boolean is
      (RFLX.Universal.Valid_Option_Type (Struct.Message_Type));
 
+   function Sufficient_Buffer_Length (Ctx : Context; Struct : Structure) return Boolean is
+     (RFLX_Types.U64 (RFLX_Types.To_Last_Bit_Index (Ctx.Buffer_Last) - RFLX_Types.To_First_Bit_Index (Ctx.Buffer_First) + 1) >= RFLX_Types.U64 (Struct.Length) * 8 + 16);
+
 end RFLX.Test.Definite_Message;

tests/integration/session_functions/generated/rflx-test-session.adb

@@ -83,7 +83,13 @@ is
             Universal.Message.Get_Data (Ctx.P.Message_Ctx, RFLX_Create_Message_Arg_2_Message (RFLX_Types.Index'First .. RFLX_Types.Index'First + RFLX_Types.Index (RFLX_Create_Message_Arg_2_Message_Length) - 2));
             Create_Message (Ctx, Message_Type, Length, RFLX_Create_Message_Arg_2_Message (RFLX_Types.Index'First .. RFLX_Types.Index'First + RFLX_Types.Index (RFLX_Create_Message_Arg_2_Message_Length) - 2), Definite_Message);
             if Test.Definite_Message.Valid_Structure (Definite_Message) then
-               Test.Definite_Message.To_Context (Definite_Message, Ctx.P.Definite_Message_Ctx);
+               if Test.Definite_Message.Sufficient_Buffer_Length (Ctx.P.Definite_Message_Ctx, Definite_Message) then
+                  Test.Definite_Message.To_Context (Definite_Message, Ctx.P.Definite_Message_Ctx);
+               else
+                  Ctx.P.Next_State := S_Terminated;
+                  pragma Assert (Process_Invariant);
+                  goto Finalize_Process;
+               end if;
             else
                Ctx.P.Next_State := S_Terminated;
                pragma Assert (Process_Invariant);
@@ -156,7 +162,13 @@ is
          Universal.Message.Data (Ctx.P.Message_Ctx, RFLX_Create_Message_Arg_2_Message (RFLX_Types.Index'First .. RFLX_Types.Index'First + RFLX_Types.Index (RFLX_Create_Message_Arg_2_Message_Length + 1) - 2));
          Create_Message (Ctx, (Known => True, Enum => Universal.OT_Data), Length, RFLX_Create_Message_Arg_2_Message (RFLX_Types.Index'First .. RFLX_Types.Index'First + RFLX_Types.Index (RFLX_Create_Message_Arg_2_Message_Length + 1) - 2), Definite_Message);
          if Test.Definite_Message.Valid_Structure (Definite_Message) then
-            Test.Definite_Message.To_Context (Definite_Message, Ctx.P.Definite_Message_Ctx);
+            if Test.Definite_Message.Sufficient_Buffer_Length (Ctx.P.Definite_Message_Ctx, Definite_Message) then
+               Test.Definite_Message.To_Context (Definite_Message, Ctx.P.Definite_Message_Ctx);
+            else
+               Ctx.P.Next_State := S_Terminated;
+               pragma Assert (Process_2_Invariant);
+               goto Finalize_Process_2;
+            end if;
          else
             Ctx.P.Next_State := S_Terminated;
             pragma Assert (Process_2_Invariant);

tests/spark/generated/rflx-enumeration-message.ads

@@ -425,12 +425,14 @@ is
      Post =>
        Valid_Structure (Struct);
 
+   function Sufficient_Buffer_Length (Ctx : Context; Unused_Struct : Structure) return Boolean;
+
    procedure To_Context (Struct : Structure; Ctx : in out Context) with
      Pre =>
-       Valid_Structure (Struct)
-       and then not Ctx'Constrained
+       not Ctx'Constrained
        and then Has_Buffer (Ctx)
-       and then RFLX_Types.U64 (RFLX_Types.To_Last_Bit_Index (Ctx.Buffer_Last) - RFLX_Types.To_First_Bit_Index (Ctx.Buffer_First) + 1) >= 8,
+       and then Valid_Structure (Struct)
+       and then Sufficient_Buffer_Length (Ctx, Struct),
      Post =>
        Has_Buffer (Ctx)
        and Structural_Valid_Message (Ctx)
@@ -646,4 +648,7 @@ private
    function Valid_Structure (Struct : Structure) return Boolean is
      (RFLX.Enumeration.Valid_Priority (Struct.Priority));
 
+   function Sufficient_Buffer_Length (Ctx : Context; Unused_Struct : Structure) return Boolean is
+     (RFLX_Types.U64 (RFLX_Types.To_Last_Bit_Index (Ctx.Buffer_Last) - RFLX_Types.To_First_Bit_Index (Ctx.Buffer_First) + 1) >= 8);
+
 end RFLX.Enumeration.Message;

tests/spark/generated/rflx-expression-message.ads

@@ -504,12 +504,14 @@ is
      Post =>
        Valid_Structure (Struct);
 
+   function Sufficient_Buffer_Length (Ctx : Context; Unused_Struct : Structure) return Boolean;
+
    procedure To_Context (Struct : Structure; Ctx : in out Context) with
      Pre =>
-       Valid_Structure (Struct)
-       and then not Ctx'Constrained
+       not Ctx'Constrained
        and then Has_Buffer (Ctx)
-       and then RFLX_Types.U64 (RFLX_Types.To_Last_Bit_Index (Ctx.Buffer_Last) - RFLX_Types.To_First_Bit_Index (Ctx.Buffer_First) + 1) >= 16,
+       and then Valid_Structure (Struct)
+       and then Sufficient_Buffer_Length (Ctx, Struct),
      Post =>
        Has_Buffer (Ctx)
        and Structural_Valid_Message (Ctx)
@@ -724,4 +726,7 @@ private
    function Valid_Structure (Struct : Structure) return Boolean is
      (Struct.Payload = (1, 2));
 
+   function Sufficient_Buffer_Length (Ctx : Context; Unused_Struct : Structure) return Boolean is
+     (RFLX_Types.U64 (RFLX_Types.To_Last_Bit_Index (Ctx.Buffer_Last) - RFLX_Types.To_First_Bit_Index (Ctx.Buffer_First) + 1) >= 16);
+
 end RFLX.Expression.Message;

tests/spark/generated/rflx-fixed_size-simple_message.ads

@@ -552,12 +552,14 @@ is
      Post =>
        Valid_Structure (Struct);
 
+   function Sufficient_Buffer_Length (Ctx : Context; Unused_Struct : Structure) return Boolean;
+
    procedure To_Context (Struct : Structure; Ctx : in out Context) with
      Pre =>
-       Valid_Structure (Struct)
-       and then not Ctx'Constrained
+       not Ctx'Constrained
        and then Has_Buffer (Ctx)
-       and then RFLX_Types.U64 (RFLX_Types.To_Last_Bit_Index (Ctx.Buffer_Last) - RFLX_Types.To_First_Bit_Index (Ctx.Buffer_First) + 1) >= 32,
+       and then Valid_Structure (Struct)
+       and then Sufficient_Buffer_Length (Ctx, Struct),
      Post =>
        Has_Buffer (Ctx)
        and Structural_Valid_Message (Ctx)
@@ -804,4 +806,7 @@ private
       and then (To_U64 (Struct.Message_Type) = RFLX_Types.U64 (To_U64 (RFLX.Universal.OT_Null))
                 or To_U64 (Struct.Message_Type) = RFLX_Types.U64 (To_U64 (RFLX.Universal.OT_Data))));
 
+   function Sufficient_Buffer_Length (Ctx : Context; Unused_Struct : Structure) return Boolean is
+     (RFLX_Types.U64 (RFLX_Types.To_Last_Bit_Index (Ctx.Buffer_Last) - RFLX_Types.To_First_Bit_Index (Ctx.Buffer_First) + 1) >= 32);
+
 end RFLX.Fixed_Size.Simple_Message;

tests/spark/generated/rflx-sequence-inner_message.ads

@@ -568,12 +568,14 @@ is
      Post =>
        Valid_Structure (Struct);
 
+   function Sufficient_Buffer_Length (Ctx : Context; Struct : Structure) return Boolean;
+
    procedure To_Context (Struct : Structure; Ctx : in out Context) with
      Pre =>
-       Valid_Structure (Struct)
-       and then not Ctx'Constrained
+       not Ctx'Constrained
        and then Has_Buffer (Ctx)
-       and then RFLX_Types.U64 (RFLX_Types.To_Last_Bit_Index (Ctx.Buffer_Last) - RFLX_Types.To_First_Bit_Index (Ctx.Buffer_First) + 1) >= RFLX_Types.U64 (Struct.Length) * 8 + 8,
+       and then Valid_Structure (Struct)
+       and then Sufficient_Buffer_Length (Ctx, Struct),
      Post =>
        Has_Buffer (Ctx)
        and Structural_Valid_Message (Ctx)
@@ -806,4 +808,7 @@ private
    function Valid_Structure (Unused_Struct : Structure) return Boolean is
      (True);
 
+   function Sufficient_Buffer_Length (Ctx : Context; Struct : Structure) return Boolean is
+     (RFLX_Types.U64 (RFLX_Types.To_Last_Bit_Index (Ctx.Buffer_Last) - RFLX_Types.To_First_Bit_Index (Ctx.Buffer_First) + 1) >= RFLX_Types.U64 (Struct.Length) * 8 + 8);
+
 end RFLX.Sequence.Inner_Message;