[GSoC] Proposal draft

classic Classic list List threaded Threaded
7 messages Options
Reply | Threaded
Open this post in threaded view
|

[GSoC] Proposal draft

Louis Dionne via cfe-dev
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

Any feedback would be much appreciated.

Thanks,
Réka

_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
Reply | Threaded
Open this post in threaded view
|

Re: [GSoC] Proposal draft

Louis Dionne via cfe-dev
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 <[hidden email]> 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

Any feedback would be much appreciated.

Thanks,
Réka


_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
Reply | Threaded
Open this post in threaded view
|

Re: [GSoC] Proposal draft

Louis Dionne via cfe-dev
In reply to this post by Louis Dionne via cfe-dev
Hi George and Artem,

Thanks for all your valuable comments!
I'll try to address all of them in a couple of hours.

Réka



2018-03-25 22:26 GMT+02:00 George Karpenkov <[hidden email]>:
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 <[hidden email]> 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

Any feedback would be much appreciated.

Thanks,
Réka



_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
Reply | Threaded
Open this post in threaded view
|

Re: [GSoC] Proposal draft

Louis Dionne via cfe-dev
In reply to this post by Louis Dionne via cfe-dev
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()?
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?

Thanks,
Réka



2018-03-25 22:26 GMT+02:00 George Karpenkov <[hidden email]>:
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 <[hidden email]> 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

Any feedback would be much appreciated.

Thanks,
Réka



_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
Reply | Threaded
Open this post in threaded view
|

Re: [GSoC] Proposal draft

Louis Dionne via cfe-dev
In reply to this post by Louis Dionne via cfe-dev
Hi Réka,

Looks good overall!

There are two more items which could be included as super-stretch-goals: they would be very important for adoption of the project,
but fall far out of scope of the GSoC:

1) Packaging. This would be a huge barrier for adopting any Z3 work by existing analyzer users,
but maybe we can think about a few vectors where we could make the adoption easier.
E.g. how difficult would it be to add a dependency from the Debian package? Or from homebrew?

2) Stability. Z3 can segfault, bringing the entire analysis down.
The only way to address this I can think of would be running the solver out-of-process, communicating e.g. via SMT-LIB.
But that would considerably complicate the architecture and debugging, and I’m not sure the trade-offs are worth it.

George

On Mar 26, 2018, at 8:05 AM, Réka Nikolett Kovács <[hidden email]> wrote:

Hi George and Artem,

Thanks for all your valuable comments!
I'll try to address all of them in a couple of hours.

Réka



2018-03-25 22:26 GMT+02:00 George Karpenkov <[hidden email]>:
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 <[hidden email]> 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

Any feedback would be much appreciated.

Thanks,
Réka




_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
Reply | Threaded
Open this post in threaded view
|

Re: [GSoC] Proposal draft

Louis Dionne via cfe-dev
In reply to this post by Louis Dionne via cfe-dev


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

Any feedback would be much appreciated.

Thanks,
Réka




_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
Reply | Threaded
Open this post in threaded view
|

Re: [GSoC] Proposal draft

Louis Dionne 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 <[hidden email]> wrote:



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

Any feedback would be much appreciated.

Thanks,
Réka



_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev


_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev