8000 Tmux · Issue #8 · goblint/bench · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

Tmux #8

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Open
stilscher opened this issue Jan 6, 2022 · 11 comments
Open

Tmux #8

stilscher opened this issue Jan 6, 2022 · 11 comments
Labels
goblint Goblint-specific problem parsing-succeeds project Project to analyze

Comments

@stilscher
Copy link
Member
stilscher commented Jan 6, 2022 •
edited
Loading

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.
@stilscher stilscher added goblint Goblint-specific problem project Project to analyze labels Jan 6, 2022
@michael-schwarz michael-schwarz mentioned this issue Jan 8, 2022
Merged
@michael-schwarz
Copy link
Member

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
Copy link
Member
sim642 commented Jan 8, 2022

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

@michael-schwarz
Copy link
Member
michael-schwarz commented Jan 8, 2022 •
edited
Loading

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
Copy link
Member
sim642 commented Jan 8, 2022

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
Copy link
Member

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
Copy link
Member
sim642 commented Jan 9, 2022

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
Copy link
Member Author

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 .

@michael-schwarz
Copy link
Member

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
Copy link
Member

Combined tmux for further experiments:
tmux.cil.zip

@michael-schwarz michael-schwarz mentioned this issue Jan 21, 2022
Closed
@michael-schwarz
Copy link
Member

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
Copy link
Member

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

@sim642 sim642 mentioned this issue Jan 21, 2022
Merged
@stilscher stilscher mentioned this issue Feb 1, 2022
Open
@sim642 sim642 mentioned this issue Mar 8, 2022
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
goblint Goblint-specific problem parsing-succeeds project Project to analyze
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
3 participants
@sim642 @michael-schwarz @stilscher
0