Cleanup expression/code cast validation #4176
Conversation
tautschnig
requested review from
cesaro,
chrisr-diffblue,
cristina-david,
kroening,
martin-cs,
NathanJPhillips,
peterschrammel,
pkesseli,
smowton and
thk123
as code owners
tautschnig
force-pushed
the
make-cast-const
branch
from
0563f78 to
b044a20
Compare
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: 0563f78).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/100773027
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: b044a20).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/100788846
tautschnig
force-pushed
the
make-cast-const
branch
from
b044a20 to
b2f1dbd
Compare
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: b2f1dbd).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/103118539
Status will be re-evaluated on next push.
Common spurious failures:
-
the cbmc commit has disappeared in the mean time (e.g. in a force-push)
-
the author is not in the list of contributors (e.g. first-time contributors).
-
the compatibility was already broken by an earlier merge.
| @@ -354,6 +354,11 @@ inline bool can_cast_expr<unary_exprt>(const exprt &base) | |||
| return base.operands().size() == 1; | |||
| } | |||
|
|
|||
| inline void validate_expr(const unary_exprt &value) | |||
There was a problem hiding this comment.
⛏️ commit message: unnecessariliy -> unnecessarily
There was a problem hiding this comment.
⛏️ some commit messages are too long
There was a problem hiding this comment.
Both done and automated spell checking enabled in my editor...
This is consistent with what validate_expr and to_code_declt assert at the moment.
The error message would fail to print as it uses a conversion that is invalid for the very reason that the error message wants to print.
Adds one implementation of validate_expr, and moves the other existing ones to replace the comment that claims there is no implementation.
Prefer code re-use over duplicated (and possibly inconsistent) implementations.
This provides two advantages: 1) Member access such as testing the number of operands does not break sharing, because it is done in a const context. 2) Code re-use: we no longer implement the same check in two different ways. All changes in this commit were applied automatically via text replacement.
Placing them above to_*_expr is the layout that std_code.h uses. Furthermore it will facilitate re-use of validate_expr. No code changes, just text motion.
This provides two advantages:
1) Member access such as testing the number of operands does not break
sharing, because it is done in a const context.
2) Code re-use: we no longer implement the same check in two different
ways.
With the exception of {exist,forall,quantifier}_exprt, all changes in
this commit were applied automatically via text replacement. For
quantifiers, additional checks were inserted (use of can_cast_expr,
validate_expr uses quantifier_exprt's validate_expr).
Placing them above to_*_expr is the layout that std_code.h uses. Furthermore it will facilitate re-use of validate_expr. No code changes, just text motion.
Some were unnecessarily missing, others were wrongly commented out.
Commented-out checks obviously don't check anything, and the code that was commented out wasn't particularly deep so that restoring it in future is trivial anyway.
This provides two advantages: 1) Member access such as testing the number of operands does not break sharing, because it is done in a const context. 2) Code re-use: we no longer implement the same check in two different ways. All changes in this commit were applied automatically via text replacement.
Prefer code re-use over duplicated (and possibly inconsistent) implementations.
tautschnig
force-pushed
the
make-cast-const
branch
from
b2f1dbd to
d4dc77f
Compare
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: d4dc77f).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/103461000
Please review commit-by-commit; several commits are text-motion only and others are automated text replacement - both indicated in the respective commit messages.
This requires/includes #4175 ("Return statements always have one operand"), so please skip that while reviewing.The original aim was to get rid of all the sharing-breaking side effects in
to_*exprtprocedures, but when starting on this I noticed that really a lot more cleanup was indicated.