Symbiotic does not correctly model zero-size realloc on valid pointers

[lzaoral]

Hi, POSIX says, that if realloc is called with a valid pointer and 0, one of the three cases must happen:

• realloc fails, NULL is returned and errno is set to ENOMEM -> original pointer is still valid,
• realloc succeeds and returns NULL,
• realloc succeeds and returns a valid zero-size pointer that shall not be dereferenced and must be later free'd.

Symbiotic does not consider the last case. The first case may be broken too, but I can't check that until #154 is resolved.

#include <errno.h>
#include <stdlib.h>

int main(void)
{
    void *ptr1 = malloc(sizeof(char));
    if (ptr1 == NULL)
        return EXIT_SUCCESS;

    errno = 0;
    void *ptr2 = realloc(ptr1, 0);
    if (ptr2 == NULL) {
        /* if realloc fails, it returns NULL and sets ENOMEM */
        if (errno == ENOMEM)
            free(ptr1);

        return EXIT_SUCCESS;
    }

    /* leak */
}

#include <errno.h>
#include <stdlib.h>

int main(void)
{
    void *ptr1 = malloc(sizeof(char));
    if (ptr1 == NULL)
        return EXIT_SUCCESS;

    errno = 0;
    char *ptr2 = realloc(ptr1, 0);
    if (ptr2 == NULL) {
        /* if realloc fails, it returns NULL and sets ENOMEM */
        if (errno == ENOMEM)
            free(ptr1);

        return EXIT_SUCCESS;
    }

    *ptr2 = 'A'; /* error */

    free(ptr2);
}

Output for the first example:

$ symbiotic --prp=memsafety 0059-test.c
7.0.0-dev-llvm-10.0.0-symbiotic:7aa510d4-dg:8fd21926-sbt-slicer:ce747eca-sbt-instrumentation:ff5d8b3f-klee:8340acee
INFO: Looking for invalid dereferences, invalid free, memory leaks, etc.
INFO: Starting instrumentation
wrapper: `which slllvm` failed with error code 1

INFO: Instrumentation time: 0.13282251358032227
INFO: Optimizations time: 0.05361819267272949
INFO: Starting slicing
[RD] error: no reaching definition for:   call void @free(i8* %22) #5, !dbg !40
[DU] error: no reaching definition for:   call void @free(i8* %22) #5, !dbg !40
INFO: Total slicing time: 0.05880928039550781
INFO: Optimizations time: 0.02026844024658203
INFO: After-slicing optimizations and transformations time: 2.8371810913085938e-05
INFO: Starting verification
b'KLEE: WARNING: undefined reference to function: __symbiotic_keep_ptr'
b'KLEE: WARNING: undefined reference to function: klee_make_nondet'
b'KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.'
INFO: Verification time: 0.3564143180847168
No error found.
NOTE: In the future, the result is going to be reported in SV-COMP format only with --report=sv-comp switch
RESULT: true
INFO: Total time elapsed: 3.4115078449249268

[mchalupa]

Interesting -- in this case the POSIX and man pages diverge. From man pages:

if size is equal to zero, and ptr is not NULL, then the call is equivalent to free(ptr).

Similarly, we do not model the case when malloc can return a non-null object that cannot be dereferenced. This needs to be fixed in KLEE.

[lzaoral]

By default man 3 realloc (that goes for other functions too) points to the documentation of given implementation of libc. The snippet you posted is relevant mainly for the GNU C Library. However, if you open man 3p realloc manual page, you get the documentation for POSIX.1-2008.

[kdudka]

... then the call is equivalent to free(ptr).

This obviously describes only the side-effect of the call, not its return value, because free does not return any value (unlike realloc).