Test failures with GCC 14

[lzaoral]

CBMC version: 5.95.1
Operating system: Fedora Rawhide
Exact command line resulting in the issue: just execute the CORE test suite
What behaviour did you expect: all tests pass
What happened instead: some tests fail

Two types of failures can be observed:

• The first is that some GCC builtins are not declared:

Failed test: SIMD1
CBMC version 5.95.1 (n/a) 64-bit x86_64 linux
Parsing main.c
Converting
Type-checking main
file /usr/lib/gcc/x86_64-redhat-linux/14/include/usermsrintrin.h line 43 function _urdmsr: function '__builtin_ia32_urdmsr' is not declared
file /usr/lib/gcc/x86_64-redhat-linux/14/include/usermsrintrin.h line 50 function _uwrmsr: function '__builtin_ia32_uwrmsr' is not declared
file /usr/lib/gcc/x86_64-redhat-linux/14/include/avxvnniint16intrin.h line 42 function _mm_dpwsud_avx_epi32: function '__builtin_ia32_vpdpwsud128' is not declared
file /usr/lib/gcc/x86_64-redhat-linux/14/include/avxvnniint16intrin.h line 50 function _mm_dpwsuds_avx_epi32: function '__builtin_ia32_vpdpwsuds128' is not declared
file /usr/lib/gcc/x86_64-redhat-linux/14/include/avxvnniint16intrin.h line 58 function _mm_dpwusd_avx_epi32: function '__builtin_ia32_vpdpwusd128' is not declared
file /usr/lib/gcc/x86_64-redhat-linux/14/include/avxvnniint16intrin.h line 66 function _mm_dpwusds_avx_epi32: function '__builtin_ia32_vpdpwusds128' is not declared
file /usr/lib/gcc/x86_64-redhat-linux/14/include/avxvnniint16intrin.h line 74 function _mm_dpwuud_avx_epi32: function '__builtin_ia32_vpdpwuud128' is not declared
file /usr/lib/gcc/x86_64-redhat-linux/14/include/avxvnniint16intrin.h line 82 function _mm_dpwuuds_avx_epi32: function '__builtin_ia32_vpdpwuuds128' is not declared
file /usr/lib/gcc/x86_64-redhat-linux/14/include/avxvnniint16intrin.h line 90 function _mm256_dpwsud_avx_epi32: function '__builtin_ia32_vpdpwsud256' is not declared
file /usr/lib/gcc/x86_64-redhat-linux/14/include/avxvnniint16intrin.h line 98 function _mm256_dpwsuds_avx_epi32: function '__builtin_ia32_vpdpwsuds256' is not declared
file /usr/lib/gcc/x86_64-redhat-linux/14/include/avxvnniint16intrin.h line 106 function _mm256_dpwusd_avx_epi32: function '__builtin_ia32_vpdpwusd256' is not declared
file /usr/lib/gcc/x86_64-redhat-linux/14/include/avxvnniint16intrin.h line 114 function _mm256_dpwusds_avx_epi32: function '__builtin_ia32_vpdpwusds256' is not declared
file /usr/lib/gcc/x86_64-redhat-linux/14/include/avxvnniint16intrin.h line 122 function _mm256_dpwuud_avx_epi32: function '__builtin_ia32_vpdpwuud256' is not declared
file /usr/lib/gcc/x86_64-redhat-linux/14/include/avxvnniint16intrin.h line 130 function _mm256_dpwuuds_avx_epi32: function '__builtin_ia32_vpdpwuuds256' is not declared
file /usr/lib/gcc/x86_64-redhat-linux/14/include/avx2intrin.h line 1932 function _mm_reduce_add_epi16: function '__builtin_shufflevector' is not declared
file /usr/lib/gcc/x86_64-redhat-linux/14/include/avx2intrin.h line 1932 function _mm_reduce_add_epi16: in expression '__builtin_shufflevector(__T1, __T1, 4, 5, 6, 7, 4, 5, 6, 7)':
conversion from 'signed int' to '__gcc_v8hi': implicit conversion not permitted
CONVERSION ERROR
EXIT=6
SIGNAL=0
Failed test.desc lines:
^EXIT=0$ [FAILED]
^VERIFICATION SUCCESSFUL$ [FAILED]

• The second is that almost all C++ related tests fail with the same error:

Failed test: Constructor1
CBMC version 5.95.1 (n/a) 64-bit x86_64 linux
Parsing main.cpp
file /usr/include/c++/14/x86_64-redhat-linux/bits/c++config.h line 2669: parse error before ') __bfloat16_t ; }'
PARSING ERROR
EXIT=6
SIGNAL=0
Failed test.desc lines:
^EXIT=0$ [FAILED]
^VERIFICATION SUCCESSFUL$ [FAILED]

[martin-cs]

Hi @lzaoral

Thanks for reporting this. Would it be possible for you to test this with GCC 13 or earlier and the latest CBMC?

[tautschnig]

For the first issue it would seem that __builtin_shufflevector is now also supported by GCC, and not just Clang. We added support for it in de4557f, but now seemingly need to remove the restriction to Clang.

For the second issue we need to add support for bf16 constants as seen here:

typedef __decltype(0.0bf16) __bfloat16_t;

[tautschnig]

For the first issue it would seem that __builtin_shufflevector is now also supported by GCC, and not just Clang. We added support for it in de4557f, but now seemingly need to remove the restriction to Clang.

Fixed in #8170.

For the second issue we need to add support for bf16 constants as seen here:

typedef __decltype(0.0bf16) __bfloat16_t;

Done in #8169.

[tautschnig]

All relevant PRs have now been merged, closing.