Skip to content

CONTRACTS: Insert reachability canary assertions #7359

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
merged 1 commit into from
Nov 29, 2022
Merged

CONTRACTS: Insert reachability canary assertions #7359

merged 1 commit into from
Nov 29, 2022

Conversation

remi-delmas-3000
Copy link
Collaborator

When a GOTO function has no body, insert a canary assertion to make sure the function is indeed unreachable.

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

@remi-delmas-3000 remi-delmas-3000 self-assigned this Nov 17, 2022
@remi-delmas-3000 remi-delmas-3000 added aws Bugs or features of importance to AWS CBMC users aws-high Code Contracts Function and loop contracts labels Nov 17, 2022
@remi-delmas-3000 remi-delmas-3000 force-pushed the assert-unreachable-when-body-unavailable branch 3 times, most recently from 7afe64f to 2e89f66 Compare November 17, 2022 23:23
@remi-delmas-3000 remi-delmas-3000 force-pushed the assert-unreachable-when-body-unavailable branch from 2e89f66 to fa89b4f Compare November 18, 2022 13:32
tautschnig
tautschnig reviewed Nov 18, 2022
View reviewed changes
@codecov
Copy link

codecov bot commented Nov 18, 2022 •
edited
Loading

Codecov Report

Base: 78.37% // Head: 78.36% // Decreases project coverage by -0.00% ⚠️

Coverage data is based on head (99eec8d) compared to base (941030e).
Patch coverage: 83.92% of modified lines in pull request are covered.

Additional details and impacted files 
@@             Coverage Diff             @@
##           develop    #7359      +/-   ##
===========================================
- Coverage    78.37%   78.36%   -0.01%     
===========================================
  Files         1647     1647              
  Lines       190328   190356      +28     
===========================================
+ Hits        149172   149180       +8     
- Misses       41156    41176      +20
Impacted Files Coverage Δ
src/analyses/constant_propagator.h 82.35% <ø> (ø)
src/ansi-c/expr2c.cpp 67.24% <ø> (ø)
src/goto-instrument/havoc_loops.cpp 0.00% <0.00%> (ø)
src/util/pointer_predicates.cpp 95.12% <ø> (+2.39%) ⬆️
src/util/pointer_predicates.h 100.00% <ø> (ø)
src/util/simplify_expr.cpp 85.36% <ø> (+0.04%) ⬆️
src/util/simplify_expr_class.h 90.47% <ø> (ø)
src/util/simplify_expr_pointer.cpp 86.58% <ø> (+0.75%) ⬆️
src/util/expr_util.cpp 84.44% <50.00%> (-5.30%) ⬇️
src/analyses/constant_propagator.cpp 95.46% <88.88%> (ø)
... and 21 more

Help us with your feedback. Take ten seconds to tell us how you rate us. Have a feature suggestion? Share it here.

☔ View full report at Codecov.
📢 Do you have feedback about the report comment? Let us know in this issue.

@remi-delmas-3000 remi-delmas-3000 force-pushed the assert-unreachable-when-body-unavailable branch 2 times, most recently from 581ebb6 to 7f60794 Compare November 23, 2022 20:16
jimgrundy
jimgrundy reviewed Nov 25, 2022
View reviewed changes
tautschnig
tautschnig reviewed Nov 25, 2022
View reviewed changes
feliperodri
feliperodri requested changes Nov 25, 2022
View reviewed changes
@diffblue diffblue deleted a comment from tautschnig Nov 25, 2022
@feliperodri feliperodri changed the title CONTRACTS: insert reachability canary assertions CONTRACTS: Insert reachability canary assertions Nov 28, 2022
@remi-delmas-3000 remi-delmas-3000 force-pushed the assert-unreachable-when-body-unavailable branch from 7f60794 to 749cebb Compare November 28, 2022 19:09
feliperodri
feliperodri approved these changes Nov 28, 2022
View reviewed changes
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.

LGTM.

@tautschnig
Copy link
Collaborator

tautschnig commented Nov 28, 2022 •
edited
Loading

The test failure is unrelated, and instead caused by #7331 having been merged (which I had failed to rebase on top of the various simplification PRs that have meanwhile been merged). I'll issue a PR to fix this. Edit: #7396 now takes care of this.

tautschnig
tautschnig reviewed Nov 28, 2022
View reviewed changes
src/goto-instrument/contracts/dynamic-frames/dfcc_library.h Outdated
@@ -233,14 +233,14 @@ class dfcc_libraryt
/// \param contract_assigns_size_hint size of the assigns clause being checked
void specialize(const std::size_t contract_assigns_size_hint);

/// Adds an ASSERT(false) body to all front-end functions
/// Adds an ASSERT(false);ASSUME(false); body to all front-end functions
Copy link
Collaborator

Choose a reason for hiding this comment

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

Is this change to the comment accurate?

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

argh, no

@remi-delmas-3000 remi-delmas-3000 force-pushed the assert-unreachable-when-body-unavailable branch 2 times, most recently from 905167f to e782174 Compare November 28, 2022 21:14
CONTRACTS: insert reachability canary asssertions
99eec8d 
When a GOTO function has no body, insert a canary assertion
to make the analysis fail in case the function is reachable.

Add `assert(false)` bodies for front-end functions
`__CPROVER_assignable`, `__CPROVER_object_whole`,
`__CPROVER_object_from`, `__CPROVER_object_upto`
to make the analysis fail when they are used
outside of contract clauses and are hence not
remapped to their library implementation.
@remi-delmas-3000 remi-delmas-3000 force-pushed the assert-unreachable-when-body-unavailable branch from e782174 to 99eec8d Compare November 28, 2022 22:00
@tautschnig tautschnig merged commit 4267df2 into diffblue:develop Nov 29, 2022
This was referenced Dec 5, 2022
Closed
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@tautschnig tautschnig tautschnig left review comments

@feliperodri feliperodri feliperodri approved these changes

@jimgrundy jimgrundy jimgrundy approved these changes

@kroening kroening Awaiting requested review from kroening

@peterschrammel peterschrammel Awaiting requested review from peterschrammel

@chris-ryder chris-ryder Awaiting requested review from chris-ryder

Assignees

@remi-delmas-3000 remi-delmas-3000

Labels
aws Bugs or features of importance to AWS CBMC users aws-high Code Contracts Function and loop contracts
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
4 participants
@remi-delmas-3000 @tautschnig @feliperodri @jimgrundy