Minimal support for __auto_type

[michael-schwarz]

GCC makes use of the __auto_type feature in code that some C11 atomic accesses get turned into by the preprocessor.

Also, on OS X, in these cases, comma_expressions may appear inside of __typeof__ without an additional pair of parentheses, so this PR also adds support for that.

[michael-schwarz]

On a similar note: Can you have a look at what is going on on MacOS for #67, e.g., by providing the output of the preprocessor for test/small1/c11-atomic-store.c? It is needed to parse code that makes use of some C11 style atomics (e.g. in OpenSSL goblint/bench#7 (comment)). It's hard to debug failures that just happen on OS X by trial and error and the CI.

atomic_ops $ make test
...
Starting test 398/425 on Fri Jan 14 10:29:33 2022: testrunc11/c11-atomic-store
c11-atomic-store.c[18:19-26] : syntax error
Parsing errorFatal error: exception Frontc.ParseError("Parse error")
Raised at Stdlib__parsing.yyparse in file "parsing.ml", line 183, characters 8-17
Called from Stats.repeattime.repeatf in file "src/ocamlutil/stats.ml", line 106, characters 10-15
make[1]: *** [testrunc11/c11-atomic-store] Error 2

    === STDOUT ===
cd ./small1; /Users/voglerr/goblint/cil/test/../bin/cilly --mode=GNUCC --decil --save-temps  --strictcheck --stats --nomerge  --commPrintLn  \
	       -D_GNUCC -Wall -g -ggdb -D_DEBUG -std=c11 -oc11-atomic-store.exe c11-atomic-store.c -lm
...

Successful tests:     381
Failed as expected:   40
Unexpected success:   2
Unexpected failure:   2

[86] GOOD NEWS: A test that used to fail (Notbug. Some gcc versions fail to compile this test on i386) now succeeds:
  CC=gcc-11 make scott/regparm0
[186] GOOD NEWS: A test that used to fail (Bug. Constant-folding of very large arrays does not work on 32-bit machines.) now succeeds:
  CC=gcc-11 make test/sizeof3
[397] A regression test command failed:
  CC=gcc-11 make testrunc11/c11-atomic-store
[399] A regression test command failed:
  CC=gcc-11 make testrunc11/c11-extendedFloat

`c11-atomic-store.i`:

# 0 "c11-atomic-store.c"
# 1 "/Users/voglerr/goblint/cil/test/small1//"
# 0 "<built-in>"
# 0 "<command-line>"
# 1 "c11-atomic-store.c"
# 1 "testharness.h" 1


  extern int printf(const char * format, ...);
# 12 "testharness.h"
extern void exit(int);
# 2 "c11-atomic-store.c" 2
# 1 "/opt/homebrew/Cellar/gcc/11.2.0_3/lib/gcc/11/gcc/aarch64-apple-darwin21/11/include/stdnoreturn.h" 1 3 4
# 3 "c11-atomic-store.c" 2
# 1 "/opt/homebrew/Cellar/gcc/11.2.0_3/lib/gcc/11/gcc/aarch64-apple-darwin21/11/include/stdatomic.h" 1 3 4
# 29 "/opt/homebrew/Cellar/gcc/11.2.0_3/lib/gcc/11/gcc/aarch64-apple-darwin21/11/include/stdatomic.h" 3 4

# 29 "/opt/homebrew/Cellar/gcc/11.2.0_3/lib/gcc/11/gcc/aarch64-apple-darwin21/11/include/stdatomic.h" 3 4
typedef enum
  {
    memory_order_relaxed = 0,
    memory_order_consume = 1,
    memory_order_acquire = 2,
    memory_order_release = 3,
    memory_order_acq_rel = 4,
    memory_order_seq_cst = 5
  } memory_order;


