Skip to content

Check subset relationship of assigns clause during replacement #6345

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 4 commits into from
Sep 17, 2021

Conversation

feliperodri
Copy link
Collaborator

If CBMC replaces a function bar() with its contract, while enforcing the contract in function foo(), it must also check whether the bar()'s assigns clause is a subset of the foo()'s assigns clause.

  • 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 Sep 15, 2021
@feliperodri feliperodri self-assigned this Sep 15, 2021
@feliperodri feliperodri force-pushed the fix-contract-replacement branch from 289c957 to cd5fef0 Compare September 15, 2021 23:49
@codecov
Copy link

codecov bot commented Sep 16, 2021

Codecov Report

Merging #6345 (bb4c90b) into develop (e4ee1ed) will increase coverage by 0.00%.
The diff coverage is 100.00%.

Impacted file tree graph

@@           Coverage Diff            @@
##           develop    #6345   +/-   ##
========================================
  Coverage    75.90%   75.90%           
========================================
  Files         1515     1515           
  Lines       163990   164005   +15     
========================================
+ Hits        124469   124484   +15     
  Misses       39521    39521           
Impacted Files Coverage Δ
src/ansi-c/ansi_c_convert_type.cpp 79.28% <100.00%> (+0.04%) ⬆️
src/goto-instrument/contracts/assigns.cpp 96.66% <100.00%> (ø)
src/goto-instrument/contracts/contracts.cpp 94.01% <100.00%> (+0.14%) ⬆️

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 4fd1a8d...bb4c90b. Read the comment docs.

@feliperodri feliperodri force-pushed the fix-contract-replacement branch from cd5fef0 to 5e8852b Compare September 16, 2021 17:15
@feliperodri feliperodri marked this pull request as ready for review September 16, 2021 17:18
@feliperodri feliperodri force-pushed the fix-contract-replacement branch from 5e8852b to b623a0b Compare September 16, 2021 17:23
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.

LTGM! Thanks 😄

Not a blocker, but I think we could make helper functions for generating containment and subset assertions. We have repeated code blocks for generating those

@@ -7,7 +7,7 @@ main.c
\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS
\[bar.\d+\] line \d+ Check that z is assignable: SUCCESS
\[foo.\d+\] line \d+ Check that \*x is assignable: SUCCESS
\[foo.\d+\] line \d+ Check that callee's assigns clause is a subset of caller's: SUCCESS
\[foo.\d+\] line \d+ Check that bar\'s assigns clause is a subset of foo\'s assigns clause: SUCCESS
Copy link
Contributor

Choose a reason for hiding this comment

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

Nice! 🎉

@@ -272,6 +272,7 @@ void ansi_c_convert_typet::read_rec(const typet &type)
for(auto &assignment : to_unary_expr(as_expr).op().operands())
assigns.add_to_operands(std::move(assignment));
}
assigns.add_source_location() = as_expr.source_location();
Copy link
Contributor

Choose a reason for hiding this comment

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

Nice! 🎉

@feliperodri feliperodri merged commit 4e38322 into diffblue:develop Sep 17, 2021
@feliperodri feliperodri deleted the fix-contract-replacement branch September 17, 2021 21:31
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 bugfix Code Contracts Function and loop contracts
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants