Investigate Vec performance issues

[zhassan-aws]

• Memory reallocation with Vec kills performance #1657
• High memory usage with a simple string vector example #1673
• Memory blows up on a simple two-dimensional vector example #1226

[tautschnig]

diffblue/cbmc#7230 appears to address #1657 and #1673, but I'm not yet entirely sure about #1226 for that one yields unwinding assertion failures (the examples do terminate much quicker than said in that issue, but I cannot say for sure that this isn't because of changes in how unwinding is interpreted, which has happened at some point).

[tautschnig]

I have now created a collection of PRs that, together, will address this issue:

• Field sensitivity for unions diffblue/cbmc#7230
• Byte extract and extract bits can be constant diffblue/cbmc#7331
• Value sets: handle extractbits out of pointers diffblue/cbmc#7339
• Simplify byte extract: use lowering when expression is a constant diffblue/cbmc#7340
• Simplify non-trivial pointer subtraction diffblue/cbmc#7341
• Further simplification of (in)equalities over pointers diffblue/cbmc#7342
• Extend simplification of extractbits diffblue/cbmc#7343
• Simplify typecast over ID_bv and pointers diffblue/cbmc#7344
• Byte-operator lowering: struct and union constants are not ID_constant diffblue/cbmc#7352

[tautschnig]

All CBMC PRs are now merged and will be part of the 5.72.0 release (due to be published 2022-12-08).