Incompleteness with uninitialized pointer fields in dynamic objects

[kenmcmil]

CBMC version: 5.15.0
Operating system: MacOS
Exact command line resulting in the issue: cbmc --trace --unwind 10 test2.c
What behaviour did you expect: Assert "test" is valid
What happened instead: Assertion "test" was violated

File test2.c:

struct list {
  struct list *next;
};


int main() {
  struct list *a = malloc(sizeof(struct list));
  struct list *b = malloc(sizeof(struct list));
  struct list *p;
  struct list *q;
  __CPROVER_assume(p == a);
  __CPROVER_assume(p->next == q);
  __CPROVER_assume(q == b);
  __CPROVER_assume(q->next == 0);
  __CPROVER_assert(p->next->next == 0,"test");
}

[kenmcmil]

Here's a slightly simpler example. The following program gives a violation of assert "test":

struct list {
  struct list *next;
};


int main() {
  struct list *a = malloc(sizeof(struct list));
  struct list *b = malloc(sizeof(struct list));
  struct list *q;
  __CPROVER_assume(a->next == q);
  __CPROVER_assume(q == b);
  __CPROVER_assume(b->next == 0);
  __CPROVER_assert(a->next->next == 0,"test");
}

On the other hand, this program gives SUCCESS:

struct list {
  struct list *next;
};


int main() {
  struct list *a = malloc(sizeof(struct list));
  struct list *b = malloc(sizeof(struct list));
  struct list *q;
  __CPROVER_assume(q == b);
  __CPROVER_assume(a->next == q);
  __CPROVER_assume(b->next == 0);
  __CPROVER_assert(a->next->next == 0,"test");
}

The only difference is reordering of two assumes.

[martin-cs]

Thank you for this report and the examples. Re-ordering like that really shouldn't change the result, you are correct. Can you try with --pointer-check enabled? Uninitialised pointers are always a bit of a murky area.

[kenmcmil]

Same result with --pointer-check. The dereference checks all pass but assertion "test" fails.

[kroening]

This isn't expected to work -- C has a concept of 'pointer provenance'. Take a look at this:
https://www.cl.cam.ac.uk/research/security/ctsrd/pdfs/201901-popl-cerberus.pdf

[kenmcmil]

Well, according to C semantics, even in the version that works, the comparison q==b is undefined, since q is uninitialized. My understanding is that CBMC extends the C semantics for the convenience of writing tests. It's plausible that the CBMC semantics should allow this program, since both a->next and q get non-deterministic values. For context, the assumes in this example come from the precondition of a function.

In any event, there is the question of why the second version passes. If it's not an incompleteness, it's an unsoundness.

[kenmcmil]

Here's another way of looking at the question. Suppose I wanted to verify this C function:

void fun(struct list *a, struct list *b, struct list *q) {
    if (a->next == q)
        if (q == b)
            if (b->next == 0)
                __CPROVER_assert(a->next->next == 0,"test");
}

How should I write a test harness for this?

[kenmcmil]

Here's another program that fails:

struct list {
  struct list *next;
};

struct list *foo(struct list *foo);
    

int main() {
  struct list *a = malloc(sizeof(struct list));
  struct list *b = malloc(sizeof(struct list));
  struct list *q = foo(a);
  a->next = foo(a);
  __CPROVER_assume(a->next == q);
  __CPROVER_assume(q == b);
  __CPROVER_assume(b->next == 0);
  __CPROVER_assert(a->next->next == 0,"test");
}

This makes me think the issue is not pointer provenance. Since pointers q and a->next are assigned from an external function, the compiler can't use alias analysis to optimize away the evaluation of a->next->next.

[kroening]

The feature "nondeterministic pointer" simply does not exist -- pointers only work when they are initialized with an address of an object.

[kenmcmil]

Is it possible that the order of assertions is affecting the points-to analysis?

Non-deterministic pointers would be quite useful for certain purposes. Suppose I wanted to modify pointer dereferencing so that an unknown pointer could dereference to any object in the state. Would I do that in value_set_dereference.cpp?

[kenmcmil]

Here's another example that makes me think the issue might be points-to analysis. This program passes, with --pointer-check:

struct list {
  struct list *next;
};


int main() {
  struct list *a = malloc(sizeof(struct list));
  struct list *b = malloc(sizeof(struct list));
  struct list **r = &(a->next);
  __CPROVER_assume(*r == b);
  __CPROVER_assume(b->next == 0);
  __CPROVER_assert(a->next->next == 0,"test");
}

At the first assume, we now that r points to a-> next, so we can infer that a->next points to b. Similarly, in the second program of the two above, we first infer that q points to b, and then that a->next point to b. Whereas in the first program, from a->next == q, we infer that q points to a->next, but then from q == b we infer nothing about a->next.

So I am not convinced that nondeterministic pointers don't exist. They're just a bit abstracted by the points-to analysis.

By the way, here is another program that passes with --pointer-check:

int main() {
  int x = 0;
  int *p;
  int y;
  if (p == &x) {
    y = *p;
    __CPROVER_assert(y == 0,"test");
  }
}

This is actually an unsoundness, since a compiler may treat the condition as undefined.

[mww-aws]

This is interesting. There are some asymmetries here. Obviously one can assert pointers are equal, but it is not possible to assume pointers are equal.

For Ken's "another way of looking at it" example, unless explicit assignments are made for the "next" pointers, then it is not even possible to compare for equality, as the dereference of the pointers leads to pointer check failures. One must force an assignment of "next" pointers to valid pointers of some kind to evaluate the program. If you do this, then it works passably well, but I need to think about what I would like the behavior to be in this case. Usually I am happy with something that flags potential bad code, even if conservative, which is what the current code is doing.

[kenmcmil]

But to be clear, in the examples above the pointer check pass, even though the pointers are not initialized. Only the assertions fail, because of the imprecise semantics of pointer dereference.