Simplify BigInt power2 API

[fbrausse]

This PR:

• Replaces potentially unbounded left-shifts 1 << n by BigInt arithmetic, and
• simplifies the usage of powers of two via BigInt. I've hidden the setPower2() function and replaced it with power2() and power2m1(). Additionally, the unary operator- on BigInt now takes its argument by-value, thereby preventing additional copies for things like -BigInt::power2(n).

I've also added a few assertions in code that was using the power2 API, mainly related to concat2t. This one used to take signedbvs, but the expr2 simplification code assumed unsigned (or at least the same sign). As it's not entirely clear what signedbv concatenation is supposed to be (sign bits extend arbitrarily far), I've tightened the assumptions here: only unsignedbv concatenations are supported now.

For this last change a few new bitcasts are inserted. I'll run this over the benchmarks to be sure nothing breaks. Locally, this already affected a few regression tests:

• regression/esbmc/github_60: wrong verdict? How can there be an overflow detected when --overflow-check is not passed?
• regression/cbmc/01_cbmc_String_Abstraction7: wrong verdict? fgets stores zero-terminated strings.
• regression/cstd/strerror: was KNOWNBUG.
• regression/esbmc-cpp/cpp/cpp_priority_queue_size_bug: was KNOWNBUG
• regression/esbmc-cpp/cpp/cpp_queue_front_bug: was KNOWNBUG

Edit: Sorry, the above regression test changes are only for a -DESBMC_SVCOMP=ON build. Without that (the default) they're unchanged. We should look into these though.

[lucasccordeiro]

@fbrausse: thanks for submitting this PR.

Shall we consider adding some regression tests here?

Shall we also run it over the sv-comp benchmarks?

[fbrausse]

sv-comp is running: https://github.com/esbmc/esbmc/actions/runs/7059767336

Regarding regression tests I'm not sure what to test exactly. There were some unmet assumptions in the concat2t simplification (which now are enforced)...

[fbrausse]

stats-30s.txt:

Statistics:          23805 Files
  correct:           14433
    correct true:     8016
    correct false:    6417
  incorrect:            26
    incorrect true:     16
    incorrect false:    10
  unknown:            9346
  Score:             21777 (max: 38482)

GitHub actions: https://github.com/esbmc/esbmc/actions/runs/6982246951

This PR:

Statistics:          23805 Files
  correct:           14431
    correct true:     8010
    correct false:    6421
  incorrect:            26
    incorrect true:     15
    incorrect false:    11
  unknown:            9348
  Score:             21785 (max: 38482)

https://github.com/esbmc/esbmc/actions/runs/7059767336

Mostly timeout fluctuation. About the incorrect:

• no-data-race: 2x new incorrect came from previous unknowns fixed earlier in Fixed crash caused by invalid id in value set #1514.
• unreach-call: 2x previously incorrect (close to 30s) now timeout

[lucasccordeiro]

Thanks for submitting this PR, @fbrausse.