Add support for additional float types

[michael-schwarz]

The goal here is to add (proper) support for _Float32, _Float64, _Float32x, _Float64x and _Float128x, as deemed necessary by goblint/bench#8 and goblint/bench#7

My suggestion is to not add support on the CIL side and limit support to machines on which these types alias to any out of float, double and _Float128.

We can check that before going from CABS->CIL and only deal with the established fkinds on the CIL side of things (and by extension Goblint) then.

[michael-schwarz]

Not adding _Float128x as

GCC does not currently support _Float128x on any systems.

https://gcc.gnu.org/onlinedocs/gcc/Floating-Types.html

[sim642]

There's a test/a.out file committed here, but since it's binary GitHub doesn't let me comment on it directly. Besides removing it, might be a good idea to add a.out or something to .gitignore?

[vogler]

This breaks the build on M1 macOS:

[NOTE] Package goblint-cil is currently pinned to git+https://github.com/goblint/cil.git#9b348e9024aea825b80efa3d55c65e62b8eab18e (version 1.8.2).
[goblint-cil.1.8.2] synchronised (no changes)
goblint-cil is now pinned to git+https://github.com/goblint/cil.git#b77c663690519be8a672f871a036df3d89b677d5 (version 1.8.2)
The following actions will be performed:
  ↻ recompile goblint-cil 1.8.2* [upstream or system changes]

<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><>  🐫
[ERROR] The compilation of goblint-cil.1.8.2 failed at "dune build -p goblint-cil -j 7 @install".

#=== ERROR while compiling goblint-cil.1.8.2 ==================================#
# context     2.1.2 | macos/arm64 | ocaml-base-compiler.4.13.1 | pinned(git+https://github.com/goblint/cil.git#b77c663690519be8a672f871a036df3d89b677d5#b77c6636)
# path        ~/goblint/analyzer/_opam/.opam-switch/build/goblint-cil.1.8.2
# command     ~/.opam/opam-init/hooks/sandbox.sh build dune build -p goblint-cil -j 7 @install
# exit-code   1
# env-file    ~/.opam/log/goblint-cil-45000-b9c220.env
# output-file ~/.opam/log/goblint-cil-45000-b9c220.out
### output ###
# [...]
# (cd _build/default && /usr/bin/make machdep)
# src/machdep-ml.c: In function 'main':
# src/machdep-ml.c:185:7: error: '_Float64x' is not supported on this target
#   185 |       _Float64x f;
#       |       ^~~~~~~~~
# src/machdep-ml.c:281:26: error: '_Float64x' is not supported on this target
#   281 |              (int)sizeof(_Float64x), alignof_float64x,
#       |                          ^~~~~~~~~
# src/machdep-ml.c:310:67: error: '_Float64x' is not supported on this target
#   310 |       printf("\t sizeof_float64x            = %d;\n", (int)sizeof(_Float64x));
#       |                                                                   ^~~~~~~~~
# make: *** [_build/machdep.ml] Error 1

[michael-schwarz]

Yeah, it is a bit annoying we don't have a runner on the M1 architecture such that we could catch these earlier.

At least on my machine __HAVE_FLOAT64X is set, so you could solve this issue by modifying the machdep-ml.c.in file to do

      # ifdef __HAVE_FLOAT64X
        printf("\t sizeof_float64x            = %d;\n", (int)sizeof(_Float64x));
      # else
        printf("\t sizeof_float64x            = 0;\n");
      # endif

(and similarly for the alignof).

That would set the size of _Float64x to 0 which means that parsing code that contains it succeeds but the conversion CABS->CIL later will fail as the size of none of the "usual" types is 0 bytes.

    | [A.Tfloat64x] ->
      if !Machdep.theMachine.Machdep.sizeof_float64x = !Machdep.theMachine.Machdep.sizeof_float &&
          !Machdep.theMachine.Machdep.alignof_float64x = !Machdep.theMachine.Machdep.alignof_float
      then
        TFloat(FFloat, [])
      else if !Machdep.theMachine.Machdep.sizeof_float64x = !Machdep.theMachine.Machdep.sizeof_double &&
        !Machdep.theMachine.Machdep.alignof_float64x = !Machdep.theMachine.Machdep.alignof_double
      then
        TFloat(FDouble, [])
      else if !Machdep.theMachine.Machdep.sizeof_float64x = !Machdep.theMachine.Machdep.sizeof_longdouble &&
        !Machdep.theMachine.Machdep.alignof_float64x = !Machdep.theMachine.Machdep.alignof_longdouble
      then
        TFloat(FLongDouble, [])
      else
        E.s (error "float64x only supported on machines where it is an alias for a conventional type: size: %i align: %i "
          !Machdep.theMachine.Machdep.sizeof_float64x
          !Machdep.theMachine.Machdep.alignof_float64x
          )

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.

