OpenSSL

[sim642]

• Goblint: goblint/analyzer@206f204
• OpenSSL: https://github.com/openssl/openssl/tree/0fcf2351ecff5db21cba431704e4da631b74904a

Attempt 1

./Configure
bear -- make
goblint -v .

Error:

Frontc is parsing /home/simmo/Desktop/openssl/.goblint/preprocessed/engines/e_afalg.i
/usr/include/stdlib.h[140:8-16] : syntax error
Parsing errorFatal error: exception Frontc.ParseError("Parse error")

The problem is _Float32 here:

# 140 "/usr/include/stdlib.h" 3 4
extern _Float32 strtof32 (const char *__restrict __nptr,
     char **__restrict __endptr)
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));

In engines/e_afalg.c:

/* Required for vmsplice */
#ifndef _GNU_SOURCE
# define _GNU_SOURCE
#endif

_GNU_SOURCE enables (through a number of intermediates) the following in the unpreprocessed stdlib.h:

#if __HAVE_FLOAT32 && __GLIBC_USE (IEC_60559_TYPES_EXT)
extern _Float32 strtof32 (const char *__restrict __nptr,
			  char **__restrict __endptr)
     __THROW __nonnull ((1));
#endif

I think OpenSSL itself doesn't even use _Float32 or that function, but it just gets pulled in with _GNU_SOURCE among tons of other GNU-specific things.

Attempt 2

In floatn-common.h there is the following typedef:

#  if !__GNUC_PREREQ (7, 0) || defined __cplusplus
typedef float _Float32;
#  endif

So in an extremely crude hack to bypass that and cause the typedef to be used in the standard headers, I tried the following to pretend to be GCC 6.0 for the purposes of preprocessing:

goblint -v . --set cppflags[+] '-D__GNUC__=6' --set cppflags[+] '-D__GNUC_MINOR__=0'

Error:

Frontc is parsing /home/simmo/Desktop/openssl/.goblint/preprocessed/engines/e_afalg.i
include/openssl/crypto.h[413:0-0] : syntax error
Parsing errorFatal error: exception Frontc.ParseError("Parse error")

The problem is the _Noreturn here:

# 413 "include/openssl/crypto.h"
_Noreturn void OPENSSL_die(const char *assertion, const char *file, int line);

_Noreturn is a C11 feature that CIL doesn't support (goblint/cil#13).

Attempt 3

In an even more desperate attempt, I tried to just preprocess that keyword away (it's just extra information that technically shouldn't matter):

goblint -v . --set cppflags[+] '-D__GNUC__=6' --set cppflags[+] '-D__GNUC_MINOR__=0' --set cppflags[+] '-D_Noreturn='

Error:

/usr/include/x86_64-linux-gnu/bits/floatn.h:86: Error: Invalid combination of type specifiers
Error on A.TYPEDEF (Errormsg.Error)
Frontc is parsing /home/simmo/Desktop/openssl/.goblint/preprocessed/engines/e_capi.i
Error: There were parsing errors in /home/simmo/Desktop/openssl/.goblint/preprocessed/engines/e_capi.i
Fatal error: exception Errormsg.Error

The problematic code is __float128:

/* The type _Float128 exists only since GCC 7.0.  */
#  if !__GNUC_PREREQ (7, 0) || defined __cplusplus
typedef __float128 _Float128;
#  endif

CIL has has some kind of support for it (goblint/cil#8), but it defines both __float128 and _Float128 as builtin type names, so maybe that's screwing with the parsing of this.
I think that aspect of CIL has been updated for GCC >=7.0, so my version hack above is probably causing this one to happen. The appropriate solution would be to handle the other GNU float types directly as well.

TODO

• Add GNU extended floating-point types to CIL (Add support for additional float types cil#60).
• Add _Noreturn support to CIL (Support for C11 _Noreturn cil#58).
• Add _Atomic support to CIL (Support for _Atomic cil#61).

[michael-schwarz]

I can patch the _Noreturn thing, it shouldn't require much work.
I guess at the same time I'll also cherry pick all C11 things from goblint/cil#24 that do no require AST changes or programmatic support in Goblint to be sound.

[michael-schwarz]

Does goblint/cil#60 resolve this?

[michael-schwarz]

After goblint/cil#60 the issue now is _Atomic:

/usr/lib/gcc/x86_64-linux-gnu/7/include/stdatomic.h[40:9-16] : syntax error
Parsing errorFatal error: exception Frontc.ParseError("Parse error")
Raised at Errormsg.parse_error in file "src/ocamlutil/errormsg.ml", line 328, characters 2-27
Called from Stdlib__parsing.yyparse.loop in file "parsing.ml", line 151, characters 8-44
Called from Stdlib__parsing.yyparse in file "parsing.ml", line 164, characters 4-28
Re-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
Re-raised at Stats.repeattime.repeatf in file "src/ocamlutil/stats.ml", line 110, characters 1-8
Called from Frontc.parse_to_cabs_inner in file "src/frontc/frontc.ml", line 189, characters 15-90
Re-raised at Frontc.parse_to_cabs_inner in file "src/frontc/frontc.ml", line 205, characters 6-73
Called from Frontc.parse_to_cabs in file "src/frontc/frontc.ml", line 121, characters 13-38
Called from Frontc.parse_helper in file "src/frontc/frontc.ml", line 256, characters 13-32

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;

[michael-schwarz]

With goblint/cil#61 there are some warnings during the merging phase, but CFG generation succeeds and solving starts.

[michael-schwarz]

Summary for all memory locations:
        safe:           47
        vulnerable:    117
        unsafe:         26
        -------------------
        total:         190

vars = 7941    evals = 185490  

Timings:
TOTAL                          1724.763 s
  parse                          13.398 s
  convert to CIL                 18.656 s
  analysis                       1692.710 s
    global_inits                   16.474 s
    solving                        1674.621 s
      S.Dom.equal                     0.535 s
      postsolver                      7.987 s
    warn_global                     0.016 s
Timing used
Memory statistics: total=3913961.25MB, max=3778.66MB, minor=3913810.16MB, major=95671.32MB, promoted=95520.23MB
    minor collections=1866348  major collections=115 compactions=0

[sim642]

Thanks for looking into the parsing errors. I'm guessing with all the patches that's with the commands I used in my first attempt, without any cppflags hackery?

Also, what about the __float128 problem from my third attempt? Is it somehow not a problem anymore? Was it just a problem because of my cppflags hacks?

[michael-schwarz]

I'm guessing with all the patches that's with the commands I used in my first attempt, without any cppflags hackery?

Yup, just with the first command.

Also, what about the __float128 problem from my third attempt? Is it somehow not a problem anymore?

Seems like it, I get no error there.

[michael-schwarz]

Found dead code on 21040 lines (including 21039 in uncalled functions)!
Total lines (logical LoC): 22475

Still somewhat on the small side :/