Open stilscher opened 2 years ago
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.
Well, the standard /usr/include/stdlib.h
header does contain it if the extended floating-point types are enabled.
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?
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.
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.
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.
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 .
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\""
Combined tmux
for further experiments:
tmux.cil.zip
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 https://github.com/goblint/analyzer/pull/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
Also, tmux
is single-threaded which means it is unsuitable if we want to go for the race warnings as our example.
Attempt:
./goblint -v [path to tmux repository]/Makefile
sh autogen.sh && ./configure && make CC="cilly --gcc=/usr/bin/gcc --merge --keepmerged" LD="cilly --gcc=/usr/bin/gcc --merge --keepmerged"
Problems and Workarounds:
_Float32
,_Float64
,_Float32x
,_Float64x
and_Float128x
) error:This is the same problem as in https://github.com/goblint/bench/issues/7. As a hacky quick fix to find out about other possible problems I patched the goblint-cil implementation: floatsquickfix.patch
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
:and
usr/include/x86_64-linux-gnu/bits/stdlib.h
: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.