Revert "Simplify Valid_Context predicate and generating code"

For eng/recordflux/recordflux#1455

This reverts commit aa0abdf.

CHANGELOG.md

@@ -16,7 +16,6 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 - Syntax for passing repeated `-i` and `-v` options to `rflx validate` (eng/recordflux/RecordFlux#1441)
 - Simplified setter code and removed internal `Successor` function (eng/recordflux/RecordFlux#1448)
-- Simplified `Valid_Context` predicate (eng/recordflux/RecordFlux#1382)
 
 ### Fixed
 

examples/apps/ping/ping.gpr

@@ -33,7 +33,6 @@ project Ping is
    package Prove is
       for Proof_Switches ("Ada") use Defaults.Proof_Switches;
       for Proof_Switches ("rflx-rflx_arithmetic.adb") use ("--prover=Z3,altergo,cvc5,colibri", "--timeout=120");
-      for Proof_Switches ("rflx-icmp-message.adb") use ("--timeout=120");
    end Prove;
 
 end Ping;

rflx/generator/common.py

@@ -322,6 +322,7 @@ def type_conversion(expression: expr.Expr) -> expr.Expr:
 
 def message_structure_invariant(
     message: model.Message,
+    prefix: str,
     embedded: bool = False,
 ) -> Expr:
     """
@@ -337,64 +338,97 @@ def message_structure_invariant(
     def prefixed(name: str) -> expr.Expr:
         return expr.Selected(expr.Variable("Ctx"), name) if not embedded else expr.Variable(name)
 
-    def field_property(fld: model.Field) -> Expr:
-        return AndThen(
-            Equal(
-                Add(
-                    Sub(
-                        Selected(
-                            Indexed(
-                                prefixed("Cursors").ada_expr(),
-                                Variable(fld.affixed_name),
+    def link_property(link: model.Link, unique: bool) -> Expr:
+        field_type = message.types[link.target]
+        condition = link.condition.substituted(substitution(message, prefix, embedded)).simplified()
+        size = (
+            field_type.size
+            if isinstance(field_type, model.Scalar)
+            else link.size.substituted(
+                substitution(message, prefix, embedded, target_type=const.TYPES_BIT_LENGTH),
+            ).simplified()
+        )
+        first = (
+            prefixed("First")
+            if link.source == model.INITIAL
+            else link.first.substituted(
+                substitution(message, prefix, embedded, target_type=const.TYPES_BIT_INDEX),
+            )
+            .substituted(
+                mapping={
+                    expr.UNDEFINED: expr.Add(
+                        expr.Selected(
+                            expr.Indexed(
+                                prefixed("Cursors"),
+                                expr.Variable(link.source.affixed_name),
                             ),
                             "Last",
                         ),
-                        Selected(
-                            Indexed(
-                                prefixed("Cursors").ada_expr(),
-                                Variable(fld.affixed_name),
-                            ),
-                            "First",
-                        ),
+                        expr.Number(1),
                     ),
-                    Number(1),
-                ),
+                },
+            )
+            .simplified()
+        )
+        precond = (
+            AndThen(
                 Call(
-                    "Field_Size_Internal",
-                    [
-                        Variable("Cursors"),
-                        Variable("First"),
-                        Variable("Verified_Last"),
-                        Variable("Written_Last"),
-                        Variable("Buffer"),
-                        *[Variable(fld.name) for fld in message.parameter_types],
-                        Variable(fld.affixed_name),
-                    ],
+                    "Well_Formed",
+                    [Indexed(Variable("Cursors"), Variable(link.source.affixed_name))],
                 ),
-            ),
-            Equal(
-                Selected(
-                    Indexed(
-                        prefixed("Cursors").ada_expr(),
-                        Variable(fld.affixed_name),
+                condition.ada_expr(),
+            )
+            if link.source != model.INITIAL and not unique
+            else TRUE
+        )
+
+        return If(
+            [
+                (
+                    precond,
+                    AndThen(
+                        Equal(
+                            Add(
+                                Sub(
+                                    Selected(
+                                        Indexed(
+                                            prefixed("Cursors").ada_expr(),
+                                            Variable(link.target.affixed_name),
+                                        ),
+                                        "Last",
+                                    ),
+                                    Selected(
+                                        Indexed(
+                                            prefixed("Cursors").ada_expr(),
+                                            Variable(link.target.affixed_name),
+                                        ),
+                                        "First",
+                                    ),
+                                ),
+                                Number(1),
+                            ),
+                            size.ada_expr(),
+                        ),
+                        Equal(
+                            Selected(
+                                Indexed(
+                                    prefixed("Cursors").ada_expr(),
+                                    Variable(link.target.affixed_name),
+                                ),
+                                "First",
+                            ),
+                            first.ada_expr(),
+                        ),
                     ),
-                    "First",
-                ),
-                Call(
-                    "Field_First_Internal",
-                    [
-                        Variable("Cursors"),
-                        Variable("First"),
-                        Variable("Verified_Last"),
-                        Variable("Written_Last"),
-                        Variable("Buffer"),
-                        *[Variable(fld.name) for fld in message.parameter_types],
-                        Variable(fld.affixed_name),
-                    ],
                 ),
-            ),
+            ],
         )
 
+    def field_property(fld: model.Field) -> Expr:
+        incoming = message.incoming(fld)
+        unique = len(incoming) == 1
+        return AndThen(*[link_property(link, unique) for link in incoming])
+
     def map_invariant(fld: model.Field) -> Expr:
         return If(
             [
@@ -413,6 +447,7 @@ def map_invariant(fld: model.Field) -> Expr:
 
 def context_predicate(
     message: model.Message,
+    prefix: str,
 ) -> Expr:
     def invalid_successors_invariant() -> Expr:
         """
@@ -494,7 +529,7 @@ def invalid_successors_invariant() -> Expr:
             ],
         ),
         invalid_successors_invariant(),
-        message_structure_invariant(message, embedded=True),
+        message_structure_invariant(message, prefix, embedded=True),
     )
 
 

