baloghadamsoftware added a comment.

In, @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?

cfe-commits mailing list

Reply via email to