I’m using AutoCorres, and one thing that just crossed my mind is: how do I check for memory safety (specifically the absence of a buffer overflow) in the heap model? Let’s say I have an array of 3 unsigned ints in C, i.e.:
unsigned int arr[3] = {1, 2, 3};
The resulting lifted_globals type will have an is_valid_w32 function, and I can use it to check the validity of pointer values at arr, arr + 1, arr + 2, etc. But, what prevents a function from writing to arr + 3 which is outside of the bounds of the declared array? Isn’t that still possible even with a validity check, since there can be a value at arr + 3 in the heap (of the same type)?
If you can prove that there is a valid value at arr + 3, then it is legal to write to that address. Not because of the array, but because of whatever argument you used to prove that there is a valid value there. How you access that valid value is not constrained.
(edit: depending on how you define memory safety, this does satisfy memory safety. It does not satisfy type safety, but C is not a type safe language, and the memory model is specifically designed to deal with type-unsafe but correct code)
I see. It is “correct” in terms of the low level memory model. I probably want to ensure that the array is only written to within its bounds by passing the array length somewhere and using that in a lemma / theorem - I think I saw this being done in some of the AutoCorres examples in the repo.
Thanks, just wanted some clarification on that.
No worries. If the code uses array subscripts, the parser (and therefore AutoCorres) will insert guards that force you to prove bounds, but if the access is via pointer arithmetic, the only recourse is memory validity.