Frama-C news and ideas

To content | To menu | To search | Frama-C Home

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.

Comments

1. On Wednesday, November 23 2011, 15:09 by Sylvain

Why not offer a nightly snapshot to "non-industrial" users?

2. On Wednesday, November 23 2011, 16:31 by pascal

Hi, Sylvain.

A line needs to be drawn somewhere. If we make nightly snapshots available, people will ask questions and file (bad) bug reports against them, even if we recommend they don't. So we could make these snapshots available and force ourselves to ignore questions and reports, but with the resources we have, it will leave a better impression overall not to make snapshots available at all.

Besides, it is difficult enough for these industrial users to justify to their respective managers that they need support for freely available software their company never decided to buy a license for. There needs to be some perks to justify the expense. Access to the SVN and development mailing list are some of these perks in addition to the actual support.