Skip to content

Disable redundant automatic checks on assigns clause checking instrumentation [depends-on: #6450] #6455

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

Conversation

remi-delmas-3000
Copy link
Collaborator

@remi-delmas-3000 remi-delmas-3000 commented Nov 12, 2021

This PR depends on PRs:

  • #6450 (allows to enable checks at the instruction level)

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:

  • we disable all pointer checks on CAR inclusion checking instructions
  • we enable pointer overflow checks on CAR snapshot instructions

The disable pragmas guard against reinstrumentation in later passes, and the enable pragmas make sure necessary checks will eventually be instantiated before analysis.

  • Each commit message has a non-empty body, explaining why the change was made.
  • Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
  • The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
  • Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
  • My commit message includes data points confirming performance improvements (if claimed).
  • My PR is restricted to a single feature or bugfix.
  • White-space or formatting changes outside the feature-related changed lines are in commits of their own.

- Readable names for instrumentation variables
- Use pointer offsets in CAR bounds checking instead of whole pointers
- Disable pointer, pointer-overflow and pointer-primitive checks on CAR inclusion checks
- Enable pointer-overflow checks on CAR upperbound computation
@remi-delmas-3000 remi-delmas-3000 force-pushed the assigns-clause-checking-disable-pointer-checks branch from 9ecd485 to 3701933 Compare November 12, 2021 03:28
@codecov
Copy link

codecov bot commented Nov 12, 2021

Codecov Report

Merging #6455 (fd0f094) into develop (a229942) will increase coverage by 0.01%.
The diff coverage is 91.93%.

❗ Current head fd0f094 differs from pull request most recent head 50765b2. Consider uploading reports for the commit 50765b2 to get more accurate results
Impacted file tree graph

@@             Coverage Diff             @@
##           develop    #6455      +/-   ##
===========================================
+ Coverage    76.01%   76.02%   +0.01%     
===========================================
  Files         1527     1527              
  Lines       164465   164565     +100     
===========================================
+ Hits        125013   125109      +96     
- Misses       39452    39456       +4     
Impacted Files Coverage Δ
jbmc/src/janalyzer/janalyzer_parse_options.cpp 48.25% <ø> (ø)
jbmc/src/jbmc/jbmc_parse_options.cpp 72.32% <ø> (ø)
src/goto-instrument/contracts/assigns.h 100.00% <ø> (ø)
src/goto-instrument/contracts/contracts.h 100.00% <ø> (ø)
src/goto-instrument/contracts/utils.h 100.00% <ø> (ø)
src/analyses/goto_check.cpp 88.43% <73.07%> (-0.36%) ⬇️
src/ansi-c/scanner.l 61.94% <92.30%> (+0.18%) ⬆️
src/ansi-c/ansi_c_parser.cpp 88.88% <92.53%> (+2.30%) ⬆️
jbmc/src/jdiff/jdiff_parse_options.cpp 68.11% <100.00%> (ø)
src/ansi-c/ansi_c_parser.h 100.00% <100.00%> (ø)
... and 9 more

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update d0e6b9a...50765b2. Read the comment docs.

@remi-delmas-3000 remi-delmas-3000 force-pushed the assigns-clause-checking-disable-pointer-checks branch from fd0f094 to 50765b2 Compare November 15, 2021 14:25
@SaswatPadhi SaswatPadhi changed the title Disable redundant automatic checks on assigns clause checking instrumentation Disable redundant automatic checks on assigns clause checking instrumentation [depends-on: #6450] Nov 16, 2021
@remi-delmas-3000
Copy link
Collaborator Author

closing this one, creating a new cleaned-up PR #6459

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
aws Bugs or features of importance to AWS CBMC users aws-high Code Contracts Function and loop contracts dependent - do not merge
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants