[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-23 19:48:03
Message-ID: CAORA-9aHwZ-AhppeEBzdxbJ+se_Ei5ovCHgwmPvq=nY-QBQ63w () mail ! gmail ! com
[Download RAW message or body]
[Attachment #2 (multipart/alternative)]
Hi,
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.
Any feedback is welcome!
Thank you,
2018-03-23 18:39 GMT+00:00 Mikhail Ramalho <mikhail.ramalho@gmail.com>:
> Indeed the constraints start to appear when there are
> multiplications/divisions/remainders, but I noticed that it only prints
> the constraints when it's able to solve them.
>
> Maybe in a higher level it's dropping constraints without querying if the
> solver can handle it?
>
> I'll keep looking into it.
>
> 2018-03-23 18:25 GMT+00:00 Artem Dergachev <noqnoqneo@gmail.com>:
>
>> Try making assumptions over 2 * x, these should work if i recall
>> correctly.
>>
>>
>> On 3/23/18 10:51 AM, Mikhail Ramalho via cfe-dev wrote:
>>
>> Hi,
>>
>>
>>> We would have to find an easier example first, where the core
>>> modification are not necessary.
>>> For the easier example: I think it would have to be simple arithmetics
>>> over integers, even negation would work.
>>> The current solver can not handle any relational constraints.
>>>
>>>
>> I'm having some problems finding a simple benchmark where the constraints
>> are not dropped.
>>
>> For instance, consider the following (safe) program:
>>
>> void foo(unsigned x, unsigned y)
>> {
>> if (x > y)
>> return;
>>
>> int base;
>>
>> if (x <= y)
>> base = 1;
>>
>> assert(base == 1);
>> }
>>
>> But the constraints are empty (both when I print the graph and the SMT
>> formula). I'm calling the analyzer:
>>
>> $ ~/myclang/bin/clang --analyze -Xclang -analyzer-viz-egraph-graphviz
>> -Xanalyzer -analyzer-checker=debug.DumpCFG main2.c
>>
>> I'm assuming that the constraints are being dropped somehow but is there
>> any other way to check it?
>>
>> Btw, I'm using the head of the release_60 branch.
>>
>> Thank you,
>>
>>
>>> 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)
>>> and see what formulas are mentioned there.
>>>
>>>
>>> Thank you,
>>>
>>>
>>> 2018-03-22 20:34 GMT+00:00 George Karpenkov <ekarpenkov@apple.com>:
>>>
>>>> Hi Mikhail,
>>>>
>>>> That's a good improvement!
>>>>
>>>> I think an awesome next step would be to see whether the analyzer
>>>> already has the formula required to solve your motivational example.
>>>> 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,
>>>> the exercise is much harder and might require substantial changes.
>>>>
>>>> Perhaps an easiest way to see what formulas the analyzer has is to
>>>> launch it with an extra flag
>>>> `-Xclang -analyzer-viz-egraph-graphviz` which would dump a graph in a
>>>> GraphViz format containing all the information analyzer has along all the
>>>> states.
>>>>
>>>> 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.
>>>> While it would be possible to change that, that would be a second step
>>>> of the project,
>>>> and for preliminary evaluation a simpler example would be needed.
>>>>
>>>> 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
>>>> can we get with only minimal modifications to the core.
>>>>
>>>> Regards,
>>>> George
>>>>
>>>> On Mar 22, 2018, at 1:19 PM, Mikhail Ramalho <mikhail.ramalho@gmail.com>
>>>> wrote:
>>>>
>>>> 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.
>>>>
>>>>
>>>>
>>>
>>>
>>> --
>>>
>>> Mikhail Ramalho.
>>>
>>>
>>>
>>
>>
>> --
>>
>> Mikhail Ramalho.
>>
>> _______________________________________________
>> cfe-dev mailing listcfe-dev@lists.llvm.orghttp://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
>>
>>
>>
>
>
> --
>
> Mikhail Ramalho.
>
--
Mikhail Ramalho.
[Attachment #5 (text/html)]
<div dir="ltr">Hi,<div><br></div><div>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><br></div><div>Any feedback is \
welcome!</div><div><br></div><div>Thank you,</div><div><br></div></div><div \
class="gmail_extra"><br><div class="gmail_quote">2018-03-23 18:39 GMT+00:00 Mikhail \
Ramalho <span dir="ltr"><<a href="mailto:mikhail.ramalho@gmail.com" \
target="_blank">mikhail.ramalho@gmail.com</a>></span>:<br><blockquote \
class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc \
solid;padding-left:1ex"><div dir="ltr">Indeed the constraints start to appear when \
there are multiplications/divisions/rema<wbr>inders, but I noticed that it only \
prints the constraints when it's able to solve them.<div><br></div><div>Maybe in \
a higher level it's dropping constraints without querying if the solver can \
handle it?<br></div><div><br></div><div>I'll keep looking into it.</div><div \
class="gmail_extra"><div><div class="h5"><br><div class="gmail_quote">2018-03-23 \
18:25 GMT+00:00 Artem Dergachev <span dir="ltr"><<a \
href="mailto:noqnoqneo@gmail.com" \
target="_blank">noqnoqneo@gmail.com</a>></span>:<br><blockquote \
class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc \
solid;padding-left:1ex">
<div text="#000000" bgcolor="#FFFFFF">
Try making assumptions over 2 * x, these should work if i recall
correctly.<div><div class="m_-2406771488922912429m_7462020983193081322h5"><br>
<br>
<div class="m_-2406771488922912429m_7462020983193081322m_-4451861523552279669moz-cite-prefix">On \
3/23/18 10:51 AM, Mikhail Ramalho via cfe-dev wrote:<br>
</div>
<blockquote type="cite">
<div dir="ltr">Hi,
<div class="gmail_extra"><br>
<div class="gmail_quote">
<blockquote class="gmail_quote" style="margin:0px 0px 0px \
0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"> <div \
style="word-wrap:break-word"> <div>
<div><br>
</div>
<div>We would have to find an easier example first,
where the core modification are not necessary.</div>
<div>For the easier example: I think it would have to
be simple arithmetics over integers, even negation
would work.</div>
<div>The current solver can not handle any relational
constraints.</div>
<div><br>
</div>
</div>
</div>
</blockquote>
<div><br>
</div>
<div>I'm having some problems finding a simple benchmark
where the constraints are not dropped.</div>
<div><br>
</div>
<div>For instance, consider the following (safe) program:</div>
<div><br>
</div>
<div>
<div>void foo(unsigned x, unsigned y)</div>
<div>{</div>
<div> if (x > y)</div>
<div> return;</div>
<div><br>
</div>
<div> int base;</div>
<div><br>
</div>
<div> if (x <= y)</div>
<div> base = 1;</div>
<div><br>
</div>
<div> assert(base == 1);</div>
<div>}</div>
</div>
<div><br>
</div>
<div>But the constraints are empty (both when I print the
graph and the SMT formula). I'm calling the analyzer:</div>
<div><br>
</div>
<div>$ ~/myclang/bin/clang --analyze -Xclang
-analyzer-viz-egraph-graphviz -Xanalyzer
-analyzer-checker=debug.DumpCF<wbr>G main2.c<br>
</div>
<div><br>
</div>
<div>I'm assuming that the constraints are being dropped
somehow but is there any other way to check it?</div>
<div><br>
</div>
<div>Btw, I'm using the head of the release_60 branch.</div>
<div><br>
</div>
<div>Thank you,</div>
<div> </div>
<blockquote class="gmail_quote" style="margin:0px 0px 0px \
0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"> <div \
style="word-wrap:break-word"> <div>
<div>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>and see what formulas are mentioned there.</div>
<div>
<div \
class="m_-2406771488922912429m_7462020983193081322m_-4451861523552279669gmail-m_-8638169037548414962gmail-h5"><br>
<blockquote type="cite">
<div>
<div dir="ltr">
<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:0px 0px \
0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"> <div \
style="word-wrap:break-word">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_-2406771488922912429m_7462020983193081322m_-4451861523552279669gmail-m_-8638169037548414962gmail-m_-52597389203126130m_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_-2406771488922912429m_7462020983193081322m_-4451861523552279669gmail-m_-86381 \
69037548414962gmail-m_-52597389203126130m_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 face="Arial,
sans-serif, sans" \
color="#333333">I tried to explain
the motivation in
the Overview
section, do you
think a motivation
section would be
better? </font></div>
<div><font face="Arial,
sans-serif, sans" \
color="#333333"><br> </font></div>
<div><font face="Arial,
sans-serif, sans" \
color="#333333">Regarding
the how, I'll have
another look in
the
BugReportVisitor
and update the
proposal with a
more concrete
solution.</font></div>
<div><font face="Arial,
sans-serif, sans" \
color="#333333"><br> </font></div>
<div><font face="Arial,
sans-serif, sans" \
color="#333333">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:0px 0px 0px 0.8ex;border-left:1px solid \
rgb(204,204,204);padding-left:1ex">
<div \
style="word-wrap:break-word">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_-2406771488922912429m_7462020983193081322m_-4451861523552279669gmail-m_-86381 \
69037548414962gmail-m_-52597389203126130m_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_-2406771488922912429m_7462020983193081322m_-4451861523552279669gmail-m_-86381 \
69037548414962gmail-m_-52597389203126130m_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:0px 0px 0px 0.8ex;border-left:1px solid \
rgb(204,204,204);padding-left:1ex">
<div \
style="word-wrap:break-word">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;f \
ont-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:40 \
0;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-spa \
ce: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: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;f \
ont-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:40 \
0;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-spa \
ce: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: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;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: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;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: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;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: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_-2406771488922912429m_7462020983193081322m_-4451861523552279669gmail-m_-86381 \
69037548414962gmail-m_-52597389203126130m_3480453752466103086m_4673560789215137001m_37 \
97644012230859096m_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:1px solid \
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_-2406771488922912429m_7462020983193081322m_-4451861523552279669gmail-m_-86381 \
69037548414962gmail-m_-52597389203126130m_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_-2406771488922912429m_7462020983193081322m_-4451861523552279669gmail-m_-86381 \
69037548414962gmail-m_-52597389203126130m_3480453752466103086m_4673560789215137001m_37 \
97644012230859096m_8959840794667446807m_-5653580683305685986Apple-converted-space"> \
</span><br> <div class="m_-2406771488922912429m_7462020983193081322m_-445186152355227 \
9669gmail-m_-8638169037548414962gmail-m_-52597389203126130m_3480453752466103086m_46735 \
60789215137001m_3797644012230859096m_8959840794667446807m_-5653580683305685986gmail_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-transf \
orm:none;white-space:normal;word-spacing:0px;float:none;display:inline">______________________________<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-cap \
s:normal;font-weight:normal;letter-spacing:normal;text-align:start;text-indent:0px;tex \
t-transform:none;white-space:normal;word-spacing:0px;float:none;display:inline">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_-2406771488922912429m_7462020983193081322m_-4451861523552279669gmail-m_-86381 \
69037548414962gmail-m_-52597389203126130m_3480453752466103086m_4673560789215137001m_3797644012230859096m_8959840794667446807gmail_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_-2406771488922912429m_7462020983193081322m_-4451861523552279669gmail-m_-86381 \
69037548414962gmail-m_-52597389203126130m_3480453752466103086m_4673560789215137001m_3797644012230859096gmail_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_-2406771488922912429m_7462020983193081322m_-4451861523552279669gmail-m_-8638169037548414962gmail-m_-52597389203126130m_3480453752466103086gmail_signature">
<div dir="ltr">
<div><br>
</div>
<div>Mikhail Ramalho.</div>
</div>
</div>
</div>
</div>
</div>
</blockquote>
</div>
</div>
</div>
<br>
</div>
</blockquote>
</div>
<br>
<br clear="all">
<div><br>
</div>
-- <br>
<div class="m_-2406771488922912429m_7462020983193081322m_-4451861523552279669gmail-m_-8638169037548414962gmail_signature">
<div dir="ltr">
<div><br>
</div>
<div>Mikhail Ramalho.</div>
</div>
</div>
</div>
</div>
<br>
<fieldset class="m_-2406771488922912429m_7462020983193081322m_-4451861523552279669mimeAttachmentHeader"></fieldset>
<pre class="m_-2406771488922912429m_7462020983193081322m_-4451861523552279669moz-quote-pre">______________________________<wbr>_________________
cfe-dev mailing list
<a class="m_-2406771488922912429m_7462020983193081322m_-4451861523552279669moz-txt-link-abbreviated" \
href="mailto:cfe-dev@lists.llvm.org" target="_blank">cfe-dev@lists.llvm.org</a> <a \
class="m_-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>mailman/listinfo/cfe-dev</a> \
</pre> </blockquote>
<br>
</div></div></div>
</blockquote></div><br><br clear="all"><div><br></div></div></div><span \
class="HOEnZb"><font color="#888888">-- <br><div \
class="m_-2406771488922912429m_7462020983193081322gmail_signature" \
data-smartmail="gmail_signature"><div dir="ltr"><div><br></div><div>Mikhail \
Ramalho.</div></div></div> </font></span></div></div>
</blockquote></div><br><br clear="all"><div><br></div>-- <br><div \
class="gmail_signature" data-smartmail="gmail_signature"><div \
dir="ltr"><div><br></div><div>Mikhail Ramalho.</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