smack cannot find this type of memory error

[ya0guang]

We tried to use smack in our research project to find memory errors. But when I was testing the functionality of smack for finding memory errors with flag "--memory-safety", I found smack cannot detect this type of memory error. In function foo1, a is a local variable and should not be pointed outside of foo1. I believe smack should be able to find this kind of invalid pointers. By the way, can I know what kind of memory errors can be find by smack? I checked test folder but I'm not sure if that's complete, and your papers of smack seems mentioned little about its ability to find memory errors. I'll be happy to contribute to the memory safety module after I'm familiar enough with smack if you don't have time to add a function for finding such errors.

#include<stdlib.h>
#include<stdio.h>

static int *p = 0;

void foo1(){
    int a = 1;
    p = &a;
}

int main(){

    foo1();

    printf("the pointer p in foo1 points to: %d\n", *p);
    printf("value of the pointer p in foo1: %p\n", p);

    return 0;
}

[zvonimir]

Thanks for reporting this. Yes, one of the current drawbacks of SMACK's memory safety checking is the fact that it cannot catch certain types of memory errors that are related to stack pointers. Your example hits one of these corner cases. We will look into potentially adding support for catching these kinds of errors as well.

[zvonimir]

One potential fix is to keep track of everything that gets allocated via alloca instruction. Then, all such objects should be freed before every return.

[shaobo-he]

One potential fix is to keep track of everything that gets allocated via alloca instruction. Then, all such objects should be freed before every return.

I wonder if this kind of memory errors can be ruled out by DSA. Intuitively, a pointer to stack variable should not be able to alias with pointers whose context is above its. For this example, &a whose context is foo1 and aliases with p whose context is ``top''. Of course, when there are recursions or SCCs in the call graph, things get tricky, but I wonder it happens in real world code.