Skip to content

Add short circuit evaluation to implies operator ==> #6401

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
thomasspriggs merged 3 commits into from
Oct 20, 2021
Merged

Add short circuit evaluation to implies operator ==> #6401

thomasspriggs merged 3 commits into from
Oct 20, 2021

Conversation

@thomasspriggs
Copy link
Contributor

@thomasspriggs thomasspriggs commented Oct 19, 2021

This PR adds short circuit evaluation to implies operator ==>, in response to #6319

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

@thomasspriggs
Add test of current handling of side effects in ==> operations
6d07357 
To ensure there are no regressions when adding short-circuiting
evaluation for the `==>` operator.
@thomasspriggs
Refactor if chain to make cases explicit
740976b 
Makes the code easier to read because it puts the values which we care
about into the code rather than the comment. As a bonus an UNREACHABLE
invariant will be violated if `expr.id()` value which we haven't
accounted for is encountered.
@thomasspriggs
Add short-circuit evaluation of implies operator
a55f5ae 
So that side effects of the right hand side are only evaluated in the
case where the left hand side is true. This allows for pointer checks to
be applied to assertions such as `assert(x != NULL ==> *x==2);` for
example.
@codecov
Copy link

codecov bot commented Oct 19, 2021

Codecov Report

Merging #6401 (a55f5ae) into develop (af94148) will increase coverage by 0.00%.
The diff coverage is 91.66%.

Impacted file tree graph

@@           Coverage Diff            @@
##           develop    #6401   +/-   ##
========================================
  Coverage    75.97%   75.97%           
========================================
  Files         1523     1523           
  Lines       164191   164201   +10     
========================================
+ Hits        124748   124758   +10     
  Misses       39443    39443
Impacted Files Coverage Δ
src/goto-programs/goto_clean_expr.cpp 99.03% <91.66%> (-0.46%) ⬇️
src/goto-analyzer/taint_analysis.cpp 78.21% <0.00%> (-0.22%) ⬇️
src/goto-instrument/dot.cpp 0.00% <0.00%> (ø)
src/goto-symex/symex_main.cpp 86.00% <0.00%> (+0.03%) ⬆️
src/goto-programs/remove_virtual_functions.cpp 92.85% <0.00%> (+0.04%) ⬆️
src/goto-instrument/goto_program2code.cpp 69.33% <0.00%> (+0.12%) ⬆️
src/goto-programs/goto_program.h 90.49% <0.00%> (+0.21%) ⬆️

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 7727f45...a55f5ae. Read the comment docs.

martin-cs
martin-cs reviewed Oct 19, 2021
View reviewed changes
Copy link
Collaborator

@martin-cs martin-cs left a comment

Choose a reason for hiding this comment

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

I appreciate that the issue that this addresses is labelled as urgent but I am a little concerned about changing the semantics of an existing operation; that feels like a non-trivial step. I am not sure if the ACSL ==> ( https://frama-c.com/html/acsl.html ) is short-cutting or not; that would give some argument one way or another.

@NlightNFotis this will have very significant consequences for #6399

@thomasspriggs
Copy link
Contributor Author

thomasspriggs commented Oct 19, 2021

I am not sure if the ACSL ==> ( https://frama-c.com/html/acsl.html ) is short-cutting or not; that would give some argument one way or another.

As I read the ACSL reference manual, it only supports pure expressions. See the first paragraph of section 2.2. If it does not allow side-effects then that would side step the issue of short circuiting or not, for usage of ACSL. Which doesn't really help us either way.

peterschrammel
peterschrammel approved these changes Oct 20, 2021
View reviewed changes
Copy link
Member

@peterschrammel peterschrammel left a comment

Choose a reason for hiding this comment

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

lgtm

@thomasspriggs thomasspriggs merged commit 49c9812 into diffblue:develop Oct 20, 2021
@thomasspriggs thomasspriggs deleted the tas/short_circuit_implies branch October 20, 2021 09:58
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@martin-cs martin-cs martin-cs left review comments

@peterschrammel peterschrammel peterschrammel approved these changes

@TGWDB TGWDB TGWDB approved these changes

@kroening kroening Awaiting requested review from kroening kroening is a code owner

@tautschnig tautschnig Awaiting requested review from tautschnig tautschnig is a code owner

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@thomasspriggs @peterschrammel @martin-cs @TGWDB