[cfe-dev] GSoC 2018

Mikhail Ramalho via cfe-dev cfe-dev at lists.llvm.org
Fri Mar 23 12:48:03 PDT 2018 

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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20180323/dc075a5d/attachment.html>

More information about the cfe-dev mailing list