From a4d0cf7b013a25387c49eb84238b6f2a9078b337 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 | 66 ++++++++++--------- .../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, 36 insertions(+), 154 deletions(-) diff --git a/rflx/generator/session.py b/rflx/generator/session.py index 3b37172b13..3627b1cdd8 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 [] @@ -4040,6 +4041,7 @@ def _set_message_fields( 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 8a5ee61956..7111b20ee6 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 cdd84a9707..9343b40561 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 505e8d6ad4..4c5509a89e 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 13f8dcfe00..28cd6e1755 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 9dc58e7508..9bdf4b4f29 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 f3da361557..3e8059678b 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));