[clang] [analyzer][solver] On SymSym RelOps, check EQClass members for contradictions (PR #71284)

via cfe-commits cfe-commits at lists.llvm.org
Mon Nov 6 03:14:40 PST 2023


================
@@ -2218,11 +2224,58 @@ bool ConstraintAssignor::assignSymExprToConst(const SymExpr *Sym,
   return true;
 }
 
+bool ConstraintAssignor::handleEquivalentAlternativeSymOperands(
+    const SymSymExpr *SymSym, RangeSet Constraint) {
+  SymbolRef LHS = SymSym->getLHS();
+  SymbolRef RHS = SymSym->getRHS();
+  EquivalenceClass LHSClass = EquivalenceClass::find(State, LHS);
+  EquivalenceClass RHSClass = EquivalenceClass::find(State, RHS);
+  SymbolSet SymbolsEqWithLHS = LHSClass.getClassMembers(State);
+  SymbolSet SymbolsEqWithRHS = RHSClass.getClassMembers(State);
+  llvm::SmallVector<SymSymExpr, 10> AlternativeSymSyms;
+
+  // Gather left alternatives.
+  for (SymbolRef AlternativeLHS : SymbolsEqWithLHS) {
+    if (AlternativeLHS == LHS)
+      continue;
+    AlternativeSymSyms.emplace_back(AlternativeLHS, SymSym->getOpcode(), RHS,
+                                    SymSym->getType());
+  }
+
+  // Gather right alternatives.
+  for (SymbolRef AlternativeRHS : SymbolsEqWithRHS) {
+    if (AlternativeRHS == RHS)
+      continue;
+    AlternativeSymSyms.emplace_back(LHS, SymSym->getOpcode(), AlternativeRHS,
+                                    SymSym->getType());
+  }
+
+  // Crosscheck the inferred ranges.
+  for (SymSymExpr AltSymSym : AlternativeSymSyms) {
+    RangeSet AltSymSymConstrant =
----------------
DonatNagyE wrote:

Nitpick: "constraint" is misspelled in this variable name.

https://github.com/llvm/llvm-project/pull/71284


More information about the cfe-commits mailing list