[cfe-dev] Clang Static Analyzer execution path for loop
Anna Zaks
ganna at apple.com
Tue Apr 9 14:13:50 PDT 2013
Jordan has just pointed out that in the third example, the analyzer knows that the loop will execute more than 4 times (we know that arg is more or equal to 314). Because of this, the analyzer is not going to explore the path on which you analyze the loop and then get to the end of the function. That is probably the unusual issue with ex3 you are seeing.
Cheers,
Anna.
On Apr 9, 2013, at 10:54 AM, Anna Zaks <ganna at apple.com> wrote:
> Arthur,
>
> The analyzer explores the exploded graph (the graph that contains all path) in SOME order (currently DFS, but could be anything). It does NOT trace paths one after another. You are not tracing the paths but just look at the order in which the nodes of the graph are explored.
>
> Anna.
>
> On Apr 9, 2013, at 6:03 AM, Arthur Yoo <phjy007 at gmail.com> wrote:
>
>> Hi Anna,
>>
>> I modified the CoreEngine.cpp and output the CFG-BlockID in the HandleBlockExit() method. So whenever a CFG Block is going to exit, it will output its BlockID. In this way, I could observe the execution path sequences.
>>
>> I am confused on the CFG execution path of code_3.c. In my tests, I used the Clang Static Analyzer default loop time value, which equals four (defined in CompilerInvocation.cpp:221). So the analyzer will execute a loop for four times. In the execution paths of code_1.c and code_2.c, the four loop executions are separated. For example, in code_2.c, the execution path sequence is B7-B2-B1-B6-B5-B1-B4-B3-B5-B1-B4-B3-B5-B1-B4-B3-B5-B1-B4-B3. B5 is a CFG block which stands for loop condition. It can also be regarded as a branch start point. In this execution sequence, after the execution of B5, the Analyzer traces B1, which can be regarded as the else branch of B5. After tracing the else branch path, the path traces back, and begins to trace the then branch path of B5, including B4 and B3. B4 and B3 are the real body of the for loop. In this way, the subsequence(B5-B1-B4-B3) is repeated for 4 times. The execution path of code_1.c also follows the same rule.
>>
>> However, the execution path of code_3.c seems to break this rule. The execution path sequence of code_3.c is B7-B5-B4-B3-B2-B4-B3-B2-B4-B3-B2-B4-B3-B2-B6-B1. B4 is a CFG block which stands for this loop condition. B2 and B3 consists of the then path of B4, which can also be regarded as the real body of the for loop. The most strange thing here is that, after tracing the B4, the analyzer begins to trace the then path(B3 and B2), instead of tracing the else path. And the analyzer repeats four times to tracing the then path of the for loop(B4-B3-B2-B4-B3-B2-B4-B3-B2-B4-B3-B2). If we use the same tracing rule to trace code_3.c, I think the execution path should be B7-B5-B4-B1-B3-B2-B4-B1-B3-B2-B4-B1-B3-B2-B4-B1-B3-B2-B6-B1. That is, after tracing B4, analyzer should trace the else path(B1), and then begins to trace the then path(B3-B2).
>>
>> So, can you help me explain the execution path produced by the Analyzer in code_3.c? Thank you.
>>
>>
>>
>> Best regards,
>> Arthur Yoo
>>
>> 2013/4/9 Anna Zaks <ganna at apple.com>
>>
>> On Apr 6, 2013, at 11:30 PM, Arthur Yoo <phjy007 at gmail.com> wrote:
>>
>>> Hi all,
>>>
>>> Now I am focusing on the execution path of Clang Static Analyzer. Firstly, I did some tests on code_1.c.
>>>
>>> //code_1.c
>>>
>>> void func(int arg) {
>>>
>>> int v;
>>>
>>> v = 0;
>>>
>>> int i;
>>>
>>> for(i = 0; i < arg; i++) {
>>>
>>> v = v + 1;
>>>
>>> }
>>>
>>> int a, b;
>>>
>>> a = v;
>>>
>>> b = a;
>>>
>>> }
>>>
>>> The CFG of code_1.c is http://ww3.sinaimg.cn/large/a74e55b4jw1e3h14gvh8vj.jpg.
>>>
>>> Then I tried to get the corresponding execution path sequence. Through test I got its execution path sequence, which is B5-B4-B1-B3-B2-B4-B1-B3-B2-B4-B1-B3-B2-B4-B1-B3-B2. (In code_1.c, the variable arg, which determines the loop times, is a symbolic value. And I used the default max_loop value in Clang Static Anaylzer, which equals 4.)
>>>
>>>
>>>
>>> I tried to do the same tests on code_2.c.
>>>
>>> //code_2.c
>>>
>>> void func(int arg) {
>>>
>>> int v;
>>>
>>> v = arg + 1;
>>>
>>> if(arg < 314) {
>>>
>>> for(int i = 0; i < arg; i++) {
>>>
>>> v = arg + 33;
>>>
>>> }
>>>
>>> } else {
>>>
>>> v = arg + 11;
>>>
>>> }
>>>
>>> int a, b;
>>>
>>> a = 62951413;
>>>
>>> b = v;
>>>
>>> }
>>>
>>> The CFG of code_2.c is http://ww2.sinaimg.cn/large/a74eed94jw1e3h13zu3raj.jpg. And its execution path sequence is B7-B2-B1-B6-B5-B1-B4-B3-B5-B1-B4-B3-B5-B1-B4-B3-B5-B1-B4-B3. The rule of tracing path in code_2.c is consistent with the rule in code_1.c.
>>>
>>>
>>>
>>> However, when I tried to do the same tests on code_3.c.
>>>
>>> //code_3.c
>>>
>>> void func(int arg) {
>>>
>>> int v;
>>>
>>> v = arg + 1;
>>>
>>> if(arg < 314) {
>>>
>>> v = arg + 11;
>>>
>>> } else {
>>>
>>> for(int i = 0; i < arg; i++) {
>>>
>>> v = arg + 33;
>>>
>>> }
>>>
>>> }
>>>
>>> int a, b;
>>>
>>> a = 62951413;
>>>
>>> b = v;
>>>
>>> }
>>>
>>> The CFG of code_3.c is http://ww4.sinaimg.cn/large/a74ecc4cjw1e3h13ae2xtj.jpg. It seems that some strange things happened. Through test I got its execution path sequence, which is B7-B5-B4-B3-B2-B4-B3-B2-B4-B3-B2-B4-B3-B2-B6-B1. In fact, I expected the execution sequence should be B7-B5-B4-B1-B3-B2-B4-B1-B3-B2-B4-B1-B3-B2-B4-B1-B3-B2-B6-B1.
>>>
>>>
>>>
>> Are you saying that 'v = arg + 11;' is executed twice on the path you are observing?
>> How are you observing the execution path sequences? You cannot see the paths by observing the callbacks from the checkers since the analyzer does not make any guarantees on the order in which statements from different paths are processed. In this example, there are more than 2 paths through this program. You might be observing parts of different paths.
>>
>> Cheers,
>> Anna.
>>> So, is there anybody can help me explain the execution path of Clang Static Analyzer in code_3.c?
>>>
>>> Am I doing something stupid here? Any help will be greatly appreciated.
>>>
>>> P.S. The version number of LLVM and Clang in my tests is 3.3.
>>>
>>> ------
>>> Best regards,
>>> Arthur Yoo
>>> _______________________________________________
>>> cfe-dev mailing list
>>> cfe-dev at cs.uiuc.edu
>>> http://lists.cs.uiuc.edu/mailman/listinfo/cfe-dev
>>
>>
>>
>>
>> --
>> ------
>> Best regards,
>> Yue Jiayuan
>
> _______________________________________________
> cfe-dev mailing list
> cfe-dev at cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/cfe-dev
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20130409/2d0d8e21/attachment.html>
More information about the cfe-dev
mailing list