Skip to content

Commit

Permalink
Improve flexibility of Read/Write interface of messages
Browse files Browse the repository at this point in the history 
Ref. #807
  • Loading branch information
@treiher
treiher committed Nov 24, 2021
1 parent 75d4c80 commit b500c1e
Show file tree
Hide file tree
Showing 107 changed files with 2,449 additions and 664 deletions.
27 changes: 25 additions & 2 deletions rflx/ada.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -435,6 +435,27 @@ class Succ(AttributeExpr):
pass


class BinAttributeExpr(Attribute):
def __init__(
self, prefix: Union[StrID, Expr], left: Expr, right: Expr, negative: bool = False
) -> None:
self.left = left
self.right = right
super().__init__(prefix)

@property
def _representation(self) -> str:
return f"{self.prefix}'{self.__class__.__name__} ({self.left}, {self.right})"


class Min(BinAttributeExpr):
pass


class Max(BinAttributeExpr):
pass


@invariant(lambda self: len(self.elements) > 0)
class Indexed(Name):
def __init__(self, prefix: Expr, *elements: Expr, negative: bool = False) -> None:
Expand Down Expand Up @@ -1028,14 +1049,16 @@ def __str__(self) -> str:


class FormalSubprogramDeclaration(FormalDeclaration):
def __init__(self, specification: "SubprogramSpecification") -> None:
def __init__(self, specification: "SubprogramSpecification", default: StrID = None) -> None:
self.specification = specification
self.default = ID(default) if default else None

def __hash__(self) -> int:
return hash(self.specification)

def __str__(self) -> str:
return f"with {self.specification};"
default = f" is {self.default}" if self.default else ""
return f"with {self.specification}{default};"


class FormalPackageDeclaration(FormalDeclaration):
Expand Down
196 changes: 162 additions & 34 deletions rflx/generator/generator.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -60,6 +60,7 @@
Less,
LessEqual,
LoopEntry,
Max,
Mod,
ModularType,
NamedAggregate,
Expand Down Expand Up @@ -375,9 +376,11 @@ def __create_message(self, message: Message) -> None:
unit += self.__create_restricted_reset_procedure(message)
unit += self.__create_take_buffer_procedure(message)
unit += self.__create_copy_procedure()
unit += self.__create_read_procedure()
unit += self.__create_write_procedure(message)
unit += self.__create_read_function()
unit += self.__create_generic_read_procedure()
unit += self.__create_generic_write_procedure(message)
unit += self.__create_has_buffer_function()
unit += self.__create_buffer_length_function()
unit += self.__create_size_function()
unit += self.__create_byte_size_function()
unit += self.__create_message_last_function()
Expand Down Expand Up @@ -1262,9 +1265,10 @@ def __create_copy_procedure() -> UnitPart:
)

@staticmethod
def __create_read_procedure() -> UnitPart:
specification = ProcedureSpecification(
def __create_read_function() -> UnitPart:
specification = FunctionSpecification(
"Read",
const.TYPES_BYTES,
[Parameter(["Ctx"], "Context")],
)

Expand All @@ -1280,60 +1284,138 @@ def __create_read_procedure() -> UnitPart:
)
),
],
)
],
[
ExpressionFunctionDeclaration(
specification,
Indexed(
Variable("Ctx.Buffer.all"),
ValueRange(
Call(const.TYPES_TO_INDEX, [Variable("Ctx.First")]),
Call(const.TYPES_TO_INDEX, [Variable("Ctx.Message_Last")]),
),
),
)
],
)

@staticmethod
def __create_generic_read_procedure() -> UnitPart:
specification = ProcedureSpecification(
"Generic_Read",
[Parameter(["Ctx"], "Context")],
)

