goblint/bench

Tmux

Opened this issue · 11 comments

stilscher commented

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 #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 commented

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 commented

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

michael-schwarz commented

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 commented

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 commented

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 commented

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 commented

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

sh autogen.sh
./configure
bear -- make
goblint -v .
  • 👍1
michael-schwarz commented

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 commented

Combined tmux for further experiments:
tmux.cil.zip

michael-schwarz commented

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

michael-schwarz commented

Also, tmux is single-threaded which means it is unsuitable if we want to go for the race warnings as our example.