rflx/generator/generator.py

@@ -496,6 +496,7 @@ def _create_message(self, message: Message) -> dict[ID, Unit]:  # noqa: PLR0912
             self._executor.submit(
                 message_generator.create_valid_context_function,
                 message,
+                self._prefix,
             ),
             self._executor.submit(message_generator.create_context_type, message),
             self._executor.submit(message_generator.create_initialize_procedure, message),

rflx/generator/message.py

@@ -794,6 +794,7 @@ def fld_first_expr(fld: Field) -> expr.Expr:
 
 def create_valid_context_function(
     message: Message,
+    prefix: str,
 ) -> UnitPart:
     specification = FunctionSpecification(
         "Valid_Context",
@@ -831,7 +832,7 @@ def create_valid_context_function(
             ),
             ExpressionFunctionDeclaration(
                 specification,
-                common.context_predicate(message),
+                common.context_predicate(message, prefix),
                 [Postcondition(TRUE)],
             ),
             Pragma(

tests/feature/messages_with_single_opaque_field/generated/rflx-test-message.ads

@@ -644,8 +644,8 @@ private
       and then ((if
                     Well_Formed (Cursors (F_Data))
                  then
-                    Cursors (F_Data).Last - Cursors (F_Data).First + 1 = Field_Size_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Data)
-                    and then Cursors (F_Data).First = Field_First_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Data))))
+                    (Cursors (F_Data).Last - Cursors (F_Data).First + 1 = RFLX_Types.Bit_Length (Written_Last - First + 1)
+                     and then Cursors (F_Data).First = First))))
     with
      Post =>
        True;

tests/feature/parameterized_messages/generated/rflx-test-message.ads

@@ -761,13 +761,13 @@ private
       and then ((if
                     Well_Formed (Cursors (F_Data))
                  then
-                    Cursors (F_Data).Last - Cursors (F_Data).First + 1 = Field_Size_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Length, Extended, F_Data)
-                    and then Cursors (F_Data).First = Field_First_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Length, Extended, F_Data))
+                    (Cursors (F_Data).Last - Cursors (F_Data).First + 1 = RFLX_Types.Bit_Length (Length) * 8
+                     and then Cursors (F_Data).First = First))
                 and then (if
                              Well_Formed (Cursors (F_Extension))
                           then
-                             Cursors (F_Extension).Last - Cursors (F_Extension).First + 1 = Field_Size_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Length, Extended, F_Extension)
-                             and then Cursors (F_Extension).First = Field_First_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Length, Extended, F_Extension))))
+                             (Cursors (F_Extension).Last - Cursors (F_Extension).First + 1 = RFLX_Types.Bit_Length (Length) * 8
+                              and then Cursors (F_Extension).First = Cursors (F_Data).Last + 1))))
     with
      Post =>
        True;

