Need sources to read up about Z3 integration GSOC project

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

Need sources to read up about Z3 integration GSOC project

Hans Wennborg via cfe-dev
Hello,

I am a 4th year undergrad CS student from India, studying at National Institute of Technology, Trichy. I am interested in contributing to Clang Static Analyzer via GSOC '18.

For the past several days I have been looking into the "Integrate with Z3 SMT solver to reduce false positives" project listed here: http://llvm.org/OpenProjects.html#analyzer-z3-smt

I went through the CSA dev-guidelines, and also glanced through this item on fabricator: https://reviews.llvm.org/D28952

Besides these two I could not find any material relevant to this project. It would be great if someone could point out additional reading material relevant to this. Since there has already been a merged item of integrating Z3, I'd like to know what the expected outcomes of this project would be.

Regards
Parth




_______________________________________________
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: Need sources to read up about Z3 integration GSOC project

Hans Wennborg via cfe-dev
Hi Parth,


Besides these two I could not find any material relevant to this project. It would be great if someone could point out additional reading material relevant to this.

Yes, unfortunately getting into the analyzer development is rather hard.
Two good entry points are:

 - Additionally, Artem has written a very good guide available at https://github.com/haoNoQ/clang-analyzer-guide 

Since there has already been a merged item of integrating Z3, I'd like to know what the expected outcomes of this project would be.

The project you have linked to had a goal of replacing the analyzer constraint manager with Z3.
The evaluation has shown a massive (> 20x) slowdown.

The motivation for the current project is that false positives is, perhaps, the largest problem static analyzer has
(that is, bug reports where the analyzer reports a bug due to imprecision, but no bug actually exists).
Thus, the idea is to analyze the project with the currently used fast and imprecise solver,
but then try to refute bug reports in the post-processing phase using the Z3 solver.


Regards
Parth



_______________________________________________
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
Reply | Threaded
Open this post in threaded view
|

Re: Need sources to read up about Z3 integration GSOC project

Hans Wennborg via cfe-dev
Thanks George! I have a better idea of the project now. I'll get back after going through the materials you sent as well as more of the code.

Regards
Parth

On Mar 6, 2018 4:16 AM, "George Karpenkov" <[hidden email]> wrote:
Hi Parth,


Besides these two I could not find any material relevant to this project. It would be great if someone could point out additional reading material relevant to this.

Yes, unfortunately getting into the analyzer development is rather hard.
Two good entry points are:

 - Additionally, Artem has written a very good guide available at https://github.com/haoNoQ/clang-analyzer-guide 

Since there has already been a merged item of integrating Z3, I'd like to know what the expected outcomes of this project would be.

The project you have linked to had a goal of replacing the analyzer constraint manager with Z3.
The evaluation has shown a massive (> 20x) slowdown.

The motivation for the current project is that false positives is, perhaps, the largest problem static analyzer has
(that is, bug reports where the analyzer reports a bug due to imprecision, but no bug actually exists).
Thus, the idea is to analyze the project with the currently used fast and imprecise solver,
but then try to refute bug reports in the post-processing phase using the Z3 solver.


Regards
Parth



_______________________________________________
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