Server mode crashes on re-analysis

[jerhard]

When analyzing the c-file mentioned in #678, Goblint crashes in server mode on re-analysis of code with:

Fatal error: exception Failure("there can only be one definition and one declaration per global")

When running goblint in server mode, as outlined here e.g. by:

goblint --enable server.enabled --conf goblint.json --enable server.reparse file.c

and the submitting commands like:

{"jsonrpc":"2.0","id":0,"method":"analyze","params":{}}

The first analysis that is triggered succeeds, while the subsequent one crashes with the Failure above. This happens even when the changes made to the file only affect white-space.

This crash does not seem to affect all programs, for some other toy examples I tried the server mode still works.

[jerhard]

For this program, the crash can be avoided when allowing multiple declarations (but not not definitions) in addGlobal in CompareCIL.compareCilFiles for a global. This is strange, that in server mode suddenly multiple declarations for a global appear. Maybe Cil keeps multiple declarations when run by Goblint in server mode?

[sim642]

Well, multiple declaration should be allowed. It's just that the comparison should take place once per varinfo. At least that's what #836 was supposed to do.

Maybe decls should be a list here instead (the name even sounds like that):

analyzer/src/incremental/compareCIL.ml

Line 10 in 33775db

type global_col = {decls: varinfo option; def: global_def option}

[jerhard]

Since we are only interested in the fact whether globals exist and what the varinfo is, I think it is ok to only keep a varinfo option. For all the declarations of global in a Cil.file, all the referenced varinfos should be the same memory object.

[jerhard]

Also see here:

Might be useful to output which declaration it finds multiple of.

There are two functions for which multiple declarations are found in the incremental server run:

static inline int pid_alive(const struct task_struct *p);
static __always_inline void data_access_exceeds_word_size(void)

Where __always_inline is defined as inline __attribute__((always_inline)). It is interesting that both functions are static inline functions. However, there are quite some static inline functions in the same source files that do not have this issue. When running the incremental analysis multiple times in server mode, the number of declarations of the two functions above (or any others) does not further increase, i.e. the number of declarations of these functions stays at two starting from the first incremental run.

@stilscher and I looked at this, and it turns out that when merge-inlines is deactivated, this crash does not occur.

[stilscher]

I created a minimal example for this issue:

static inline void f(void);

static inline void f(void)
{
}

int main(void)
{
    return 0;
}

When analyzed with the following

configuration

{
	"files": ["file.c"],
	"kernel": true,
	"pre": {
		"kernel-root":"headers",
		"cppflags":["-D GOBLINT_NO_PTHREAD_ONCE", "-U __weak"]
	}
}

it fails in the incremental run (with empty diff) due to two declarations for f (with server mode and without). The problem does not appear when f is just a static instead of a static inline function. So there seems to be an issue with merging declarations for static inline functions. I will look into this further.

[stilscher]

I found out that this issue is caused by something rather unrelated to my previous hunch. The command for starting the server mode listed in the issue description above also hands over the file to be analyzed (in contrast to what is described in https://github.com/goblint/bench/blob/8ff038ba93c6cdbdb0ed3d6f992083d14047c719/gobpie-demos/chrony/story.md).
In Goblint files that are handed over as arguments are added to the files option of the configuration unconditionally, no matter whether the respective file is already specified in the list. So if the respective file was already set in the configuration option as in the configuration above, it will be twice in the list of files analyzed by Goblint.

I do not understand yet, why this is actually problematic, but it can be solved by removing the file name either from the command-line arguments or the configuration option files. Also, it doesn't seem to be about merging, because simply parsing and merging two copies of the above minimal test case file (with just one main method) in CIL works just fine. Also, the problem already occurs in the from-scratch run (a CIL warning about the same name being used for two globals is shown), but only leads to failure in the incremental run (because of the additional check when comparing two versions).

So a couple of ideas to avoid this issue:

• only add file arguments from the command-line that are not specified yet
• or alternatively disallow specifying the same file as a command-line argument and in the configuration option at the same time
• document the correct use of the server mode (e.g. in our Read The Docs)
• turn some CIL warnings that often indicate a serious problem into errors (like duplicate globals, conflicting main methods)

What do you think?

[sim642]

• only add file arguments from the command-line that are not specified yet

Deduplicating files would probably be a good idea in general since duplicates can also be added by multiple command line arguments or multiple conf values.

• document the correct use of the server mode (e.g. in our Read The Docs)

We should probably do this, so it's not just documented some random issues. Although duplicate files isn't specifically a server mode issue.

• turn some CIL warnings that often indicate a serious problem into errors (like duplicate globals, conflicting main methods)

I think in SV-COMP we have a lot of duplicate globals errors because we always use the system's 64bit version of pthread.h, which conflicts with the preprocessed versions for 32bit architecture. That would require fixing #54.
Also, CIL's error reporting is very poor (it prints errors itself instead of using specific exceptions), so currently we wouldn't be able to distinguish different kinds from Goblint.