<html xmlns:o="urn:schemas-microsoft-com:office:office" xmlns:w="urn:schemas-microsoft-com:office:word" xmlns:m="http://schemas.microsoft.com/office/2004/12/omml" xmlns="http://www.w3.org/TR/REC-html40"><head><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></head><body lang=HU link=blue vlink="#954F72"><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 lang=EN-US style='font-family:"Segoe UI Emoji",sans-serif'>😊</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">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">dkszelethus@gmail.com</a>; <a href="mailto:lewisurn@gmail.com">lewisurn@gmail.com</a><br><b>Cc: </b><a href="mailto:cfe-dev@lists.llvm.org">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">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">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">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">cfe-dev@lists.llvm.org</a><br><a href="http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev" target="_blank">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">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">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></body></html>