From a1cfbac3a672c51797c2dd51bb5410e0b2e14bbf Mon Sep 17 00:00:00 2001 From: Johannes Kanig Date: Thu, 4 Apr 2024 12:03:12 +0900 Subject: [PATCH] Fix code generation for Boolean conditions In substitutions, field values and parameters are usually converted to the "target type" (typically Base_Integer). This conversion is now disabled for Boolean expressions. We add a simplification that rewrites (dis)equalities of the form "X = True/False" to simply "X" (or "not X"). The existing simplification which rewrites expressions such as "True = X" to "X = True" is removed, as both would now be simplified to "X". Ref. eng/recordflux/RecordFlux#1365 --- CHANGELOG.md | 5 ++ rflx/expression.py | 15 ++++ rflx/generator/common.py | 71 ++++++--------- rflx/generator/generator.py | 3 +- rflx/generator/message.py | 18 +++- .../boolean_variable/rflx-p-message.adb | 2 +- .../boolean_variable/rflx-p-message.ads | 18 ++-- .../generated/rflx-test-m.ads | 14 +-- .../generated/rflx-test-message.adb | 5 +- .../generated/rflx-test-message.ads | 34 ++----- tests/spark/generated/rflx-ipv4-option.ads | 1 - tests/spark/generated/rflx-ipv4-packet.ads | 12 +-- tests/unit/expression_test.py | 9 +- tests/unit/generator/generator_test.py | 89 ++++++++++--------- tests/unit/model/message_test.py | 20 ++--- 15 files changed, 154 insertions(+), 162 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 506ada1ae..e1e57b71a 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -11,6 +11,11 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 - Improve error messages for type refinements of non-message types (eng/recordflux/RecordFlux#383) +### Fixed + +- Generation of uncompilable code in the presence of some Boolean conditions (eng/recordflux/RecordFlux#1365) + + ## [0.20.0] - 2024-03-26 ### Added diff --git a/rflx/expression.py b/rflx/expression.py index 6a7d7dbcb..ec5430648 100644 --- a/rflx/expression.py +++ b/rflx/expression.py @@ -2400,6 +2400,21 @@ def _simplified( else FALSE ) + # We simplify expressions of the form X = True to X + # We need to negate X if the Boolean literal is False or the relation is "ne", + # but not when both are true + if relation_operator in [operator.eq, operator.ne]: + + def apply_op(e: Expr, invert: bool) -> Expr: + if invert: + return Not(e) + return e + + if left in [TRUE, FALSE]: + return apply_op(right, (left == FALSE) != (relation_operator == operator.ne)) + if right in [TRUE, FALSE]: + return apply_op(left, (right == FALSE) != (relation_operator == operator.ne)) + return self.__class__(left, right, self.location) @property diff --git a/rflx/generator/common.py b/rflx/generator/common.py index cfe161ff1..6edd3682e 100644 --- a/rflx/generator/common.py +++ b/rflx/generator/common.py @@ -82,10 +82,7 @@ def substitution( ) -> Callable[[expr.Expr], expr.Expr]: facts = substitution_facts(message, prefix, embedded, public, target_type) - def type_conversion(expression: expr.Expr) -> expr.Expr: - return expr.Call(type_to_id(target_type), target_type, [expression]) - - def func( # noqa: PLR0912 + def func( expression: expr.Expr, ) -> expr.Expr: def byte_aggregate(aggregate: expr.Aggregate) -> expr.Aggregate: @@ -161,28 +158,6 @@ def byte_aggregate(aggregate: expr.Aggregate) -> expr.Aggregate: ) return equal_call if isinstance(expression, expr.Equal) else expr.Not(equal_call) - boolean_literal = None - other = None - if ( - isinstance(expression.left, expr.Literal) - and expression.left.identifier in model.BOOLEAN.literals - ): - boolean_literal = expression.left - other = expression.right - if ( - isinstance(expression.right, expr.Literal) - and expression.right.identifier in model.BOOLEAN.literals - ): - boolean_literal = expression.right - other = expression.left - if boolean_literal and other: - return expression.__class__( - other, - type_conversion( - expr.Call("To_Base_Integer", rty.BASE_INTEGER, [boolean_literal]), - ), - ) - def field_value(field: model.Field) -> expr.Expr: if public: return expr.Call( @@ -275,40 +250,48 @@ def field_size(field: model.Field) -> expr.Expr: ) def parameter_value(parameter: model.Field, parameter_type: model.Type) -> expr.Expr: + var = ( + expr.Variable(parameter.name, type_=parameter_type.type_) + if embedded + else expr.Variable("Ctx" * parameter.identifier, type_=parameter_type.type_) + ) + if parameter_type == model.BOOLEAN: + return var if isinstance(parameter_type, model.Enumeration): - if embedded: - return expr.Call( - "To_Base_Integer", - rty.BASE_INTEGER, - [expr.Variable(parameter.name)], - ) - return expr.Call( - "To_Base_Integer", - rty.BASE_INTEGER, - [expr.Variable("Ctx" * parameter.identifier)], - ) + return expr.Call("To_Base_Integer", rty.BASE_INTEGER, [var]) if isinstance(parameter_type, model.Scalar): - if embedded: - return expr.Variable(parameter.name) - return expr.Variable("Ctx" * parameter.identifier) + return var assert False, f'unexpected type "{type(parameter_type).__name__}"' def field_value(field: model.Field, field_type: model.Type) -> expr.Expr: + call = expr.Call( + f"Get_{field.name}", + field_type.type_, + [expr.Variable("Ctx")], + ) + if isinstance(field_type, model.Enumeration): if public: + if field_type == model.BOOLEAN: + return call + return expr.Call( "To_Base_Integer", rty.BASE_INTEGER, - [expr.Call(f"Get_{field.name}", field_type.type_, [expr.Variable("Ctx")])], + [call], ) - return expr.Selected( + value = expr.Selected( expr.Indexed(cursors, expr.Variable(field.affixed_name)), "Value", ) + if field_type == model.BOOLEAN: + return expr.Call("To_Actual", rty.BOOLEAN, [value]) + return value + if isinstance(field_type, model.Scalar): if public: - return expr.Call(f"Get_{field.name}", field_type.type_, [expr.Variable("Ctx")]) + return call return expr.Selected( expr.Indexed(cursors, expr.Variable(field.affixed_name)), "Value", @@ -319,6 +302,8 @@ def field_value(field: model.Field, field_type: model.Type) -> expr.Expr: assert False, f'unexpected type "{type(field_type).__name__}"' def type_conversion(expression: expr.Expr) -> expr.Expr: + if expression.type_ == rty.BOOLEAN: + return expression return expr.Call(type_to_id(target_type), target_type, [expression]) return { diff --git a/rflx/generator/generator.py b/rflx/generator/generator.py index 3f95853b8..515b72b66 100644 --- a/rflx/generator/generator.py +++ b/rflx/generator/generator.py @@ -407,10 +407,9 @@ def _create_message( # noqa: PLR0912 context: list[ContextItem] = [WithClause(prefix * const.TYPES_PACKAGE)] body_context: list[ContextItem] = [] - if any(t.package == BUILTINS_PACKAGE for t in message.types.values()): + if any(t.package == BUILTINS_PACKAGE for t in message.field_types.values()): context.extend( [ - WithClause(prefix * const.BUILTIN_TYPES_PACKAGE), WithClause(prefix * const.BUILTIN_TYPES_CONVERSIONS_PACKAGE), UsePackageClause(prefix * const.BUILTIN_TYPES_CONVERSIONS_PACKAGE), ], diff --git a/rflx/generator/message.py b/rflx/generator/message.py index 9cfbcb5c9..8ea024ca1 100644 --- a/rflx/generator/message.py +++ b/rflx/generator/message.py @@ -86,6 +86,7 @@ ) from rflx.identifier import ID from rflx.model import ( + BOOLEAN, FINAL, INITIAL, Composite, @@ -2141,6 +2142,14 @@ def condition(field: Field, message: Message) -> Expr: **{expr.ValidChecksum(f): expr.TRUE for f in message.checksums}, }, ) + if message.field_types[field] == BOOLEAN: + c = c.substituted( + lambda x: ( + expr.Call("To_Actual", rty.BOOLEAN, [expr.Variable("Val")]) + if x == expr.Variable(field.name) + else x + ), + ) if isinstance(message.field_types[field], Scalar): c = c.substituted( lambda x: expr.Variable("Val") if x == expr.Variable(field.name) else x, @@ -3618,21 +3627,24 @@ def func(expression: expr.Expr) -> expr.Expr: if isinstance(expression, expr.Variable) and Field(expression.identifier) in message.fields: field_type = message.types[Field(expression.identifier)] + var = expr.Variable("Struct" * expression.identifier) + if field_type == BOOLEAN: + return var if isinstance(field_type, Enumeration): return expr.Call( "To_Base_Integer", rty.BASE_INTEGER, - [expr.Variable("Struct" * expression.identifier)], + [var], ) if isinstance(field_type, Scalar): return expr.Call( const.TYPES_BASE_INT, rty.BASE_INTEGER, - [expr.Variable("Struct" * expression.identifier)], + [var], ) - return expr.Variable("Struct" * expression.identifier) + return var return expression diff --git a/tests/data/generator/generated/boolean_variable/rflx-p-message.adb b/tests/data/generator/generated/boolean_variable/rflx-p-message.adb index 90b0b121b..153e165fe 100644 --- a/tests/data/generator/generated/boolean_variable/rflx-p-message.adb +++ b/tests/data/generator/generated/boolean_variable/rflx-p-message.adb @@ -150,7 +150,7 @@ is Value := Get (Ctx, Fld); if Valid_Value (Fld, Value) - and then Field_Condition (Ctx, Fld, Value) + and then Field_Condition (Ctx, Fld) then pragma Assert ((if Fld = F_B then Field_Last (Ctx, Fld) mod RFLX_Types.Byte'Size = 0)); pragma Assert ((((Field_Last (Ctx, Fld) + RFLX_Types.Byte'Size - 1) / RFLX_Types.Byte'Size) * RFLX_Types.Byte'Size) mod RFLX_Types.Byte'Size = 0); diff --git a/tests/data/generator/generated/boolean_variable/rflx-p-message.ads b/tests/data/generator/generated/boolean_variable/rflx-p-message.ads index aacf14f3c..439b14b2d 100644 --- a/tests/data/generator/generated/boolean_variable/rflx-p-message.ads +++ b/tests/data/generator/generated/boolean_variable/rflx-p-message.ads @@ -12,7 +12,6 @@ pragma Ada_2012; pragma Style_Checks ("N3aAbCdefhiIklnOprStux"); pragma Warnings (Off, "redundant conversion"); with RFLX.RFLX_Types; -with RFLX.RFLX_Builtin_Types; with RFLX.RFLX_Builtin_Types.Conversions; use RFLX.RFLX_Builtin_Types.Conversions; @@ -265,10 +264,9 @@ is pragma Warnings (Off, "postcondition does not mention function result"); - function Field_Condition (Ctx : Context; Fld : Field; Val : RFLX_Types.Base_Integer) return Boolean with + function Field_Condition (Ctx : Context; Fld : Field) return Boolean with Pre => RFLX.P.Message.Has_Buffer (Ctx) - and then RFLX.P.Message.Valid_Value (Fld, Val) and then RFLX.P.Message.Valid_Next (Ctx, Fld) and then RFLX.P.Message.Sufficient_Space (Ctx, Fld), Post => @@ -385,7 +383,7 @@ is and then RFLX.P.Message.Valid_Next (Ctx, RFLX.P.Message.F_A) and then Valid_Boolean (To_Base_Integer (Val)) and then RFLX.P.Message.Available_Space (Ctx, RFLX.P.Message.F_A) >= RFLX.P.Message.Field_Size (Ctx, RFLX.P.Message.F_A) - and then RFLX.P.Message.Field_Condition (Ctx, RFLX.P.Message.F_A, To_Base_Integer (Val)), + and then RFLX.P.Message.Field_Condition (Ctx, RFLX.P.Message.F_A), Post => Has_Buffer (Ctx) and Valid (Ctx, F_A) @@ -407,7 +405,7 @@ is and then RFLX.P.Message.Valid_Next (Ctx, RFLX.P.Message.F_B) and then RFLX.P.Valid_T (RFLX.P.To_Base_Integer (Val)) and then RFLX.P.Message.Available_Space (Ctx, RFLX.P.Message.F_B) >= RFLX.P.Message.Field_Size (Ctx, RFLX.P.Message.F_B) - and then RFLX.P.Message.Field_Condition (Ctx, RFLX.P.Message.F_B, RFLX.P.To_Base_Integer (Val)), + and then RFLX.P.Message.Field_Condition (Ctx, RFLX.P.Message.F_B), Post => Has_Buffer (Ctx) and Valid (Ctx, F_B) @@ -699,12 +697,12 @@ private when F_B => RFLX.P.Valid_T (Val))); - function Field_Condition (Ctx : Context; Fld : Field; Val : RFLX_Types.Base_Integer) return Boolean is + function Field_Condition (Ctx : Context; Fld : Field) return Boolean is ((case Fld is when F_A => True, when F_B => - RFLX_Types.Base_Integer (Ctx.Cursors (F_A).Value) = RFLX_Types.Base_Integer (To_Base_Integer (True)))); + To_Actual (Ctx.Cursors (F_A).Value))); function Field_Size (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Length is (Field_Size_Internal (Ctx.Cursors, Ctx.First, Ctx.Verified_Last, Ctx.Written_Last, Ctx.Buffer, Fld)); @@ -745,11 +743,11 @@ private function Well_Formed_Message (Ctx : Context) return Boolean is (Valid (Ctx, F_B) - and then RFLX_Types.Base_Integer (Ctx.Cursors (F_A).Value) = RFLX_Types.Base_Integer (To_Base_Integer (True))); + and then To_Actual (Ctx.Cursors (F_A).Value)); function Valid_Message (Ctx : Context) return Boolean is (Valid (Ctx, F_B) - and then RFLX_Types.Base_Integer (Ctx.Cursors (F_A).Value) = RFLX_Types.Base_Integer (To_Base_Integer (True))); + and then To_Actual (Ctx.Cursors (F_A).Value)); function Incomplete_Message (Ctx : Context) return Boolean is ((for some F in Field => @@ -780,7 +778,7 @@ private (Cursors (Fld)); function Valid_Structure (Struct : Structure) return Boolean is - (To_Base_Integer (Struct.A) = RFLX_Types.Base_Integer (To_Base_Integer (True))); + (Struct.A); function Sufficient_Buffer_Length (Ctx : Context; Unused_Struct : Structure) return Boolean is (RFLX_Types.Base_Integer (RFLX_Types.To_Last_Bit_Index (Ctx.Buffer_Last) - RFLX_Types.To_First_Bit_Index (Ctx.Buffer_First) + 1) >= 8); diff --git a/tests/feature/messages_with_multiple_initial_links/generated/rflx-test-m.ads b/tests/feature/messages_with_multiple_initial_links/generated/rflx-test-m.ads index 13e8dd047..4a0f88524 100644 --- a/tests/feature/messages_with_multiple_initial_links/generated/rflx-test-m.ads +++ b/tests/feature/messages_with_multiple_initial_links/generated/rflx-test-m.ads @@ -12,9 +12,6 @@ pragma Ada_2012; pragma Style_Checks ("N3aAbCdefhiIklnOprStux"); pragma Warnings (Off, "redundant conversion"); with RFLX.RFLX_Types; -with RFLX.RFLX_Builtin_Types; -with RFLX.RFLX_Builtin_Types.Conversions; -use RFLX.RFLX_Builtin_Types.Conversions; with RFLX.Universal; use RFLX.Universal; @@ -498,15 +495,8 @@ private pragma Warnings (Off, "unused variable ""*"""); function Valid_Predecessors_Invariant (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr; P : Boolean) return Boolean is - ((if - Well_Formed (Cursors (F_F1)) - then - RFLX_Types.Base_Integer (To_Base_Integer (P)) = RFLX_Types.Base_Integer (To_Base_Integer (True))) - and then (if - Well_Formed (Cursors (F_F2)) - then - Valid (Cursors (F_F1)) - or RFLX_Types.Base_Integer (To_Base_Integer (P)) = RFLX_Types.Base_Integer (To_Base_Integer (False)))) + ((if Well_Formed (Cursors (F_F1)) then P) + and then (if Well_Formed (Cursors (F_F2)) then Valid (Cursors (F_F1)) or not P)) with Pre => Cursors_Invariant (Cursors, First, Verified_Last), diff --git a/tests/feature/parameterized_messages/generated/rflx-test-message.adb b/tests/feature/parameterized_messages/generated/rflx-test-message.adb index ff757e5e2..b6b87035c 100644 --- a/tests/feature/parameterized_messages/generated/rflx-test-message.adb +++ b/tests/feature/parameterized_messages/generated/rflx-test-message.adb @@ -219,10 +219,7 @@ is and then Field_Size (Ctx, F_Data) = RFLX_Types.To_Bit_Length (Length) and then Ctx.Verified_Last = Field_Last (Ctx, F_Data) and then Invalid (Ctx, F_Extension) - and then (if - RFLX_Types.Base_Integer (To_Base_Integer (Ctx.Extended)) = RFLX_Types.Base_Integer (To_Base_Integer (True)) - then - Valid_Next (Ctx, F_Extension)) + and then (if Ctx.Extended then Valid_Next (Ctx, F_Extension)) and then Ctx.Buffer_First = Ctx.Buffer_First'Old and then Ctx.Buffer_Last = Ctx.Buffer_Last'Old and then Ctx.First = Ctx.First'Old diff --git a/tests/feature/parameterized_messages/generated/rflx-test-message.ads b/tests/feature/parameterized_messages/generated/rflx-test-message.ads index 6a28cd1ca..d1cc1912b 100644 --- a/tests/feature/parameterized_messages/generated/rflx-test-message.ads +++ b/tests/feature/parameterized_messages/generated/rflx-test-message.ads @@ -12,9 +12,6 @@ pragma Ada_2012; pragma Style_Checks ("N3aAbCdefhiIklnOprStux"); pragma Warnings (Off, "redundant conversion"); with RFLX.RFLX_Types; -with RFLX.RFLX_Builtin_Types; -with RFLX.RFLX_Builtin_Types.Conversions; -use RFLX.RFLX_Builtin_Types.Conversions; package RFLX.Test.Message with SPARK_Mode, @@ -456,10 +453,7 @@ is and then Well_Formed (Ctx, F_Data) and then (if Well_Formed_Message (Ctx) then Message_Last (Ctx) = Field_Last (Ctx, F_Data)) and then Invalid (Ctx, F_Extension) - and then (if - RFLX_Types.Base_Integer (To_Base_Integer (Ctx.Extended)) = RFLX_Types.Base_Integer (To_Base_Integer (True)) - then - Valid_Next (Ctx, F_Extension)) + and then (if Ctx.Extended then Valid_Next (Ctx, F_Extension)) and then Ctx.Buffer_First = Ctx.Buffer_First'Old and then Ctx.Buffer_Last = Ctx.Buffer_Last'Old and then Ctx.First = Ctx.First'Old @@ -502,10 +496,7 @@ is and Well_Formed (Ctx, F_Data) and (if Well_Formed_Message (Ctx) then Message_Last (Ctx) = Field_Last (Ctx, F_Data)) and Invalid (Ctx, F_Extension) - and (if - RFLX_Types.Base_Integer (To_Base_Integer (Ctx.Extended)) = RFLX_Types.Base_Integer (To_Base_Integer (True)) - then - Valid_Next (Ctx, F_Extension)) + and (if Ctx.Extended then Valid_Next (Ctx, F_Extension)) and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old @@ -556,10 +547,7 @@ is and Well_Formed (Ctx, F_Data) and (if Well_Formed_Message (Ctx) then Message_Last (Ctx) = Field_Last (Ctx, F_Data)) and Invalid (Ctx, F_Extension) - and (if - RFLX_Types.Base_Integer (To_Base_Integer (Ctx.Extended)) = RFLX_Types.Base_Integer (To_Base_Integer (True)) - then - Valid_Next (Ctx, F_Extension)) + and (if Ctx.Extended then Valid_Next (Ctx, F_Extension)) and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old @@ -659,11 +647,7 @@ private function Valid_Predecessors_Invariant (Cursors : Field_Cursors; First : RFLX_Types.Bit_Index; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length; Buffer : RFLX_Types.Bytes_Ptr; Length : Test.Length; Extended : Boolean) return Boolean is ((if Well_Formed (Cursors (F_Data)) then True) - and then (if - Well_Formed (Cursors (F_Extension)) - then - (Well_Formed (Cursors (F_Data)) - and then RFLX_Types.Base_Integer (To_Base_Integer (Extended)) = RFLX_Types.Base_Integer (To_Base_Integer (True))))) + and then (if Well_Formed (Cursors (F_Extension)) then (Well_Formed (Cursors (F_Data)) and then Extended))) with Pre => Cursors_Invariant (Cursors, First, Verified_Last), @@ -684,7 +668,7 @@ private True, when F_Extension => (Well_Formed (Cursors (F_Data)) - and then RFLX_Types.Base_Integer (To_Base_Integer (Extended)) = RFLX_Types.Base_Integer (To_Base_Integer (True))))) + and then Extended))) with Pre => Cursors_Invariant (Cursors, First, Verified_Last) @@ -832,8 +816,8 @@ private function Field_Condition (Ctx : Context; Fld : Field) return Boolean is ((case Fld is when F_Data => - RFLX_Types.Base_Integer (To_Base_Integer (Ctx.Extended)) = RFLX_Types.Base_Integer (To_Base_Integer (True)) - or else RFLX_Types.Base_Integer (To_Base_Integer (Ctx.Extended)) = RFLX_Types.Base_Integer (To_Base_Integer (False)), + Ctx.Extended + or else not Ctx.Extended, when F_Extension => True)); @@ -876,12 +860,12 @@ private function Well_Formed_Message (Ctx : Context) return Boolean is ((Well_Formed (Ctx, F_Data) - and then RFLX_Types.Base_Integer (To_Base_Integer (Ctx.Extended)) = RFLX_Types.Base_Integer (To_Base_Integer (False))) + and then not Ctx.Extended) or else Well_Formed (Ctx, F_Extension)); function Valid_Message (Ctx : Context) return Boolean is ((Valid (Ctx, F_Data) - and then RFLX_Types.Base_Integer (To_Base_Integer (Ctx.Extended)) = RFLX_Types.Base_Integer (To_Base_Integer (False))) + and then not Ctx.Extended) or else Valid (Ctx, F_Extension)); function Incomplete_Message (Ctx : Context) return Boolean is diff --git a/tests/spark/generated/rflx-ipv4-option.ads b/tests/spark/generated/rflx-ipv4-option.ads index 5c52bea1b..5e663aaf7 100644 --- a/tests/spark/generated/rflx-ipv4-option.ads +++ b/tests/spark/generated/rflx-ipv4-option.ads @@ -12,7 +12,6 @@ pragma Ada_2012; pragma Style_Checks ("N3aAbCdefhiIklnOprStux"); pragma Warnings (Off, "redundant conversion"); with RFLX.RFLX_Types; -with RFLX.RFLX_Builtin_Types; with RFLX.RFLX_Builtin_Types.Conversions; use RFLX.RFLX_Builtin_Types.Conversions; diff --git a/tests/spark/generated/rflx-ipv4-packet.ads b/tests/spark/generated/rflx-ipv4-packet.ads index e6774ae7c..51723f920 100644 --- a/tests/spark/generated/rflx-ipv4-packet.ads +++ b/tests/spark/generated/rflx-ipv4-packet.ads @@ -12,7 +12,6 @@ pragma Ada_2012; pragma Style_Checks ("N3aAbCdefhiIklnOprStux"); pragma Warnings (Off, "redundant conversion"); with RFLX.RFLX_Types; -with RFLX.RFLX_Builtin_Types; with RFLX.RFLX_Builtin_Types.Conversions; use RFLX.RFLX_Builtin_Types.Conversions; with RFLX.IPv4.Options; @@ -728,10 +727,7 @@ is and Invalid (Ctx, F_Destination) and Invalid (Ctx, F_Options) and Invalid (Ctx, F_Payload) - and (if - RFLX_Types.Base_Integer (To_Base_Integer (Get_Flag_R (Ctx))) = RFLX_Types.Base_Integer (To_Base_Integer (False)) - then - Valid_Next (Ctx, F_Flag_DF)) + and (if not Get_Flag_R (Ctx) then Valid_Next (Ctx, F_Flag_DF)) and Ctx.Buffer_First = Ctx.Buffer_First'Old and Ctx.Buffer_Last = Ctx.Buffer_Last'Old and Ctx.First = Ctx.First'Old @@ -1457,7 +1453,7 @@ private Well_Formed (Cursors (F_Flag_DF)) then (Valid (Cursors (F_Flag_R)) - and then RFLX_Types.Base_Integer (Cursors (F_Flag_R).Value) = RFLX_Types.Base_Integer (To_Base_Integer (False)))) + and then not To_Actual (Cursors (F_Flag_R).Value))) and then (if Well_Formed (Cursors (F_Flag_MF)) then Valid (Cursors (F_Flag_DF))) and then (if Well_Formed (Cursors (F_Fragment_Offset)) then Valid (Cursors (F_Flag_MF))) and then (if Well_Formed (Cursors (F_TTL)) then Valid (Cursors (F_Fragment_Offset))) @@ -1505,7 +1501,7 @@ private and then True), when F_Flag_DF => (Valid (Cursors (F_Flag_R)) - and then RFLX_Types.Base_Integer (Cursors (F_Flag_R).Value) = RFLX_Types.Base_Integer (To_Base_Integer (False))), + and then not To_Actual (Cursors (F_Flag_R).Value)), when F_Flag_MF => (Valid (Cursors (F_Flag_DF)) and then True), @@ -1852,7 +1848,7 @@ private when F_Identification => True, when F_Flag_R => - Val = RFLX_Types.Base_Integer (To_Base_Integer (False)), + not To_Actual (Val), when F_Flag_DF | F_Flag_MF | F_Fragment_Offset | F_TTL | F_Protocol | F_Header_Checksum | F_Source | F_Destination | F_Options | F_Payload => True)); diff --git a/tests/unit/expression_test.py b/tests/unit/expression_test.py index 31abd676d..f63ec9ba1 100644 --- a/tests/unit/expression_test.py +++ b/tests/unit/expression_test.py @@ -340,12 +340,12 @@ def test_ass_expr_simplified() -> None: And( Variable("A"), Or(Variable("B"), Variable("C")), - Equal(Variable("D"), TRUE), + Variable("D"), ), And( Variable("A"), Or(Variable("B"), Variable("C")), - Equal(Variable("D"), FALSE), + Not(Variable("D")), ), ), Variable("X"), @@ -1684,6 +1684,11 @@ def test_equal_simplified() -> None: assert Equal(Div(Number(1), Number(8)), Div(Number(1), Number(8))).simplified() == TRUE assert Equal(Div(Number(1), Number(8)), Div(Number(2), Number(8))).simplified() == FALSE assert Equal(Div(Number(1), Number(6)), Div(Number(1), Number(8))).simplified() == FALSE + assert Equal(Variable("X"), TRUE).simplified() == Variable("X") + assert Equal(Variable("X"), FALSE).simplified() == Not(Variable("X")) + assert NotEqual(Variable("X"), FALSE).simplified() == Variable("X") + assert NotEqual(Variable("X"), TRUE).simplified() == Not(Variable("X")) + assert NotEqual(TRUE, Variable("X")).simplified() == Not(Variable("X")) def test_equal_z3expr() -> None: diff --git a/tests/unit/generator/generator_test.py b/tests/unit/generator/generator_test.py index 16f5c9d9a..2c33782ed 100644 --- a/tests/unit/generator/generator_test.py +++ b/tests/unit/generator/generator_test.py @@ -58,9 +58,7 @@ class TC: Link( Field("B"), FINAL, - # TODO(eng/recordflux/RecordFlux#1365): Fix code generation - # condition=expr.Variable("A"), - condition=expr.Equal(expr.Variable("A"), expr.TRUE), + condition=expr.Variable("A"), ), ], { @@ -291,44 +289,6 @@ def test_substitution_relation_aggregate( ) -@pytest.mark.parametrize( - ("left", "right", "expected_left", "expected_right"), - [ - ( - expr.Variable("Value"), - expr.TRUE, - expr.Call("RFLX_Types::Base_Integer", rty.BASE_INTEGER, [expr.Variable("Value")]), - expr.Call( - "RFLX_Types::Base_Integer", - rty.BASE_INTEGER, - [expr.Call("To_Base_Integer", rty.BASE_INTEGER, [expr.TRUE])], - ), - ), - ( - expr.FALSE, - expr.Variable("Value"), - expr.Call("RFLX_Types::Base_Integer", rty.BASE_INTEGER, [expr.Variable("Value")]), - expr.Call( - "RFLX_Types::Base_Integer", - rty.BASE_INTEGER, - [expr.Call("To_Base_Integer", rty.BASE_INTEGER, [expr.FALSE])], - ), - ), - ], -) -@pytest.mark.parametrize("relation", [expr.Equal, expr.NotEqual]) -def test_substitution_relation_boolean_literal( - relation: Callable[[expr.Expr, expr.Expr], expr.Relation], - left: expr.Expr, - right: expr.Expr, - expected_left: expr.Expr, - expected_right: expr.Expr, -) -> None: - assert relation(left, right).substituted( - common.substitution(models.tlv_message(), ""), - ) == relation(expected_left, expected_right) - - @pytest.mark.parametrize( ("expressions", "expected"), [ @@ -2249,6 +2209,53 @@ def test_generate_field_size_optimization() -> None: ) +def test_param_enumeration_condition() -> None: + """Test proper substitution of parameter of enumeration type in link condition.""" + type_ = mty.Enumeration( + "P::T", + literals=[("E1", expr.Number(1)), ("E2", expr.Number(2))], + size=expr.Number(8), + always_valid=False, + ) + link = Link( + Field("A"), + Field("B"), + condition=expr.Equal(expr.Variable("Param", type_=type_.type_), expr.Literal("E1")), + ) + + message = Message( + "P::Message", + [ + Link(INITIAL, Field("A")), + link, + Link( + Field("B"), + FINAL, + ), + ], + { + Field("A"): type_, + Field("B"): models.universal_length(), + Field("Param"): type_, + }, + ) + assert_equal( + link.condition.substituted(common.substitution(message, "", embedded=True)), + expr.Equal( + expr.Call( + "RFLX_Types::Base_Integer", + rty.BASE_INTEGER, + [expr.Call("To_Base_Integer", rty.BASE_INTEGER, [expr.Variable("Param")])], + ), + expr.Call( + "RFLX_Types::Base_Integer", + rty.BASE_INTEGER, + [expr.Call("To_Base_Integer", rty.BASE_INTEGER, [expr.Literal("E1")])], + ), + ), + ) + + def test_generate_string_substitution() -> None: subst = common.substitution(models.definite_message(), "") assert subst(expr.String("abc")) == expr.Aggregate( diff --git a/tests/unit/model/message_test.py b/tests/unit/model/message_test.py index 7ef86838a..7f7c4b082 100644 --- a/tests/unit/model/message_test.py +++ b/tests/unit/model/message_test.py @@ -3071,13 +3071,13 @@ def test_size() -> None: Link( Field("Length"), Field("Data"), - condition=Equal(Variable("Has_Data"), TRUE), + condition=Variable("Has_Data"), size=Mul(Variable("Length"), Number(8)), ), Link( Field("Length"), Field("Data"), - condition=Equal(Variable("Has_Data"), FALSE), + condition=Not(Variable("Has_Data")), size=Number(0), ), Link( @@ -3101,7 +3101,7 @@ def test_size() -> None: IfExpr( [ ( - Or(Equal(Variable("X"), FALSE), Equal(Variable("X"), TRUE)), + Or(Variable("X"), Not(Variable("X"))), Size(Selected(Variable("M"), "F")), ), ], @@ -3117,7 +3117,7 @@ def test_size() -> None: }, ) == Add( IfExpr( - [(Or(Equal(Variable("X"), FALSE), Equal(Variable("X"), TRUE)), Size(Variable("Z")))], + [(Or(Variable("X"), Not(Variable("X"))), Size(Variable("Z")))], Number(0), ), Number(16), @@ -3382,8 +3382,8 @@ def test_size_subpath() -> None: [ ( Or( - Equal(Selected(Variable("X"), "Has_Data"), FALSE), - Equal(Selected(Variable("X"), "Has_Data"), TRUE), + Selected(Variable("X"), "Has_Data"), + Not(Selected(Variable("X"), "Has_Data")), ), Size(Selected(Variable("M"), "F")), ), @@ -3404,8 +3404,8 @@ def test_size_subpath() -> None: [ ( Or( - Equal(Selected(Variable("X"), "Has_Data"), FALSE), - Equal(Selected(Variable("X"), "Has_Data"), TRUE), + Selected(Variable("X"), "Has_Data"), + Not(Selected(Variable("X"), "Has_Data")), ), Size(Variable("Z")), ), @@ -4485,7 +4485,7 @@ def test_merge_message_with_condition_on_message_type_field() -> None: Field("Payload"), FINAL, condition=And( - Equal(Variable("Flag"), TRUE), + Variable("Flag"), Equal(Variable("Parameter"), Variable("E1")), ), ), @@ -4510,7 +4510,7 @@ def test_merge_message_with_condition_on_message_type_field() -> None: Field("Payload_I"), FINAL, condition=And( - Equal(Variable("Flag"), TRUE), + Variable("Flag"), Equal(Variable("Parameter"), Literal("P::E1")), ), ),