Disable redundant automatic checks on assigns clause checking instrumentation [depends-on: #6450] #6455
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR depends on PRs:
This PR fixes some performance issues with assigns clause checking for function and loop contracts.
The problem was that the goto variables and instructions generated to instrument the checks were themselves re-instrumented with automatic VCCs in subsequent passes, causing an explosion in the number of VCCs (with unwanted VCCs representing up to 85% of the total VCCs in some problems).
Instructions performing CAR inclusion checks are read-only logical expressions whose evaluation cannot fail so we can safely disable automatic checks on them.
CAR snapshotting instructions however perform some pointer arithmetic and need to be ultimately checked for pointer overflow.
In this PR:
The disable pragmas guard against reinstrumentation in later passes, and the enable pragmas make sure necessary checks will eventually be instantiated before analysis.