[PATCH] D49074: [Analyzer] [WIP] Basic support for multiplication and division in the constraint manager

[Balogh, Ádám via Phabricator via cfe-commits]

baloghadamsoftware added a comment.

I evaluated this patch on different open-source projects, with Z3 refutation off and on:

F9660704: MulDivEvaluation.xlsx <https://reviews.llvm.org/F9660704>

I cannot always decide whether a bug is false positive or true positive. Most of them seem false positives. Honestly, we cannot except too many true positives in these projects. My findings:

- Execution time is largely unaffected. The most interesting thing here is that in one case (PostGreS) Z3 refutation causes 7x execution time with the original range-based constraint manager, but only 1,5x with our patch. The reason for this could be that with the more advanced range-based constraint manager the analyzer does not produce the problematic false positive on which the Z3 refutation spends a huge time.

- In case of Curl and also in case of BitCoin we found false positives not produced with our patch but produced with the original, even with Z3 enabled.

- The extra false positives produced by the analyzer with our patch are not caused by bugs in the implementation of division and multiplication of ranges but the less "unknown" symbolic values. Without the patch the result of a multiplication or division was unknown so the analyzer could not reason about it. Now with the patch it has a valid range so the analyzer can reason about it and report bugs (which may be false positives as well).


CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D49074/new/

https://reviews.llvm.org/D49074