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

[Brenda So 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 <ekarpenkov at apple.com>
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 <sogun3 at gmail.com> 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
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20180323/4eef1cce/attachment.html>