<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="">Great! Don’t forget to submit the PDF through the official website!<br class=""><div><br class=""><blockquote type="cite" class=""><div class="">On Mar 26, 2018, at 9:13 AM, Mikhail Ramalho <<a href="mailto:mikhail.ramalho@gmail.com" class="">mikhail.ramalho@gmail.com</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><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; -webkit-text-stroke-width: 0px;" class="">Hi all,<div class=""><br class=""></div><div class="">I expanded the report quite a bit over the weekend, adding the suggested example, writing a bit more about the current state of the analyzer and implementing the suggestions (thank you George and Artem).</div><div class=""><br class=""></div><div class=""><span style="color: rgb(34, 34, 34); font-family: arial, sans-serif; font-size: 12.8px; 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;" class="">Any feedback is welcome! I plan to submit the report tomorrow, mid-afternoon.</span><br class=""></div><div class=""><span style="color: rgb(34, 34, 34); font-family: arial, sans-serif; font-size: 12.8px; 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;" class=""><br class=""></span></div><div class=""><span style="color: rgb(34, 34, 34); font-family: arial, sans-serif; font-size: 12.8px; 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;" class="">Thank you,</span></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; -webkit-text-stroke-width: 0px;"><br class=""><div class="gmail_quote">2018-03-23 21:54 GMT+00:00 George Karpenkov<span class="Apple-converted-space"> </span><span dir="ltr" class=""><<a href="mailto:ekarpenkov@apple.com" target="_blank" class="">ekarpenkov@apple.com</a>></span>:<br class=""><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;"><div style="word-wrap: break-word; line-break: after-white-space;" class="">Hi Mikhail,<div class=""><br class=""></div><div class="">Indeed, it seems that the constraint manager is more eager to throw out complex constraints than I’ve anticipated initially.</div><div class="">It might be partly a good thing: now we need to know that evaluating disabling this heuristic and measuring a change in footprint</div><div class="">on a large number of project needs to be a part of the schedule.</div><div class="">An example where a change in this optimization is required would be also beneficial for proposal.</div><div class=""><br class=""></div><div class="">Now onto the example.</div><div class=""><br class=""></div><div class="">1. Unlike SV-COMP, the analyzer treats “assert” as “assume”. So you would need to e.g. perform null pointer dereference to see whether there’s an error.</div><div class="">(or use a debug checker and a special function, consult tests for those)</div><div class="">2. The following function seems to give the desired behavior:</div><div class=""><br class=""></div><div class=""><div class=""><div class="">int foo(int x) {</div><div class=""> <span class="Apple-converted-space"> </span>int *z = 0;</div><div class=""> <span class="Apple-converted-space"> </span>if ((x & 1) && ((x & 1) ^ 1))</div><div class=""> <span class="Apple-converted-space"> </span>return *z;</div><div class=""> <span class="Apple-converted-space"> </span>return 0;</div><div class="">}</div></div><div class=""><br class=""></div><div class="">In a sense that the analyzer reports a false positive (if x & 1 is true, last bit is one, but then (x & 1) is the last bit and (x & 1) ^ 1 should be zero),</div><div class="">it is non-obvious, and just using Z3 with constraints present in the graph should be sufficient.</div><div class=""><br class=""></div><div class="">Regards,</div><div class="">George</div><div class=""><div class="h5"><div class=""><br class=""><blockquote type="cite" class=""><div class="">On Mar 23, 2018, at 12:48 PM, Mikhail Ramalho <<a href="mailto:mikhail.ramalho@gmail.com" target="_blank" class="">mikhail.ramalho@gmail.com</a>> wrote:</div><br class="m_-6481325030509720384Apple-interchange-newline"><div class=""><div dir="ltr" class="">Hi,<div class=""><br class=""></div><div class="">Just a quick update: I still haven't found a suitable case to add to the report but I tried to address every other comment there. </div><div class=""><br class=""></div><div class="">Any feedback is welcome!</div><div class=""><br class=""></div><div class="">Thank you,</div><div class=""><br class=""></div></div><div class="gmail_extra"><br class=""><div class="gmail_quote">2018-03-23 18:39 GMT+00:00 Mikhail Ramalho<span class="Apple-converted-space"> </span><span dir="ltr" class=""><<a href="mailto:mikhail.ramalho@gmail.com" target="_blank" class="">mikhail.ramalho@gmail.com</a>></span>:<br class=""><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;"><div dir="ltr" class="">Indeed the constraints start to appear when there are multiplications/divisions/rema<wbr class="">inders, but I noticed that it only prints the constraints when it's able to solve them.<div class=""><br class=""></div><div class="">Maybe in a higher level it's dropping constraints without querying if the solver can handle it?<br class=""></div><div class=""><br class=""></div><div class="">I'll keep looking into it.</div><div class="gmail_extra"><div class=""><div class="m_-6481325030509720384h5"><br class=""><div class="gmail_quote">2018-03-23 18:25 GMT+00:00 Artem Dergachev<span class="Apple-converted-space"> </span><span dir="ltr" class=""><<a href="mailto:noqnoqneo@gmail.com" target="_blank" class="">noqnoqneo@gmail.com</a>></span>:<br class=""><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;"><div text="#000000" bgcolor="#FFFFFF" class="">Try making assumptions over 2 * x, these should work if i recall correctly.<div class=""><div class="m_-6481325030509720384m_-2406771488922912429m_7462020983193081322h5"><br class=""><br class=""><div class="m_-6481325030509720384m_-2406771488922912429m_7462020983193081322m_-4451861523552279669moz-cite-prefix">On 3/23/18 10:51 AM, Mikhail Ramalho via cfe-dev wrote:<br class=""></div><blockquote type="cite" class=""><div dir="ltr" class="">Hi,<div class="gmail_extra"><br class=""><div class="gmail_quote"><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;"><div style="word-wrap: break-word;" class=""><div class=""><div class=""><br class=""></div><div class="">We would have to find an easier example first, where the core modification are not necessary.</div><div class="">For the easier example: I think it would have to be simple arithmetics over integers, even negation would work.</div><div class="">The current solver can not handle any relational constraints.</div><div class=""><br class=""></div></div></div></blockquote><div class=""><br class=""></div><div class="">I'm having some problems finding a simple benchmark where the constraints are not dropped.</div><div class=""><br class=""></div><div class="">For instance, consider the following (safe) program:</div><div class=""><br class=""></div><div class=""><div class="">void foo(unsigned x, unsigned y)</div><div class="">{</div><div class=""> <span class="Apple-converted-space"> </span>if (x > y)</div><div class=""> <span class="Apple-converted-space"> </span>return;</div><div class=""><br class=""></div><div class=""> <span class="Apple-converted-space"> </span>int base;</div><div class=""><br class=""></div><div class=""> <span class="Apple-converted-space"> </span>if (x <= y)</div><div class=""> <span class="Apple-converted-space"> </span>base = 1;</div><div class=""><br class=""></div><div class=""> <span class="Apple-converted-space"> </span>assert(base == 1);</div><div class="">}</div></div><div class=""><br class=""></div><div class="">But the constraints are empty (both when I print the graph and the SMT formula). I'm calling the analyzer:</div><div class=""><br class=""></div><div class="">$ ~/myclang/bin/clang --analyze -Xclang -analyzer-viz-egraph-graphviz -Xanalyzer -analyzer-checker=debug.DumpCF<wbr class="">G main2.c<br class=""></div><div class=""><br class=""></div><div class="">I'm assuming that the constraints are being dropped somehow but is there any other way to check it?</div><div class=""><br class=""></div><div class="">Btw, I'm using the head of the release_60 branch.</div><div class=""><br class=""></div><div class="">Thank you,</div><div class=""> </div><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;"><div style="word-wrap: break-word;" class=""><div class=""><div class="">BTW instead of looking into the Z3ConstraintManager I think it would be easier to look at the exploded graph (using the option I have previously described)</div><div class="">and see what formulas are mentioned there.</div><div class=""><div class="m_-6481325030509720384m_-2406771488922912429m_7462020983193081322m_-4451861523552279669gmail-m_-8638169037548414962gmail-h5"><br class=""><blockquote type="cite" class=""><div class=""><div dir="ltr" class=""><div class=""><br class=""></div><div class="">Thank you,</div><div class=""><br class=""></div><div class="gmail_extra"><br class=""><div class="gmail_quote">2018-03-22 20:34 GMT+00:00 George Karpenkov<span class="Apple-converted-space"> </span><span dir="ltr" class=""><<a href="mailto:ekarpenkov@apple.com" target="_blank" class="">ekarpenkov@apple.com</a>></span>:<br class=""><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;"><div style="word-wrap: break-word;" class="">Hi Mikhail,<div class=""><br class=""></div><div class="">That’s a good improvement!</div><div class=""><br class=""></div><div class="">I think an awesome next step would be to see whether the analyzer already has the formula required to solve your<span class="Apple-converted-space"> </span> <span class="Apple-converted-space"> </span><span class="Apple-converted-space"> </span> <span class="Apple-converted-space"> </span><span class="Apple-converted-space"> </span> <span class="Apple-converted-space"> </span><span class="Apple-converted-space"> </span> <span class="Apple-converted-space"> </span><span class="Apple-converted-space"> </span> <span class="Apple-converted-space"> </span><span class="Apple-converted-space"> </span> <span class="Apple-converted-space"> </span><span class="Apple-converted-space"> </span> <span class="Apple-converted-space"> </span><span class="Apple-converted-space"> </span> <span class="Apple-converted-space"> </span><span class="Apple-converted-space"> </span> <span class="Apple-converted-space"> </span><span class="Apple-converted-space"> </span> <span class="Apple-converted-space"> </span><span class="Apple-converted-space"> </span> <span class="Apple-converted-space"> </span><span class="Apple-converted-space"> </span> <span class="Apple-converted-space"> </span><span class="Apple-converted-space"> </span> <span class="Apple-converted-space"> </span>motivational example.</div><div class="">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 class="">the exercise is much harder and might require substantial changes.</div><div class=""><br class=""></div><div class="">Perhaps an easiest way to see what formulas the analyzer has is to launch it with an extra flag</div><div class="">`-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 class=""><br class=""></div><div class="">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 class="">While it would be possible to change that, that would be a second step of the project,</div><div class="">and for preliminary evaluation a simpler example would be needed.</div><div class=""><br class=""></div><div class="">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 class="">can we get with only minimal modifications to the core.</div><div class=""><br class=""></div><div class="">Regards,</div><div class="">George</div><div class=""><div class="m_-6481325030509720384m_-2406771488922912429m_7462020983193081322m_-4451861523552279669gmail-m_-8638169037548414962gmail-m_-52597389203126130m_3480453752466103086h5"><div class=""><div class=""><br class=""><blockquote type="cite" class=""><div class="">On Mar 22, 2018, at 1:19 PM, Mikhail Ramalho <<a href="mailto:mikhail.ramalho@gmail.com" target="_blank" class="">mikhail.ramalho@gmail.com</a>> wrote:</div><br class="m_-6481325030509720384m_-2406771488922912429m_7462020983193081322m_-4451861523552279669gmail-m_-8638169037548414962gmail-m_-52597389203126130m_3480453752466103086m_4673560789215137001Apple-interchange-newline"><div class=""><div dir="ltr" class="">Hi all,<div class=""><br class=""></div><div class="">Thank you for the feedback, George and Dominic.</div><div class=""><br class=""></div><div class="">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 class=""><br class=""></div><div class="">May I ask for some feedback in this section?</div><div class=""><br class=""></div><div class="">~</div><div class=""><br class=""></div><div class="">I addressed most of the comments, except for: </div><div class=""><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); float: none; display: inline;" class=""><br class=""></span></div><div class=""><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); float: none; display: inline;" class=""><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); float: none; display: inline;" class="">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 class=""> </span></span></span></div><div class=""><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); float: none; display: inline;" class=""><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); float: none; display: inline;" class=""><span class=""><br class=""></span></span></span></div><div class=""><font face="Arial,
sans-serif, sans" color="#333333" class="">I tried to explain the motivation in the Overview section, do you think a motivation section would be better? </font></div><div class=""><font face="Arial,
sans-serif, sans" color="#333333" class=""><br class=""></font></div><div class=""><font face="Arial,
sans-serif, sans" color="#333333" class="">Regarding the how, I'll have another look in the BugReportVisitor and update the proposal with a more concrete solution.</font></div><div class=""><font face="Arial,
sans-serif, sans" color="#333333" class=""><br class=""></font></div><div class=""><font face="Arial,
sans-serif, sans" color="#333333" class="">Thank you,</font></div><div class=""><br class=""></div><div class="gmail_extra"><br class=""><div class="gmail_quote">2018-03-21 17:54 GMT+00:00 George Karpenkov<span class="Apple-converted-space"> </span><span dir="ltr" class=""><<a href="mailto:ekarpenkov@apple.com" target="_blank" class="">ekarpenkov@apple.com</a>></span>:<br class=""><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;"><div style="word-wrap: break-word;" class="">Hi Mikhail,<div class=""><br class=""></div><div class="">I’ve added some feedback.</div><div class="">Overall, I think we should be aiming for something more low-level and concrete:</div><div class="">adding examples with explanations would be a great improvement.</div><div class=""><br class=""></div><div class="">Regards,</div><div class="">George<div class=""><div class="m_-6481325030509720384m_-2406771488922912429m_7462020983193081322m_-4451861523552279669gmail-m_-8638169037548414962gmail-m_-52597389203126130m_3480453752466103086m_4673560789215137001m_3797644012230859096h5"><br class=""><div class=""><br class=""><blockquote type="cite" class=""><div class="">On Mar 21, 2018, at 10:12 AM, Mikhail Ramalho <<a href="mailto:mikhail.ramalho@gmail.com" target="_blank" class="">mikhail.ramalho@gmail.com</a>> wrote:</div><br class="m_-6481325030509720384m_-2406771488922912429m_7462020983193081322m_-4451861523552279669gmail-m_-8638169037548414962gmail-m_-52597389203126130m_3480453752466103086m_4673560789215137001m_3797644012230859096m_8959840794667446807Apple-interchange-newline"><div class=""><div dir="ltr" class="">Hi all,<div class=""><br class=""></div><div class="">I've written a first draft of my proposal:</div><div class=""><br class=""></div><div class=""><a href="https://docs.google.com/document/d/1-zNSv0l4WyoxYpJUAw8LFnQq_TY4AGjIpPu1VPkmO-g/edit?usp=sharing" target="_blank" class="">https://docs.google.com/docume<wbr class="">nt/d/1-zNSv0l4WyoxYpJUAw8LFnQq<wbr class="">_TY4AGjIpPu1VPkmO-g/edit?usp=s<wbr class="">haring</a><br class=""></div><div class=""><br class=""></div><div class="">I've added a few comments in places I think need improvement. </div><div class=""><br class=""></div><div class="">May I ask the community to have a look and give some feedback? </div><div class=""><br class=""></div><div class="">Thank you,</div><div class=""><br class=""></div></div><div class="gmail_extra"><br class=""><div class="gmail_quote">2018-03-12 18:24 GMT+00:00 George Karpenkov<span class="Apple-converted-space"> </span><span dir="ltr" class=""><<a href="mailto:ekarpenkov@apple.com" target="_blank" class="">ekarpenkov@apple.com</a>></span>:<br class=""><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;"><div style="word-wrap: break-word;" class="">Hi Mikhail,<div class=""><br class=""></div><div class="">I’m assuming Dominic have answered your questions regarding the point (3).</div><div class=""><br class=""></div><div class="">On point (1) I have recently sent an email on the list answering, I believe, to essentially the same question:</div><div class=""><a href="http://lists.llvm.org/pipermail/cfe-dev/2018-March/057064.html" target="_blank" class="">http://lists.llvm.org/pipermai<wbr class="">l/cfe-dev/2018-March/057064.ht<wbr class="">ml</a></div><div class=""><br class=""></div><div class="">(yes, unfortunately we do not have better archives, so messages might be often hard to track)<br class=""><div class=""><span class=""><br class=""><blockquote type="cite" class=""><div class=""><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;" class=""><div class="">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;" class="">might need to be extended somehow (a plan will be added to the proposal).</span></div></div></div></blockquote><div class=""><br class=""></div></span><div class="">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 class=""><br class=""></div><div class="">Please feel free to ask any further questions, bug reporter visitors are quite messy in the analyzer.</div><div class=""><br class=""></div><div class="">Regards,</div><div class="">George</div><br class=""><blockquote type="cite" class=""><div class=""><span class=""><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;" class=""><div class=""><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;" class=""><br class=""></span></div><div class=""><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;" class="">~</span></div><div class=""><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;" class=""><br class=""></span></div><div class=""><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;" class="">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;" class="">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 class=""><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;" class=""><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;" class=""><br class=""></span></span></div><div class=""><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;" class=""><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;" class="">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 class=""><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;" class=""><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;" class=""><br class=""></span></span></div><div class=""><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;" class=""><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;" class="">3.2. Don't add all the constraints, only the relevant ones: adding unnecessary constraints will slowdown the solver.</span></span></div><div class=""><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;" class=""><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;" class=""><br class=""></span></span></div><div class=""><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;" class=""><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;" class="">3.3. Refactor doTypeConversion to use built-in conversion functions (</span></span>Refactor to Sema::FindCompositePointerType<wbr class="">(), and Sema::CheckCompareOperands(); <wbr class="">Refine behavior for invalid type casts)</div><div class=""><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;" class=""><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;" class="">3.4. Refactor doIntTypeConversion to use Sema::handleIntegerConversion(<wbr class="">)</span></span></div><div class=""><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;" class=""><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;" class="">3.5. Refactor doFloatTypeConversion to use Sema::handleFloatConversion()</span></span></div><div class=""><br class=""></div><div class="">I bundled this together because, although the conversion seems incomplete (based on the comments), it's about removing duplicated code.</div><div class=""><br class=""></div><div class="">3.6. Refactor getAPSIntType(const llvm::APSInt &Int) const to put elsewhere.</div><div class=""><br class=""></div><div class="">~</div><div class=""><br class=""></div><div class="">Thank you,</div><div class=""><br class=""></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 class=""><div class="gmail_quote">2018-02-24 1:03 GMT+00:00 Devin Coughlin<span class="m_-6481325030509720384m_-2406771488922912429m_7462020983193081322m_-4451861523552279669gmail-m_-8638169037548414962gmail-m_-52597389203126130m_3480453752466103086m_4673560789215137001m_3797644012230859096m_8959840794667446807m_-5653580683305685986Apple-converted-space"> </span><span dir="ltr" class=""><<a href="mailto:dcoughlin@apple.com" target="_blank" class="">dcoughlin@apple.com</a>></span><wbr class="">:<br class=""><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 class=""><br class=""><br class="">> On Feb 23, 2018, at 9:29 AM, Mikhail Ramalho via cfe-dev <<a href="mailto:cfe-dev@lists.llvm.org" target="_blank" class="">cfe-dev@lists.llvm.org</a>> wrote:<br class="">><br class="">> 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 class=""><br class=""></span>Please make sure to keep email discussions on the mailing list rather than just personal email. This is<span class="Apple-converted-space"> </span> <span class="Apple-converted-space"> </span> <span class="Apple-converted-space"> </span><span class="Apple-converted-space"> </span> <span class="Apple-converted-space"> </span><span class="Apple-converted-space"> </span> <span class="Apple-converted-space"> </span><span class="Apple-converted-space"> </span> <span class="Apple-converted-space"> </span><span class="Apple-converted-space"> </span> <span class="Apple-converted-space"> </span><span class="Apple-converted-space"> </span> <span class="Apple-converted-space"> </span><span class="Apple-converted-space"> </span> <span class="Apple-converted-space"> </span><span class="Apple-converted-space"> </span> <span class="Apple-converted-space"> </span><span class="Apple-converted-space"> </span> <span class="Apple-converted-space"> </span><span class="Apple-converted-space"> </span> <span class="Apple-converted-space"> </span><span class="Apple-converted-space"> </span> <span class="Apple-converted-space"> </span><span class="Apple-converted-space"> </span> <span class="Apple-converted-space"> </span><span class="Apple-converted-space"> </span> <span class="Apple-converted-space"> </span><span class="Apple-converted-space"> </span> <span class="Apple-converted-space"> </span><span class="Apple-converted-space"> </span> <span class="Apple-converted-space"> </span><span class="Apple-converted-space"> </span> <span class="Apple-converted-space"> </span><span class="Apple-converted-space"> </span> <span class="Apple-converted-space"> </span><span class="Apple-converted-space"> </span> <span class="Apple-converted-space"> </span><span class="Apple-converted-space"> </span> <span class="Apple-converted-space"> </span>a topic that members of the community will be interested in and will have valuable feedback on.<br class=""><span class="m_-6481325030509720384m_-2406771488922912429m_7462020983193081322m_-4451861523552279669gmail-m_-8638169037548414962gmail-m_-52597389203126130m_3480453752466103086m_4673560789215137001m_3797644012230859096m_8959840794667446807m_-5653580683305685986HOEnZb"><font color="#888888" class=""><br class="">Devin<br class=""><br class=""></font></span></blockquote></div><br class=""><br clear="all" class=""><div class=""><br class=""></div>--<span class="m_-6481325030509720384m_-2406771488922912429m_7462020983193081322m_-4451861523552279669gmail-m_-8638169037548414962gmail-m_-52597389203126130m_3480453752466103086m_4673560789215137001m_3797644012230859096m_8959840794667446807m_-5653580683305685986Apple-converted-space"> </span><br class=""><div class="m_-6481325030509720384m_-2406771488922912429m_7462020983193081322m_-4451861523552279669gmail-m_-8638169037548414962gmail-m_-52597389203126130m_3480453752466103086m_4673560789215137001m_3797644012230859096m_8959840794667446807m_-5653580683305685986gmail_signature"><div dir="ltr" class=""><div class=""><br class=""></div><div class="">Mikhail Ramalho.</div></div></div></div></span><span class=""><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;" class="">______________________________<wbr class="">_________________</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;" class=""><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;" class="">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;" class=""><a href="mailto:cfe-dev@lists.llvm.org" target="_blank" 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;" class="">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;" class=""><a href="http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev" target="_blank" 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;" class="">http://lists.llvm.org/cgi-bin/<wbr class="">mailman/listinfo/cfe-dev</a></span></div></blockquote></div><br class=""></div></div></blockquote></div><br class=""><br clear="all" class=""><div class=""><br class=""></div>--<span class="Apple-converted-space"> </span><br class=""><div class="m_-6481325030509720384m_-2406771488922912429m_7462020983193081322m_-4451861523552279669gmail-m_-8638169037548414962gmail-m_-52597389203126130m_3480453752466103086m_4673560789215137001m_3797644012230859096m_8959840794667446807gmail_signature"><div dir="ltr" class=""><div class=""><br class=""></div><div class="">Mikhail Ramalho.</div></div></div></div></div></blockquote></div><br class=""></div></div></div></div></blockquote></div><br class=""><br clear="all" class=""><div class=""><br class=""></div>--<span class="Apple-converted-space"> </span><br class=""><div class="m_-6481325030509720384m_-2406771488922912429m_7462020983193081322m_-4451861523552279669gmail-m_-8638169037548414962gmail-m_-52597389203126130m_3480453752466103086m_4673560789215137001m_3797644012230859096gmail_signature"><div dir="ltr" class=""><div class=""><br class=""></div><div class="">Mikhail Ramalho.</div></div></div></div></div></div></blockquote></div><br class=""></div></div></div></div></blockquote></div><br class=""><br clear="all" class=""><div class=""><br class=""></div>--<span class="Apple-converted-space"> </span><br class=""><div class="m_-6481325030509720384m_-2406771488922912429m_7462020983193081322m_-4451861523552279669gmail-m_-8638169037548414962gmail-m_-52597389203126130m_3480453752466103086gmail_signature"><div dir="ltr" class=""><div class=""><br class=""></div><div class="">Mikhail Ramalho.</div></div></div></div></div></div></blockquote></div></div></div><br class=""></div></blockquote></div><br class=""><br clear="all" class=""><div class=""><br class=""></div>--<span class="Apple-converted-space"> </span><br class=""><div class="m_-6481325030509720384m_-2406771488922912429m_7462020983193081322m_-4451861523552279669gmail-m_-8638169037548414962gmail_signature"><div dir="ltr" class=""><div class=""><br class=""></div><div class="">Mikhail Ramalho.</div></div></div></div></div><br class=""><fieldset class="m_-6481325030509720384m_-2406771488922912429m_7462020983193081322m_-4451861523552279669mimeAttachmentHeader"></fieldset><pre class="m_-6481325030509720384m_-2406771488922912429m_7462020983193081322m_-4451861523552279669moz-quote-pre">______________________________<wbr class="">_________________
cfe-dev mailing list
<a class="m_-6481325030509720384m_-2406771488922912429m_7462020983193081322m_-4451861523552279669moz-txt-link-abbreviated" href="mailto:cfe-dev@lists.llvm.org" target="_blank">cfe-dev@lists.llvm.org</a>
<a class="m_-6481325030509720384m_-2406771488922912429m_7462020983193081322m_-4451861523552279669moz-txt-link-freetext" href="http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev" target="_blank">http://lists.llvm.org/cgi-bin/<wbr class="">mailman/listinfo/cfe-dev</a>
</pre></blockquote><br class=""></div></div></div></blockquote></div><br class=""><br clear="all" class=""><div class=""><br class=""></div></div></div><span class="m_-6481325030509720384HOEnZb"><font color="#888888" class="">--<span class="Apple-converted-space"> </span><br class=""><div class="m_-6481325030509720384m_-2406771488922912429m_7462020983193081322gmail_signature" data-smartmail="gmail_signature"><div dir="ltr" class=""><div class=""><br class=""></div><div class="">Mikhail Ramalho.</div></div></div></font></span></div></div></blockquote></div><br class=""><br clear="all" class=""><div class=""><br class=""></div>--<span class="Apple-converted-space"> </span><br class=""><div class="m_-6481325030509720384gmail_signature" data-smartmail="gmail_signature"><div dir="ltr" class=""><div class=""><br class=""></div><div class="">Mikhail Ramalho.</div></div></div></div></div></blockquote></div><br class=""></div></div></div></div></blockquote></div><br class=""><br clear="all" class=""><div class=""><br class=""></div>--<span class="Apple-converted-space"> </span><br class=""><div class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr" class=""><div class=""><br class=""></div><div class="">Mikhail Ramalho.</div></div></div></div></div></blockquote></div><br class=""></body></html>