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

Optimize messages if only fields are used #1114

Closed
Tracked by #908
jklmnn opened this issue Jul 22, 2022 · 4 comments · Fixed by #1149
Closed
Tracked by #908

Optimize messages if only fields are used #1114

jklmnn opened this issue Jul 22, 2022 · 4 comments · Fixed by #1149
Assignees
Labels
generator Related to generator package (SPARK code generation) model Related to model package (e.g., model verification)

Comments

@jklmnn
Copy link
Member

jklmnn commented Jul 22, 2022

Sometimes message have to be returned from platform functions in session, e.g. to get an opaque value to to group multiple values. These messages are never used in another message, as a sequence element or as an opaque value:

type Blob is message
   Length : Length;
   Data : Opaque with
      Size => Length * 8;
end message;

generic
   with function Get_Blob return Blob;
session Session
...
is
begin
   state Add_Blob
   is
      Blob : Blob;
   begin
      Blob := Get_Blob;
      Message.Data_Length := Blob.Length;
      Message.Data := Blob.Data;
   end Add_Blob;
end Session;

The generated code for blob includes the returned structure that already contains the data buffer and the length field, both with the appropriate types. Now that structure is transformed into a context as it is a proper message. Since only fields of Blob are accessed only getters of that context are called. These getters simply return the same values the structure already contained.
The optimization is to remove the context creation in that case and directly use the structure. This allows to save a significant amount of memory, code size and execution time.
This optimization cannot be done when the specific properties of a real message are required:

  • Calling 'Opaque.
  • Appending it to a sequence.
@jklmnn jklmnn added generator Related to generator package (SPARK code generation) model Related to model package (e.g., model verification) labels Jul 22, 2022
@jklmnn jklmnn self-assigned this Jul 22, 2022
@senier
Copy link
Member

senier commented Jul 22, 2022

@jklmnn I guess your intention was to call the external function at some point in your example? Also, did you mean to call it Get_Blob?

@jklmnn
Copy link
Member Author

jklmnn commented Jul 22, 2022

You're right. I fixed that.

@treiher
Copy link
Collaborator

treiher commented Jul 25, 2022

This optimization cannot be done when the specific properties of a real message are required:

What about setting of message fields? I think it shouldn't be needed for the use case. If we still would want to support it, we would have to ensure that no message conditions get violated.

I suppose we only want to support state-local variables. Otherwise, we also have to consider 'Read and 'Write.

@jklmnn
Copy link
Member Author

jklmnn commented Jul 25, 2022

I think the setting of message fields doesn't need to be supported for this optimization. The usual use case are types that are returned by platform functions.

jklmnn added a commit that referenced this issue Aug 2, 2022
jklmnn added a commit that referenced this issue Aug 3, 2022
jklmnn added a commit that referenced this issue Aug 3, 2022
jklmnn added a commit that referenced this issue Aug 16, 2022
jklmnn added a commit that referenced this issue Aug 16, 2022
jklmnn added a commit that referenced this issue Aug 16, 2022
jklmnn added a commit that referenced this issue Aug 18, 2022
jklmnn added a commit that referenced this issue Aug 19, 2022
jklmnn added a commit that referenced this issue Aug 19, 2022
jklmnn added a commit that referenced this issue Aug 22, 2022
jklmnn added a commit that referenced this issue Aug 22, 2022
jklmnn added a commit that referenced this issue Aug 22, 2022
jklmnn added a commit that referenced this issue Aug 22, 2022
jklmnn added a commit that referenced this issue Aug 22, 2022
jklmnn added a commit that referenced this issue Aug 22, 2022
jklmnn added a commit that referenced this issue Aug 23, 2022
jklmnn added a commit that referenced this issue Aug 23, 2022
jklmnn added a commit that referenced this issue Aug 23, 2022
jklmnn added a commit that referenced this issue Aug 23, 2022
jklmnn added a commit that referenced this issue Aug 23, 2022
jklmnn added a commit that referenced this issue Aug 23, 2022
jklmnn added a commit that referenced this issue Aug 23, 2022
jklmnn added a commit that referenced this issue Aug 23, 2022
jklmnn added a commit that referenced this issue Aug 25, 2022
jklmnn added a commit that referenced this issue Aug 30, 2022
jklmnn added a commit that referenced this issue Aug 30, 2022
jklmnn added a commit that referenced this issue Aug 30, 2022
jklmnn added a commit that referenced this issue Aug 30, 2022
jklmnn added a commit that referenced this issue Aug 30, 2022
jklmnn added a commit that referenced this issue Aug 30, 2022
jklmnn added a commit that referenced this issue Aug 30, 2022
jklmnn added a commit that referenced this issue Aug 30, 2022
jklmnn added a commit that referenced this issue Aug 31, 2022
jklmnn added a commit that referenced this issue Aug 31, 2022
jklmnn added a commit that referenced this issue Aug 31, 2022
jklmnn added a commit that referenced this issue Aug 31, 2022
jklmnn added a commit that referenced this issue Aug 31, 2022
jklmnn added a commit that referenced this issue Aug 31, 2022
jklmnn added a commit that referenced this issue Aug 31, 2022
jklmnn added a commit that referenced this issue Aug 31, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
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