[cfe-dev] [analyzer] Condition optimization improvements for RangeConstraintManager

[Balázs Benics via cfe-dev]

The ranged based constraint manager is kinda weak, we all know that.
To circumvent such infeasible bugreports, I highly recommend enabling the
Z3 refutation (`-analyzer-config crosscheck-with-z3=true`)
which validates the constraints on the bugpath. Invalidates the bugreport
if the constraints are UnSAT.
This option would suppress this report for sure.

Another solution is to make the constraint manager smarter, to reason about
sym-sym comparisons, at least for the obvious ones.
My patch under review is partially solving this (still in WIP): D77792
<https://reviews.llvm.org/D77792>

Note that this limitation is well known and understood.
Introducing sym-sym comparisons seems to be valuable, though I'm not
entirely sure how would fit into our model.
It would cover some sym-sym-comparisons, but potentially not all of them.
Debugging why a certain comparison evaluated to true/false would be a
somewhat cumbersome process even if we dump the ExplodedGraph.

Imagine this example:
void transitivity(int x, int y, int z) {
  if (x >= y)
    return;
  // x < y for sure
  if (y >= z)
    return;
  // y < z for sure
  clang_analyzer_eval(x < z); // ?
}

Regards,
Balazs

Denis Petrov via cfe-dev <cfe-dev at lists.llvm.org> ezt írta (időpont: 2020.
ápr. 22., Sze, 22:55):

> Hi, CSA ​community.
>
>
> I got an idea how to make RangeConstraintManager​ more sofisticated.
> I want you speak out, share your vision about this idea.
>
> Actually this bug https://bugs.llvm.org/show_bug.cgi?id=13426 pushed me
> to these thoughts.
>
> Let's consider the next snippet:
>
>
> int foo(int y, int x) {
> int x;
> if (y == z) {
> x = 0;
> }
> if (y != z) {
> x = 1;
> }
> return x;
> }
>
> Finally CSA reports you:
> warning: Undefined or garbage value returned to caller
>       [core.uninitialized.UndefReturn]
>         return x;
>
> But as a human you know that `x` has definitely been initialized.
> As you can see CSA builds paths without relying on previous
> conditions (except the case {A-B} {B-A}m it is already done).
> The same behavior appears when:
> (y >  z) (y <= z)
> (y <= z) (y >  z)​
> (y == z) (z != y)​
> etc.
> I made a solution for this but have not upload it for review yet.
>
> I also have some more thoughts about optimization such:
> if (y <  z) {}
> if (y <= z) {} // which is a subset of (y < z)
>
> I can continue to do this improvement and show you the result soon.
>
>
> ------------------------------
> *Denys Petrov*
> Senior С++ Developer | Kharkiv, Ukraine
>
> _______________________________________________
> 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/20200424/2af84a34/attachment.html>