[GSoC Proposal Draft] Integrate z3 SMT solver with Clang Static Analyzer

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

[GSoC Proposal Draft] Integrate z3 SMT solver with Clang Static Analyzer

Louis Dionne via cfe-dev
Hi all,

Base on the previous discussions on the cfe-dev mailing list and my personal research, I wrote a proposal for integrating z3 SMT solver with clang static analyzer. Base on George's advice, I would like the cfe-dev community to take a look at the proposal and give me some feedback. I do not have much experience with the Clang Static Analyzer so there might be some misunderstanding on my part, therefore any feedback is appreciated!

https://docs.google.com/document/d/1vg1-y1P9lChTyZ5ritxC6He-jIS8ARSfSryT4nXLhe0/edit?usp=sharing

Looking forward to your response,
Brenda


_______________________________________________
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] Integrate z3 SMT solver with Clang Static Analyzer

Louis Dionne via cfe-dev
Hi Brenda,

It’s great that you are interested in the project!
However, unfortunately the current proposal is to high-level and does not contain a sufficient level of detail.

I can see the following issues:
 
1) The only example given is on proving DeMorgan’s law, which is unrelated to the proposal
2) It is not specified why or in what cases using an SMT solver would be more precise than using a current solver
3) Breaking down into parts is a bit arbitrary: e.g. “Flag bugs in Bug Reporter”: how would you plan to do this? Why a new bug type is needed?
“Constructing Z3SolverVisitor”: yes, but what would that visitor do and why?
“Implement z3_solve()”: what constraints? What would this function do?

4) Similar problems appear in the timeline, with evaluation postponed until the very end, and many items being too vague
(e.g. how would bug reporter figure out which paths are too complex? What “complex” means in this case? What would z3_solve function do?
Why is the function name relevant at this stage?)

Regards,
George

On Mar 22, 2018, at 10:18 PM, Brenda So <[hidden email]> wrote:

Hi all,

Base on the previous discussions on the cfe-dev mailing list and my personal research, I wrote a proposal for integrating z3 SMT solver with clang static analyzer. Base on George's advice, I would like the cfe-dev community to take a look at the proposal and give me some feedback. I do not have much experience with the Clang Static Analyzer so there might be some misunderstanding on my part, therefore any feedback is appreciated!

https://docs.google.com/document/d/1vg1-y1P9lChTyZ5ritxC6He-jIS8ARSfSryT4nXLhe0/edit?usp=sharing

Looking forward to your response,
Brenda



_______________________________________________
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] Integrate z3 SMT solver with Clang Static Analyzer

Louis Dionne via cfe-dev
Hi George,

Thanks for the advice! I found a bug on Bugzilla that addresses exactly what I want to do in this project -- using Z3 to track symbolic values in the program since the current analyzer doesn't have the power to do so. I believe this could be a beneficial add on to the clang static analyzer! I addressed issues 1 and 2 by adding a motivational example and demonstrated how z3 can be used to solve the problem.

I also added a lot more detail under ProjectGoal and Implementation -- hopefully that addressed issues 3 and 4. In the timeline I laid out plans to test each step of the program.

Moreover, I realize that modifying the BugReporter internally might be too difficult, so I put it as an extra goal instead.

I  updated the proposal with the above changes. Again if you have any concerns please let me know!

https://docs.google.com/document/d/1vg1-y1P9lChTyZ5ritxC6He-jIS8ARSfSryT4nXLhe0/edit?usp=sharing


Yours,
Brenda

On Fri, Mar 23, 2018 at 1:53 PM, George Karpenkov <[hidden email]> wrote:
Hi Brenda,

It’s great that you are interested in the project!
However, unfortunately the current proposal is to high-level and does not contain a sufficient level of detail.

I can see the following issues:
 
1) The only example given is on proving DeMorgan’s law, which is unrelated to the proposal
2) It is not specified why or in what cases using an SMT solver would be more precise than using a current solver
3) Breaking down into parts is a bit arbitrary: e.g. “Flag bugs in Bug Reporter”: how would you plan to do this? Why a new bug type is needed?
“Constructing Z3SolverVisitor”: yes, but what would that visitor do and why?
“Implement z3_solve()”: what constraints? What would this function do?

4) Similar problems appear in the timeline, with evaluation postponed until the very end, and many items being too vague
(e.g. how would bug reporter figure out which paths are too complex? What “complex” means in this case? What would z3_solve function do?
Why is the function name relevant at this stage?)

Regards,
George

On Mar 22, 2018, at 10:18 PM, Brenda So <[hidden email]> wrote:

Hi all,

Base on the previous discussions on the cfe-dev mailing list and my personal research, I wrote a proposal for integrating z3 SMT solver with clang static analyzer. Base on George's advice, I would like the cfe-dev community to take a look at the proposal and give me some feedback. I do not have much experience with the Clang Static Analyzer so there might be some misunderstanding on my part, therefore any feedback is appreciated!

https://docs.google.com/document/d/1vg1-y1P9lChTyZ5ritxC6He-jIS8ARSfSryT4nXLhe0/edit?usp=sharing

Looking forward to your response,
Brenda




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