--- layout: fc_discuss_archives title: Message 30 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



Thanks for the reports, we will take a look at the issues. INFINITY and 
NAN are indeed missing from our libc and will be added. About the other 
remarks, we'll take a look and see what needs to be changed, and come 
back to you later.


On 17/07/18 16:27, Manuel Rigger wrote:
> 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 	 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
> _______________________________________________
> 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


-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 3797 bytes
Desc: S/MIME Cryptographic Signature
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20180718/73b4f8cf/attachment-0001.bin>