Skip to content

Avoid crashing when applying trivial contracts #6255

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.

Sign up for GitHub

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

Jump to bottom
Merged
feliperodri merged 6 commits into from
Jul 28, 2021
Merged

Avoid crashing when applying trivial contracts #6255

feliperodri merged 6 commits into from
Jul 28, 2021

Conversation

@feliperodri
Copy link
Collaborator

@feliperodri feliperodri commented Jul 27, 2021

Resolves #5950.
Resolves #5941.

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

@feliperodri feliperodri added bugfix aws Bugs or features of importance to AWS CBMC users Code Contracts Function and loop contracts labels Jul 27, 2021
@feliperodri feliperodri requested a review from SaswatPadhi as a code owner July 27, 2021 04:25
@feliperodri feliperodri self-assigned this Jul 27, 2021
@feliperodri feliperodri requested a review from tautschnig as a code owner July 27, 2021 04:25
@feliperodri feliperodri force-pushed the do-not-bail-trivial-contracts branch from 3a43e18 to 505fbb0 Compare July 27, 2021 04:29
@codecov
Copy link

codecov bot commented Jul 27, 2021 •
edited
Loading

Codecov Report

Merging #6255 (0397819) into develop (3493061) will decrease coverage by 0.00%.
The diff coverage is 90.24%.

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

@@             Coverage Diff             @@
##           develop    #6255      +/-   ##
===========================================
- Coverage    76.16%   76.16%   -0.01%     
===========================================
  Files         1484     1484              
  Lines       162173   162164       -9     
===========================================
- Hits        123525   123516       -9     
  Misses       38648    38648
Impacted Files Coverage Δ
src/goto-instrument/contracts/assigns.cpp 92.36% <ø> (ø)
src/goto-instrument/contracts/contracts.h 100.00% <ø> (ø)
...rc/goto-instrument/contracts/memory_predicates.cpp 83.81% <ø> (-0.19%) ⬇️
src/goto-instrument/contracts/contracts.cpp 91.83% <90.24%> (-0.10%) ⬇️

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 c5871d7...2c32f86. Read the comment docs.

martin-cs
martin-cs approved these changes Jul 27, 2021
View reviewed changes
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.

Yes but in future please can the commit messages and the code be a little closer. For some of the refactorings, it is not clear why you are doing them.

@feliperodri feliperodri force-pushed the do-not-bail-trivial-contracts branch from 505fbb0 to 84e8ced Compare July 27, 2021 19:19
SaswatPadhi
SaswatPadhi approved these changes Jul 27, 2021
View reviewed changes
Copy link
Contributor

@SaswatPadhi SaswatPadhi left a comment

Choose a reason for hiding this comment

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

LGTM, with couple of minor comments:

@feliperodri
Removes get_namespace() from contracts module
0c4574f 
Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
@feliperodri
Consistent order of parameters across contracts functions
552beee 
Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
@feliperodri
Avoid crashing when applying trivial contracts
61ea8ed 
Requires and ensures are currently treated as conjunctions,
thus empty clauses are mapped to true. This commit also
prevents that trivials `assert(true)` are injected into functions.

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
@feliperodri
Removes unimplemented method from code_contractst
3a1b249 
Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
@feliperodri
Improves description of code_contractst methods
a0646ec 
Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
@feliperodri
Fixes typos across contracts manual
2c32f86 
Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
@feliperodri feliperodri force-pushed the do-not-bail-trivial-contracts branch from 0397819 to 2c32f86 Compare July 28, 2021 04:23
@feliperodri feliperodri merged commit b158d86 into diffblue:develop Jul 28, 2021
@feliperodri feliperodri deleted the do-not-bail-trivial-contracts branch July 28, 2021 05:14
SaswatPadhi
SaswatPadhi reviewed Jul 28, 2021
View reviewed changes
doc/cprover-manual/contracts-assigns.md
clause. Since these objects might be modified by the function, CBMC uses
non-deterministic assignments to havoc them and restrict their values only by
assuming the postconditions.
assuming the postconditions (i.e., requires clauses).
Copy link
Contributor

@SaswatPadhi SaswatPadhi Jul 28, 2021

Choose a reason for hiding this comment

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

Thanks for fixing the docs! So many tiny errors (including errors in code examples) went unnoticed the last time!

Just one small issues: I think you meant "ensures" (not "requires") clauses in this sentence.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@martin-cs martin-cs martin-cs approved these changes

@tautschnig tautschnig Awaiting requested review from tautschnig tautschnig is a code owner

+1 more reviewer

@SaswatPadhi SaswatPadhi SaswatPadhi approved these changes

Reviewers whose approvals may not affect merge requirements

Assignees

@feliperodri feliperodri

Labels

aws Bugs or features of importance to AWS CBMC users bugfix Code Contracts Function and loop contracts

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

Remove all get_namespace from code_contracts Consistent order of parameters across the various instrument_* functions in code_contracts.*

3 participants

@feliperodri @SaswatPadhi @martin-cs