[cfe-dev] GSoC 2018
Artem Dergachev via cfe-dev
cfe-dev at lists.llvm.org
Fri Mar 23 11:25:51 PDT 2018
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
>> <mailto: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
>>> <mailto: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 <mailto: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
>>>> <mailto: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
>>>> <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 <mailto: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
>>>> <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
>>>>> <mailto:dcoughlin at apple.com>>:
>>>>>
>>>>>
>>>>>
>>>>> > On Feb 23, 2018, at 9:29 AM, Mikhail Ramalho
>>>>> via cfe-dev <cfe-dev at lists.llvm.org
>>>>> <mailto: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 <mailto:cfe-dev at lists.llvm.org>
>>>>> http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
>>>>> <http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev>
>>>>
>>>>
>>>>
>>>>
>>>> --
>>>>
>>>> Mikhail Ramalho.
>>>
>>>
>>>
>>>
>>> --
>>>
>>> Mikhail Ramalho.
>>
>>
>>
>>
>> --
>>
>> Mikhail Ramalho.
>
>
>
>
> --
>
> Mikhail Ramalho.
>
> _______________________________________________
> cfe-dev mailing list
> cfe-dev at lists.llvm.org
> http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20180323/325aaee6/attachment.html>
More information about the cfe-dev
mailing list