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
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