tests/feature/session_case_expression_numeric/generated/rflx-test-message.ads

@@ -581,8 +581,8 @@ private
       and then ((if
                     Well_Formed (Cursors (F_Value))
                  then
-                    Cursors (F_Value).Last - Cursors (F_Value).First + 1 = Field_Size_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Value)
-                    and then Cursors (F_Value).First = Field_First_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Value))))
+                    (Cursors (F_Value).Last - Cursors (F_Value).First + 1 = 8
+                     and then Cursors (F_Value).First = First))))
     with
      Post =>
        True;

tests/feature/session_endianness/generated/rflx-messages-msg.ads

@@ -621,13 +621,13 @@ private
       and then ((if
                     Well_Formed (Cursors (F_A))
                  then
-                    Cursors (F_A).Last - Cursors (F_A).First + 1 = Field_Size_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_A)
-                    and then Cursors (F_A).First = Field_First_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_A))
+                    (Cursors (F_A).Last - Cursors (F_A).First + 1 = 32
+                     and then Cursors (F_A).First = First))
                 and then (if
                              Well_Formed (Cursors (F_B))
                           then
-                             Cursors (F_B).Last - Cursors (F_B).First + 1 = Field_Size_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_B)
-                             and then Cursors (F_B).First = Field_First_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_B))))
+                             (Cursors (F_B).Last - Cursors (F_B).First + 1 = 32
+                              and then Cursors (F_B).First = Cursors (F_A).Last + 1))))
     with
      Post =>
        True;

tests/feature/session_endianness/generated/rflx-messages-msg_le.ads

@@ -621,13 +621,13 @@ private
       and then ((if
                     Well_Formed (Cursors (F_C))
                  then
-                    Cursors (F_C).Last - Cursors (F_C).First + 1 = Field_Size_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_C)
-                    and then Cursors (F_C).First = Field_First_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_C))
+                    (Cursors (F_C).Last - Cursors (F_C).First + 1 = 32
+                     and then Cursors (F_C).First = First))
                 and then (if
                              Well_Formed (Cursors (F_D))
                           then
-                             Cursors (F_D).Last - Cursors (F_D).First + 1 = Field_Size_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_D)
-                             and then Cursors (F_D).First = Field_First_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_D))))
+                             (Cursors (F_D).Last - Cursors (F_D).First + 1 = 32
+                              and then Cursors (F_D).First = Cursors (F_C).Last + 1))))
     with
      Post =>
        True;

tests/feature/session_endianness/generated/rflx-messages-msg_le_nested.ads

@@ -664,18 +664,18 @@ private
       and then ((if
                     Well_Formed (Cursors (F_X_A))
                  then
-                    Cursors (F_X_A).Last - Cursors (F_X_A).First + 1 = Field_Size_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_X_A)
-                    and then Cursors (F_X_A).First = Field_First_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_X_A))
+                    (Cursors (F_X_A).Last - Cursors (F_X_A).First + 1 = 32
+                     and then Cursors (F_X_A).First = First))
                 and then (if
                              Well_Formed (Cursors (F_X_B))
                           then
-                             Cursors (F_X_B).Last - Cursors (F_X_B).First + 1 = Field_Size_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_X_B)
-                             and then Cursors (F_X_B).First = Field_First_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_X_B))
+                             (Cursors (F_X_B).Last - Cursors (F_X_B).First + 1 = 32
+                              and then Cursors (F_X_B).First = Cursors (F_X_A).Last + 1))
                 and then (if
                              Well_Formed (Cursors (F_Y))
                           then
-                             Cursors (F_Y).Last - Cursors (F_Y).First + 1 = Field_Size_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Y)
-                             and then Cursors (F_Y).First = Field_First_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Y))))
+                             (Cursors (F_Y).Last - Cursors (F_Y).First + 1 = 32
+                              and then Cursors (F_Y).First = Cursors (F_X_B).Last + 1))))
     with
      Post =>
        True;

