Prevent different casings for same entity

Ref. eng/recordflux/RecordFlux#563

CHANGELOG.md

@@ -7,6 +7,10 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ## [Unreleased]
 
+### Added
+
+- Prevent different casings for same entity (eng/recordflux/RecordFlux#563)
+
 ### Fixed
 
 - Unexpected errors when using different casings for same entity (AdaCore/RecordFlux#562, eng/recordflux/RecordFlux#1506)

examples/specs/tls_record.rflx

@@ -1,5 +1,5 @@
 with TLS_Alert;
-with Tls_Common;
+with TLS_Common;
 with Tls_Handshake;
 with Tls_Parameters;
 
@@ -62,22 +62,22 @@ package TLS_Record is
       message
          Prefix : Plaintext_Prefix;
          Tag : Plaintext_Content_Type;
-         Legacy_Record_Version : Tls_Common::Protocol_Version
+         Legacy_Record_Version : TLS_Common::Protocol_Version
             -- TLS
             then Length
-               if (Legacy_Record_Version = Tls_Common::TLS_1_0
-                  or Legacy_Record_Version = Tls_Common::TLS_1_1
-                  or Legacy_Record_Version = Tls_Common::TLS_1_2
-                  or Legacy_Record_Version = Tls_Common::TLS_1_3)
+               if (Legacy_Record_Version = TLS_Common::TLS_1_0
+                  or Legacy_Record_Version = TLS_Common::TLS_1_1
+                  or Legacy_Record_Version = TLS_Common::TLS_1_2
+                  or Legacy_Record_Version = TLS_Common::TLS_1_3)
                   and
                      -- The following content types are not defined for TLS
                      (Tag /= Tls12_Cid and Tag /= ACK)
             -- DTLS
             then Epoch
-               if Legacy_Record_Version /= Tls_Common::TLS_1_0
-                  and Legacy_Record_Version /= Tls_Common::TLS_1_1
-                  and Legacy_Record_Version /= Tls_Common::TLS_1_2
-                  and Legacy_Record_Version /= Tls_Common::TLS_1_3;
+               if Legacy_Record_Version /= TLS_Common::TLS_1_0
+                  and Legacy_Record_Version /= TLS_Common::TLS_1_1
+                  and Legacy_Record_Version /= TLS_Common::TLS_1_2
+                  and Legacy_Record_Version /= TLS_Common::TLS_1_3;
          Epoch : Plaintext_Epoch;
          Sequence_Number : Plaintext_Sequence_Number;
          Length : Plaintext_Length
@@ -87,8 +87,8 @@ package TLS_Record is
             then Encrypted_Record
                with Size => Length * 8
                if Tag = Application_Data
-                  and (Legacy_Record_Version = Tls_Common::TLS_1_2
-                     or Legacy_Record_Version = Tls_Common::DTLS_1_2);
+                  and (Legacy_Record_Version = TLS_Common::TLS_1_2
+                     or Legacy_Record_Version = TLS_Common::DTLS_1_2);
          Fragment : Opaque
             then null;
          Encrypted_Record : Opaque;
@@ -104,18 +104,18 @@ package TLS_Record is
    -- tls_handshake.rflx for more information.
    for TLS_Plaintext use (Fragment => TLS_Handshake::TLS_Handshake)
       if Tag = Handshake
-         and (Legacy_Record_Version = Tls_Common::TLS_1_0
-               or Legacy_Record_Version = Tls_Common::TLS_1_1
-               or Legacy_Record_Version = Tls_Common::TLS_1_2
-               or Legacy_Record_Version = Tls_Common::TLS_1_3);
+         and (Legacy_Record_Version = TLS_Common::TLS_1_0
+               or Legacy_Record_Version = TLS_Common::TLS_1_1
+               or Legacy_Record_Version = TLS_Common::TLS_1_2
+               or Legacy_Record_Version = TLS_Common::TLS_1_3);
 
    -- DTLS Handshake
    for TLS_Plaintext use (Fragment => TLS_Handshake::DTLS_Handshake)
       if Tag = Handshake
-         and (Legacy_Record_Version /= Tls_Common::TLS_1_0
-                  and Legacy_Record_Version /= Tls_Common::TLS_1_1
-                  and Legacy_Record_Version /= Tls_Common::TLS_1_2
-                  and Legacy_Record_Version /= Tls_Common::TLS_1_3);
+         and (Legacy_Record_Version /= TLS_Common::TLS_1_0
+                  and Legacy_Record_Version /= TLS_Common::TLS_1_1
+                  and Legacy_Record_Version /= TLS_Common::TLS_1_2
+                  and Legacy_Record_Version /= TLS_Common::TLS_1_3);
 
    for TLS_Plaintext use (Fragment => TLS_Alert::Alert)
       if Tag = Alert;
@@ -209,17 +209,17 @@ package TLS_Record is
 
    for TLS_Record use (Plaintext_Rec_Fragment => TLS_Handshake::TLS_Handshake)
       if Plaintext_Rec_Tag = Handshake
-         and (Plaintext_Rec_Legacy_Record_Version = Tls_Common::TLS_1_0
-               or Plaintext_Rec_Legacy_Record_Version = Tls_Common::TLS_1_1
-               or Plaintext_Rec_Legacy_Record_Version = Tls_Common::TLS_1_2
-               or Plaintext_Rec_Legacy_Record_Version = Tls_Common::TLS_1_3);
+         and (Plaintext_Rec_Legacy_Record_Version = TLS_Common::TLS_1_0
+               or Plaintext_Rec_Legacy_Record_Version = TLS_Common::TLS_1_1
+               or Plaintext_Rec_Legacy_Record_Version = TLS_Common::TLS_1_2
+               or Plaintext_Rec_Legacy_Record_Version = TLS_Common::TLS_1_3);
 
    for TLS_Record use (Plaintext_Rec_Fragment => TLS_Handshake::DTLS_Handshake)
       if Plaintext_Rec_Tag = Handshake
-         and (Plaintext_Rec_Legacy_Record_Version /= Tls_Common::TLS_1_0
-                  and Plaintext_Rec_Legacy_Record_Version /= Tls_Common::TLS_1_1
-                  and Plaintext_Rec_Legacy_Record_Version /= Tls_Common::TLS_1_2
-                  and Plaintext_Rec_Legacy_Record_Version /= Tls_Common::TLS_1_3);
+         and (Plaintext_Rec_Legacy_Record_Version /= TLS_Common::TLS_1_0
+                  and Plaintext_Rec_Legacy_Record_Version /= TLS_Common::TLS_1_1
+                  and Plaintext_Rec_Legacy_Record_Version /= TLS_Common::TLS_1_2
+                  and Plaintext_Rec_Legacy_Record_Version /= TLS_Common::TLS_1_3);
 
    for TLS_Record use (Plaintext_Rec_Fragment => TLS_Alert::Alert)
       if Plaintext_Rec_Tag = Alert;

rflx/error.py

@@ -51,6 +51,10 @@ def start(self) -> tuple[int, int]:
     def end(self) -> Optional[tuple[int, int]]:
         return self._end
 
+    @property
+    def short(self) -> Location:
+        return Location(self.start, Path(self.source.name) if self.source else None, self.end)
+
     def __hash__(self) -> int:
         return hash(self._start)
 

rflx/graph.py

@@ -11,7 +11,7 @@
 from rflx.error import RecordFluxError, Severity, Subsystem
 from rflx.expression import TRUE, UNDEFINED
 from rflx.identifier import ID
-from rflx.model import FINAL_STATE, AbstractSession, Link, Message
+from rflx.model import FINAL_STATE, Link, Message, Session
 
 log = logging.getLogger(__name__)
 
@@ -104,7 +104,7 @@ def _edge_label(link: Link) -> str:
     return result
 
 
-def create_session_graph(session: AbstractSession, ignore: Optional[Sequence[str]] = None) -> Dot:
+def create_session_graph(session: Session, ignore: Optional[Sequence[str]] = None) -> Dot:
     """
     Return pydot graph representation of session.
 

rflx/model/__init__.py

@@ -20,7 +20,6 @@
 from .model import Model as Model, UncheckedModel as UncheckedModel
 from .session import (
     FINAL_STATE as FINAL_STATE,
-    AbstractSession as AbstractSession,
     Session as Session,
     State as State,
     Transition as Transition,

rflx/model/message.py

@@ -171,6 +171,8 @@ def __init__(  # noqa: PLR0913
         if not self.error.errors and not skip_verification:
             self._verify()
 
+        self._check_identifiers(structure, types)
+
         self.error.propagate()
 
     def __hash__(self) -> int:
@@ -1253,7 +1255,6 @@ def _verify(self) -> None:
             proofs.check(self.error)
 
             self._prove_reachability(valid_paths)
-            self.error.propagate()
 
     def _determine_valid_paths(self) -> set[tuple[Link, ...]]:
         """Return all paths without contradictions."""
@@ -2118,6 +2119,29 @@ def _compute_first(self, lnk: Link) -> tuple[Field, expr.Expr]:
             return (lnk.source, expr.Size(lnk.source.affixed_name))
         return (root, expr.Add(dist, source_size).simplified())
 
+    def _check_identifiers(self, structure: Sequence[Link], types: Iterable[Field]) -> None:
+        self.error.extend(
+            mty.check_identifier_notation(
+                (
+                    e
+                    for l in sorted(structure)
+                    for e in (
+                        expr.Variable(l.source.identifier),
+                        expr.Variable(l.target.identifier),
+                        l.condition,
+                        l.size,
+                        l.first,
+                    )
+                ),
+                itertools.chain(
+                    (f.identifier for f in types),
+                    self._unqualified_enum_literals,
+                    self._qualified_enum_literals,
+                    self._type_names,
+                ),
+            ),
+        )
+
 
 class DerivedMessage(Message):
     def __init__(  # noqa: PLR0913
@@ -2213,6 +2237,7 @@ def __init__(  # noqa: PLR0913
         self._qualified_enum_literals = mty.qualified_enum_literals(self.dependencies)
         self._type_names = mty.qualified_type_names(self.dependencies)
 
+        self._check_identifiers()
         self._normalize()
 
         if not skip_verification:
@@ -2344,6 +2369,19 @@ def _verify_condition(self) -> None:
                         ],
                     )
 
+    def _check_identifiers(self) -> None:
+        self.error.extend(
+            mty.check_identifier_notation(
+                [expr.Variable(self.field.identifier), self.condition],
+                itertools.chain(
+                    (f.identifier for f in self.pdu.fields),
+                    self._unqualified_enum_literals,
+                    self._qualified_enum_literals,
+                    self._type_names,
+                ),
+            ),
+        )
+
     def __str__(self) -> str:
         condition = f"\n   if {self.condition}" if self.condition != expr.TRUE else ""
         return f"for {self.pdu.name} use ({self.field.name} => {self.sdu.name}){condition}"