[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.

In https://reviews.llvm.org/D49074#1156110, @george.karpenkov wrote:

> @baloghadamsoftware @dkrupp @xazax.hun Interesting. What do you think about instead using Z3 cross-check functionality recently added, to solve this and all other similar problems instead?


Using Z3 generally is 20 to 30 times slower according to our measurements. This means that a 8 hours analysis (one night, this is quite common) would take 7-10 days. Our customers would never accept that. As far as I know the purpose of the cross-check functionality is to execute Z3 only for the cases which are too complex for the range-based constraint manager. If we regard simple multiplications and divisions as too complex cases we are afraid that it still takes too long. That is why we try to reduce the set of too complex cases by improving the range-based constraint manager.

As we discussed with @dcoughlin at the Euro LLVM 2018 the community should consider a new constraint manager, which is in between the range-based one and the Z3 both feature and performance wise. However, this is something long term, until then we should improve the existing one  as far as reasonable. I am sure that multiplicative operations can be solved similarly to the additive ones.



================
Comment at: test/Analysis/constraint_manager_scale.c:78
+  assert(x * 2 < 8);
+  clang_analyzer_eval(x < 4); // expected-warning{{TRUE}}
+  clang_analyzer_eval(x < 2); // expected-warning{{UNKNOWN}}
----------------
NoQ wrote:
> If `int` is 32-bit and `x` equal to 2³¹ - 1, we have `x * 2` equal to `-2` which is less than 8, while `x` is greater than 4.
Thank you for pointing me out this! I uploaded this patch as WIP since I was sure I missed something because of modular arithmetic. I think this can be solved, even if not so easily. Maybe we should restrict the first version to division only?


https://reviews.llvm.org/D49074