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

Better explanations and extra functionality in MutableBody #3382

Merged
merged 7 commits into from
Jul 25, 2024

Conversation

artemagvanian
Copy link
Contributor

MutableBody is the core data structure for MIR manipulation in instrumentation passes. However, its public methods have limited documentation and unclear semantics. This slowed down the development of instrumentation passes.

This PR aims to fix that by:

  • Clarifying how source instruction shifts when the methods are called;
  • Adding functionality for inserting basic blocks;
  • Expanding the support for different terminator types.

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

@artemagvanian artemagvanian marked this pull request as ready for review July 24, 2024 20:11
@artemagvanian artemagvanian requested a review from a team as a code owner July 24, 2024 20:11
@github-actions github-actions bot added the Z-BenchCI Tag a PR to run benchmark CI label Jul 24, 2024
@artemagvanian artemagvanian self-assigned this Jul 24, 2024
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.

It looks good. Thanks for improving documentation.

kani-compiler/src/kani_middle/transform/body.rs Outdated Show resolved Hide resolved
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.

Looks good. Thanks

@artemagvanian artemagvanian merged commit 114beea into model-checking:main Jul 25, 2024
25 checks passed
@artemagvanian artemagvanian deleted the mutable-body-ext branch July 25, 2024 17:14
tautschnig added a commit to tautschnig/kani that referenced this pull request Aug 5, 2024
* Remove `gen_function_local_variable` and `initializer_fn_name`, the
  last uses of both of which were removed in model-checking#3305.
* Remove `arg_count`, which was introduced in model-checking#3363, but not actually
  used.
* Remove `insert_bb`, which was introduced in model-checking#3382, but not actually
  used.

The toolchain upgrade to 2024-08-04 includes several bugfixes to
dead-code analysis in rustc, explaining why we the recent PRs as listed
above weren't flagged before for introducing dead code.

Resolves: model-checking#3411
github-merge-queue bot pushed a commit that referenced this pull request Aug 5, 2024
* Remove `gen_function_local_variable` and `initializer_fn_name`, the
last uses of both of which were removed in #3305.
* Mark `arg_count`, which was introduced in #3363, as `allow(dead_code)`
as it will soon be used.
* Mark `insert_bb`, which was introduced in #3382, as `allow(dead_code)`
as it will soon be used.

The toolchain upgrade to 2024-08-04 includes several bugfixes to
dead-code analysis in rustc, explaining why we the recent PRs as listed
above weren't flagged before for introducing dead code.

Resolves: #3411

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
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.

2 participants