Remove session aspects

Ref. AdaCore/RecordFlux#700
AdaCore · Sep 20, 2022 · 76e5a0c · 76e5a0c
1 parent 48e0580
commit 76e5a0c
Show file tree

Hide file tree

Showing 7 changed files with 6 additions and 49 deletions.
diff --git a/language/lexer.py b/language/lexer.py
@@ -74,8 +74,6 @@ class Token(LexerToken):  # type: ignore[misc]
     Opaque = WithText()
     Present = WithText()
     Valid = WithText()
-    Initial = WithText()
-    Final = WithText()
 
     # Symbols
     Dot = WithText()
@@ -224,8 +222,6 @@ class Token(LexerToken):  # type: ignore[misc]
     (Literal("Opaque"), Token.Opaque),
     (Literal("Present"), Token.Present),
     (Literal("Valid"), Token.Valid),
-    (Literal("Initial"), Token.Initial),
-    (Literal("Final"), Token.Final),
     (Literal(";"), Token.Semicolon),
     (Literal("::"), Token.DoubleColon),
     (Literal(":="), Token.Assignment),

diff --git a/language/parser.py b/language/parser.py
@@ -57,8 +57,6 @@
             lexer.Opaque,
             lexer.Present,
             lexer.Valid,
-            lexer.Initial,
-            lexer.Final,
             lexer.And,
             lexer.Or,
             lexer.Case,
@@ -476,16 +474,6 @@
         grammar.formal_function_declaration,
         grammar.channel_declaration,
     ),
-    session_aspects=ast.SessionAspects(
-        "with",
-        "Initial",
-        "=>",
-        grammar.unqualified_identifier,
-        ",",
-        "Final",
-        "=>",
-        grammar.unqualified_identifier,
-    ),
     renaming_declaration=ast.RenamingDecl(
         grammar.unqualified_identifier,
         ":",
@@ -546,7 +534,7 @@
     ),
     transition=ast.Transition(
         "goto",
-        grammar.unqualified_identifier,
+        Or(ast.NullID("null"), grammar.unqualified_identifier),
         Opt("with", grammar.description_aspect),
     ),
     state_body=ast.StateBody(
@@ -572,7 +560,6 @@
         Opt(List(grammar.session_parameter, sep=";"), ";"),
         "session",
         grammar.unqualified_identifier,
-        grammar.session_aspects,
         "is",
         Opt(List(grammar.declaration, sep=";"), ";"),
         "begin",

diff --git a/language/rflx_ast.py b/language/rflx_ast.py
@@ -145,13 +145,6 @@ class FormalDecl(RFLXNode):
     """Base class for generic formal session declarations."""
 
 
-class SessionAspects(RFLXNode):
-    """Session aspects (Initial, Final)."""
-
-    initial = Field(type=UnqualifiedID)
-    final = Field(type=UnqualifiedID)
-
-
 @abstract
 class LocalDecl(RFLXNode):
     """Base class for session or state local declarations."""
@@ -267,7 +260,7 @@ class Description(RFLXNode):
 class Transition(RFLXNode):
     """Unconditional session state transition."""
 
-    target = Field(type=UnqualifiedID)
+    target = Field(type=AbstractID)
     description = Field(type=Description)
 
 
@@ -300,7 +293,6 @@ class SessionDecl(Declaration):
 
     parameters = Field(type=FormalDecl.list)
     identifier = Field(type=UnqualifiedID)
-    aspects = Field(type=SessionAspects)
     declarations = Field(type=LocalDecl.list)
     states = Field(type=State.list)
     end_identifier = Field(type=UnqualifiedID)

diff --git a/tests/data/session/tls_handshake_session.rflx b/tests/data/session/tls_handshake_session.rflx
@@ -37,10 +37,7 @@ package TLS_Handshake_Session is
       with function Update_Hash (Context : Hash_Context; Data : Opaque) return Hash_Context;
       with function Validate_Certificate_Verify_Signature (Certificate_Message : TLS_Handshake::Certificate; Certificate_Verify_Message : TLS_Handshake::Certificate_Verify; Transcript_Hash : GreenTLS::Content) return GreenTLS::Signature_Validation_Result;
       with function Validate_Server_Certificate (Certificate_Message : TLS_Handshake::Certificate; Configuration : GreenTLS::Configuration; Connection : GreenTLS::Connection) return GreenTLS::Certificate_Validation_Result;
-   session Client with
-      Initial => START,
-      Final => TERMINATED
-   is
+   session Client is
       Application_Layer_Protocol_Negotiation_Received : Boolean := False;
       Binders : TLS_Handshake::PSK_Binder_Entries;
       Binders_Length : TLS_Handshake::Binders_Length;

diff --git a/tests/data/session/tls_record_session.rflx b/tests/data/session/tls_record_session.rflx
@@ -13,10 +13,7 @@ package TLS_Record_Session is
       Heartbeat_Data_Channel : Channel with Readable, Writable;
       with function Decrypt (Server_Key_Update_Message : GreenTLS::Key_Update_Message; Server_Sequence_Number : GreenTLS::Sequence_Number; Encrypted_Record : Opaque) return TLS_Record::TLS_Inner_Plaintext;
       with function Encrypt (Client_Key_Update_Message : GreenTLS::Key_Update_Message; Client_Sequence_Number : GreenTLS::Sequence_Number; Fragment : Opaque) return GreenTLS::Content;
-   session Client with
-      Initial => IDLE,
-      Final => TERMINATED
-   is
+   session Client is
       Alert_Message : TLS_Alert::Alert;
       Application_Control_Message : GreenTLS::Application_Control_Message;
       Ciphertext : GreenTLS::Content;

diff --git a/tests/grammar_test.py b/tests/grammar_test.py
@@ -3260,9 +3260,7 @@ def test_state(string: str, expected: Dict[str, str]) -> None:
                generic
                   X : Channel with Readable, Writable;
                   with function F return Boolean;
-               session Session with
-                  Initial => A,
-                  Final => B
+               session Session
                is
                   Y : Boolean := True;
                begin
@@ -3281,11 +3279,6 @@ def test_state(string: str, expected: Dict[str, str]) -> None:
          """,
             {
                 "_kind": "SessionDecl",
-                "aspects": {
-                    "_kind": "SessionAspects",
-                    "final": {"_kind": "UnqualifiedID", "_value": "B"},
-                    "initial": {"_kind": "UnqualifiedID", "_value": "A"},
-                },
                 "declarations": [
                     {
                         "_kind": "VariableDecl",

diff --git a/tests/parser_test.py b/tests/parser_test.py
@@ -345,10 +345,6 @@ def test_suffix_precedence() -> None:
             "{keyword} : Channel with Readable, Writable",
             librflxlang.GrammarRule.channel_declaration_rule,
         ),
-        (
-            "with Initial => {keyword}, Final => {keyword}",
-            librflxlang.GrammarRule.session_aspects_rule,
-        ),
         (
             "{keyword} : {keyword} renames {keyword}",
             librflxlang.GrammarRule.renaming_declaration_rule,
@@ -390,8 +386,7 @@ def test_suffix_precedence() -> None:
             librflxlang.GrammarRule.state_rule,
         ),
         (
-            "generic session {keyword} with "
-            "Initial => {keyword}, Final => {keyword} is begin end {keyword}",
+            "generic session {keyword} is begin end {keyword}",
             librflxlang.GrammarRule.session_declaration_rule,
         ),
         (