Skip to content

Handle escaping of locals (after thread-creation/via globals) soundly #246

Closed
#686
Closed
Handle escaping of locals (after thread-creation/via globals) soundly#246
#686
Labels
bugunsound
Milestone
v2.0.0
@jerhard

Description

@jerhard
jerhard
opened on Jun 10, 2021

Goblint does not handle the case when a local variable escapes to another thread after the thread has been started.
A local may become reachable for a thread after the thread has been created, e.g. if the ego-thread stores its address in an object reachable from the parameters passed to the created thread.

The following is an example where this happens:

analyzer/tests/regression/37-escape/01-local-in-pthread.c

Lines 9 to 29 in 4be9ab0

void *foo(void* p){
sleep(2);
int* ip = *((int**) p);
printf("ip is %d\n", *ip);
*ip = 42;
return NULL;
}
int main(){
int x = 0;
int *xp = &x;
int** ptr = &xp;
int x2 = 35;
pthread_t thread;
pthread_create(&thread, NULL, foo, ptr);
*ptr = &x2;
sleep(4); // to make sure that we actually fail the assert when running.
assert(x2 == 35); // UNKNOWN!
pthread_join(thread, NULL);
return 0;
}

Metadata

Metadata

Assignees

No one assigned

    Labels

    bugunsound

    Type

    No type

    Projects

    No projects

    Milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions