[analyzer] Fix symbol simplification assertion failure

[martong]

Summary

Fixes https://github.com/llvm/llvm-project/issues/55546

The assertion mentioned in the issue is triggered because an
inconsistency is formed in the Sym->Class and Class->Sym relations. A
simpler but similar inconsistency is demonstrated here:
https://reviews.llvm.org/D114887 .

Previously in removeMember, we didn't remove the old symbol's
Sym->Class relation. Back then, we explained it with the following two
bullet points:

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.

This patch do remove the old symbol's Sym->Class relation in order to
keep the Sym->Class relation consistent with the Class->Sym relations.
Point 2) above has negligible performance impact, empirical measurements
do not show any noticeable difference in the run-time. Point 1) above
seems to be a not well justified statement. This is because we cannot
create a new symbol that would be equal to the old symbol after the
simplification had happened. The reason for this is that the SValBuilder
uses the available constant constraints for each sub-symbol.

[martong]

clang/test/Analysis/symbol-simplification-assertion.c

16–19

TODO remove.

[martong]

Point 2) above has negligible performance impact, empirical measurements do not show any noticeable difference in the run-time.

Attaching the measurement results that show the run-time difference is not noticeable, or rather it is within the margin of measurement error.

[steakhal]

In D126281#3533755, @martong wrote:

Point 2) above has negligible performance impact, empirical measurements do not show any noticeable difference in the run-time.

Attaching the measurement results that show the run-time difference is not noticeable, or rather it is within the margin of measurement error.

Can C++ projects behave differently?

Please add the Fixes #55546 comment into the commit message, to let GitHub recognize this.

clang/test/Analysis/symbol-simplification-assertion.c

28

Is this statement still reachable? Demonstrate it by using the clang_analyzer_warnIfReached().

[martong]

• Add clang_analyzer_warnIfReached() to the test and remove unused debug function decls

clang/test/Analysis/symbol-simplification-assertion.c

28

Ok, I've added that.

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

 }
 
 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);
 
+  // Remove `Old`'s Sym->Class relation.
+  ClassMapTy Classes = State->get<ClassMap>();
+  ClassMapTy::Factory &CMF = State->get_context<ClassMap>();
+  Classes = CMF.remove(Classes, Old);
+  State = State->set<ClassMap>(Classes);
+
   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)

clang/test/Analysis/symbol-simplification-assertion.c

+// RUN: %clang_analyze_cc1 %s \
+// RUN:   -analyzer-checker=core \
+// RUN:   -analyzer-checker=debug.ExprInspection \
+// RUN:   -analyzer-config eagerly-assume=true \
+// RUN:   -verify
+
+// Here we test that no assertion is fired during symbol simplification.
+// Related issue: https://github.com/llvm/llvm-project/issues/55546
+
+extern void abort() __attribute__((__noreturn__));
+#define assert(expr) ((expr) ? (void)(0) : abort())
+
+void clang_analyzer_warnIfReached();
+
+int a, b, c;
+long L, L1;
+void test() {
+  assert(a + L + 1 + b != c);
+  assert(L == a);
+  assert(c == 0);
+  L1 = 0;
+  assert(a + L1 + 1 + b != c);
+  assert(a == 0); // no-assertion
+  clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+}