Address reuse of malloc cannot be detected

[peterschrammel]

CBMC returns VERIFICATION SUCCESSFUL for the following program, although the assertion can fail.

void main()
{
  int *x = malloc(sizeof(int));
  free(x);
  int *y = malloc(sizeof(int));
  if(x == y) {
    // should be reachable
    assert(0);
  }
  free(y);
}

CBMC's object encoding assumes that malloc never returns the same address.

[kroening]

The equality check x == y is undefined behaviour.

[remi-delmas-3000]

The pointer comparison should be flagged as UB, but --pointer-checks does not catch this at the moment.

[feliperodri]

Is there any documentation with a list of all UBs that --pointer-checks covers?

[tautschnig]

May I elevate this to a discussion of the (absence of) tracking of object lifetimes? After all, addresses could only be reused when an earlier object at the same address has been freed (or gone out of scope). The following example (making use of knowledge of encoding internals) shows the other side of this, i.e., asserting that an object is accessible before its lifetime starts:

int *p;

void foo()
{
  int local;
  __CPROVER_assert(p == &local, "prepared pointer");
}

int main()
{
  p = 2ULL << ((sizeof(int*) - 1) * 8);
  __CPROVER_assert(__CPROVER_r_ok(p, sizeof(int)), "non-existent object is readable");
  foo();
}

This succeeds with cbmc --no-simplify (the combination of constant propagation and the simplifier picks out the integer value of the pointer, and then deems it to be out-of-bounds of the NULL object).

[jimgrundy]

There is a lot here.

• Comparison of pointers with different provenance is UB, but that doesn't give us a pass. It appears as if we have chosen a particular interpretation that makes this program correct.
• Certainly it looks like pointer comparison should generate the check that the compared pointers have the same object. Though it further confirms my feeling that we should not consider CBMC results sound unless pointer-checks are enabled.
• But what if we were to cast those pointers to long before doing the comparison, would we still know that the object ID test was required?
  I don't know that tracking object lifetimes would solve this would it (though it might solve other problems)? It seems like even if the object above was live at the time of the assertion we should still have a problem because we have manufactured a pointer in an illegal way.

[remi-delmas-3000]

we need to decouple the identity of an allocation from the address at where it lives

[jimgrundy]

There is a long-term fix we need to contemplate that involves a richer model of pointers and malloc such that malloc can reuse previous freed addresses. This addresses Remi's point that

we need to decouple the identity of an allocation from the address at where it lives

But for now, there is a bandaid that we need to apply to limit the soundness bleed that leverage's Daniel's comment that

The equality check x == y is undefined behaviour

Pointer comparisons (==, <, <=, >, >=, !=) are UB for pointers with different provenance. Pointer values with different object-bits in CBMC have different provenance, so we could implement a check on all pointer comparisons that the object bits of the compared pointers match. That would improve the situation here because with --pointer-checks enabled (which should become the default in the next major release) the program in this issue would fail verification (because the pointer check would fail).

This is not a complete solution. You might be able to get around this by casting the pointers to integers before comparing. You might get around this by comparing them with XOR rather than ==, but we would catch more errors and reduce the risk of unsoundness. This should be fairly easy to do, so we should do it soon.