32-bit builds with warnings as errors are broken

[reuk]

Currently it is not possible to produce a 32-bit build of CBMC with -Wall -Wpedantic -Werror set. This is because there is a cast from 2<<32 to size_t which gets truncated to 0 on 32-bit platforms (in interpreter.cpp).

There have been several attempts to fix this problem.

The first attempt, #987, solves the problem by reducing the shift amount to 1<<32. It is not clear why this PR was not accepted.

The second attempt, #1330, keeps the shift amount at 2<<32 and attempts to solve the problem by using mp_integer wherever possible in the interpreter in order to avoid truncation altogether. However, to facilitate minimal changes in this patch, the binary operators in mp_integer had to be changed to allow conversions on both sides of operators (it's surprising to have BigInt + size_t work, but size_t + BigInt result in a compile error - associative operators should be really associative). As a result, #1330 depends on #1341.

There were concerns about the performance implications of the new mp_integer operators in #1341, which may introduce conversions which weren't required before. It is not practical for me to build a benchmarking suite (this would be an enormous undertaking and I do not have the necessary expertise in either benchmarking or the customer requirements), and so #1341 will not be merge-able in the near future.

[mgudemann]

#987 left too little space for object allocation I think, after that we decided to leave 32-bit support aside for the moment. The initial change of 2<<32` was also to make it consistent with the comment, but it turned out that a real solution would be more complex

[reuk]

I see. That probably means that #1330 is too simplistic then, if it keeps the 2<<32 value in place

[mgudemann]

not necessarily, but the comment should be consistent with the code, which wasn't the case. Also 2<<32 is undefined on 32-bit, so this was found when trying to compile CBMC on a 32-bit system after the move to -Werror was made.

[tautschnig]

@reuk Would you happen to know whether this is solved, or how we would confirm it is? #1341 and #1330#1484 have been merged.

[reuk]

Not sure if it's solved. It should be possible to do a cross-compile with CMake (which might be a good nightly build candidate...), but I haven't done that before so it will take me some time to work out how to do it. I'll give it a go if I have time.

[reuk]

The following completes without any problems. Hopefully it's enough to resolve this issue.

$ cmake -H. -Bbuild-32-release -GNinja -DCMAKE_BUILD_TYPE=Release '-DCMAKE_CXX_FLAGS=-m32'
$ cmake --build build-32-release

[tautschnig]

@reuk Thank you very much for undertaking this experiment!