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

Refactoring contracts macro logic into separate modules #2992

Merged
merged 3 commits into from
Feb 6, 2024

Conversation

JustusAdam
Copy link
Contributor

Refactors the contracts module into several smaller modules grouped by task. The previous modules was very long and interleaved a lot of logic for various parts of the contracts state machine. This refactoring groups functions by specificity, task correlation and reusability.

All code changes here are exclusively moves with no changes to functionality.

The split is as follows:

  • mod.rs contains definitions of the data structures used to handle contracts, the entry point for contract handling, as well as a documentation overview.
  • bootstrap.rs is the logic that initialized the central data structures, such as the handler and the functions state
  • check.rs is all the logic required to create the function that checks a contract.
  • replace.rs is all the logic required to create a function that abstracts via contract
  • shared.rs are Kani/contract-specific helper functions that are used in more than one of bootstrap, check or replace
  • helpers.rs are Kani/contract-independent helper functions

I was going to make the old PR but I shudder at the though of appending more logic to the extremely long contracts.rs file so I figured I'd split the logic real quick before adding more.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

@JustusAdam JustusAdam requested a review from a team as a code owner February 5, 2024 17:58
@github-actions github-actions bot added the Z-BenchCI Tag a PR to run benchmark CI label Feb 5, 2024
Copy link
Contributor

@feliperodri feliperodri left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM.

Copy link
Contributor

@celinval celinval left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Awesome! This looks much cleaner. Thank you, @JustusAdam!

I'm assuming there was no change in the logic, just moving stuff around, right?

@JustusAdam
Copy link
Contributor Author

Yes. The only "code" that changed is that some functions are now "pub". Other than that there wasn't anything.

Does anyone know what's up with this release bundle failure?

@feliperodri
Copy link
Contributor

Does anyone know what's up with this release bundle failure?

I have no idea. @celinval do you have permission to re-trigger that job?

@feliperodri feliperodri merged commit 409a83d into model-checking:main Feb 6, 2024
20 checks passed
@JustusAdam JustusAdam deleted the refactoring-contracts branch February 6, 2024 18:37
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Z-BenchCI Tag a PR to run benchmark CI
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants