Soundness bug with unconstrained pointers

[qaphla]

The handling of writes to unconstrained pointers treats all writes, regardless of offset, as writing to a single object. This can result in soundness issues. See, for example, the following program, which CBMC verifies:

#include <assert.h>

void main()
{
  int *x;
  x[0] = 1;
  x[1] = 2;
  assert(x[0] == 2);
}

While unconstrained pointers are unlikely to occur in actual C code, some goto-instrument passes (in particular, the code-contracts passes) create unconstrained variables for checking purposes, and are unsound as a result of this issue.

[kroening]

The unsoundness is fixed by giving the --pointer-check option to CBMC. This option should become default at some point.

For contracts, you will need to be able to express a precondition that requires a pointer to point to something. This feature is yet to be implemented.

[martin-cs]

Thanks for the bug report. Uninitialised / unconstrained pointers are always an issue as it is far from clear what the semantics should be. For example, if you have typedef struct _tree { int label; struct _tree *left, struct _tree *right} tree; and are verifying a function int search (tree * root), should root->value work? What about root->left->value? Is it different to root->right->value? Is it possible to have root->right->right == root->right?

Our current approach to handling this is to ask users to build a calling context that constructs what they think are valid memory configurations. This could be automated to some degree but it would likely require many SAT calls and something like Cristina's small model property for heaps.

[esteffin]

Adding --pointer-check as default parameter to CBMC has been proposed to be part of version 6 here #7975.

Adding contracts support to express a precondition that requires a pointer to point to something has to be addressed separately, so it will be left out of version 6.