bitreverse_exprt: Expression to reverse the order of bits

[tautschnig]

Clang has a __builtin_bitreverse (and at some point GCC might as well:
https://gcc.gnu.org/bugzilla/show_bug.cgi?id=50481).

Creating this as a draft: the actual implementation in the back-end is yet to be added, as are tests.

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

[codecov]

Codecov Report

Merging #6581 (57e7b2c) into develop (9d91abc) will increase coverage by 0.00%.
The diff coverage is 80.00%.

@@           Coverage Diff            @@
##           develop    #6581   +/-   ##
========================================
  Coverage    76.65%   76.65%           
========================================
  Files         1578     1579    +1     
  Lines       181219   181294   +75     
========================================
+ Hits        138907   138973   +66     
- Misses       42312    42321    +9     

Impacted Files	Coverage Δ
src/ansi-c/expr2c_class.h	100.00% <ø> (ø)
src/solvers/flattening/boolbv.h	62.50% <ø> (ø)
src/util/simplify_expr_class.h	90.47% <ø> (ø)
src/ansi-c/expr2c.cpp	65.78% <10.00%> (-0.27%)	⬇️
src/ansi-c/c_typecheck_expr.cpp	76.53% <71.42%> (-0.04%)	⬇️
src/solvers/flattening/boolbv_bitreverse.cpp	85.71% <85.71%> (ø)
src/util/simplify_expr_int.cpp	85.09% <92.85%> (+0.22%)	⬆️
src/solvers/flattening/boolbv.cpp	80.50% <100.00%> (+0.11%)	⬆️
src/solvers/smt2/smt2_conv.cpp	67.57% <100.00%> (+0.05%)	⬆️
src/util/bitvector_expr.cpp	94.59% <100.00%> (+0.65%)	⬆️
... and 6 more

---

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 23306ee...57e7b2c. Read the comment docs.

[chrisr-diffblue]

Generally looks great to me. Given the effort that went into removing unstructure exceptions in the error reporting previously, it seems a shame to be adding a throw 0 back in here - so could I kindly ask if that could be replaced with a structured exception? It'd be an approval from me if that were done :-)

[chrisr-diffblue]

Throw a structured exception?

Suggested change

	error().source_location = f_op.source_location();
	error() << identifier << " expects one operand" << eom;
	throw 0;
	std::ostringstream error_message;
	error_message << expr.source_location().as_string() << ": " << identifier
	<< " expects expects one operand";
	throw invalid_source_file_exceptiont{error_message.str()};

[tautschnig]

Done, but I really wish we had #5837 (with its two dependencies) in place to make things even more structured!

[tautschnig]

And now also includes a test for this one :-)

[chrisr-diffblue]

Many thanks for the updates - looks great to me... And given that I poked a raw nerve on the structured exception point - feel free to assign any PRs that need reviews/comments on that front to me. 👍