added instructiont::set_X #4205
Conversation
kroening
commented
Feb 16, 2019
kroening
commented
- 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).
- 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.
kroening
requested review from
chrisr-diffblue,
danpoe,
hannes-steffenhagen-diffblue,
martin-cs,
peterschrammel,
pkesseli,
smowton,
tautschnig and
thk123
as code owners
kroening
force-pushed
the
get_set_instructiont_code
branch
from
afde693 to
f74d5a3
Compare
kroening
requested review from
cesaro,
cristina-david and
NathanJPhillips
as code owners
kroening
force-pushed
the
get_set_instructiont_code
branch
from
f74d5a3 to
cec23bf
Compare
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: cec23bf).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/101189026
| @@ -1046,13 +1046,13 @@ void string_abstractiont::move_lhs_arithmetic(exprt &lhs, exprt &rhs) | |||
|
|
|||
| goto_programt::targett string_abstractiont::abstract_pointer_assign( | |||
| goto_programt &dest, | |||
| goto_programt::targett target) | |||
| const goto_programt::targett target) | |||
There was a problem hiding this comment.
Shouldn't this rather be goto_programt::const_targett target - adding the const to an object passed by value doesn't add much (other than forbidding the operator++ application below)?
kroening
force-pushed
the
get_set_instructiont_code
branch
from
cec23bf to
27d96c5
Compare
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: 27d96c5).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/101217016
src/analyses/constant_propagator.cpp
Outdated
| constant_propagator_domaint::partial_evaluate(d.values, arg, ns); | ||
| } | ||
|
|
||
| it->set_function_call(call); |
There was a problem hiding this comment.
This one could also be made conditional, though it requires an additional Boolean to track whether any modification took place.
There was a problem hiding this comment.
I did contemplate it, and arrived at the conclusion that the "set" is likely cheaper than the Boolean logic.
There was a problem hiding this comment.
The set_function_call might be cheap, but the problem with breaking sharing is that you pay the price multiple times: every time the expression is stored in a std::unordered_set or std::unordered_map the operator== becomes more expensive, because pointer-comparison cannot be used. There is of course a question whether this expression is shared, but it quite possibly is if the function has multiple call sites. Destroying sharing will thus make writing the simplified goto binary more expensive.
There was a problem hiding this comment.
ok, now with boolean logic
kroening
force-pushed
the
get_set_instructiont_code
branch
from
27d96c5 to
331c449
Compare
This avoids accidental disruption of sharing.
kroening
force-pushed
the
get_set_instructiont_code
branch
from
331c449 to
e70816e
Compare