return UnitPart(
[
Pragma(
"Warnings",
[Variable("Off"), String('formal parameter "*" is not referenced')],
),
ExpressionFunctionDeclaration(
FunctionSpecification(
"Always_Valid",
"Boolean",
[Parameter(["Buffer"], const.TYPES_BYTES)],
),
TRUE,
aspects=[Ghost()],
),
Pragma(
"Warnings",
[Variable("On"), String('formal parameter "*" is not referenced')],
),
SubprogramDeclaration(
specification,
[
Precondition(
AndThen(
Call("Has_Buffer", [Variable("Ctx")]),
Call("Structural_Valid_Message", [Variable("Ctx")]),
Call("Pre", [Call("Read", [Variable("Ctx")])]),
)
),
],
[
FormalSubprogramDeclaration(
ProcedureSpecification(
"Read",
[Parameter(["Buffer"], const.TYPES_BYTES)],
)
),
FormalSubprogramDeclaration(
FunctionSpecification(
"Pre",
"Boolean",
[Parameter(["Buffer"], const.TYPES_BYTES)],
),
"Always_Valid",
),
],
)
),
],
[
SubprogramBody(
specification,
[],
[
CallStatement(
"Read",
[
Indexed(
Variable("Ctx.Buffer.all"),
ValueRange(
Call(const.TYPES_TO_INDEX, [Variable("Ctx.First")]),
Call(const.TYPES_TO_INDEX, [Variable("Ctx.Message_Last")]),
),
)
],
)
CallStatement("Read", [Call("Read", [Variable("Ctx")])]),
],
)
],
)

@staticmethod
def __create_write_procedure(message: Message) -> UnitPart:
def __create_generic_write_procedure(message: Message) -> UnitPart:
"""
Write data into the buffer of the context using an externally provided subprogram.
The complete buffer of the context can be overwritten. Buffer bounds that were set during
the initialization of the context will not be considered or preserved.
"""
specification = ProcedureSpecification(
"Write",
[InOutParameter(["Ctx"], "Context")],
"Generic_Write",
[
InOutParameter(["Ctx"], "Context"),
Parameter(["Offset"], const.TYPES_LENGTH, Number(0)),
],
)

