Model realloc

[shaobo-he]

Memory reallocation is used by rust libraries (e.g., vec). We need to model it properly.

[michael-emmi]

Is it possible to write a C-language test case for this?

[zvonimir]

@Guoanshisb (Shaobo): Please write a simple C program that uses realloc, which we can use to debug this.
@michael-emmi : To model realloc, we most likely need $Size to be present in all memory models. The pull request related to memory safety is supposed to do that. I just provided feedback to that pull request. I will stay on top of it this time around and try to merge it soon. Then we can take care of realloc.

[keram88]

Simple tests for correct realloc behavior. Attached as a .txt file since github rejects .c files.
realloc_simple.txt

[shaobo-he]

This issue has been resolved: we model realloc as free-then-malloc.

[zvonimir]

Has Mark's program been added to our regressions?

[shaobo-he]

Has Mark's program been added to our regressions?

No, SMACK reports an error for Mark's program as we don't model copying in realloc.

[zvonimir]

Could we update the model to include copying as well?

[shaobo-he]

Could we update the model to include copying as well?

This might be very tricky since we have to keep track of the memory associated with the base pointer.

@keram88 thoughts?

[shaobo-he]

A concrete instance of what is missing, found while auditing #853.

share/smack/lib/stdlib.c models realloc as free(ptr); malloc(size), which does not preserve the old block's contents. C11 7.22.3.5p2 requires them up to the smaller of the two sizes, so a legal program is reported buggy:

#include "smack.h"
#include <stdlib.h>
int main(void) {
  char *p = malloc(4);
  p[0] = 42;
  char *q = realloc(p, 8);
  __VERIFIER_assert(q[0] == 42);   // guaranteed by 7.22.3.5p2
  free(q);
  return 0;
}

smack i161.c --check assertions memory-safety --verifier=corral reports an error under all three memory models, on develop @ 9dca4d9 and on #853 alike.

The two boundary cases are now settled by the allocation model rather than by realloc itself, and #853 documents them in a comment on the function: realloc(NULL, n) is malloc(n) because free(NULL) is a no-op, and realloc(p, 0) frees p and returns a size-zero block that must itself be freed. What remains for this issue is the copy.