SMACK does not catch freeing of stack locations as an invalid-free error

[zvonimir]

Here is a simple regression for this:

#include "smack.h"

int main(void) {
  int x = __VERIFIER_nondet_int();
  int *y = &x;
  free(y);
  return 0;
}

This regression should fail, and yet it passes. This is due to both stack variable allocation (alloc) and malloc being modeled the same way, mainly setting the Alloc array entry to allocated. Stack variable allocation should probably not do that.

[zvonimir]

My proposed fix is to keep track of stack allocation in a separate map. So instead of having just $Alloc we should probably have $HeapAlloc and $StackAlloc maps. Thoughts @michael-emmi and @shaobo-he?

[michael-emmi]

Would DSA-region merging be a problem in that proposal, e.g., when some variable may alias both with some local and some heap location?

[zvonimir]

Bumping this up since I would like to fix it since I think it might simplify some of our memory models.

@michael-emmi I thought about your comment above. I am not sure if what you said is true since we will still end up using the same memory map for aliasing pointers. So I think it'll still work. Could you maybe come up with a counterexample if you disagree? That would be helpful. Thx!

[shaobo-he]

Still reproduces on develop @ 9dca4d9. Running the program from the description with --check=valid-free:

--mem-mod	result
no-reuse-impls	verified
reuse	verified
no-reuse	verified

Under the full --check=memory-safety it does report an error, but for the wrong reason: $free decrements $allocatedCounter to -1 and the failure surfaces as valid-memtrack, not valid-free. That is the same mis-attribution #838 measures across the Juliet CWE590 families.

The diagnosis in the description is confirmed by the layout: $alloc (LLVM alloca, including ordinary locals and VLAs) draws addresses from the same $CurrAddr stream as $malloc, so a stack object satisfies every clause of $free's check — $base(p) == p, $Alloc[p], 0 < p — even though the comment at the top of share/smack/lib/smack.c describes A > 0 as the heap.

One nuance for whoever fixes this. Before #853 a zero-length VLA freed under the default model happened to be reported as an invalid free, but only because the size-zero alloca left its pointer unassigned. #853 makes it a real block, so it now behaves like every other stack object, i.e. like this issue. That removes an accidental detection rather than adding a new hole, and it is one more reason the underlying provenance distinction is the thing to fix.