Bug in Nitrogen's value analysis

In the course of restructuring the value analysis, I noticed a difference in some regression tests. The \after" version had some new warnings that weren't in the "before" version. After further investigation it turned out that displaying the warnings was correct and that the "before" version was unsound.

This soundness bug is particularly hard to reproduce even if you know it's there. I am still pondering whether to back-port the fix to the released Nitrogen version because it basically means back-porting the internal architecture change not the kind of small obviously uniform improvements I like to release as post-release patches.

The bug appears in this example program:

char *p = "foo";
char c;
char s = 'F';
void f(int u)
{
  if (u) p = &c;
  *p = s;
}

Here is the entire output of an analysis with Nitrogen:

$ ~/nitrogen-20111001/bin/toplevel.opt -val t.c -main f
[kernel] preprocessing with "gcc -C -E -I.  t.c"
[value] Analyzing a complete application starting at f
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
        p ∈ {{ &"foo" }}
        c ∈ {0}
        s ∈ {70}
[value] Recording results for f
[value] done for function f
[value] ====== VALUES COMPUTED ======
[value] Values for function f:
          p ∈ {{ &c }}
          c ∈ {70}

Here is the output of today's version. Can you spot the difference?

[kernel] preprocessing with "gcc -C -E -I.  t.c"
[value] Analyzing a complete application starting at f
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
        p ∈ {{ &"foo" }}
        c ∈ {0}
        s ∈ {70}
t.c:8:[kernel] warning: out of bounds write. assert \valid(p);
[value] Recording results for f
[value] done for function f
[value] ====== VALUES COMPUTED ======
[value] Values for function f:
          p ∈ {{ &c }}
          c ∈ {70}

In Nitrogen the value analysis sees that it is illegal for p to point to literal string "foo" since *p is used for writing. It deduces that the value of p can only be &c and that the assignment of 'F' (ASCII code 70) can only take place in c and that the final value of c is therefore necessarily 70 but it forgets to emit the alarm stating that p must not point to "foo". The current development version follows the same reasoning but remembers to emit the alarm.

In order to observe this bug it is necessary to shape *p = ...; as an lvalue to lvalue assignment (*p = 'F'; does not produce the bug). Lvalue to lvalue assignments are handled specially in order to enable precise results on struct assignments and memcpy() of addresses.

Besides the bug only occurs with pointers to literal strings or to arrays that are automatically allocated when the analysis entry point takes pointers in arguments — but the creation of these arrays is not documented in enough detail for users to realize there is a bug in this case.

Lastly if in the example p pointed only inside the literal string then the illegal write access would be even more obvious (since there would be no location for the write to happen) and the alarm would be emitted (that is the bug wouldn't occur).

Industrial users with SVN read access can simply use today's version where the bug is fixed.

Sometimes I wish the value analysis only propagated intervals. It would have simpler bugs then.