Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

compilation errors on simple session #770

Closed
kanigsson opened this issue Sep 15, 2021 · 5 comments · Fixed by #772
Closed

compilation errors on simple session #770

kanigsson opened this issue Sep 15, 2021 · 5 comments · Fixed by #772
Assignees
Labels
bug generator Related to generator package (SPARK code generation) model Related to model package (e.g., model verification)

Comments

@kanigsson
Copy link
Collaborator

chat.rflx.txt
server.rflx.txt

Running Recordflux on the attached files results in code that doesn't compile:

rflx-server-session.adb:31:79: error: "Message" is undefined (more references follow)
rflx-server-session.adb:33:45: error: expected private type "Only_Payload.Context" defined at rflx-server-only_payload.ads:51
rflx-server-session.adb:33:45: error: found private type "Chat_msg.Context" defined at rflx-chat-chat_msg.ads:51

As far as I can see, there are two problems:

  • reference to "Message" variable which doesn't exist
  • type error when building the "Outgoing" object.

Is there a workaround?

@treiher
Copy link
Collaborator

treiher commented Sep 15, 2021

Thanks for the report. There are several issues:

  1. This message specification is incorrect, but not detected by the model verification:
   type Only_Payload is
      message
         P : Opaque with Size => Message'Last;
   end message;

Message'Last must be replaced by Message'Size to get a valid message.

The missing detection of Message'Last will be solved in #627.

  1. A "payload only" message is not yet supported by the generator for protocol sessions. The fixed specification leads to:
rflx.error.FatalError: server.rflx:6:34: generator: error: unexpected Variable with undefined type in Size attribute

The issue will be obsolete after realizing #736, as Message'Size will not be allowed for this use case anymore.

  1. Using a parameterized message would be an option:
diff --git a/server.rflx b/server.rflx
index 7fcb473..6cf8dc7 100644
--- a/server.rflx
+++ b/server.rflx
@@ -1,9 +1,13 @@
 with Chat;
 package Server is
 
-   type Only_Payload is
+   type Payload_Size is mod 2**16;
+
+   type Only_Payload (Size : Payload_Size) is
       message
-         P : Opaque with Size => Message'Last;
+         P : Opaque
+            with Size => Size
+            if Size mod 8 = 0;
    end message;
 
    generic
@@ -19,7 +23,7 @@ package Server is
       state First is
       begin
         Channel'Read (Msg);
-        Outgoing := Only_Payload'(P => Msg.Payload);
+        Outgoing := Only_Payload'(Size => Msg'Size, P => Msg.Payload);
         Output'Write(Outgoing);
       transition
          then Last

But the code generated for the parameterized message is invalid:

   type Only_Payload (Size : Payload_Size) is
      message
         null
            then P
               if Size mod 8 = 0;
         P : Opaque with Size => Size;
   end message;
rflx-server-only_payload.adb:285:07: no candidate interpretations match the actuals:
rflx-server-only_payload.adb:285:07: missing argument for parameter "First" in call to "RESET" declared at rflx-server-only_payload.ads:127
rflx-server-only_payload.adb:285:07: missing argument for parameter "Size" in call to "RESET" declared at rflx-server-only_payload.ads:114
rflx-server-only_payload.adb:287:53: missing argument for parameter "Ctx" in call to "SIZE" declared at rflx-server-only_payload.ads:191

Will be fixed in #771.

  1. Another option would be adding a length field to Only_Payload (if that is acceptable for your use case).
diff --git a/server.rflx b/server.rflx
index 7fcb473..3c24b97 100644
--- a/server.rflx
+++ b/server.rflx
@@ -1,9 +1,14 @@
 with Chat;
 package Server is
 
+   type Payload_Size is mod 2**16;
+
    type Only_Payload is
       message
-         P : Opaque with Size => Message'Last;
+         Size : Payload_Size;
+         P : Opaque
+            with Size => Size
+            if Size mod 8 = 0;
    end message;
 
    generic
@@ -19,7 +24,7 @@ package Server is
       state First is
       begin
         Channel'Read (Msg);
-        Outgoing := Only_Payload'(P => Msg.Payload);
+        Outgoing := Only_Payload'(Size => Msg'Size, P => Msg.Payload);
         Output'Write(Outgoing);
       transition
          then Last

But Msg'Size leads to a "not yet supported error".

server.rflx:27:43: generator: error: Size with type universal integer (undefined) in message aggregate not yet supported

Will be solved in this issue.

  1. The error vanishes when Msg'Size is replaced by Msg'Size + 0, but there is another bug in the code generation for sessions:
rflx-server-session.adb:38:48: expected private type "Only_Payload.Context" defined at rflx-server-only_payload.ads:51
rflx-server-session.adb:38:48: found private type "Chat_msg.Context" defined at rflx-chat-chat_msg.ads:51

Will be solved in this issue.

Unfortunately, I don't see a simple workaround yet. Moving the data of an opaque field from one message to a message of another type seems to be broken (cf. 5; the wrong context type is used, the fix should be rather simple in the code generator). Using the same message type should work, but probably does not really fit to your example.

@treiher treiher added generator Related to generator package (SPARK code generation) model Related to model package (e.g., model verification) labels Sep 15, 2021
@senier
Copy link
Member

senier commented Sep 15, 2021

@treiher Feels like we should create anther 4-5 issues that address the underlying problems?

@treiher
Copy link
Collaborator

treiher commented Sep 15, 2021

@treiher Feels like we should create anther 4-5 issues that address the underlying problems?

I have added a note to each issue found in my previous comment to indicate in which ticket the particular issue is fixed.

@treiher
Copy link
Collaborator

treiher commented Sep 15, 2021

@kanigsson The issues (3), (4) and (5) are fixed on branch issue_771 and will be merged to main in #772. After applying the patch shown in (3) on your session specification, compiling the generated code should work. The specification should be semantically equivalent to your original one. In the future, parameterized messages will probably be the only way to specify "opaque only" messages because of the design decisions in #736.

@kanigsson
Copy link
Collaborator Author

Thanks, with your suggested patch (I modified it slightly to use a size in bytes instead of bits) and the changes on issue_771, the generated code compiles and I was able to complete my small example.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug generator Related to generator package (SPARK code generation) model Related to model package (e.g., model verification)
Projects
None yet
Development

Successfully merging a pull request may close this issue.

3 participants