Building fails when running checks

[xypron]

CBMC version: 5.89.0-2 (Debian)
Operating system: Ubuntu 23.10
Exact command line resulting in the issue: building in Launchpad
What behaviour did you expect: build succeeds
What happened instead:

Building on some architechtures (e.g. arm64) fails as shown at the end of the buildlog https://launchpadlibrarian.net/683935172/buildlog_ubuntu-mantic-arm64.cbmc_5.89.0-2_BUILDING.txt.gz .

Could it be that the sorting of predicates is not stable?

Best regards

Heinrich

[tautschnig]

Assigning @thomasspriggs: it seems that #7878 yields the very same results, which isn't surprising for the above build also tries to use LTO.

[xypron]

Disabling LTO resolves the problems with the originally failing tests on arm64 and s390x. But on arm64 we now see:

Failed test: fmod1
CBMC version 5.89.0 (cbmc-5.89.0) 64-bit arm64 linux
Parsing main.c
file /usr/include/aarch64-linux-gnu/bits/math-vector.h line 30: syntax error before '__f32x4_t'
PARSING ERROR

https://launchpadlibrarian.net/688275364/buildlog_ubuntu-mantic-arm64.cbmc_5.89.0-2ubuntu1~ppa1_BUILDING.txt.gz

[thomasspriggs]

Have you tried building without LTO?

The work in #7878 includes some symbol de-duplication work, which I should work to get merged to develop regardless of a completely working LTO build. I think LTO also causes issues with building the cproverlib for rust/ffi. It may also reveal issues with undefined behaviour due to more aggressive optimisation.

[thomasspriggs]

Disabling LTO resolves the problems with the originally failing tests on arm64 and s390x. But on arm64 we now see:

Failed test: fmod1 CBMC version 5.89.0 (cbmc-5.89.0) 64-bit arm64 linux Parsing main.c file /usr/include/aarch64-linux-gnu/bits/math-vector.h line 30: syntax error before '__f32x4_t' PARSING ERROR

https://launchpadlibrarian.net/688275364/buildlog_ubuntu-mantic-arm64.cbmc_5.89.0-2ubuntu1~ppa1_BUILDING.txt.gz

I'd guess that the math-vector library is using types specific to the platform on which you are trying to build cbmc, which aren't recognised by cbmc's C parser. However I don't have an arm machine to confirm/debug this with. It is also worth noting that we don't test cbmc on arm in our CI system and the github hosted runners we currently use for our CI don't include an option to test on the ARM platform. (not even for mac). I am not trying to say that we should not support this platform, just explaining that there are some obstacles in our path.

I have shared the information I have on this subject. I am going to re-assign this issue to @TGWDB for prioritisation within my team.