Skip to content

Commit

Permalink
Remove unnecessary checking of buffer sizes
Browse files Browse the repository at this point in the history
Ref. #1131
  • Loading branch information
treiher committed Aug 22, 2022
1 parent fa44bab commit c6c5573
Show file tree
Hide file tree
Showing 5 changed files with 87 additions and 177 deletions.
125 changes: 76 additions & 49 deletions rflx/generator/session.py
Original file line number Diff line number Diff line change
Expand Up @@ -2212,12 +2212,14 @@ def _assign( # pylint: disable = too-many-arguments
return self._assign_to_selected(target, expression, exception_handler, is_global)

if isinstance(expression, expr.Head):
return self._assign_to_head(target, expression, exception_handler, is_global, alloc_id)
return self._assign_to_head(
target, expression, exception_handler, is_global, state, alloc_id
)

if isinstance(expression, expr.Comprehension):
assert isinstance(target_type, rty.Sequence)
return self._assign_to_comprehension(
target, target_type, expression, exception_handler, is_global, alloc_id
target, target_type, expression, exception_handler, is_global, state, alloc_id
)

if isinstance(expression, expr.Call):
Expand Down Expand Up @@ -2536,12 +2538,13 @@ def _assign_to_delta_message_aggregate(
],
]

def _assign_to_head(
def _assign_to_head( # pylint: disable = too-many-arguments
self,
target: ID,
head: expr.Head,
exception_handler: ExceptionHandler,
is_global: Callable[[ID], bool],
state: ID,
alloc_id: Optional[Location],
) -> Sequence[Statement]:
assert isinstance(head.prefix.type_, (rty.Sequence, rty.Aggregate))
Expand All @@ -2556,16 +2559,19 @@ def _assign_to_head(

if isinstance(head.prefix, expr.Comprehension):
return self._assign_to_head_comprehension(
target, head, exception_handler, is_global, alloc_id
target, head, exception_handler, is_global, state, alloc_id
)
return self._assign_to_head_sequence(target, head, exception_handler, is_global, alloc_id)
return self._assign_to_head_sequence(
target, head, exception_handler, is_global, state, alloc_id
)

def _assign_to_head_comprehension( # pylint: disable = too-many-locals
def _assign_to_head_comprehension( # pylint: disable = too-many-arguments, too-many-locals
self,
target: ID,
head: expr.Head,
exception_handler: ExceptionHandler,
is_global: Callable[[ID], bool],
state: ID,
alloc_id: Optional[Location],
) -> Sequence[Statement]:
comprehension = head.prefix
Expand Down Expand Up @@ -2650,6 +2656,8 @@ def comprehension_statements(
message_id = ID(selected.prefix.name)
message_type = selected.prefix.type_.identifier
message_field = selected.selector
source_buffer_size = self._allocator.get_size(message_id, state)
target_buffer_size = self._allocator.get_size(target, state)

return [
self._if_structural_valid_message(
Expand All @@ -2663,6 +2671,7 @@ def comprehension_statements(
sequence_id,
sequence_type_id,
comprehension_statements,
target_buffer_size < source_buffer_size,
exception_handler,
is_global,
alloc_id,
Expand All @@ -2679,12 +2688,13 @@ def comprehension_statements(
location=comprehension.sequence.location,
)

def _assign_to_head_sequence( # pylint: disable = too-many-locals
def _assign_to_head_sequence( # pylint: disable = too-many-arguments, too-many-locals
self,
target: ID,
head: expr.Head,
exception_handler: ExceptionHandler,
is_global: Callable[[ID], bool],
state: ID,
alloc_id: Optional[Location],
) -> Sequence[Statement]:
assert isinstance(head.prefix.type_, rty.Sequence)
Expand Down Expand Up @@ -2740,6 +2750,8 @@ def _assign_to_head_sequence( # pylint: disable = too-many-locals
target_buffer = buffer_id("RFLX_Target_" + target)
element_context = ID("RFLX_Head_Ctx")
copied_sequence_context = context_id(copy_id(sequence_id), is_global)
source_buffer_size = self._allocator.get_size(sequence_id, state)
target_buffer_size = self._allocator.get_size(target, state)

def statements(exception_handler: ExceptionHandler) -> list[Statement]:
update_context = self._update_context(
Expand Down Expand Up @@ -2795,6 +2807,7 @@ def statements(exception_handler: ExceptionHandler) -> list[Statement]:
target_type,
element_context,
target_buffer,
target_buffer_size < source_buffer_size,
local_exception_handler.copy(
[
CallStatement(
Expand Down Expand Up @@ -2859,6 +2872,7 @@ def _assign_to_comprehension( # pylint: disable = too-many-arguments
comprehension: expr.Comprehension,
exception_handler: ExceptionHandler,
is_global: Callable[[ID], bool],
state: ID,
alloc_id: Optional[Location],
) -> Sequence[Statement]:
# pylint: disable = too-many-locals
Expand Down Expand Up @@ -2929,6 +2943,8 @@ def statements(local_exception_handler: ExceptionHandler) -> list[Statement]:
location=selected.location,
)
message_field = selected.selector
source_buffer_size = self._allocator.get_size(message_id, state)
target_buffer_size = self._allocator.get_size(target, state)

return [
reset_target,
Expand Down Expand Up @@ -2957,6 +2973,7 @@ def statements(local_exception_handler: ExceptionHandler) -> list[Statement]:
alloc_id,
)
],
target_buffer_size < source_buffer_size,
exception_handler,
is_global,
alloc_id,
Expand Down Expand Up @@ -4532,7 +4549,8 @@ def _declare_sequence_copy( # pylint: disable = too-many-arguments
sequence_type,
sequence_context,
copy_id(buffer_id(sequence_identifier)),
exception_handler.copy(free_buffer),
target_buffer_is_smaller=False,
exception_handler=exception_handler.copy(free_buffer),
),
self._initialize_context(
copy_id(sequence_identifier),
Expand Down Expand Up @@ -4560,6 +4578,7 @@ def _declare_message_field_sequence_copy( # pylint: disable = too-many-argument
sequence_identifier: ID,
sequence_type: ID,
statements: Callable[[ExceptionHandler], Sequence[Statement]],
target_buffer_is_smaller: bool,
exception_handler: ExceptionHandler,
is_global: Callable[[ID], bool],
alloc_id: Optional[Location],
Expand All @@ -4576,6 +4595,7 @@ def _declare_message_field_sequence_copy( # pylint: disable = too-many-argument
message_type,
context_id(message_identifier, is_global),
buffer_id(sequence_identifier),
target_buffer_is_smaller,
local_exception_handler,
),
self._if_structural_valid_message_field(
Expand Down Expand Up @@ -4864,7 +4884,8 @@ def _comprehension_assign_element( # pylint: disable = too-many-arguments
target_type_id,
element_id,
buffer_id(target_buffer),
exception_handler,
target_buffer_is_smaller=True,
exception_handler=exception_handler,
),
CallStatement(
target_type_id * "Initialize",
Expand Down Expand Up @@ -5137,54 +5158,60 @@ def _copy_to_buffer(
type_: ID,
source_context: ID,
target_buffer: ID,
target_buffer_is_smaller: bool,
exception_handler: ExceptionHandler,
) -> IfStatement:
) -> Statement:
self._session_context.used_types_body.append(const.TYPES_LENGTH)
return IfStatement(
copy = CallStatement(
type_ * "Copy",
[
(
LessEqual(
Call(
type_ * "Byte_Size",
[Variable(source_context)],
),
Length(target_buffer),
),
[
CallStatement(
type_ * "Copy",
[
Variable(source_context),
Indexed(
Variable(target_buffer * "all"),
ValueRange(
First(target_buffer),
Add(
First(target_buffer),
Call(
const.TYPES_INDEX,
[
Add(
Call(
type_ * "Byte_Size",
[Variable(source_context)],
),
Number(1),
)
],
),
-Number(2),
Variable(source_context),
Indexed(
Variable(target_buffer * "all"),
ValueRange(
First(target_buffer),
Add(
First(target_buffer),
Call(
const.TYPES_INDEX,
[
Add(
Call(
type_ * "Byte_Size",
[Variable(source_context)],
),
),
),
],
Number(1),
)
],
),
-Number(2),
),
],
)
),
),
],
exception_handler.execute(),
)

if target_buffer_is_smaller:
return IfStatement(
[
(
LessEqual(
Call(
type_ * "Byte_Size",
[Variable(source_context)],
),
Length(target_buffer),
),
[
copy,
],
)
],
exception_handler.execute(),
)

return copy

def _convert_type(
self, expression: expr.Expr, target_type: rty.Type, expression_type: rty.Type = None
) -> expr.Expr:
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -173,17 +173,7 @@ is
pragma Warnings (Off, "unused assignment");
Ctx.P.Slots.Slot_Ptr_4 := null;
pragma Warnings (On, "unused assignment");
if Universal.Options.Byte_Size (Ctx.P.Options_Ctx) <= RFLX_Copy_Options_Buffer'Length then
Universal.Options.Copy (Ctx.P.Options_Ctx, RFLX_Copy_Options_Buffer.all (RFLX_Copy_Options_Buffer'First .. RFLX_Copy_Options_Buffer'First + RFLX_Types.Index (Universal.Options.Byte_Size (Ctx.P.Options_Ctx) + 1) - 2));
else
Ctx.P.Next_State := S_Terminated;
pragma Assert (Ctx.P.Slots.Slot_Ptr_4 = null);
pragma Assert (RFLX_Copy_Options_Buffer /= null);
Ctx.P.Slots.Slot_Ptr_4 := RFLX_Copy_Options_Buffer;
pragma Assert (Ctx.P.Slots.Slot_Ptr_4 /= null);
pragma Assert (Process_1_Invariant);
goto Finalize_Process_1;
end if;
Universal.Options.Copy (Ctx.P.Options_Ctx, RFLX_Copy_Options_Buffer.all (RFLX_Copy_Options_Buffer'First .. RFLX_Copy_Options_Buffer'First + RFLX_Types.Index (Universal.Options.Byte_Size (Ctx.P.Options_Ctx) + 1) - 2));
Universal.Options.Initialize (RFLX_Copy_Options_Ctx, RFLX_Copy_Options_Buffer, RFLX_Types.To_First_Bit_Index (RFLX_Copy_Options_Buffer'First), Universal.Options.Sequence_Last (Ctx.P.Options_Ctx));
declare
RFLX_First_Option_Length_Found : Boolean := False;
Expand Down Expand Up @@ -284,17 +274,7 @@ is
pragma Warnings (Off, "unused assignment");
Ctx.P.Slots.Slot_Ptr_5 := null;
pragma Warnings (On, "unused assignment");
if Universal.Options.Byte_Size (Ctx.P.Options_Ctx) <= RFLX_Copy_Options_Buffer'Length then
Universal.Options.Copy (Ctx.P.Options_Ctx, RFLX_Copy_Options_Buffer.all (RFLX_Copy_Options_Buffer'First .. RFLX_Copy_Options_Buffer'First + RFLX_Types.Index (Universal.Options.Byte_Size (Ctx.P.Options_Ctx) + 1) - 2));
else
Ctx.P.Next_State := S_Terminated;
pragma Assert (Ctx.P.Slots.Slot_Ptr_5 = null);
pragma Assert (RFLX_Copy_Options_Buffer /= null);
Ctx.P.Slots.Slot_Ptr_5 := RFLX_Copy_Options_Buffer;
pragma Assert (Ctx.P.Slots.Slot_Ptr_5 /= null);
pragma Assert (Process_1_Invariant);
goto Finalize_Process_1;
end if;
Universal.Options.Copy (Ctx.P.Options_Ctx, RFLX_Copy_Options_Buffer.all (RFLX_Copy_Options_Buffer'First .. RFLX_Copy_Options_Buffer'First + RFLX_Types.Index (Universal.Options.Byte_Size (Ctx.P.Options_Ctx) + 1) - 2));
Universal.Options.Initialize (RFLX_Copy_Options_Ctx, RFLX_Copy_Options_Buffer, RFLX_Types.To_First_Bit_Index (RFLX_Copy_Options_Buffer'First), Universal.Options.Sequence_Last (Ctx.P.Options_Ctx));
declare
RFLX_First_Option_Found : Boolean := False;
Expand Down Expand Up @@ -496,17 +476,7 @@ is
pragma Warnings (Off, "unused assignment");
Ctx.P.Slots.Slot_Ptr_4 := null;
pragma Warnings (On, "unused assignment");
if Universal.Message.Byte_Size (Ctx.P.Message_Ctx) <= RFLX_Message_Options_Buffer'Length then
Universal.Message.Copy (Ctx.P.Message_Ctx, RFLX_Message_Options_Buffer.all (RFLX_Message_Options_Buffer'First .. RFLX_Message_Options_Buffer'First + RFLX_Types.Index (Universal.Message.Byte_Size (Ctx.P.Message_Ctx) + 1) - 2));
else
Ctx.P.Next_State := S_Terminated;
pragma Assert (Ctx.P.Slots.Slot_Ptr_4 = null);
pragma Assert (RFLX_Message_Options_Buffer /= null);
Ctx.P.Slots.Slot_Ptr_4 := RFLX_Message_Options_Buffer;
pragma Assert (Ctx.P.Slots.Slot_Ptr_4 /= null);
pragma Assert (Process_2_Invariant);
goto Finalize_Process_2;
end if;
Universal.Message.Copy (Ctx.P.Message_Ctx, RFLX_Message_Options_Buffer.all (RFLX_Message_Options_Buffer'First .. RFLX_Message_Options_Buffer'First + RFLX_Types.Index (Universal.Message.Byte_Size (Ctx.P.Message_Ctx) + 1) - 2));
if Universal.Message.Structural_Valid (Ctx.P.Message_Ctx, Universal.Message.F_Options) then
Universal.Options.Initialize (RFLX_Message_Options_Ctx, RFLX_Message_Options_Buffer, Universal.Message.Field_First (Ctx.P.Message_Ctx, Universal.Message.F_Options), Universal.Message.Field_Last (Ctx.P.Message_Ctx, Universal.Message.F_Options));
declare
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -86,17 +86,7 @@ is
pragma Warnings (Off, "unused assignment");
Ctx.P.Slots.Slot_Ptr_3 := null;
pragma Warnings (On, "unused assignment");
if Universal.Message.Byte_Size (Ctx.P.Message_Ctx) <= RFLX_Message_Options_Buffer'Length then
Universal.Message.Copy (Ctx.P.Message_Ctx, RFLX_Message_Options_Buffer.all (RFLX_Message_Options_Buffer'First .. RFLX_Message_Options_Buffer'First + RFLX_Types.Index (Universal.Message.Byte_Size (Ctx.P.Message_Ctx) + 1) - 2));
else
Ctx.P.Next_State := S_Terminated;
pragma Assert (Ctx.P.Slots.Slot_Ptr_3 = null);
pragma Assert (RFLX_Message_Options_Buffer /= null);
Ctx.P.Slots.Slot_Ptr_3 := RFLX_Message_Options_Buffer;
pragma Assert (Ctx.P.Slots.Slot_Ptr_3 /= null);
pragma Assert (Process_Invariant);
goto Finalize_Process;
end if;
Universal.Message.Copy (Ctx.P.Message_Ctx, RFLX_Message_Options_Buffer.all (RFLX_Message_Options_Buffer'First .. RFLX_Message_Options_Buffer'First + RFLX_Types.Index (Universal.Message.Byte_Size (Ctx.P.Message_Ctx) + 1) - 2));
if Universal.Message.Structural_Valid (Ctx.P.Message_Ctx, Universal.Message.F_Options) then
Universal.Options.Initialize (RFLX_Message_Options_Ctx, RFLX_Message_Options_Buffer, Universal.Message.Field_First (Ctx.P.Message_Ctx, Universal.Message.F_Options), Universal.Message.Field_Last (Ctx.P.Message_Ctx, Universal.Message.F_Options));
while Universal.Options.Has_Element (RFLX_Message_Options_Ctx) loop
Expand Down Expand Up @@ -193,17 +183,7 @@ is
pragma Warnings (Off, "unused assignment");
Ctx.P.Slots.Slot_Ptr_4 := null;
pragma Warnings (On, "unused assignment");
if Universal.Message.Byte_Size (Ctx.P.Message_Ctx) <= RFLX_Message_Options_Buffer'Length then
Universal.Message.Copy (Ctx.P.Message_Ctx, RFLX_Message_Options_Buffer.all (RFLX_Message_Options_Buffer'First .. RFLX_Message_Options_Buffer'First + RFLX_Types.Index (Universal.Message.Byte_Size (Ctx.P.Message_Ctx) + 1) - 2));
else
Ctx.P.Next_State := S_Terminated;
pragma Assert (Ctx.P.Slots.Slot_Ptr_4 = null);
pragma Assert (RFLX_Message_Options_Buffer /= null);
Ctx.P.Slots.Slot_Ptr_4 := RFLX_Message_Options_Buffer;
pragma Assert (Ctx.P.Slots.Slot_Ptr_4 /= null);
pragma Assert (Process_Invariant);
goto Finalize_Process;
end if;
Universal.Message.Copy (Ctx.P.Message_Ctx, RFLX_Message_Options_Buffer.all (RFLX_Message_Options_Buffer'First .. RFLX_Message_Options_Buffer'First + RFLX_Types.Index (Universal.Message.Byte_Size (Ctx.P.Message_Ctx) + 1) - 2));
if Universal.Message.Structural_Valid (Ctx.P.Message_Ctx, Universal.Message.F_Options) then
Universal.Options.Initialize (RFLX_Message_Options_Ctx, RFLX_Message_Options_Buffer, Universal.Message.Field_First (Ctx.P.Message_Ctx, Universal.Message.F_Options), Universal.Message.Field_Last (Ctx.P.Message_Ctx, Universal.Message.F_Options));
while Universal.Options.Has_Element (RFLX_Message_Options_Ctx) loop
Expand Down

0 comments on commit c6c5573

Please sign in to comment.