[analyzer] Condition optimization improvements for RangeConstraintManager

classic Classic list List threaded Threaded
2 messages Options
Reply | Threaded
Open this post in threaded view
|

[analyzer] Condition optimization improvements for RangeConstraintManager

Fangrui Song via cfe-dev

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
[hidden email]
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
Reply | Threaded
Open this post in threaded view
|

Re: [analyzer] Condition optimization improvements for RangeConstraintManager

Fangrui Song 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

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 <[hidden email]> 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
[hidden email]
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev

_______________________________________________
cfe-dev mailing list
[hidden email]
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev