[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.
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
More information about the cfe-commits