<html><head><meta http-equiv="Content-Type" content="text/html; charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">On 12 Apr 2021, at 03:30, Manas <<a href="mailto:manas18244@iiitd.ac.in" class="">manas18244@iiitd.ac.in</a>> wrote:<br class=""><div><blockquote type="cite" class=""><div class=""><div class="">I went through the code in RangeConstraintManager.cpp and comprehended<br class="">about the constraint manager overall. canReasonAbout() (line: 1948)<br class="">shows which all operations are left being implemented (namely, Mul, Div, <br class="">Shl, Shr, and also the Xor operator). I have added these into the<br class="">proposal.<br class=""></div></div></blockquote>There is also an elephant in the room, - Add and Sub.<br class=""><blockquote type="cite" class=""><div class=""><div class=""><br class=""><blockquote type="cite" class="">However, we have found another application for z3 - refute produced warnings. When we are about to report a new warning, we can check that constraints are sat/unsat and discard the warning in the latter case. This happens way less frequently and good in terms of performance. Alas, the majority of users have static analyzer build without z3, and some false positives warnings sneak in.<br class=""><br class="">So, there are two main directions that I see:<br class="">Figure out cases when z3 refutation works better than the built-in fast solver. <br class="">Run the analyzer in both modes and analyze the difference. Usually it’s under 10 warnings, so it won’t be very tedious.<br class=""></blockquote>I have added this into the proposal too.<br class=""><br class=""><blockquote type="cite" class="">Add reasoning about range-based binary operations. <br class="">If we know ranges for symbols or symbolic expressions x and y, we can often reason about possible ranges for x OP y, where OP is some binary operator. At the moment, we have support for &, |, and % (it’s a bit weird set of operators, but it was driven by reported false positives).<br class=""></blockquote>Going through D80117, D79434, and D79336, one of the first things was to<br class="">bisect the condition based on the sign of symbols. Followed by<br class="">appropriate handling of upper/lower bounds for the expression.<br class=""></div></div></blockquote><div>Correct, we should always care about the bit vector nature of integers.</div><br class=""><blockquote type="cite" class=""><div class=""><div class=""><br class="">Regarding the TODO #1 (L:931) and TODO #2 (L:936) in RangeConstraintManager.cpp, <br class="">should I put these into the proposal too? (this to be done for other binary <br class="">operations as well apart from {rem, and, or} operations)<br class=""></div></div></blockquote>It didn’t seem to cause any performance problems so far, and I’d say this is not a priority right now.</div><div><br class=""></div><div><blockquote type="cite" class=""><div class=""><div class=""><br class="">These todos are related to lazy implemetation for VisitBinaryOperator and<br class="">caching mechanism for analysis of nested expressions.<br class=""><br class=""><blockquote type="cite" class="">It’s a logical continuation of my work:<br class="">D86465, D82445, D83286, D82381, D80117, D79434, and D79336<br class=""><br class=""></blockquote>I went through these patches as well in order to understand the workflow<br class="">and things which have been done so far.<br class=""><br class="">The description of project also mentions about a unit-test framework.<br class="">Can I get more details regarding this?<br class=""></div></div></blockquote>As you looked through those patches, you probably noticed that we usually add more checks into <b class="">constant-folding.c </b>test.</div><div>It is pretty good, but it would be much better to have a dedicated section of unit-tests especially because the solver is pretty isolated and doesn’t really depend on AST (only on APSInt’s actually, but this is easy to overcome, you can see how it is done in <b class="">RangeSetTest.cpp</b>).</div><div><br class=""></div><div>I guess my idea of perfect unit tests for the solver would be to have a special class for test symbols that we can construct like this <font face="Menlo" class="">TestSymbol x = {{0, 10}, {20, 40}}</font> with overloaded operators that call solver, so we can do stuff like this: <font face="Menlo" class="">TestSymbol z = x + y; /* check for expected ranges in z */</font></div><div>This way the actual tests are very straightforward, easy to add new ones, easy to read and maintain. And all the nitty gritty should be hidden inside of the test class and the test symbol class. The main challenge here is to design this testing framework, so it is as invisible as possible.</div><div><blockquote type="cite" class=""><div class=""><div class=""><br class="">I have drafted the initial version of my proposal here.<br class="">(<a href="https://docs.google.com/document/d/1ts_jxi1eAPGgeSzy5cs1dwZDcrmCHao8skZT8yWtOPI/edit?usp=sharing" class="">https://docs.google.com/document/d/1ts_jxi1eAPGgeSzy5cs1dwZDcrmCHao8skZT8yWtOPI/edit?usp=sharing</a>)<br class=""></div></div></blockquote>Awesome, I’ll take a look and respond in comments.</div><div><br class=""><blockquote type="cite" class=""><div class=""><div class=""><br class="">Thank you<br class="">-- <br class="">Manas<br class="">CSAM Undergraduate | 2022<br class="">IIIT-Delhi, India<br class=""></div></div></blockquote></div><br class=""><div class="">Cheers,</div><div class="">Valeriy</div></body></html>