[GSoC] Proposal draft

Clang Frontend
1

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

2

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

3

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

4

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.

5

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