Skip to content

Commit

Permalink
Add generation of record types for fixed-size messages
Browse files Browse the repository at this point in the history 
Ref. #292, #650
  • Loading branch information
@treiher
treiher committed May 27, 2021
1 parent 9df6a83 commit f8f9b70
Show file tree
Hide file tree
Showing 24 changed files with 1,697 additions and 93 deletions.
1 change: 1 addition & 0 deletions .github/workflows/tests.yml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -291,6 +291,7 @@ jobs:
- "sequence"
- "derivation"
- "expression"
- "fixed_size"
steps:
- uses: actions/checkout@v2
if: ${{ needs.skip_check_spark.outputs.should_skip != 'true' }}
Expand Down
20 changes: 14 additions & 6 deletions rflx/ada.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1736,16 +1736,24 @@ def name(self) -> str:

@dataclass
class UnitPart:
specification: Sequence[Declaration] = dataclass_field(default_factory=list)
body: Sequence[Declaration] = dataclass_field(default_factory=list)
private: Sequence[Declaration] = dataclass_field(default_factory=list)
specification: List[Declaration] = dataclass_field(default_factory=list)
body: List[Declaration] = dataclass_field(default_factory=list)
private: List[Declaration] = dataclass_field(default_factory=list)

def __iadd__(self, other: object) -> "UnitPart":
if isinstance(other, UnitPart):
self.specification += other.specification
self.body += other.body
self.private += other.private
return self
return NotImplemented


@dataclass
class SubprogramUnitPart:
specification: Sequence[Subprogram] = dataclass_field(default_factory=list)
body: Sequence[Subprogram] = dataclass_field(default_factory=list)
private: Sequence[Subprogram] = dataclass_field(default_factory=list)
specification: List[Subprogram] = dataclass_field(default_factory=list)
body: List[Subprogram] = dataclass_field(default_factory=list)
private: List[Subprogram] = dataclass_field(default_factory=list)


def generic_formal_part(parameters: Sequence[FormalDeclaration] = None) -> str:
Expand Down
34 changes: 34 additions & 0 deletions rflx/generator/common.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,9 @@ def byte_aggregate(aggregate: expr.Aggregate) -> expr.Aggregate:
if isinstance(expression, expr.Name) and expression in facts:
return facts[expression]

if isinstance(expression, expr.String):
return expr.Aggregate(*expression.elements)

if isinstance(expression, (expr.Equal, expr.NotEqual)):
field = None
aggregate = None
Expand Down Expand Up @@ -656,6 +659,37 @@ def field_byte_location_declarations() -> Sequence[ada.Declaration]:
]


def field_condition_call(message: model.Message, field: model.Field, value: ada.Expr) -> ada.Expr:
return ada.Call(
"Field_Condition",
[
ada.Variable("Ctx"),
ada.NamedAggregate(
("Fld", ada.Variable(field.affixed_name)),
*(
[(f"{field.identifier}_Value", value)]
if isinstance(message.types[field], model.Scalar)
or is_compared_to_aggregate(field, message)
else []
),
),
*(
[
ada.Call(
"Field_Size",
[
ada.Variable("Ctx"),
ada.Variable(field.affixed_name),
],
)
]
if size_dependent_condition(message)
else []
),
],
)


def prefixed_type_identifier(type_identifier: ada.ID, prefix: str) -> ada.ID:
if model.is_builtin_type(type_identifier):
return type_identifier
Expand Down
239 changes: 228 additions & 11 deletions rflx/generator/generator.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -92,7 +92,6 @@
SubprogramBody,
SubprogramDeclaration,
SubprogramUnitPart,
TypeDeclaration,
Unit,
UnitPart,
UsePackageClause,
Expand All @@ -117,6 +116,7 @@
Message,
Model,
ModularInteger,
Opaque,
RangeInteger,
Refinement,
Scalar,
Expand Down Expand Up @@ -383,6 +383,7 @@ def __create_message(self, message: Message) -> None:
unit += self.__create_update_procedures(message, sequence_fields)
unit += self.__create_cursor_function()
unit += self.__create_cursors_function()
unit += self.__create_structure(message)

@staticmethod
def __create_use_type_clause(composite_fields: ty.Sequence[Field]) -> UnitPart:
Expand Down Expand Up @@ -655,9 +656,10 @@ def __create_field_dependent_type(self, message: Message) -> UnitPart:
],
)
)
elif isinstance(t, Composite):
size = message.field_size(f)
assert isinstance(size, expr.Number)
else:
assert isinstance(t, Composite)
length = expr.Div(message.field_size(f), expr.Number(8)).simplified()
assert isinstance(length, expr.Number)
variants.append(
Variant(
[Variable(f.affixed_name)],
Expand All @@ -669,9 +671,7 @@ def __create_field_dependent_type(self, message: Message) -> UnitPart:
First(const.TYPES_INDEX),
Add(
First(const.TYPES_INDEX),
expr.Sub(expr.Div(size, expr.Number(8)), expr.Number(1))
.simplified()
.ada_expr(),
expr.Sub(length, expr.Number(1)).simplified().ada_expr(),
),
),
)
Expand Down Expand Up @@ -2703,6 +2703,223 @@ def __create_cursors_function() -> UnitPart:
[ExpressionFunctionDeclaration(specification, Variable("Ctx.Cursors"))],
)

def __create_structure(self, message: Message) -> UnitPart:
unit = UnitPart()
unit += self.__create_structure_type(message)
unit += self.__create_to_structure_procedure(message)
unit += self.__create_to_context_procedure(message)
return unit

def __create_structure_type(self, message: Message) -> UnitPart:
if not message.has_fixed_size:
return UnitPart()

assert len(message.paths(FINAL)) == 1

components = []

