Skip to content

replace_symbolt with bindings #6827

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 3 commits into from
Apr 25, 2022
Merged

replace_symbolt with bindings #6827

merged 3 commits into from
Apr 25, 2022

Conversation

kroening
Copy link
Member

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

tautschnig
tautschnig approved these changes Apr 24, 2022
View reviewed changes
Copy link
Collaborator

@tautschnig tautschnig 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!! Would it make sense to explicitly document this behaviour in replace_symbol.h?

@tautschnig
Copy link
Collaborator

I believe the failing tests just document that we aren't really using bindings the way they are supposed to work, but instead introduce symbols for quantified expressions in the front-end.

@kroening
Copy link
Member Author

The failures focus on the contracts code, which I don't think I can fix.

May I suggest merging the variant in #6807 to unblock.

@tautschnig
Copy link
Collaborator

The failures focus on the contracts code, which I don't think I can fix.

May I suggest merging the variant in #6807 to unblock.

I'll create a patch for add_quantified_variable in the contracts code that will remove the use of replace_symbol in that context.

tautschnig added a commit to tautschnig/cbmc that referenced this pull request Apr 24, 2022
@tautschnig
CONTRACTS: do not rely on replace_symbol for bound variables
ed4b77f 
replace_symbolt will cease to support bound variables, which presently
is not well documented behaviour. See diffblue#6827 for upcoming changes.
@tautschnig tautschnig mentioned this pull request Apr 24, 2022
Merged
3 tasks
@tautschnig
Copy link
Collaborator

I'll create a patch for add_quantified_variable in the contracts code that will remove the use of replace_symbol in that context.

Done in #6828.

kroening added a commit that referenced this pull request Apr 25, 2022
@kroening
Merge pull request #6828 from tautschnig/cleanup/contracts-use-instan…
ba7ad3d 
…tiate

CONTRACTS: do not rely on replace_symbol for bound variables [blocks: #6827]
kroening added 3 commits April 25, 2022 07:59
@kroening
add non-const to_binding_expr
333e700 
This adds a non-const variant of to_binding_expr.
@kroening
add array_comprehension case to to_binding_expr
f21971d 
As identified in #6810, to_binding_expr could also cover array_comprehension
expressions.
@kroening
replace_symbolt now knows bindings
e46d2f3 
This makes replace_symbolt aware of bound symbols, which may hide the
symbols that are being replaced.
@kroening kroening force-pushed the replace_symbol_with_bindings branch from 71434a7 to e46d2f3 Compare April 25, 2022 07:10
@kroening
Copy link
Member Author

Done in #6828.

Many thanks -- note my comment there. It may be possible to simplify that code further.

@kroening kroening marked this pull request as ready for review April 25, 2022 08:04
@codecov
Copy link

codecov bot commented Apr 25, 2022

Codecov Report

Merging #6827 (e46d2f3) into develop (ed4b77f) will increase coverage by 0.00%.
The diff coverage is 92.85%.

@@           Coverage Diff            @@
##           develop    #6827   +/-   ##
========================================
  Coverage    77.01%   77.01%           
========================================
  Files         1594     1594           
  Lines       184415   184436   +21     
========================================
+ Hits        142019   142038   +19     
- Misses       42396    42398    +2
Impacted Files Coverage Δ
src/util/replace_symbol.h 100.00% <ø> (ø)
src/util/replace_symbol.cpp 88.29% <91.30%> (+0.34%) ⬆️
src/util/std_expr.h 93.18% <100.00%> (ø)

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 ba7ad3d...e46d2f3. Read the comment docs.

@kroening kroening merged commit c2e1cb6 into develop Apr 25, 2022
@kroening kroening deleted the replace_symbol_with_bindings branch April 25, 2022 08:25
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@tautschnig tautschnig tautschnig approved these changes

@peterschrammel peterschrammel peterschrammel approved these changes

Assignees

@tautschnig tautschnig

@kroening kroening

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@kroening @tautschnig @peterschrammel