--- layout: fc_discuss_archives title: Message 29 from Frama-C-discuss on July 2018 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] GCC Builtins Support



Hello André,

thanks a lot for your response!

With this option, 41 of the 100 test cases do not result in a warning
or error. In 35 cases, builtins are still not recognized.

In 9 cases, Frama-C aborts because the INFINITY or NAN macro are used.
Is there some way to define them over compiler flags?

14 test cases fail due to type mismatches in the __sync builtins. For
example, for the __sync_add_and_fetch test case I get the error below:

[kernel] Parsing test-cases/12-__sync_add_and_fetch.c (with preprocessing)
[kernel:typing:incompatible-types-call]
test-cases/12-__sync_add_and_fetch.c:5: Warning:
  expected 'int *' but got argument of type 'int volatile *': & a
[kernel:typing:incompatible-types-call]
test-cases/12-__sync_add_and_fetch.c:12: Warning:
  expected 'int *' but got argument of type 'long volatile *': & a
[kernel:typing:incompatible-types-call]
test-cases/12-__sync_add_and_fetch.c:19: Warning:
  expected 'long long *' but got argument of type 'long long volatile *': & a

It seems that Frama-C does not expect volatile variables as input.
Furthermore, the warning in line 12 is surprising. It can be
reproduced with this simplified test case:

#include <assert.h>

void test_long() {
  long a = 1;
  long result = __sync_add_and_fetch(&a, 5L);
  assert(a == 6);
  assert(result == 6);
}


Frama-C expects `a` to be an int instead of a long variable, which is
in conflict with the GCC docs (see
https://gcc.gnu.org/onlinedocs/gcc-4.5.4/gcc/Atomic-Builtins.html).
The versions for int and long long variables work as expected. Similar
warnings are also emitted for __sync_fetch_and_xor,
__sync_val_compare_and_swap, __sync_fetch_and_sub,
__sync_fetch_and_add, __sync_fetch_and_and, __sync_and_and_fetch,
__sync_fetch_and_and, __sync_or_and_fetch, __sync_fetch_and_or,
__sync_bool_compare_and_swap, __sync_lock_test_and_set,
__sync_lock_release, and __sync_sub_and_fetch.

Is this a bug?

I also stumbled over a second unexpected warning for
__builtin_object_size. The reduced test case looks as follows:

#include <assert.h>
#include <stdlib.h>

void local_buffer() {
  int var;
  size_t size = __builtin_object_size(&var, 0);
  assert(size == sizeof(int) || size == (size_t)-1);
}

The warning that I get is this: "[kernel] test.c:6: Failure: Cannot
resolve variable ptr" Since there is no `ptr` variable in the test
case, I assume that __builtin_object_size is implemented in terms of a
macro that uses this undeclared variable?

Best,
Manuel

2018-07-17 15:05 GMT+02:00 Andre Maroneze <Andre.OLIVEIRAMARONEZE at cea.fr>:
> Hello,
>
> Thanks for the interest in Frama-C.
>
> By default, Frama-C assumes the input source code to be as close to the C
> standard as possible, which excludes compiler builtins in the name of
> portability.
>
> That said, usage of GCC-based architecture configuration files (called
> "machdeps", which include both machine features such as register size, but
> also compiler extensions, such as GCC and MSVC), e.g. with option `-machdep
> gcc_x86_32`, should enable some GCC builtins to be recognized.
>
> For instance, if I run `frama-c tests/syntax/gcc_builtins.c` (using the test
> files distributed in the Frama-C .tar.gz), I get:
>
> [kernel] Parsing tests/syntax/gcc_builtins.c (with preprocessing)
> [kernel:typing:implicit-function-declaration]
> tests/syntax/gcc_builtins.c:187: Warning:
>   Calling undeclared function __builtin_expect. Old style K&R code?
>
> However, if I add a GCC machdep, with `frama-c -machdep gcc_x86_32
> tests/syntax/gcc_builtins.c`, the warning disappears:
>
> [kernel] Parsing tests/syntax/gcc_builtins.c (with preprocessing)
>
> Option `-machdep help` lists the available machdeps. Those prefixed with
> `gcc` enable GCC-specific features.
>
> Note that variadic functions, by default, are handled using the Variadic
> plug-in, so __builtin_va_start and similar ones may end up being translated
> by the plug-in after parsing. If you want to disable it, you'll need option
> `-variadic-no-translation`.
>
> Adding extra built-ins is usually done when needed for a case study;
> ideally, if there are interesting pieces of code using those builtins, we
> add them to be able to handle the code. Still, if all that is required is to
> add some macros, and there are already unit tests to check them, it could be
> worthwhile to add more built-ins.
>
>
>
> On 12/07/18 14:18, Manuel Rigger wrote:
>
> Hi everyone,
>
> we are currently studying the usage of GCC builtins [1] by GitHub projects
> and how well various tools support them. To that end, we are also developing
> a test suite for the most frequently used machine-independent GCC builtins
> (available at https://github.com/gcc-builtins/tests). We'd be glad to
> contribute the test suite (or parts of it) to Frama-C, if you are
> interested.
>
> From the test cases, it seems that Frama-C does not support any of the
> most-frequently-used public builtins. It appears that they are not
> recognized, as I get warnings like this one: "Warning: Calling undeclared
> function __builtin_expect. Old style K&R code?"
>
> From the source code (in src/kernel_internals/typing/cabs2cil.ml), it seems
> that the GCC-internal builtins for varargs handling (e.g.,
> __builtin_va_start, __builtin_va_arg, and __builtin_va_end) are supported,
> which I verified with an additional test case. Besides, I found some
> evidence in the code that __builtin_compatible_p is supported (which is also
> mentioned in the changelog: "Support for static evaluation of the
> __builtin_compatible_p GCC specific function."). Nevertheless, Frama-C does
> not seem to actually support that builtin. The same is true for some other
> builtins (like __builtin_constant_p and __builtin_expect).
>
> Are there any plans to support more GCC builtins in Frama-C or does a
> Frama-C plugin already support them?
>
> Some of the frequently used builtins have equivalent libc functions (e.g.,
> __builtin_fabs is equivalent to fabs). To me, defining aliases to the libc
> equivalents would seem like a first step to add better builtin support to
> Frama-C.
>
> Best,
> Manuel
>
> [1] https://gcc.gnu.org/onlinedocs/gcc/Other-Builtins.html
>
>
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss
>
>
> --
> André Maroneze
> Researcher/Engineer CEA/LIST
> Software Reliability and Security Laboratory
>
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss