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

_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

Reply via email to