Skip to content

Commit

Permalink
Improve setting of message fields for message aggregates
Browse files Browse the repository at this point in the history 
Ref. #908
  • Loading branch information
@treiher
treiher committed Jul 20, 2022
1 parent d1d70bc commit 373a1c9
Show file tree
Hide file tree
Showing 22 changed files with 492 additions and 1,272 deletions.
2 changes: 1 addition & 1 deletion examples/apps/dhcp_client/Makefile
View file
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@ clean:
rm -rf generated/* obj obj_optimized

binary_size: $(bin-optimized)
test $(shell size -A -d obj_optimized/dhcp_client | grep .text | awk '{ print $$2 }') -le 175000
test $(shell size -A -d obj_optimized/dhcp_client | grep .text | awk '{ print $$2 }') -le 171000

$(src): $(specs)
rflx generate -d generated --debug built-in $^
Expand Down
3 changes: 3 additions & 0 deletions rflx/ada.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -40,6 +40,9 @@ def __str__(self) -> str:
self._update_str()
return self._str

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

def __neg__(self) -> "Expr":
raise NotImplementedError

Expand Down
159 changes: 109 additions & 50 deletions rflx/generator/session.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -84,6 +84,7 @@
While,
WithClause,
)
from rflx.common import unique
from rflx.const import BUILTINS_PACKAGE, INTERNAL_PACKAGE
from rflx.error import Location, Subsystem, fail, fatal_fail
from rflx.identifier import ID
Expand Down Expand Up @@ -2143,7 +2144,7 @@ def _assign( # pylint: disable = too-many-arguments
) -> Sequence[Statement]:
if isinstance(expression, expr.MessageAggregate):
return self._assign_to_message_aggregate(
target, expression, exception_handler, is_global
target, expression, exception_handler, is_global, state
)

if isinstance(target_type, rty.Message):
Expand Down Expand Up @@ -2375,6 +2376,7 @@ def _assign_to_message_aggregate(
message_aggregate: expr.MessageAggregate,
exception_handler: ExceptionHandler,
is_global: Callable[[ID], bool],
state: ID,
) -> Sequence[Statement]:
assert isinstance(message_aggregate.type_, rty.Message)

Expand Down Expand Up @@ -2404,7 +2406,7 @@ def _assign_to_message_aggregate(
},
),
*self._set_message_fields(
target_context, message_aggregate, exception_handler, is_global
target_context, message_aggregate, exception_handler, is_global, state
),
]

Expand Down Expand Up @@ -3063,14 +3065,47 @@ def _assign_message_field( # pylint: disable = too-many-arguments
is_global: Callable[[ID], bool],
) -> Sequence[Statement]:
assert isinstance(message_type, rty.Message)
return self._set_message_field(
context_id(target, is_global),
target_field,
message_type,
value,
exception_handler,
is_global,
)

target_context = context_id(target, is_global)

return [
self._raise_exception_if(
Not(
Call(
message_type.identifier * "Valid_Next",
[
Variable(target_context),
Variable(message_type.identifier * f"F_{target_field}"),
],
)
),
f'trying to set message field "{target_field}" to "{value}" although'
f' "{target_field}" is not valid next field',
exception_handler,
),
self._raise_exception_if(
Not(
Call(
message_type.identifier * "Sufficient_Space",
[
Variable(target_context),
Variable(message_type.identifier * f"F_{target_field}"),
],
)
),
f'insufficient space in message "{target_context}" to set field "{target_field}"'
f' to "{value}"',
exception_handler,
),
*self._set_message_field(
target_context,
target_field,
message_type,
value,
exception_handler,
is_global,
),
]

def _append(
self,
Expand Down Expand Up @@ -3183,6 +3218,7 @@ def check(
append.parameters[0],
local_exception_handler,
is_global,
state,
)
if isinstance(append.parameters[0], expr.MessageAggregate)
else []
Expand Down Expand Up @@ -3260,20 +3296,33 @@ def _required_space(
.substituted(self._substitution(is_global))
.ada_expr()
)
# https://github.com/Componolit/RecordFlux/issues/691
# Validity of fields accessed in `size` must be checked before access.
precondition = [
e
for v in size.variables()
if isinstance(v.type_, (rty.Message, rty.Sequence))
for s in [expr.Size(v).substituted(self._substitution(is_global)).ada_expr()]
for e in [
LessEqual(
s,
Number(self._allocator.get_size(v.identifier, state) * 8),
),
Equal(Mod(s, Size(const.TYPES_BYTE)), Number(0)),
]
*unique(
e
for v in size.variables()
if isinstance(v.type_, (rty.Message, rty.Sequence))
for s in [expr.Size(v).substituted(self._substitution(is_global)).ada_expr()]
for e in [
LessEqual(
s,
Number(self._allocator.get_size(v.identifier, state) * 8),
),
Equal(Mod(s, Size(const.TYPES_BYTE)), Number(0)),
]
),
*unique(
Call(
s.prefix.type_.identifier * "Structural_Valid",
[
Variable(context_id(s.prefix.identifier, is_global)),
Variable(s.prefix.type_.identifier * model.Field(s.selector).affixed_name),
],
)
for s in size.findall(lambda x: isinstance(x, expr.Selected))
if isinstance(s, expr.Selected)
and isinstance(s.prefix, expr.Variable)
and isinstance(s.prefix.type_, rty.Message)
),
]
return (required_space, AndThen(*precondition) if precondition else None)

Expand Down Expand Up @@ -3688,11 +3737,46 @@ def _set_message_fields(
message_aggregate: expr.MessageAggregate,
exception_handler: ExceptionHandler,
is_global: Callable[[ID], bool],
) -> Sequence[Statement]:
state: ID,
) -> list[Statement]:
assert isinstance(message_aggregate.type_, rty.Message)

message_type = message_aggregate.type_
statements = []
size = self._message_size(message_aggregate)
required_space, required_space_precondition = self._required_space(size, is_global, state)

statements: list[Statement] = [
*(
[
self._raise_exception_if(
Not(required_space_precondition),
"violated precondition for calculating required space of message for"
f' "{target_context}" (one of the message arguments is invalid or has a too'
" small buffer)",
exception_handler,
)
]
if required_space_precondition
else []
),
self._raise_exception_if(
Less(
Call(
message_type.identifier * "Available_Space",
[
Variable(target_context),
Variable(
message_type.identifier
* model.Field(next(iter(message_type.field_types))).affixed_name
),
],
),
required_space,
),
f'insufficient space in "{target_context}" for creating message',
exception_handler,
),
]

for f, v in message_aggregate.field_values.items():
if f not in message_type.field_types:
Expand Down Expand Up @@ -3722,31 +3806,6 @@ def _set_message_field(
statements: list[Statement] = []
result = statements

statements = self._ensure(
statements,
Call(
message_type_id * "Valid_Next",
[
Variable(message_context),
Variable(message_type_id * f"F_{field}"),
],
),
f'trying to set message field "{field}" to "{value}" although "{field}" is not valid'
" next field",
exception_handler,
)

statements = self._ensure(
statements,
Call(
message_type_id * "Sufficient_Space",
[Variable(message_context), Variable(message_type_id * f"F_{field}")],
),
f'insufficient space in message "{message_context}" to set field "{field}"'
f' to "{value}"',
exception_handler,
)

if isinstance(field_type, rty.Sequence):
size: Expr
if isinstance(value, expr.Variable) and isinstance(
Expand Down
2 changes: 1 addition & 1 deletion rflx/model/message.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1922,7 +1922,7 @@ def _typed_variable(self, expression: expr.Expr, types: Mapping[Field, mty.Type]
assert expression.identifier not in {
*self._qualified_enum_literals,
*self._type_literals,
}
}, f'variable "{expression.identifier}" has the same name as a literal'
if expression.name.lower() == "message":
expression.type_ = rty.OPAQUE
elif Field(expression.identifier) in types:
Expand Down
78 changes: 34 additions & 44 deletions tests/integration/messages_with_implict_size/generated/rflx-test-session.adb
View file
Original file line number Diff line number Diff line change
Expand Up @@ -48,54 +48,44 @@ is
pragma Assert (Process_Invariant);
-- tests/integration/messages_with_implict_size/test.rflx:24:10
Universal.Message.Reset (Ctx.P.M_S_Ctx);
if Universal.Message.Valid_Next (Ctx.P.M_S_Ctx, Universal.Message.F_Message_Type) then
if Universal.Message.Sufficient_Space (Ctx.P.M_S_Ctx, Universal.Message.F_Message_Type) then
Universal.Message.Set_Message_Type (Ctx.P.M_S_Ctx, Universal.MT_Unconstrained_Data);
else
Ctx.P.Next_State := S_Terminated;
pragma Assert (Process_Invariant);
goto Finalize_Process;
end if;
else
if
not (Universal.Message.Size (Ctx.P.M_R_Ctx) <= 32768
and then Universal.Message.Size (Ctx.P.M_R_Ctx) mod RFLX_Types.Byte'Size = 0
and then Universal.Message.Structural_Valid (Ctx.P.M_R_Ctx, Universal.Message.F_Data))
then
Ctx.P.Next_State := S_Terminated;
pragma Assert (Process_Invariant);
goto Finalize_Process;
end if;
if Universal.Message.Available_Space (Ctx.P.M_S_Ctx, Universal.Message.F_Message_Type) < Universal.Message.Field_Size (Ctx.P.M_R_Ctx, Universal.Message.F_Data) + 8 then
Ctx.P.Next_State := S_Terminated;
pragma Assert (Process_Invariant);
goto Finalize_Process;
end if;
if Universal.Message.Valid_Next (Ctx.P.M_S_Ctx, Universal.Message.F_Data) then
if Universal.Message.Sufficient_Space (Ctx.P.M_S_Ctx, Universal.Message.F_Data) then
if Universal.Message.Valid_Next (Ctx.P.M_R_Ctx, Universal.Message.F_Data) then
if Universal.Message.Valid_Length (Ctx.P.M_S_Ctx, Universal.Message.F_Data, RFLX_Types.To_Length (Universal.Message.Field_Size (Ctx.P.M_R_Ctx, Universal.Message.F_Data))) then
if Universal.Message.Structural_Valid (Ctx.P.M_R_Ctx, Universal.Message.F_Data) then
declare
pragma Warnings (Off, "is not modified, could be declared constant");
RFLX_Ctx_P_M_R_Ctx_Tmp : Universal.Message.Context := Ctx.P.M_R_Ctx;
pragma Warnings (On, "is not modified, could be declared constant");
function RFLX_Process_Data_Pre (Length : RFLX_Types.Length) return Boolean is
(Universal.Message.Has_Buffer (RFLX_Ctx_P_M_R_Ctx_Tmp)
and then Universal.Message.Structural_Valid (RFLX_Ctx_P_M_R_Ctx_Tmp, Universal.Message.F_Data)
and then Length = RFLX_Types.To_Length (Universal.Message.Field_Size (RFLX_Ctx_P_M_R_Ctx_Tmp, Universal.Message.F_Data)));
procedure RFLX_Process_Data (Data : out RFLX_Types.Bytes) with
Pre =>
RFLX_Process_Data_Pre (Data'Length)
is
begin
Universal.Message.Get_Data (RFLX_Ctx_P_M_R_Ctx_Tmp, Data);
end RFLX_Process_Data;
procedure RFLX_Universal_Message_Set_Data is new Universal.Message.Generic_Set_Data (RFLX_Process_Data, RFLX_Process_Data_Pre);
begin
RFLX_Universal_Message_Set_Data (Ctx.P.M_S_Ctx, RFLX_Types.To_Length (Universal.Message.Field_Size (RFLX_Ctx_P_M_R_Ctx_Tmp, Universal.Message.F_Data)));
Ctx.P.M_R_Ctx := RFLX_Ctx_P_M_R_Ctx_Tmp;
end;
else
Ctx.P.Next_State := S_Terminated;
pragma Assert (Process_Invariant);
goto Finalize_Process;
end if;
else
Ctx.P.Next_State := S_Terminated;
pragma Assert (Process_Invariant);
goto Finalize_Process;
end if;
Universal.Message.Set_Message_Type (Ctx.P.M_S_Ctx, Universal.MT_Unconstrained_Data);
if Universal.Message.Valid_Next (Ctx.P.M_R_Ctx, Universal.Message.F_Data) then
if Universal.Message.Valid_Length (Ctx.P.M_S_Ctx, Universal.Message.F_Data, RFLX_Types.To_Length (Universal.Message.Field_Size (Ctx.P.M_R_Ctx, Universal.Message.F_Data))) then
if Universal.Message.Structural_Valid (Ctx.P.M_R_Ctx, Universal.Message.F_Data) then
declare
pragma Warnings (Off, "is not modified, could be declared constant");
RFLX_Ctx_P_M_R_Ctx_Tmp : Universal.Message.Context := Ctx.P.M_R_Ctx;
pragma Warnings (On, "is not modified, could be declared constant");
function RFLX_Process_Data_Pre (Length : RFLX_Types.Length) return Boolean is
(Universal.Message.Has_Buffer (RFLX_Ctx_P_M_R_Ctx_Tmp)
and then Universal.Message.Structural_Valid (RFLX_Ctx_P_M_R_Ctx_Tmp, Universal.Message.F_Data)
and then Length = RFLX_Types.To_Length (Universal.Message.Field_Size (RFLX_Ctx_P_M_R_Ctx_Tmp, Universal.Message.F_Data)));
procedure RFLX_Process_Data (Data : out RFLX_Types.Bytes) with
Pre =>
RFLX_Process_Data_Pre (Data'Length)
is
begin
Universal.Message.Get_Data (RFLX_Ctx_P_M_R_Ctx_Tmp, Data);
end RFLX_Process_Data;
procedure RFLX_Universal_Message_Set_Data is new Universal.Message.Generic_Set_Data (RFLX_Process_Data, RFLX_Process_Data_Pre);
begin
RFLX_Universal_Message_Set_Data (Ctx.P.M_S_Ctx, RFLX_Types.To_Length (Universal.Message.Field_Size (RFLX_Ctx_P_M_R_Ctx_Tmp, Universal.Message.F_Data)));
Ctx.P.M_R_Ctx := RFLX_Ctx_P_M_R_Ctx_Tmp;
end;
else
Ctx.P.Next_State := S_Terminated;
pragma Assert (Process_Invariant);
Expand Down
Loading

0 comments on commit 373a1c9

Please sign in to comment.