[Analyzer][solver] Do not remove the simplified symbol from the eq class

[martong]

Summary

Currently, during symbol simplification we remove the original member symbol
from the equivalence class (ClassMembers trait). However, we keep the
reverse link (ClassMap trait), in order to be able the query the
related constraints even for the old member. This asymmetry can lead to
a problem when we merge equivalence classes:

ClassA: [a, b]   // ClassMembers trait,
a->a, b->a       // ClassMap trait, a is the representative symbol

Now let,s delete a:

ClassA: [b]
a->a, b->a

Let's merge ClassA into the trivial class c:

ClassA: [c, b]
c->c, b->c, a->a

Now, after the merge operation, c and a are actually in different
equivalence classes, which is inconsistent.

One solution to this problem is to simply avoid removing the original
member and this is what this patch does.

Other options I have considered:

1. Always merge the trivial class into the non-trivial class. This might work most of the time, however, will fail if we have to merge two non-trivial classes (in that case we no longer can track equivalences precisely).
2. In removeMember, update the reverse link as well. This would cease the inconsistency, but we'd loose precision since we could not query the constraints for the removed member.

[steakhal]

I see. Simplification is always good. Let's measure and compare the runtime characteristics before moving forward.

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

2226

Emphasize what you mean by relaxation. You meant probably something like not replacing the complex symbol, just adding the simplified version to the class.

2227

nor memory consumption

2228–2229

Could you please elaborate on this in the review? I don't get the reasoning. I might miss something.

clang/test/Analysis/symbol-simplification-disequality-info.cpp

15–27

Please try to omit unnecessary changes.

[martong]

• Update a comment

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

2226

ok

2227

ok

2228–2229

It's not a reasoning, just a guessing. Another reason could be that simply the time we spend here is negligible compared to the time we spend e.g. in removeDeadBindings. (Actually, removeDeadBindings is very hot and takes roughly 15-20 % of the runtime.) Perhaps I could do a measurement with a sampling profiler to be able to provide a precise explanation to this. But I think the point is that the runtime/memory consumption do not grow and the concrete reason is secondary.

However, you are right, I should not get into guessing here, I'll just remove this sentence.

clang/test/Analysis/symbol-simplification-disequality-info.cpp

15–27

I've made this change intentionally, so all hunks for each simplification steps are indented similarly. E.g., after the CHECK-NEXT: string comes 3 space characters until we the { character, see L16 and L34 and L51. Actually, I've made an indentation error in a previous patch, which I though I can correct now.

[martong]

In D114619#3155363, @steakhal wrote:

I see. Simplification is always good. Let's measure and compare the runtime characteristics before moving forward.

Here they are. Seems like the runtime and memory consumption are pretty much the same.

stats.html90 KBDownload

[steakhal]

I think it looks great.

clang/test/Analysis/symbol-simplification-disequality-info.cpp

15–27

Fine by me.

[thakis]

The test sometimes fails flakily: http://45.33.8.238/macm1/22813/step_7.txt

[martong]

In D114619#3164898, @thakis wrote:

The test sometimes fails flakily: http://45.33.8.238/macm1/22813/step_7.txt

Thanks @thakis for the report, I am aware of the issue and addressing that in
https://reviews.llvm.org/D114887

[martong]

@thakis, if the issue is really disturbing and cannot wait until the review of D114887 finishes then please do a revert of this patch. But then the dependent child patch D103317 needs to be reverted as well.
I am trying my best to make D114887 reviewed in the next 24 hours.

[martong]

I've had the confidence to commit D114887, the test should not be flaky anymore.

[thakis]

Thanks for the fix!

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

public:
   getDisequalClasses(DisequalityMapTy Map, ClassSet::Factory &Factory) const;
 
   LLVM_NODISCARD static inline Optional<bool> areEqual(ProgramStateRef State,
                                                        EquivalenceClass First,
                                                        EquivalenceClass Second);
   LLVM_NODISCARD static inline Optional<bool>
   areEqual(ProgramStateRef State, SymbolRef First, SymbolRef Second);
 
