[cfe-dev] Generating range constraints in the static analyzer

[Balázs Benics via cfe-dev]

Hi,

the existing range based constraint manager only produces constraints for
> certain symbols
>
You are right, our constraint manager has its limitations.

Right now, it can not deal with symbol comparisons like `$1 < $2` even if
both `$1` and `$2` are well-constrained symbols.
Although I recently made a patch implementing such: D77792
<https://reviews.llvm.org/D77792>

There is already a huge complexity behind the range based constraint
manager and we should not bloat it even further.
Probably a complete redesign would help, but there is no free lunch. You
can not have both accuracy and speed.

... generating range constraints for some C programs, in the hopes of
> finding potential UB for bitshift operatio
>
For precise constraint modeling, you should use the Z3 based constraint
manager instead of the default ranged based one.
You can enable that with the `-analyzer-config -analyzer-constraints=z3`
flags.
Note that, it will introduce a *significant *runtime overhead.

Christoph Steefel via cfe-dev <cfe-dev at lists.llvm.org> ezt írta (időpont:
2020. ápr. 18., Szo, 23:57):

> Hello all,
>
> I have been looking into generating range constraints for some C programs,
> in the hopes of finding potential UB for bitshift operations. However, it
> seems that the existing range based constraint manager only produces
> constraints for certain symbols. For other symbols, such as those generated
> by arithmetic on a range bounded symbol, I found myself needing to
> calculate the new range constraint myself. Is this a reasonable path
> forwards, or is there some existing code that does something  similar to
> this already?
>
> I have been looking at the RangedConstraintManager, and using it's
> RangeSet implementation,  but I also haven't  found where the RangeSet is
> actually used.
>
> Any help would be appreciated.
>
> Best,
> Christoph
> _______________________________________________
> cfe-dev mailing list
> cfe-dev at lists.llvm.org
> https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20200419/cedfaf9d/attachment-0001.html>