> But in this model, how can you implement malloc?

This is not about runtime implementation, it's about how the compiler reasons about pointers to allocated memory on a symbolic level. It just means the compiler would consider all memory accessed through the pointer (and other pointers computed from it) other than the pointed (allocated) memory block to be undefined.

Even if this was about runtime behavior, a basic malloc would fulfill this requirement with no changes. It returns a pointer to the allocated block and this pointer itself is the "memory block ID".

So absolutely no change, with a reasonable assumption that successive allocations (without freeing in between) always return a different pointer. The compiler could simply generate fat pointers with allocation base address + offset to actual location.

This is an extremely good question, and I do not have a satisfying answer. Note that `malloc` is special in the C standard as well, and AFAIK it is not possible to implement `malloc` in standard C at all.

Heck, there are several models of C out there where you cannot implement `memcpy`.

Hmm. My answer would be “you don’t, unless you are willing to accidentally give stronger guarantees”. I believe that standard C11 permits a function to allocate malloc-style from a big static arena of type array of char. You can even implement free() and reuse the memory. But then all the allocations are really pointers into the arena, and certain operations that should be UB aren’t if you use this type of malloc.

But then you throw something like __attribute__((malloc)) on it, and define that as transforming the return value into a new Pointer that is in a different, fresh allocation. And you declare that access to the range of the arena in use is UB until free() gets called.

I don’t know how well this fits into the formalism, but I think that a complete formal memory model would need to understand that free() is permitted to treat its argument as a pointer into a large array of char, but that free()’s caller is not.

> Note that `malloc` is special in the C standard as well, and AFAIK it is not possible to implement `malloc` in standard C at all.

malloc() is usually implemented in C [0] and to be honest I'm not sure why do you think it wouldn't be? Of course you need OS API calls to actually get some memory (unless you want to operate on statically defined memory buffer) but well it's still C.

[0] https://github.com/lattera/glibc/blob/master/malloc/malloc.c

It's C, but it's not standard C. It uses implementation defined behavior. Every compiler has some implementation defined behavior because they would be much less useful without it.

That linked implementation relies on OS primitives (sysmalloc()), implemented in C, Assembly or whatever was used to write the OS.

Try to implement malloc() on bare metal, without using either Assembly or language extensions.

You can't implement malloc in standard C, but there is no actual C compiler that implements only standard C and provides no other guarantees. There is always implementation defined behavior in addition to what the standard defines.

On Linux, compilers will ensure that you can make system calls to the kernel such as brk[1] or mmap[2] which will let you allocate larger chunks of memory that malloc can split up and give out. On Windows, you will have access to Windows APIs which will let you use VirtualAlloc[3] to do the same.

[1] http://man7.org/linux/man-pages/man2/brk.2.html

[2] http://man7.org/linux/man-pages/man2/mmap.2.html

[3] https://msdn.microsoft.com/en-us/library/aa366887(VS.85).asp...

By having malloc take an allocation from a lower-level allocator and hand out pieces of that. The lower-level allocator (mmap or -- historically -- brk) is a primitive, implemented as a syscall.

One option: Just go further up the chain. Malloc is going to be implemented (probably) using mmap/VirtualAlloc/whatever, just teach the system about those native calls as allocations.

(This probably is not a satisfying resolution there, since it's likely impossible to enumerate all the primitive memory allocation functions)