-  /// Remove one member from the class.
-  LLVM_NODISCARD ProgramStateRef removeMember(ProgramStateRef State,
-                                              const SymbolRef Old);
-
   /// Iterate over all symbols and try to simplify them.
   LLVM_NODISCARD static inline ProgramStateRef simplify(SValBuilder &SVB,
                                                         RangeSet::Factory &F,
                                                         ProgramStateRef State,
                                                         EquivalenceClass Class);
 
   void dumpToStream(ProgramStateRef State, raw_ostream &os) const;
   LLVM_DUMP_METHOD void dump(ProgramStateRef State) const {
inline Optional<bool> EquivalenceClass::areEqual(ProgramStateRef State,
   ClassSet DisequalToFirst = First.getDisequalClasses(State);
   if (DisequalToFirst.contains(Second))
     return false;
 
   // It is not clear.
   return llvm::None;
 }
 
-LLVM_NODISCARD ProgramStateRef
-EquivalenceClass::removeMember(ProgramStateRef State, const SymbolRef Old) {
-
-  SymbolSet ClsMembers = getClassMembers(State);
-  assert(ClsMembers.contains(Old));
-
-  // We don't remove `Old`'s Sym->Class relation for two reasons:
-  // 1) This way constraints for the old symbol can still be found via it's
-  // equivalence class that it used to be the member of.
-  // 2) Performance and resource reasons. We can spare one removal and thus one
-  // additional tree in the forest of `ClassMap`.
-
-  // Remove `Old`'s Class->Sym relation.
-  SymbolSet::Factory &F = getMembersFactory(State);
-  ClassMembersTy::Factory &EMFactory = State->get_context<ClassMembers>();
-  ClsMembers = F.remove(ClsMembers, Old);
-  // Ensure another precondition of the removeMember function (we can check
-  // this only with isEmpty, thus we have to do the remove first).
-  assert(!ClsMembers.isEmpty() &&
-         "Class should have had at least two members before member removal");
-  // Overwrite the existing members assigned to this class.
-  ClassMembersTy ClassMembersMap = State->get<ClassMembers>();
-  ClassMembersMap = EMFactory.add(ClassMembersMap, *this, ClsMembers);
-  State = State->set<ClassMembers>(ClassMembersMap);
-
-  return State;
-}
-
 // Re-evaluate an SVal with top-level `State->assume` logic.
 LLVM_NODISCARD ProgramStateRef reAssume(ProgramStateRef State,
                                         const RangeSet *Constraint,
                                         SVal TheValue) {
   if (!Constraint)
     return State;
 
   const auto DefinedVal = TheValue.castAs<DefinedSVal>();
if (SimplifiedMemberSym && MemberSym != SimplifiedMemberSym) {
       State = merge(F, State, MemberSym, SimplifiedMemberSym);
       if (!State)
         return nullptr;
       // No state change, no merge happened actually.
       if (OldState == State)
         continue;
 
       assert(find(State, MemberSym) == find(State, SimplifiedMemberSym));
-      // Remove the old and more complex symbol.
-      State = find(State, MemberSym).removeMember(State, MemberSym);
 
       // Query the class constraint again b/c that may have changed during the
       // merge above.
       const RangeSet *ClassConstraint = getConstraint(State, Class);
 
       // Re-evaluate an SVal with top-level `State->assume`, this ignites
       // a RECURSIVE algorithm that will reach a FIXPOINT.
       //
       // About performance and complexity: Let us assume that in a State we
       // have N non-trivial equivalence classes and that all constraints and
       // disequality info is related to non-trivial classes. In the worst case,
-      // we can simplify only one symbol of one class in each iteration. The
-      // number of symbols in one class cannot grow b/c we replace the old
-      // symbol with the simplified one. Also, the number of the equivalence
-      // classes can decrease only, b/c the algorithm does a merge operation
-      // optionally. We need N iterations in this case to reach the fixpoint.
-      // Thus, the steps needed to be done in the worst case is proportional to
-      // N*N.
+      // we can simplify only one symbol of one class in each iteration.
       //
+      // The number of the equivalence classes can decrease only, because the
+      // algorithm does a merge operation optionally.
+      // ASSUMPTION G: Let us assume that the
+      // number of symbols in one class cannot grow because we replace the old
+      // symbol with the simplified one.
+      // If assumption G holds then we need N iterations in this case to reach
+      // the fixpoint. Thus, the steps needed to be done in the worst case is
+      // proportional to N*N.
       // This worst case scenario can be extended to that case when we have
       // trivial classes in the constraints and in the disequality map. This
       // case can be reduced to the case with a State where there are only
       // non-trivial classes. This is because a merge operation on two trivial
       // classes results in one non-trivial class.
+      //
+      // Empirical measurements show that if we relax assumption G (i.e. if we
+      // do not replace the complex symbol just add the simplified one) then
+      // the runtime and memory consumption does not grow noticeably.
       State = reAssume(State, ClassConstraint, SimplifiedMemberVal);
       if (!State)
         return nullptr;
     }
   }
   return State;
 }
 
 inline ClassSet EquivalenceClass::getDisequalClasses(ProgramStateRef State,

clang/test/Analysis/expr-inspection-printState-eq-classes.c

void test_equivalence_classes(int a, int b, int c, int d) {
   if (b != 0)
     return;
   clang_analyzer_printState();
   (void)(a * b * c * d);
   return;
 }
 
 // CHECK:      "equivalence_classes": [
-// CHECK-NEXT:     [ "(reg_$0<int a>) != (reg_$2<int c>)" ],
-// CHECK-NEXT:     [ "reg_$0<int a>", "reg_$2<int c>", "reg_$3<int d>" ]
+// CHECK-NEXT:   [ "((reg_$0<int a>) + (reg_$1<int b>)) != (reg_$2<int c>)", "(reg_$0<int a>) != (reg_$2<int c>)" ],
+// CHECK-NEXT:   [ "(reg_$0<int a>) + (reg_$1<int b>)", "reg_$0<int a>", "reg_$2<int c>", "reg_$3<int d>" ]
 // CHECK-NEXT: ],

clang/test/Analysis/symbol-simplification-disequality-info.cpp

 // RUN: %clang_analyze_cc1 %s \
 // RUN:   -analyzer-checker=core \
 // RUN:   -analyzer-checker=debug.ExprInspection \
 // RUN:   2>&1 | FileCheck %s
 
 // In this test we check how the solver's symbol simplification mechanism
 // simplifies the disequality info.
 
 void clang_analyzer_printState();
 
 void test(int a, int b, int c, int d) {
   if (a + b + c == d)
     return;
   clang_analyzer_printState();
-  // CHECK:       "disequality_info": [
-  // CHECK-NEXT:    {
-  // CHECK-NEXT:      "class": [ "((reg_$0<int a>) + (reg_$1<int b>)) + (reg_$2<int c>)" ],
-  // CHECK-NEXT:      "disequal_to": [
-  // CHECK-NEXT:        [ "reg_$3<int d>" ]]
-  // CHECK-NEXT:    },
-  // CHECK-NEXT:    {
-  // CHECK-NEXT:      "class": [ "reg_$3<int d>" ],
-  // CHECK-NEXT:      "disequal_to": [
-  // CHECK-NEXT:        [ "((reg_$0<int a>) + (reg_$1<int b>)) + (reg_$2<int c>)" ]]
-  // CHECK-NEXT:    }
-  // CHECK-NEXT:  ],
+  // CHECK:      "disequality_info": [
+  // CHECK-NEXT:   {
+  // CHECK-NEXT:     "class": [ "((reg_$0<int a>) + (reg_$1<int b>)) + (reg_$2<int c>)" ],
+  // CHECK-NEXT:     "disequal_to": [
+  // CHECK-NEXT:       [ "reg_$3<int d>" ]]
+  // CHECK-NEXT:   },
+  // CHECK-NEXT:   {
+  // CHECK-NEXT:     "class": [ "reg_$3<int d>" ],
+  // CHECK-NEXT:     "disequal_to": [
+  // CHECK-NEXT:       [ "((reg_$0<int a>) + (reg_$1<int b>)) + (reg_$2<int c>)" ]]
+  // CHECK-NEXT:   }
+  // CHECK-NEXT: ],
 
 
   // Simplification starts here.
   if (b != 0)
     return;
   clang_analyzer_printState();
   // CHECK:      "disequality_info": [
   // CHECK-NEXT:   {
-  // CHECK-NEXT:     "class": [ "(reg_$0<int a>) + (reg_$2<int c>)" ],
+  // CHECK-NEXT:     "class": [ "((reg_$0<int a>) + (reg_$1<int b>)) + (reg_$2<int c>)", "(reg_$0<int a>) + (reg_$2<int c>)" ],
   // CHECK-NEXT:     "disequal_to": [
   // CHECK-NEXT:       [ "reg_$3<int d>" ]]
   // CHECK-NEXT:   },
   // CHECK-NEXT:   {
   // CHECK-NEXT:     "class": [ "reg_$3<int d>" ],
   // CHECK-NEXT:     "disequal_to": [
-  // CHECK-NEXT:        [ "(reg_$0<int a>) + (reg_$2<int c>)" ]]
-  // CHECK-NEXT:    }
-  // CHECK-NEXT:  ],
+  // CHECK-NEXT:       [ "((reg_$0<int a>) + (reg_$1<int b>)) + (reg_$2<int c>)", "(reg_$0<int a>) + (reg_$2<int c>)" ]]
+  // CHECK-NEXT:   }
+  // CHECK-NEXT: ],
 
   if (c != 0)
     return;
   clang_analyzer_printState();
-  // CHECK:       "disequality_info": [
-  // CHECK-NEXT:    {
-  // CHECK-NEXT:      "class": [ "reg_$0<int a>" ],
-  // CHECK-NEXT:      "disequal_to": [
-  // CHECK-NEXT:        [ "reg_$3<int d>" ]]
-  // CHECK-NEXT:    },
-  // CHECK-NEXT:    {
-  // CHECK-NEXT:      "class": [ "reg_$3<int d>" ],
-  // CHECK-NEXT:      "disequal_to": [
-  // CHECK-NEXT:        [ "reg_$0<int a>" ]]
-  // CHECK-NEXT:    }
-  // CHECK-NEXT:  ],
+
+  // CHECK:      "disequality_info": [
+  // CHECK-NEXT:   {
+  // CHECK-NEXT:     "class": [ "((reg_$0<int a>) + (reg_$1<int b>)) + (reg_$2<int c>)", "(reg_$0<int a>) + (reg_$2<int c>)", "reg_$0<int a>" ],
+  // CHECK-NEXT:     "disequal_to": [
+  // CHECK-NEXT:       [ "reg_$3<int d>" ]]
+  // CHECK-NEXT:   },
+  // CHECK-NEXT:   {
+  // CHECK-NEXT:     "class": [ "reg_$3<int d>" ],
+  // CHECK-NEXT:     "disequal_to": [
+  // CHECK-NEXT:       [ "((reg_$0<int a>) + (reg_$1<int b>)) + (reg_$2<int c>)", "(reg_$0<int a>) + (reg_$2<int c>)", "reg_$0<int a>" ]]
+  // CHECK-NEXT:   }
+  // CHECK-NEXT: ],
 
   // Keep the symbols and the constraints! alive.
   (void)(a * b * c * d);
   return;
 }

clang/test/Analysis/symbol-simplification-fixpoint-one-iteration.cpp

void test(int a, int b, int c) {
   // CHECK-NEXT:   [ "(reg_$0<int a>) + (reg_$1<int b>)", "reg_$2<int c>" ]
   // CHECK-NEXT: ],
   // CHECK-NEXT: "disequality_info": null,
 
   // Simplification starts here.
   if (b != 0)
     return;
   clang_analyzer_printState();
-  // CHECK:        "constraints": [
-  // CHECK-NEXT:     { "symbol": "(reg_$0<int a>) != (reg_$2<int c>)", "range": "{ [0, 0] }" },
-  // CHECK-NEXT:     { "symbol": "reg_$1<int b>", "range": "{ [0, 0] }" }
-  // CHECK-NEXT:   ],
-  // CHECK-NEXT:   "equivalence_classes": [
-  // CHECK-NEXT:     [ "(reg_$0<int a>) != (reg_$2<int c>)" ],
-  // CHECK-NEXT:     [ "reg_$0<int a>", "reg_$2<int c>" ]
-  // CHECK-NEXT:   ],
+  // CHECK:      "constraints": [
+  // CHECK-NEXT:   { "symbol": "((reg_$0<int a>) + (reg_$1<int b>)) != (reg_$2<int c>)", "range": "{ [0, 0] }" },
+  // CHECK-NEXT:   { "symbol": "(reg_$0<int a>) != (reg_$2<int c>)", "range": "{ [0, 0] }" },
+  // CHECK-NEXT:   { "symbol": "reg_$1<int b>", "range": "{ [0, 0] }" }
+  // CHECK-NEXT: ],
+  // CHECK-NEXT: "equivalence_classes": [
+  // CHECK-NEXT:   [ "((reg_$0<int a>) + (reg_$1<int b>)) != (reg_$2<int c>)", "(reg_$0<int a>) != (reg_$2<int c>)" ],
+  // CHECK-NEXT:   [ "(reg_$0<int a>) + (reg_$1<int b>)", "reg_$0<int a>", "reg_$2<int c>" ]
+  // CHECK-NEXT: ],
   // CHECK-NEXT: "disequality_info": null,
 
   // Keep the symbols and the constraints! alive.
   (void)(a * b * c);
   return;
 }

clang/test/Analysis/symbol-simplification-fixpoint-two-iterations.cpp

void test(int a, int b, int c, int d) {
   // CHECK-NEXT:   [ "((reg_$0<int a>) + (reg_$1<int b>)) + (reg_$2<int c>)", "reg_$3<int d>" ]
   // CHECK-NEXT: ],
   // CHECK-NEXT: "disequality_info": null,
 
   // Simplification starts here.
   if (b != 0)
     return;
   clang_analyzer_printState();
-  // CHECK:       "constraints": [
-  // CHECK-NEXT:    { "symbol": "(reg_$0<int a>) != (reg_$3<int d>)", "range": "{ [0, 0] }" },
-  // CHECK-NEXT:    { "symbol": "reg_$1<int b>", "range": "{ [0, 0] }" },
-  // CHECK-NEXT:    { "symbol": "reg_$2<int c>", "range": "{ [0, 0] }" }
-  // CHECK-NEXT:  ],
-  // CHECK-NEXT:  "equivalence_classes": [
-  // CHECK-NEXT:    [ "(reg_$0<int a>) != (reg_$3<int d>)" ],
-  // CHECK-NEXT:    [ "reg_$0<int a>", "reg_$3<int d>" ],
-  // CHECK-NEXT:    [ "reg_$2<int c>" ]
-  // CHECK-NEXT:  ],
-  // CHECK-NEXT:  "disequality_info": null,
+  // CHECK:      "constraints": [
+  // CHECK-NEXT:   { "symbol": "(((reg_$0<int a>) + (reg_$1<int b>)) + (reg_$2<int c>)) != (reg_$3<int d>)", "range": "{ [0, 0] }" },
+  // CHECK-NEXT:   { "symbol": "((reg_$0<int a>) + (reg_$2<int c>)) != (reg_$3<int d>)", "range": "{ [0, 0] }" },
+  // CHECK-NEXT:   { "symbol": "(reg_$0<int a>) != (reg_$3<int d>)", "range": "{ [0, 0] }" },
+  // CHECK-NEXT:   { "symbol": "(reg_$2<int c>) + (reg_$1<int b>)", "range": "{ [0, 0] }" },
+  // CHECK-NEXT:   { "symbol": "reg_$1<int b>", "range": "{ [0, 0] }" },
+  // CHECK-NEXT:   { "symbol": "reg_$2<int c>", "range": "{ [0, 0] }" }
+  // CHECK-NEXT: ],
+  // CHECK-NEXT: "equivalence_classes": [
+  // CHECK-NEXT:   [ "(((reg_$0<int a>) + (reg_$1<int b>)) + (reg_$2<int c>)) != (reg_$3<int d>)", "((reg_$0<int a>) + (reg_$2<int c>)) != (reg_$3<int d>)", "(reg_$0<int a>) != (reg_$3<int d>)" ],
+  // CHECK-NEXT:   [ "((reg_$0<int a>) + (reg_$1<int b>)) + (reg_$2<int c>)", "(reg_$0<int a>) + (reg_$2<int c>)", "reg_$0<int a>", "reg_$3<int d>" ],
+  // CHECK-NEXT:   [ "(reg_$2<int c>) + (reg_$1<int b>)", "reg_$2<int c>" ]
+  // CHECK-NEXT: ],
+  // CHECK-NEXT: "disequality_info": null,
 
   // Keep the symbols and the constraints! alive.
   (void)(a * b * c * d);
   return;
 }