[cfe-dev] [GSoC] Proposal draft

[George Karpenkov via cfe-dev]

> On Mar 26, 2018, at 2:05 PM, Réka Nikolett Kovács <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
> 
> 

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20180326/b52faf4b/attachment.html>