From 31b0d764288cbc95b1f08c7be2af71a0ae127640 Mon Sep 17 00:00:00 2001 From: Tobias Reiher Date: Wed, 17 Aug 2022 17:46:16 +0200 Subject: [PATCH] Remove redundant checking of available space Ref. #1131 --- rflx/generator/session.py | 68 ++++++++++--------- .../generated/rflx-test-session.adb | 24 ------- .../generated/rflx-test-session.adb | 24 ------- .../generated/rflx-test-session.adb | 24 ------- .../generated/rflx-test-session.adb | 8 --- .../generated/rflx-test-session.adb | 20 ------ .../generated/rflx-test-session.adb | 24 ------- 7 files changed, 37 insertions(+), 155 deletions(-) diff --git a/rflx/generator/session.py b/rflx/generator/session.py index 3b37172b1..3b2878090 100644 --- a/rflx/generator/session.py +++ b/rflx/generator/session.py @@ -3504,6 +3504,7 @@ def check( local_exception_handler, is_global, state, + size_check=False, ) if isinstance(append.parameters[0], expr.MessageAggregate) else [] @@ -4033,13 +4034,14 @@ def _raise_exception_if( ] ) - def _set_message_fields( + def _set_message_fields( # pylint: disable = too-many-arguments self, target_context: ID, message_aggregate: expr.MessageAggregate, exception_handler: ExceptionHandler, is_global: Callable[[ID], bool], state: ID, + size_check: bool = True, ) -> list[Statement]: assert isinstance(message_aggregate.type_, rty.Message) @@ -4047,38 +4049,42 @@ def _set_message_fields( size = self._message_size(message_aggregate) required_space, required_space_precondition = self._required_space(size, is_global, state) - statements: list[Statement] = [ - *( - [ - self._raise_exception_if( - Not(required_space_precondition), - "violated precondition for calculating required space of message for" - f' "{target_context}" (one of the message arguments is invalid or has a too' - " small buffer)", - exception_handler, - ) - ] - if required_space_precondition - else [] - ), - self._raise_exception_if( - Less( - Call( - message_type.identifier * "Available_Space", - [ - Variable(target_context), - Variable( - message_type.identifier - * model.Field(next(iter(message_type.field_types))).affixed_name - ), - ], + statements: list[Statement] = ( + [ + *( + [ + self._raise_exception_if( + Not(required_space_precondition), + "violated precondition for calculating required space of message for" + f' "{target_context}" (one of the message arguments is invalid or has a' + " too small buffer)", + exception_handler, + ) + ] + if required_space_precondition + else [] + ), + self._raise_exception_if( + Less( + Call( + message_type.identifier * "Available_Space", + [ + Variable(target_context), + Variable( + message_type.identifier + * model.Field(next(iter(message_type.field_types))).affixed_name + ), + ], + ), + required_space, ), - required_space, + f'insufficient space in "{target_context}" for creating message', + exception_handler, ), - f'insufficient space in "{target_context}" for creating message', - exception_handler, - ), - ] + ] + if size_check + else [] + ) for f, v in message_aggregate.field_values.items(): if f not in message_type.field_types: diff --git a/tests/integration/session_append_unconstrained/generated/rflx-test-session.adb b/tests/integration/session_append_unconstrained/generated/rflx-test-session.adb index 8a5ee6195..7111b20ee 100644 --- a/tests/integration/session_append_unconstrained/generated/rflx-test-session.adb +++ b/tests/integration/session_append_unconstrained/generated/rflx-test-session.adb @@ -51,14 +51,6 @@ is RFLX_Element_Options_Ctx : Universal.Option.Context; begin Universal.Options.Switch (Options_Ctx, RFLX_Element_Options_Ctx); - if Universal.Option.Available_Space (RFLX_Element_Options_Ctx, Universal.Option.F_Option_Type) < 32 then - Ctx.P.Next_State := S_Terminated; - pragma Warnings (Off, """RFLX_Element_Options_Ctx"" is set by ""Update"" but not used after the call"); - Universal.Options.Update (Options_Ctx, RFLX_Element_Options_Ctx); - pragma Warnings (On, """RFLX_Element_Options_Ctx"" is set by ""Update"" but not used after the call"); - pragma Assert (Start_Invariant); - goto Finalize_Start; - end if; pragma Assert (Universal.Option.Sufficient_Space (RFLX_Element_Options_Ctx, Universal.Option.F_Option_Type)); Universal.Option.Set_Option_Type (RFLX_Element_Options_Ctx, Universal.OT_Data); pragma Assert (Universal.Option.Sufficient_Space (RFLX_Element_Options_Ctx, Universal.Option.F_Length)); @@ -91,14 +83,6 @@ is RFLX_Element_Options_Ctx : Universal.Option.Context; begin Universal.Options.Switch (Options_Ctx, RFLX_Element_Options_Ctx); - if Universal.Option.Available_Space (RFLX_Element_Options_Ctx, Universal.Option.F_Option_Type) < 40 then - Ctx.P.Next_State := S_Terminated; - pragma Warnings (Off, """RFLX_Element_Options_Ctx"" is set by ""Update"" but not used after the call"); - Universal.Options.Update (Options_Ctx, RFLX_Element_Options_Ctx); - pragma Warnings (On, """RFLX_Element_Options_Ctx"" is set by ""Update"" but not used after the call"); - pragma Assert (Start_Invariant); - goto Finalize_Start; - end if; pragma Assert (Universal.Option.Sufficient_Space (RFLX_Element_Options_Ctx, Universal.Option.F_Option_Type)); Universal.Option.Set_Option_Type (RFLX_Element_Options_Ctx, Universal.OT_Data); pragma Assert (Universal.Option.Sufficient_Space (RFLX_Element_Options_Ctx, Universal.Option.F_Length)); @@ -131,14 +115,6 @@ is RFLX_Element_Options_Ctx : Universal.Option.Context; begin Universal.Options.Switch (Options_Ctx, RFLX_Element_Options_Ctx); - if Universal.Option.Available_Space (RFLX_Element_Options_Ctx, Universal.Option.F_Option_Type) < 8 then - Ctx.P.Next_State := S_Terminated; - pragma Warnings (Off, """RFLX_Element_Options_Ctx"" is set by ""Update"" but not used after the call"); - Universal.Options.Update (Options_Ctx, RFLX_Element_Options_Ctx); - pragma Warnings (On, """RFLX_Element_Options_Ctx"" is set by ""Update"" but not used after the call"); - pragma Assert (Start_Invariant); - goto Finalize_Start; - end if; pragma Assert (Universal.Option.Sufficient_Space (RFLX_Element_Options_Ctx, Universal.Option.F_Option_Type)); Universal.Option.Set_Option_Type (RFLX_Element_Options_Ctx, Universal.OT_Null); pragma Warnings (Off, """RFLX_Element_Options_Ctx"" is set by ""Update"" but not used after the call"); diff --git a/tests/integration/session_comprehension_head/generated/rflx-test-session.adb b/tests/integration/session_comprehension_head/generated/rflx-test-session.adb index cdd84a970..9343b4056 100644 --- a/tests/integration/session_comprehension_head/generated/rflx-test-session.adb +++ b/tests/integration/session_comprehension_head/generated/rflx-test-session.adb @@ -45,14 +45,6 @@ is RFLX_Element_Options_Ctx : Universal.Option.Context; begin Universal.Options.Switch (Ctx.P.Options_Ctx, RFLX_Element_Options_Ctx); - if Universal.Option.Available_Space (RFLX_Element_Options_Ctx, Universal.Option.F_Option_Type) < 32 then - Ctx.P.Next_State := S_Terminated; - pragma Warnings (Off, """RFLX_Element_Options_Ctx"" is set by ""Update"" but not used after the call"); - Universal.Options.Update (Ctx.P.Options_Ctx, RFLX_Element_Options_Ctx); - pragma Warnings (On, """RFLX_Element_Options_Ctx"" is set by ""Update"" but not used after the call"); - pragma Assert (Start_Invariant); - goto Finalize_Start; - end if; pragma Assert (Universal.Option.Sufficient_Space (RFLX_Element_Options_Ctx, Universal.Option.F_Option_Type)); Universal.Option.Set_Option_Type (RFLX_Element_Options_Ctx, Universal.OT_Data); pragma Assert (Universal.Option.Sufficient_Space (RFLX_Element_Options_Ctx, Universal.Option.F_Length)); @@ -85,14 +77,6 @@ is RFLX_Element_Options_Ctx : Universal.Option.Context; begin Universal.Options.Switch (Ctx.P.Options_Ctx, RFLX_Element_Options_Ctx); - if Universal.Option.Available_Space (RFLX_Element_Options_Ctx, Universal.Option.F_Option_Type) < 8 then - Ctx.P.Next_State := S_Terminated; - pragma Warnings (Off, """RFLX_Element_Options_Ctx"" is set by ""Update"" but not used after the call"); - Universal.Options.Update (Ctx.P.Options_Ctx, RFLX_Element_Options_Ctx); - pragma Warnings (On, """RFLX_Element_Options_Ctx"" is set by ""Update"" but not used after the call"); - pragma Assert (Start_Invariant); - goto Finalize_Start; - end if; pragma Assert (Universal.Option.Sufficient_Space (RFLX_Element_Options_Ctx, Universal.Option.F_Option_Type)); Universal.Option.Set_Option_Type (RFLX_Element_Options_Ctx, Universal.OT_Null); pragma Warnings (Off, """RFLX_Element_Options_Ctx"" is set by ""Update"" but not used after the call"); @@ -112,14 +96,6 @@ is RFLX_Element_Options_Ctx : Universal.Option.Context; begin Universal.Options.Switch (Ctx.P.Options_Ctx, RFLX_Element_Options_Ctx); - if Universal.Option.Available_Space (RFLX_Element_Options_Ctx, Universal.Option.F_Option_Type) < 40 then - Ctx.P.Next_State := S_Terminated; - pragma Warnings (Off, """RFLX_Element_Options_Ctx"" is set by ""Update"" but not used after the call"); - Universal.Options.Update (Ctx.P.Options_Ctx, RFLX_Element_Options_Ctx); - pragma Warnings (On, """RFLX_Element_Options_Ctx"" is set by ""Update"" but not used after the call"); - pragma Assert (Start_Invariant); - goto Finalize_Start; - end if; pragma Assert (Universal.Option.Sufficient_Space (RFLX_Element_Options_Ctx, Universal.Option.F_Option_Type)); Universal.Option.Set_Option_Type (RFLX_Element_Options_Ctx, Universal.OT_Data); pragma Assert (Universal.Option.Sufficient_Space (RFLX_Element_Options_Ctx, Universal.Option.F_Length)); diff --git a/tests/integration/session_comprehension_on_sequence/generated/rflx-test-session.adb b/tests/integration/session_comprehension_on_sequence/generated/rflx-test-session.adb index 505e8d6ad..4c5509a89 100644 --- a/tests/integration/session_comprehension_on_sequence/generated/rflx-test-session.adb +++ b/tests/integration/session_comprehension_on_sequence/generated/rflx-test-session.adb @@ -48,14 +48,6 @@ is RFLX_Element_Options_Ctx : Universal.Option.Context; begin Universal.Options.Switch (Ctx.P.Options_Ctx, RFLX_Element_Options_Ctx); - if Universal.Option.Available_Space (RFLX_Element_Options_Ctx, Universal.Option.F_Option_Type) < 32 then - Ctx.P.Next_State := S_Terminated; - pragma Warnings (Off, """RFLX_Element_Options_Ctx"" is set by ""Update"" but not used after the call"); - Universal.Options.Update (Ctx.P.Options_Ctx, RFLX_Element_Options_Ctx); - pragma Warnings (On, """RFLX_Element_Options_Ctx"" is set by ""Update"" but not used after the call"); - pragma Assert (Start_Invariant); - goto Finalize_Start; - end if; pragma Assert (Universal.Option.Sufficient_Space (RFLX_Element_Options_Ctx, Universal.Option.F_Option_Type)); Universal.Option.Set_Option_Type (RFLX_Element_Options_Ctx, Universal.OT_Data); pragma Assert (Universal.Option.Sufficient_Space (RFLX_Element_Options_Ctx, Universal.Option.F_Length)); @@ -88,14 +80,6 @@ is RFLX_Element_Options_Ctx : Universal.Option.Context; begin Universal.Options.Switch (Ctx.P.Options_Ctx, RFLX_Element_Options_Ctx); - if Universal.Option.Available_Space (RFLX_Element_Options_Ctx, Universal.Option.F_Option_Type) < 8 then - Ctx.P.Next_State := S_Terminated; - pragma Warnings (Off, """RFLX_Element_Options_Ctx"" is set by ""Update"" but not used after the call"); - Universal.Options.Update (Ctx.P.Options_Ctx, RFLX_Element_Options_Ctx); - pragma Warnings (On, """RFLX_Element_Options_Ctx"" is set by ""Update"" but not used after the call"); - pragma Assert (Start_Invariant); - goto Finalize_Start; - end if; pragma Assert (Universal.Option.Sufficient_Space (RFLX_Element_Options_Ctx, Universal.Option.F_Option_Type)); Universal.Option.Set_Option_Type (RFLX_Element_Options_Ctx, Universal.OT_Null); pragma Warnings (Off, """RFLX_Element_Options_Ctx"" is set by ""Update"" but not used after the call"); @@ -115,14 +99,6 @@ is RFLX_Element_Options_Ctx : Universal.Option.Context; begin Universal.Options.Switch (Ctx.P.Options_Ctx, RFLX_Element_Options_Ctx); - if Universal.Option.Available_Space (RFLX_Element_Options_Ctx, Universal.Option.F_Option_Type) < 40 then - Ctx.P.Next_State := S_Terminated; - pragma Warnings (Off, """RFLX_Element_Options_Ctx"" is set by ""Update"" but not used after the call"); - Universal.Options.Update (Ctx.P.Options_Ctx, RFLX_Element_Options_Ctx); - pragma Warnings (On, """RFLX_Element_Options_Ctx"" is set by ""Update"" but not used after the call"); - pragma Assert (Start_Invariant); - goto Finalize_Start; - end if; pragma Assert (Universal.Option.Sufficient_Space (RFLX_Element_Options_Ctx, Universal.Option.F_Option_Type)); Universal.Option.Set_Option_Type (RFLX_Element_Options_Ctx, Universal.OT_Data); pragma Assert (Universal.Option.Sufficient_Space (RFLX_Element_Options_Ctx, Universal.Option.F_Length)); diff --git a/tests/integration/session_functions_opaque/generated/rflx-test-session.adb b/tests/integration/session_functions_opaque/generated/rflx-test-session.adb index 13f8dcfe0..28cd6e175 100644 --- a/tests/integration/session_functions_opaque/generated/rflx-test-session.adb +++ b/tests/integration/session_functions_opaque/generated/rflx-test-session.adb @@ -148,14 +148,6 @@ is RFLX_Element_Message_Sequence_Ctx : Universal.Option.Context; begin Universal.Options.Switch (Message_Sequence_Ctx, RFLX_Element_Message_Sequence_Ctx); - if Universal.Option.Available_Space (RFLX_Element_Message_Sequence_Ctx, Universal.Option.F_Option_Type) < 40 then - Ctx.P.Next_State := S_Error; - pragma Warnings (Off, """RFLX_Element_Message_Sequence_Ctx"" is set by ""Update"" but not used after the call"); - Universal.Options.Update (Message_Sequence_Ctx, RFLX_Element_Message_Sequence_Ctx); - pragma Warnings (On, """RFLX_Element_Message_Sequence_Ctx"" is set by ""Update"" but not used after the call"); - pragma Assert (Check_Message_Sequence_Invariant); - goto Finalize_Check_Message_Sequence; - end if; pragma Assert (Universal.Option.Sufficient_Space (RFLX_Element_Message_Sequence_Ctx, Universal.Option.F_Option_Type)); Universal.Option.Set_Option_Type (RFLX_Element_Message_Sequence_Ctx, Universal.OT_Data); pragma Assert (Universal.Option.Sufficient_Space (RFLX_Element_Message_Sequence_Ctx, Universal.Option.F_Length)); diff --git a/tests/integration/session_sequence_append/generated/rflx-test-session.adb b/tests/integration/session_sequence_append/generated/rflx-test-session.adb index 9dc58e750..9bdf4b4f2 100644 --- a/tests/integration/session_sequence_append/generated/rflx-test-session.adb +++ b/tests/integration/session_sequence_append/generated/rflx-test-session.adb @@ -82,26 +82,6 @@ is RFLX_Element_Options_Ctx : Universal.Option.Context; begin Universal.Options.Switch (Options_Ctx, RFLX_Element_Options_Ctx); - if - not (Universal.Option.Size (Ctx.P.Option_Ctx) <= 32768 - and then Universal.Option.Size (Ctx.P.Option_Ctx) mod RFLX_Types.Byte'Size = 0 - and then Universal.Option.Structural_Valid (Ctx.P.Option_Ctx, Universal.Option.F_Data)) - then - Ctx.P.Next_State := S_Terminated; - pragma Warnings (Off, """RFLX_Element_Options_Ctx"" is set by ""Update"" but not used after the call"); - Universal.Options.Update (Options_Ctx, RFLX_Element_Options_Ctx); - pragma Warnings (On, """RFLX_Element_Options_Ctx"" is set by ""Update"" but not used after the call"); - pragma Assert (Process_Invariant); - goto Finalize_Process; - end if; - if Universal.Option.Available_Space (RFLX_Element_Options_Ctx, Universal.Option.F_Option_Type) < Universal.Option.Field_Size (Ctx.P.Option_Ctx, Universal.Option.F_Data) + 24 then - Ctx.P.Next_State := S_Terminated; - pragma Warnings (Off, """RFLX_Element_Options_Ctx"" is set by ""Update"" but not used after the call"); - Universal.Options.Update (Options_Ctx, RFLX_Element_Options_Ctx); - pragma Warnings (On, """RFLX_Element_Options_Ctx"" is set by ""Update"" but not used after the call"); - pragma Assert (Process_Invariant); - goto Finalize_Process; - end if; pragma Assert (Universal.Option.Sufficient_Space (RFLX_Element_Options_Ctx, Universal.Option.F_Option_Type)); Universal.Option.Set_Option_Type (RFLX_Element_Options_Ctx, Universal.OT_Data); if Universal.Option.Valid (Ctx.P.Option_Ctx, Universal.Option.F_Length) then diff --git a/tests/integration/session_sequence_append_head/generated/rflx-test-session.adb b/tests/integration/session_sequence_append_head/generated/rflx-test-session.adb index f3da36155..3e8059678 100644 --- a/tests/integration/session_sequence_append_head/generated/rflx-test-session.adb +++ b/tests/integration/session_sequence_append_head/generated/rflx-test-session.adb @@ -47,14 +47,6 @@ is RFLX_Element_Messages_Ctx : TLV.Message.Context; begin TLV.Messages.Switch (Ctx.P.Messages_Ctx, RFLX_Element_Messages_Ctx); - if TLV.Message.Available_Space (RFLX_Element_Messages_Ctx, TLV.Message.F_Tag) < 32 then - Ctx.P.Next_State := S_Terminated; - pragma Warnings (Off, """RFLX_Element_Messages_Ctx"" is set by ""Update"" but not used after the call"); - TLV.Messages.Update (Ctx.P.Messages_Ctx, RFLX_Element_Messages_Ctx); - pragma Warnings (On, """RFLX_Element_Messages_Ctx"" is set by ""Update"" but not used after the call"); - pragma Assert (Global_Invariant); - goto Finalize_Global; - end if; pragma Assert (TLV.Message.Sufficient_Space (RFLX_Element_Messages_Ctx, TLV.Message.F_Tag)); TLV.Message.Set_Tag (RFLX_Element_Messages_Ctx, TLV.Msg_Data); pragma Assert (TLV.Message.Sufficient_Space (RFLX_Element_Messages_Ctx, TLV.Message.F_Length)); @@ -285,14 +277,6 @@ is RFLX_Element_Local_Messages_Ctx : TLV.Message.Context; begin TLV.Messages.Switch (Local_Messages_Ctx, RFLX_Element_Local_Messages_Ctx); - if TLV.Message.Available_Space (RFLX_Element_Local_Messages_Ctx, TLV.Message.F_Tag) < 40 then - Ctx.P.Next_State := S_Terminated; - pragma Warnings (Off, """RFLX_Element_Local_Messages_Ctx"" is set by ""Update"" but not used after the call"); - TLV.Messages.Update (Local_Messages_Ctx, RFLX_Element_Local_Messages_Ctx); - pragma Warnings (On, """RFLX_Element_Local_Messages_Ctx"" is set by ""Update"" but not used after the call"); - pragma Assert (Local_Invariant); - goto Finalize_Local; - end if; pragma Assert (TLV.Message.Sufficient_Space (RFLX_Element_Local_Messages_Ctx, TLV.Message.F_Tag)); TLV.Message.Set_Tag (RFLX_Element_Local_Messages_Ctx, TLV.Msg_Data); pragma Assert (TLV.Message.Sufficient_Space (RFLX_Element_Local_Messages_Ctx, TLV.Message.F_Length)); @@ -325,14 +309,6 @@ is RFLX_Element_Messages_Ctx : TLV.Message.Context; begin TLV.Messages.Switch (Ctx.P.Messages_Ctx, RFLX_Element_Messages_Ctx); - if TLV.Message.Available_Space (RFLX_Element_Messages_Ctx, TLV.Message.F_Tag) < 32 then - Ctx.P.Next_State := S_Terminated; - pragma Warnings (Off, """RFLX_Element_Messages_Ctx"" is set by ""Update"" but not used after the call"); - TLV.Messages.Update (Ctx.P.Messages_Ctx, RFLX_Element_Messages_Ctx); - pragma Warnings (On, """RFLX_Element_Messages_Ctx"" is set by ""Update"" but not used after the call"); - pragma Assert (Local_Invariant); - goto Finalize_Local; - end if; pragma Assert (TLV.Message.Sufficient_Space (RFLX_Element_Messages_Ctx, TLV.Message.F_Tag)); TLV.Message.Set_Tag (RFLX_Element_Messages_Ctx, TLV.Msg_Data); pragma Assert (TLV.Message.Sufficient_Space (RFLX_Element_Messages_Ctx, TLV.Message.F_Length));