<div dir="ltr"><div>The ranged based constraint manager is kinda weak, we all know that.<br></div><div>To circumvent such infeasible bugreports, I highly recommend enabling the Z3 refutation (`-analyzer-config crosscheck-with-z3=true`)<br>which validates the constraints on the bugpath. Invalidates the bugreport if the constraints are UnSAT.<br>This option would suppress this report for sure.<br><br></div><div>Another solution is to make the constraint manager smarter, to reason about sym-sym comparisons, at least for the obvious ones.<br></div><div>My patch under review is partially solving this (still in WIP): <a href="https://reviews.llvm.org/D77792">D77792</a></div><div><br></div><div>Note that this limitation is well known and understood.<br>Introducing sym-sym comparisons seems to be valuable, though I'm not entirely sure how would fit into our model.</div><div>It would cover some sym-sym-comparisons, but potentially not all of them.</div><div>Debugging why a certain comparison evaluated to true/false would be a somewhat cumbersome process even if we dump the ExplodedGraph.</div><div><br></div><div>Imagine this example:<br><span style="font-family:monospace">void transitivity(int x, int y, int z) {<br>  if (x >= y)<br>    return;<br>  // x < y for sure<br>  if (y >= z)<br>    return;<br>  // y < z for sure<br>  clang_analyzer_eval(x < z); // ?<br>}</span><br></div><div><br></div><div>Regards,<br></div><div>Balazs<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">Denis Petrov via cfe-dev <<a href="mailto:cfe-dev@lists.llvm.org">cfe-dev@lists.llvm.org</a>> ezt írta (időpont: 2020. ápr. 22., Sze, 22:55):<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">




<div dir="ltr" style="font-size:12pt;color:rgb(0,0,0);background-color:rgb(255,255,255);font-family:Calibri,Arial,Helvetica,sans-serif">
<p>Hi, CSA ​community.<br>
</p>
<p><br>
</p>
<p>I got an idea how to make RangeConstraintManager​ more sofisticated.<br>
</p>
<div><span style="font-family:Calibri,Arial,Helvetica,sans-serif;font-size:16px;background-color:rgb(255,255,255)">I want you speak out, share your vision about this idea.</span><br>
<br>
</div>
<p>Actually this bug <a href="https://bugs.llvm.org/show_bug.cgi?id=13426" target="_blank">https://bugs.llvm.org/show_bug.cgi?id=13426</a> pushed me to these thoughts.<br>
</p>
<p>Let's consider the next snippet:<br>
</p>
<p><br>
</p>
<div>
<div><span style="font-family:Consolas,monospace"></span><span style="font-family:Consolas,monospace">int foo(int y, int x) {</span></div>
<div><span style="white-space:pre-wrap;font-family:Consolas,monospace"></span><span style="font-family:Consolas,monospace">int x;</span><br style="font-family:Consolas,monospace">
</div>
<div><span style="white-space:pre-wrap;font-family:Consolas,monospace"></span><span style="font-family:Consolas,monospace">if (y == z) {</span><br style="font-family:Consolas,monospace">
</div>
<div><span style="white-space:pre-wrap;font-family:Consolas,monospace"></span><span style="font-family:Consolas,monospace">x = 0;</span></div>
<div><span style="white-space:pre-wrap;font-family:Consolas,monospace"></span><span style="font-family:Consolas,monospace">}</span><br style="font-family:Consolas,monospace">
</div>
<div><span style="white-space:pre-wrap;font-family:Consolas,monospace"></span><span style="font-family:Consolas,monospace">if (y != z) {</span></div>
<div><span style="white-space:pre-wrap;font-family:Consolas,monospace"></span><span style="font-family:Consolas,monospace">x = 1;</span></div>
<div><span style="white-space:pre-wrap;font-family:Consolas,monospace"></span><span style="font-family:Consolas,monospace">}</span><br style="font-family:Consolas,monospace">
</div>
<div><span style="white-space:pre-wrap;font-family:Consolas,monospace"></span><span style="font-family:Consolas,monospace">return x;</span><br style="font-family:Consolas,monospace">
</div>
<div><span style="font-family:Consolas,monospace">}</span><br>
</div>
<div><span style="font-family:Consolas,monospace"><br>
</span></div>
Finally CSA reports you: <br>
</div>
<div>
<div><span style="font-family:Consolas,monospace"><span style="font-family:Consolas,monospace">warning: Undefined or garbage value returned to caller</span></span></div>
<div><span style="font-family:Consolas,monospace"><span style="font-family:Consolas,monospace">      [core.uninitialized.UndefReturn]</span></span></div>
<div><span style="font-family:Consolas,monospace"><span style="font-family:Consolas,monospace">        return x;</span></span><br>
</div>
<div><br>
</div>
<div>But as a human <span style="font-family:Calibri,Arial,Helvetica,sans-serif;font-size:16px;background-color:rgb(255,255,255)">you</span><span style="font-family:Calibri,Arial,Helvetica,sans-serif;font-size:16px;background-color:rgb(255,255,255)"> </span>know that
 `x` has <span style="font-family:Calibri,Arial,Helvetica,sans-serif;font-size:16px;background-color:rgb(255,255,255)">
