[cfe-dev] [GSoC] Proposal draft

[George Karpenkov via cfe-dev]

Also please don’t forget to submit the PDF of the final proposal *using the GSoC website*!

> On Mar 26, 2018, at 2:12 PM, George Karpenkov via cfe-dev <cfe-dev at lists.llvm.org> wrote:
> 
> 
> 
>> On Mar 26, 2018, at 2:05 PM, Réka Nikolett Kovács <rekanikolett at gmail.com <mailto:rekanikolett at gmail.com>> wrote:
>> 
>> Hi,
>> 
>> Thanks again for the comments and explanations. I hope I've incorporated all of your advice, except for this one.
>> 
>> George: I've been thinking about what you wrote ("unifying a place where the constraints are dropped, and adding a flag guarding that") 
>> and I have to admit that I'm not sure I understand that precisely.
>> 
>> Constraints dropped before being added to the environment should mean that SValBuilder gave up while trying to construct a specific
>> symbolic expression from them (returned an UnknownVal), if I understand correctly. Now, the logic responsible for this seems pretty
>> much scattered around, so I thought maybe by unifying you mean creating a function like the constraint managers' canReasonAbout()?
> 
> Yes.
> 
>> Supposing that building more complex expressions (if such will be added) might be expensive, something like that could come handy in
>> controlling the level of detail. Did you mean something like that?
> 
> Yes, precisely, the logic is currently all over the place, so we don’t even know whether we get any performance benefit from dropping the constraints.
> Having logic in one place behind the flag would at least let us perform an evaluation and to see whether the optimization is worth it.
> 
> I would say it’s a fairly important stretch goal, due to the fact that as we have seen, very many useful constraints are getting dropped.
> 
>> 
>> Thanks,
>> Réka
>> 
>> 
>> 
>> 2018-03-25 22:26 GMT+02:00 George Karpenkov <ekarpenkov at apple.com <mailto:ekarpenkov at apple.com>>:
>> Hi Réka,
>> 
>> Great! I think it would be beneficial to add an example where the “complex” constraint is dropped before even being added to the environment,
>> and add a stretch goal of fixing those (e.g. by unifying a place where the constraints are dropped, and adding a flag guarding that).
>> 
>> George
>> 
>> 
>>> On Mar 24, 2018, at 1:52 PM, Réka Nikolett Kovács <rekanikolett at gmail.com <mailto:rekanikolett at gmail.com>> wrote:
>>> 
>>> Hi,
>>> 
>>> I'd like to add my own version of a Z3 integration proposal draft:
>>> 
>>> https://docs.google.com/document/d/1Qpw_rQ8-JFJJtqyJz8YBqui-FNcBgJJvpLBvPcCzHV4/edit?usp=sharing <https://docs.google.com/document/d/1Qpw_rQ8-JFJJtqyJz8YBqui-FNcBgJJvpLBvPcCzHV4/edit?usp=sharing>
>>> 
>>> Any feedback would be much appreciated.
>>> 
>>> Thanks,
>>> Réka
>> 
>> 
> 
> _______________________________________________
> 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>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20180326/270f88f6/attachment.html>