SMT solvers in clang SA

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

SMT solvers in clang SA

Yvan Roux via cfe-dev
Hi all,

Currently studying the impact of SMT solvers on Clang SA. Can anyone help in telling more about the SMT solvers use in clang SA ? ( Have already tested Z3 SMT solver implemented in GSoC 2018 , also looking for other SMT solvers if possible )

Thanks,
Siddharth

_______________________________________________
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: SMT solvers in clang SA

Yvan Roux via cfe-dev
We are currently implementing the backends for other solvers (you can follow the progress here: https://github.com/mikhailramalho/clang). So far we got Boolector, MathSAT and Yices ready. CVC4 should be done soon.

When used to refute bugs, they all give roughly the same results: a ~5% speedup if there are refuted bugs or a ~5% slowdown if no bug is refuted.

I've only tried to analyze one full project (tmux) with Yices; the CSA ran for 24hrs and it didn't complete the analyze. For comparison, it takes 90s to analyze it with the ranged constraint manager in the CSA.

Thanks, 

Em sex, 21 de set de 2018 às 12:32, Siddharth Shankar Swain via cfe-dev <[hidden email]> escreveu:
Hi all,

Currently studying the impact of SMT solvers on Clang SA. Can anyone help in telling more about the SMT solvers use in clang SA ? ( Have already tested Z3 SMT solver implemented in GSoC 2018 , also looking for other SMT solvers if possible )

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


--

Mikhail Ramalho.

_______________________________________________
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: SMT solvers in clang SA

Yvan Roux via cfe-dev
Thanks Mikhail. Can you tell while refuting false positives does inclusion of SMT solvers lead to elimination of some genuine issues by mistake ?

On Fri, Sep 21, 2018 at 5:21 PM Mikhail Ramalho <[hidden email]> wrote:
We are currently implementing the backends for other solvers (you can follow the progress here: https://github.com/mikhailramalho/clang). So far we got Boolector, MathSAT and Yices ready. CVC4 should be done soon.

When used to refute bugs, they all give roughly the same results: a ~5% speedup if there are refuted bugs or a ~5% slowdown if no bug is refuted.

I've only tried to analyze one full project (tmux) with Yices; the CSA ran for 24hrs and it didn't complete the analyze. For comparison, it takes 90s to analyze it with the ranged constraint manager in the CSA.

Thanks, 

Em sex, 21 de set de 2018 às 12:32, Siddharth Shankar Swain via cfe-dev <[hidden email]> escreveu:
Hi all,

Currently studying the impact of SMT solvers on Clang SA. Can anyone help in telling more about the SMT solvers use in clang SA ? ( Have already tested Z3 SMT solver implemented in GSoC 2018 , also looking for other SMT solvers if possible )

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


--

Mikhail Ramalho.

_______________________________________________
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: SMT solvers in clang SA

Yvan Roux via cfe-dev
It's possible and it happened before (see: https://reviews.llvm.org/D48324), but I haven't seen any true positive being removed lately.

Em sex, 21 de set de 2018 às 13:03, Siddharth Shankar Swain <[hidden email]> escreveu:
Thanks Mikhail. Can you tell while refuting false positives does inclusion of SMT solvers lead to elimination of some genuine issues by mistake ?

On Fri, Sep 21, 2018 at 5:21 PM Mikhail Ramalho <[hidden email]> wrote:
We are currently implementing the backends for other solvers (you can follow the progress here: https://github.com/mikhailramalho/clang). So far we got Boolector, MathSAT and Yices ready. CVC4 should be done soon.

When used to refute bugs, they all give roughly the same results: a ~5% speedup if there are refuted bugs or a ~5% slowdown if no bug is refuted.

I've only tried to analyze one full project (tmux) with Yices; the CSA ran for 24hrs and it didn't complete the analyze. For comparison, it takes 90s to analyze it with the ranged constraint manager in the CSA.

Thanks, 

Em sex, 21 de set de 2018 às 12:32, Siddharth Shankar Swain via cfe-dev <[hidden email]> escreveu:
Hi all,

Currently studying the impact of SMT solvers on Clang SA. Can anyone help in telling more about the SMT solvers use in clang SA ? ( Have already tested Z3 SMT solver implemented in GSoC 2018 , also looking for other SMT solvers if possible )

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


--

Mikhail Ramalho.


--

Mikhail Ramalho.

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