<html><head></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; "><div>Another big missing feature is reasoning about (linear) constraints between symbolic values. For example:</div><div><br></div><div> p = malloc(len);</div><div> if (i > len)</div><div> p[i] = ...</div><div><br></div><div>Right now we track range constraints on individual symbolic values (e.g., the values of 'i' and 'len' respectively), but don't track linear constraints between symbolic values. Doing so really is a prerequisite for doing interesting buffer overflow checking on arrays of dynamic size.</div><div><br></div><div>Tracking linear constraints between symbolic values would likely be a big win in the analyzer's overall precision, and not just useful for buffer overflow checking. Doing this would reduce down to implementing a new ConstraintManager (that possibly was built on the currently existing ones).</div><div><br></div><div><div>On Jan 18, 2010, at 11:34 PM, Zhongxing Xu wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite">Hi Chris,<br><br>The current clang static analyzer only has a basic array bounds checker (ArrayBoundChecker.cpp). Its function is very simple: whenever a location is visited, if it's an array element, compare its index with the size of the array. Some errors it can detect:<br>
<br>int a[4];<br>a[4] = 3;<br><br>and<br>int *p = malloc(12);<br>p[3] = 3;<br><br>That is, the current analyzer has the basic infrastructure for detecting out-of-bound array access.<br><br>The complexity of bounds checking arises from two facts: (may be there are others)<br>
<br>a. Many out-of-bound accesses occur in loops. Depending on the length of the buffer, it may require looping many times before triggering the out-of-bound access. But currently we only unwrap the loop for 2 or 3 times.<br>
<br>b. There are several string manipulation functions, such as strcpy(), strcat(). Currently we don't handle them. One simple way is to provide a fake implementation of them and inline them into the call site, and treat them as normal loops. Another way is to create some linear constraints over the arguments of them, and solve it. But this has complexity that we need to model the actual length of the string and the size of the array.<br>
<br>Some other projects includes integer overflow checking. This has not been implemented at all in clang.<br><br>Also inter-procedural analysis is required to enhance all other checks.<br><br><div class="gmail_quote">2010/1/19 Chris Hacking <span dir="ltr"><<a href="mailto:chacking@cs.washington.edu">chacking@cs.washington.edu</a>></span><br>
<blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">Hi all,<br>
<br>
I'm a student (part of a group of 3) looking for a project involving<br>
software engineering tools, preferably static analysis. I do a lot of work<br>
in C and have long felt that a static analysis tool for bounds checking on<br>
memory buffers (arrays/strings) would be very helpful. I saw that this was a<br>
requested feature for the Clang analysis tool, but there's very little info<br>
and it's apparently not fully developed yet. Therefore I have two questions:<br>
<br>
What is the state of bounds checking for C in the Clang analyzer, in terms<br>
of how far it has gotten and how much work is progressing on it?<br>
<br>
Is there another static analysis area that the Clang static analyzer needs<br>
implemented that would be a reasonable project for a few CS grad students?<br>
<br>
Thanks,<br>
Chris Hacking<br>
<br>
There's no place I can be,<br>
Since I found Serenity.<br>
But you can't take the sky from me.<br>
<br>
<br>
_______________________________________________<br>
cfe-dev mailing list<br>
<a href="mailto:cfe-dev@cs.uiuc.edu">cfe-dev@cs.uiuc.edu</a><br>
<a href="http://lists.cs.uiuc.edu/mailman/listinfo/cfe-dev" target="_blank">http://lists.cs.uiuc.edu/mailman/listinfo/cfe-dev</a><br>
</blockquote></div><br>
_______________________________________________<br>cfe-dev mailing list<br><a href="mailto:cfe-dev@cs.uiuc.edu">cfe-dev@cs.uiuc.edu</a><br>http://lists.cs.uiuc.edu/mailman/listinfo/cfe-dev<br></blockquote></div><br></body></html>