Goto-cc doesn't handle BUILD_BUG_ON_ZERO macro in Linux

[rodionov]

CBMC version:

goto-cc --version
gcc (goto-cc 5.85.0 (cbmc-5.85.0)) 13.2.0

Copyright (C) 2006-2018 Daniel Kroening, Christoph Wintersteiger
CBMC version: 5.85.0 (cbmc-5.85.0)
Architecture: x86_64
OS: linux
gcc: 13.2.0

Exact command line resulting in the issue:

cat > test.c<< EOF
#define __is_constexpr(x) \
  (sizeof(int) == sizeof(*(8 ? ((void *)((long)(x) * 0l)) : (int *)8)))

#define BUILD_BUG_ON_ZERO(e) ((int)(sizeof(struct { int:(-!!(e)); })))
#define GENMASK_INPUT_CHECK(h, l) \
  (BUILD_BUG_ON_ZERO(__builtin_choose_expr( \
    __is_constexpr((l) > (h)), (l) > (h), 0)))

int test(int field)
{
  return GENMASK_INPUT_CHECK(field + 3, field);
}
EOF

goto-cc /tmp/test.c 
/tmp/test.c: In function 'test':
/tmp/test.c:12:1: error: expected constant expression, but got '-(field >= field + 3 ? 0 : 1)'
   return BUILD_BUG_ON_ZERO(field + 3 > field);
CONVERSION ERROR

What behaviour did you expect:

Both gcc and clang compile this code without errors:

clang --version
Debian clang version 14.0.6
Target: x86_64-pc-linux-gnu
Thread model: posix
InstalledDir: /usr/bin

gcc --version
cc --version
gcc (Debian 13.2.0-2+build1) 13.2.0
Copyright (C) 2023 Free Software Foundation, Inc.

clang -c test.c
gcc -c test.c

The macro BUILD_BUG_ON_ZERO is used in Linux kernel, thus, fixing this issue would help with enabling cbmc for Linux.

[kroening]

The problem would appear to be that __is_constexpr doesn't work as expected.

[rodionov]

Interestingly, defining #define BUILD_BUG_ON_ZERO(e) (e) so that the reproducer looks like

#define __is_constexpr(x) \
  (sizeof(int) == sizeof(*(8 ? ((void *)((long)(x) * 0l)) : (int *)8)))

#define BUILD_BUG_ON_ZERO(e) (e)
#define GENMASK_INPUT_CHECK(h, l) \
  (BUILD_BUG_ON_ZERO(__builtin_choose_expr( \
    __is_constexpr((l) > (h)), (l) > (h), 0)))

int test(int field)
{
  return GENMASK_INPUT_CHECK(field + 3, field);
}

doesn't generate the error by goto-cc.

[tautschnig]

I recalled that I had looked into this before. Patch from 2021 now PRed as #7959.