Rename Structural_Valid to Well_Formed

Ref. #986
AdaCore · Nov 4, 2022 · 0c641e8 · 0c641e8
1 parent e045fd8
commit 0c641e8
Show file tree

Hide file tree

Showing 119 changed files with 1,432 additions and 1,451 deletions.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -5,6 +5,12 @@ All notable changes to this project will be documented in this file.
 The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/),
 and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html).
 
+## [Unreleased]
+
+### Changed
+
+- Rename `Structural_Valid` to `Well_Formed` (#986)
+
 ## [0.7.1] - 2022-11-04
 
 ### Fixed

diff --git a/doc/user_guide/index.rst b/doc/user_guide/index.rst
@@ -202,20 +202,20 @@ All types and subprograms related to ``Message`` can be found in the package ``R
 - ``procedure Verify_Message (Ctx : in out Context)``
    - Verify all fields of message
 
-- ``function Structural_Valid (Ctx : Context; Fld : Field) return Boolean``
-   - Check if composite field is structural valid (i.e. location and size of field is correct, but content is not necessarily valid)
+- ``function Well_Formed (Ctx : Context; Fld : Field) return Boolean``
+   - Check if composite field is well formed (i.e. location and size of field is correct, but content is not necessarily valid)
 
 - ``function Present (Ctx : Context; Fld : Field) return Boolean``
-   - Check if composite field is structural valid and has non-zero size
+   - Check if composite field is well formed and has non-zero size
 
 - ``function Valid (Ctx : Context; Fld : Field) return Boolean``
    - Check if field is valid (i.e. it has valid structure and valid content)
 
 - ``function Incomplete (Ctx : Context; Fld : Field) return Boolean``
    - Check if buffer was too short to verify field
 
-- ``function Structural_Valid_Message (Ctx : Context) return Boolean``
-   - Check if all fields of message are at least structural valid
+- ``function Well_Formed_Message (Ctx : Context) return Boolean``
+   - Check if all fields of message are at least well formed
 
 - ``function Valid_Message (Ctx : Context) return Boolean``
    - Check if all fields of message are valid
@@ -267,7 +267,7 @@ A simple program to parse a ``TLV.Message`` could be as follows:
    begin
       RFLX.TLV.Message.Initialize (Context, Buffer, RFLX.RFLX_Types.To_Last_Bit_Index (Buffer'Last));
       RFLX.TLV.Message.Verify_Message (Context);
-      if RFLX.TLV.Message.Structural_Valid_Message (Context) then
+      if RFLX.TLV.Message.Well_Formed_Message (Context) then
          case RFLX.TLV.Message.Get_Tag (Context) is
             when RFLX.TLV.Msg_Data =>
                if RFLX.TLV.Message.Present (Context, RFLX.TLV.Message.F_Value) then

diff --git a/examples/apps/ping/src/icmpv4.adb b/examples/apps/ping/src/icmpv4.adb
@@ -239,7 +239,7 @@ is
       RFLX.IPv4.Packet.Initialize (IP_Context, Buf, RFLX.RFLX_Types.To_Last_Bit_Index (Buf'Last));
       RFLX.IPv4.Packet.Verify_Message (IP_Context);
       if
-         not RFLX.IPv4.Packet.Structural_Valid_Message (IP_Context)
+         not RFLX.IPv4.Packet.Well_Formed_Message (IP_Context)
          or else not RFLX.IPv4.Contains.ICMP_Message_In_Packet_Payload (IP_Context)
       then
          RFLX.IPv4.Packet.Take_Buffer (IP_Context, Buf);
@@ -249,7 +249,7 @@ is
       RFLX.IPv4.Contains.Switch_To_Payload (IP_Context, ICMP_Context);
       RFLX.ICMP.Message.Verify_Message (ICMP_Context);
       if
-         not RFLX.ICMP.Message.Structural_Valid_Message (ICMP_Context)
+         not RFLX.ICMP.Message.Well_Formed_Message (ICMP_Context)
          or else RFLX.ICMP.Message.Get_Tag (ICMP_Context) /= RFLX.ICMP.Echo_Reply
       then
          RFLX.ICMP.Message.Take_Buffer (ICMP_Context, Buf);

diff --git a/rflx/generator/common.py b/rflx/generator/common.py
@@ -370,7 +370,7 @@ def prefixed(name: str) -> expr.Expr:
             (
                 AndThen(
                     Call(
-                        "Structural_Valid",
+                        "Well_Formed",
                         [Indexed(prefixed("Cursors").ada_expr(), Variable(target.affixed_name))],
                     ),
                     *([condition.ada_expr()] if condition != expr.TRUE else []),
@@ -433,7 +433,7 @@ def cursors_invariant() -> Expr:
         Create the invariant that defines valid representations of fields.
 
         Each field cursor represents the state of one parsed or serialized message field.
-        This invariant ensures for all structurally valid fields that
+        This invariant ensures for all well formed fields that
 
             - the field bounds are inside the range of verified buffer part,
             - the field size is greater or equal to zero,
@@ -446,7 +446,7 @@ def cursors_invariant() -> Expr:
                 [
                     (
                         Call(
-                            "Structural_Valid",
+                            "Well_Formed",
                             [Indexed(Variable("Cursors"), Variable("F"))],
                         ),
                         And(
@@ -488,13 +488,13 @@ def valid_predecessors_invariant() -> Expr:
         """
         Create the invariant that defines the state of predecessors of valid fields.
 
-        This invariant ensures for all structurally valid message fields that
+        This invariant ensures for all well formed message fields that
 
-            - one of its predecessor fields is structurally valid,
+            - one of its predecessor fields is well formed,
             - the predecessor component in the cursor refers to a valid predecessor,
             - and the condition on the link between the field and its predecessor is fulfilled.
 
-        This ensures that there is a valid message path from each structurally valid field to the
+        This ensures that there is a valid message path from each well formed field to the
         initial field.
         """
         return AndThen(
@@ -503,7 +503,7 @@ def valid_predecessors_invariant() -> Expr:
                     [
                         (
                             Call(
-                                "Structural_Valid",
+                                "Well_Formed",
                                 [
                                     Indexed(
                                         Variable("Cursors"),
@@ -515,7 +515,7 @@ def valid_predecessors_invariant() -> Expr:
                                 *[
                                     expr.AndThen(
                                         expr.Call(
-                                            "Structural_Valid"
+                                            "Well_Formed"
                                             if l.source in composite_fields
                                             else "Valid",
                                             [
@@ -794,7 +794,7 @@ def initialize_field_statements(
         Assignment(
             Indexed(Variable("Ctx.Cursors"), Variable(field.affixed_name)),
             NamedAggregate(
-                ("State", Variable("S_Structural_Valid")),
+                ("State", Variable("S_Well_Formed")),
                 ("First", Variable("First")),
                 ("Last", Variable("Last")),
                 ("Value", Number(0)),
@@ -983,7 +983,7 @@ def create_sequence_instantiation(
                 element_type_identifier * "Size",
                 element_type_identifier * "Message_Last",
                 element_type_identifier * "Initialized",
-                element_type_identifier * "Structural_Valid_Message",
+                element_type_identifier * "Well_Formed_Message",
             ],
         )
     elif isinstance(element_type, model.Scalar):

diff --git a/rflx/generator/generator.py b/rflx/generator/generator.py
@@ -536,13 +536,11 @@ def _create_message(self, message: Message) -> dict[ID, Unit]:
             ),
             self._executor.submit(parser_generator.create_verify_message_procedure, message),
             self._executor.submit(parser_generator.create_present_function),
-            self._executor.submit(parser_generator.create_structural_valid_function),
+            self._executor.submit(parser_generator.create_well_formed_function),
             self._executor.submit(parser_generator.create_valid_function),
             self._executor.submit(parser_generator.create_incomplete_function),
             self._executor.submit(parser_generator.create_invalid_function),
-            self._executor.submit(
-                parser_generator.create_structural_valid_message_function, message
-            ),
+            self._executor.submit(parser_generator.create_well_formed_message_function, message),
             self._executor.submit(parser_generator.create_valid_message_function, message),
             self._executor.submit(parser_generator.create_incomplete_message_function),
             self._executor.submit(
@@ -1419,7 +1417,7 @@ def _refinement_conditions(
             conditions.extend(
                 [
                     expr.Call(
-                        pdu_identifier * "Structural_Valid",
+                        pdu_identifier * "Well_Formed",
                         [
                             expr.Variable(pdu_context),
                             expr.Variable(pdu_identifier * refinement.field.affixed_name),

diff --git a/rflx/generator/message.py b/rflx/generator/message.py
@@ -202,9 +202,7 @@ def create_state_type() -> UnitPart:
         private=[
             EnumerationType(
                 "Cursor_State",
-                dict.fromkeys(
-                    map(ID, ("S_Valid", "S_Structural_Valid", "S_Invalid", "S_Incomplete"))
-                ),
+                dict.fromkeys(map(ID, ("S_Valid", "S_Well_Formed", "S_Invalid", "S_Incomplete"))),
             )
         ]
     )
@@ -233,7 +231,7 @@ def create_cursor_type() -> UnitPart:
                     "State",
                     [
                         Variant(
-                            [Variable("S_Valid"), Variable("S_Structural_Valid")],
+                            [Variable("S_Valid"), Variable("S_Well_Formed")],
                             [
                                 Component(
                                     "First",
@@ -271,10 +269,10 @@ def create_cursor_validation_functions() -> UnitPart:
         [],
         [
             ExpressionFunctionDeclaration(
-                FunctionSpecification("Structural_Valid", "Boolean", parameters),
+                FunctionSpecification("Well_Formed", "Boolean", parameters),
                 Or(
                     Equal(Variable("Cursor.State"), Variable("S_Valid")),
-                    Equal(Variable("Cursor.State"), Variable("S_Structural_Valid")),
+                    Equal(Variable("Cursor.State"), Variable("S_Well_Formed")),
                 ),
             ),
             ExpressionFunctionDeclaration(
@@ -961,7 +959,7 @@ def create_copy_procedure(prefix: str, message: Message) -> UnitPart:
                         AndThen(
                             Call(prefix * message.identifier * "Has_Buffer", [Variable("Ctx")]),
                             Call(
-                                prefix * message.identifier * "Structural_Valid_Message",
+                                prefix * message.identifier * "Well_Formed_Message",
                                 [Variable("Ctx")],
                             ),
                             Equal(
@@ -1038,7 +1036,7 @@ def create_read_function(prefix: str, message: Message) -> UnitPart:
                         AndThen(
                             Call(prefix * message.identifier * "Has_Buffer", [Variable("Ctx")]),
                             Call(
-                                prefix * message.identifier * "Structural_Valid_Message",
+                                prefix * message.identifier * "Well_Formed_Message",
                                 [Variable("Ctx")],
                             ),
                         )
@@ -1095,7 +1093,7 @@ def create_generic_read_procedure(prefix: str, message: Message) -> UnitPart:
                         AndThen(
                             Call(prefix * message.identifier * "Has_Buffer", [Variable("Ctx")]),
                             Call(
-                                prefix * message.identifier * "Structural_Valid_Message",
+                                prefix * message.identifier * "Well_Formed_Message",
                                 [Variable("Ctx")],
                             ),
                             Call("Pre", [Call("Read", [Variable("Ctx")])]),
@@ -1928,7 +1926,7 @@ def create_successor_function(prefix: str, message: Message) -> UnitPart:
                         And(
                             Call(prefix * message.identifier * "Has_Buffer", [Variable("Ctx")]),
                             Call(
-                                prefix * message.identifier * "Structural_Valid",
+                                prefix * message.identifier * "Well_Formed",
                                 [Variable("Ctx"), Variable("Fld")],
                             ),
                             Call(
@@ -2050,9 +2048,7 @@ def create_valid_predecessor_function(
                                 *[
                                     expr.And(
                                         expr.Call(
-                                            "Structural_Valid"
-                                            if p in composite_fields
-                                            else "Valid",
+                                            "Well_Formed" if p in composite_fields else "Valid",
                                             [
                                                 expr.Indexed(
                                                     expr.Variable(ID("Ctx") * "Cursors"),
@@ -2150,7 +2146,7 @@ def create_message_last_function(prefix: str, message: Message) -> UnitPart:
                         AndThen(
                             Call(prefix * message.identifier * "Has_Buffer", [Variable("Ctx")]),
                             Call(
-                                prefix * message.identifier * "Structural_Valid_Message",
+                                prefix * message.identifier * "Well_Formed_Message",
                                 [Variable("Ctx")],
                             ),
                         )
@@ -2194,7 +2190,7 @@ def create_data_procedure(prefix: str, message: Message) -> UnitPart:
                         AndThen(
                             Call(prefix * message.identifier * "Has_Buffer", [Variable("Ctx")]),
                             Call(
-                                prefix * message.identifier * "Structural_Valid_Message",
+                                prefix * message.identifier * "Well_Formed_Message",
                                 [Variable("Ctx")],
                             ),
                             Equal(
@@ -2748,7 +2744,7 @@ def specification(field: Field) -> ProcedureSpecification:
                     ContractCases(
                         (
                             Call(
-                                "Structural_Valid",
+                                "Well_Formed",
                                 [Variable("Ctx"), Variable(f.affixed_name)],
                             ),
                             And(*common.context_cursor_unchanged(message, f, predecessors=False)),
@@ -3352,7 +3348,7 @@ def _create_to_structure_procedure(prefix: str, message: Message) -> UnitPart:
                         AndThen(
                             Call(prefix * message.identifier * "Has_Buffer", [Variable("Ctx")]),
                             Call(
-                                prefix * message.identifier * "Structural_Valid_Message",
+                                prefix * message.identifier * "Well_Formed_Message",
                                 [Variable("Ctx")],
                             ),
                         )
@@ -3497,7 +3493,7 @@ def _create_to_context_procedure(prefix: str, message: Message) -> UnitPart:
                     Postcondition(
                         And(
                             Call("Has_Buffer", [Variable("Ctx")]),
-                            Call("Structural_Valid_Message", [Variable("Ctx")]),
+                            Call("Well_Formed_Message", [Variable("Ctx")]),
                             *[
                                 Equal(e, Old(e))
                                 for e in [