xr0-org / xr0

The Xr0 Verifier for C
https://xr0.dev
Apache License 2.0
173 stars 4 forks source link

Runaway recursion with pointer cycle #46

Closed jorendorff closed 4 months ago

jorendorff commented 4 months ago

xr0 should find a leak in this program:

#include <stdlib.h>

struct node {
        struct node *next;
};

struct node *f() ~[
    struct node *one;

        one = malloc(sizeof(struct node));
        one->next = one;
        return one;
]
{
    struct node *one;

        one = malloc(sizeof(struct node));
        one->next = one;
        malloc(1);  /* LEAK */
        return one;
}

Instead we get stack overflow. object_referencesheap and friends do not account for the possibility of cycles in the state graph.

Another test case that crashes this way is given below.

struct node {
    struct node *next;
};

struct node *f() {
    struct node one;

    one.next = &one;
        return &one;
}
akiarie commented 4 months ago

This is a really great spot. We've been meaning to change to a reference-counting based model for the leaks thing but haven't gotten the chance to yet.

I've put in a "circuit breaker" for now (see above branch); this will be added to the next release.

I've also added a couple of tests here and here based on your comment.

Please let us know if this doesn't address your concern before we close the issue (will do so in a couple of days).

jorendorff commented 4 months ago

Yes, this totally addresses the issue. :+1: