llvm dev - Sep 2018 - [cfe-dev] SMT solvers in clang SA

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
<http://lists.llvm.org/pipermail/llvm-dev/attachments/20180921/a73bbd3b/attachment.html>

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 <
cfe-dev at lists.llvm.org> 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
> cfe-dev at lists.llvm.org
> http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
>

-- 

Mikhail Ramalho.
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
<http://lists.llvm.org/pipermail/llvm-dev/attachments/20180921/a23ee851/attachment-0001.html>

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 <mikhail.ramalho at
gmail.com>
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
<
> cfe-dev at lists.llvm.org> 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
>> cfe-dev at lists.llvm.org
>> http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
>>
>
>
> --
>
> Mikhail Ramalho.
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
<http://lists.llvm.org/pipermail/llvm-dev/attachments/20180921/f02d9bdc/attachment.html>