Account for allocated heap memory which is unreachable from globals

[mrstanb]

This PR:

• Adds a refinement to the reporting for valid-memtrack
• We now warn whenever there's allocated heap memory at program exit which is not reachable from the global program vars

Some notes:

• The SV-COMP rule for valid-memtrack states: All allocated memory is tracked, i.e., pointed to or deallocated. Hence, for now I've kept the setting of the global SV-COMP flag for InvalidMemTrack also for the case of not calling free on allocated heap memory (not necessarily only referenced by global vars). I'm open for a discussion here if you think we could improve on that as well
• There are some false positives for heap memory, reachable through local variables in case it's not freed (I also described this in test 76/09):

int main(int argc, char const *argv[]) {
    g = malloc(sizeof(int));
    g = NULL;
    int *p = malloc(sizeof(int));

    return 0; //WARN
}

In the above example, p's memory is leaked (missing free), but it's also reported as unreachable (because it's not reachable via the globals, but only via a local var). Should we try to improve on that (maybe at least in the error reporting for the unreachable-from-globals-memory case) or are we ok with it as is?

Sidenote:

• Added 76/08 and 76/09 as new test cases

TODOs:

• If earlyglobs is activated, then abort the analysis

[michael-schwarz]

Thank you for the PR!

In the above example, p's memory is leaked (missing free), but it's also reported as unreachable (because it's not reachable via the globals, but only via a local var). Should we try to improve on that (maybe at least in the error reporting for the unreachable-from-globals-memory case) or are we ok with it as is?

Confusingly this is exactly the definition of valid-memtrack in SV-COMP (I was also surprised by this). See e.g.: https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/merge_requests/1464
So we cannot really improve here and actually need to report this as a violation of valid-memtrack.

[michael-schwarz]

I will start a run with the two suggestions from above applied to see what the results are.

[michael-schwarz]

With these two suggestions on top of #1234, we succeed on an additional 17 tasks:

Statistics:           3862 Files
  correct:            1175
    correct true:     1175
    correct false:       0
  incorrect:             0
    incorrect true:      0
    incorrect false:     0
  unknown:            2687
  Score:              2350 (max: 5857)

[michael-schwarz]

Tables: results.2023-11-08_10-02-03.zip

[mrstanb]

Confusingly this is exactly the definition of valid-memtrack in SV-COMP (I was also surprised by this). See e.g.: https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/merge_requests/1464
So we cannot really improve here and actually need to report this as a violation of valid-memtrack.

I see, thanks for the clarification! It's a bit confusing, indeed. In this case I'll leave the reporting of this violation as is.

[mrstanb]

I added some changes regarding the check of whether some memory is still transitively reachable via the points-to set of a global struct variable (both of pointer and non-pointer type), as well as its fields and the contents of the points-to sets.

I also added two new regression test cases to check if the changes make sense (cf. 76/{13, 14}).

[mrstanb]

Maybe we should add a check that if earlyglobs is activated, then we should abort the analysis?

Iirc, we discussed with @jerhard that earlyglobs would stop us from obtaining meaningful information about what global vars can reference.

[michael-schwarz]

Maybe we should add a check that if earlyglobs is activated, then we should abort the analysis?

I don't think we use earlyglobs in sv-comp, so this doesn't seem too pressing.

[sim642]

I may have missed this, but in what sense are global structs special? As in, why aren't we also considering the contents of global arrays and whatnot?
Or are we just less precise for global array contents then?

[mrstanb]

I may have missed this, but in what sense are global structs special? As in, why aren't we also considering the contents of global arrays and whatnot?
Or are we just less precise for global array contents then?

I'm not really sure about arrays, because I haven't worked a lot with the array domain of Goblint and so I can't express an opinion on that.

I've thought about global unions, however I'm unsure about what should happen in a situation like the following. Consider:

typedef union {
    int i;
    char *str;
} un;

un *glob_var;

int main() {
    ...
}

What happens if the program first accesses str of glob_var and then subsequently accesses i of glob_var? Wouldn't str be "lost" so to speak? I mean the memory is there, but i is the thing that's now occupying the place of str, unless I'm thinking in the wrong direction.

[michael-schwarz]

Yeah, unions do not seem to be a good candidate here. We discussed the issue of arrays at our Gobcon yesterday, and decided that due to the abstraction we use for arrays, it is unlikely that things are must-reachable from arrays and have thus decided against implementing dedicated support for it for now.

[sim642]

We then need to explicitly limit the filtering to structs though. CIL's TComp represents both structs and unions.

[michael-schwarz]

I think we can now merge this into master as well? Wdyt @sim642?