GSOC | clang Z3

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

GSOC | clang Z3

Louis Dionne via cfe-dev
Hello all,

I was testing the performance of the z3 clang analyzer using the sv-benchmarks. I experienced a huge performance issue in the analyzer[image]. Is there a way we can use something similar to z3 -v<N> when we run the analyzer to see where the z3 is getting stuck?

Another thing I wanted to ask is that does LLVM has a particular format in which a student has to submit his proposal?

Thank You,
Ashish Kumar Gahlot

--
Ashish Kumar Gahlot
IV year, UG
Govt. Engg. College, Ajmer, India

_______________________________________________
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 | clang Z3

Louis Dionne via cfe-dev
Hi Ashish,

On Mar 15, 2018, at 11:41 PM, Ashish Gahlot via cfe-dev <[hidden email]> wrote:

Hello all,

I was testing the performance of the z3 clang analyzer using the sv-benchmarks. I experienced a huge performance issue in the analyzer[image].

Yes, hence the point of the GSOC project to only cross-check the counterexamples.

Is there a way we can use something similar to z3 -v<N> when we run the analyzer to see where the z3 is getting stuck?

No, there is no similar option for the analyzer.
I don’t think it would help you much though: most likely z3 is just performing a very large number of small queries at every step.


Another thing I wanted to ask is that does LLVM has a particular format in which a student has to submit his proposal?

Probably the easiest is to search the list archives from the last year and to look for the previous analyzer GSoC applications.

Regards,
George


Thank You,
Ashish Kumar Gahlot

--
Ashish Kumar Gahlot
IV year, UG
Govt. Engg. College, Ajmer, India
_______________________________________________
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: GSOC | clang Z3

Louis Dionne via cfe-dev
Hello all,

I will be submitting my proposal within a couple of days for the community review. Please add your valuable comments so that I can refactor the proposal.
I have never worked with solvers before so it is pretty new for me. I am not able to figure out the exact reason for the slowing down of the solver and the reason it generates false positives by just reading the code. Can you please give me some pointers where should I focus on?

Thank you very much,
Ashish Kumar Gahlot

On Fri, Mar 16, 2018 at 11:06 PM, George Karpenkov <[hidden email]> wrote:
Hi Ashish,

On Mar 15, 2018, at 11:41 PM, Ashish Gahlot via cfe-dev <[hidden email]> wrote:

Hello all,

I was testing the performance of the z3 clang analyzer using the sv-benchmarks. I experienced a huge performance issue in the analyzer[image].

Yes, hence the point of the GSOC project to only cross-check the counterexamples.

Is there a way we can use something similar to z3 -v<N> when we run the analyzer to see where the z3 is getting stuck?

No, there is no similar option for the analyzer.
I don’t think it would help you much though: most likely z3 is just performing a very large number of small queries at every step.


Another thing I wanted to ask is that does LLVM has a particular format in which a student has to submit his proposal?

Probably the easiest is to search the list archives from the last year and to look for the previous analyzer GSoC applications.

Regards,
George


Thank You,
Ashish Kumar Gahlot

--
Ashish Kumar Gahlot
IV year, UG
Govt. Engg. College, Ajmer, India
_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev




--
Ashish Kumar Gahlot
IV year, UG
Govt. Engg. College, Ajmer, India

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