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.

Sign up for GitHub

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

Jump to bottom

Proofs of Reset_Dependent_Fields too slow #840

Closed
kanigsson opened this issue Nov 8, 2021 · 0 comments · Fixed by #842
Closed

Proofs of Reset_Dependent_Fields too slow #840

kanigsson opened this issue Nov 8, 2021 · 0 comments · Fixed by #842
Assignees
@kanigsson
Labels
bug generator Related to generator package (SPARK code generation)
Projects
RecordFlux 0.6

Comments

@kanigsson
Copy link
Collaborator

As @jklmnn observed on #767, proofs of the Reset_Dependent_Fields procedure still dominate the running time of gnatprove (on SPDM at least), and eat up a lot of memory. I will try to improve that on this ticket.

My current idea is to replace the large case statement by a loop over all record fields, similar to what I did in the postcondition of the procedure.
@kanigsson kanigsson added the bug label Nov 8, 2021
@kanigsson kanigsson self-assigned this Nov 8, 2021
@kanigsson kanigsson added this to To do in RecordFlux 0.6 via automation Nov 8, 2021
@kanigsson kanigsson moved this from To do to In progress in RecordFlux 0.6 Nov 8, 2021
@kanigsson kanigsson added the generator Related to generator package (SPARK code generation) label Nov 8, 2021
kanigsson added a commit that referenced this issue Nov 9, 2021
@kanigsson
Improve code generation for Reset_Dependent_Fields
daf64fc 
Use a loop rather than case statement + explicit assignments to
reset the fields.

Closes #840
kanigsson added a commit that referenced this issue Nov 9, 2021
@kanigsson
Improve code generation for Reset_Dependent_Fields
602386a 
Use a loop rather than case statement + explicit assignments to
reset the fields.

Closes #840
kanigsson added a commit that referenced this issue Nov 10, 2021
@kanigsson
Improve code generation for Reset_Dependent_Fields
d5d10fe 
Use a loop rather than case statement + explicit assignments to
reset the fields.

Closes #840
@kanigsson kanigsson mentioned this issue Nov 10, 2021
Merged
@kanigsson kanigsson moved this from In progress to Under review in RecordFlux 0.6 Nov 10, 2021
RecordFlux 0.6 automation moved this from Under review to Merged Nov 10, 2021
kanigsson added a commit that referenced this issue Nov 10, 2021
@kanigsson
Improve code generation for Reset_Dependent_Fields
5c3aad4 
Use a loop rather than case statement + explicit assignments to
reset the fields.

Closes #840
@kanigsson kanigsson mentioned this issue Nov 10, 2021
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@kanigsson kanigsson

Labels
bug generator Related to generator package (SPARK code generation)
Projects
No open projects
RecordFlux 0.6
  
Done
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Improve code generation for Reset_Dependent_Fields AdaCore/RecordFlux
1 participant
@kanigsson