<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=gb2312">
<style type="text/css" style="display:none;"> P {margin-top:0;margin-bottom:0;} </style>
</head>
<body 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.(http://clang-developers.42468.n3.nabble.com/improving-the-ArrayBoundChecker-td4037769.html#a4037803). <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><br>
</div>
<div>2.Modify "RangedConstraintManager::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><br>
</div>
<div>==========================================================</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>==========================================================</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="signature">
<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>
</body>
</html>