A might be uninitialized message after being initialized

[Ganton]

Dear NASA IKOS people,

First of all, thanks your good work.

When people read https://ntrs.nasa.gov/api/citations/20190032510/downloads/20190032510.pdf or https://ntrs.nasa.gov/api/citations/20220007431/downloads/SWS_TC3_IKOS_Tutorial.pdf , tries its example:

    int tab[10];
    for (int i = 0; i < 10; i++) {
        tab[i] = i * i;
    }

and (at the end) adds a simple

    tab[2] = tab[1];

people get a

    warning: expression 'tab[1]' might be uninitialized
    tab[2] = tab[1];

Thanks again for the good work!

[arthaud]

Hi @Ganton,

This is a known limitation of ikos. The uninitialized variable checker can cause many false positives, I usually recommend to disable it.

For more context, this is because ikos uses abstract interpretation under the hood, which enables us to compute an over-approximation of all reachable states. The loop invariant we currently infer is: for all i, tab[i] is either uninitialized or is between [0, 9*9]. When we exit the loop, we are not able to refine that invariant to infer that all elements are initialized. This could be fixed with a custom abstract domain - something called array slicing or array smashing IIRC? For instance, we need to infer that: at iteration i, for all j with 0 <= j < i, tab[j] is initialized so we can infer the right constraint when i = 10 at the end.

[ivanperez-keera]

Is this something that it's actionable at this point or would it require a fair amount of investigation before we could implement it? If the latter, I'd like to move it to "Discussions > Ideas" to keep the issues for those things we are actively planning to solve. Thanks!

[arthaud]

It is actionable, I have a pretty concrete idea on how to implement that, but obviously it's a good amount of work (maybe a week, or more? hard to say, it might impact many APIs). Right now we have an abstract domain for each information (nullity, numerical, initialization, etc.). Those are grouped together using a domain product, see:
https://github.com/NASA-SW-VnV/ikos/blob/master/core/include/ikos/core/domain/scalar/composite.hpp#L131-L141
The problem is that we cannot infer "relations" between them, i.e "x is uninitialized OR between [0, 10]". If x may be uninitialized, it is necessarily TOP in all the other domains. This is because our domains cannot represent "x doesn't have any value" without setting the whole domain to bottom (i.e the unreachable state).
We could build another abstract domain which is weakly relational so we could represent "uninitialized OR X".

[ivanperez-keera]

Related: #138.