<div dir="ltr">I think it is a good idea improve it by the GSoC 2014 Edward! This can speed development and put in conform static analyzer with NIST nomenclature.<div><br><div><br><div><br></div></div></div></div><div class="gmail_extra">
<br><br><div class="gmail_quote">2014-03-11 8:47 GMT-03: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:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Hi Ted,<br>
<br>
Thank you for your answer.<br>
<br>
If I got it right, the parameter variables of a certain function,<br>
cannot be constrained until inside the TU (I hope we can manage to<br>
analyze together two or more TU) there's a call to such function<br>
somewhere else and the arguments are constrained.<br>
If we get a function call and we don't have the declaration of such<br>
function or it's inside another TU, we can't tell anything regarding<br>
the parameters or the global variables (is it possible for a function<br>
declared in another TU access to a static variable from another TU?),<br>
which might change, but for the stl functions, we know how they work,<br>
hence we can choose between:<br>
1)"inject" inside the TU their "generic" declarations (I wonder which<br>
functions are OS-dependent...) and make it parse,<br>
2)hardcode their behavior inside clang ...<br>
<br>
Obviously, we should add something to the model.<br>
<br>
Anyways, since we got in the Juliet Test Suite argument, is it<br>
possible to open a new bug report with a status of the static analyzer<br>
with it? It would keep track and could be improved by the GSoC 2014<br>
student(s) who wants to work on it.<br>
Also, I suggest to include to the todo things for the GSoC the idea of<br>
conforming the new Unique Defect ID to the CWE ID. This would be<br>
helpful when you want to test clang analyzer with the Static Analysis<br>
Tool Exposition (SATE): <a href="http://samate.nist.gov/SATE.html" target="_blank">http://samate.nist.gov/SATE.html</a><br>
<br>
<br>
2014-03-10 2:32 GMT+01:00 Ted Kremenek <<a href="mailto:kremenek@apple.com">kremenek@apple.com</a>>:<br>
<div class="HOEnZb"><div class="h5">> Hi Edoardo,<br>
><br>
> What you are observing is something that is potentially easy to "fix", but<br>
> essentially requires additional domain-specific modeling in the static<br>
> analyzer.<br>
><br>
> To understand what is going on, consider the following example:<br>
><br>
> void foo(int x) {<br>
> 1 / x;<br>
> }<br>
><br>
> In this example we have a potential division-by-zero. If 'foo' is analyzed<br>
> in isolation, we don't know anything about the value of 'x'. We can do one<br>
> of two things:<br>
><br>
> (1) Warn that 'x' could potentially be zero.<br>
><br>
> (2) Do not emit a warning, but register there was a division and that 'x'<br>
> cannot be zero after the division, and keep analyzing.<br>
><br>
> In both cases the value of 'x' is unconstrained, so we can look at #1 and #2<br>
> as two potential default behaviors. In the analyzer we do #2. Essentially,<br>
> although the value of 'x' is unconstrained, we don't warn here. The<br>
> rationale is that the analyzer would emit a huge number of false positives<br>
> for integers that are possibly perfectly safe. We take the same tactic for<br>
> pointers, who all could hypothetically could be null.<br>
><br>
> Instead, we take the strategy in the analyzer to flag bugs like null<br>
> pointers and division-by-zero if we have evidence belief there may be a<br>
> problem. For example, if a pointer is checked against null, we have<br>
> evidence to believe that the pointer could be null. Similarly, there may be<br>
> some APIs that we know could return a null pointer, and thus we can possibly<br>
> track that information and see if a pointer coming from one of these sources<br>
> is dereferenced.<br>
><br>
> The same tactic can be taken with integers and divide-by-zero. Let's look<br>
> at one of your examples:<br>
><br>
> 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>
><br>
> After the call to 'fscanf' the analyzer tracks that 'data' binds to some<br>
> symbolic integer value. That value is considered to be underconstrained,<br>
> just like in my example above. In this example however, we could track some<br>
> additional information that it came from an unsafe API like fscanf. This<br>
> information is something *additional* that we would need to model, as we<br>
> probably would not want to do this for any arbitrary API call. Modeling<br>
> this might not be too hard. For example, the symbolic integer value does<br>
> have some information associated with it to tell us where it originated; we<br>
> could possibly use this to consult an API list to determine if the integer<br>
> value should be treated as unsafe. We'd then modify the divide-by-zero<br>
> logic in the analyzer to emit a warning if an under constrained integer came<br>
> from one of these sources. We'd probably could conjure up something fairly<br>
> ad hoc at first for a few specific cases, and then generalize it. A while<br>
> ago we experimented with generalized taint analysis in the analyzer, which<br>
> is something that would also possibly be useful here.<br>
><br>
> Does that answer your question? Essentially we need a little additional<br>
> modeling in the analyzer for these APIs.<br>
><br>
> Ted<br>
><br>
><br>
> 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:<br>
><br>
> Ping?<br>
><br>
><br>
> 2014-02-20 22:25 GMT+01:00 Edoardo P. <<a href="mailto:ed0.88.prez@gmail.com">ed0.88.prez@gmail.com</a>>:<br>
>><br>
>> I forgot to add more info regarding the not detected int divisions:<br>
>><br>
>> the only correctly warned parts are for very simple cases, like this:<br>
>><br>
>> int x = 0; ... int y = 100 / x;<br>
>><br>
>> and the modulo variant. The other ones, which are not detected, assign x<br>
>> with:<br>
>><br>
>> - atoi (used when converting a string returned by socket functions or<br>
>> fgets)<br>
>> - fscanf<br>
>> - rand<br>
>><br>
>> And all the variants of such functions. The examples for fscanf and rand<br>
>> are simple:<br>
>><br>
>> fscanf variant:<br>
>><br>
>> 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>
>><br>
>> rand variant:<br>
>><br>
>> void f_rand()<br>
>> {<br>
>> int data;<br>
>> data = rand();<br>
>> /* POTENTIAL FLAW: Possibly divide by zero */<br>
>> printIntLine(100 / data);<br>
>> }<br>
>><br>
>> 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<br>
>> result (13 bits overflow, but that is okay) */<br>
>> #define RAND32() ((rand()<<30) ^ (rand()<<15) ^ rand())<br>
>><br>
>> (I'd truncate the first rand() to the first 2 bits before shifting it to<br>
>> 30th bit position, just to avoid overflow ...)<br>
>><br>
>> The 'itoa' case is more complex. Imho, the analyzer, before reporting the<br>
>> warning, should check that there can be a possibility that the string<br>
>> argument will be converted to 0. I hope it's possible with the current<br>
>> analyzer architecture...<br>
>><br>
>> Cheers,<br>
>> Edward-san<br>
>><br>
>> 2014-02-20 15:26 GMT+01:00 Edoardo P. <<a href="mailto:ed0.88.prez@gmail.com">ed0.88.prez@gmail.com</a>>:<br>
>><br>
>>> Hi Lucas:<br>
>>><br>
>>>><br>
>>>> 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.<br>
>>><br>
>>><br>
>>> Please do.<br>
>>><br>
>>>><br>
>>>> 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>
>>>><br>
>>><br>
>>> I can confirm that. In IRC I discussed with some llvm devs about the need<br>
>>> to report the float division by zero (Standard C/C++ says it's undefined<br>
>>> behavior, but Annex F implicitly allows it, thanks to IEEE 754). I have an<br>
>>> idea: add a new static analyzer option which allows or disallows optional<br>
>>> features, including the optional Annexes. That would help a lot imho.<br>
>>><br>
>>> Cheers,<br>
>>> Edward-san<br>
>>><br>
>>>><br>
>>>> 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>
>>>> ><br>
>>>> > testcases/CWE369_Divide_by_Zero/s02/CWE369_Divide_by_Zero__int_zero_divide_01.c<br>
>>>> > -o /dev/null<br>
>>>> ><br>
>>>> ><br>
>>>> > and I get the warnng:<br>
>>>> ><br>
>>>> ><br>
>>>> > testcases/CWE369_Divide_by_Zero/s02/CWE369_Divide_by_Zero__int_zero_divide_01.c:30:22:<br>
>>>> > 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">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">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">kanashiro.duarte@gmail.com</a><br>
>>>> > > ><br>
>>>> > > > _______________________________________________<br>
>>>> > > > cfe-users mailing list<br>
>>>> > > > <a href="mailto:cfe-users@cs.uiuc.edu">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">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">kanashiro.duarte@gmail.com</a><br>
>>>><br>
>>><br>
>>><br>
>>><br>
>>> --<br>
>>> Mathematics is the language with which God has written the universe.<br>
>>> (Galilei)<br>
>><br>
>><br>
>><br>
>><br>
>> --<br>
>> Mathematics is the language with which God has written the universe.<br>
>> (Galilei)<br>
><br>
><br>
><br>
><br>
> --<br>
> Mathematics is the language with which God has written the universe.<br>
> (Galilei)<br>
><br>
><br>
<br>
<br>
<br>
--<br>
Mathematics is the language with which God has written the universe. (Galilei)<br>
</div></div></blockquote></div><br></div>