[cfe-dev] [GSoC] Re: CSA constraint solver improvements

[Manas via cfe-dev]

On Mon, Apr 12, 2021 at 06:28:19PM -0400, Mikhail Ramalho Gadelha wrote:
> Hi,
> 
> Em dom., 11 de abr. de 2021 às 20:30, Manas via cfe-dev <
> cfe-dev at lists.llvm.org> escreveu:
> 
> > On Fri, Apr 09, 2021 at 12:40:24PM +0300, Valeriy Savchenko wrote:
> > > The solver in question is fully located in RangeConstraintManager.cpp.
> > There we try our best to provide useful ranges for symbolic expressions AND
> > do it real fast. The last part is probably the most important thing here.
> > This solver works every time we see a condition in code and when we tried
> > using z3 for this instead, it degraded performance so drastically that the
> > analyzer is not useable (e.g 10min --> 25h).
> > >
> 
> 
> Yeah, IIRC most of the slowdown comes from the calls at branching points:
> we end up calling the solver twice and we never cache the results :/
> Incremental solving would probably improve the performance a bit.
> 
> Fun fact: I implemented the support for Boolector, CVC4, MathSAT, and Yices
> in a separate fork, and Yices does considerably better than Z3, however,
> still not good enough to make it usable.
> 
> Feel free to ask any questions you might have about the SMT stuff in LLVM.
> The bug refutation might be a good source of insight for your project,
> especially if you are looking at implementing these other operations.
> 
I am hoping to look in this z3 refutation (this month) before starting the 
project if my university workload allows it. :)
I agree with you that it will surely give me an insight for the work.

-- 
Manas
CSAM Undergraduate | 2022
IIIT-Delhi, India