Minimal support for `__auto_type` by michael-schwarz · Pull Request #67 · goblint/cil

michael-schwarz · 2022-01-12T16:52:35Z

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 · 2022-01-17T09:05:04Z

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 · 2022-01-17T09:08:16Z

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

michael-schwarz · 2022-01-17T09:25:33Z

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 · 2022-01-17T20:11:40Z

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

michael-schwarz · 2022-01-19T10:27:25Z

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

vogler · 2022-01-21T11:24:41Z

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

michael-schwarz added 2 commits January 12, 2022 16:11

Test for c11 atomic ops

f2ea240

minimal __auto_type

62d873d

michael-schwarz mentioned this pull request Jan 12, 2022

OpenSSL goblint/bench#7

Open

3 tasks

Replace usage of Option.

3b672e6

sim642 added the enhancement label Jan 13, 2022

michael-schwarz mentioned this pull request Jan 14, 2022

Add support for additional float types #60

Merged

Allow comma_expression in __typeof__

85b174f

michael-schwarz marked this pull request as ready for review January 17, 2022 10:12

michael-schwarz requested review from sim642 and vogler January 17, 2022 10:12

sim642 approved these changes Jan 17, 2022

View reviewed changes

michael-schwarz merged commit f8c8fe4 into develop Jan 19, 2022

sim642 deleted the atomic_ops branch May 30, 2022 07:12

sim642 added this to the 2.0.0 milestone Jul 17, 2022

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Minimal support for `__auto_type`#67

Minimal support for `__auto_type`#67
michael-schwarz merged 4 commits intodevelopfrom
atomic_ops

michael-schwarz commented Jan 12, 2022 •

edited

Loading

Uh oh!

michael-schwarz commented Jan 17, 2022

Uh oh!

michael-schwarz commented Jan 17, 2022

Uh oh!

michael-schwarz commented Jan 17, 2022

Uh oh!

michael-schwarz commented Jan 17, 2022

Uh oh!

michael-schwarz commented Jan 19, 2022

Uh oh!

vogler commented Jan 21, 2022

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Conversation

michael-schwarz commented Jan 12, 2022 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

michael-schwarz commented Jan 17, 2022

Uh oh!

michael-schwarz commented Jan 17, 2022

Uh oh!

michael-schwarz commented Jan 17, 2022

Uh oh!

michael-schwarz commented Jan 17, 2022

Uh oh!

michael-schwarz commented Jan 19, 2022

Uh oh!

vogler commented Jan 21, 2022

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

michael-schwarz commented Jan 12, 2022 •

edited

Loading