Skip to content

Simplify goto-program generated for short-circuit operators #7051

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 2 commits into from
Aug 17, 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.
  • 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.
  • n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

@codecov
Copy link

codecov bot commented Aug 1, 2022

Codecov Report

Merging #7051 (318ddb3) into develop (438aad3) will decrease coverage by 0.02%.
The diff coverage is 100.00%.

❗ Current head 318ddb3 differs from pull request most recent head 1570e0a. Consider uploading reports for the commit 1570e0a to get more accurate results

@@             Coverage Diff             @@
##           develop    #7051      +/-   ##
===========================================
- Coverage    77.88%   77.86%   -0.03%     
===========================================
  Files         1569     1569              
  Lines       180989   180996       +7     
===========================================
- Hits        140962   140924      -38     
- Misses       40027    40072      +45     
Impacted Files Coverage Δ
src/goto-programs/goto_clean_expr.cpp 99.02% <100.00%> (-0.50%) ⬇️
src/goto-programs/goto_convert_class.h 88.15% <100.00%> (+0.32%) ⬆️
src/goto-programs/goto_convert_side_effect.cpp 94.47% <100.00%> (-0.67%) ⬇️
src/goto-programs/goto_convert.cpp 88.12% <0.00%> (-4.22%) ⬇️
src/solvers/flattening/boolbv_quantifier.cpp 89.91% <0.00%> (-3.37%) ⬇️
src/ansi-c/goto_check_c.cpp 91.65% <0.00%> (+0.09%) ⬆️

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

This introduces goto_convertt::assignment_lhs_needs_temporary, to be used
instead of needs_cleaning when determining whether to introduce a temporary
for the value of an assignment expression, compound assignment expression,
or pre- or post-increment or decrement operator.

This allows weakening the condition computed by needs_cleaning.
Both dereference and index expressions are no longer lifted out of
expressions using temporaries during conversion into the goto program.
@kroening kroening marked this pull request as ready for review August 3, 2022 13:37
Copy link
Collaborator

@jimgrundy jimgrundy left a comment

Choose a reason for hiding this comment

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

Looks like there are three places where we used to replace an index/dereference with a temporary and now we don't. It would make it all much clearer for me if you could give a small code snippet example of each of the three cases.

@kroening kroening merged commit acb58e7 into develop Aug 17, 2022
@kroening kroening deleted the shortcircuit2 branch August 17, 2022 16:40
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants