Generating range constraints in the static analyzer

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

Generating range constraints in the static analyzer

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

Re: Generating range constraints in the static analyzer

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

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 <[hidden email]> 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
[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
Reply | Threaded
Open this post in threaded view
|

Re: Generating range constraints in the static analyzer

Fangrui Song via cfe-dev
Hello,

My hope was to aim for limited accuracy, simply because the overall complexity of the bitshift constraint is fairly simple. However, in the use case we are looking at, a large slowdown (I've read 15x, although that may be untrue now) for Z3 seems pretty bad.

I have been looking at a plugin for implementing this check, and since it sounds like the constraint manager doesn't have anything already to calculate more complex constraints, I intend to keep looking at calculating them as needed for the bitshift verification. This avoids direct interaction with the Ranged Constraint Manager, and just uses the results it produces, hopefully.

Thank you for the insight.

Best,
Christoph

On Sun, Apr 19, 2020 at 5:41 AM Balázs Benics <[hidden email]> wrote:
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

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 <[hidden email]> 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
[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