[PATCH] D103096: [analyzer] Implement cast for ranges of symbolic integers

Gabor Marton via Phabricator via cfe-commits cfe-commits at lists.llvm.org
Thu Jun 30 09:48:51 PDT 2022


martong added a comment.

In D103096#3613059 <https://reviews.llvm.org/D103096#3613059>, @ASDenysPetrov wrote:

> @martong Just FYI. I've been working on reworking this solution to using `EquivalenceClasses` for several weeks. It turned out that this is an extremely hard task to acomplish. There're a lot of cast cases like: `(int8)x==y, (uint16)a==(int64)b, (uint8)y == b`, Merging and inferring all of this without going beyond the complexity O(n) is really tricky.

Please elaborate. I don't see how is it different than merging and inferring without the handling of casts. My understanding is that, we have more symbols (additional `SymbolCast`s) indeed. But, the merging algorithm should not change at all, that should be agnostic to the actual symbol kind (whether that is a `SymbolCast` or a `SymbolData` or a `SymSymEpxr`).
The infer algorithm might be different though, but there I think the original algorithm you delved for `SymExpr`s should work as well for `EquivalenceClass`es.



================
Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1289-1291
+      auto It = llvm::find_if(*CM, [MinBitWidth](CastMap::value_type &Item) {
+        return Item.first >= MinBitWidth;
+      });
----------------
ASDenysPetrov wrote:
> martong wrote:
> > There might be a problem here because the iteration of the map is non-deterministic. We should probably have a copy that is sorted, or the container should be sorted (sorted immutable list maybe?).
> > 
> > Your tests below passed probably because the cast chains are too small. Could you please have a test, where the chain is really long (20 maybe) and shuffled.
> > (My thanks for @steakhal for this additional comment.)
> I've checked. `ImmutableSet` gave me a sorted order. But I agree that it could be just a coincidence. I'll try to add more tests.
Yes, your are right, and I was wrong. `ImmutableSet` is based on an AVL tree, which is a balanced binary tree and the `begin()` gives such an iterator that conducts an inorder - thus sorted - traversal. And the key is an integer. (I don't know now how, but we were mislead, @steakhal too. I guess, we thought that the key of `CastMap` is a pointer.)


================
Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:2300-2303
+    for (auto &Item : *CM) {
+      // Stop after reaching a bigger bitwidth.
+      if (Item.first > MinBitWidth)
+        break;
----------------
martong wrote:
> Same here.
Please disregard the comment above.


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

https://reviews.llvm.org/D103096



More information about the cfe-commits mailing list