<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body text="#000000" bgcolor="#FFFFFF">
The addTransition() method family is well-defended against
accidentally squeezing the current state into it, there's no need to
check if the state has changed on the checker side. I don't remember
what i was thinking, but this statement in the guide is definitely
outdated or incorrect.<br>
<br>
I don't think this TODO is anyhow important to address. State
comparison is O(1) regardless of how many changes were made. The
TODO should probably be removed.<br>
<br>
That said, these special cases and default arguments of
addTransition(), i.e., passing null state, passing current state,
passing null predecessor, passing current predecessor, passing null
tag, etc., are too numerous and counter-intuitive to memorize, no
wonder i was confused. I believe we should break this up into
several methods instead (with different, intuitive names).<br>
<br>
<br>
<div class="moz-cite-prefix">On 10/9/18 5:50 AM, Whisperity via
cfe-dev wrote:<br>
</div>
<blockquote type="cite"
cite="mid:5bbca422.1c69fb81.68c7.812e@mx.google.com">
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
<meta name="Generator" content="Microsoft Word 15 (filtered
medium)">
<style><!--
/* Font Definitions */
@font-face
{font-family:"Cambria Math";
panose-1:2 4 5 3 5 4 6 3 2 4;}
@font-face
{font-family:Calibri;
panose-1:2 15 5 2 2 2 4 3 2 4;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
{margin:0cm;
margin-bottom:.0001pt;
font-size:11.0pt;
font-family:"Calibri",sans-serif;}
a:link, span.MsoHyperlink
{mso-style-priority:99;
color:blue;
text-decoration:underline;}
a:visited, span.MsoHyperlinkFollowed
{mso-style-priority:99;
color:#954F72;
text-decoration:underline;}
pre
{mso-style-priority:99;
mso-style-link:"HTML Preformatted Char";
margin:0cm;
margin-bottom:.0001pt;
font-size:10.0pt;
font-family:"Courier New";}
tt
{mso-style-priority:99;
font-family:"Courier New";}
span.HTMLPreformattedChar
{mso-style-name:"HTML Preformatted Char";
mso-style-priority:99;
mso-style-link:"HTML Preformatted";
font-family:"Courier New";}
.MsoChpDefault
{mso-style-type:export-only;}
@page WordSection1
{size:612.0pt 792.0pt;
margin:72.0pt 72.0pt 72.0pt 72.0pt;}
div.WordSection1
{page:WordSection1;}
--></style>
<div class="WordSection1">
<p class="MsoNormal"><span lang="EN-US">Use Occam’s razor, there
is a very easy explanation for that particular TODO. Namely
that no one had the time or effort to fix the checkers
mentioned in the comment, and potentially the plethora of
others introduced that exploit the early return. </span><span
style="font-family:"Segoe UI Emoji",sans-serif"
lang="EN-US">😊</span></p>
<p class="MsoNormal"><o:p> </o:p></p>
<div
style="mso-element:para-border-div;border:none;border-top:solid
#E1E1E1 1.0pt;padding:3.0pt 0cm 0cm 0cm">
<p class="MsoNormal" style="border:none;padding:0cm"><b>From:
</b><a href="mailto:cfe-dev@lists.llvm.org"
moz-do-not-send="true">Donát Nagy via cfe-dev</a><br>
<b>Sent: </b>2018. október 9., kedd 14:03<br>
<b>To: </b><a href="mailto:dkszelethus@gmail.com"
moz-do-not-send="true">dkszelethus@gmail.com</a>; <a
href="mailto:lewisurn@gmail.com" moz-do-not-send="true">lewisurn@gmail.com</a><br>
<b>Cc: </b><a href="mailto:cfe-dev@lists.llvm.org"
moz-do-not-send="true">cfe-dev@lists.llvm.org</a><br>
<b>Subject: </b>Re: [cfe-dev] avoid loops in the exploded
graph?</p>
</div>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">Hi,<o:p></o:p></p>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">My intuition is that in some situations
it is guaranteed that the state will be modified and then
the if (NewState!=State) check is unnecessary. In other
situations there is a possibility that the state will remain
the same (e.g. the expression was already marked as tainted,
so nothing changes) and this could theoretically create to a
loop edge (an edge from the current node to itself) in the
exploded graph.<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">A loop edge is obviously undesirable,
because it could send graph traversal into infinite loops,
so wee need to guarantee that they do not appear in the
exploded graph. As Kristóf wrote, the method
CheckerContext::addTransitionImpl() always guarantees this
with a defensive check (with a TODO to turn it into an
assert); but in some checkers it is also tested by the
checker itself.<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">Donát<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">On k, 2018-10-09 at 11:10 +0200, Kristóf
Umann via cfe-dev wrote:<o:p></o:p></p>
</div>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<div>
<div>
<div>
<p class="MsoNormal" style="margin-bottom:12.0pt">Hi!<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal">If you look at how <span
style="font-family:"Courier New"">addTransition</span>
is implemented, you can see a big TODO before a
defensive check:<br>
<a
href="https://github.com/llvm-mirror/clang/blob/7c8e954f273730037b454edf94c8d13123dbedf6/include/clang/StaticAnalyzer/Core/PathSensitive/CheckerContext.h#L289"
moz-do-not-send="true">https://github.com/llvm-mirror/clang/blob/7c8e954f273730037b454edf94c8d13123dbedf6/include/clang/StaticAnalyzer/Core/PathSensitive/CheckerContext.h#L289</a><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-bottom:12.0pt">According
to that, it would seem that a checker-side check
should always be there.<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal">Let's see what others think of this
-- to me it would make more sense to have this check
within <span style="font-family:"Courier
New"">addTransition</span>, and I'm unsure
myself why that TODO is there.<o:p></o:p></p>
</div>
</div>
</div>
<p class="MsoNormal"><o:p> </o:p></p>
<div>
<div>
<p class="MsoNormal">Lou Wynn via cfe-dev <<a
href="mailto:cfe-dev@lists.llvm.org"
moz-do-not-send="true">cfe-dev@lists.llvm.org</a>>
ezt írta (időpont: 2018. okt. 9., K, 3:42):<o:p></o:p></p>
</div>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<div>
<p><span style="font-size:13.5pt">Hi,</span></p>
<p><span style="font-size:13.5pt">I read the comment
"avoid loops in the exploded graph" in the following
snippet of code which is on page 32 of the <a
href="https://github.com/haoNoQ/clang-analyzer-guide/releases/download/v0.1/clang-analyzer-guide-v0.1.pdf"
target="_blank" moz-do-not-send="true">workbook</a>.</span></p>
<p><tt><span style="font-size:13.5pt">LocationContext
*LC = C. getLocationContext (); </span></tt><span
style="font-size:13.5pt;font-family:"Courier
New""><br>
<tt>ProgramStateRef State = C. getState (); </tt><br>
<tt>const Expr *E = /* Obtain an expression value of
which is untrusted */; </tt><br>
<tt>ProgramStateRef NewState = State -> addTaint
(E, LC ); </tt><br>
<tt>if ( NewState != State ) // avoid loops in the
exploded graph </tt><br>
<tt> C. addTransition ( NewState );</tt></span></p>
<p><span style="font-size:13.5pt">My question is why the
new tainted state requires the if statement to
prevent loops, while other new states in the book do
not have the if statement when
C.addTransition(State) is used? Do other states
which are not tainted not need to prevent loops? For
example, on page 30, when a new state is added, it
reads:</span></p>
<p><tt><span style="font-size:13.5pt">ProgramStateRef
State = C. getState (); </span></tt><span
style="font-size:13.5pt;font-family:"Courier
New""><br>
<tt>State = modifyState ( State ); // do stuff </tt><br>
<tt>C. addTransition ( State );</tt></span></p>
<p><span style="font-size:13.5pt">There is no if state
to prevent a loop.</span><o:p></o:p></p>
<pre>-- </pre>
<pre>Love,</pre>
<pre>Lou</pre>
<pre><o:p> </o:p></pre>
</div>
<p class="MsoNormal" style="margin-bottom:12.0pt">_______________________________________________<br>
cfe-dev mailing list<br>
<a href="mailto:cfe-dev@lists.llvm.org" target="_blank"
moz-do-not-send="true">cfe-dev@lists.llvm.org</a><br>
<a
href="http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev"
target="_blank" moz-do-not-send="true">http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev</a><o:p></o:p></p>
</blockquote>
</div>
<pre>_______________________________________________</pre>
<pre>cfe-dev mailing list</pre>
<pre><a href="mailto:cfe-dev@lists.llvm.org" moz-do-not-send="true">cfe-dev@lists.llvm.org</a></pre>
</blockquote>
<pre style="mso-margin-top-alt:0cm;margin-right:36.0pt;margin-bottom:5.0pt;margin-left:36.0pt"><a href="http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev" moz-do-not-send="true">http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev</a></pre>
<p class="MsoNormal"><span
style="font-size:10.0pt;font-family:"Courier New""><o:p> </o:p></span></p>
</div>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<pre class="moz-quote-pre" wrap="">_______________________________________________
cfe-dev mailing list
<a class="moz-txt-link-abbreviated" href="mailto:cfe-dev@lists.llvm.org">cfe-dev@lists.llvm.org</a>
<a class="moz-txt-link-freetext" href="http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev">http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev</a>
</pre>
</blockquote>
<br>
</body>
</html>