<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=us-ascii">
<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);">
</div>
<div style=" margin: 0px; font-size: 15px; font-family: "Segoe UI", "Segoe UI Web (West European)", "Segoe UI", -apple-system, BlinkMacSystemFont, Roboto, "Helvetica Neue", sans-serif; color: rgb(33, 33, 33); background-color: rgb(255, 255, 255)">
<font face="Calibri,Helvetica,sans-serif" size="3" color="black"><span style=" margin: 0px; font-size: 12pt">Thanks for the explanation, Artem! <font face="Calibri,Helvetica,sans-serif" size="3" color="black"><span style=" margin: 0px">Sorry for my mistaken!
ArrayBoundCheckerV2 did</span></font><font face="Calibri,Helvetica,sans-serif" size="3" color="black"><span style=" margin: 0px"> add the `Idx >= 0</span></font><font face="Calibri,Helvetica,sans-serif" size="3" color="black"><span style=" margin: 0px">` constraint
as well.</span></font></span></font></div>
<div style=" margin: 0px; font-size: 15px; font-family: "Segoe UI", "Segoe UI Web (West European)", "Segoe UI", -apple-system, BlinkMacSystemFont, Roboto, "Helvetica Neue", sans-serif; color: rgb(33, 33, 33); background-color: rgb(255, 255, 255)">
<font face="Calibri,Helvetica,sans-serif" size="3" color="black"><span style=" margin: 0px; font-size: 12pt"><br>
</span></font></div>
<div style=" margin: 0px; font-size: 15px; font-family: "Segoe UI", "Segoe UI Web (West European)", "Segoe UI", -apple-system, BlinkMacSystemFont, Roboto, "Helvetica Neue", sans-serif; color: rgb(33, 33, 33); background-color: rgb(255, 255, 255)">
<font face="Calibri,Helvetica,sans-serif" size="3" color="black"><span style=" margin: 0px; font-size: 12pt">It make sense to me that add the constraints on the symbol according to the program semantic!</span></font></div>
<div style=" margin: 0px; font-size: 15px; font-family: "Segoe UI", "Segoe UI Web (West European)", "Segoe UI", -apple-system, BlinkMacSystemFont, Roboto, "Helvetica Neue", sans-serif; color: rgb(33, 33, 33); background-color: rgb(255, 255, 255)">
<font face="Calibri,Helvetica,sans-serif" size="3" color="black"><span style=" margin: 0px; font-size: 12pt"><br>
</span></font></div>
<div style=" margin: 0px; font-size: 15px; font-family: "Segoe UI", "Segoe UI Web (West European)", "Segoe UI", -apple-system, BlinkMacSystemFont, Roboto, "Helvetica Neue", sans-serif; color: rgb(33, 33, 33); background-color: rgb(255, 255, 255)">
<font face="Calibri,Helvetica,sans-serif" size="3" color="black"><span style=" margin: 0px; font-size: 12pt">My problem can be explained by the following diagram. IMHO, the constraints should be added on `x` after the access really occurred, this request may
be a bit picky. </span></font></div>
<div style=" margin: 0px; font-size: 15px; font-family: "Segoe UI", "Segoe UI Web (West European)", "Segoe UI", -apple-system, BlinkMacSystemFont, Roboto, "Helvetica Neue", sans-serif; color: rgb(33, 33, 33); background-color: rgb(255, 255, 255)">
<font face="Calibri,Helvetica,sans-serif" size="3" color="black"><span style=" margin: 0px; font-size: 12pt"><br>
</span></font></div>
<div style=" margin: 0px; font-size: 15px; font-family: "Segoe UI", "Segoe UI Web (West European)", "Segoe UI", -apple-system, BlinkMacSystemFont, Roboto, "Helvetica Neue", sans-serif; color: rgb(33, 33, 33); background-color: rgb(255, 255, 255)">
<font face="Calibri,Helvetica,sans-serif" size="3" color="black"><span style=" margin: 0px; font-size: 12pt"><br>
<div style=" margin: 0px"> ---------------------------------------------------------------<br>
</div>
<div style=" margin: 0px"> | BinaryOperator 0x9a0d8f0 buf[x] = 1 |<br>
</div>
<div style=" margin: 0px"> | --------------------------------------------------------------<br>
</div>
<div style=" margin: 0px"> | Ranges are empty. |<br>
</div>
<div style=" margin: 0px"> ---------------------------------------------------------------<br>
</div>
<div style=" margin: 0px"> |<br>
</div>
<div style=" margin: 0px"> \|/ ArrayBoundCheckerV2::checkLocation()<br>
</div>
<div style=" margin: 0px"> ---------------------------------------------------------------<br>
</div>
<div style=" margin: 0px"> | BinaryOperator 0x9a0d8f0 buf[x] = 1 |<br>
</div>
<div style=" margin: 0px"> | --------------------------------------------------------------<br>
</div>
<div style=" margin: 0px"> | Ranges of symbol values: |<br>
</div>
<div style=" margin: 0px"> | reg_$0<unsigned long x> : { [0, 99] } |<br>
</div>
<div style=" margin: 0px"> ----------------------------------------------------------------<br>
</div>
<div style=" margin: 0px"> |<br>
</div>
<div style=" margin: 0px"> \|/<br>
</div>
<div style=" margin: 0px"> MyOwnChecker::checkLocation()<br>
</div>
<div style=" margin: 0px"> Want to get the original constraint info on `x`, however the constraint information has changed.<br>
</div>
<div style=" margin: 0px"> ...<br>
</div>
<div style=" margin: 0px"> |<br>
</div>
<div style=" margin: 0px"> \|/<br>
</div>
<div style=" margin: 0px"> ----------------------------------------------------------------<br>
</div>
<div style=" margin: 0px"> | BinaryOperator 0x9a0d8f0 buf[x] = 1 |<br>
</div>
<div style=" margin: 0px"> | PostStore |<br>
</div>
<div style=" margin: 0px"> | ---------------------------------------------------------------<br>
</div>
<div style=" margin: 0px"> | Ranges of symbol values: |<br>
</div>
<div style=" margin: 0px"> | reg_$0<unsigned long x> : { [0, 99] } |<br>
</div>
<div style=" margin: 0px"> ---------------------------------------------------------------<br>
</div>
<div style=" margin: 0px"> |<br>
</div>
\|/ The constraint should be added to `x` after the access really happens.<br>
</span></font></div>
<div style=" margin: 0px; font-size: 15px; font-family: "Segoe UI", "Segoe UI Web (West European)", "Segoe UI", -apple-system, BlinkMacSystemFont, Roboto, "Helvetica Neue", sans-serif; color: rgb(33, 33, 33); background-color: rgb(255, 255, 255)">
<font face="Calibri,Helvetica,sans-serif" size="3" color="black"><span style=" margin: 0px; font-size: 12pt"><br>
</span></font></div>
<div style=" margin: 0px; font-size: 15px; font-family: "Segoe UI", "Segoe UI Web (West European)", "Segoe UI", -apple-system, BlinkMacSystemFont, Roboto, "Helvetica Neue", sans-serif; color: rgb(33, 33, 33); background-color: rgb(255, 255, 255)">
<font face="Calibri,Helvetica,sans-serif" size="3" color="black"><span style=" margin: 0px; font-size: 12pt"><span style=" margin: 0px; background-color: white">My problem has been solved by moving</span><span style=" margin: 0px; background-color: white"> the
code logic of</span><span style=" margin: 0px; background-color: white"> `MyOwnChecker::checkLocation()</span><span style=" margin: 0px; background-color: white">` to `ArrayBoundCheckerV2::checkLocation()</span><span style=" margin: 0px; background-color: white">`.</span><br>
</span></font></div>
<div style=" margin: 0px; font-size: 15px; font-family: "Segoe UI", "Segoe UI Web (West European)", "Segoe UI", -apple-system, BlinkMacSystemFont, Roboto, "Helvetica Neue", sans-serif; color: rgb(33, 33, 33); background-color: rgb(255, 255, 255)">
<font face="Calibri,Helvetica,sans-serif" size="3" color="black"><span style=" margin: 0px; font-size: 12pt"><br>
</span></font></div>
<div style=" margin: 0px; font-size: 15px; font-family: "Segoe UI", "Segoe UI Web (West European)", "Segoe UI", -apple-system, BlinkMacSystemFont, Roboto, "Helvetica Neue", sans-serif; color: rgb(33, 33, 33); background-color: rgb(255, 255, 255)">
<div style=" margin: 0px"><font face="Calibri,Helvetica,sans-serif" size="3" color="black"><span style=" margin: 0px; font-size: 12pt">Henry Wong</span></font></div>
<div style=" margin: 0px"><font face="Calibri,Helvetica,sans-serif" size="3" color="black"><span style=" margin: 0px; font-size: 12pt">Qihoo 360 Codesafe Team</span></font></div>
</div>
<div id="signature">
<div style="font-family:Calibri,Helvetica,sans-serif; font-size:12pt; color:rgb(0,0,0)">
</div>
</div>
<hr style="display:inline-block;width:98%" tabindex="-1">
<div id="divRplyFwdMsg" dir="ltr"><font face="Calibri, sans-serif" style="font-size:11pt" color="#000000"><b>From:</b> Artem Dergachev <noqnoqneo@gmail.com><br>
<b>Sent:</b> Thursday, July 12, 2018 3:00<br>
<b>To:</b> Henry Wong; cfe-dev@lists.llvm.org<br>
<b>Subject:</b> Re: [cfe-dev] [Analyzer] ArrayBoundCheckerV2: Why the analyzer add the constraint `Idx < ArraySize` after element access?</font>
<div> </div>
</div>
<meta content="text/html; charset=Windows-1252">
<div style="background-color:#FFFFFF">If 'x' is 100 or greater, it'd mean that undefined behavior has already occured, and it's pointless to explore that path further.<br>
<br>
Same with 'x' being less than 0, so the checker should have added that as well.<br>
<br>
So i believe that this is a valid behavior. A similar approach is taken by, say, DivZeroChecker that refutes the "y == 0" patch after "x / y" is evaluated. NullDereferenceChecker also assumes that all dereferenced pointers are non-null.<br>
<br>
If they can prove that the operation is indeed unsafe on the current path, then the assumption would fail, and these checkers would report a warning instead.<br>
<br>
What sort of problem are you having with these assumptions? Why are they affecting your checker? With constraints it shouldn't normally ever be an issue, because adding constraints doesn't really "mutate" the program state, it just "clarifies" it.<br>
<br>
<div class="x_moz-cite-prefix">On 7/11/18 3:27 AM, Henry Wong via cfe-dev wrote:<br>
</div>
<blockquote type="cite"><style type="text/css" style="display:none">
<!--
p
{margin-top:0;
margin-bottom:0}
-->
</style>
<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)">
<br>
</div>
<div style="font-family:Calibri,Helvetica,sans-serif; font-size:12pt; color:rgb(0,0,0)">
For the code below, the `ArrayBoundCheckerV2` will add the constraint `x < 100` after the `buf[x] = 1`, see
<a href="https://reviews.llvm.org/D23112" id="LPlnk612572">https://reviews.llvm.org/D23112</a>. </div>
<div style="font-family:Calibri,Helvetica,sans-serif; font-size:12pt; color:rgb(0,0,0)">
```</div>
<div style="font-family:Calibri,Helvetica,sans-serif; font-size:12pt; color:rgb(0,0,0)">
<span>void test_assume_after_access(unsigned long x) {<br>
</span>
<div> int buf[100];<br>
</div>
<div> buf[x] = 1;<br>
</div>
<div> clang_analyzer_eval(x <= 99); // expected-warning{{TRUE}}<br>
</div>
<span>}</span><br>
</div>
<div style="font-family:Calibri,Helvetica,sans-serif; font-size:12pt; color:rgb(0,0,0)">
```</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)">
<span style="background-color:rgb(255,255,255); display:inline!important">1.<span> </span></span><span style="background-color:rgb(255,255,255); display:inline!important">What is the purpose for doing this? </span></div>
<div style="font-family:Calibri,Helvetica,sans-serif; font-size:12pt; color:rgb(0,0,0)">
<span style="background-color:rgb(255,255,255); display:inline!important">2. why not add `x >= 0</span><span style="background-color:rgb(255,255,255); display:inline!important">` as well?</span><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)">
I <span style="color:rgb(0,0,0); font-family:Calibri,Helvetica,sans-serif; font-size:12pt">
used</span><span style="color:rgb(0,0,0); font-family:Calibri,Helvetica,sans-serif; font-size:12pt"> `checkLocation()</span><span style="color:rgb(0,0,0); font-family:Calibri,Helvetica,sans-serif; font-size:12pt">`, same as `ArrayBoundCheckerV2</span><span style="color:rgb(0,0,0); font-family:Calibri,Helvetica,sans-serif; font-size:12pt">`,
in my</span><span style="color:rgb(0,0,0); font-family:Calibri,Helvetica,sans-serif; font-size:12pt"> own
</span><span style="color:rgb(0,0,0); font-family:Calibri,Helvetica,sans-serif; font-size:12pt">c</span><span style="color:rgb(0,0,0); font-family:Calibri,Helvetica,sans-serif; font-size:12pt">hecker too</span><span style="color:rgb(0,0,0); font-family:Calibri,Helvetica,sans-serif; font-size:12pt">.
</span><span style="color:rgb(0,0,0); font-family:Calibri,Helvetica,sans-serif; font-size:12pt">Due to the uncertain calling order,</span><span style="color:rgb(0,0,0); font-family:Calibri,Helvetica,sans-serif; font-size:12pt"> I got the
</span><span style="color:rgb(0,0,0); font-family:Calibri,Helvetica,sans-serif; font-size:12pt">wrong constraints on `</span><span style="color:rgb(0,0,0); font-family:Calibri,Helvetica,sans-serif; font-size:12pt">x` in my own checker.
</span><span style="color:rgb(0,0,0); font-family:Calibri,Helvetica,sans-serif; font-size:12pt">T</span><span style="color:rgb(0,0,0); font-family:Calibri,Helvetica,sans-serif; font-size:12pt">hat's why I
</span><span style="color:rgb(0,0,0); font-family:Calibri,Helvetica,sans-serif; font-size:12pt">pay attention to this problem.</span></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)">
Thanks in advance!</div>
<div style="font-family:Calibri,Helvetica,sans-serif; font-size:12pt; color:rgb(0,0,0)">
<br>
</div>
<div id="x_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>
<br>
<fieldset class="x_mimeAttachmentHeader"></fieldset>
<pre class="x_moz-quote-pre">_______________________________________________
cfe-dev mailing list
<a class="x_moz-txt-link-abbreviated" href="mailto:cfe-dev@lists.llvm.org">cfe-dev@lists.llvm.org</a>
<a class="x_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>
</div>
</body>
</html>