<html><head><meta http-equiv="Content-Type" content="text/html charset=windows-1252"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;"><div>Hi Edoardo,</div><div><br></div><div>What you are observing is something that is potentially easy to “fix”, but essentially requires additional domain-specific modeling in the static analyzer.</div><div><br></div><div>To understand what is going on, consider the following example:</div><div><br></div><div> void foo(int x) {</div><div> 1 / x;</div><div> }</div><div><br></div><div>In this example we have a potential division-by-zero. If ‘foo’ is analyzed in isolation, we don’t know anything about the value of ‘x’. We can do one of two things:</div><div><br></div><div>(1) Warn that ‘x’ could potentially be zero.</div><div><br></div><div>(2) Do not emit a warning, but register there was a division and that ‘x’ cannot be zero after the division, and keep analyzing.</div><div><br></div><div>In both cases the value of ‘x’ is unconstrained, so we can look at #1 and #2 as two potential default behaviors. In the analyzer we do #2. Essentially, although the value of ‘x’ is unconstrained, we don’t warn here. The rationale is that the analyzer would emit a huge number of false positives for integers that are possibly perfectly safe. We take the same tactic for pointers, who all could hypothetically could be null.</div><div><br></div><div>Instead, we take the strategy in the analyzer to flag bugs like null pointers and division-by-zero if we have evidence belief there may be a problem. For example, if a pointer is checked against null, we have evidence to believe that the pointer could be null. Similarly, there may be some APIs that we know could return a null pointer, and thus we can possibly track that information and see if a pointer coming from one of these sources is dereferenced.</div><div><br></div><div>The same tactic can be taken with integers and divide-by-zero. Let’s look at one of your examples:</div><div><br></div><div>void f_fscanf()<br>{<br> int data;<br> fscanf(stdin, "%d", &data); <br> /* POTENTIAL FLAW: Possibly divide by zero */ <br> printIntLine(100 / data);<br>}<br></div><div><br></div><div>After the call to ‘fscanf’ the analyzer tracks that ‘data’ binds to some symbolic integer value. That value is considered to be underconstrained, just like in my example above. In this example however, we could track some additional information that it came from an unsafe API like fscanf. This information is something *additional* that we would need to model, as we probably would not want to do this for any arbitrary API call. Modeling this might not be too hard. For example, the symbolic integer value does have some information associated with it to tell us where it originated; we could possibly use this to consult an API list to determine if the integer value should be treated as unsafe. We’d then modify the divide-by-zero logic in the analyzer to emit a warning if an under constrained integer came from one of these sources. We’d probably could conjure up something fairly ad hoc at first for a few specific cases, and then generalize it. A while ago we experimented with generalized taint analysis in the analyzer, which is something that would also possibly be useful here.</div><div><br></div><div>Does that answer your question? Essentially we need a little additional modeling in the analyzer for these APIs.</div><div><br></div><div>Ted</div><div><br></div><br><div><div>On Mar 9, 2014, at 9:17 AM, Edoardo P. <<a href="mailto:ed0.88.prez@gmail.com">ed0.88.prez@gmail.com</a>> wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite"><div dir="ltr">Ping?<br></div><div class="gmail_extra"><br><br><div class="gmail_quote">2014-02-20 22:25 GMT+01:00 Edoardo P. <span dir="ltr"><<a href="mailto:ed0.88.prez@gmail.com" target="_blank">ed0.88.prez@gmail.com</a>></span>:<br>
<blockquote class="gmail_quote" style="margin: 0px 0px 0px 0.8ex; border-left-width: 1px; border-left-color: rgb(204, 204, 204); border-left-style: solid; padding-left: 1ex; position: static; z-index: auto;"><div dir="ltr"><div><div>I forgot to add more info regarding the not detected int divisions:<br><br></div>the only correctly warned parts are for very simple cases, like this:<br>
<br></div>int x = 0; ... int y = 100 / x;<br>
<br><div class="gmail_extra">and the modulo variant. The other ones, which are not detected, assign x with:<br><br></div><div class="gmail_extra">- atoi (used when converting a string returned by socket functions or fgets)<br>
- fscanf<br>- rand<br></div><div class="gmail_extra"><br></div><div class="gmail_extra">And all the variants of such functions. The examples for fscanf and rand are simple:<br><br></div><div class="gmail_extra">fscanf variant:<br>
</div><div class="gmail_extra"><br></div><div class="gmail_extra">void f_fscanf()<br>{<br></div><div class="gmail_extra"> int data;<br></div><div class="gmail_extra"> fscanf(stdin, "%d", &data);
<br> /* POTENTIAL FLAW: Possibly divide by zero */
<br> printIntLine(100 / data);<br>}<br><br></div><div class="gmail_extra">rand variant:<br><br></div>void f_rand()<br>{<br> int data;
<br> data = rand();
<br> /* POTENTIAL FLAW: Possibly divide by zero */
<br> printIntLine(100 / data);<br>}<br><div class="gmail_extra"><br></div><div class="gmail_extra">in the test suite, rand is replaced with a macro, RAND_32(), defined as:<br><br>from testcasesupport/std_testcase.h:<br>
/* rand only returns 15 bits, so we xor 3 calls together to get the full result (13 bits overflow, but that is okay) */<br>#define RAND32() ((rand()<<30) ^ (rand()<<15) ^ rand())<br></div><div class="gmail_extra">
<br></div><div class="gmail_extra">(I'd truncate the first rand() to the first 2 bits before shifting it to 30th bit position, just to avoid overflow ...)<br><br></div><div class="gmail_extra">The 'itoa' case is more complex. Imho, the analyzer, before reporting the warning, should check that there can be a possibility that the string argument will be converted to 0. I hope it's possible with the current analyzer architecture...<br>
<br></div><div class="gmail_extra">Cheers,<br>Edward-san<br></div><div class="gmail_extra"><br></div><div class="gmail_extra"><div class="gmail_quote">2014-02-20 15:26 GMT+01:00 Edoardo P. <span dir="ltr"><<a href="mailto:ed0.88.prez@gmail.com" target="_blank">ed0.88.prez@gmail.com</a>></span>:<div>
<div class="h5"><br>
<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><div class="gmail_extra"><div class="gmail_quote"><div>Hi Lucas:<br> <br></div><div>
<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">I am doing today a script to run all test case in Juliet with Clang and<br>
generate a report (CSV file), when a finished this i will send you the<br>
results.</blockquote><div><br></div></div><div>Please do.<br> <br></div><div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">But a run manually and clang can find only 54 weaknesses in a<br>
total of 1476 files (into testcases/CWE369_Divide_by_zero, including s01<br>
and s02 directories).<br>
<div><br></div></blockquote></div><div><br>I can confirm that. In IRC I discussed with some llvm devs about the need to report
the float division by zero (Standard C/C++ says it's undefined behavior,
but Annex F implicitly allows it, thanks to IEEE 754). I have an idea: add a new static analyzer option which allows or disallows optional features, including the optional Annexes. That would help a lot imho.<br><br></div>
<div>Cheers,<br></div><div>Edward-san<br></div><div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
On Tue, 2014-02-18 at 16:19 +0100, Edoardo P. wrote:<br>
> Hi, Lucas, Jordan:<br>
><br>
><br>
> About the division by zero checking, I run this:<br>
><br>
><br>
> scan-build --use-analyzer /usr/bin/clang -o buildres/ clang -c -I<br>
> testcasesupport -DOMITGOOD<br>
> testcases/CWE369_Divide_by_Zero/s02/CWE369_Divide_by_Zero__int_zero_divide_01.c -o /dev/null<br>
><br>
><br>
> and I get the warnng:<br>
><br>
> testcases/CWE369_Divide_by_Zero/s02/CWE369_Divide_by_Zero__int_zero_divide_01.c:30:22: warning: Division by zero<br>
> printIntLine(100 / data);<br>
> ~~~~^~~~~~<br>
><br>
><br>
> So, Lucas, which file was failing for you?<br>
><br>
><br>
> Regarding the experience, here it is what I gathered till now:<br>
><br>
> I created a very huge file_list.txt, containing the source files to<br>
> compile (I used 'find -name *.c*' in the juliet directory), then<br>
> filtered away the 'main\.c', 'main_linux\.c' and 'testcasesupport'<br>
> files (grep -v), which have nothing to check, then I sorted the list<br>
> by CWE number (I had to do manual sorting because I couldn't manage to<br>
> sort, for example, CWE15_* and CWE114_* correctly).<br>
><br>
> Since I can't check for win32-only tests (I'm using linux), I filtered<br>
> them via 'grep -v w32' and 'grep -v wchar_t' (some tests require a<br>
> 'fopen'-like function with wchar_t string, which seems to be exclusive<br>
> to win32).<br>
><br>
><br>
> Regarding the per-translation-unit analysis, some files are, indeed,<br>
> separated sources for a program, so I didn't hesitate to filter them<br>
> with these patterns, according to the manual: "[abcdeBG]\.c" and<br>
> "good1" (last was associated with a 'bad' file, which was already<br>
> filtered).<br>
><br>
><br>
> With this file_lists.txt, I run the static analyzer only for the false<br>
> positives, with this command:<br>
><br>
> < file_list.txt xargs -n 1 scan-build --use-analyzer /usr/bin/clang<br>
> -disable-checker deadcode.DeadStores -o buildres/ clang -c -I<br>
> testcasesupport -DOMITBAD -o /dev/null > /dev/null 2> warns.txt<br>
><br>
><br>
> so, it checks all the files in the file list, saves the results in<br>
> buildres and reports the warnings in warns.txt file, ignoring the<br>
> DeadStores warns because they're reported a lot often.<br>
><br>
><br>
> Well, there are tons of false positives, caused by the flow variants<br>
> which involve global and static variables, shadow variables usage,<br>
> etc.<br>
><br>
><br>
> To the devs, I'd like to know which CWE are you interested, from the<br>
> list I attached on that email:<br>
> <a href="http://lists.cs.uiuc.edu/pipermail/cfe-dev/2014-February/035113.html" target="_blank">http://lists.cs.uiuc.edu/pipermail/cfe-dev/2014-February/035113.html</a> .<br>
><br>
><br>
> About the results, if I have more time, I'll post some of them.<br>
><br>
><br>
><br>
> 2014-02-18 2:05 GMT+01:00 Lucas Kanashiro<br>
> <<a href="mailto:kanashiro.duarte@gmail.com" target="_blank">kanashiro.duarte@gmail.com</a>>:<br>
> Thanks Jordan!<br>
><br>
> Could you leave me updated on the matter? I am so interested<br>
> in this,<br>
> and if it is necessary and possible i want to help to solve<br>
> the<br>
> potential issue.<br>
><br>
> Edward, can you tell us your experience with Clang and Juliet<br>
> Test<br>
> Suite?<br>
><br>
><br>
> On Mon, 2014-02-17 at 09:43 -0800, Jordan Rose wrote:<br>
> > Hi, Lucas. The analyzer currently runs a<br>
> per-translation-unit analysis, so it misses some bugs that<br>
> whole-program analysis may be able to catch. I'm guessing<br>
> that's the reason it's unable to catch this particular issue.<br>
> ><br>
> > In general, the analyzer is set for reasonably fast<br>
> turnaround (depending on the size of the project, of course),<br>
> so it also might not do a fully precise interprocedural<br>
> analysis if the state space gets too big. I'd have to see the<br>
> particular test case to tell what's going on here.<br>
> ><br>
> > I did see that Edward (CC'd) wanted to try bringing in the<br>
> Juliet Test Suite for the analyzer, but neither I nor Ted (the<br>
> lead on the analyzer) have gotten the chance to sit down and<br>
> look at what this would actually entail. It's possible he's<br>
> encountered similar issues, however.<br>
> ><br>
> > Jordan<br>
> ><br>
> ><br>
> > On Feb 15, 2014, at 5:58 , Lucas Kanashiro<br>
> <<a href="mailto:kanashiro.duarte@gmail.com" target="_blank">kanashiro.duarte@gmail.com</a>> wrote:<br>
> ><br>
> > > I am trying to running 'scan-build' in Juliet suite<br>
> testcase v1.2 (NIST<br>
> > > indication) to catch some bugs of 'Division by zero' (CWE<br>
> 369) and I<br>
> > > can't do it, the scan-build can't show me the existing<br>
> bugs. Did someone<br>
> > > try to do it yet?<br>
> > ><br>
> > > I have a doubt that scan-build can identify a bug of<br>
> division by zero in<br>
> > > this case (when parameter denominator is zero):<br>
> > ><br>
> > > int divide (int denominator) {<br>
> > > return 10/denominator;<br>
> > > }<br>
> > ><br>
> > > Can someone help me? Is this a deficiency of scan-build?<br>
> Can scan-build<br>
> > > identify the bugs in Juliet suite?<br>
> > ><br>
> > > Thanks in advance!<br>
> > ><br>
> > > --<br>
> > > Lucas Kanashiro Duarte<br>
> > > Engenharia de Software - FGA/UnB<br>
> > > <a href="mailto:kanashiro.duarte@gmail.com" target="_blank">kanashiro.duarte@gmail.com</a><br>
> > ><br>
> > > _______________________________________________<br>
> > > cfe-users mailing list<br>
> > > <a href="mailto:cfe-users@cs.uiuc.edu" target="_blank">cfe-users@cs.uiuc.edu</a><br>
> > > <a href="http://lists.cs.uiuc.edu/mailman/listinfo/cfe-users" target="_blank">http://lists.cs.uiuc.edu/mailman/listinfo/cfe-users</a><br>
> ><br>
><br>
> --<br>
> Lucas Kanashiro Duarte<br>
> Engenharia de Software - FGA/UnB<br>
> <a href="mailto:kanashiro.duarte@gmail.com" target="_blank">kanashiro.duarte@gmail.com</a><br>
><br>
><br>
><br>
><br>
><br>
> --<br>
> Mathematics is the language with which God has written the universe.<br>
> (Galilei)<br>
<br>
--<br>
Lucas Kanashiro Duarte<br>
Engenharia de Software - FGA/UnB<br>
<a href="mailto:kanashiro.duarte@gmail.com" target="_blank">kanashiro.duarte@gmail.com</a><br>
<br>
</blockquote></div></div><div><br><br clear="all"><br>-- <br>Mathematics is the language with which God has written the universe. (Galilei)
</div></div></div>
</blockquote></div></div></div><div><div class="h5"><br><br clear="all"><br>-- <br>Mathematics is the language with which God has written the universe. (Galilei)
</div></div></div></div>
</blockquote></div><br><br clear="all"><br>-- <br>Mathematics is the language with which God has written the universe. (Galilei)
</div>
</blockquote></div><br></body></html>