valid-memtrack analysis doesn't check sizes, only checks at end & doesn't consider locals

[sim642]

I started looking into allowing our SV-COMP valid-memtrack analysis to still consider one-past-end pointers to track memory for the rule change: https://gitlab.com/sosy-lab/sv-comp/bench-defs/-/merge_requests/471.
However, I am really confused because the memLeak analysis we use for that doesn't seem to check sizes anywhere.

It looks like our valid-memtrack analysis is unsound. For example:

//PARAM: --set ana.malloc.unique_address_count 1 --set ana.activated[+] memLeak
#include <stdlib.h>

int main(int argc, char const *argv[]) {
    int *p = malloc(sizeof(int));
    p += 1; // NOWARN (valid-memtrack not yet violated because one-past-end)
    p -= 1;
    p += 2; // WARN (valid-memtrack violated)
    p -= 2;
    free(p);

    return 0; //NOWARN
}

We don't warn about anything on this program, but there is a point where the allocated memory has no pointer to it (or one past the end).

[michael-schwarz]

As @mrstanb checked the other day: The usage of free already produces a warning when the offset is non-zero.
Why is this program a problem? We still have the pointer in some way?

Otherwise we need to check for each program point whether we still have a pointer to it and not just at the end.

Is it legal to C to even construct such a pointer?

[michael-schwarz]

The program you give is actually UB and can thus not appear in SV-COMP.

If both the pointer operand and the result point to elements of the same array object, or one past the last element of the array object, the evaluation shall not produce an overflow; otherwise, the behavior is undefined.

C11 Draft 6.5.6 (8)

[sim642]

The usage of free already produces a warning when the offset is non-zero.
Why is this program a problem? We still have the pointer in some way?

This isn't about the free at all. That just makes the program satisfy valid-memcleanup, but it still doesn't satisfy valid-memtrack at an intermediate point.

Otherwise we need to check for each program point whether we still have a pointer to it and not just at the end.

Yes, that's what valid-memtrack is about: whether all allocated memory is reachable at every point.

Is it legal to C to even construct such a pointer?
The program you give is actually UB and can thus not appear in SV-COMP.

Hence the property to find such UB. SV-COMP programs can contain UB if it's the UB that's supposed to be found by the verifier as a violation of the property. Otherwise valid-deref and valid-free wouldn't also be allowed to have any violating programs...

[michael-schwarz]

It's neither valid-deref nor valid-free though. The problem is constructing the pointer already.

[sim642]

The problem is constructing the pointer already.

And precisely constructing that pointer is the valid-memtrack violation by going out of the allowed bound. The valid-memtrack property definition is updated to exactly match the C standard to allow one-past-end to be valid.

[sim642]

I started looking into it, thinking perhaps one could just reuse bounds checking from memOutOfBounds analysis, but that lead me to another issue: memLeak analysis only looks for reachable things from globals, but everything pointed to by locals should also be considered reachable for the valid-memtrack property. Furthermore, everything pointed to by locals/parameters of outer call stack frames should also be considered reachable.

I'm very surprised that none of this unsoundness shows on sv-benchmarks. This perhaps reveals quite a shortcoming of sv-benchmarks tasks for valid-memtrack.

[michael-schwarz]

Hmm, that's interesting. I think when we implemented it, we considered the definition which explicitly limits the property to finite executions and not finite prefixes of executions.

More precisely: There exists no finite execution of the program on which the program lost track of some previously allocated memory.

This finite execution seems to be required for some of the properties in SV-COMP but not others, so one would think it has some meaning. But maybe it doesn't and it's just a historical artifact that some properties mention while others don't?

[sim642]

All the points above have nothing to do with finiteness though.

The reason valid-memtrack is an interesting property (not just in SV-COMP, but that's also what Valgrind and LeakSanitizer analyze) is because non-terminating programs (e.g. servers/control systems with infinte main event loops) would under valid-memcleanup be trivially non-leaky because they simply never terminate. But such non-terminating program may still allocate memory that it forgets to clean up. For such applications it's not possible to directly tell what memory has leaked and what's still around because some procedure hasn't finished yet. But unreachable memory has definitely leaked.

valid-memtrack doesn't require the analysis of termination at the same time (and we don't do that either). It's just saying that a counterexample is finite. The mention of finiteness is removed with the updated definition anyway.