return UnitPart(
[
Pragma(
"Warnings",
[Variable("Off"), String('formal parameter "*" is not referenced')],
),
ExpressionFunctionDeclaration(
FunctionSpecification(
"Always_Valid",
"Boolean",
[
Parameter(["Context_Buffer_Length"], const.TYPES_LENGTH),
Parameter(["Offset"], const.TYPES_LENGTH),
],
),
TRUE,
aspects=[Ghost()],
),
Pragma(
"Warnings",
[Variable("On"), String('formal parameter "*" is not referenced')],
),
SubprogramDeclaration(
specification,
[
Precondition(
And(
AndThen(
Not(Constrained("Ctx")),
Call("Has_Buffer", [Variable("Ctx")]),
Less(Variable("Offset"), Call("Buffer_Length", [Variable("Ctx")])),
Call(
"Pre",
[Call("Buffer_Length", [Variable("Ctx")]), Variable("Offset")],
),
)
),
Postcondition(
Expand Down Expand Up @@ -1364,11 +1446,24 @@ def __create_write_procedure(message: Message) -> UnitPart:
[
OutParameter(["Buffer"], const.TYPES_BYTES),
OutParameter(["Length"], const.TYPES_LENGTH),
Parameter(["Context_Buffer_Length"], const.TYPES_LENGTH),
Parameter(["Offset"], const.TYPES_LENGTH),
],
)
),
FormalSubprogramDeclaration(
FunctionSpecification(
"Pre",
"Boolean",
[
Parameter(["Context_Buffer_Length"], const.TYPES_LENGTH),
Parameter(["Offset"], const.TYPES_LENGTH),
],
),
"Always_Valid",
),
],
)
),
],
[
SubprogramBody(
Expand All @@ -1378,8 +1473,20 @@ def __create_write_procedure(message: Message) -> UnitPart:
CallStatement(
"Write",
[
Variable("Ctx.Buffer.all"),
Slice(
Variable("Ctx.Buffer.all"),
Add(
First("Ctx.Buffer"),
Call(
const.TYPES_INDEX, [Add(Variable("Offset"), Number(1))]
),
-Number(1),
),
Last("Ctx.Buffer"),
),
Variable("Length"),
Length("Ctx.Buffer"),
Variable("Offset"),
],
),
# ISSUE: Componolit/Workarounds#39
Expand All @@ -1406,18 +1513,23 @@ def __create_write_procedure(message: Message) -> UnitPart:
Call(
const.TYPES_TO_FIRST_BIT_INDEX, [Variable("Ctx.Buffer_First")]
),
Call(
const.TYPES_TO_LAST_BIT_INDEX,
[
Add(
Call(
const.TYPES_LENGTH,
[Variable("Ctx.Buffer_First")],
Max(
const.TYPES_BIT_INDEX,
Variable("Ctx.Last"),
Call(
const.TYPES_TO_LAST_BIT_INDEX,
[
Add(
Call(
const.TYPES_LENGTH,
[Variable("Ctx.Buffer_First")],
),
Variable("Offset"),
Variable("Length"),
-Number(1),
),
Variable("Length"),
-Number(1),
),
],
],
),
),
*[
Variable(ID("Ctx" * p.identifier))
Expand Down Expand Up @@ -2091,6 +2203,22 @@ def __create_has_buffer_function() -> UnitPart:
],
)

@staticmethod
def __create_buffer_length_function() -> UnitPart:
specification = FunctionSpecification(
"Buffer_Length", const.TYPES_LENGTH, [Parameter(["Ctx"], "Context")]
)

return UnitPart(
[
SubprogramDeclaration(
specification,
[Precondition(Call("Has_Buffer", [Variable("Ctx")]))],
)
],
private=[ExpressionFunctionDeclaration(specification, Length("Ctx.Buffer"))],
)

@staticmethod
def __create_valid_predecessor_function(
message: Message, composite_fields: ty.Sequence[Field]
Expand Down
4 changes: 2 additions & 2 deletions rflx/generator/session.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1926,7 +1926,7 @@ def _read(read: stmt.Read) -> Sequence[Statement]:
[
GenericProcedureInstantiation(
identifier,
ProcedureSpecification(target_type * "Write"),
ProcedureSpecification(target_type * "Generic_Write"),
[f"{read.identifier}_Read"],
)
],
Expand Down Expand Up @@ -1966,7 +1966,7 @@ def write_statements(exception_handler: ExceptionHandler) -> Sequence[Statement]
[
GenericProcedureInstantiation(
identifier,
ProcedureSpecification(target_type * "Read"),
ProcedureSpecification(target_type * "Generic_Read"),
[f"{write.identifier}_Write"],
)
],
Expand Down
17 changes: 10 additions & 7 deletions tests/integration/messages/generated/rflx-universal-message.adb
View file
Original file line number Diff line number Diff line change
Expand Up @@ -43,18 +43,21 @@ is
end if;
end Copy;

procedure Read (Ctx : Context) is
function Read (Ctx : Context) return RFLX_Types.Bytes is
(Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Message_Last)));

procedure Generic_Read (Ctx : Context) is
begin
Read (Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Message_Last)));
end Read;
Read (Read (Ctx));
end Generic_Read;

procedure Write (Ctx : in out Context) is
procedure Generic_Write (Ctx : in out Context; Offset : RFLX_Types.Length := 0) is
Length : RFLX_Types.Length;
begin
Write (Ctx.Buffer.all, Length);
Write (Ctx.Buffer.all (Ctx.Buffer'First + RFLX_Types.Index (Offset + 1) - 1 .. Ctx.Buffer'Last), Length, Ctx.Buffer'Length, Offset);
pragma Assert (Length <= Ctx.Buffer.all'Length, "Length <= Buffer'Length is not ensured by postcondition of ""Write""");
Reset (Ctx, RFLX_Types.To_First_Bit_Index (Ctx.Buffer_First), RFLX_Types.To_Last_Bit_Index (RFLX_Types.Length (Ctx.Buffer_First) + Length - 1));
end Write;
Reset (Ctx, RFLX_Types.To_First_Bit_Index (Ctx.Buffer_First), RFLX_Types.Bit_Index'Max (Ctx.Last, RFLX_Types.To_Last_Bit_Index (RFLX_Types.Length (Ctx.Buffer_First) + Offset + Length - 1)));
end Generic_Write;

function Size (Ctx : Context) return RFLX_Types.Bit_Length is
((if Ctx.Message_Last = Ctx.First - 1 then 0 else Ctx.Message_Last - Ctx.First + 1));
Expand Down
Loading

0 comments on commit b500c1e

Please sign in to comment.