Skip to content

Commit

Permalink
Remove redundant checking of available space
Browse files Browse the repository at this point in the history 
Ref. #1131
  • Loading branch information
@treiher
treiher committed Aug 22, 2022
1 parent c6c5573 commit 31b0d76
Show file tree
Hide file tree
Showing 7 changed files with 37 additions and 155 deletions.
68 changes: 37 additions & 31 deletions rflx/generator/session.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3504,6 +3504,7 @@ def check(
local_exception_handler,
is_global,
state,
size_check=False,
)
if isinstance(append.parameters[0], expr.MessageAggregate)
else []
Expand Down Expand Up @@ -4033,52 +4034,57 @@ 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)

message_type = message_aggregate.type_
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:
Expand Down
24 changes: 0 additions & 24 deletions tests/integration/session_append_unconstrained/generated/rflx-test-session.adb
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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));
Expand Down Expand Up @@ -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));
Expand Down Expand Up @@ -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");
Expand Down
24 changes: 0 additions & 24 deletions tests/integration/session_comprehension_head/generated/rflx-test-session.adb
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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));
Expand Down Expand Up @@ -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");
Expand All @@ -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));
Expand Down
24 changes: 0 additions & 24 deletions tests/integration/session_comprehension_on_sequence/generated/rflx-test-session.adb
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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));
Expand Down Expand Up @@ -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");
Expand All @@ -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));
Expand Down
8 changes: 0 additions & 8 deletions tests/integration/session_functions_opaque/generated/rflx-test-session.adb
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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));
Expand Down
20 changes: 0 additions & 20 deletions tests/integration/session_sequence_append/generated/rflx-test-session.adb
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
24 changes: 0 additions & 24 deletions tests/integration/session_sequence_append_head/generated/rflx-test-session.adb
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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));
Expand Down Expand Up @@ -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));
Expand Down Expand Up @@ -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));
Expand Down

0 comments on commit 31b0d76

Please sign in to comment.