On 01/21/2010 04:06 PM, Brian William Hackett wrote:
Resending finished email (grr... at email client).
----- Taras Glek<[email protected]> wrote:
The two errors I looked at, seem to be false positives
Hi, yeah, the great majority of these reports are going to be false positives
(I hope that was clear from the talk!). The trick here is that it should be
clear from the report where the tool got confused, and it should be easy to add
an annotation which the tool can use to check the assertion.
For both of these reports, the tool picked the wrong postcondition for a called
function, and in both the right postcondition is easy to specify.
Ok.
http://sixgill.org/firefox/write_overflow/ResolveSymlink_1244447419593944471.html
The first step the tool took for this access was pick the (wrong) postcondition
(__return< 4097) for PR_Read:
PR_IMPLEMENT(PRInt32) PR_Read(PRFileDesc *fd, void *buf, PRInt32 amount);
Adding __postcondition(return<= amount) will fix this report (the same
postcondition would have to be added to pl_DefRead due to its potential recursion,
this is an issue with the tool that needs to be fixed).
http://sixgill.org/firefox/write_overflow/EncodeString_3315072988729628109.html
Again, the first step the tool took was picking a wrong postcondition for
nsEncoderSupport::Convert.
nsresult nsEncoderSupport::Convert(const PRUnichar * aSrc,
PRInt32 * aSrcLength,
char * aDest,
PRInt32 * aDestLength)
This can be fixed with a precondition and postcondition describing this
interface:
__precondition(ubound(aDest)>= *aDestLength)
__postcondition(ubound(aDest)>= *aDestLength)
(An alternative would be __postcondition(*aDestLength<= initial(*aDestLength))
where initial indicates the value at function entry for a term. This isn't
supported yet though (would be easy to fix)).
Ok. Thanks for the examples. Can you assign the sixgill bug to yourself?
I think the way we will land this is by adding another build option to
Mozilla(similar to --with-static-checking flag).
Once we land this we will need to land annotations to fix the false
positives. These annotations would have to broken up into patches with
module-granularity. Generally that is done by filing individual bugs for
each component. Should set the bugs as depedent on 541220. Hopefully,
module-maintaines will help out.
Doing this is more work than using a bugfinder, a tool that guesses which
accesses are likely to be bugs. Once the code is annotated though, you get
strong guarantees (not airtight yet) that *all* the bugs have been found; with
a bugfinder you don't get anything. Also, improvements to the tool's inference
will reduce the need for annotations. In both the above cases it would not be
too hard to work on the tool to infer these and similar postconditions.
What would it take to be airtight? Is that even realistic?
Taras
Taras
_______________________________________________
dev-static-analysis mailing list
[email protected]
https://lists.mozilla.org/listinfo/dev-static-analysis
