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

@@ -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

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

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 {

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),
                 ],

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
 

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);

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);

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),

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