Skip to content

Commit

Permalink
[analyzer] Fix symbol simplification assertion failure
Browse files Browse the repository at this point in the history
Fixes #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.

Differential Revision: https://reviews.llvm.org/D126281
  • Loading branch information
Gabor Marton committed May 25, 2022
1 parent 9ffb594 commit f75bc5b
Show file tree
Hide file tree
Showing 2 changed files with 31 additions and 6 deletions.
12 changes: 6 additions & 6 deletions clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
Expand Up @@ -2508,12 +2508,6 @@ 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>();
Expand All @@ -2527,6 +2521,12 @@ EquivalenceClass::removeMember(ProgramStateRef State, const SymbolRef Old) {
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;
}

Expand Down
25 changes: 25 additions & 0 deletions clang/test/Analysis/symbol-simplification-assertion.c
@@ -0,0 +1,25 @@
// 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}}
}

0 comments on commit f75bc5b

Please sign in to comment.