Skip to content

Commit

Permalink
Enable comprehensions with message sequence as target
Browse files Browse the repository at this point in the history 
Ref. #890
  • Loading branch information
@treiher
treiher committed Jan 5, 2022
1 parent fe60af1 commit 8dc0e4f
Show file tree
Hide file tree
Showing 118 changed files with 1,350 additions and 227 deletions.
2 changes: 2 additions & 0 deletions rflx/generator/common.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -879,7 +879,9 @@ def create_sequence_instantiation(
element_type_identifier * "Context",
element_type_identifier * "Initialize",
element_type_identifier * "Take_Buffer",
element_type_identifier * "Copy",
element_type_identifier * "Has_Buffer",
element_type_identifier * "Size",
element_type_identifier * "Message_Last",
element_type_identifier * "Initialized",
element_type_identifier * "Structural_Valid_Message",
Expand Down
25 changes: 23 additions & 2 deletions rflx/generator/generator.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2443,7 +2443,16 @@ def __create_size_function() -> UnitPart:
)

return UnitPart(
[SubprogramDeclaration(specification)],
[
SubprogramDeclaration(
specification,
[
Postcondition(
Equal(Mod(Result("Size"), Size(const.TYPES_BYTE)), Number(0)),
)
],
)
],
[
ExpressionFunctionDeclaration(
specification,
Expand Down Expand Up @@ -2474,7 +2483,19 @@ def __create_byte_size_function() -> UnitPart:
)

return UnitPart(
[SubprogramDeclaration(specification)],
[
SubprogramDeclaration(
specification,
[
Postcondition(
Equal(
Result("Byte_Size"),
Call(const.TYPES_TO_LENGTH, [Call("Size", [Variable("Ctx")])]),
)
),
],
)
],
[
ExpressionFunctionDeclaration(
specification,
Expand Down
135 changes: 94 additions & 41 deletions rflx/generator/session.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2230,13 +2230,6 @@ def _assign_to_comprehension(
# pylint: disable = too-many-locals

assert isinstance(comprehension.type_, (rty.Sequence, rty.Aggregate))
if not isinstance(comprehension.type_.element, (rty.Integer, rty.Enumeration)):
fail(
f"creating sequence with element {comprehension.type_.element}"
" using list comprehension not yet supported",
Subsystem.GENERATOR,
location=comprehension.location,
)
assert isinstance(comprehension.sequence.type_, rty.Sequence)

self._session_context.used_types_body.append(const.TYPES_BIT_LENGTH)
Expand Down Expand Up @@ -3406,40 +3399,12 @@ def _comprehension( # pylint: disable = too-many-arguments
condition.substituted(
self._substitution()
).ada_expr(),
[
self._if_sufficient_space_in_sequence(
Size(
ID(
target_type.element.identifier
+ "_Enum"
if isinstance(
target_type.element,
rty.Enumeration,
)
and target_type.element.always_valid
else target_type.element.identifier
)
),
target_type_id,
context_id(target_identifier),
[
CallStatement(
target_type_id * "Append_Element",
[
Variable(
context_id(
target_identifier
)
),
selector.substituted(
self._substitution()
).ada_expr(),
],
)
],
local_exception_handler,
),
],
self._comprehension_append_element(
target_identifier,
target_type,
selector,
local_exception_handler,
),
)
]
)
Expand All @@ -3457,6 +3422,94 @@ def _comprehension( # pylint: disable = too-many-arguments
],
)

def _comprehension_append_element(
self,
target_identifier: ID,
target_type: rty.Sequence,
selector: expr.Expr,
exception_handler: ExceptionHandler,
) -> List[Statement]:
target_type_id = ID(target_type.identifier)
required_space: Expr
append_element: Statement

if isinstance(target_type.element, rty.Message):
if not isinstance(selector, expr.Variable):
fail(
"expressions other than variables not yet supported"
" as selector for message types",
Subsystem.GENERATOR,
location=selector.location,
)

element_id = ID(selector.identifier + "_Ctx")
required_space = Call(
ID(target_type.element.identifier * "Size"),
[Variable(element_id)],
)
append_element = self._if_structural_valid_message(
ID(target_type.element.identifier),
element_id,
[
self._if(
Greater(
Call(
ID(target_type.element.identifier) * "Size",
[
Variable(element_id),
],
),
Number(0),
),
[
CallStatement(
target_type_id * "Append_Element",
[
Variable(context_id(target_identifier)),
Variable(element_id),
],
)
],
"empty messages cannot be appended to sequence",
exception_handler,
)
],
exception_handler,
)

elif isinstance(target_type.element, (rty.Integer, rty.Enumeration)):
required_space = Size(
ID(
target_type.element.identifier + "_Enum"
if isinstance(
target_type.element,
rty.Enumeration,
)
and target_type.element.always_valid
else target_type.element.identifier
)
)
append_element = CallStatement(
target_type_id * "Append_Element",
[
Variable(context_id(target_identifier)),
selector.substituted(self._substitution()).ada_expr(),
],
)

else:
assert False

return [
self._if_sufficient_space_in_sequence(
required_space,
target_type_id,
context_id(target_identifier),
[append_element],
exception_handler,
),
]

def _free_context_buffer(
self, identifier: ID, type_: ID, alloc_id: Optional[Location]
) -> Sequence[Statement]:
Expand Down
6 changes: 6 additions & 0 deletions rflx/templates/rflx_message_sequence.adb
View file
Original file line number Diff line number Diff line change
Expand Up @@ -39,6 +39,12 @@ is
end if;
end Copy;

procedure Append_Element (Ctx : in out Context; Element_Ctx : Element_Context) is
begin
Element_Copy (Element_Ctx, Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.Sequence_Last + 1) .. RFLX_Types.To_Index (Ctx.Sequence_Last + Element_Size (Element_Ctx))));
Ctx.Sequence_Last := Ctx.Sequence_Last + Element_Size (Element_Ctx);
end Append_Element;

procedure Switch (Ctx : in out Context; Element_Ctx : out Element_Context) is
Buffer : RFLX_Types.Bytes_Ptr := Ctx.Buffer;
begin
Expand Down
19 changes: 19 additions & 0 deletions rflx/templates/rflx_message_sequence.ads
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,9 @@ generic
type Element_Context (Buffer_First, Buffer_Last : RFLX_Types.Index; First : RFLX_Types.Bit_Index; Last : RFLX_Types.Bit_Length) is private;
with procedure Element_Initialize (Ctx : out Element_Context; Buffer : in out RFLX_Types.Bytes_Ptr; First : RFLX_Types.Bit_Index; Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length := 0);
with procedure Element_Take_Buffer (Ctx : in out Element_Context; Buffer : out RFLX_Types.Bytes_Ptr);
with procedure Element_Copy (Ctx : Element_Context; Buffer : out RFLX_Types.Bytes);
with function Element_Has_Buffer (Ctx : Element_Context) return Boolean;
with function Element_Size (Ctx : Element_Context) return RFLX_Types.Bit_Length;
with function Element_Last (Ctx : Element_Context) return RFLX_Types.Bit_Index;
with function Element_Initialized (Ctx : Element_Context) return Boolean;
with function Element_Valid_Message (Ctx : Element_Context) return Boolean;
Expand Down Expand Up @@ -115,6 +117,23 @@ is
(Has_Buffer (Ctx) => (Has_Element'Result or not Has_Element'Result) and Has_Buffer (Ctx),
not Has_Buffer (Ctx) => (Has_Element'Result or not Has_Element'Result) and not Has_Buffer (Ctx));

procedure Append_Element (Ctx : in out Context; Element_Ctx : Element_Context) with
Pre =>
(Has_Buffer (Ctx)
and then Valid (Ctx)
and then Element_Has_Buffer (Element_Ctx)
and then Element_Valid_Message (Element_Ctx)
and then Element_Size (Element_Ctx) > 0
and then Available_Space (Ctx) >= Element_Size (Element_Ctx)),
Post =>
(Has_Buffer (Ctx)
and Valid (Ctx)
and Sequence_Last (Ctx) = Sequence_Last (Ctx)'Old + Element_Size (Element_Ctx)
and Ctx.Buffer_First = Ctx.Buffer_First'Old
and Ctx.Buffer_Last = Ctx.Buffer_Last'Old
and Ctx.First = Ctx.First'Old
and Ctx.Last = Ctx.Last'Old);

procedure Switch (Ctx : in out Context; Element_Ctx : out Element_Context) with
Pre =>
(not Element_Ctx'Constrained
Expand Down
6 changes: 6 additions & 0 deletions tests/integration/messages/generated/rflx-rflx_message_sequence.adb
View file
Original file line number Diff line number Diff line change
Expand Up @@ -39,6 +39,12 @@ is
end if;
end Copy;

procedure Append_Element (Ctx : in out Context; Element_Ctx : Element_Context) is
begin
Element_Copy (Element_Ctx, Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.Sequence_Last + 1) .. RFLX_Types.To_Index (Ctx.Sequence_Last + Element_Size (Element_Ctx))));
Ctx.Sequence_Last := Ctx.Sequence_Last + Element_Size (Element_Ctx);
end Append_Element;

procedure Switch (Ctx : in out Context; Element_Ctx : out Element_Context) is
Buffer : RFLX_Types.Bytes_Ptr := Ctx.Buffer;
begin
Expand Down
19 changes: 19 additions & 0 deletions tests/integration/messages/generated/rflx-rflx_message_sequence.ads
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,9 @@ generic
type Element_Context (Buffer_First, Buffer_Last : RFLX_Types.Index; First : RFLX_Types.Bit_Index; Last : RFLX_Types.Bit_Length) is private;
with procedure Element_Initialize (Ctx : out Element_Context; Buffer : in out RFLX_Types.Bytes_Ptr; First : RFLX_Types.Bit_Index; Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length := 0);
with procedure Element_Take_Buffer (Ctx : in out Element_Context; Buffer : out RFLX_Types.Bytes_Ptr);
with procedure Element_Copy (Ctx : Element_Context; Buffer : out RFLX_Types.Bytes);
with function Element_Has_Buffer (Ctx : Element_Context) return Boolean;
with function Element_Size (Ctx : Element_Context) return RFLX_Types.Bit_Length;
with function Element_Last (Ctx : Element_Context) return RFLX_Types.Bit_Index;
with function Element_Initialized (Ctx : Element_Context) return Boolean;
with function Element_Valid_Message (Ctx : Element_Context) return Boolean;
Expand Down Expand Up @@ -115,6 +117,23 @@ is
(Has_Buffer (Ctx) => (Has_Element'Result or not Has_Element'Result) and Has_Buffer (Ctx),
not Has_Buffer (Ctx) => (Has_Element'Result or not Has_Element'Result) and not Has_Buffer (Ctx));

procedure Append_Element (Ctx : in out Context; Element_Ctx : Element_Context) with
Pre =>
(Has_Buffer (Ctx)
and then Valid (Ctx)
and then Element_Has_Buffer (Element_Ctx)
and then Element_Valid_Message (Element_Ctx)
and then Element_Size (Element_Ctx) > 0
and then Available_Space (Ctx) >= Element_Size (Element_Ctx)),
Post =>
(Has_Buffer (Ctx)
and Valid (Ctx)
and Sequence_Last (Ctx) = Sequence_Last (Ctx)'Old + Element_Size (Element_Ctx)
and Ctx.Buffer_First = Ctx.Buffer_First'Old
and Ctx.Buffer_Last = Ctx.Buffer_Last'Old
and Ctx.First = Ctx.First'Old
and Ctx.Last = Ctx.Last'Old);

procedure Switch (Ctx : in out Context; Element_Ctx : out Element_Context) with
Pre =>
(not Element_Ctx'Constrained
Expand Down
8 changes: 6 additions & 2 deletions tests/integration/messages/generated/rflx-universal-message.ads
View file
Original file line number Diff line number Diff line change
Expand Up @@ -224,9 +224,13 @@ is
Pre =>
Has_Buffer (Ctx);

function Size (Ctx : Context) return RFLX_Types.Bit_Length;
function Size (Ctx : Context) return RFLX_Types.Bit_Length with
Post =>
Size'Result mod RFLX_Types.Byte'Size = 0;

function Byte_Size (Ctx : Context) return RFLX_Types.Length;
function Byte_Size (Ctx : Context) return RFLX_Types.Length with
Post =>
Byte_Size'Result = RFLX_Types.To_Length (Size (Ctx));

function Message_Last (Ctx : Context) return RFLX_Types.Bit_Length with
Pre =>
Expand Down
8 changes: 6 additions & 2 deletions tests/integration/messages/generated/rflx-universal-option.ads
View file
Original file line number Diff line number Diff line change
Expand Up @@ -219,9 +219,13 @@ is
Pre =>
Has_Buffer (Ctx);

function Size (Ctx : Context) return RFLX_Types.Bit_Length;
function Size (Ctx : Context) return RFLX_Types.Bit_Length with
Post =>
Size'Result mod RFLX_Types.Byte'Size = 0;

function Byte_Size (Ctx : Context) return RFLX_Types.Length;
function Byte_Size (Ctx : Context) return RFLX_Types.Length with
Post =>
Byte_Size'Result = RFLX_Types.To_Length (Size (Ctx));

function Message_Last (Ctx : Context) return RFLX_Types.Bit_Length with
Pre =>
Expand Down
2 changes: 1 addition & 1 deletion tests/integration/messages/generated/rflx-universal-options.ads
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,4 +7,4 @@ pragma Warnings (Off, "unit ""*RFLX_Types"" is not referenced");
with RFLX.RFLX_Types;
pragma Warnings (On, "unit ""*RFLX_Types"" is not referenced");

package RFLX.Universal.Options is new RFLX.RFLX_Message_Sequence (RFLX.Universal.Option.Context, RFLX.Universal.Option.Initialize, RFLX.Universal.Option.Take_Buffer, RFLX.Universal.Option.Has_Buffer, RFLX.Universal.Option.Message_Last, RFLX.Universal.Option.Initialized, RFLX.Universal.Option.Structural_Valid_Message);
package RFLX.Universal.Options is new RFLX.RFLX_Message_Sequence (RFLX.Universal.Option.Context, RFLX.Universal.Option.Initialize, RFLX.Universal.Option.Take_Buffer, RFLX.Universal.Option.Copy, RFLX.Universal.Option.Has_Buffer, RFLX.Universal.Option.Size, RFLX.Universal.Option.Message_Last, RFLX.Universal.Option.Initialized, RFLX.Universal.Option.Structural_Valid_Message);
6 changes: 6 additions & 0 deletions tests/integration/messages_with_implict_size/generated/rflx-rflx_message_sequence.adb
View file
Original file line number Diff line number Diff line change
Expand Up @@ -39,6 +39,12 @@ is
end if;
end Copy;

procedure Append_Element (Ctx : in out Context; Element_Ctx : Element_Context) is
begin
Element_Copy (Element_Ctx, Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.Sequence_Last + 1) .. RFLX_Types.To_Index (Ctx.Sequence_Last + Element_Size (Element_Ctx))));
Ctx.Sequence_Last := Ctx.Sequence_Last + Element_Size (Element_Ctx);
end Append_Element;

procedure Switch (Ctx : in out Context; Element_Ctx : out Element_Context) is
Buffer : RFLX_Types.Bytes_Ptr := Ctx.Buffer;
begin
Expand Down
19 changes: 19 additions & 0 deletions tests/integration/messages_with_implict_size/generated/rflx-rflx_message_sequence.ads
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,9 @@ generic
type Element_Context (Buffer_First, Buffer_Last : RFLX_Types.Index; First : RFLX_Types.Bit_Index; Last : RFLX_Types.Bit_Length) is private;
with procedure Element_Initialize (Ctx : out Element_Context; Buffer : in out RFLX_Types.Bytes_Ptr; First : RFLX_Types.Bit_Index; Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length := 0);
with procedure Element_Take_Buffer (Ctx : in out Element_Context; Buffer : out RFLX_Types.Bytes_Ptr);
with procedure Element_Copy (Ctx : Element_Context; Buffer : out RFLX_Types.Bytes);
with function Element_Has_Buffer (Ctx : Element_Context) return Boolean;
with function Element_Size (Ctx : Element_Context) return RFLX_Types.Bit_Length;
with function Element_Last (Ctx : Element_Context) return RFLX_Types.Bit_Index;
with function Element_Initialized (Ctx : Element_Context) return Boolean;
with function Element_Valid_Message (Ctx : Element_Context) return Boolean;
Expand Down Expand Up @@ -115,6 +117,23 @@ is
(Has_Buffer (Ctx) => (Has_Element'Result or not Has_Element'Result) and Has_Buffer (Ctx),
not Has_Buffer (Ctx) => (Has_Element'Result or not Has_Element'Result) and not Has_Buffer (Ctx));

procedure Append_Element (Ctx : in out Context; Element_Ctx : Element_Context) with
Pre =>
(Has_Buffer (Ctx)
and then Valid (Ctx)
and then Element_Has_Buffer (Element_Ctx)
and then Element_Valid_Message (Element_Ctx)
and then Element_Size (Element_Ctx) > 0
and then Available_Space (Ctx) >= Element_Size (Element_Ctx)),
Post =>
(Has_Buffer (Ctx)
and Valid (Ctx)
and Sequence_Last (Ctx) = Sequence_Last (Ctx)'Old + Element_Size (Element_Ctx)
and Ctx.Buffer_First = Ctx.Buffer_First'Old
and Ctx.Buffer_Last = Ctx.Buffer_Last'Old
and Ctx.First = Ctx.First'Old
and Ctx.Last = Ctx.Last'Old);

procedure Switch (Ctx : in out Context; Element_Ctx : out Element_Context) with
Pre =>
(not Element_Ctx'Constrained
Expand Down
8 changes: 6 additions & 2 deletions tests/integration/messages_with_implict_size/generated/rflx-universal-message.ads
View file
Original file line number Diff line number Diff line change
Expand Up @@ -224,9 +224,13 @@ is
Pre =>
Has_Buffer (Ctx);

function Size (Ctx : Context) return RFLX_Types.Bit_Length;
function Size (Ctx : Context) return RFLX_Types.Bit_Length with
Post =>
Size'Result mod RFLX_Types.Byte'Size = 0;

function Byte_Size (Ctx : Context) return RFLX_Types.Length;
function Byte_Size (Ctx : Context) return RFLX_Types.Length with
Post =>
Byte_Size'Result = RFLX_Types.To_Length (Size (Ctx));

function Message_Last (Ctx : Context) return RFLX_Types.Bit_Length with
Pre =>
Expand Down
Loading

0 comments on commit 8dc0e4f

Please sign in to comment.