Hi Ted,<br><br>
<div class="gmail_quote">在 2011年6月9日 上午7:38，Ted Kremenek <span dir="ltr"><<a href="mailto:kremenek@apple.com" target="_blank">kremenek@apple.com</a>></span>写道：<br>
<blockquote class="gmail_quote" style="PADDING-LEFT: 1ex; MARGIN: 0px 0px 0px 0.8ex; BORDER-LEFT: #ccc 1px solid">
<div style="WORD-WRAP: break-word">
<div>
<div>
<div>On Jun 6, 2011, at 8:14 PM, 章磊 wrote:</div><br>
<blockquote type="cite"><span style="WORD-SPACING: 0px; FONT: medium Helvetica; TEXT-TRANSFORM: none; TEXT-INDENT: 0px; WHITE-SPACE: normal; LETTER-SPACING: normal; BORDER-COLLAPSE: separate">Hi Ted,
<div><br></div>
<div>Thank you very much for your reply and sorry for misunderstanding the word "<span style="FONT-SIZE: 13px; FONT-FAMILY: arial, sans-serif; BORDER-COLLAPSE: collapse">aggregate</span>".</div>
<div><span style="FONT-SIZE: 13px; FONT-FAMILY: arial, sans-serif; BORDER-COLLAPSE: collapse"><br></span></div>
<div><span style="FONT-SIZE: 13px; FONT-FAMILY: arial, sans-serif; BORDER-COLLAPSE: collapse">I thought that we can do aggregation only when a path is fully analyzed, so when you mention the aggregation in checkDeadSymbols, i didn't get what you mean to do.</span></div>
<div><br></div>
<div>I think this counting strategy is great, but i have a little problem:<span> </span><br><br>IMO, it's a trade-off between counting statistics along individual paths and counting statistics in your way. When there is no path explosion, they give the same counts. But when the path explodes, they works different.<br>
<br>In the first way, we will fully analyze part of all the paths and we can give the accurate results of those paths. But we will leave out some paths because of the step limit and the analyzer should work in a particular way.<br>
In the second way, we do not fully analyze a path, we will call checkEndPath while we are not meet the actual path end, so we<span lang="en"><span title="点击可显示其他翻译"><span> </span>can not guarantee the states we are counting are totally right(the aggregation in checkDeadSymbols is ok, since all the dead symbols will not be checked; but in checkEndPath some symbols may be checked after this "step limited end path"). And could this results be the<span> </span></span></span>"representative evidence of behavioral trends"<span lang="en"><span title="点击可显示其他翻译"><span> </span>?<br>
<br>If the second way is ok, and since we should not force the analyzer to<span> </span></span></span>exploring the state space in a particular way, i will do it in the second way.</div></span></blockquote></div><br></div>
<div>Hi Lei,</div>
<div><br></div>
<div>Let me focus around this particular comment:</div>
<div>
<div><br></div>
<div>
<blockquote type="cite">
<blockquote type="cite"><span style="WORD-SPACING: 0px; FONT: medium Helvetica; TEXT-TRANSFORM: none; TEXT-INDENT: 0px; WHITE-SPACE: normal; LETTER-SPACING: normal; BORDER-COLLAPSE: separate">
<div>In the first way, we will fully analyze part of all the paths and we can give the accurate results of those paths. </div></span></blockquote></blockquote><br></div></div>
<div>I think this is a misconception. We never will fully analyze part of all the paths in a manner where each count in our statistics can be considered to have come from a single path. Consider:</div>
<div><br></div>
<div><br></div>
<div> void foo() {</div>
<div> int x = bar();</div>
<div> if (x > 0)</div>
<div> x++;</div>
<div> else</div>
<div> x--;</div>
<div> // never use 'x' afterwards</div>
<div> ...</div>
<div> }</div>
<div><br></div>
<div>The exact operations here are not important. What I want to stress is that, regardless of path exploration, we will merge the two paths after the if..else... because 'x' is not used afterwards. When a variable is no longer live, the analysis engine prunes that variable binding, and any associated symbolic constraints, from the state. In the example above, this means that the GRState along the two paths (one for the true branch, the other for the false branch) will be the same. At this point, the paths are *merged* in the ExplodedGraph, because analyzing either of them from that point on would produce the same analysis results. This is a key optimization in the analyzer engine to reduce the exponential growth from path exploration.</div>
<div><br></div>
<div>My point is that "counting paths" just doesn't make sense. Paths get merged all the time, or we may come up with other ways to cut out paths from the ExplodedGraph that don't need to be explicitly represented or explicitly explored. Definitely this impacts how we count statistics, but I'm suggesting we pick a scheme that seems less sensitive to how we enumerate paths, and more on the behavior we observed from those paths.</div>
<div> </div></div></blockquote>
<div> </div>
<div>Thank you very much to expound this and sorry for taking this long time to get your idea.</div>
<div> </div>
<blockquote class="gmail_quote" style="PADDING-LEFT: 1ex; MARGIN: 0px 0px 0px 0.8ex; BORDER-LEFT: #ccc 1px solid">
<div style="WORD-WRAP: break-word">
<div>The motivation behind my suggesting for how to aggregate statistics was simple: forgo any notion that we are enumerating paths, and instead accumulate distinct observations where behavior was consistent or different. Here I actually try and marginalize out the effects of path explosion or merging, and instead focus on the behavior at particular program points.</div>
<div>
<div><br></div>
<div>
<blockquote type="cite"><span style="WORD-SPACING: 0px; FONT: medium Helvetica; TEXT-TRANSFORM: none; TEXT-INDENT: 0px; WHITE-SPACE: normal; LETTER-SPACING: normal; BORDER-COLLAPSE: separate">
<div>In the second way, we do not fully analyze a path, we will call checkEndPath while we are not meet the actual path end, so we<span lang="en"><span title="点击可显示其他翻译"> can not guarantee the states we are counting are totally right(the aggregation in checkDeadSymbols is ok, since all the dead symbols will not be checked; but in checkEndPath some symbols may be checked after this "step limited end path").</span></span></div>
</span></blockquote><br></div></div>
<div>I don't fully understand this comment. All I am suggesting is that aggregate statistics when a symbol no longer is being tracked. When a symbol "dies" early, we do that aggregation in checkDeadSymbols. If a symbol lives to the end of a path, when do it in checkEndPath.</div>
<div><br></div>
<div>Can you clarify, precisely, what you mean by 'but in checkEndPath some symbols may be checked after this "step limited end path"'? checkEndPath will never be called when we are step limited. It is only called when we actually hit the end of a function. When we are step limited, we simply stop analyzing a path.</div>
</div></blockquote>
<div> </div>
<div>Sorry, my bad, I mistaken the checkEndAnalysis as checkEndPath.</div>
<div> </div>
<blockquote class="gmail_quote" style="PADDING-LEFT: 1ex; MARGIN: 0px 0px 0px 0.8ex; BORDER-LEFT: #ccc 1px solid">
<div style="WORD-WRAP: break-word">
<div><br></div>
<div>Cheers,</div>
<div>Ted</div></div></blockquote></div><br>I still corcern about that how the second way really works, so i will take this way and do some test.<br clear="all"><br>-- <br>Best regards!<br><br>Lei Zhang<br>