definitely </span>been initialized.<br>
</div>
<div>As you can see CSA builds paths without relying on previous conditions (except the case {A-B} {B-A}m it is already done).<br>
</div>
</div>
<div>The same behavior appears when:<br>
</div>
<div><span style="font-size:16px;background-color:rgb(255,255,255);font-family:Consolas,monospace"><span style="font-family:Consolas,monospace"><span style="font-family:Consolas,monospace">(y >  z)</span></span></span><span style="font-family:Consolas,monospace"><span style="font-family:Consolas,monospace">
 (y <= </span></span><span style="font-size:16px;background-color:rgb(255,255,255);font-family:Consolas,monospace"><span style="font-family:Consolas,monospace"><span style="font-family:Consolas,monospace">z)</span></span></span><br style="font-family:Consolas,monospace">
</div>
<div><span style="font-size:16px;background-color:rgb(255,255,255);font-family:Consolas,monospace"><span style="font-family:Consolas,monospace"><span style="font-family:Consolas,monospace">(y <= z)</span></span></span><span style="font-size:16px;background-color:rgb(255,255,255);font-family:Consolas,monospace"><span style="font-family:Consolas,monospace"><span style="font-family:Consolas,monospace"> (y >  </span></span></span><span style="font-size:16px;background-color:rgb(255,255,255);font-family:Consolas,monospace"><span style="font-family:Consolas,monospace"><span style="font-family:Consolas,monospace">z)</span></span></span><span style="font-size:16px;background-color:rgb(255,255,255);font-family:Consolas,monospace">​</span><br style="font-family:Consolas,monospace">
</div>
<div><span style="font-size:16px;background-color:rgb(255,255,255);font-family:Consolas,monospace"><span style="font-family:Consolas,monospace"><span style="font-family:Consolas,monospace">(y == z)</span></span></span><span style="font-size:16px;background-color:rgb(255,255,255);font-family:Consolas,monospace"><span style="font-family:Consolas,monospace"><span style="font-family:Consolas,monospace"> (z !=
 y</span></span></span><span style="font-size:16px;background-color:rgb(255,255,255);font-family:Consolas,monospace"><span style="font-family:Consolas,monospace"><span style="font-family:Consolas,monospace">)</span></span></span><span style="font-size:16px;background-color:rgb(255,255,255);font-family:Consolas,monospace">​</span></div>
<div><span style="font-size:16px;background-color:rgb(255,255,255);font-family:Consolas,monospace">etc.</span></div>
<div><span style="font-size:12pt">I made a solution for this but have not upload it for review yet</span><span style="font-size:12pt">.</span></div>
<div><span style="font-size:12pt"><br>
</span></div>
<div><span style="font-size:12pt">I also have some more thoughts about optimization such:</span></div>
<div><span style="font-size:12pt"></span><span style="font-family:Consolas,monospace">if (y <  z) {</span><span style="font-family:Consolas,monospace">}</span></div>
<div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif;font-size:16px;background-color:rgb(255,255,255)">
<span style="font-family:Consolas,monospace">if (y <= z) {} // which is a subset of <span style="font-family:Consolas,monospace;font-size:16px;background-color:rgb(255,255,255)">(</span><span style="font-family:Consolas,monospace;font-size:16px;background-color:rgb(255,255,255)">y
 < </span><span style="font-family:Consolas,monospace;font-size:16px;background-color:rgb(255,255,255)">z</span><span style="font-family:Consolas,monospace;font-size:16px;background-color:rgb(255,255,255)">)</span></span></div>
<div style="font-size:16px;background-color:rgb(255,255,255)"><br>
</div>
<div style="font-size:16px;background-color:rgb(255,255,255)">I can continue to do this improvement and show you the result soon.<br>
</div>
</div>
<p><br>
</p>
<div id="gmail-m_4387762360841155781Signature">
<div name="divtagdefaultwrapper">
<hr>
<div><b>Denys Petrov</b></div>
<div>Senior С++ Developer | Kharkiv, Ukraine</div>
<div><br>
</div>
<div></div>
</div>
</div>
</div>

_______________________________________________<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="https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev" rel="noreferrer" target="_blank">https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev</a><br>
</blockquote></div>