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

Gabor Marton via Phabricator via cfe-commits cfe-commits at lists.llvm.org
Thu Apr 28 09:43:58 PDT 2022


martong added a comment.

Thanks Denys for the update! This is getting really good.

I have some concerns though about the `CastMap = Map<uint32_t, RangeSet>`. I think we should have `CastMap = Map<uint32_t, EquivalenceClass>` instead, and we could get the `RangeSet` from the existing `ConstraintRange` mapping. By storing directly the `RangeSet`, the State might get out-of-sync when we introduce a constraint to another member in an equivalence class. (Besides that, our mapping of constraints is happening always by using the EquivalenceClasses as keys.)
I think this could solve the problematic code you posted earlier

  int x, y;
  if(x == y)
    if ((char)x == 2)
      if(y == 259)
        // Here we shall update `(char)x` and find this branch infeasible.

Here we have EqClass1: [x, y] , EqClass2: [(char)x] and they are not the same class, thus when you iterate over the CastMap, you can get the updated RangeSet for both classes, and the infeasibility can be discovered.

About this:

  if(x == (short)y)
    // What we should do(store) with(in) `EquivalenceClass`es.

In this case, we have one EqClass with two members,  the SymbolRef `x` and the SymbolCast `(short)y`. They both must have the same `RangeSet` associated to them. And this is already implemented. By referreing to the EqClass in the CastMap, we simply can reuse this information.



================
Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1229-1230
+  // bool -  parsing successfully occured.
+  using SymbolCastParsedStruct =
+      std::tuple<SymbolRef, QualType, uint32_t, NestedTypesOfSymbolCast, bool>;
+
----------------
By using `llvm::Expected<T>` we would be more aligned with the [[ https://llvm.org/docs/ProgrammersManual.html#recoverable-errors |  llvm error handling practices ]]. Besides, the `bool` in the tuple and the `Success` variable in the function below would not be needed.


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

https://reviews.llvm.org/D103096



More information about the cfe-commits mailing list