typedef _Atomic _Bool atomic_bool;
typedef _Atomic char atomic_char;
typedef _Atomic signed char atomic_schar;
typedef _Atomic unsigned char atomic_uchar;
typedef _Atomic short atomic_short;
typedef _Atomic unsigned short atomic_ushort;
typedef _Atomic int atomic_int;
typedef _Atomic unsigned int atomic_uint;
typedef _Atomic long atomic_long;
typedef _Atomic unsigned long atomic_ulong;
typedef _Atomic long long atomic_llong;
typedef _Atomic unsigned long long atomic_ullong;
typedef _Atomic short unsigned int atomic_char16_t;
typedef _Atomic unsigned int atomic_char32_t;
typedef _Atomic int atomic_wchar_t;
typedef _Atomic signed char atomic_int_least8_t;
typedef _Atomic unsigned char atomic_uint_least8_t;
typedef _Atomic short int atomic_int_least16_t;
typedef _Atomic short unsigned int atomic_uint_least16_t;
typedef _Atomic int atomic_int_least32_t;
typedef _Atomic unsigned int atomic_uint_least32_t;
typedef _Atomic long long int atomic_int_least64_t;
typedef _Atomic long long unsigned int atomic_uint_least64_t;
typedef _Atomic signed char atomic_int_fast8_t;
typedef _Atomic unsigned char atomic_uint_fast8_t;
typedef _Atomic short int atomic_int_fast16_t;
typedef _Atomic short unsigned int atomic_uint_fast16_t;
typedef _Atomic int atomic_int_fast32_t;
typedef _Atomic unsigned int atomic_uint_fast32_t;
typedef _Atomic long long int atomic_int_fast64_t;
typedef _Atomic long long unsigned int atomic_uint_fast64_t;
typedef _Atomic long int atomic_intptr_t;
typedef _Atomic long unsigned int atomic_uintptr_t;
typedef _Atomic long unsigned int atomic_size_t;
typedef _Atomic long int atomic_ptrdiff_t;
typedef _Atomic long int atomic_intmax_t;
typedef _Atomic long unsigned int atomic_uintmax_t;
# 92 "/opt/homebrew/Cellar/gcc/11.2.0_3/lib/gcc/11/gcc/aarch64-apple-darwin21/11/include/stdatomic.h" 3 4
extern void atomic_thread_fence (memory_order);

extern void atomic_signal_fence (memory_order);
# 218 "/opt/homebrew/Cellar/gcc/11.2.0_3/lib/gcc/11/gcc/aarch64-apple-darwin21/11/include/stdatomic.h" 3 4
typedef _Atomic struct
{

  _Bool __val;



} atomic_flag;




extern _Bool atomic_flag_test_and_set (volatile atomic_flag *);


extern _Bool atomic_flag_test_and_set_explicit (volatile atomic_flag *,
      memory_order);



extern void atomic_flag_clear (volatile atomic_flag *);

extern void atomic_flag_clear_explicit (volatile atomic_flag *, memory_order);
# 4 "c11-atomic-store.c" 2


# 5 "c11-atomic-store.c"
typedef _Atomic _Bool atomic_bool;


int main() {
    atomic_int ato;
    _Atomic int* ptr = &ato;

    __extension__ ({
        __auto_type blub = ato;
        ato = 8;
    });


    
# 18 "c11-atomic-store.c" 3 4
   __extension__ ({ __auto_type __atomic_store_ptr = (
# 18 "c11-atomic-store.c"
   ptr
# 18 "c11-atomic-store.c" 3 4
   ); __typeof__ ((void)0, *__atomic_store_ptr) __atomic_store_tmp = (
# 18 "c11-atomic-store.c"
   17
# 18 "c11-atomic-store.c" 3 4
   ); __atomic_store (__atomic_store_ptr, &__atomic_store_tmp, (5)); })
# 18 "c11-atomic-store.c"
                       ;
    
# 19 "c11-atomic-store.c" 3 4
   __extension__ ({ __auto_type __atomic_store_ptr = (
# 19 "c11-atomic-store.c"
   ptr
# 19 "c11-atomic-store.c" 3 4
   ); __typeof__ ((void)0, *__atomic_store_ptr) __atomic_store_tmp = (
# 19 "c11-atomic-store.c"
   17
# 19 "c11-atomic-store.c" 3 4
   ); __atomic_store (__atomic_store_ptr, &__atomic_store_tmp, (
# 19 "c11-atomic-store.c"
   memory_order_relaxed
# 19 "c11-atomic-store.c" 3 4
   )); })
# 19 "c11-atomic-store.c"
                                                     ;
    { printf("Success\n"); exit(0); };
}

Originally posted by @vogler in #60 (comment)

[michael-schwarz]

The issue seems to be that we end up with a __typeof__ on the left-hand-side of a declaration.

[michael-schwarz]

Actually, CIL even supports that.
What is problematic is the marvelous idea to put a comma expression inside of a __typeof__:

__typeof__ ((void)0, *__atomic_store_ptr)

[michael-schwarz]

@vogler could you check if this works on M1 too?

[michael-schwarz]

I'll merge it for now, please complain if there is issues with M1.

[vogler]

Works:

Successful tests:     383
Failed as expected:   40
Unexpected success:   2
Unexpected failure:   0

[86] GOOD NEWS: A test that used to fail (Notbug. Some gcc versions fail to compile this test on i386) now succeeds:
  CC=gcc-11 make scott/regparm0
[186] GOOD NEWS: A test that used to fail (Bug. Constant-folding of very large arrays does not work on 32-bit machines.) now succeeds:
  CC=gcc-11 make test/sizeof3

However, had to do a make clean. Before, make; make test gave me this for some reason:

Successful tests:     327
Failed as expected:   22
Unexpected success:   20
Unexpected failure:   56