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

baloghadamsoftware updated this revision to Diff 211727. baloghadamsoftware added a comment. Rebased. CHANGES SINCE LAST ACTION https://reviews.llvm.org/D49074/new/ https://reviews.llvm.org/D49074 Files: include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h

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

baloghadamsoftware added a comment. I evaluated this patch on different open-source projects, with Z3 refutation off and on: F9660704: MulDivEvaluation.xlsx I cannot always decide whether a bug is false positive or true positive. Most of them seem false

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

baloghadamsoftware added a comment. I tested this on several open-source projects. Lots of false-positives disappeared. There are also some new findings, mainly new false-positives but not because of this feature but of "loops executed 0 times". CHANGES SINCE LAST ACTION

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

baloghadamsoftware updated this revision to Diff 202192. baloghadamsoftware removed a reviewer: george.karpenkov. baloghadamsoftware added a comment. Herald added a subscriber: Charusso. Rebased. CHANGES SINCE LAST ACTION https://reviews.llvm.org/D49074/new/ https://reviews.llvm.org/D49074

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

baloghadamsoftware added a comment. Here is the proof of the algorithm for `signed char` and `unsigned char` types. The dumper which tests every `n` for the `n*k m` relation and creates ranges from values satisfying the expression for every `k` and `m` produces exactly the same output as the

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

baloghadamsoftware updated this revision to Diff 174190. baloghadamsoftware added a comment. Herald added a subscriber: gamesh411. Rebased on the previous part. Tests updated for the now default `eagerly assume` mode. https://reviews.llvm.org/D49074 Files:

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

baloghadamsoftware added a comment. Since modifications of the infrastructure are always error-prone I tried to generate tests to have full coverage for smaller numbers. However for full coverage I need type `signed char` and `unsigned char`, but these tests failed because of this bug: Bug

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

baloghadamsoftware added a comment. This also solves the examples in the comment of bug 32911 . https://reviews.llvm.org/D49074 ___ cfe-commits mailing list cfe-commits@lists.llvm.org

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

baloghadamsoftware added a comment. Disabled? No, that was a different thing. I have some ideas there as well, how to solve it, but it was the rearrangement in the `SValBuilder`. This one is one level lower, the `ConstraintManager` which only calculate the range for a symbol where we have and

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

george.karpenkov added a comment. > where addition and subtraction is already supported? Is it though? From what I recall we had to disable it from the default set of options due to the fact that it gives rise to the exponential running time in some cases. I am somewhat afraid of similar

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

baloghadamsoftware added a comment. Of course we would like to try the Z3 for refutation, we do not dispute its usefulness. This patch is about something really different. It extends the range-based constraint manager in a very natural way. Is the code of the range-based constraint manager

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

george.karpenkov added a comment. @baloghadamsoftware @xazax.hun we've had very promising results with using Z3 for refutation so far, almost at no cost, see Mikhail's recent email on cfe-dev (and sometimes at a negative cost!). Do you still not want to try it first? False negatives could be

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

baloghadamsoftware updated this revision to Diff 159012. baloghadamsoftware edited the summary of this revision. baloghadamsoftware added a comment. Completely rewritten: works correctly for modular arithmetic (multiplication), works correctly for truncation (division), only uses integers, no

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

baloghadamsoftware added a comment. In https://reviews.llvm.org/D49074#1160793, @NoQ wrote: > I'd also rather stick to integer arithmetic and avoid using floats even in > intermediate calculations. It'd be hard to make sure that no rounding errors > kick in if we use floats. Yes, I agree. I

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

NoQ added a comment. I'd also rather stick to integer arithmetic and avoid using floats even in intermediate calculations. It'd be hard to make sure that no rounding errors kick in if we use floats. https://reviews.llvm.org/D49074 ___ cfe-commits

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

george.karpenkov added a comment. > The imprecision in the built in solver might result in failure to constrain a > value to zero while the Z3 might be able to do that. Ah right, that's a good point, we only throw a null-pointer deref/division by zero when the pointer/value is definitely zero.

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

xazax.hun added a comment. In https://reviews.llvm.org/D49074#1159095, @george.karpenkov wrote: > > This may remove false-positives (like the example above), but we surely > > cannot find new errors where multiplicative operations are used. > > Do you have examples of those? In my

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

george.karpenkov added a comment. > What issues could it cause since it is guarded by an option? I've meant the rearrangement. Actually, I would like to apologize for that point, I thought it was causing some issues, but it wasn't, we've just checked it yesterday. > As far as I know the

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

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

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

baloghadamsoftware added a comment. In https://reviews.llvm.org/D49074#1156609, @george.karpenkov wrote: > The overall point is that writing this kind of code is *extremely* > error-prone. Every modifications on the core is extremely error-prone. That is why we must cross check it and only

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

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

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

george.karpenkov added a comment. The overall point is that writing this kind of code is *extremely* error-prone. We are actually considering going in a different direction and doing a rollback for the previous rearrangement patches due to some issues. Could you see whether Z3 visitor would meet

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

NoQ added inline comments. 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}} If `int` is 32-bit and `x` equal to

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

george.karpenkov requested changes to this revision. george.karpenkov added a comment. This revision now requires changes to proceed. Let's discuss alternatives first. https://reviews.llvm.org/D49074 ___ cfe-commits mailing list

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

george.karpenkov added a comment. @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? https://reviews.llvm.org/D49074

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

baloghadamsoftware added a comment. This seems to solve https://bugs.llvm.org/show_bug.cgi?id=32911. https://reviews.llvm.org/D49074 ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

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

baloghadamsoftware added a comment. All existing tests pass. I could not find the appropriate test file so I created a new one, but this is probably not the correct way. https://reviews.llvm.org/D49074 ___ cfe-commits mailing list

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

baloghadamsoftware created this revision. baloghadamsoftware added reviewers: NoQ, dcoughlin. Herald added subscribers: mikhail.ramalho, a.sidorin, szepet. Herald added a reviewer: george.karpenkov. Currently, the default (range-based) constrain manager supports symbolic expressions of the