<div dir="ltr">Hi,<div><br></div><div>I made some small changes to the Z3ConstraintManager, so it could print the SMT formula and the only thing I got was:</div><div><br></div><div><div>(declare-fun $0 () (_ BitVec 32))</div><div>(assert (not (= $0 #x00000000)))</div></div><div><br></div><div><div> Constraints:</div><div> reg_$0<unsigned int width> : (not (= $0 #x00000000))</div></div><div><br></div><div>which comes from the core.DivideZero checker.</div><div><br></div><div>Maybe it's dropping the "complex" constraint as you said? Both paths should have the (i % width == 0) constraint.</div><div><br></div><div>Thank you,</div><div><br></div><div class="gmail_extra"><br><div class="gmail_quote">2018-03-22 20:34 GMT+00:00 George Karpenkov <span dir="ltr"><<a href="mailto:ekarpenkov@apple.com" target="_blank">ekarpenkov@apple.com</a>></span>:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div style="word-wrap:break-word;line-break:after-white-space">Hi Mikhail,<div><br></div><div>That’s a good improvement!</div><div><br></div><div>I think an awesome next step would be to see whether the analyzer already has the formula required to solve your motivational example.</div><div>This would be a preliminary feasibility study: if the formula is there, it’s just a matter of converting it and giving it to Z3, and otherwise,</div><div>the exercise is much harder and might require substantial changes.</div><div><br></div><div>Perhaps an easiest way to see what formulas the analyzer has is to launch it with an extra flag</div><div>`-Xclang -analyzer-viz-egraph-graphviz` which would dump a graph in a GraphViz format containing all the information analyzer has along all the states.</div><div><br></div><div>This is important for judging feasibility, as it might be the case that analyzer at some point decides to get rid of the “complex” constraint.</div><div>While it would be possible to change that, that would be a second step of the project,</div><div>and for preliminary evaluation a simpler example would be needed.</div><div><br></div><div>Also, the information above could be helpful for structuring the project: a first stage would be checking most trivial examples, a second stage would be seeing how far</div><div>can we get with only minimal modifications to the core.</div><div><br></div><div>Regards,</div><div>George</div><div><div class="m_3480453752466103086h5"><div><div><br><blockquote type="cite"><div>On Mar 22, 2018, at 1:19 PM, Mikhail Ramalho <<a href="mailto:mikhail.ramalho@gmail.com" target="_blank">mikhail.ramalho@gmail.com</a>> wrote:</div><br class="m_3480453752466103086m_4673560789215137001Apple-interchange-newline"><div><div dir="ltr">Hi all,<div><br></div><div>Thank you for the feedback, George and Dominic.</div><div><br></div><div>I updated my proposal with an example, showing the encoded SMT formula for the program and a brief explanation of the verification process. I used a simplified program from a bug report in Bugzilla.</div><div><br></div><div>May I ask for some feedback in this section?</div><div><br></div><div>~</div><div><br></div><div>I addressed most of the comments, except for: </div><div><span style="color:rgb(51,51,51);font-family:Arial,sans-serif,sans;font-size:13px;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:left;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial;float:none;display:inline"><br></span></div><div><span style="color:rgb(51,51,51);font-family:Arial,sans-serif,sans;font-size:13px;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:left;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial;float:none;display:inline"><span style="color:rgb(51,51,51);font-family:Arial,sans-serif,sans;font-size:13px;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:left;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial;float:none;display:inline">George: stretch goals are great, but for now I think it would be better to focus on writing a considerably more detailed proposal on how and why the main goal would be implemented.<span> </span></span></span></div><div><span style="color:rgb(51,51,51);font-family:Arial,sans-serif,sans;font-size:13px;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:left;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial;float:none;display:inline"><span style="color:rgb(51,51,51);font-family:Arial,sans-serif,sans;font-size:13px;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:left;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial;float:none;display:inline"><span><br></span></span></span></div><div><font color="#333333" face="Arial, sans-serif, sans">I tried to explain the motivation in the Overview section, do you think a motivation section would be better? </font></div><div><font color="#333333" face="Arial, sans-serif, sans"><br></font></div><div><font color="#333333" face="Arial, sans-serif, sans">Regarding the how, I'll have another look in the BugReportVisitor and update the proposal with a more concrete solution.</font></div><div><font color="#333333" face="Arial, sans-serif, sans"><br></font></div><div><font color="#333333" face="Arial, sans-serif, sans">Thank you,</font></div><div><br></div><div class="gmail_extra"><br><div class="gmail_quote">2018-03-21 17:54 GMT+00:00 George Karpenkov <span dir="ltr"><<a href="mailto:ekarpenkov@apple.com" target="_blank">ekarpenkov@apple.com</a>></span>:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div style="word-wrap:break-word;line-break:after-white-space">Hi Mikhail,<div><br></div><div>I’ve added some feedback.</div><div>Overall, I think we should be aiming for something more low-level and concrete:</div><div>adding examples with explanations would be a great improvement.</div><div><br></div><div>Regards,</div><div>George<div><div class="m_3480453752466103086m_4673560789215137001m_3797644012230859096h5"><br><div><br><blockquote type="cite"><div>On Mar 21, 2018, at 10:12 AM, Mikhail Ramalho <<a href="mailto:mikhail.ramalho@gmail.com" target="_blank">mikhail.ramalho@gmail.com</a>> wrote:</div><br class="m_3480453752466103086m_4673560789215137001m_3797644012230859096m_8959840794667446807Apple-interchange-newline"><div><div dir="ltr">Hi all,<div><br></div><div>I've written a first draft of my proposal:</div><div><br></div><div><a href="https://docs.google.com/document/d/1-zNSv0l4WyoxYpJUAw8LFnQq_TY4AGjIpPu1VPkmO-g/edit?usp=sharing" target="_blank">https://docs.google.com/docume<wbr>nt/d/1-zNSv0l4WyoxYpJUAw8LFnQq<wbr>_TY4AGjIpPu1VPkmO-g/edit?usp=s<wbr>haring</a><br></div><div><br></div><div>I've added a few comments in places I think need improvement. </div><div><br></div><div>May I ask the community to have a look and give some feedback? </div><div><br></div><div>Thank you,</div><div><br></div></div><div class="gmail_extra"><br><div class="gmail_quote">2018-03-12 18:24 GMT+00:00 George Karpenkov <span dir="ltr"><<a href="mailto:ekarpenkov@apple.com" target="_blank">ekarpenkov@apple.com</a>></span>:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div style="word-wrap:break-word;line-break:after-white-space">Hi Mikhail,<div><br></div><div>I’m assuming Dominic have answered your questions regarding the point (3).</div><div><br></div><div>On point (1) I have recently sent an email on the list answering, I believe, to essentially the same question:</div><div><a href="http://lists.llvm.org/pipermail/cfe-dev/2018-March/057064.html" target="_blank">http://lists.llvm.org/pipermai<wbr>l/cfe-dev/2018-March/057064.ht<wbr>ml</a></div><div><br></div><div>(yes, unfortunately we do not have better archives, so messages might be often hard to track)<br><div><span><br><blockquote type="cite"><div><div dir="ltr" style="font-family:Helvetica;font-size:12px;font-style:normal;font-variant-caps:normal;font-weight:normal;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px"><div>2. I still don't quite understand how dynamic memory track works in the analyzer, is the double checker expected to work for pointers and dynamic memory as well? I'm assuming yes here and that Z3ConstraintManager <span style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:small;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);float:none;display:inline">might need to be extended somehow (a plan will be added to the proposal).</span></div></div></div></blockquote><div><br></div></span><div>I think here we should get the extra precision for free by adding a bug reporter visitor, as described in the email thread I have linked to.</div><div><br></div><div>Please feel free to ask any further questions, bug reporter visitors are quite messy in the analyzer.</div><div><br></div><div>Regards,</div><div>George</div><br><blockquote type="cite"><div><span><div dir="ltr" style="font-family:Helvetica;font-size:12px;font-style:normal;font-variant-caps:normal;font-weight:normal;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px"><div><span style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:small;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);float:none;display:inline"><br></span></div><div><span style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:small;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);float:none;display:inline">~</span></div><div><span style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:small;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);float:none;display:inline"><br></span></div><div><span style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:small;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);float:none;display:inline">3. This is a list of the TODOs in <span style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:small;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);float:none;display:inline">Z3ConstraintManager, from more important to less important, in my opinion. I just want to know if the analyzer's developers (and the project mentor) agree with this list, as it might go into my proposal:</span></span></div><div><span style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:small;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);float:none;display:inline"><span style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:small;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);float:none;display:inline"><br></span></span></div><div><span style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:small;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);float:none;display:inline"><span style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:small;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);float:none;display:inline">3.1. Don't assume nearest ties to even rounding mode: currently, only rounding to even is supported, even if the code changes the rounding mode using fesetround.</span></span></div><div><span style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:small;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);float:none;display:inline"><span style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:small;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);float:none;display:inline"><br></span></span></div><div><span style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:small;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);float:none;display:inline"><span style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:small;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);float:none;display:inline">3.2. Don't add all the constraints, only the relevant ones: adding unnecessary constraints will slowdown the solver.</span></span></div><div><span style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:small;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);float:none;display:inline"><span style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:small;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);float:none;display:inline"><br></span></span></div><div><span style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:small;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);float:none;display:inline"><span style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:small;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);float:none;display:inline">3.3. Refactor doTypeConversion to use built-in conversion functions (</span></span>Refactor to Sema::FindCompositePointerType<wbr>(), and Sema::CheckCompareOperands(); <wbr>Refine behavior for invalid type casts)</div><div><span style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:small;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);float:none;display:inline"><span style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:small;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);float:none;display:inline">3.4. Refactor doIntTypeConversion to use Sema::handleIntegerConversion(<wbr>)</span></span></div><div><span style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:small;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);float:none;display:inline"><span style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:small;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);float:none;display:inline">3.5. Refactor doFloatTypeConversion to use Sema::handleFloatConversion()</span></span></div><div><br></div><div>I bundled this together because, although the conversion seems incomplete (based on the comments), it's about removing duplicated code.</div><div><br></div><div>3.6. Refactor getAPSIntType(const llvm::APSInt &Int) const to put elsewhere.</div><div><br></div><div>~</div><div><br></div><div>Thank you,</div><div><br></div></div><div class="gmail_extra" style="font-family:Helvetica;font-size:12px;font-style:normal;font-variant-caps:normal;font-weight:normal;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px"><br><div class="gmail_quote">2018-02-24 1:03 GMT+00:00 Devin Coughlin<span class="m_3480453752466103086m_4673560789215137001m_3797644012230859096m_8959840794667446807m_-5653580683305685986Apple-converted-space"> </span><span dir="ltr"><<a href="mailto:dcoughlin@apple.com" target="_blank">dcoughlin@apple.com</a>></span><wbr>:<br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-style:solid;border-left-color:rgb(204,204,204);padding-left:1ex"><span><br><br>> On Feb 23, 2018, at 9:29 AM, Mikhail Ramalho via cfe-dev <<a href="mailto:cfe-dev@lists.llvm.org" target="_blank">cfe-dev@lists.llvm.org</a>> wrote:<br>><br>> I also have a question about the proposal. I understand that ideas about the project will be discussed in the mailing list. However, once that's settled and I write my first draft proposal, should I send it to the mailing list for discussion again or should I send it only to the mentor?<br><br></span>Please make sure to keep email discussions on the mailing list rather than just personal email. This is a topic that members of the community will be interested in and will have valuable feedback on.<br><span class="m_3480453752466103086m_4673560789215137001m_3797644012230859096m_8959840794667446807m_-5653580683305685986HOEnZb"><font color="#888888"><br>Devin<br><br></font></span></blockquote></div><br><br clear="all"><div><br></div>--<span class="m_3480453752466103086m_4673560789215137001m_3797644012230859096m_8959840794667446807m_-5653580683305685986Apple-converted-space"> </span><br><div class="m_3480453752466103086m_4673560789215137001m_3797644012230859096m_8959840794667446807m_-5653580683305685986gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><div><br></div><div>Mikhail Ramalho.</div></div></div></div></span><span><span style="font-family:Helvetica;font-size:12px;font-style:normal;font-variant-caps:normal;font-weight:normal;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;float:none;display:inline!important">______________________________<wbr>_________________</span><br style="font-family:Helvetica;font-size:12px;font-style:normal;font-variant-caps:normal;font-weight:normal;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px"><span style="font-family:Helvetica;font-size:12px;font-style:normal;font-variant-caps:normal;font-weight:normal;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;float:none;display:inline!important">cfe-dev mailing list</span><br style="font-family:Helvetica;font-size:12px;font-style:normal;font-variant-caps:normal;font-weight:normal;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px"><a href="mailto:cfe-dev@lists.llvm.org" style="font-family:Helvetica;font-size:12px;font-style:normal;font-variant-caps:normal;font-weight:normal;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px" target="_blank">cfe-dev@lists.llvm.org</a><br style="font-family:Helvetica;font-size:12px;font-style:normal;font-variant-caps:normal;font-weight:normal;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px"><a href="http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev" style="font-family:Helvetica;font-size:12px;font-style:normal;font-variant-caps:normal;font-weight:normal;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px" target="_blank">http://lists.llvm.org/cgi-bin/<wbr>mailman/listinfo/cfe-dev</a></span></div></blockquote></div><br></div></div></blockquote></div><br><br clear="all"><div><br></div>-- <br><div class="m_3480453752466103086m_4673560789215137001m_3797644012230859096m_8959840794667446807gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><div><br></div><div>Mikhail Ramalho.</div></div></div>
</div>
</div></blockquote></div><br></div></div></div></div></blockquote></div><br><br clear="all"><div><br></div>-- <br><div class="m_3480453752466103086m_4673560789215137001m_3797644012230859096gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><div><br></div><div>Mikhail Ramalho.</div></div></div>
</div></div>
</div></blockquote></div><br></div></div></div></div></blockquote></div><br><br clear="all"><div><br></div>-- <br><div class="m_3480453752466103086gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><div><br></div><div>Mikhail Ramalho.</div></div></div>
</div></div>