[cfe-dev] GSoC 2018

Mikhail Ramalho via cfe-dev cfe-dev at lists.llvm.org
Tue Mar 27 08:38:02 PDT 2018 

Hi all,

I just submitted my proposal.

Thank you very much everyone for the feedback.


2018-03-26 23:13 GMT+01:00 George Karpenkov <ekarpenkov at apple.com>:

> Great! Don’t forget to submit the PDF through the official website!
>
>
> On Mar 26, 2018, at 9:13 AM, Mikhail Ramalho <mikhail.ramalho at gmail.com>
> wrote:
>
> Hi all,
>
> 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).
>
> Any feedback is welcome! I plan to submit the report tomorrow,
> mid-afternoon.
>
> Thank you,
>
> 2018-03-23 21:54 GMT+00:00 George Karpenkov <ekarpenkov at apple.com>:
>
>> Hi Mikhail,
>>
>> Indeed, it seems that the constraint manager is more eager to throw out
>> complex constraints than I’ve anticipated initially.
>> It might be partly a good thing: now we need to know that evaluating
>> disabling this heuristic and measuring a change in footprint
>> on a large number of project needs to be a part of the schedule.
>> An example where a change in this optimization is required would be also
>> beneficial for proposal.
>>
>> Now onto the example.
>>
>> 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.
>> (or use a debug checker and a special function, consult tests for those)
>> 2. The following function seems to give the desired behavior:
>>
>> int foo(int x) {
>>   int *z = 0;
>>   if ((x & 1) && ((x & 1) ^ 1))
>>       return *z;
>>   return 0;
>> }
>>
>> 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),
>> it is non-obvious, and just using Z3 with constraints present in the
>> graph should be sufficient.
>>
>> Regards,
>> George
>>
>> On Mar 23, 2018, at 12:48 PM, Mikhail Ramalho <mikhail.ramalho at gmail.com>
>> wrote:
>>
>> 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 at 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 at 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 at 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 at 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 at 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 at 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 at 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 at apple.com>:
>>>>>>>>
>>>>>>>>>
>>>>>>>>>
>>>>>>>>> > On Feb 23, 2018, at 9:29 AM, Mikhail Ramalho via cfe-dev <
>>>>>>>>> cfe-dev at 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 at 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 at lists.llvm.orghttp://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
>>>>
>>>>
>>>>
>>>
>>>
>>> --
>>>
>>> Mikhail Ramalho.
>>>
>>
>>
>>
>> --
>>
>> Mikhail Ramalho.
>>
>>
>>
>
>
> --
>
> Mikhail Ramalho.
>
>
>


-- 

Mikhail Ramalho.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20180327/bdac07e8/attachment.html>

More information about the cfe-dev mailing list