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

[Mikhail Ramalho Gadelha via cfe-dev]

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.

BTW, any plans to implement anything floating-point-related?


> I went through the code in RangeConstraintManager.cpp and comprehended
> about the constraint manager overall. canReasonAbout() (line: 1948)
> shows which all operations are left being implemented (namely, Mul, Div,
> Shl, Shr, and also the Xor operator). I have added these into the
> proposal.
>
> > However, we have found another application for z3 - refute produced
> warnings. When we are about to report a new warning, we can check that
> constraints are sat/unsat and discard the warning in the latter case.  This
> happens way less frequently and good in terms of performance.  Alas, the
> majority of users have static analyzer build without z3, and some false
> positives warnings sneak in.
> >
> > So, there are two main directions that I see:
> > Figure out cases when z3 refutation works better than the built-in fast
> solver.
> > Run the analyzer in both modes and analyze the difference.  Usually it’s
> under 10 warnings, so it won’t be very tedious.
> I have added this into the proposal too.
>
> > Add reasoning about range-based binary operations.
> > If we know ranges for symbols or symbolic expressions x and y, we can
> often reason about possible ranges for x OP y, where OP is some binary
> operator.  At the moment, we have support for &, |, and % (it’s a bit weird
> set of operators, but it was driven by reported false positives).
> Going through D80117, D79434, and D79336, one of the first things was to
> bisect the condition based on the sign of symbols. Followed by
> appropriate handling of upper/lower bounds for the expression.
>
> Regarding the TODO #1 (L:931) and TODO #2 (L:936) in
> RangeConstraintManager.cpp,
> should I put these into the proposal too? (this to be done for other
> binary
> operations as well apart from {rem, and, or} operations)
>
> These todos are related to lazy implemetation for VisitBinaryOperator and
> caching mechanism for analysis of nested expressions.
>
> > It’s a logical continuation of my work:
> > D86465, D82445, D83286, D82381, D80117, D79434, and D79336
> >
> I went through these patches as well in order to understand the workflow
> and things which have been done so far.
>
> The description of project also mentions about a unit-test framework.
> Can I get more details regarding this?
>
> I have drafted the initial version of my proposal here.
> (
> https://docs.google.com/document/d/1ts_jxi1eAPGgeSzy5cs1dwZDcrmCHao8skZT8yWtOPI/edit?usp=sharing
> )
>
> Thank you
> --
> Manas
> CSAM Undergraduate | 2022
> IIIT-Delhi, India
> _______________________________________________
> cfe-dev mailing list
> cfe-dev at lists.llvm.org
> https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
>


-- 

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