<div dir="ltr">Hi,<br><div class="gmail_extra"><br><div class="gmail_quote">On 23 October 2017 at 13:47, Wong Henry via cfe-dev <span dir="ltr"><<a href="mailto:cfe-dev@lists.llvm.org" target="_blank">cfe-dev@lists.llvm.org</a>></span> wrote:<br><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">
<div style="font-family:Calibri,Helvetica,sans-serif;font-size:12pt;color:rgb(0,0,0)">
Hi all, </div>
<div style="font-family:Calibri,Helvetica,sans-serif;font-size:12pt;color:rgb(0,0,0)">
Due to the limitations of range-based constraint solver, ArrayBoundCheckerV2 has false negatives now.(<a href="http://clang-developers.42468.n3.nabble.com/improving-the-ArrayBoundChecker-td4037769.html#a4037803" target="_blank">http://clang-<wbr>developers.42468.n3.nabble.<wbr>com/improving-the-<wbr>ArrayBoundChecker-td4037769.<wbr>html#a4037803</a>). <br>
</div>
<div style="font-family:Calibri,Helvetica,sans-serif;font-size:12pt;color:rgb(0,0,0)">
<br>
</div>
<div style="font-family:Calibri,Helvetica,sans-serif;font-size:12pt;color:rgb(0,0,0)">
<div>There are some simple false negative scenes can be tried to solve, like "index * sizeof(int) >= 10", and there are two ways I can think of to solve this problem.</div>
<div><br>
</div>
<div>1.Modify the ArrayBoundCheckerV2, convert "symbol * sizeof(ElementType) >= RegionExtent" into "symbol >= RegionExtent / sizeof(ElementType)", "sizeof (ElementType)" and "RegionExtent" can get as concrete int. <span style="color:rgb(0,0,0);font-family:Calibri,Helvetica,sans-serif;font-size:12pt">If
we're dealing with two known constants, we can perform the operation '/' directly.</span></div></div></div></blockquote><div><br></div><div>Which version did you chek? Are you sure that this transformation is not done yet? See <a href="https://github.com/llvm-mirror/clang/blob/master/lib/StaticAnalyzer/Checkers/ArrayBoundCheckerV2.cpp#L83">https://github.com/llvm-mirror/clang/blob/master/lib/StaticAnalyzer/Checkers/ArrayBoundCheckerV2.cpp#L83</a></div><div> </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"><div style="font-family:Calibri,Helvetica,sans-serif;font-size:12pt;color:rgb(0,0,0)">
<div><br>
</div>
<div>2.Modify "RangedConstraintManager::<wbr>computeAdjustment()", which can support other arithmetic operators, such as '/', etc. This method can slightly increase the ability of the constraint solver, so that other false negatives can also be solved. For example:</div></div></div></blockquote><div><br></div><div>While improving the constraint manager is a good idea generally speaking, it is not a trivial task. For example the work on the ArrayBoundCheckerV2 introduced some false positives, see: <a href="https://reviews.llvm.org/D39049">https://reviews.llvm.org/D39049</a></div><div><br></div><div>The other problem is the performance. I think if you feel like improving the situation here, it would be awesome, but we should make sure not to regress the performance much and also work correctly for edge cases (overflows, signedness conversions). <br></div><div><br></div><div>Regards,</div><div>Gábor<br></div><div> </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"><div style="font-family:Calibri,Helvetica,sans-serif;font-size:12pt;color:rgb(0,0,0)">
<div><br>
</div>
<div>==============================<wbr>============================</div>
<div>
<div></div>
<div> 1 int num_foo; </div>
<div> 2 int foo()</div>
<div> 3 {</div>
<div> 4 int *ptr = 0;</div>
<div> 5 if (num_foo > 100) {</div>
<div> 6 if (num_foo / 10 < 10) </div>
<div> 7 *ptr = 0; <---- Dereference of null pointer (loaded from variable 'ptr')</div>
<div> 8 }</div>
<div> 9 }</div>
<div> 10 </div>
<div> 11 int num_goo;</div>
<div> 12 int goo()</div>
<div> 13 {</div>
<div> 14 int *ptr = 0;</div>
<div> 15 if (num_goo > 100) {</div>
<div> 16 if (num_goo < 100)</div>
<div> 17 *ptr = 0;</div>
<div> 18 }</div>
<div> 19 }</div>
<div></div>
</div>
<div>==============================<wbr>============================</div>
<div>I want to know which method is appropriate? After the constraint solver Z3 is integrated, is it necessary to implement the second methods?<br>
</div>
</div>
<div style="font-family:Calibri,Helvetica,sans-serif;font-size:12pt;color:rgb(0,0,0)">
<br>
</div>
<div id="gmail-m_5741236084448587443signature">
<div style="font-family:Calibri,Helvetica,sans-serif;font-size:12pt;color:rgb(0,0,0)">
Henry Wong</div>
<div style="font-family:Calibri,Helvetica,sans-serif;font-size:12pt;color:rgb(0,0,0)">
Qihoo 360 Codesafe Team</div>
</div>
</div>
<br>______________________________<wbr>_________________<br>
cfe-dev mailing list<br>
<a href="mailto:cfe-dev@lists.llvm.org">cfe-dev@lists.llvm.org</a><br>
<a href="http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev" rel="noreferrer" target="_blank">http://lists.llvm.org/cgi-bin/<wbr>mailman/listinfo/cfe-dev</a><br>
<br></blockquote></div><br></div></div>