[prev in list] [next in list] [prev in thread] [next in thread]
List: cfe-dev
Subject: Re: [cfe-dev] GSoC 2018
From: Mikhail Ramalho via cfe-dev <cfe-dev () lists ! llvm ! org>
Date: 2018-03-22 20:19:11
Message-ID: CAORA-9a3vGOJDn+Ra+9m2a2N_Eg_=-aC7U8avWGeYw8hsXQNew () mail ! gmail ! com
[Download RAW message or body]
[Attachment #2 (multipart/alternative)]
Hi all,
Thank you for the feedback, George and Dominic.
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.
May I ask for some feedback in this section?
~
I addressed most of the comments, except for:
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.
I tried to explain the motivation in the Overview section, do you think a
motivation section would be better?
Regarding the how, I'll have another look in the BugReportVisitor and
update the proposal with a more concrete solution.
Thank you,
2018-03-21 17:54 GMT+00:00 George Karpenkov <ekarpenkov@apple.com>:
> Hi Mikhail,
>
> I've added some feedback.
> Overall, I think we should be aiming for something more low-level and
> concrete:
> adding examples with explanations would be a great improvement.
>
> Regards,
> George
>
>
> On Mar 21, 2018, at 10:12 AM, Mikhail Ramalho <mikhail.ramalho@gmail.com>
> wrote:
>
> Hi all,
>
> I've written a first draft of my proposal:
>
> https://docs.google.com/document/d/1-zNSv0l4WyoxYpJUAw8LFnQq
> _TY4AGjIpPu1VPkmO-g/edit?usp=sharing
>
> I've added a few comments in places I think need improvement.
>
> May I ask the community to have a look and give some feedback?
>
> Thank you,
>
>
> 2018-03-12 18:24 GMT+00:00 George Karpenkov <ekarpenkov@apple.com>:
>
>> Hi Mikhail,
>>
>> I'm assuming Dominic have answered your questions regarding the point (3).
>>
>> On point (1) I have recently sent an email on the list answering, I
>> believe, to essentially the same question:
>> http://lists.llvm.org/pipermail/cfe-dev/2018-March/057064.html
>>
>> (yes, unfortunately we do not have better archives, so messages might be
>> often hard to track)
>>
>> 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 might
>> need to be extended somehow (a plan will be added to the proposal).
>>
>>
>> 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.
>>
>> Please feel free to ask any further questions, bug reporter visitors are
>> quite messy in the analyzer.
>>
>> Regards,
>> George
>>
>>
>> ~
>>
>> 3. This is a list of the TODOs in 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:
>>
>> 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.
>>
>> 3.2. Don't add all the constraints, only the relevant ones: adding
>> unnecessary constraints will slowdown the solver.
>>
>> 3.3. Refactor doTypeConversion to use built-in conversion functions (Refactor
>> to Sema::FindCompositePointerType(), and Sema::CheckCompareOperands(); Refine
>> behavior for invalid type casts)
>> 3.4. Refactor doIntTypeConversion to use Sema::handleIntegerConversion()
>> 3.5. Refactor doFloatTypeConversion to use Sema::handleFloatConversion()
>>
>> I bundled this together because, although the conversion seems incomplete
>> (based on the comments), it's about removing duplicated code.
>>
>> 3.6. Refactor getAPSIntType(const llvm::APSInt &Int) const to put
>> elsewhere.
>>
>> ~
>>
>> Thank you,
>>
>>
>> 2018-02-24 1:03 GMT+00:00 Devin Coughlin <dcoughlin@apple.com>:
>>
>>>
>>>
>>> > On Feb 23, 2018, at 9:29 AM, Mikhail Ramalho via cfe-dev <
>>> cfe-dev@lists.llvm.org> wrote:
>>> >
>>> > 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?
>>>
>>> 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.
>>>
>>> Devin
>>>
>>>
>>
>>
>> --
>>
>> Mikhail Ramalho.
>> _______________________________________________
>> cfe-dev mailing list
>> cfe-dev@lists.llvm.org
>> http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
>>
>>
>>
>
>
> --
>
> Mikhail Ramalho.
>
>
>
--
Mikhail Ramalho.
[Attachment #5 (text/html)]
<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_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_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:nor \
mal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spac \
ing: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:nor \
mal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spac \
ing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;wor \
d-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:nor \
mal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spac \
ing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;wor \
d-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:nor \
mal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spac \
ing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;wor \
d-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:nor \
mal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spac \
ing: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:nor \
mal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spac \
ing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;wor \
d-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:nor \
mal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spac \
ing: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:nor \
mal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spac \
ing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;wor \
d-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:nor \
mal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spac \
ing: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:nor \
mal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spac \
ing: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:nor \
mal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spac \
ing: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:nor \
mal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spac \
ing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;wor \
d-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:nor \
mal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spac \
ing: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:nor \
mal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spac \
ing: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:nor \
mal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spac \
ing: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:nor \
mal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spac \
ing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;wor \
d-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:nor \
mal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spac \
ing: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:nor \
mal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spac \
ing: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:nor \
mal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spac \
ing: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:nor \
mal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spac \
ing: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:nor \
mal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spac \
ing: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:nor \
mal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spac \
ing: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_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 \
</div>
</div></blockquote></div><br></div></div></div></div></blockquote></div><br><br \
clear="all"><div><br></div>-- <br><div class="m_3797644012230859096gmail_signature" \
data-smartmail="gmail_signature"><div dir="ltr"><div><br></div><div>Mikhail \
Ramalho.</div></div></div> </div></div>
[Attachment #6 (text/plain)]
_______________________________________________
cfe-dev mailing list
cfe-dev@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
[prev in list] [next in list] [prev in thread] [next in thread]
Configure |
About |
News |
Add a list |
Sponsored by KoreLogic