search

diffblue / cbmc

C Bounded Model Checker
https://diffblue.github.io/cbmc
Other
822 stars 259 forks source link

Building fails when running checks #7908

Open xypron opened 1 year ago

xypron commented 1 year ago

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 commented 1 year ago

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 commented 12 months ago

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 commented 12 months ago

Have you tried building without LTO?

The work in https://github.com/diffblue/cbmc/pull/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 commented 12 months ago

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.