[cfe-dev] GSoC 2018

Fri Mar 23 10:51:42 PDT 2018

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