[PATCH] D80117: [analyzer] Introduce reasoning about symbolic remainder operator

[Artem Dergachev via Phabricator via cfe-commits]

NoQ accepted this revision.
NoQ added a comment.
This revision is now accepted and ready to land.

Aha, so performance regressions on real code weren't real, that's a relief :)

> I believe that as of now we can submit these modifications as is and explore performance optimizations later if needed.

I still encourage you to explore the tests we have from our previous attempts to simplify expressions recursively without memoization (`test/Analysis/hangs.c`). I'm asking because these aren't all that artificial: this kind of code was previously reported by a frustrated user as "the analyzer started hanging on my code". Like, please replace a bunch of `+`es with `&`/`|`/`%` and see if this causes your code to perform exponentially over the size of the program. If so, i'd rather have us hurry up and implement memoization.

The math in this patch looks great, thanks!



================
Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:506-507
+  ///
+  /// where abs(Origin) is the maximal absolute value of any possible values
+  ///       from Origin, and min(T) is a minimal value for the type T.
+  ///
----------------
I suggest not trying to express signed types and unsigned types in a single formula, the reader will have to unwrap it back into the two cases anyway in order to understand what's going on.

The following would imho be easier to read: "If T is signed, return the smallest range `[-x..x]` that covers the original range, or `[-min(T), max(T)]` if the aforementioned symmetric range doesn't exist due to original range covering `min(T)`). If T is unsigned, return the smallest range `[0..x]` that covers the original range".


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D80117