False positive because of temporary variables

[Earnestly]

Potentially a false positive:

#include <stdlib.h>
#include <string.h>

struct Storage {
    char *a;
    char *b;
};

int
main(void)
{
    struct Storage storage = {0};

    char *message = "hello world";
    size_t length = strlen(message) + 1;

    storage.a = calloc(length, 1);

    if(storage.a)
        strncpy(storage.a, message, length);

    free(storage.a);
    return 0;
}

When running ikos on this source it produces:

ikos.c: In function 'main':
ikos.c:20:9: warning: pointer 'storage.a' might be null
        strncpy(storage.a, message, length);
        ^

I'm not sure why the analyser is concluding this if the strncpy is guarded by the preceeding if statement.

Any suggestions or clarification would be welcome.

Edit: This seems related to the https://github.com/NASA-SW-VnV/ikos/issues/80#issuecomment-453801815 about ikos not knowing the standard C library functions.

[arthaud]

Hi @Earnestly, Thanks for trying ikos.

This is indeed a false positive. This is similar to #94 and is due to temporary variables. The LLVM bitcode looks like:

char* tmp1 = storage->a;
if (tmp1 != NULL) {
  char* tmp2 = storage->a;
  strncpy(tmp2, message, length);
}

The analysis infers that tmp1 cannot be null, but doesn't relate tmp1 and tmp2.

I have 2 ideas that could fix this:

• Use an llvm pass to optimize away the second memory read, and remove tmp2
• Use a symbolic abstract domain to keep equalities between storage->a, tmp1 and tmp2. This needs to be very efficient so that it scales well. I think this is what Frama-C does.

[yakobowski]

I can confirm that this kind of code would trigger the equality domain of Frama-C/Eva. We are also helped by the fact that we control our front-end (which would not introduce temporaries here), but the equality domain solves the cases where temporaries are used (typically because they exist in the original code).

[arthaud]

Thanks Boris.

I would like to implement this in IKOS as well. I tried to read the source code of Frama-C before to understand how you implemented a bunch of things, but I got lost in the OCaml code.

[yakobowski]

Hi Maxime,

I forgot to answer to this message, sorry about that. The equality domain of Eva is in src/plugins/value/domain/equality. Feel free to ask high-level questions, I should still be able to answer :smile: (And I can always pass on low-level ones :sweat_smile: )

[arthaud]

Thank you @yakobowski, I will take a look at it.