Skip to content

New flag for only processing loop contracts #6184

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

Merged
merged 1 commit into from
Jun 22, 2021

Conversation

SaswatPadhi
Copy link
Contributor

@SaswatPadhi SaswatPadhi commented Jun 16, 2021

Created a new flag, --apply-loop-contracts, to be able to separately process loop and function contracts.

The --enforce-contract foo flag would only enforce function contracts on foo now. The previous behavior of enforcing both function and loop contracts can be achieved by --apply-loop-contracts --enforce-contract foo.

  • Each commit message has a non-empty body, explaining why the change was made.
  • n/a 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).
  • n/a My commit message includes data points confirming performance improvements (if claimed).
  • My PR is restricted to a single feature or bugfix.
  • n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

@SaswatPadhi SaswatPadhi added aws Bugs or features of importance to AWS CBMC users Code Contracts Function and loop contracts labels Jun 16, 2021
@SaswatPadhi SaswatPadhi requested a review from feliperodri June 16, 2021 23:36
@SaswatPadhi SaswatPadhi self-assigned this Jun 16, 2021
@SaswatPadhi SaswatPadhi force-pushed the loop_contracts_flag branch from 73a33a3 to 5f2f7e9 Compare June 16, 2021 23:39
@codecov
Copy link

codecov bot commented Jun 17, 2021

Codecov Report

Merging #6184 (9cdca48) into develop (0002950) will increase coverage by 7.73%.
The diff coverage is n/a.

Impacted file tree graph

@@             Coverage Diff             @@
##           develop    #6184      +/-   ##
===========================================
+ Coverage    67.40%   75.14%   +7.73%     
===========================================
  Files         1157     1456     +299     
  Lines        95236   161132   +65896     
===========================================
+ Hits         64197   121081   +56884     
- Misses       31039    40051    +9012     
Flag Coverage Δ
cproversmt2 ?
regression ?
unit ?

Flags with carried forward coverage won't be shown. Click here to find out more.

Impacted Files Coverage Δ
src/util/mathematical_expr.cpp 50.00% <0.00%> (-50.00%) ⬇️
src/util/string_container.cpp 52.94% <0.00%> (-47.06%) ⬇️
src/solvers/prop/prop.cpp 42.85% <0.00%> (-41.76%) ⬇️
src/solvers/flattening/boolbv_member.cpp 53.65% <0.00%> (-38.65%) ⬇️
src/cpp/cpp_storage_spec.cpp 65.00% <0.00%> (-35.00%) ⬇️
src/util/cmdline.h 66.66% <0.00%> (-33.34%) ⬇️
src/solvers/strings/array_pool.h 66.66% <0.00%> (-33.34%) ⬇️
src/solvers/strings/string_refinement.h 66.66% <0.00%> (-33.34%) ⬇️
...rs/strings/string_concatenation_builtin_function.h 0.00% <0.00%> (-33.34%) ⬇️
src/cbmc/c_test_input_generator.cpp 60.00% <0.00%> (-30.33%) ⬇️
... and 1435 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 f9be0eb...9cdca48. Read the comment docs.

Copy link
Collaborator

@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.

Thanks!

@@ -1,6 +1,6 @@
CORE
CORE smt-backend
Copy link
Collaborator

Choose a reason for hiding this comment

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

Can it work with both back-ends or it was spuriously passing?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

This test works correctly either way, we explicitly provide --z3 in the next line.

I added the tag because on systems that don't have z3 installed and that only run SAT-specific tests, this test should be ignored. Also see #6181.

Currently test tags are not respected within regression/contract. I have reported this already @ #5986 (comment). When that's fixed, this test would be automatically ignored in SAT-only mode.

Copy link
Collaborator

@martin-cs martin-cs left a comment

Choose a reason for hiding this comment

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

Approve although it might be good if you could think about the comments.

Added `--apply-loop-contracts` to check and use loop contracts
(invariants and variants) independent of function contracts.
@SaswatPadhi SaswatPadhi force-pushed the loop_contracts_flag branch from 5f2f7e9 to 9cdca48 Compare June 22, 2021 17:37
@SaswatPadhi SaswatPadhi merged commit b31f952 into diffblue:develop Jun 22, 2021
@SaswatPadhi SaswatPadhi deleted the loop_contracts_flag branch June 22, 2021 22:38
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 Code Contracts Function and loop contracts
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants