Prohibit appending independently created message

Ref. #514
AdaCore · Dec 7, 2020 · 1ef3242 · 1ef3242
1 parent 6f38469
commit 1ef3242
Show file tree

Hide file tree

Showing 3 changed files with 68 additions and 38 deletions.
diff --git a/rflx/statement.py b/rflx/statement.py
@@ -3,7 +3,7 @@
 
 import rflx.typing_ as rty
 from rflx.common import Base
-from rflx.error import Location, RecordFluxError
+from rflx.error import Location, RecordFluxError, Severity, Subsystem
 from rflx.expression import Expr, Variable
 from rflx.identifier import ID, StrID
 
@@ -86,6 +86,21 @@ def check_type(
         )
         if isinstance(statement_type, rty.Array):
             error += self.parameters[0].check_type(statement_type.element)
+            if isinstance(statement_type.element, rty.Message) and isinstance(
+                self.parameters[0], Variable
+            ):
+                error.append(
+                    "appending independently created message not supported",
+                    Subsystem.MODEL,
+                    Severity.ERROR,
+                    self.parameters[0].location,
+                )
+                error.append(
+                    "message aggregate should be used instead",
+                    Subsystem.MODEL,
+                    Severity.INFO,
+                    self.parameters[0].location,
+                )
         return error
 
 

diff --git a/tests/integration/session/tls_handshake_session.rflx b/tests/integration/session/tls_handshake_session.rflx
@@ -148,11 +148,9 @@ package TLS_Handshake_Session is
 
       state CREATE_CLIENT_HELLO_EXTENSIONS is
          Supported_Version : TLS_Handshake::Supported_Version;
-         Supported_Versions_Extension : TLS_Handshake::CH_Extension;
       begin
          Supported_Version := TLS_Handshake::Supported_Version'(Version => TLS_Handshake::TLS_1_3);
-         Supported_Versions_Extension := TLS_Handshake::CH_Extension'(Tag => TLS_Handshake::EXTENSION_SUPPORTED_VERSIONS, Data_Length => Supported_Version'Size, Data => Supported_Version'Opaque);
-         Extensions_List'Append (Supported_Versions_Extension);
+         Extensions_List'Append (TLS_Handshake::CH_Extension'(Tag => TLS_Handshake::EXTENSION_SUPPORTED_VERSIONS, Data_Length => Supported_Version'Size, Data => Supported_Version'Opaque));
          Extensions_List'Extend (Create_Client_Hello_Extensions (Configuration));
       transition
          then ERROR_INTERNAL_ERROR
@@ -167,10 +165,8 @@ package TLS_Handshake_Session is
       end CREATE_CLIENT_HELLO_EXTENSIONS;
 
       state START_POST_HANDSHAKE_AUTH_EXTENSION is
-         Post_Handshake_Auth_Extension : TLS_Handshake::CH_Extension;
       begin
-         Post_Handshake_Auth_Extension := TLS_Handshake::CH_Extension'(Tag => TLS_Handshake::EXTENSION_POST_HANDSHAKE_AUTH, Data_Length => 0, Data => []);
-         Extensions_List'Append (Post_Handshake_Auth_Extension);
+         Extensions_List'Append (TLS_Handshake::CH_Extension'(Tag => TLS_Handshake::EXTENSION_POST_HANDSHAKE_AUTH, Data_Length => 0, Data => []));
       transition
          then ERROR_INTERNAL_ERROR
             if Extensions_List'Valid = False
@@ -182,19 +178,13 @@ package TLS_Handshake_Session is
       end START_POST_HANDSHAKE_AUTH_EXTENSION;
 
       state START_DHE is
-         Supported_Groups_Extension : TLS_Handshake::CH_Extension;
-         Key_Share_Extension : TLS_Handshake::CH_Extension;
-         Signature_Algorithms_Extension : TLS_Handshake::CH_Extension;
-      begin
-         Supported_Groups_Extension := TLS_Handshake::CH_Extension'(Tag => TLS_Handshake::EXTENSION_SUPPORTED_GROUPS, Data_Length => Modes'Size, Data => Modes)
-            where Modes = TLS_Handshake::Supported_Groups'(Length => Configuration.Supported_Groups_Length, Groups => Configuration.Supported_Groups_Groups);
-         Extensions_List'Append (Supported_Groups_Extension);
-         Key_Share_Extension := TLS_Handshake::CH_Extension'(Tag => TLS_Handshake::EXTENSION_KEY_SHARE, Data_Length => Modes'Size, Data => Modes)
-            where Modes = TLS_Handshake::Key_Share_CH'(Length => Configuration.Key_Shares_Length, Shares => Configuration.Key_Shares_Shares);
-         Extensions_List'Append (Key_Share_Extension);
-         Signature_Algorithms_Extension := TLS_Handshake::CH_Extension'(Tag => TLS_Handshake::EXTENSION_SIGNATURE_ALGORITHMS, Data_Length => Modes'Size, Data => Modes)
-            where Modes = TLS_Handshake::Signature_Algorithms'(Length => Configuration.Signature_Algorithms_Length, Algorithms => Configuration.Signature_Algorithms_Algorithms);
-         Extensions_List'Append (Signature_Algorithms_Extension);
+      begin
+         Extensions_List'Append (TLS_Handshake::CH_Extension'(Tag => TLS_Handshake::EXTENSION_SUPPORTED_GROUPS, Data_Length => Modes'Size, Data => Modes)
+            where Modes = TLS_Handshake::Supported_Groups'(Length => Configuration.Supported_Groups_Length, Groups => Configuration.Supported_Groups_Groups));
+         Extensions_List'Append (TLS_Handshake::CH_Extension'(Tag => TLS_Handshake::EXTENSION_KEY_SHARE, Data_Length => Modes'Size, Data => Modes)
+            where Modes = TLS_Handshake::Key_Share_CH'(Length => Configuration.Key_Shares_Length, Shares => Configuration.Key_Shares_Shares));
+         Extensions_List'Append (TLS_Handshake::CH_Extension'(Tag => TLS_Handshake::EXTENSION_SIGNATURE_ALGORITHMS, Data_Length => Modes'Size, Data => Modes)
+            where Modes = TLS_Handshake::Signature_Algorithms'(Length => Configuration.Signature_Algorithms_Length, Algorithms => Configuration.Signature_Algorithms_Algorithms));
       transition
          then ERROR_INTERNAL_ERROR
             if Extensions_List'Valid = False
@@ -207,11 +197,9 @@ package TLS_Handshake_Session is
       end START_DHE;
 
       state START_DHE_SIGNATURE_ALGORITHMS is
-         Signature_Algorithms_Cert_Extension : TLS_Handshake::CH_Extension;
       begin
-         Signature_Algorithms_Cert_Extension := TLS_Handshake::CH_Extension'(Tag => TLS_Handshake::EXTENSION_SIGNATURE_ALGORITHMS_CERT, Data_Length => Modes'Size, Data => Modes)
-            where Modes = TLS_Handshake::Signature_Algorithms_Cert'(Length => Configuration.Signature_Algorithms_Cert_Length, Algorithms => Configuration.Signature_Algorithms_Cert_Algorithms);
-         Extensions_List'Append (Signature_Algorithms_Cert_Extension);
+         Extensions_List'Append (TLS_Handshake::CH_Extension'(Tag => TLS_Handshake::EXTENSION_SIGNATURE_ALGORITHMS_CERT, Data_Length => Modes'Size, Data => Modes)
+            where Modes = TLS_Handshake::Signature_Algorithms_Cert'(Length => Configuration.Signature_Algorithms_Cert_Length, Algorithms => Configuration.Signature_Algorithms_Cert_Algorithms));
       transition
          then ERROR_INTERNAL_ERROR
             if Extensions_List'Valid = False
@@ -261,12 +249,10 @@ package TLS_Handshake_Session is
       end START_GET_RANDOM;
 
       state START_PSK_EXTENSIONS is
-         PSK_Key_Exchange_Modes_Extension : TLS_Handshake::CH_Extension;
          Client_Hello_Hash : Hash_Context;
       begin
-         PSK_Key_Exchange_Modes_Extension := TLS_Handshake::CH_Extension'(Tag => TLS_Handshake::EXTENSION_PSK_KEY_EXCHANGE_MODES, Data_Length => Modes'Size, Data => Modes)
-            where Modes = TLS_Handshake::PSK_Key_Exchange_Modes'(Length => Configuration.PSK_Key_Exchange_Modes_Length, Modes => Configuration.PSK_Key_Exchange_Modes_Modes);
-         Extensions_List'Append (PSK_Key_Exchange_Modes_Extension);
+         Extensions_List'Append (TLS_Handshake::CH_Extension'(Tag => TLS_Handshake::EXTENSION_PSK_KEY_EXCHANGE_MODES, Data_Length => Modes'Size, Data => Modes)
+            where Modes = TLS_Handshake::PSK_Key_Exchange_Modes'(Length => Configuration.PSK_Key_Exchange_Modes_Length, Modes => Configuration.PSK_Key_Exchange_Modes_Modes));
          Extensions_List'Append (TLS_Handshake::CH_Extension'(Tag => TLS_Handshake::EXTENSION_PRE_SHARED_KEY, Data_Length => Pre_Shared_Key_CH'Size, Data => Pre_Shared_Key_CH));
          Client_Hello_Handshake_Message := TLS_Handshake::Handshake'(Tag => TLS_Handshake::HANDSHAKE_CLIENT_HELLO, Length => CH'Size, Payload => CH)
             where CH = TLS_Handshake::Client_Hello'(Legacy_Version => TLS_Handshake::TLS_1_2, Random => Random_Message.Data, Legacy_Session_ID_Length => 0, Legacy_Session_ID => [], Cipher_Suites_Length => Configuration.Cipher_Suites'Size, Cipher_Suites => Configuration.Cipher_Suites, Legacy_Compression_Methods_Length => 0, Legacy_Compression_Methods => [], Extensions_Length => Extensions_List'Size, Extensions => Extensions_List);
@@ -539,12 +525,10 @@ package TLS_Handshake_Session is
       end WAIT_SH_PSK_EXTENSION_CHECK;
 
       state WAIT_SH_PSK_EXTENSIONS is
-         PSK_Key_Exchange_Modes_Extension : TLS_Handshake::CH_Extension;
          Client_Hello_Hash : Hash_Context;
       begin
-         PSK_Key_Exchange_Modes_Extension := TLS_Handshake::CH_Extension'(Tag => TLS_Handshake::EXTENSION_PSK_KEY_EXCHANGE_MODES, Data_Length => Modes'Size, Data => Modes)
-            where Modes = TLS_Handshake::PSK_Key_Exchange_Modes'(Length => Configuration.PSK_Key_Exchange_Modes_Length, Modes => Configuration.PSK_Key_Exchange_Modes_Modes);
-         Extensions_List'Append (PSK_Key_Exchange_Modes_Extension);
+         Extensions_List'Append (TLS_Handshake::CH_Extension'(Tag => TLS_Handshake::EXTENSION_PSK_KEY_EXCHANGE_MODES, Data_Length => Modes'Size, Data => Modes)
+            where Modes = TLS_Handshake::PSK_Key_Exchange_Modes'(Length => Configuration.PSK_Key_Exchange_Modes_Length, Modes => Configuration.PSK_Key_Exchange_Modes_Modes));
          Extensions_List'Append (TLS_Handshake::CH_Extension'(Tag => TLS_Handshake::EXTENSION_PRE_SHARED_KEY, Data_Length => Pre_Shared_Key_CH'Size, Data => Pre_Shared_Key_CH));
          Client_Hello_Handshake_Message := TLS_Handshake::Handshake'(Tag => TLS_Handshake::HANDSHAKE_CLIENT_HELLO, Length => CH'Size, Payload => CH)
             where CH = TLS_Handshake::Client_Hello'(Legacy_Version => TLS_Handshake::TLS_1_2, Random => Random_Message.Data, Legacy_Session_ID_Length => 0, Legacy_Session_ID => [], Cipher_Suites_Length => Configuration.Cipher_Suites'Size, Cipher_Suites => Configuration.Cipher_Suites, Legacy_Compression_Methods_Length => 0, Legacy_Compression_Methods => [], Extensions_Length => Extensions_List'Size, Extensions => Extensions_List);

diff --git a/tests/unit/model/session_test.py b/tests/unit/model/session_test.py
@@ -1381,16 +1381,21 @@ def test_append() -> None:
                 "Start",
                 transitions=[Transition(target=ID("End"))],
                 declarations=[],
-                actions=[stmt.Append("List", expr.Variable("Element"))],
+                actions=[
+                    stmt.Append(
+                        "List",
+                        expr.MessageAggregate(
+                            "TLV::Message",
+                            {"Tag": expr.Variable("TLV::Msg_Error")},
+                        ),
+                    )
+                ],
             ),
             State("End"),
         ],
-        declarations=[
-            decl.VariableDeclaration("List", "TLV::Messages"),
-            decl.VariableDeclaration("Element", "TLV::Message"),
-        ],
+        declarations=[decl.VariableDeclaration("List", "TLV::Messages")],
         parameters=[],
-        types=[BOOLEAN, TLV_MESSAGE, TLV_MESSAGES],
+        types=[TLV_TAG, TLV_MESSAGE, TLV_MESSAGES],
     )
 
 
@@ -1417,6 +1422,32 @@ def test_append_incompatible() -> None:
     )
 
 
+def test_append_message_unsupported() -> None:
+    assert_session_model_error(
+        states=[
+            State(
+                "Start",
+                transitions=[Transition(target=ID("End"))],
+                declarations=[],
+                actions=[
+                    stmt.Append("List", expr.Variable("Element", location=Location((10, 20))))
+                ],
+            ),
+            State("End"),
+        ],
+        declarations=[
+            decl.VariableDeclaration("List", "TLV::Messages"),
+            decl.VariableDeclaration("Element", "TLV::Message"),
+        ],
+        parameters=[],
+        types=[TLV_MESSAGE, TLV_MESSAGES],
+        regex=(
+            r"^<stdin>:10:20: model: error: appending independently created message not supported\n"
+            r"<stdin>:10:20: model: info: message aggregate should be used instead$"
+        ),
+    )
+
+
 def test_extend() -> None:
     Session(
         identifier="P::S",