[Analyzer][solver] Fix crashes during symbol simplification

Consider the code
```
  void f(int a0, int b0, int c)
  {
      int a1 = a0 - b0;
      int b1 = (unsigned)a1 + c;
      if (c == 0) {
          int d = 7L / b1;
      }
  }
```
At the point of divisiion by `b1` that is considered to be non-zero,
which results in a new constraint for `$a0 - $b0 + $c`. The type
of this sym is unsigned, however, the simplified sym is `$a0 -
$b0` and its type is signed. This is probably the result of the
inherent improper handling of casts. Anyway, Range assignment
for constraints use this type information. Therefore, we must
make sure that first we simplify the symbol and only then we
assign the range.

Differential Revision: https://reviews.llvm.org/D104844

clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h

@@ -384,6 +384,11 @@ private:
   static void computeAdjustment(SymbolRef &Sym, llvm::APSInt &Adjustment);
 };
 
+/// Try to simplify a given symbolic expression's associated value based on the
+/// constraints in State. This is needed because the Environment bindings are
+/// not getting updated when a new constraint is added to the State.
+SymbolRef simplify(ProgramStateRef State, SymbolRef Sym);
+
 } // namespace ento
 } // namespace clang
 

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

@@ -1384,12 +1384,6 @@ RangeSet SymbolicRangeInferrer::VisitBinaryOperator<BO_Rem>(Range LHS,
 //                  Constraint manager implementation details
 //===----------------------------------------------------------------------===//
 
-static SymbolRef simplify(ProgramStateRef State, SymbolRef Sym) {
-  SValBuilder &SVB = State->getStateManager().getSValBuilder();
-  SVal SimplifiedVal = SVB.simplifySVal(State, SVB.makeSymbolVal(Sym));
-  return SimplifiedVal.getAsSymbol();
-}
-
 class RangeConstraintManager : public RangedConstraintManager {
 public:
   RangeConstraintManager(ExprEngine *EE, SValBuilder &SVB)
@@ -1503,9 +1497,6 @@ private:
       // This is an infeasible assumption.
       return nullptr;
 
-    if (SymbolRef SimplifiedSym = simplify(State, Sym))
-      Sym = SimplifiedSym;
-
     if (ProgramStateRef NewState = setConstraint(State, Sym, NewConstraint)) {
       if (auto Equality = EqualityInfo::extract(Sym, Int, Adjustment)) {
         // If the original assumption is not Sym + Adjustment !=/</> Int,
@@ -1962,7 +1953,7 @@ LLVM_NODISCARD ProgramStateRef EquivalenceClass::simplify(
     SValBuilder &SVB, RangeSet::Factory &F, ProgramStateRef State) {
   SymbolSet ClassMembers = getClassMembers(State);
   for (const SymbolRef &MemberSym : ClassMembers) {
-    SymbolRef SimplifiedMemberSym = ::simplify(State, MemberSym);
+    SymbolRef SimplifiedMemberSym = ento::simplify(State, MemberSym);
     if (SimplifiedMemberSym && MemberSym != SimplifiedMemberSym) {
       EquivalenceClass ClassOfSimplifiedSym =
           EquivalenceClass::find(State, SimplifiedMemberSym);
@@ -2288,7 +2279,6 @@ RangeConstraintManager::assumeSymNE(ProgramStateRef St, SymbolRef Sym,
     return St;
 
   llvm::APSInt Point = AdjustmentType.convert(Int) - Adjustment;
-
   RangeSet New = getRange(St, Sym);
   New = F.deletePoint(New, Point);
 

clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp

@@ -23,12 +23,14 @@ RangedConstraintManager::~RangedConstraintManager() {}
 ProgramStateRef RangedConstraintManager::assumeSym(ProgramStateRef State,
                                                    SymbolRef Sym,
                                                    bool Assumption) {
+  Sym = simplify(State, Sym);
+
   // Handle SymbolData.
-  if (isa<SymbolData>(Sym)) {
+  if (isa<SymbolData>(Sym))
     return assumeSymUnsupported(State, Sym, Assumption);
 
-    // Handle symbolic expression.
-  } else if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(Sym)) {
+  // Handle symbolic expression.
+  if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(Sym)) {
     // We can only simplify expressions whose RHS is an integer.
 
     BinaryOperator::Opcode op = SIE->getOpcode();
@@ -93,6 +95,9 @@ ProgramStateRef RangedConstraintManager::assumeSym(ProgramStateRef State,
 ProgramStateRef RangedConstraintManager::assumeSymInclusiveRange(
     ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
     const llvm::APSInt &To, bool InRange) {
+
+  Sym = simplify(State, Sym);
+
   // Get the type used for calculating wraparound.
   BasicValueFactory &BVF = getBasicVals();
   APSIntType WraparoundType = BVF.getAPSIntType(Sym->getType());
@@ -121,6 +126,8 @@ ProgramStateRef RangedConstraintManager::assumeSymInclusiveRange(
 ProgramStateRef
 RangedConstraintManager::assumeSymUnsupported(ProgramStateRef State,
                                               SymbolRef Sym, bool Assumption) {
+  Sym = simplify(State, Sym);
+
   BasicValueFactory &BVF = getBasicVals();
   QualType T = Sym->getType();
 
@@ -219,5 +226,13 @@ void RangedConstraintManager::computeAdjustment(SymbolRef &Sym,
   }
 }
 
+SymbolRef simplify(ProgramStateRef State, SymbolRef Sym) {
+  SValBuilder &SVB = State->getStateManager().getSValBuilder();
+  SVal SimplifiedVal = SVB.simplifySVal(State, SVB.makeSymbolVal(Sym));
+  if (SymbolRef SimplifiedSym = SimplifiedVal.getAsSymbol())
+    return SimplifiedSym;
+  return Sym;
+}
+
 } // end of namespace ento
 } // end of namespace clang

clang/test/Analysis/solver-sym-simplification-no-crash.c

@@ -0,0 +1,26 @@
+// RUN: %clang_analyze_cc1 %s \
+// RUN:   -analyzer-checker=core \
+// RUN:   -analyzer-checker=debug.ExprInspection \
+// RUN:   -verify
+
+// Here, we test that symbol simplification in the solver does not produce any
+// crashes.
+
+// expected-no-diagnostics
+
+static int a, b;
+static long c;
+
+static void f(int i, int j)
+{
+    (void)(j <= 0 && i ? i : j);
+}
+
+static void g(void)
+{
+    int d = a - b | (c < 0);
+    for (;;)
+    {
+        f(d ^ c, c);
+    }
+}

clang/test/Analysis/solver-sym-simplification-with-proper-range-type.c

@@ -0,0 +1,29 @@
+// RUN: %clang_analyze_cc1 %s \
+// RUN:   -analyzer-checker=core \
+// RUN:   -analyzer-checker=debug.ExprInspection \
+// RUN:   -verify
+
+// Here we test that the range based solver equivalency tracking mechanism
+// assigns a properly typed range to the simplified symbol.
+
+void clang_analyzer_printState();
+void clang_analyzer_eval(int);
+
+void f(int a0, int b0, int c)
+{
+    int a1 = a0 - b0;
+    int b1 = (unsigned)a1 + c;
+    if (c == 0) {
+
+        int d = 7L / b1; // ...
+        // At this point b1 is considered non-zero, which results in a new
+        // constraint for $a0 - $b0 + $c. The type of this sym is unsigned,
+        // however, the simplified sym is $a0 - $b0 and its type is signed.
+        // This is probably the result of the inherent improper handling of
+        // casts. Anyway, Range assignment for constraints use this type
+        // information. Therefore, we must make sure that first we simplify the
+        // symbol and only then we assign the range.
+
+        clang_analyzer_eval(a0 - b0 != 0); // expected-warning{{TRUE}}
+    }
+}