From 408120d3447783f76cb4835d2b98ac7481918899 Mon Sep 17 00:00:00 2001 From: Tobias Reiher Date: Thu, 11 Aug 2022 16:43:55 +0200 Subject: [PATCH] Optimize consecutive message field assignments Ref. #1120 --- rflx/expression.py | 136 ++++++- rflx/generator/session.py | 97 ++++- rflx/model/message.py | 105 ++++-- rflx/model/session.py | 80 ++++- tests/data/models.py | 12 +- .../generated/rflx-test-session.adb | 124 ++++++- .../generated/rflx-test-session_allocator.adb | 2 + .../generated/rflx-test-session_allocator.ads | 11 +- .../parameterized_messages/test.rflx | 9 +- .../generated/rflx-test-session.adb | 65 ++-- .../generated/rflx-test-session_allocator.adb | 2 + .../generated/rflx-test-session_allocator.ads | 11 +- .../test.rflx | 7 +- tests/unit/expression_test.py | 169 +++++++++ tests/unit/model/message_test.py | 334 +++++++++++++++++- tests/unit/model/session_test.py | 271 ++++++++++++++ 16 files changed, 1349 insertions(+), 86 deletions(-) diff --git a/rflx/expression.py b/rflx/expression.py index 98c05e952..010ecc1de 100644 --- a/rflx/expression.py +++ b/rflx/expression.py @@ -2745,6 +2745,138 @@ def variables(self) -> List["Variable"]: return result +class DeltaMessageAggregate(Expr): + """For internal use only.""" + + def __init__( + self, + identifier: StrID, + field_values: Mapping[StrID, Expr], + type_: rty.Type = rty.Undefined(), + location: Location = None, + ) -> None: + super().__init__(type_, location) + self.identifier = ID(identifier) + self.field_values = {ID(k): v for k, v in field_values.items()} + + def _update_str(self) -> None: + field_values = ( + ", ".join([f"{k} => {self.field_values[k]}" for k in self.field_values]) + if self.field_values + else "null message" + ) + self._str = intern(f"{self.identifier} with delta {field_values}") + + def _check_type_subexpr(self) -> RecordFluxError: + if not isinstance(self.type_, rty.Message): + error = RecordFluxError() + + for d in self.field_values.values(): + error += d.check_type_instance(rty.Any) + + return error + + error = RecordFluxError() + field_combinations = set(self.type_.field_combinations) + fields: tuple[str, ...] = () + + for i, (field, expr) in enumerate(self.field_values.items()): + if field not in self.type_.fields: + error.extend( + [ + ( + f'invalid field "{field}" for {self.type_}', + Subsystem.MODEL, + Severity.ERROR, + field.location, + ), + *_similar_field_names(field, self.type_.fields, field.location), + ] + ) + continue + + field_type = self.type_.types[field] + + if field_type == rty.OPAQUE: + if not any( + r.field == field and expr.type_.is_compatible(r.sdu) + for r in self.type_.refinements + ): + error += expr.check_type(field_type) + else: + error += expr.check_type(field_type) + + fields = (*fields, str(field)) + field_combinations = { + c + for c in field_combinations + if any(fields == c[i : len(fields) + i] for i in range(len(c) - len(fields) + 1)) + } + + if not field_combinations: + error.extend( + [ + ( + f'invalid position for field "{field}" of {self.type_}', + Subsystem.MODEL, + Severity.ERROR, + field.location, + ) + ], + ) + break + + return error + + def __neg__(self) -> Expr: + raise NotImplementedError + + def findall(self, match: Callable[[Expr], bool]) -> Sequence[Expr]: + return [ + *([self] if match(self) else []), + *[e for v in self.field_values.values() for e in v.findall(match)], + ] + + def simplified(self) -> Expr: + return DeltaMessageAggregate( + self.identifier, + {k: self.field_values[k].simplified() for k in self.field_values}, + self.type_, + self.location, + ) + + def substituted( + self, func: Callable[[Expr], Expr] = None, mapping: Mapping[Name, Expr] = None + ) -> Expr: + func = substitution(mapping or {}, func) + expr = func(self) + if isinstance(expr, DeltaMessageAggregate): + return expr.__class__( + expr.identifier, + {k: expr.field_values[k].substituted(func) for k in expr.field_values}, + type_=expr.type_, + location=expr.location, + ) + return expr + + @property + def precedence(self) -> Precedence: + raise NotImplementedError + + def ada_expr(self) -> ada.Expr: + raise NotImplementedError + + @lru_cache(maxsize=None) + def z3expr(self) -> z3.ExprRef: + raise NotImplementedError + + def variables(self) -> List[Variable]: + result = [] + for v in self.field_values.values(): + result.extend(v.variables()) + return result + + class Binding(Expr): def __init__(self, expr: Expr, data: Mapping[StrID, Expr], location: Location = None) -> None: super().__init__(expr.type_, location) @@ -2850,12 +2982,12 @@ def _entity_name(expr: Expr) -> str: else "type" if isinstance(expr, Conversion) else "message" - if isinstance(expr, MessageAggregate) + if isinstance(expr, (MessageAggregate, DeltaMessageAggregate)) else "expression" ) expr_name = ( str(expr.identifier) - if isinstance(expr, (Variable, Call, Conversion, MessageAggregate)) + if isinstance(expr, (Variable, Call, Conversion, MessageAggregate, DeltaMessageAggregate)) else str(expr) ) return f'{expr_type} "{expr_name}"' diff --git a/rflx/generator/session.py b/rflx/generator/session.py index 73ad79dfa..997b1594f 100644 --- a/rflx/generator/session.py +++ b/rflx/generator/session.py @@ -2159,6 +2159,11 @@ def _assign( # pylint: disable = too-many-arguments target, expression, exception_handler, is_global, state ) + if isinstance(expression, expr.DeltaMessageAggregate): + return self._assign_to_delta_message_aggregate( + target, expression, exception_handler, is_global, state + ) + if isinstance(target_type, rty.Message): for v in expression.findall( lambda x: isinstance(x, expr.Variable) and x.identifier == target @@ -2424,6 +2429,85 @@ def _assign_to_message_aggregate( return assign_to_message_aggregate + def _assign_to_delta_message_aggregate( + self, + target: ID, + delta_message_aggregate: expr.DeltaMessageAggregate, + exception_handler: ExceptionHandler, + is_global: Callable[[ID], bool], + state: ID, + ) -> Sequence[Statement]: + assert isinstance(delta_message_aggregate.type_, rty.Message) + + self._session_context.used_types_body.append(const.TYPES_BIT_LENGTH) + + target_type_id = delta_message_aggregate.type_.identifier + target_context = context_id(target, is_global) + + fields = list(delta_message_aggregate.field_values) + first_field = fields[0] + last_field = fields[-1] + + required_space, required_space_precondition = self._required_space( + self._message_subpath_size(delta_message_aggregate), is_global, state + ) + + return [ + self._raise_exception_if( + Not( + Call( + target_type_id * "Valid_Next", + [ + Variable(target_context), + Variable(target_type_id * model.Field(first_field).affixed_name), + ], + ) + ), + f'trying to set message fields "{first_field}" to "{last_field}" although' + f' "{first_field}" is not valid next field', + exception_handler, + ), + *( + [ + self._raise_exception_if( + Not(required_space_precondition), + "violated precondition for calculating required space for setting message" + f' fields "{first_field}" to "{last_field}" (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( + target_type_id * "Available_Space", + [ + Variable(target_context), + Variable(target_type_id * model.Field(first_field).affixed_name), + ], + ), + required_space, + ), + f'insufficient space for setting message fields "{first_field}" to "{last_field}"', + exception_handler, + ), + *[ + s + for f, v in delta_message_aggregate.field_values.items() + for s in self._set_message_field( + target_context, + f, + delta_message_aggregate.type_, + v, + exception_handler, + is_global, + ) + ], + ] + def _assign_to_head( self, target: ID, @@ -3434,6 +3518,18 @@ def _message_size(self, message_aggregate: expr.MessageAggregate) -> expr.Expr: assert isinstance(message, model.Message) return message.size({model.Field(f): v for f, v in message_aggregate.field_values.items()}) + def _message_subpath_size( + self, delta_message_aggregate: expr.DeltaMessageAggregate + ) -> expr.Expr: + assert isinstance(delta_message_aggregate.type_, rty.Message) + message = self._model_type(delta_message_aggregate.type_.identifier) + assert isinstance(message, model.Message) + return message.size( + {model.Field(f): v for f, v in delta_message_aggregate.field_values.items()}, + delta_message_aggregate.identifier, + subpath=True, + ) + def _required_space( self, size: expr.Expr, is_global: Callable[[ID], bool], state: ID ) -> tuple[Expr, Optional[Expr]]: @@ -3441,7 +3537,6 @@ def _required_space( size.substituted( lambda x: expr.Call(const.TYPES_BIT_LENGTH, [x]) if (isinstance(x, expr.Variable) and isinstance(x.type_, rty.AnyInteger)) - or (isinstance(x, expr.Selected) and x.type_ != rty.OPAQUE) else x ) .substituted(self._substitution(is_global)) diff --git a/rflx/model/message.py b/rflx/model/message.py index 8af8246cb..5579a5f21 100644 --- a/rflx/model/message.py +++ b/rflx/model/message.py @@ -955,7 +955,12 @@ def is_definite(self) -> bool: and not any(isinstance(t, mty.Sequence) for t in self.types.values()) ) - def size(self, field_values: Mapping[Field, expr.Expr] = None) -> expr.Expr: + def size( + self, + field_values: Mapping[Field, expr.Expr] = None, + message_instance: ID = None, + subpath: bool = False, + ) -> expr.Expr: # pylint: disable-next = too-many-locals """ Determine the size of the message based on the given field values. @@ -964,17 +969,77 @@ def size(self, field_values: Mapping[Field, expr.Expr] = None) -> expr.Expr: if-expressions to represent these dependencies. Only message paths which contain all given fields are considered. The evaluation of the returned size expression may result in a size greater than zero, even if the field values do not lead to a valid message. + + The message fields can be prefixed by the message instance. + + The size calculation can be restricted to the size of a subpath. The subpath is defined by + the given field values. """ def typed_variable(expression: expr.Expr) -> expr.Expr: return self._typed_variable(expression, self.types) - if not self.structure: - return expr.Number(0) - field_values = field_values if field_values else {} + if subpath: + if not field_values: + return expr.Number(0) + + fields = list(field_values) + possible_paths = [ + p + for p in sorted(self.paths(FINAL)) + if any( + fields == [l.target for l in p[i : len(fields) + i]] + for i in range(len(p) - len(fields) + 1) + ) + ] + + if not possible_paths: + subpath_str = " -> ".join(f.name for f in fields) + fail( + f'unable to calculate size of invalid subpath "{subpath_str}"' + f' of message "{self.identifier}"', + Subsystem.MODEL, + Severity.ERROR, + self.location, + ) + else: + if not self.structure: + return expr.Number(0) + + fields = list(self.fields) + possible_paths = [ + path + for path in sorted(self.paths(FINAL)) + if not ( + set(field_values) + - set(self.parameters) + - set(l.target for l in path if l.target != FINAL) + ) + ] + + def add_message_prefix(expression: expr.Expr) -> expr.Expr: + if ( + message_instance + and isinstance(expression, expr.Variable) + and Field(expression.identifier) in self.types + ): + return expr.Selected( + expr.Variable(message_instance, type_=self.type_), + expression.identifier, + negative=expression.negative, + type_=expression.type_, + location=expression.location, + ) + return expression + def remove_variable_prefix(expression: expr.Expr) -> expr.Expr: + """ + Remove prefix from variables. + + The prefix is used to prevent name conflicts between field values and field names. + """ if isinstance(expression, expr.Variable) and expression.name.startswith("RFLX_"): return expression.copy(identifier=expression.name[5:]) if ( @@ -1019,30 +1084,14 @@ def remove_variable_prefix(expression: expr.Expr) -> expr.Expr: ) facts: list[expr.Expr] = [*values, *aggregate_sizes, *composite_sizes] type_constraints = to_mapping(self._aggregate_constraints() + self._type_size_constraints()) - possible_paths = [ - path - for path in sorted(self.paths(FINAL)) - if not ( - set(field_values) - - set(self.parameters) - - set(l.target for l in path if l.target != FINAL) - ) - ] definite_fields = set.intersection(*[{l.target for l in path} for path in possible_paths]) - optional_fields = set(self.fields) - definite_fields + optional_fields = set(fields) - definite_fields conditional_field_size = [] - for field in self.fields: - overlay_condition: expr.Expr = expr.TRUE - - if any(l.first != expr.UNDEFINED for l in self.outgoing(field)): - if all(l.first != expr.UNDEFINED for l in self.outgoing(field)): - continue - - overlay_condition = expr.Or( - *[l.condition for l in self.outgoing(field) if l.first == expr.UNDEFINED] - ) - + for field in fields: + overlay_condition = expr.Not( + expr.Or(*[l.condition for l in self.incoming(field) if l.first != expr.UNDEFINED]) + ).simplified() paths_to_field = sorted( { path[ @@ -1070,16 +1119,18 @@ def remove_variable_prefix(expression: expr.Expr) -> expr.Expr: ) .substituted(mapping=to_mapping(link_size_expressions + facts)) .substituted(mapping=type_constraints) - .substituted(remove_variable_prefix) .substituted(typed_variable) + .substituted(add_message_prefix) + .substituted(remove_variable_prefix) .simplified() ) field_size = ( expr.Size(expr.Variable(field.name, type_=self.types[field].type_)) .substituted(mapping=to_mapping(link_size_expressions + facts)) .substituted(mapping=type_constraints) - .substituted(remove_variable_prefix) .substituted(typed_variable) + .substituted(add_message_prefix) + .substituted(remove_variable_prefix) ) conditional_field_size.append( diff --git a/rflx/model/session.py b/rflx/model/session.py index 5cc75c92e..5c2e948a0 100644 --- a/rflx/model/session.py +++ b/rflx/model/session.py @@ -67,6 +67,8 @@ def __init__( self.description = description self.location = location + self._normalize() + def __repr__(self) -> str: return verbose_repr(self, ["identifier", "transitions", "actions", "declarations"]) @@ -122,6 +124,7 @@ def has_exceptions(self) -> bool: expr.Head, expr.Comprehension, expr.MessageAggregate, + expr.DeltaMessageAggregate, expr.Conversion, expr.Opaque, ), @@ -132,6 +135,69 @@ def has_exceptions(self) -> bool: for a in self._actions ) + def _normalize(self) -> None: # pylint: disable = too-many-branches + field_assignments: list[stmt.MessageFieldAssignment] = [] + actions: list[stmt.Statement] = [] + + for a in self._actions: + if not field_assignments: + if isinstance(a, stmt.MessageFieldAssignment): + field_assignments.append(a) + else: + actions.append(a) + elif len(field_assignments) == 1: + if isinstance(a, stmt.MessageFieldAssignment): + if field_assignments[0].message == a.message: + field_assignments.append(a) + else: + actions.extend(field_assignments) + field_assignments = [a] + else: + actions.extend( + [ + *field_assignments, + a, + ] + ) + field_assignments = [] + else: + if isinstance(a, stmt.MessageFieldAssignment): + if field_assignments[0].message == a.message: + field_assignments.append(a) + else: + actions.append(self._collect_message_field_assignments(field_assignments)) + field_assignments = [a] + else: + actions.extend( + [ + self._collect_message_field_assignments(field_assignments), + a, + ] + ) + field_assignments = [] + + if len(field_assignments) == 1: + actions.extend(field_assignments) + elif len(field_assignments) > 1: + actions.append(self._collect_message_field_assignments(field_assignments)) + + self._actions = actions + + def _collect_message_field_assignments( + self, field_assignments: list[stmt.MessageFieldAssignment] + ) -> stmt.Assignment: + return stmt.Assignment( + field_assignments[0].identifier, + expr.DeltaMessageAggregate( + field_assignments[0].identifier, {a.field: a.value for a in field_assignments} + ), + location=Location( + field_assignments[0].location.start if field_assignments[0].location else (0, 0), + field_assignments[0].location.source if field_assignments[0].location else None, + field_assignments[-1].location.end if field_assignments[-1].location else None, + ), + ) + class AbstractSession(BasicDeclaration): # pylint: disable=too-many-arguments, too-many-instance-attributes @@ -640,12 +706,19 @@ def _validate_usage(self) -> None: ], ) - def _typify_variable( + def _typify_variable( # pylint: disable = too-many-branches self, expression: expr.Expr, declarations: Mapping[ID, decl.Declaration] ) -> expr.Expr: if isinstance( expression, - (expr.Variable, expr.Literal, expr.Call, expr.Conversion, expr.MessageAggregate), + ( + expr.Variable, + expr.Literal, + expr.Call, + expr.Conversion, + expr.MessageAggregate, + expr.DeltaMessageAggregate, + ), ): identifier = expression.identifier @@ -674,6 +747,9 @@ def _typify_variable( type_identifier = mty.internal_type_identifier(identifier, self.package) if type_identifier in self.types: expression.type_ = self.types[type_identifier].type_ + if isinstance(expression, expr.DeltaMessageAggregate): + if identifier in declarations: + expression.type_ = declarations[identifier].type_ return expression diff --git a/tests/data/models.py b/tests/data/models.py index 5e12bb402..77558b84c 100644 --- a/tests/data/models.py +++ b/tests/data/models.py @@ -480,10 +480,10 @@ Field("Message_Type"), Field("Data"), condition=Or( - Equal(Variable("Message_Type"), Variable("Universal.MT_Null")), - Equal(Variable("Message_Type"), Variable("Universal.MT_Data")), - Equal(Variable("Message_Type"), Variable("Universal.MT_Values")), - Equal(Variable("Message_Type"), Variable("Universal.MT_Options")), + Equal(Variable("Message_Type"), Variable("Universal::MT_Null")), + Equal(Variable("Message_Type"), Variable("Universal::MT_Data")), + Equal(Variable("Message_Type"), Variable("Universal::MT_Values")), + Equal(Variable("Message_Type"), Variable("Universal::MT_Options")), ), size=Number(64), ), @@ -517,8 +517,8 @@ Field("Message_Type"), Field("Data"), condition=Or( - Equal(Variable("Message_Type"), Variable("Universal.OT_Null")), - Equal(Variable("Message_Type"), Variable("Universal.OT_Data")), + Equal(Variable("Message_Type"), Variable("Universal::OT_Null")), + Equal(Variable("Message_Type"), Variable("Universal::OT_Data")), ), size=Number(24), ), diff --git a/tests/integration/parameterized_messages/generated/rflx-test-session.adb b/tests/integration/parameterized_messages/generated/rflx-test-session.adb index a878a9c05..267aeb4b2 100644 --- a/tests/integration/parameterized_messages/generated/rflx-test-session.adb +++ b/tests/integration/parameterized_messages/generated/rflx-test-session.adb @@ -18,7 +18,8 @@ is 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_2 = null + and Ctx.P.Slots.Slot_Ptr_3 /= null) with Annotate => (GNATprove, Inline_For_Proof), @@ -39,7 +40,8 @@ is is function Receive_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_2 = null + and Ctx.P.Slots.Slot_Ptr_3 /= null) with Annotate => (GNATprove, Inline_For_Proof), @@ -63,18 +65,29 @@ is Initialized (Ctx) is Length : Test.Length; + M_T_Ctx : Test.Message.Context; + Equal : Boolean; + M_T_Buffer : RFLX_Types.Bytes_Ptr; function Process_Invariant return Boolean is - (Ctx.P.Slots.Slot_Ptr_1 = null + (Global_Initialized (Ctx) + and Test.Message.Has_Buffer (M_T_Ctx) + and M_T_Ctx.Buffer_First = RFLX.RFLX_Types.Index'First + and M_T_Ctx.Buffer_Last >= RFLX.RFLX_Types.Index'First + 4095 + and Ctx.P.Slots.Slot_Ptr_3 = null + and Ctx.P.Slots.Slot_Ptr_1 = null and Ctx.P.Slots.Slot_Ptr_2 = null) with Annotate => (GNATprove, Inline_For_Proof), Ghost; begin + M_T_Buffer := Ctx.P.Slots.Slot_Ptr_3; + pragma Warnings (Off, "unused assignment"); + Ctx.P.Slots.Slot_Ptr_3 := null; + pragma Warnings (On, "unused assignment"); + Test.Message.Initialize (M_T_Ctx, M_T_Buffer, Length => Test.Length'First, Extended => Boolean'First); pragma Assert (Process_Invariant); - -- tests/integration/parameterized_messages/test.rflx:49:10 - Test.Message.Reset (Ctx.P.M_S_Ctx, Length => Ctx.P.M_R_Ctx.Length, Extended => True); - -- tests/integration/parameterized_messages/test.rflx:50:10 + -- tests/integration/parameterized_messages/test.rflx:51:10 Test.Message.Reset (Ctx.P.M_S_Ctx, Length => Ctx.P.M_R_Ctx.Length, Extended => True); if not (Test.Message.Size (Ctx.P.M_R_Ctx) <= 32768 @@ -136,15 +149,97 @@ is pragma Assert (Process_Invariant); goto Finalize_Process; end if; - -- tests/integration/parameterized_messages/test.rflx:51:10 + -- tests/integration/parameterized_messages/test.rflx:52:10 Length := Ctx.P.M_S_Ctx.Length; - if Length = Ctx.P.M_R_Ctx.Length then + -- tests/integration/parameterized_messages/test.rflx:53:10 + Test.Message.Reset (M_T_Ctx, Length => Ctx.P.M_S_Ctx.Length, Extended => True); + -- tests/integration/parameterized_messages/test.rflx:54:10 + if not Test.Message.Valid_Next (M_T_Ctx, Test.Message.F_Data) then + Ctx.P.Next_State := S_Error; + pragma Assert (Process_Invariant); + goto Finalize_Process; + end if; + if + not (Test.Message.Size (Ctx.P.M_R_Ctx) <= 32768 + and then Test.Message.Size (Ctx.P.M_R_Ctx) mod RFLX_Types.Byte'Size = 0 + and then Test.Message.Structural_Valid (Ctx.P.M_R_Ctx, Test.Message.F_Data)) + then + Ctx.P.Next_State := S_Error; + pragma Assert (Process_Invariant); + goto Finalize_Process; + end if; + if Test.Message.Available_Space (M_T_Ctx, Test.Message.F_Data) < Test.Message.Field_Size (Ctx.P.M_R_Ctx, Test.Message.F_Data) + 16 then + Ctx.P.Next_State := S_Error; + pragma Assert (Process_Invariant); + goto Finalize_Process; + end if; + if Test.Message.Valid_Next (Ctx.P.M_R_Ctx, Test.Message.F_Data) then + if Test.Message.Valid_Length (M_T_Ctx, Test.Message.F_Data, RFLX_Types.To_Length (Test.Message.Field_Size (Ctx.P.M_R_Ctx, Test.Message.F_Data))) then + if Test.Message.Structural_Valid (Ctx.P.M_R_Ctx, Test.Message.F_Data) then + declare + pragma Warnings (Off, "is not modified, could be declared constant"); + RFLX_Ctx_P_M_R_Ctx_Tmp : Test.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 + (Test.Message.Has_Buffer (RFLX_Ctx_P_M_R_Ctx_Tmp) + and then Test.Message.Structural_Valid (RFLX_Ctx_P_M_R_Ctx_Tmp, Test.Message.F_Data) + and then Length = RFLX_Types.To_Length (Test.Message.Field_Size (RFLX_Ctx_P_M_R_Ctx_Tmp, Test.Message.F_Data))); + procedure RFLX_Process_Data (Data : out RFLX_Types.Bytes) with + Pre => + RFLX_Process_Data_Pre (Data'Length) + is + begin + Test.Message.Get_Data (RFLX_Ctx_P_M_R_Ctx_Tmp, Data); + end RFLX_Process_Data; + procedure RFLX_Test_Message_Set_Data is new Test.Message.Generic_Set_Data (RFLX_Process_Data, RFLX_Process_Data_Pre); + begin + RFLX_Test_Message_Set_Data (M_T_Ctx, RFLX_Types.To_Length (Test.Message.Field_Size (RFLX_Ctx_P_M_R_Ctx_Tmp, Test.Message.F_Data))); + Ctx.P.M_R_Ctx := RFLX_Ctx_P_M_R_Ctx_Tmp; + end; + else + Ctx.P.Next_State := S_Error; + pragma Assert (Process_Invariant); + goto Finalize_Process; + end if; + else + Ctx.P.Next_State := S_Error; + pragma Assert (Process_Invariant); + goto Finalize_Process; + end if; + else + Ctx.P.Next_State := S_Error; + pragma Assert (Process_Invariant); + goto Finalize_Process; + end if; + if Test.Message.Valid_Length (M_T_Ctx, Test.Message.F_Extension, RFLX_Types.To_Length (2 * RFLX_Types.Byte'Size)) then + pragma Assert (Test.Message.Sufficient_Space (M_T_Ctx, Test.Message.F_Extension)); + Test.Message.Set_Extension (M_T_Ctx, (RFLX_Types.Byte'Val (3), RFLX_Types.Byte'Val (4))); + else + Ctx.P.Next_State := S_Error; + pragma Assert (Process_Invariant); + goto Finalize_Process; + end if; + -- tests/integration/parameterized_messages/test.rflx:56:10 + Equal := Ctx.P.M_S_Ctx.Length = M_T_Ctx.Length + and then Ctx.P.M_S_Ctx.Extended = M_T_Ctx.Extended; + if + Length = Ctx.P.M_R_Ctx.Length + and then Equal + then Ctx.P.Next_State := S_Reply; else Ctx.P.Next_State := S_Error; end if; pragma Assert (Process_Invariant); <> + pragma Warnings (Off, """M_T_Ctx"" is set by ""Take_Buffer"" but not used after the call"); + Test.Message.Take_Buffer (M_T_Ctx, M_T_Buffer); + pragma Warnings (On, """M_T_Ctx"" is set by ""Take_Buffer"" but not used after the call"); + pragma Assert (Ctx.P.Slots.Slot_Ptr_3 = null); + pragma Assert (M_T_Buffer /= null); + Ctx.P.Slots.Slot_Ptr_3 := M_T_Buffer; + pragma Assert (Ctx.P.Slots.Slot_Ptr_3 /= null); + pragma Assert (Global_Initialized (Ctx)); end Process; procedure Reply (Ctx : in out Context'Class) with @@ -155,14 +250,15 @@ is 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_2 = null + and Ctx.P.Slots.Slot_Ptr_3 /= null) with Annotate => (GNATprove, Inline_For_Proof), Ghost; begin pragma Assert (Reply_Invariant); - -- tests/integration/parameterized_messages/test.rflx:63:10 + -- tests/integration/parameterized_messages/test.rflx:68:10 Ctx.P.Next_State := S_Reset; pragma Assert (Reply_Invariant); end Reply; @@ -175,14 +271,15 @@ is is function Reset_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_2 = null + and Ctx.P.Slots.Slot_Ptr_3 /= null) with Annotate => (GNATprove, Inline_For_Proof), Ghost; begin pragma Assert (Reset_Invariant); - -- tests/integration/parameterized_messages/test.rflx:71:10 + -- tests/integration/parameterized_messages/test.rflx:76:10 Test.Message.Reset (Ctx.P.M_S_Ctx, Length => Ctx.P.M_R_Ctx.Length, Extended => Ctx.P.M_R_Ctx.Extended); Ctx.P.Next_State := S_Terminated; pragma Assert (Reset_Invariant); @@ -196,7 +293,8 @@ is is function Error_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_2 = null + and Ctx.P.Slots.Slot_Ptr_3 /= null) with Annotate => (GNATprove, Inline_For_Proof), diff --git a/tests/integration/parameterized_messages/generated/rflx-test-session_allocator.adb b/tests/integration/parameterized_messages/generated/rflx-test-session_allocator.adb index 85d68b5b9..8d6547ec8 100644 --- a/tests/integration/parameterized_messages/generated/rflx-test-session_allocator.adb +++ b/tests/integration/parameterized_messages/generated/rflx-test-session_allocator.adb @@ -12,6 +12,7 @@ is begin 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; end Initialize; procedure Finalize (S : in out Slots) with @@ -21,6 +22,7 @@ is begin S.Slot_Ptr_1 := null; S.Slot_Ptr_2 := null; + S.Slot_Ptr_3 := null; end Finalize; end RFLX.Test.Session_Allocator; diff --git a/tests/integration/parameterized_messages/generated/rflx-test-session_allocator.ads b/tests/integration/parameterized_messages/generated/rflx-test-session_allocator.ads index f2a5c83ae..ff9dffac9 100644 --- a/tests/integration/parameterized_messages/generated/rflx-test-session_allocator.ads +++ b/tests/integration/parameterized_messages/generated/rflx-test-session_allocator.ads @@ -14,6 +14,7 @@ is record 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); end record; subtype Slot_Ptr_Type_4096 is RFLX_Types.Bytes_Ptr with @@ -26,15 +27,18 @@ is record Slot_Ptr_1 : Slot_Ptr_Type_4096; Slot_Ptr_2 : Slot_Ptr_Type_4096; + Slot_Ptr_3 : 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_2 /= null + and S.Slot_Ptr_3 /= null); function Uninitialized (S : Slots) return Boolean is (S.Slot_Ptr_1 = null - and S.Slot_Ptr_2 = null); + and S.Slot_Ptr_2 = null + and S.Slot_Ptr_3 = null); procedure Initialize (S : out Slots; M : Memory) with Post => @@ -46,6 +50,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_2 = null + and S.Slot_Ptr_3 /= null); end RFLX.Test.Session_Allocator; diff --git a/tests/integration/parameterized_messages/test.rflx b/tests/integration/parameterized_messages/test.rflx index 25aa425f8..1f8d8706b 100644 --- a/tests/integration/parameterized_messages/test.rflx +++ b/tests/integration/parameterized_messages/test.rflx @@ -45,13 +45,18 @@ package Test is state Process is Length : Length; + M_T : Message; + Equal : Boolean; begin - M_S'Reset (Length => M_R.Length, Extended => True); M_S := Message'(Length => M_R.Length, Extended => True, Data => M_R.Data, Extension => [3, 4]); Length := M_S.Length; + M_T'Reset (Length => M_S.Length, Extended => True); + M_T.Data := M_R.Data; + M_T.Extension := [3, 4]; + Equal := M_S.Length = M_T.Length and M_S.Extended = M_T.Extended; transition goto Reply - if Length = M_R.Length + if Length = M_R.Length and Equal goto Error exception goto Error diff --git a/tests/integration/session_setting_of_message_fields/generated/rflx-test-session.adb b/tests/integration/session_setting_of_message_fields/generated/rflx-test-session.adb index 4b02b61dd..64e7fb176 100644 --- a/tests/integration/session_setting_of_message_fields/generated/rflx-test-session.adb +++ b/tests/integration/session_setting_of_message_fields/generated/rflx-test-session.adb @@ -21,7 +21,8 @@ is Initialized (Ctx) is function Start_Invariant return Boolean is - (Ctx.P.Slots.Slot_Ptr_1 = null) + (Ctx.P.Slots.Slot_Ptr_1 = null + and Ctx.P.Slots.Slot_Ptr_2 /= null) with Annotate => (GNATprove, Inline_For_Proof), @@ -48,62 +49,77 @@ is Post => Initialized (Ctx) is + Local_Message_Ctx : Universal.Message.Context; + Local_Message_Buffer : RFLX_Types.Bytes_Ptr; function Process_Invariant return Boolean is - (Ctx.P.Slots.Slot_Ptr_1 = null) + (Global_Initialized (Ctx) + and Universal.Message.Has_Buffer (Local_Message_Ctx) + and Local_Message_Ctx.Buffer_First = RFLX.RFLX_Types.Index'First + and Local_Message_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) with Annotate => (GNATprove, Inline_For_Proof), Ghost; begin + Local_Message_Buffer := Ctx.P.Slots.Slot_Ptr_2; + pragma Warnings (Off, "unused assignment"); + Ctx.P.Slots.Slot_Ptr_2 := null; + pragma Warnings (On, "unused assignment"); + Universal.Message.Initialize (Local_Message_Ctx, Local_Message_Buffer); pragma Assert (Process_Invariant); - -- tests/integration/session_setting_of_message_fields/test.rflx:27:10 + -- tests/integration/session_setting_of_message_fields/test.rflx:28:10 if not Universal.Message.Valid_Next (Ctx.P.Message_Ctx, Universal.Message.F_Message_Type) then Ctx.P.Next_State := S_Terminated; pragma Assert (Process_Invariant); goto Finalize_Process; end if; - if not Universal.Message.Sufficient_Space (Ctx.P.Message_Ctx, Universal.Message.F_Message_Type) then + if Universal.Message.Available_Space (Ctx.P.Message_Ctx, Universal.Message.F_Message_Type) < 32 then Ctx.P.Next_State := S_Terminated; pragma Assert (Process_Invariant); goto Finalize_Process; end if; pragma Assert (Universal.Message.Sufficient_Space (Ctx.P.Message_Ctx, Universal.Message.F_Message_Type)); Universal.Message.Set_Message_Type (Ctx.P.Message_Ctx, Universal.MT_Data); - -- tests/integration/session_setting_of_message_fields/test.rflx:29:10 - if not Universal.Message.Valid_Next (Ctx.P.Message_Ctx, Universal.Message.F_Length) then - Ctx.P.Next_State := S_Terminated; - pragma Assert (Process_Invariant); - goto Finalize_Process; - end if; - if not Universal.Message.Sufficient_Space (Ctx.P.Message_Ctx, Universal.Message.F_Length) then + pragma Assert (Universal.Message.Sufficient_Space (Ctx.P.Message_Ctx, Universal.Message.F_Length)); + Universal.Message.Set_Length (Ctx.P.Message_Ctx, 1); + if Universal.Message.Valid_Length (Ctx.P.Message_Ctx, Universal.Message.F_Data, RFLX_Types.To_Length (1 * RFLX_Types.Byte'Size)) then + pragma Assert (Universal.Message.Sufficient_Space (Ctx.P.Message_Ctx, Universal.Message.F_Data)); + Universal.Message.Set_Data (Ctx.P.Message_Ctx, (RFLX_Types.Index'First => RFLX_Types.Byte'Val (2))); + else Ctx.P.Next_State := S_Terminated; pragma Assert (Process_Invariant); goto Finalize_Process; end if; - pragma Assert (Universal.Message.Sufficient_Space (Ctx.P.Message_Ctx, Universal.Message.F_Length)); - Universal.Message.Set_Length (Ctx.P.Message_Ctx, 1); - -- tests/integration/session_setting_of_message_fields/test.rflx:31:10 - if not Universal.Message.Valid_Next (Ctx.P.Message_Ctx, Universal.Message.F_Data) then + -- tests/integration/session_setting_of_message_fields/test.rflx:34:10 + if not Universal.Message.Valid_Next (Local_Message_Ctx, Universal.Message.F_Message_Type) then Ctx.P.Next_State := S_Terminated; pragma Assert (Process_Invariant); goto Finalize_Process; end if; - if not Universal.Message.Sufficient_Space (Ctx.P.Message_Ctx, Universal.Message.F_Data) then + if not Universal.Message.Sufficient_Space (Local_Message_Ctx, Universal.Message.F_Message_Type) then Ctx.P.Next_State := S_Terminated; pragma Assert (Process_Invariant); goto Finalize_Process; end if; - if Universal.Message.Valid_Length (Ctx.P.Message_Ctx, Universal.Message.F_Data, RFLX_Types.To_Length (1 * RFLX_Types.Byte'Size)) then - pragma Assert (Universal.Message.Sufficient_Space (Ctx.P.Message_Ctx, Universal.Message.F_Data)); - Universal.Message.Set_Data (Ctx.P.Message_Ctx, (RFLX_Types.Index'First => RFLX_Types.Byte'Val (2))); + pragma Assert (Universal.Message.Sufficient_Space (Local_Message_Ctx, Universal.Message.F_Message_Type)); + Universal.Message.Set_Message_Type (Local_Message_Ctx, Universal.MT_Null); + if Universal.Message.Get_Message_Type (Ctx.P.Message_Ctx) /= Universal.Message.Get_Message_Type (Local_Message_Ctx) then + Ctx.P.Next_State := S_Reply; else Ctx.P.Next_State := S_Terminated; - pragma Assert (Process_Invariant); - goto Finalize_Process; end if; - Ctx.P.Next_State := S_Reply; pragma Assert (Process_Invariant); <> + pragma Warnings (Off, """Local_Message_Ctx"" is set by ""Take_Buffer"" but not used after the call"); + Universal.Message.Take_Buffer (Local_Message_Ctx, Local_Message_Buffer); + pragma Warnings (On, """Local_Message_Ctx"" is set by ""Take_Buffer"" but not used after the call"); + pragma Assert (Ctx.P.Slots.Slot_Ptr_2 = null); + pragma Assert (Local_Message_Buffer /= null); + Ctx.P.Slots.Slot_Ptr_2 := Local_Message_Buffer; + pragma Assert (Ctx.P.Slots.Slot_Ptr_2 /= null); + pragma Assert (Global_Initialized (Ctx)); end Process; procedure Reply (Ctx : in out Context'Class) with @@ -113,14 +129,15 @@ is Initialized (Ctx) is function Reply_Invariant return Boolean is - (Ctx.P.Slots.Slot_Ptr_1 = null) + (Ctx.P.Slots.Slot_Ptr_1 = null + and Ctx.P.Slots.Slot_Ptr_2 /= null) with Annotate => (GNATprove, Inline_For_Proof), Ghost; begin pragma Assert (Reply_Invariant); - -- tests/integration/session_setting_of_message_fields/test.rflx:40:10 + -- tests/integration/session_setting_of_message_fields/test.rflx:45:10 Ctx.P.Next_State := S_Terminated; pragma Assert (Reply_Invariant); end Reply; diff --git a/tests/integration/session_setting_of_message_fields/generated/rflx-test-session_allocator.adb b/tests/integration/session_setting_of_message_fields/generated/rflx-test-session_allocator.adb index e1ad07013..85d68b5b9 100644 --- a/tests/integration/session_setting_of_message_fields/generated/rflx-test-session_allocator.adb +++ b/tests/integration/session_setting_of_message_fields/generated/rflx-test-session_allocator.adb @@ -11,6 +11,7 @@ is is begin S.Slot_Ptr_1 := M.Slot_1'Unrestricted_Access; + S.Slot_Ptr_2 := M.Slot_2'Unrestricted_Access; end Initialize; procedure Finalize (S : in out Slots) with @@ -19,6 +20,7 @@ is is begin S.Slot_Ptr_1 := null; + S.Slot_Ptr_2 := null; end Finalize; end RFLX.Test.Session_Allocator; diff --git a/tests/integration/session_setting_of_message_fields/generated/rflx-test-session_allocator.ads b/tests/integration/session_setting_of_message_fields/generated/rflx-test-session_allocator.ads index a89492048..f5966169d 100644 --- a/tests/integration/session_setting_of_message_fields/generated/rflx-test-session_allocator.ads +++ b/tests/integration/session_setting_of_message_fields/generated/rflx-test-session_allocator.ads @@ -13,6 +13,7 @@ is type Memory is record 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); end record; subtype Slot_Ptr_Type_4096 is RFLX_Types.Bytes_Ptr with @@ -24,13 +25,16 @@ is type Slots is record Slot_Ptr_1 : Slot_Ptr_Type_4096; + Slot_Ptr_2 : Slot_Ptr_Type_4096; end record; function Initialized (S : Slots) return Boolean is - (S.Slot_Ptr_1 /= null); + (S.Slot_Ptr_1 /= null + and S.Slot_Ptr_2 /= null); function Uninitialized (S : Slots) return Boolean is - (S.Slot_Ptr_1 = null); + (S.Slot_Ptr_1 = null + and S.Slot_Ptr_2 = null); procedure Initialize (S : out Slots; M : Memory) with Post => @@ -41,6 +45,7 @@ is Uninitialized (S); function Global_Allocated (S : Slots) return Boolean is - (S.Slot_Ptr_1 = null); + (S.Slot_Ptr_1 = null + and S.Slot_Ptr_2 /= null); end RFLX.Test.Session_Allocator; diff --git a/tests/integration/session_setting_of_message_fields/test.rflx b/tests/integration/session_setting_of_message_fields/test.rflx index 9ee991ec1..d1fa601d4 100644 --- a/tests/integration/session_setting_of_message_fields/test.rflx +++ b/tests/integration/session_setting_of_message_fields/test.rflx @@ -22,6 +22,7 @@ package Test is end Start; state Process is + Local_Message : Universal::Message; begin -- §S-S-A-MFA-L Message.Message_Type := Universal::MT_Data; @@ -29,8 +30,12 @@ package Test is Message.Length := 1; -- §S-S-A-MFA-A Message.Data := [2]; + -- §S-S-A-MFA-L + Local_Message.Message_Type := Universal::MT_Null; transition - goto Reply -- §S-S-T-N + goto Reply + if Message.Message_Type /= Local_Message.Message_Type -- §S-S-T-S, §S-E-S-V + goto Terminated -- §S-S-T-N exception goto Terminated -- §S-S-E end Process; diff --git a/tests/unit/expression_test.py b/tests/unit/expression_test.py index 1be9a107b..8bd772f4c 100644 --- a/tests/unit/expression_test.py +++ b/tests/unit/expression_test.py @@ -22,6 +22,7 @@ CaseExpr, Comprehension, Conversion, + DeltaMessageAggregate, Div, Equal, Expr, @@ -2245,6 +2246,174 @@ def test_message_aggregate_variables() -> None: assert result == expected +@pytest.mark.parametrize( + "field_values,type_", + [ + ( + {"Y": Variable("A", type_=rty.Integer("A")), "Z": Variable("B", type_=rty.BOOLEAN)}, + rty.Message( + "M", + { + ("X",), + ("X", "Y"), + ("X", "Y", "Z"), + }, + {}, + { + ID("Y"): rty.Integer("A"), + ID("Z"): rty.BOOLEAN, + }, + ), + ), + ( + {"Y": Variable("A", type_=rty.Message("I"))}, + rty.Message( + "M", + { + ("X", "Y", "Z"), + }, + {}, + { + ID("Y"): rty.OPAQUE, + }, + [ + rty.Refinement(ID("Y"), rty.Message("I"), "P"), + rty.Refinement(ID("Y"), rty.Message("J"), "P"), + ], + ), + ), + ], +) +def test_delta_message_aggregate_type(field_values: Mapping[StrID, Expr], type_: rty.Type) -> None: + assert_type( + DeltaMessageAggregate( + "M", + field_values, + type_=type_, + ), + type_, + ) + + +@pytest.mark.parametrize( + "field_values,type_,match", + [ + ( + { + "X": Variable("A", location=Location((10, 30))), + "Y": Variable("B", location=Location((10, 40))), + }, + rty.Message( + "M", + { + ("X", "Y"), + }, + {}, + { + ID("X"): rty.Integer("A"), + ID("Y"): rty.BOOLEAN, + }, + ), + r'^:10:30: model: error: undefined variable "A"\n' + r':10:40: model: error: undefined variable "B"$', + ), + ( + { + "X": Variable("A", type_=rty.Integer("A")), + "Y": Variable("B", type_=rty.BOOLEAN), + ID("Z", location=Location((10, 50))): Variable("Z", type_=rty.Integer("A")), + }, + rty.Message( + "M", + { + ("X", "Y"), + }, + {}, + { + ID("X"): rty.Integer("A"), + ID("Y"): rty.BOOLEAN, + }, + ), + r'^:10:50: model: error: invalid field "Z" for message type "M"$', + ), + ( + { + "Y": Variable("B", type_=rty.BOOLEAN), + ID("X", location=Location((10, 30))): Variable("A", type_=rty.Integer("A")), + }, + rty.Message( + "M", + { + ("X", "Y"), + }, + {}, + { + ID("X"): rty.Integer("A"), + ID("Y"): rty.BOOLEAN, + }, + ), + r'^:10:30: model: error: invalid position for field "X" of message type "M"$', + ), + ( + { + "X": Variable("A", location=Location((10, 40))), + "Y": Variable("B", location=Location((10, 30))), + }, + rty.Undefined(), + r'^:10:40: model: error: undefined variable "A"\n' + r':10:30: model: error: undefined variable "B"\n' + r':10:20: model: error: undefined message "T"$', + ), + ], +) +def test_delta_message_aggregate_type_error( + field_values: Mapping[StrID, Expr], type_: rty.Type, match: str +) -> None: + assert_type_error( + DeltaMessageAggregate("T", field_values, type_=type_, location=Location((10, 20))), + match, + ) + + +def test_delta_message_aggregate_substituted() -> None: + assert_equal( + DeltaMessageAggregate("X", {"Y": Variable("A"), "Z": Variable("B")}).substituted( + lambda x: Variable(f"P_{x}") if isinstance(x, Variable) else x + ), + DeltaMessageAggregate("X", {"Y": Variable("P_A"), "Z": Variable("P_B")}), + ) + assert_equal( + DeltaMessageAggregate("X", {"Y": Variable("A"), "Z": Variable("B")}).substituted( + lambda x: Variable("Z") if isinstance(x, DeltaMessageAggregate) else x + ), + Variable("Z"), + ) + + +def test_delta_message_aggregate_substituted_location() -> None: + expr = DeltaMessageAggregate( + "X", {"Y": Variable("A"), "Z": Variable("B")}, location=Location((1, 2)) + ).substituted(lambda x: x) + assert expr.location + + +def test_delta_message_aggregate_simplified() -> None: + assert_equal( + DeltaMessageAggregate( + "X", {"Y": Variable("A"), "Z": Add(Number(1), Number(2))} + ).simplified(), + DeltaMessageAggregate("X", {"Y": Variable("A"), "Z": Number(3)}), + ) + + +def test_delta_message_aggregate_variables() -> None: + result = DeltaMessageAggregate( + "Aggr", {"X": Variable("A"), "Y": Variable("B"), "Baz": Variable("C")} + ).variables() + expected = [Variable("A"), Variable("B"), Variable("C")] + assert result == expected + + def test_binding_type() -> None: assert_type( Binding( diff --git a/tests/unit/model/message_test.py b/tests/unit/model/message_test.py index f59260f56..6b027a1ad 100644 --- a/tests/unit/model/message_test.py +++ b/tests/unit/model/message_test.py @@ -2897,8 +2897,16 @@ def test_size() -> None: } ) == Number(32) assert optional_overlayed_field.size() == Add( - IfExpr([(Equal(Variable("A"), Number(0)), Number(16))], Number(0)), - IfExpr([(Greater(Variable("A"), Number(0)), Number(32))], Number(0)), + IfExpr( + [ + ( + And(Greater(Variable("A"), Number(0)), NotEqual(Variable("A"), Number(0))), + Number(16), + ) + ], + Number(0), + ), + Number(16), ) path_dependent_fields = Message( @@ -2940,6 +2948,328 @@ def test_size() -> None: ) +def test_size_subpath() -> None: + assert NULL_MESSAGE.size({}, subpath=True) == Number(0) + + assert FIXED_SIZE_MESSAGE.size( + { + Field("Message_Type"): Literal("Universal::MT_Data"), + }, + subpath=True, + ) == Number(8) + assert FIXED_SIZE_MESSAGE.size( + { + Field("Data"): Aggregate(*[Number(0)] * 4), + }, + subpath=True, + ) == Number(32) + assert FIXED_SIZE_MESSAGE.size( + { + Field("Message_Type"): Literal("Universal::MT_Data"), + Field("Data"): Aggregate(*[Number(0)] * 4), + }, + subpath=True, + ) == Number(40) + + assert DEFINITE_MESSAGE.size( + { + Field("Length"): Number(8), + }, + subpath=True, + ) == Number(16) + assert DEFINITE_MESSAGE.size( + { + Field("Data"): Variable("D"), + }, + subpath=True, + ) == Size("D") + assert DEFINITE_MESSAGE.size( + { + Field("Length"): Variable("L"), + Field("Data"): Variable("D"), + }, + subpath=True, + ) == Add(Size("D"), Number(16)) + + assert TLV_MESSAGE.size( + { + Field("Tag"): Variable("T"), + }, + subpath=True, + ) == Number(8) + assert TLV_MESSAGE.size( + { + Field("Tag"): Variable("T"), + Field("Length"): Variable("L"), + Field("Value"): Aggregate(*[Number(0)] * 4), + }, + subpath=True, + ) == Number(56) + assert TLV_MESSAGE.size( + { + Field("Tag"): Variable("T"), + Field("Length"): Variable("L"), + }, + subpath=True, + ) == Number(24) + assert TLV_MESSAGE.size( + { + Field("Length"): Div(Add(Size("Tag"), Size("TLV::Length")), Number(8)), + Field("Value"): Aggregate(*[Number(0)] * 3), + }, + subpath=True, + ) == Number(40) + assert TLV_MESSAGE.size( + { + Field("Length"): Add(Div(Size("X"), Number(8)), Variable("Y")), + Field("Value"): Variable("Z"), + }, + subpath=True, + ) == Add(Size("Z"), Number(16)) + assert TLV_MESSAGE.size( + { + Field("Length"): Div(Size("Msg_Data"), Number(8)), + Field("Value"): Opaque("Msg_Data"), + }, + subpath=True, + ) == Add(Mul(Div(Size("Msg_Data"), Number(8)), Number(8)), Number(16)) + + assert ETHERNET_FRAME.size( + { + Field("Destination"): Number(0), + Field("Source"): Number(0), + Field("Type_Length_TPID"): Number(46), + Field("Type_Length"): Number(46), + Field("Payload"): Aggregate(*[Number(0)] * 46), + }, + subpath=True, + ) == Number(480) + assert ETHERNET_FRAME.size( + { + Field("Destination"): Number(0), + Field("Source"): Number(0), + Field("Type_Length_TPID"): Number(0x8100), + Field("TPID"): Number(0x8100), + Field("TCI"): Number(0), + Field("Type_Length"): Number(46), + Field("Payload"): Aggregate(*[Number(0)] * 46), + }, + subpath=True, + ) == Number(512) + assert ETHERNET_FRAME.size( + { + Field("Destination"): Number(0), + Field("Source"): Number(0), + Field("Type_Length_TPID"): Number(1536), + Field("Type_Length"): Number(1536), + Field("Payload"): Aggregate(*[Number(0)] * 46), + }, + subpath=True, + ) == Number(480) + assert ETHERNET_FRAME.size( + { + Field("Destination"): Number(0), + Field("Source"): Number(0), + Field("Type_Length_TPID"): Number(1536), + Field("Type_Length"): Number(1536), + Field("Payload"): Variable("Payload"), + }, + subpath=True, + ) == Add(Size("Payload"), Number(112)) + + variable_field_value = Message( + "Test::Message", + [ + Link(INITIAL, Field("Length")), + Link( + Field("Length"), + Field("Data"), + condition=Equal(Variable("Has_Data"), TRUE), + size=Mul(Variable("Length"), Number(8)), + ), + Link( + Field("Length"), + Field("Data"), + condition=Equal(Variable("Has_Data"), FALSE), + size=Number(0), + ), + Link( + Field("Data"), + FINAL, + ), + ], + { + Field("Has_Data"): BOOLEAN, + Field("Length"): TLV_LENGTH, + Field("Data"): OPAQUE, + }, + ) + assert variable_field_value.size( + { + Field("Length"): Variable("Y"), + Field("Data"): Selected(Variable("M"), "F"), + }, + ID("X"), + subpath=True, + ) == Add( + IfExpr( + [ + ( + Equal(Selected(Variable("X"), "Has_Data"), FALSE), + Size(Selected(Variable("M"), "F")), + ) + ], + Number(0), + ), + IfExpr( + [ + ( + Equal(Selected(Variable("X"), "Has_Data"), TRUE), + Size(Selected(Variable("M"), "F")), + ) + ], + Number(0), + ), + Number(16), + ) + assert variable_field_value.size( + { + Field("Length"): Variable("Y"), + Field("Data"): Variable("Z"), + }, + ID("X"), + subpath=True, + ) == Add( + IfExpr( + [(Equal(Selected(Variable("X"), "Has_Data"), FALSE), Size(Variable("Z")))], Number(0) + ), + IfExpr( + [(Equal(Selected(Variable("X"), "Has_Data"), TRUE), Size(Variable("Z")))], Number(0) + ), + Number(16), + ) + + optional_overlayed_field = Message( + "Test::Message", + [ + Link(INITIAL, Field("A")), + Link( + Field("A"), + Field("B"), + condition=Equal(Variable("A"), Number(0)), + first=First(Variable("A")), + ), + Link( + Field("A"), + Field("B"), + condition=Greater(Variable("A"), Number(0)), + ), + Link( + Field("B"), + FINAL, + ), + ], + { + Field("A"): TLV_LENGTH, + Field("B"): TLV_LENGTH, + }, + ) + assert optional_overlayed_field.size( + { + Field("A"): Number(0), + Field("B"): Number(0), + }, + subpath=True, + ) == Number(16) + assert optional_overlayed_field.size( + { + Field("A"): Number(1), + Field("B"): Number(2), + }, + subpath=True, + ) == Number(32) + assert optional_overlayed_field.size( + { + Field("A"): Number(1), + }, + subpath=True, + ) == Number(16) + assert optional_overlayed_field.size({Field("B"): Number(1)}, subpath=True) == IfExpr( + [ + ( + And(Greater(Variable("A"), Number(0)), NotEqual(Variable("A"), Number(0))), + Number(16), + ) + ], + Number(0), + ) + + path_dependent_fields = Message( + "Test::Message", + [ + Link(INITIAL, Field("A")), + Link( + Field("A"), + Field("B"), + condition=Equal(Variable("A"), Number(0)), + ), + Link( + Field("A"), + Field("C"), + condition=Greater(Variable("A"), Number(0)), + ), + Link( + Field("B"), + FINAL, + ), + Link( + Field("C"), + FINAL, + ), + ], + { + Field("A"): TLV_LENGTH, + Field("B"): TLV_LENGTH, + Field("C"): TLV_LENGTH, + }, + ) + assert path_dependent_fields.size( + {Field("A"): Variable("X"), Field("B"): Number(0)}, + subpath=True, + ) == Number(32) + assert path_dependent_fields.size( + {Field("A"): Variable("X"), Field("C"): Variable("Y")}, + subpath=True, + ) == Number(32) + assert path_dependent_fields.size( + {Field("A"): Variable("X")}, + subpath=True, + ) == Number(16) + assert path_dependent_fields.size( + {Field("B"): Variable("X")}, + subpath=True, + ) == Number(16) + + +def test_size_subpath_error() -> None: + with pytest.raises( + RecordFluxError, + match=( + r"^" + r'model: error: unable to calculate size of invalid subpath "Tag -> Value"' + r' of message "TLV::Message"' + r"$" + ), + ): + TLV_MESSAGE.size( + { + Field("Tag"): Variable("T"), + Field("Value"): Variable("V"), + }, + subpath=True, + ) + + def test_max_size() -> None: assert NULL_MESSAGE.max_size() == Number(0) assert FIXED_SIZE_MESSAGE.max_size() == Number(8 + 3 * 64) diff --git a/tests/unit/model/session_test.py b/tests/unit/model/session_test.py index d9706fd1e..1cffd7866 100644 --- a/tests/unit/model/session_test.py +++ b/tests/unit/model/session_test.py @@ -1,4 +1,7 @@ # pylint: disable=too-many-lines + +from __future__ import annotations + import typing as ty import pytest @@ -646,6 +649,30 @@ def test_assignment_from_undeclared_variable() -> None: ) +def test_assignment_with_undeclared_message_in_delta_message_aggregate() -> None: + assert_session_model_error( + states=[ + State( + "Start", + transitions=[Transition(target=ID("End"))], + exception_transition=Transition(target=ID("End")), + declarations=[], + actions=[ + stmt.Assignment( + "Global", + expr.DeltaMessageAggregate("Undefined", {}, location=Location((10, 20))), + ) + ], + ), + State("End"), + ], + declarations=[decl.VariableDeclaration("Global", "Boolean")], + parameters=[], + types=[BOOLEAN], + regex=r'^:10:20: model: error: undefined message "Undefined"$', + ) + + def test_reset_of_undeclared_list() -> None: assert_session_model_error( states=[ @@ -2372,3 +2399,247 @@ def test_resolving_of_function_calls() -> None: local_stmt = session.states[0].actions[0] assert isinstance(local_stmt, stmt.Assignment) assert local_stmt.expression == expr.Call("Func") + + +@pytest.mark.parametrize( + "actions, normalized_actions", + [ + ( + [ + stmt.MessageFieldAssignment( + "M", + "A", + expr.Number(1), + ), + ], + [ + stmt.MessageFieldAssignment( + "M", + "A", + expr.Number(1), + ), + ], + ), + ( + [ + stmt.MessageFieldAssignment( + "M", + "A", + expr.Number(1), + ), + stmt.MessageFieldAssignment( + "M", + "B", + expr.Number(2), + ), + stmt.MessageFieldAssignment( + "M", + "C", + expr.Number(3), + ), + ], + [ + stmt.Assignment( + "M", + expr.DeltaMessageAggregate( + "M", + { + "A": expr.Number(1), + "B": expr.Number(2), + "C": expr.Number(3), + }, + ), + ), + ], + ), + ( + [ + stmt.MessageFieldAssignment( + "M1", + "A", + expr.Number(1), + ), + stmt.MessageFieldAssignment( + "M2", + "B", + expr.Number(2), + ), + stmt.MessageFieldAssignment( + "M2", + "C", + expr.Number(3), + ), + ], + [ + stmt.MessageFieldAssignment( + "M1", + "A", + expr.Number(1), + ), + stmt.Assignment( + "M2", + expr.DeltaMessageAggregate( + "M2", + { + "B": expr.Number(2), + "C": expr.Number(3), + }, + ), + ), + ], + ), + ( + [ + stmt.MessageFieldAssignment( + "M1", + "A", + expr.Number(1), + ), + stmt.MessageFieldAssignment( + "M1", + "B", + expr.Number(2), + ), + stmt.MessageFieldAssignment( + "M2", + "C", + expr.Number(3), + ), + ], + [ + stmt.Assignment( + "M1", + expr.DeltaMessageAggregate( + "M1", + { + "A": expr.Number(1), + "B": expr.Number(2), + }, + ), + ), + stmt.MessageFieldAssignment( + "M2", + "C", + expr.Number(3), + ), + ], + ), + ( + [ + stmt.MessageFieldAssignment( + "M1", + "A", + expr.Number(1), + ), + stmt.MessageFieldAssignment( + "M1", + "B", + expr.Number(2), + ), + stmt.MessageFieldAssignment( + "M2", + "C", + expr.Number(3), + ), + stmt.MessageFieldAssignment( + "M2", + "D", + expr.Number(4), + ), + ], + [ + stmt.Assignment( + "M1", + expr.DeltaMessageAggregate( + "M1", + { + "A": expr.Number(1), + "B": expr.Number(2), + }, + ), + ), + stmt.Assignment( + "M2", + expr.DeltaMessageAggregate( + "M2", + { + "C": expr.Number(3), + "D": expr.Number(4), + }, + ), + ), + ], + ), + ], +) +def test_state_normalization( + actions: list[stmt.Statement], normalized_actions: list[stmt.Statement] +) -> None: + assert str( + State( + "S", + transitions=[Transition(target=ID("End"))], + exception_transition=Transition(target=ID("End")), + actions=actions, + ) + ) == str( + State( + "S", + transitions=[Transition(target=ID("End"))], + exception_transition=Transition(target=ID("End")), + actions=normalized_actions, + ) + ) + assert State( + "S", + transitions=[Transition(target=ID("End"))], + exception_transition=Transition(target=ID("End")), + actions=actions, + ) == State( + "S", + transitions=[Transition(target=ID("End"))], + exception_transition=Transition(target=ID("End")), + actions=normalized_actions, + ) + assert str( + State( + "S", + transitions=[Transition(target=ID("End"))], + exception_transition=Transition(target=ID("End")), + actions=[ + stmt.Assignment("X", expr.Number(0)), + *actions, + stmt.Assignment("Y", expr.Number(9)), + ], + ) + ) == str( + State( + "S", + transitions=[Transition(target=ID("End"))], + exception_transition=Transition(target=ID("End")), + actions=[ + stmt.Assignment("X", expr.Number(0)), + *normalized_actions, + stmt.Assignment("Y", expr.Number(9)), + ], + ) + ) + assert State( + "S", + transitions=[Transition(target=ID("End"))], + exception_transition=Transition(target=ID("End")), + actions=[ + stmt.Assignment("X", expr.Number(0)), + *actions, + stmt.Assignment("Y", expr.Number(9)), + ], + ) == State( + "S", + transitions=[Transition(target=ID("End"))], + exception_transition=Transition(target=ID("End")), + actions=[ + stmt.Assignment("X", expr.Number(0)), + *normalized_actions, + stmt.Assignment("Y", expr.Number(9)), + ], + )