Tmux

[stilscher]

• Goblint: goblint/analyzer@8fb8d8f
• Tmux: https://github.com/tmux/tmux/tree/47923bd5f62f49924e20f3cabcff9350968449a2

Attempt:

• ./goblint -v [path to tmux repository]/Makefile
• or, as an intermediate step, to only check whether it can be build with cilly:
  sh autogen.sh && ./configure && make CC="cilly --gcc=/usr/bin/gcc --merge --keepmerged" LD="cilly --gcc=/usr/bin/gcc --merge --keepmerged"

Problems and Workarounds:

1. missing GNU extended floating point types in CIL (_Float32, _Float64, _Float32x, _Float64x and _Float128x)
   error:

   /usr/include/stdlib.h[140:8-16] : syntax error
   Parsing errorFatal error: exception Frontc.ParseError("Parse error")
   

   This is the same problem as in OpenSSL #7. As a hacky quick fix to find out about other possible problems I patched the goblint-cil implementation: floatsquickfix.patch
2. error during merging with cilly:

   /usr/include/x86_64-linux-gnu/bits/stdlib.h:37:37: error: redefinition of ‘realpath’
   37 | __NTH (realpath (const char *__restrict __name, char *__restrict __resolved))
   

   I think this has something to do with fortify functions which are some form of extern inlining and that it can be tracked back to this code in usr/include/stdlib.h:

   /* Define some macros helping to catch buffer overflows.  */
   #if __USE_FORTIFY_LEVEL > 0 && defined __fortify_function
   # include <bits/stdlib.h>
   #endif
   

   and usr/include/x86_64-linux-gnu/bits/stdlib.h:

   __fortify_function __wur char *
   __NTH (realpath (const char *__restrict __name, char *__restrict __resolved))
   {...}
   

   But I haven't found out yet, what exactly causes the problem with cilly.
   If one turns off the gcc option FORTIFIED_SOURCE with
   ./goblint -v --set cppflags[+] -D_FORTIFY_SOURCE=0 [path to tmux repository]/Makefile
   cilly combines the files without any errors and the analysis is started.
   FORTIFY_SOURCE is implicitly enabled (and set to 2) with the activation of optimization level 2 (-O2) in the tmux Makefile.

[michael-schwarz]

How come you need Float128x? Probably something is still wrong with the way you are building things here?

GCC does not currently support _Float128x on any systems.

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

[sim642]

Well, the standard /usr/include/stdlib.h header does contain it if the extended floating-point types are enabled.

[michael-schwarz]

At least on my machine that is inside a #if __HAVE_FLOAT128X and it would be strange if this is set given GCC does not support that type?

[sim642]

Yeah, I didn't check where and how that is defined, but for some reason it is in the header (although conditionally). If there was no use to that, why would it even be conditionally in there.

[michael-schwarz]

Idk, maybe for other compilers?

If it is necessary I can also add support to CIL where machdep.c contains an additional flag to check for _Float128x and accept programs that contain it if this is set in machdep.ml and use the appropriate sizeof and align values and reject the program otherwise.

But I don't really see the point if it will always be false for GCC, which is the only compiler we want to support.

[sim642]

Idk, maybe for other compilers?

I thought about it, but I'm not sure if or how the headers get shared between compilers because on my system at least that stdlib.h has a GNU copyright declaration on top.
And apparently #define __HAVE_FLOAT128X 0 is just hardcoded in bits/floatn-common.h, which is highly GCC specific (with all the GCC version macros), so I'm not sure how it could behave differently.

Also, I just noticed bits/floatn-common.h ends with this cryptic code:

#  if !__GNUC_PREREQ (7, 0) || defined __cplusplus
#   error "_Float128x supported but no type"
#  endif

No idea what that means. It is supported, but also doesn't have a type? And it triggers a compiler error?

I suspect you might be right that it isn't actually needed, but we'll find out once we try to build the projects with the CIL PR.

[stilscher]

With the added support for additional float types (goblint/cil#60) and by using the compilation database support in goblint, the parsing is successful:

• Goblint: goblint/analyzer@0e68f51
• Tmux: https://github.com/tmux/tmux/tree/47923bd5f62f49924e20f3cabcff9350968449a2

sh autogen.sh
./configure
bear -- make
goblint -v .

[michael-schwarz]

To get it to work with compiledb, one needs to manually edit the compilation database to replace:

• "-DTMUX_TERM=screen-256color" with "-DTMUX_TERM=\"screen-256color\""
• "-DTMUX_CONF=/etc/tmux.conf:~/.tmux.conf:$XDG_CONFIG_HOME/tmux/tmux.conf:~/.config/tmux/tmux.conf" with -DTMUX_CONF=\"/etc/tmux.conf:~/.tmux.conf:$XDG_CONFIG_HOME/tmux/tmux.conf:~/.config/tmux/tmux.conf\""
• "-DTMUX_VERSION=next-3.4" with "-DTMUX_VERSION=\"next-3.4\""

[michael-schwarz]

Combined tmux for further experiments:
tmux.cil.zip

[michael-schwarz]

I left it running overnight with ./goblint ../tmux --disable ana.base.context.non-ptr --disable sem.unknown_function.spawn --set ana.thread.domain plain --enable exp.earlyglobs --set ana.base.privatization none --enable dbg.print_dead_code and goblint/analyzer#547

Results are:

runtime: 02:48:45.203
vars: 1721947, evals: 10638900

Live lines: 10822
Found dead code on 22345 lines (including 21972 in uncalled functions)!
Total lines (logical LoC): 33167

We have ~260 instances of Function definition missing, so my guess would be that once again more code should be live here.

Complete log: tmux.txt