<div dir="ltr"><div class="gmail_extra">
<p class="">Thank you for your reply, Jordan.</p>
<p class="">As you said, what I want to do is to merge the two paths together. You're right that in my previous source code sample, 'arg' and 'v' are not referenced after the full if-statement. And as you said, they could get cleaned out of the state being tracked. So I've made a little modification on the code this time and it may be better:</p>
<p class=""><i> 1 void func(int arg) {</i></p><p class=""><i> 2 int v;</i></p>
<p class=""><i> 3 if(arg > 0) </i></p>
<p class=""><i> 4 v = arg + 1;</i></p>
<p class=""><i> 5 else</i></p>
<p class=""><i> 6 v = arg + 999;</i></p>
<p class=""><i> 7 int a, b;</i></p>
<p class=""><i> 8 a = 99; </i></p>
<p class=""><i> 9 b = v;</i></p>
<p class=""><i>10 }</i></p>
<p class="">Thus, the symbolic execution path can be <span class="">roughly</span> represented as follow(based on ExplodedGraph):</p>
<p class=""><a href="http://ww1.sinaimg.cn/large/a74ecc4cjw1e203yily40j.jpg">http://ww1.sinaimg.cn/large/a74ecc4cjw1e203yily40j.jpg</a></p>
<p class="">As you said, merging paths may lead to the loss of precision. I agree with it. However, in my work, the precision requirement is not very high. For example, for the same variable 'v', I don't care whether the values of 'v' conflict after merging. In my work, the performance requirement is relatively high. So if the if-else blocks are not merged, the analyzer's original traversing will cost too much time, especially for complex source code files. </p>
<p class="">In this way, is there any way to tell the analyzer that "after finish traversing the block2, you should go to the block4 rather than the block3"? If this idea is not feasible, is there any other way to realize my goal even if I have to modify the CoreEngine. And if there was, which part should I modify? That is, if I want to implement 'merge', is there any other part of Clang needed to be modified in addition to CoreEngine? CFG, AST or any other possible part? <br>
</p>
<p class="">What' more, any explanation on the mechanism of CoreEngine and the construction of ExplodedGraph/ExplodedNode will help me. <br></p>
<p class="">Am I doing something stupid here? Thank you for the help. :-)<br></p><p class=""><br></p><p class=""><span style="font-family:arial,sans-serif;font-size:14px">Best regards,</span><br style="font-family:arial,sans-serif;font-size:14px">
<span style="font-family:arial,sans-serif;font-size:14px">Arthur Yoo</span><br></p><p class=""><span style="font-family:arial,sans-serif;font-size:14px"><br></span></p><br><div class="gmail_quote">2013/2/5 Jordan Rose <span dir="ltr"><<a href="mailto:jordan_rose@apple.com" target="_blank">jordan_rose@apple.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"><div style="word-wrap:break-word"><div>Hi, Arthur. The static analyzer is very much built on finding all possible paths through a program -- right now there's no way to tell it that two paths "merge" together in this way. However, in this case it may actually be able to figure this out: because 'arg' and 'v' are not referenced after the full if-statement, they could get cleaned out of the state being tracked, which means that the second time through the analyzer will say "oh, I've seen this state before".</div>
<div><br></div><div>We would like to do more things like this ("widening" to encompass/join two paths), but it's a hard problem to decide that two states are "the same", and if they aren't the same how to merge them with minimal loss of precision.</div>
<div><br></div><div>Apart from that, though, the analyzer's not even guaranteed to traverse paths in a depth-first search. Currently it does, but that decision has gone back and forth, and we might try BFS or some mixed search order again in the future. This currently isn't convenient to change: you have to tweak the constructor of CoreEngine in CoreEngine.h and then recompile.</div>
<div><br></div><div>Finally, though, if you are trying to generate notes along the path of execution, you should do this after the fact using a BugReporterVisitor. This is sort of like a checker for a bug path—you get to see all the nodes on <i>one</i> path that led to a particular bug report.</div>
<div><br></div><div>Hope that helps,</div><div>Jordan</div><div><br></div><br><div><div><div class="h5"><div>On Feb 2, 2013, at 8:25 , Arthur Yoo <<a href="mailto:phjy007@gmail.com" target="_blank">phjy007@gmail.com</a>> wrote:</div>
<br></div></div><blockquote type="cite"><div><div class="h5"><div dir="ltr">Hi all,<div><br></div><div>Recently I am working on developing a checker of Clang Static Analyzer. Because Clang Static Analyzer has a powerful symbolic execution engine, I choose Clang Static Analyzer as the platform for my work. My Checker mainly does some analysis work for C source code files. The checker will make use of the program states during its analysis execution and it will generate a report for each analysis. </div>
<div><br></div><div>In my understanding, symbolic execution(Clang static analyzer) will cover all possible paths. For example, here is an sample source code which will be <span style="font-family:'Microsoft YaHei';font-size:13px;white-space:nowrap">analyzed</span> by static analyzer:</div>
<div><div> 1 void func(int arg) {</div><div> 2 int v;</div><div> 3 if(arg > 0) </div><div> 4 v = arg + 1;</div><div> 5 else</div><div> 6 v = arg + 999;</div><div> 7 int a, b;</div><div>
8 a = 99; </div><div> 9 b = a;</div><div>10 }</div><div><div>The symbolic execution path can be <span style="font-family:'Microsoft YaHei';font-size:13px;white-space:nowrap">roughly</span> represented as follow(based on ExplodedGraph):</div>
<div><a href="http://ww2.sinaimg.cn/large/a74ecc4cjw1e1fipmgpy5j.jpg" target="_blank">http://ww2.sinaimg.cn/large/a74ecc4cjw1e1fipmgpy5j.jpg</a><br></div><div><div>And the execution sequence is 1-2-3-(1)-4-5. However, is there any possible means to change the execution sequence to be linear? That is to say, is there any possible means to change the execution sequence to be 1-2-(1)-4-5?</div>
<div>Thanks for the help.</div></div><br>------<br>Best regards,<br>Arthur Yoo</div></div></div></div></div>
_______________________________________________<br>cfe-dev mailing list<br><a href="mailto:cfe-dev@cs.uiuc.edu" target="_blank">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></div></blockquote></div><br><br clear="all"><div><br></div>-- <br>------<br>Best regards,<br>Yue Jiayuan
</div></div>