[PATCH] D138037: [analyzer] Remove unjustified assertion from EQClass::simplify

[Balázs Benics via Phabricator via cfe-commits]

steakhal updated this revision to Diff 475480.
steakhal added a comment.

Add test case.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D138037

Files:
  clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
  clang/test/Analysis/symbol-simplification-symplify-results-in-dead-symbol.cpp


Index: clang/test/Analysis/symbol-simplification-symplify-results-in-dead-symbol.cpp
===================================================================
--- /dev/null
+++ clang/test/Analysis/symbol-simplification-symplify-results-in-dead-symbol.cpp
@@ -0,0 +1,11 @@
+// RUN: %clang_analyze_cc1 -analyzer-checker=core -verify %s
+// expected-no-diagnostics
+
+#define assert(cond) if (!(cond)) return
+
+unsigned a, b;
+void f(unsigned c) {
+  assert(c == b);
+  assert((c | a) != a);
+  assert(a); // no-crash
+}
Index: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
===================================================================
--- clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
+++ clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
@@ -2616,7 +2616,18 @@
       if (OldState == State)
         continue;
 
-      assert(find(State, MemberSym) == find(State, SimplifiedMemberSym));
+      // Be aware that `SimplifiedMemberSym` might refer to an already dead
+      // symbol. In that case, the eqclass of that might not be the same as the
+      // eqclass of `MemberSym`. This is because the dead symbols are not
+      // preserved in the `ClassMap`, hence
+      // `find(State, SimplifiedMemberSym)` will result in a trivial eqclass
+      // compared to the eqclass of `MemberSym`.
+      // These eqclasses should be the same if `SimplifiedMemberSym` is alive.
+      // --> assert(find(State, MemberSym) == find(State, SimplifiedMemberSym))
+      //
+      // Note that `MemberSym` must be alive here since that is from the
+      // `ClassMembers` where all the symbols are alive.
+
       // Remove the old and more complex symbol.
       State = find(State, MemberSym).removeMember(State, MemberSym);
 


-------------- next part --------------
A non-text attachment was scrubbed...
Name: D138037.475480.patch
Type: text/x-patch
Size: 1749 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20221115/5b45a471/attachment-0001.bin>