Support realloc

[JonasOberhauser]

No description provided.

[michaliskok]

Hi Jonas,

Thanks for all the issues you reported. I am currently working on some other aspects of the implementation so fixing all of them might take some time. If you would like me to prioritize some of them, please let me know.

As far as supporting realloc() is concerned, I was wondering whether you have any concrete test cases you would like to be supported. Wouldn't it be easier to simply allocate a large chunk of memory to begin with (for verification purposes) than using realloc()? Does any concrete algorithm that you have rely on realloc() being used?

The reason I am asking is because adding support for realloc() is a bit tricky. If the user requests a chunk of memory to be reallocated to a bigger one, then the newly allocated chunk needs to be initialized with the contents of the old (for offsets less than the old size of the file). But that means that we have to check how these offsets are manipulated after the initial malloc() call and use similar accesses for the initialization: we can't simply do a bytewise copy, as this would lead to mixed-size accesses, which the model does not currently support.

[JonasOberhauser]

Unfortunately, we are trying to verify dynamic arrays and some data structures that use them. Making sure that the code survives changing the pointers due to a realloc and so on is part of the verification, and we do need to copy the memory. The reason we would like to have an implementation of realloc in GenMC is that otherwise the client has to do the copying in a non-mixed size way, which means we need to reimplement a mock-realloc every time we use it for a different type.

However it's not a high priority at the moment.

As a side note, lack of mixed size accesses is the #1 pain point with GenMC at the moment, since they are very common in practice, both on racy and non-racy accesses. But at least to me it's not obvious how to extend GenMC to mixed-size accesses (efficiently).