Page MenuHomePhabricator

[analyzer] Use DisequalityMap while inferring constraints
AbandonedPublic

Authored by ASDenysPetrov on Aug 2 2022, 11:45 AM.

Details

Summary

Infer range using associated unequal symbols from DisequalityMap.
Example:

if(x == 42)
  if(x != y)
    y; // [-2147483648, 41]U[43, 2147483647]
NOTE: Currently, this revision causes test failure due to assertion in related to IteratorModeling.cpp in relateSymbols on line assert(isa<SymIntExpr>(CompSym) && "Symbol comparison must be a SymIntExpr`");`. It needs to be fixed in some way before loading. The revision is exposed to show the motivation for D130372.

Diff Detail

Event Timeline

ASDenysPetrov created this revision.Aug 2 2022, 11:45 AM
Herald added a project: Restricted Project. · View Herald TranscriptAug 2 2022, 11:45 AM
ASDenysPetrov requested review of this revision.Aug 2 2022, 11:45 AM

Awesome!

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
1512–1516

unite should be working with an empty set as well, shouldn't it?

clang/test/Analysis/range-inferring-from-disequality-map.cpp
10–11

Good point.

We should have an additional check in removeDeadBindings that goes through the disequality map of the dead symbol. And if any of the mapped classes are not dead then we shall not delete the dead symbol's equivalent class.

50–51

Why can't we return an empty set from getInvertedRangeFromDisequalityMap in this case? intersect should handle the rest then.

martong added inline comments.Aug 4 2022, 2:53 AM
clang/test/Analysis/range-inferring-from-disequality-map.cpp
10–11

Good point.

We should have an additional check in removeDeadBindings that goes through the disequality map of the dead symbol. And if any of the mapped classes are not dead then we shall not delete the dead symbol's equivalent class.

It would be better to address that in a child patch.

Awesome!

Thank you!

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
1512–1516

You are right.

It's interesting that for some reason I was sure that unite returns empty if any given set is empty (mixed up with intersect). And this is at a time when I'm the author of unite :-P

clang/test/Analysis/range-inferring-from-disequality-map.cpp
50–51

Currently, we can't. At least, in this patch.
We produce infeasible branches (aka nullptr ProgramStateRef) when use ConstraintAssignor::assign.
But here we use SymbolicRangeInferrer which only produces a RangeSet. In other words, we don't store this range anywhere but infer it every time.

Basically, this is a work for the next patches. They should remove the TODOs.

martong added inline comments.Aug 4 2022, 11:45 AM
clang/test/Analysis/range-inferring-from-disequality-map.cpp
50–51

You mean this hunk?

for (EquivalenceClass DisequalClass : Class.getDisequalClasses(State)) {
 RangeSet UpdatedConstraint = SymbolicRangeInferrer::inferRange(
     RangeFactory, State, DisequalClass);

 UpdatedConstraint = RangeFactory.deletePoint(UpdatedConstraint, *Point);

 // If we end up with at least one of the disequal classes to be
 // constrained with an empty range-set, the state is infeasible.
 if (UpdatedConstraint.isEmpty())
   return nullptr;

Yeah, I am not sure why do we infer a range here instead of simply getting the associated range from the constraint set. Inferring here might result with an inconsistent result. I think we should infer only in the SymbolicRangeInferrer.

ASDenysPetrov added a comment.EditedAug 9 2022, 10:59 AM

@martong
This solution has an essential logical mistake. It relies on the erroneous assumption that
if x > 0 && x != y then y is in range [MIN, 0] but that's not true.
x and y could be 1 and 2 respectively.

My idea will only work with concrete ints but not ranges and it is already implemented in RangeConstraintManager in the snippet you mentioned (ConstraintAssignor::assign).

I'm sorry for the lost time.

P.S. The best I can do is just to add more tests for this. Created D131514 instead.

ASDenysPetrov abandoned this revision.Aug 9 2022, 11:08 AM