Skip to content

Refactor assigns clause implementation #6334

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 3 commits into from
Sep 11, 2021

Conversation

SaswatPadhi
Copy link
Contributor

@SaswatPadhi SaswatPadhi commented Sep 8, 2021

I was planning to merge these changes as part of #6249, but given the volume of changes, I thought it would be best to create a separate PR.

Main changes are:

  • bug fixes in containment (previously called alias) and subset (previously called subset) checks
  • usused fields (e.g., function_id, init_block) are removed,
  • redundant functions (e.g. pointer_for) are removed,
  • const references are used throughout consistently
  • targets are tracked in an unordered_set as opposed to vector
  • introduced a "normalize" method for extracting base object of arrays
  • 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.
  • n/a 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.

@SaswatPadhi SaswatPadhi added aws Bugs or features of importance to AWS CBMC users aws-high Code Contracts Function and loop contracts labels Sep 8, 2021
@SaswatPadhi SaswatPadhi self-assigned this Sep 8, 2021
@SaswatPadhi SaswatPadhi force-pushed the assigns-cleanup branch 2 times, most recently from e6678b5 to 2859f9f Compare September 8, 2021 22:29
@SaswatPadhi SaswatPadhi marked this pull request as draft September 9, 2021 00:13
@SaswatPadhi
Copy link
Contributor Author

Marked draft for now.

assigns_enforce_16 is failing but I cannot reproduce the failure locally!

@SaswatPadhi
Copy link
Contributor Author

SaswatPadhi commented Sep 9, 2021

Marked draft for now.

assigns_enforce_16 is failing but I cannot reproduce the failure locally!

Fixed this by removing dead variables from freely assignable set all together (although the implementation is still incorrect and, as discussed offline, @feliperodri would make a separate PR to fix that properly).

But, what's concerning here is that goto-cc / goto-instrument was generating different goto binaries on my machine vs CI.

EDIT: The remaining CI issues with Windows tests seem completely unrelated.

@SaswatPadhi SaswatPadhi marked this pull request as ready for review September 9, 2021 19:17
@jimgrundy
Copy link
Collaborator

I realize I'm late here and that the coding practices for this code base are established ... but I would want to see more comments in the code. While particularly valuable for a new comer like myself, a header comment per method stating what it does, and maybe also per method argument/result, would help a great deal. I imagine one day being able to run doxygen on the code and learning something useful from it.

@codecov
Copy link

codecov bot commented Sep 9, 2021

Codecov Report

Merging #6334 (e1e7235) into develop (aeba3f0) will decrease coverage by 0.00%.
The diff coverage is 96.20%.

Impacted file tree graph

@@             Coverage Diff             @@
##           develop    #6334      +/-   ##
===========================================
- Coverage    75.89%   75.89%   -0.01%     
===========================================
  Files         1515     1515              
  Lines       163972   163969       -3     
===========================================
- Hits        124444   124440       -4     
- Misses       39528    39529       +1     
Impacted Files Coverage Δ
src/goto-instrument/contracts/contracts.cpp 92.37% <85.71%> (+0.04%) ⬆️
src/goto-instrument/contracts/assigns.cpp 97.40% <98.30%> (-0.38%) ⬇️
src/goto-instrument/contracts/assigns.h 100.00% <100.00%> (ø)
src/goto-programs/goto_program.h 89.30% <0.00%> (-0.20%) ⬇️

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 38d945a...e1e7235. Read the comment docs.

@SaswatPadhi SaswatPadhi force-pushed the assigns-cleanup branch 5 times, most recently from b50690e to e414eb0 Compare September 9, 2021 21:19
+ usused fields (e.g., `function_id`, `init_block`) are removed,
+ redundant functions (e.g. `pointer_for`) are removed,
+ const references are used throughout consistently
+ targets are tracked in an `unordered_set` as opposed to `vector`
+ introduced a "normalize" method for extracting base object of arrays
+ API renamed for clarity
@SaswatPadhi SaswatPadhi marked this pull request as draft September 10, 2021 20:35
@SaswatPadhi
Copy link
Contributor Author

Will push a few more things before final review & merge, so marked as draft.

@SaswatPadhi SaswatPadhi force-pushed the assigns-cleanup branch 2 times, most recently from 39a3440 to 00ebb97 Compare September 10, 2021 21:34
@SaswatPadhi SaswatPadhi marked this pull request as ready for review September 10, 2021 21:35
@SaswatPadhi SaswatPadhi force-pushed the assigns-cleanup branch 4 times, most recently from 7204528 to b74afd5 Compare September 11, 2021 00:51
assigns_clauset was calling `compatible_expression` (not
`alias_expression`) on each target, and was thus only comparing the
object IDs (not offsets and sizes).
We fix this by removing `compatible_expression` entirely and calling
`alias_expression` for each from assigns_clauset.
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.

Thank you for all the subsequent clean up and fixes!

@feliperodri feliperodri merged commit d0eee83 into diffblue:develop Sep 11, 2021
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
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants