[PATCH] D82445: [analyzer][solver] Track symbol equivalence

[Valeriy Savchenko via Phabricator via cfe-commits]

vsavchenko marked 8 inline comments as done.
vsavchenko added inline comments.


================
Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:506
+  APSIntType Type(Int);
+  return Int == Type.getZeroValue();
+}
----------------
xazax.hun wrote:
> Does the semantics if this differ from ` llvm::APInt::isNullValue`?
Good catch!


================
Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1254
+    //       sufficient.
+    return S1->get<ConstraintRange>() == S2->get<ConstraintRange>() &&
+           S1->get<ClassMap>() == S2->get<ClassMap>();
----------------
xazax.hun wrote:
> xazax.hun wrote:
> > Sorry, but I am a bit confused here.
> > 
> > Does `haveEqualConstraints` have anything to do with equivalence classes?
> > 
> > I.e., what if I have two symbols with the same constraints (but those two symbols were never compared).
> > ```
> > void f(int a, int b) {
> >   int c = clamp(a, 5, 10);
> >   int d = clamp(b, 5, 10);
> > }
> > ```
> > 
> > In the code above if analyzer understands clamp, the range for `c` and `d` will be the same. Even though we never really compared them.
> > I would expect `haveEqualConstraints` to return true, even if they do not belong to the same equivalence class.
> > 
> > Do I miss something?
> Never mind, I misunderstood this function. It operates on program states not on symbols.
Nothing to be sorry about, I'm happy to clarify!

`haveEqualConstraints` is here for our join heuristic that helps removing duplicating paths.


================
Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1380
 
+ConstraintMap ento::getConstraintMap(ProgramStateRef State) {
+  ConstraintMap::Factory &F = State->get_context<ConstraintMap>();
----------------
xazax.hun wrote:
> So we basically do a conversion to Symbol -> Ranges from Class -> Ranges.
> I wonder if it is possible to get rid of this conversion in the future to get some performance benefits.
> We could either make all code work with both kind of range maps or have something like (Symbol + Class) -> Ranges to avoid conversion.
> What do you think?
> 
> I am not opposed to this code at the moment, I just wonder if there is a relatively low hanging fruit for some performance gains in the future.
This is here only for a very specific mode - when we double check found warnings with Z3.  That mode needs constraints assigned to symbols, so here we construct such a set on-the-fly.  So, we store ALL of the ranges in the map Class -> Ranges and construct Symbol -> Ranges on very special occasions.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D82445