tests/feature/session_functions/generated/rflx-test-definite_message.ads

@@ -773,18 +773,18 @@ private
       and then ((if
                     Well_Formed (Cursors (F_Message_Type))
                  then
-                    Cursors (F_Message_Type).Last - Cursors (F_Message_Type).First + 1 = Field_Size_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Message_Type)
-                    and then Cursors (F_Message_Type).First = Field_First_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Message_Type))
+                    (Cursors (F_Message_Type).Last - Cursors (F_Message_Type).First + 1 = 8
+                     and then Cursors (F_Message_Type).First = First))
                 and then (if
                              Well_Formed (Cursors (F_Length))
                           then
-                             Cursors (F_Length).Last - Cursors (F_Length).First + 1 = Field_Size_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Length)
-                             and then Cursors (F_Length).First = Field_First_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Length))
+                             (Cursors (F_Length).Last - Cursors (F_Length).First + 1 = 8
+                              and then Cursors (F_Length).First = Cursors (F_Message_Type).Last + 1))
                 and then (if
                              Well_Formed (Cursors (F_Data))
                           then
-                             Cursors (F_Data).Last - Cursors (F_Data).First + 1 = Field_Size_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Data)
-                             and then Cursors (F_Data).First = Field_First_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Data))))
+                             (Cursors (F_Data).Last - Cursors (F_Data).First + 1 = RFLX_Types.Bit_Length (Cursors (F_Length).Value) * 8
+                              and then Cursors (F_Data).First = Cursors (F_Length).Last + 1))))
     with
      Post =>
        True;

tests/feature/session_message_optimization/generated/rflx-test-option_data.ads

@@ -712,13 +712,13 @@ private
       and then ((if
                     Well_Formed (Cursors (F_Length))
                  then
-                    Cursors (F_Length).Last - Cursors (F_Length).First + 1 = Field_Size_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Length)
-                    and then Cursors (F_Length).First = Field_First_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Length))
+                    (Cursors (F_Length).Last - Cursors (F_Length).First + 1 = 16
+                     and then Cursors (F_Length).First = First))
                 and then (if
                              Well_Formed (Cursors (F_Data))
                           then
-                             Cursors (F_Data).Last - Cursors (F_Data).First + 1 = Field_Size_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Data)
-                             and then Cursors (F_Data).First = Field_First_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Data))))
+                             (Cursors (F_Data).Last - Cursors (F_Data).First + 1 = RFLX_Types.Bit_Length (Cursors (F_Length).Value) * 8
+                              and then Cursors (F_Data).First = Cursors (F_Length).Last + 1))))
     with
      Post =>
        True;

tests/feature/session_sequence_append_head/generated/rflx-tlv-message.ads

@@ -740,18 +740,18 @@ private
       and then ((if
                     Well_Formed (Cursors (F_Tag))
                  then
-                    Cursors (F_Tag).Last - Cursors (F_Tag).First + 1 = Field_Size_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Tag)
-                    and then Cursors (F_Tag).First = Field_First_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Tag))
+                    (Cursors (F_Tag).Last - Cursors (F_Tag).First + 1 = 8
+                     and then Cursors (F_Tag).First = First))
                 and then (if
                              Well_Formed (Cursors (F_Length))
                           then
-                             Cursors (F_Length).Last - Cursors (F_Length).First + 1 = Field_Size_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Length)
-                             and then Cursors (F_Length).First = Field_First_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Length))
+                             (Cursors (F_Length).Last - Cursors (F_Length).First + 1 = 16
+                              and then Cursors (F_Length).First = Cursors (F_Tag).Last + 1))
                 and then (if
                              Well_Formed (Cursors (F_Value))
                           then
-                             Cursors (F_Value).Last - Cursors (F_Value).First + 1 = Field_Size_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Value)
-                             and then Cursors (F_Value).First = Field_First_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Value))))
+                             (Cursors (F_Value).Last - Cursors (F_Value).First + 1 = RFLX_Types.Bit_Length (Cursors (F_Length).Value) * 8
+                              and then Cursors (F_Value).First = Cursors (F_Length).Last + 1))))
     with
      Post =>
        True;