for path in message.paths(FINAL):
for link in path:
if link.target == FINAL:
continue

type_ = message.types[link.target]

component_type: ty.Union[ID, Expr]

if isinstance(type_, Scalar):
component_type = ID(self.__prefix * type_.identifier)
elif isinstance(type_, Opaque):
component_type = Indexed(
Variable(const.TYPES_BYTES),
ValueRange(
First(const.TYPES_INDEX),
Add(
First(const.TYPES_INDEX),
expr.Sub(expr.Div(link.size, expr.Number(8)), expr.Number(1))
.simplified()
.ada_expr(),
),
),
)
else:
return UnitPart()

components.append(Component(ID(link.target.identifier), component_type))

return UnitPart(
[
RecordType("Structure", components),
]
)

@staticmethod
def __create_to_structure_procedure(message: Message) -> UnitPart:
if not message.has_fixed_size:
return UnitPart()

assert len(message.paths(FINAL)) == 1

statements: ty.List[Statement] = []

for path in message.paths(FINAL):
for link in path:
if link.target == FINAL:
continue

type_ = message.types[link.target]

if isinstance(type_, Scalar):
statements.append(
Assignment(
Variable(f"Struct.{link.target.identifier}"),
Call(f"Get_{link.target.identifier}", [Variable("Ctx")]),
)
)
elif isinstance(type_, Opaque):
statements.append(
CallStatement(
f"Get_{link.target.identifier}",
[Variable("Ctx"), Variable(f"Struct.{link.target.identifier}")],
)
)
else:
return UnitPart()

specification = ProcedureSpecification(
"To_Structure",
[Parameter(["Ctx"], "Context"), OutParameter(["Struct"], "Structure")],
)

return UnitPart(
[
SubprogramDeclaration(
specification,
[
Precondition(
AndThen(
Call("Has_Buffer", [Variable("Ctx")]),
Call("Structural_Valid_Message", [Variable("Ctx")]),
)
),
],
)
],
[
SubprogramBody(specification, [], statements),
],
)

@staticmethod
def __create_to_context_procedure(message: Message) -> UnitPart:
if not message.has_fixed_size:
return UnitPart()

assert len(message.paths(FINAL)) == 1

body: ty.List[Statement] = [CallStatement("Reset", [Variable("Ctx")])]
statements = body

for path in message.paths(FINAL):
for link in path:
if link.target == FINAL:
continue

type_ = message.types[link.target]

if isinstance(type_, (Scalar, Opaque)):
if isinstance(type_, Enumeration) and type_.always_valid:
dependent_statements: ty.List[Statement] = [
CallStatement(
f"Set_{link.target.identifier}",
[
Variable("Ctx"),
Variable(f"Struct.{link.target.identifier}.Enum"),
],
)
]
statements.append(
IfStatement(
[
(
Variable(f"Struct.{link.target.identifier}.Known"),
dependent_statements,
)
]
)
)
statements = dependent_statements
else:
set_field = CallStatement(
f"Set_{link.target.identifier}",
[Variable("Ctx"), Variable(f"Struct.{link.target.identifier}")],
)
if common.is_compared_to_aggregate(link.target, message):
dependent_statements = [set_field]
statements.append(
IfStatement(
[
(
common.field_condition_call(
message,
link.target,
Variable(f"Struct.{link.target.identifier}"),
),
dependent_statements,
)
]
)
)
statements = dependent_statements
else:
statements.append(set_field)
else:
return UnitPart()

specification = ProcedureSpecification(
"To_Context",
[Parameter(["Struct"], "Structure"), InOutParameter(["Ctx"], "Context")],
)
first_field = message.fields[0]
message_size = message.size()
assert isinstance(message_size, expr.Number)

return UnitPart(
[
SubprogramDeclaration(
specification,
[
Precondition(
AndThen(
Not(Constrained("Ctx")),
Call("Has_Buffer", [Variable("Ctx")]),
Call(
"Valid_Next",
[Variable("Ctx"), Variable(first_field.affixed_name)],
),
GreaterEqual(
Call(
"Available_Space",
[
Variable("Ctx"),
Variable(first_field.affixed_name),
],
),
message_size.ada_expr(),
),
)
),
Postcondition(
Call("Has_Buffer", [Variable("Ctx")]),
),
],
)
],
[
SubprogramBody(specification, [], body),
],
)

def __create_refinement(self, refinement: Refinement) -> None:
unit_name = refinement.package * const.REFINEMENT_PACKAGE
null_sdu = not refinement.sdu.fields
Expand Down Expand Up @@ -3245,7 +3462,7 @@ def create_file(filename: Path, content: str) -> None:
f.write(content)


def modular_types(integer: ModularInteger) -> ty.List[TypeDeclaration]:
def modular_types(integer: ModularInteger) -> ty.List[Declaration]:
return [
ModularType(
integer.name,
Expand All @@ -3255,7 +3472,7 @@ def modular_types(integer: ModularInteger) -> ty.List[TypeDeclaration]:
]


def range_types(integer: RangeInteger) -> ty.List[TypeDeclaration]:
def range_types(integer: RangeInteger) -> ty.List[Declaration]:
return [
ModularType(
common.base_type_name(integer),
Expand All @@ -3271,8 +3488,8 @@ def range_types(integer: RangeInteger) -> ty.List[TypeDeclaration]:
]


def enumeration_types(enum: Enumeration) -> ty.List[TypeDeclaration]:
types: ty.List[TypeDeclaration] = []
def enumeration_types(enum: Enumeration) -> ty.List[Declaration]:
types: ty.List[Declaration] = []

types.append(
ModularType(common.base_type_name(enum), Pow(Number(2), enum.size_expr.ada_expr()))
Expand Down
Loading

0 comments on commit f8f9b70

Please sign in to comment.