simplify_exprt::simplify_bitwise is now independent of bitvector representation #3105
Conversation
kroening
commented
Oct 6, 2018
kroening
commented
- Each commit message has a non-empty body, explaining why the change was made.
- My contribution is formatted in line with CODING_STANDARD.md.
- Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
- 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.
kroening
requested review from
peterschrammel,
pkesseli,
smowton and
tautschnig
as code owners
kroening
force-pushed
the
hex-bitvectors6
branch
from
67e90f2 to
eb0a457
Compare
There was a problem hiding this comment.
I think a unit test that evaluates the performance differences is necessary to show that it does not have a negative impact. The code path modified here might not be as hot as #3106, but care must be taken. Taking apart mp_integers is very expensive. The fast path in binary2integer is in place for good reasons.
There was a problem hiding this comment.
Passed Diffblue compatibility checks (cbmc commit: eb0a457).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/87102947
kroening
force-pushed
the
hex-bitvectors6
branch
from
eb0a457 to
97bea15
Compare
|
Now with new approach that works on the representation directly! |
kroening
force-pushed
the
hex-bitvectors6
branch
3 times, most recently
from
272fd5c to
910b5f6
Compare
| /// perform a binary bit-wise operation, given as a functor, | ||
| /// on a bit-vector representation | ||
| /// \param f: the functor | ||
| irep_idt bitvector_bitwise_op( |
There was a problem hiding this comment.
Missing documentation of the other parameters, which trips up Doxygen.
src/util/arith_tools.h
Outdated
| const std::size_t width, | ||
| std::function<bool(bool, bool)>); | ||
|
|
||
| /// perform a unnary bit-wise operation, given as a functor, |
There was a problem hiding this comment.
Typo: s/unnary/unary/, but also this documentation should go with the definition, not the declaration.
src/util/arith_tools.cpp
Outdated
| for(std::size_t i = 0; i < width; i++) | ||
| { | ||
| const bool bit_a = a[i] == '1'; | ||
| const bool bit_b = b[i] == '1'; |
There was a problem hiding this comment.
Should this become get_bitvector_bit?
There was a problem hiding this comment.
Yes, can do once #3106 is merged.
kroening
force-pushed
the
hex-bitvectors6
branch
from
910b5f6 to
855b35e
Compare
There was a problem hiding this comment.
Passed Diffblue compatibility checks (cbmc commit: 855b35e).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/87130249
kroening
force-pushed
the
hex-bitvectors6
branch
from
855b35e to
2a5599a
Compare
kroening
force-pushed
the
hex-bitvectors6
branch
from
2a5599a to
3db8644
Compare
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: 2a5599a).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/87134978
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.
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).
There was a problem hiding this comment.
Passed Diffblue compatibility checks (cbmc commit: 3db8644).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/87139343
