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

Prevent unnecessary checks in session states #1131

Open
treiher opened this issue Aug 9, 2022 · 1 comment
Open

Prevent unnecessary checks in session states #1131

treiher opened this issue Aug 9, 2022 · 1 comment
Labels
architectural decision Discussion of design decision generator Related to generator package (SPARK code generation)

Comments

@treiher
Copy link
Collaborator

treiher commented Aug 9, 2022

Context and Problem Statement

Some error handling in the generated session code is unnecessary and could be removed. We currently do not detect such issues because proof warnings are disabled (#670). There is currently not enough information in the code generator to decide whether a property is already established or requires verification.

Use Cases

Removing the unnecessary code will improve the efficiency and binary size of the generated code (#908).

Considered Options

O1 Consider contracts of statements and states

  • The pre- and post-conditions are determined for each statement.
  • The necessity of a check is inferred based on the pre-conditions of the statement and the current facts.
  • The facts are established by the post-conditions of all previous statements and the pre-conditions of the state.
  • The post-condition of a state is equivalent to the established facts after the last statement of the state.
  • The pre-condition of a state is a disjunction, where each disjunct is a conjunction of the post-condition and transition condition of all possible predecessor states (exception transitions will not be considered).

Decision Outcome

O1

@treiher treiher added bug generator Related to generator package (SPARK code generation) labels Aug 9, 2022
@treiher treiher self-assigned this Aug 12, 2022
treiher added a commit that referenced this issue Aug 18, 2022
treiher added a commit that referenced this issue Aug 18, 2022
treiher added a commit that referenced this issue Aug 18, 2022
treiher added a commit that referenced this issue Aug 18, 2022
treiher added a commit that referenced this issue Aug 18, 2022
@treiher
Copy link
Collaborator Author

treiher commented Aug 18, 2022

There are several checks, where SPARK is able to show that these checks are unnecessary. The code generator does not yet contain the necessary information to come to the same conclusion. This will probably change with the work for #691.

treiher added a commit that referenced this issue Aug 19, 2022
treiher added a commit that referenced this issue Aug 19, 2022
treiher added a commit that referenced this issue Aug 19, 2022
treiher added a commit that referenced this issue Aug 19, 2022
treiher added a commit that referenced this issue Aug 19, 2022
treiher added a commit that referenced this issue Aug 19, 2022
treiher added a commit that referenced this issue Aug 19, 2022
treiher added a commit that referenced this issue Aug 19, 2022
treiher added a commit that referenced this issue Aug 19, 2022
@treiher treiher changed the title Unreachable error handling code in session states Prevent unnecessary checks in session states Aug 22, 2022
@treiher treiher added architectural decision Discussion of design decision and removed bug labels Aug 22, 2022
treiher added a commit that referenced this issue Aug 22, 2022
treiher added a commit that referenced this issue Aug 22, 2022
treiher added a commit that referenced this issue Aug 22, 2022
treiher added a commit that referenced this issue Aug 22, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
architectural decision Discussion of design decision generator Related to generator package (SPARK code generation)
Projects
None yet
Development

No branches or pull requests

1 participant