[sim642]

Hold on, what version of GCC is the one failing on M1? These are compiler built-in types, so it seems a bit weird that there would be differences like that, because it's not just a question of M1 having a different set of headers.

Or actually, is CIL's Machdep and tests even using the actual gcc from homebrew? In Goblint we have the hack to find a compiler which is actually GCC, not clang pretending to be GCC. If I remember correctly, on Macos the default gcc is symlinked to clang.

[michael-schwarz]

The _Float64x type is supported on all systems where __float128 is supported

__float128 is available on i386, x86_64, IA-64, and hppa HP-UX, as well as on PowerPC GNU/Linux targets that enable the vector scalar (VSX) instruction set

https://gcc.gnu.org/onlinedocs/gcc/Floating-Types.html
So according to the GCC docs at least I'd guess _Float64x is unsupported for M1.

[sim642]

The more I look into this the more confused I am. Homebrew has GCC 11, but that doesn't yet support M1. That's still in progress and maybe only comes to GCC 12: https://www.phoronix.com/scan.php?page=news_item&px=GCC-12-Apple-M1-Port-Plan.

So how can gcc-11 (from homebrew) work at all on M1? Or has it been using gcc (symlinked to Apple's clang with M1 support) all along?

I was thinking of maybe trying out some cross-compilation for M1 to at least be able to run the preprocessor with M1 builtins and M1 standard library, but apart from that WIP GCC fork, that doesn't seem to exist yet at all.

[vogler]

Idk, I've been using gcc-11 since December.

$ gcc-11 --version
gcc-11 (Homebrew GCC 11.2.0_3) 11.2.0
Copyright (C) 2021 Free Software Foundation, Inc.
This is free software; see the source for copying conditions.  There is NO
warranty; not even for MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.

$ brew info gcc
gcc: stable 11.2.0 (bottled), HEAD
GNU compiler collection
https://gcc.gnu.org/
/opt/homebrew/Cellar/gcc/11.2.0_3 (1,412 files, 338.3MB) *
  Poured from bottle on 2021-12-01 at 21:59:41
From: https://github.com/Homebrew/homebrew-core/blob/HEAD/Formula/gcc.rb
License: GPL-3.0-or-later with GCC-exception-3.1
==> Dependencies
Required: gmp ✔, isl ✔, libmpc ✔, mpfr ✔, zstd ✔
==> Options
--HEAD
	Install HEAD version
==> Analytics
install: 104,795 (30 days), 402,866 (90 days), 1,425,189 (365 days)
install-on-request: 44,035 (30 days), 186,932 (90 days), 655,663 (365 days)
build-error: 268 (30 days)

$ gcc --version
Configured with: --prefix=/Library/Developer/CommandLineTools/usr --with-gxx-include-dir=/Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/c++/4.2.1
Apple clang version 13.0.0 (clang-1300.0.29.30)
Target: arm64-apple-darwin21.2.0
Thread model: posix
InstalledDir: /Library/Developer/CommandLineTools/usr/bin

CIL is also using it:

$ ./configure
...
CIL configuration:
  gcc to use                  CC                 gcc-11
  default compiler            DEFAULT_COMPILER   _GNUCC
  CIL version                 CIL_VERSION        1.8.2
  Native OCaml CIL libs                          yes

[sim642]

Apparently GCC 11 from homebrew on M1 (ARM) uses a backport of the WIP GCC 12: https://github.com/Homebrew/homebrew-core/blob/59a84bc37721fcd79b3043b5b2bbc1421104dfd2/Formula/gcc.rb#L4-L10. That explains how it works at all.

EDIT: Although I wonder what standard library it uses then though. Because I think that isn't part of GCC itself, but on Linux separately glibc. Does it still use Apple's standard (Clang) headers on M1 then? @vogler

[vogler]

EDIT: Although I wonder what standard library it uses then though. Because I think that isn't part of GCC itself, but on Linux separately glibc. Does it still use Apple's standard (Clang) headers on M1 then? @vogler

I thought it did, but with keepcpp I just have gcc paths for goblint's stdlib.c:

# 1 "/Users/voglerr/goblint/analyzer/includes/stdlib.c"
...
# 143 "/opt/homebrew/Cellar/gcc/11.2.0_3/lib/gcc/11/gcc/aarch64-apple-darwin21/11/include/stddef.h" 3 4
typedef long int ptrdiff_t;

However, the problem in #41 was in /Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/mach/arm/_structs.h.

[vogler]

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); };
}