SV-COMP: Check the `valid-memtrack` and `valid-memcleanup` properties

[RyanGlScott]

SV-COMP has two similar, but still distinct, properties called valid-memtrack and valid-memcleanup, neither of which Crux checks for at the moment. Here is how they are described in the SV-COMP 2021 rules:

• G valid-memtrack

  All allocated memory is tracked, i.e., pointed to or deallocated (counterexample: memory leak). More precisely: There exists no finite execution of the program on which the program lost track of some previously allocated memory. (Comparison to Valgrind: This property is violated if Valgrind reports 'definitely lost'.)

• G valid-memcleanup

  All allocated memory is deallocated before the program terminates. In addition to valid-memtrack: There exists no finite execution of the program on which the program terminates but still points to allocated memory. (Comparison to Valgrind: This property can be violated even if Valgrind reports 'still reachable'.)

What is the difference between the two? My understanding of the description above, as well as reading these SV-COMP mailing list posts, is that the following program would violate both properties:

#include <stdlib.h>

int *f() {
  int *x = malloc(sizeof(int));
  int *y = malloc(sizeof(int));
  x = y;
  return x;
}

int main() {
  int *x = f();
  free(x);
  return 0;
}

On the other hand, this program would violate valid-memcleanup but not valid-memtrack:

#include <stdlib.h>

int main() {
  int *x = malloc(sizeof(int));
  return 0;
}

The difference depends on whether one considers programs which have live variables that still point to un-freed memory upon exit to constitute a memory leak or not. valid-memtrack answers "no" to this question, whereas valid-memcleanup answers "yes" to this question.

Checking valid-memtrack is a prerequisite to competing in the MemSafety category of SV-COMP, while checking valid-memcleanup is a prerequisite to competing in the MemCleanup category.

[robdockins]

Conceptually, I think valid-memcleanup would be relatively easy. We just need to ensure at each program exit point that all (heap) allocations have been freed. I think the only slightly tricky thing is determining what, exactly, is meant by "program exit point." We might need to slightly rearrange how we handle the EarlyExit abort.

valid-memtrack is quite a bit tricker, as it is essentially a graph reachability question. Moreover, pinning down when and where the last live pointer to a memory region is dropped seems both difficult and expensive. If we only check for memory tracking at program exit, it might not be too bad, but it's not clear what kind of counterexamples will be accepted for this property.

[RyanGlScott]

Indeed, we might be able to fare better on valid-memcleanup than valid-memtrack. Nevertheless, it seems likely that Crux won't be able to handle a decent chunk of the programs in the valid-memcleanup category. Having re-read the 2021 contest report recently, this bit from the Verification Tasks section stood out to me:

Eliminating __VERIFIER_assume was more complicated: In some tasks for property memory-cleanup, __VERIFIER_assume(p); was replaced by the C code assume_cycle_if_not(p);, which is implemented as if (!p) while(1);, while for other tasks, __VERIFIER_assume(p); was replaced by assume_abort_if_not(p);, which is implemented as if (!p) abort();. The solution nicely illustrates the problem of the special semantics: Consider property memory-cleanup, which requires that all allocated memory is deallocated before the program terminates. Here, the desired behavior of a failing assume statement would be that the program does not terminate (and does not unintendedly violate the memory-cleanup property). Now consider property termination, which requires that every path finally reaches the end of the program. Here, the desired behavior of a failing assume statement would be that the program terminates (and does not unintendedly violate the termination property).

If I'm reading that correctly, then any program in valid-memcleanup which uses __VERIFIER_assume() will need a basic termination check, lest it falter when simulating while(1);.

[robdockins]

What a pain. Eliminating __VERIFIER_assume and __VERIFIER_assert was fundamentally a mistake, IMO.