Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Fix missing reset in assignment to comprehension #1050

Merged
merged 1 commit into from
May 24, 2022
Merged

Fix missing reset in assignment to comprehension #1050

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 7 additions & 0 deletions rflx/generator/session.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2652,18 +2652,24 @@ def _assign_to_comprehension( # pylint: disable = too-many-arguments
self._session_context.used_types_body.append(const.TYPES_BIT_LENGTH)

target_id = ID(target)
target_context = context_id(target_id, is_global)
sequence_type_id = ID(comprehension.sequence.type_.identifier)
iterator_id = ID(comprehension.iterator)

sequence_element_type = comprehension.sequence.type_.element

reset_target = CallStatement(
ID(target_type.identifier) * "Reset", [Variable(target_context)]
)

if isinstance(sequence_element_type, rty.Message):
iterator_type_id = ID(sequence_element_type.identifier)

if isinstance(comprehension.sequence, expr.Variable):
sequence_id = ID(rid.ID(f"{comprehension.sequence}"))
with exception_handler.local() as local_exception_handler:
return [
reset_target,
self._declare_sequence_copy(
sequence_id,
sequence_type_id,
Expand Down Expand Up @@ -2710,6 +2716,7 @@ def _assign_to_comprehension( # pylint: disable = too-many-arguments

with exception_handler.local() as local_exception_handler:
return [
reset_target,
self._if_structural_valid_message(
message_type,
context_id(message_id, is_global),
Expand Down
89 changes: 85 additions & 4 deletions tests/integration/session_comprehension_on_message_field/generated/rflx-test-session.adb
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,8 @@ is
function Start_Invariant return Boolean is
(Ctx.P.Slots.Slot_Ptr_1 = null
and Ctx.P.Slots.Slot_Ptr_2 /= null
and Ctx.P.Slots.Slot_Ptr_3 /= null)
and Ctx.P.Slots.Slot_Ptr_3 /= null
and Ctx.P.Slots.Slot_Ptr_4 /= null)
with
Annotate =>
(GNATprove, Inline_For_Proof),
Expand Down Expand Up @@ -61,7 +62,8 @@ is
and Option_Types_Ctx.Buffer_Last = RFLX.RFLX_Types.Index'First + 4095
and Ctx.P.Slots.Slot_Ptr_2 = null
and Ctx.P.Slots.Slot_Ptr_1 = null
and Ctx.P.Slots.Slot_Ptr_3 /= null)
and Ctx.P.Slots.Slot_Ptr_3 /= null
and Ctx.P.Slots.Slot_Ptr_4 /= null)
with
Annotate =>
(GNATprove, Inline_For_Proof),
Expand All @@ -75,6 +77,7 @@ is
Universal.Option_Types.Initialize (Option_Types_Ctx, Option_Types_Buffer);
pragma Assert (Process_Invariant);
-- tests/integration/session_comprehension_on_message_field/test.rflx:27:10
Universal.Option_Types.Reset (Option_Types_Ctx);
if Universal.Message.Structural_Valid_Message (Ctx.P.Message_Ctx) then
declare
RFLX_Message_Options_Ctx : Universal.Options.Context;
Expand Down Expand Up @@ -151,6 +154,83 @@ is
goto Finalize_Process;
end if;
-- tests/integration/session_comprehension_on_message_field/test.rflx:29:10
Universal.Option_Types.Reset (Option_Types_Ctx);
if Universal.Message.Structural_Valid_Message (Ctx.P.Message_Ctx) then
declare
RFLX_Message_Options_Ctx : Universal.Options.Context;
RFLX_Message_Options_Buffer : RFLX_Types.Bytes_Ptr;
begin
RFLX_Message_Options_Buffer := Ctx.P.Slots.Slot_Ptr_4;
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
RFLX_Exception := True;
end if;
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
pragma Loop_Invariant (Universal.Options.Has_Buffer (RFLX_Message_Options_Ctx));
pragma Loop_Invariant (Universal.Option_Types.Has_Buffer (Option_Types_Ctx));
pragma Loop_Invariant (RFLX_Message_Options_Ctx.Buffer_First = RFLX_Message_Options_Ctx.Buffer_First'Loop_Entry);
pragma Loop_Invariant (Option_Types_Ctx.Buffer_First = Option_Types_Ctx.Buffer_First'Loop_Entry);
pragma Loop_Invariant (RFLX_Message_Options_Ctx.Buffer_Last = RFLX_Message_Options_Ctx.Buffer_Last'Loop_Entry);
pragma Loop_Invariant (Option_Types_Ctx.Buffer_Last = Option_Types_Ctx.Buffer_Last'Loop_Entry);
pragma Loop_Invariant (Universal.Option_Types.Valid (Option_Types_Ctx));
declare
E_Ctx : Universal.Option.Context;
begin
Universal.Options.Switch (RFLX_Message_Options_Ctx, E_Ctx);
Universal.Option.Verify_Message (E_Ctx);
if Universal.Option.Valid (E_Ctx, Universal.Option.F_Option_Type) then
if
Universal.Option.Get_Option_Type (E_Ctx).Known
and then Universal.Option.Get_Option_Type (E_Ctx).Enum = Universal.OT_Data
then
if
Universal.Option_Types.Has_Element (Option_Types_Ctx)
and then Universal.Option_Types.Available_Space (Option_Types_Ctx) >= Universal.Option_Type_Enum'Size
then
Universal.Option_Types.Append_Element (Option_Types_Ctx, Universal.Option.Get_Option_Type (E_Ctx));
else
RFLX_Exception := True;
end if;
end if;
else
RFLX_Exception := True;
end if;
pragma Warnings (Off, """E_Ctx"" is set by ""Update"" but not used after the call");
Universal.Options.Update (RFLX_Message_Options_Ctx, E_Ctx);
pragma Warnings (On, """E_Ctx"" is set by ""Update"" but not used after the call");
end;
exit when RFLX_Exception;
end loop;
pragma Warnings (Off, """RFLX_Message_Options_Ctx"" is set by ""Take_Buffer"" but not used after the call");
Universal.Options.Take_Buffer (RFLX_Message_Options_Ctx, RFLX_Message_Options_Buffer);
pragma Warnings (On, """RFLX_Message_Options_Ctx"" is set by ""Take_Buffer"" but not used after the call");
else
RFLX_Exception := True;
end if;
Ctx.P.Slots.Slot_Ptr_4 := RFLX_Message_Options_Buffer;
end;
else
Ctx.P.Next_State := S_Terminated;
pragma Assert (Process_Invariant);
goto Finalize_Process;
end if;
if RFLX_Exception then
Ctx.P.Next_State := S_Terminated;
pragma Assert (Process_Invariant);
goto Finalize_Process;
end if;
if RFLX_Exception then
Ctx.P.Next_State := S_Terminated;
pragma Assert (Process_Invariant);
goto Finalize_Process;
end if;
-- tests/integration/session_comprehension_on_message_field/test.rflx:31:10
if
Universal.Option_Types.Size (Option_Types_Ctx) <= 32768
and then Universal.Option_Types.Size (Option_Types_Ctx) mod RFLX_Types.Byte'Size = 0
Expand Down Expand Up @@ -195,14 +275,15 @@ is
function Reply_Invariant return Boolean is
(Ctx.P.Slots.Slot_Ptr_1 = null
and Ctx.P.Slots.Slot_Ptr_2 /= null
and Ctx.P.Slots.Slot_Ptr_3 /= null)
and Ctx.P.Slots.Slot_Ptr_3 /= null
and Ctx.P.Slots.Slot_Ptr_4 /= null)
with
Annotate =>
(GNATprove, Inline_For_Proof),
Ghost;
begin
pragma Assert (Reply_Invariant);
-- tests/integration/session_comprehension_on_message_field/test.rflx:40:10
-- tests/integration/session_comprehension_on_message_field/test.rflx:42:10
Ctx.P.Next_State := S_Terminated;
pragma Assert (Reply_Invariant);
end Reply;
Expand Down
2 changes: 2 additions & 0 deletions ...egration/session_comprehension_on_message_field/generated/rflx-test-session_allocator.adb
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@ is
S.Slot_Ptr_1 := M.Slot_1'Unrestricted_Access;
S.Slot_Ptr_2 := M.Slot_2'Unrestricted_Access;
S.Slot_Ptr_3 := M.Slot_3'Unrestricted_Access;
S.Slot_Ptr_4 := M.Slot_4'Unrestricted_Access;
end Initialize;

procedure Finalize (S : in out Slots) with
Expand All @@ -23,6 +24,7 @@ is
S.Slot_Ptr_1 := null;
S.Slot_Ptr_2 := null;
S.Slot_Ptr_3 := null;
S.Slot_Ptr_4 := null;
end Finalize;

end RFLX.Test.Session_Allocator;
11 changes: 8 additions & 3 deletions ...egration/session_comprehension_on_message_field/generated/rflx-test-session_allocator.ads
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@ is
Slot_1 : aliased RFLX_Types.Bytes (RFLX_Types.Index'First .. RFLX_Types.Index'First + 4095) := (others => 0);
Slot_2 : aliased RFLX_Types.Bytes (RFLX_Types.Index'First .. RFLX_Types.Index'First + 4095) := (others => 0);
Slot_3 : aliased RFLX_Types.Bytes (RFLX_Types.Index'First .. RFLX_Types.Index'First + 4095) := (others => 0);
Slot_4 : aliased RFLX_Types.Bytes (RFLX_Types.Index'First .. RFLX_Types.Index'First + 4095) := (others => 0);
end record;

subtype Slot_Ptr_Type_4096 is RFLX_Types.Bytes_Ptr with
Expand All @@ -28,17 +29,20 @@ is
Slot_Ptr_1 : Slot_Ptr_Type_4096;
Slot_Ptr_2 : Slot_Ptr_Type_4096;
Slot_Ptr_3 : Slot_Ptr_Type_4096;
Slot_Ptr_4 : Slot_Ptr_Type_4096;
end record;

function Initialized (S : Slots) return Boolean is
(S.Slot_Ptr_1 /= null
and S.Slot_Ptr_2 /= null
and S.Slot_Ptr_3 /= null);
and S.Slot_Ptr_3 /= null
and S.Slot_Ptr_4 /= null);

function Uninitialized (S : Slots) return Boolean is
(S.Slot_Ptr_1 = null
and S.Slot_Ptr_2 = null
and S.Slot_Ptr_3 = null);
and S.Slot_Ptr_3 = null
and S.Slot_Ptr_4 = null);

procedure Initialize (S : out Slots; M : Memory) with
Post =>
Expand All @@ -51,6 +55,7 @@ is
function Global_Allocated (S : Slots) return Boolean is
(S.Slot_Ptr_1 = null
and S.Slot_Ptr_2 /= null
and S.Slot_Ptr_3 /= null);
and S.Slot_Ptr_3 /= null
and S.Slot_Ptr_4 /= null);

end RFLX.Test.Session_Allocator;
2 changes: 2 additions & 0 deletions tests/integration/session_comprehension_on_message_field/test.rflx
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -25,6 +25,8 @@ package Test is
begin
-- §S-S-A-A-LC, §S-E-LC-S, §S-E-LC-SMS, §S-E-LC-TSS, §S-E-LC-CS, §S-E-LC-A, §S-E-S-V
Option_Types := [for E in Message.Options if E.Option_Type = Universal::OT_Data => E.Option_Type];
-- Test that target sequence is reset by assignment
Option_Types := [for E in Message.Options if E.Option_Type = Universal::OT_Data => E.Option_Type];
-- §S-S-A-A-MA
Message := Universal::Message'(Message_Type => Universal::MT_Option_Types,
Length => Option_Types'Size / 8,
Expand Down
Loading