Lower-byte-operators: bv_to_expr should support bool target type

[tautschnig]

When byte updating or byte extracting structs that contain single-bit __CPROVER_bool members (as is used in __CPROVER_contracts_car_t) we may need to turn a bv typed single-bit extractbits expression into one that has bool (__CPROVER_bool) type.

Fixes: #8303

• Each commit message has a non-empty body, explaining why the change was made.
• n/a 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

Attention: Patch coverage is 75.00000% with 1 line in your changes missing coverage. Please review.

Project coverage is 78.05%. Comparing base (37511f3) to head (7118b73).

Files	Patch %	Lines
src/util/lower_byte_operators.cpp	75.00%	1 Missing ⚠️

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #8318      +/-   ##
===========================================
- Coverage    78.13%   78.05%   -0.09%     
===========================================
  Files         1722     1722              
  Lines       188886   189096     +210     
  Branches     18421    18420       -1     
===========================================
+ Hits        147588   147592       +4     
- Misses       41298    41504     +206     

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

[kroening]

I am not sure I like the idea of pointer accesses into __CPROVER_bool.

[kroening]

It's not meant to be used as an alternative to bit-fields. Think of it as a mathematical type, with no memory layout.

[rod-chapman]

Re-running my little test case, cbmc no longer crashes, but does not terminate:

cbmc --verbosity 6 --bounds-check --pointer-check --memory-cleanup-check --div-by-zero-check --signed-overflow-check --unsigned-overflow-check --pointer-overflow-check --conversion-check --undefined-shift-check --enum-range-check --pointer-primitive-check --smt2 ar_contracts.goto
CBMC version 6.0.0-preview (cbmc-6.0.0-alpha-420-g8c229d75e4) 64-bit arm64 macos
Reading GOTO program from file ar_contracts.goto
Generating GOTO Program
Adding CPROVER library (arm64)
file <builtin-library-__builtin___memcpy_chk> line 2:  '__builtin___memcpy_chk'
old definition in module  file <builtin-architecture-strings> line 20
void * (void *__param$0, const void *__param$1, __CPROVER_size_t __param$2, __CPROVER_size_t __param$3, __CPROVER_contracts_write_set_ptr_t __write_set_to_check)
new definition in module <built-in-library> file <builtin-library-__builtin___memcpy_chk> line 2
void * (void *dst, const void *src, __CPROVER_size_t n, __CPROVER_size_t size)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 8 object bits, 56 offset bits (default)
Starting Bounded Model Checking
Runtime Symex: 0.190901s
Runtime Postprocess Equation: 0.000155583s
Passing problem to SMT2 QF_AUFBV using Z3
converting SSA

and no more... "top" now shows cbmc consuming 100% CPU time...

This was running "make TARGET=ctcc" in my cbmc-examples/arrays repo.

[rod-chapman]

It moved on to:

Runtime Convert SSA: 285.824s
Running SMT2 QF_AUFBV using Z3

and now I see Z3 consuming 100% CPU after 7 minutes,,,

[rod-chapman]

Z3 has now clocked up 20 minutes CPU time.
I re-wrote this function in SPARK. Verification is automatic and complete in 4 seconds.