Group globals for comparison and updating of ids

[stilscher]

This PR a fix for the way globals are handled in the version comparison and when updating the ids. Globals are now identified only by their name. The associated declaration and at most one definition of a global are grouped together, when collecting them for comparison. In case a definition exists, it is sufficient to consider the definition only, since declarations share the same varinfo with the defnition. We checked in cabs2cil that also only at most one declaration is created for a global, even though the cil documentation does not state this clearly. Therefore, when grouping entities belonging to a global, only a single declaration can be collected. In case multiple are found in the CIL file, an error is thrown. I updated the cil documentation about GVarDecls in goblint/cil@729a1ff3f300330043af118141229079e0fad499 for future reference.

This PR also fixes the incremental tests 03/02 and 03/03 which previously failed when the cfg comparison was enabled.

Closes #627

[sim642]

We checked in cabs2cil that also only at most one declaration is created for a global, even though the cil documentation does not state this clearly. Therefore, when grouping entities belonging to a global, only a single declaration can be collected. In case multiple are found in the CIL file, an error is thrown.

Is that also preserved by Mergecil? Because even if Cabs2cil on each file does produce at most one declaration (in addition to a definition), then maybe Mergecil leaves all the declarations?

[michael-schwarz]

We also checked that, and Mergecil preserves that invariant.

[jerhard]

Is that also preserved by Mergecil? Because even if Cabs2cil on each file does produce at most one declaration (in addition to a definition), then maybe Mergecil leaves all the declarations?

In mergecilit is checked with hashmaps emittedVarDefn, and emittedVarDecls that no duplicate variable definitions and declarations are inserted. For functions, if the function is not static or inline, this is also checked with a hashmap emittedFunDefn. static functions are not explicitely merged, but from my understanding there should be no need to.

Definitions of inline functions are only merged when merge_inlines is true, and their function bodies (not looking at the function's name) are the same.

[jerhard]

The question thus is whether

• when merge_inlines is false, there can be multiple inline function definitions with the same name?
• when merge_inlines is true, there can be multiple inline function definitions with the same name, but different bodies?

[sim642]

From what I recall, duplicate inline functions, which are not merged, just get renamed with suffixes. At least I remember seeing large numbers of copies of inline functions in the HTML view of such programs.

[michael-schwarz]

From what I recall, duplicate inline functions, which are not merged, just get renamed with suffixes. At least I remember seeing large numbers of copies of inline functions in the HTML view of such programs.

Yes, I think that is the behavior when merge_inlines is false.

[michael-schwarz]

What is the status here? It would be nice to get this so we can merge #609 which will hopefully give a nice performance boost (that the students from our practical starting on Thursday could measure for instance.

[stilscher]

I created a small example to test the open questions that @jerhard posted above. It seems that the merger is not behaving correctly. If merge_inline is disabled a function definition and an inline function definition with the same name but in a different translation unit do not get merged but are not renamed either. This is also the case when merge_inline is enabled but the function bodies are not the same. I will take a look at the merger and try to fix it, in a way that multiple function definitions either get a unique name or are merged.

[jerhard]

If merge_inline is disabled a function definition and an inline function definition with the same name but in a different translation unit do not get merged but are not renamed either. This is also the case when merge_inline is enabled but the function bodies are not the same.

Does this already lead to problems with the current master branch? Do the changes in this branch cause additional problematic cases?