Skip to content
Snippets Groups Projects
2011-12-05-Formidable-colleagues-patchlevels-and-new-features-in-Nitrogen.html 6.57 KiB
Newer Older
---
layout: post
author: Pascal Cuoq
date: 2011-12-05 21:45 +0200
categories: facetious-colleagues nitrogen value
format: xhtml
title: "Formidable colleagues, patchlevels and new features in Nitrogen"
summary: 
---
{% raw %}
<p>My colleagues are formidable. Over the last few days, three of them fixed four bugs in my code. And one of the fixes was a simple, obviously correct fix for the bug previously discussed <a href="/index.php?post/2011/11/23/Bug-in-Nitrogen">here</a>.</p> 
<p>In celebration of these terrific colleagues  here is a new patchset for Nitrogen 20111001  <a href="/assets/img/blog/imported-posts/patchlevel2">patchlevel 2</a>. It replaces patchlevel 1. I have tested it as thoroughly as the previous one  that is  I didn't even check if it applied cleanly to the Nitrogen tarball.</p> 
<p>Finally  with the aforementioned bugfix out the door  it is time to boast about another new feature available in Nitrogen: <strong>string constants</strong>. String constants are now properly treated as read-only: the program is not supposed to write there. If it does  an alarm is emitted  and for the sake of precision when analyzing the rest of the program  it is assumed that the write did not take place in the string constant. If the pointer could also point somewhere writable  then the write is assumed to take place there instead. If the pointer was only pointing to read-only or otherwise unwritable locations  the propagation ends for that state.</p> 
<p>If this seems a bit abstract  here is the same example as before  revisited:</p> 
<pre>char *p = "foo"; 
char c; 
char s = 'F'; 
void f(int u) 
{ 
  if (u) p = &amp;c; 
  *p = s; 
} 
</pre> 
<p>Treating <code>f</code> as the entry point of the program  the analyzer doesn't know what values may be passed for the argument <code>u</code>. Just before assigning to <code>*p</code>  it assumes that <code>p</code> may point to <code>c</code> or inside <code>"foo"</code>  but as the program tries to write to <code>*p</code>  it warns that <code>p</code> had better point somewhere writable  and since the user will of course make sure of that  it then knows that <code>p</code> points to <code>c</code>  and since <code>p</code> was pointing to <code>c</code>  it also knows that <code>c</code> contains <code>'F'</code> at the end of the function:</p> 
<pre>... 
bl.c:8:[kernel] warning: out of bounds write. assert \valid(p); 
... 
[value] Values at end of function f: 
          p ∈ {{ &amp;c }} 
          c ∈ {70} 
</pre> 
<p>One of the next steps will be to transform the "<code>p</code> points somewhere writable" condition before the assignment into "<code>u</code> is non-null" as a pre-condition of function <code>f()</code>  using weakest pre-condition computation. Quite a lot of effort remains before this works. For one thing  the value analysis does not yet distinguish between "valid for reading" and "valid for writing" in the ACSL predicates it annotates the program with (although it makes the distinction in the log messages).</p> 
<blockquote><p>Speaking of string constants  I should also mention that the value analysis in Nitrogen emits a warning for <code>"foo" == "foo"</code>. I already boasted about that <a href="/index.php?post/2011/06/04/Valid-compare-pointers">here</a>  but Nitrogen wasn't released at the time.</p> 
</blockquote> 
<p>This post was brought to you thanks to the formidableness of Philippe Herrmann  Virgile Prevosto  and Boris Yakobowski.</p>
 <p>My colleagues are formidable. Over the last few days, three of them fixed four bugs in my code. And one of the fixes was a simple, obviously correct fix for the bug previously discussed <a href="/index.php?post/2011/11/23/Bug-in-Nitrogen">here</a>.</p> 
<p>In celebration of these terrific colleagues  here is a new patchset for Nitrogen 20111001  <a href="/assets/img/blog/imported-posts/patchlevel2">patchlevel 2</a>. It replaces patchlevel 1. I have tested it as thoroughly as the previous one  that is  I didn't even check if it applied cleanly to the Nitrogen tarball.</p> 
<p>Finally  with the aforementioned bugfix out the door  it is time to boast about another new feature available in Nitrogen: <strong>string constants</strong>. String constants are now properly treated as read-only: the program is not supposed to write there. If it does  an alarm is emitted  and for the sake of precision when analyzing the rest of the program  it is assumed that the write did not take place in the string constant. If the pointer could also point somewhere writable  then the write is assumed to take place there instead. If the pointer was only pointing to read-only or otherwise unwritable locations  the propagation ends for that state.</p> 
<p>If this seems a bit abstract  here is the same example as before  revisited:</p> 
<pre>char *p = "foo"; 
char c; 
char s = 'F'; 
void f(int u) 
{ 
  if (u) p = &amp;c; 
  *p = s; 
} 
</pre> 
<p>Treating <code>f</code> as the entry point of the program  the analyzer doesn't know what values may be passed for the argument <code>u</code>. Just before assigning to <code>*p</code>  it assumes that <code>p</code> may point to <code>c</code> or inside <code>"foo"</code>  but as the program tries to write to <code>*p</code>  it warns that <code>p</code> had better point somewhere writable  and since the user will of course make sure of that  it then knows that <code>p</code> points to <code>c</code>  and since <code>p</code> was pointing to <code>c</code>  it also knows that <code>c</code> contains <code>'F'</code> at the end of the function:</p> 
<pre>... 
bl.c:8:[kernel] warning: out of bounds write. assert \valid(p); 
... 
[value] Values at end of function f: 
          p ∈ {{ &amp;c }} 
          c ∈ {70} 
</pre> 
<p>One of the next steps will be to transform the "<code>p</code> points somewhere writable" condition before the assignment into "<code>u</code> is non-null" as a pre-condition of function <code>f()</code>  using weakest pre-condition computation. Quite a lot of effort remains before this works. For one thing  the value analysis does not yet distinguish between "valid for reading" and "valid for writing" in the ACSL predicates it annotates the program with (although it makes the distinction in the log messages).</p> 
<blockquote><p>Speaking of string constants  I should also mention that the value analysis in Nitrogen emits a warning for <code>"foo" == "foo"</code>. I already boasted about that <a href="/index.php?post/2011/06/04/Valid-compare-pointers">here</a>  but Nitrogen wasn't released at the time.</p> 
</blockquote> 
<p>This post was brought to you thanks to the formidableness of Philippe Herrmann  Virgile Prevosto  and Boris Yakobowski.</p>
{% endraw %}