[Analyzer][solver] Fix crashes during symbol simplification

[martong]

Summary

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.

[vsavchenko]

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

2307–2308

I don't like the idea of duplicating it into every assume method. This way we drastically increase our chances to forget it (like you did with assumeSymGE and assumeSymLE).
I think the better place for it is in RangedConstraintManager::assumeSymRel and neighboring methods, though still not perfect.
I don't really get why we get not simplified symbol to begin with.

[martong]

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

2307–2308

assumeSymRel is not enough, because e.g. assumeSymGE is called also e.g. from assumeSymUnsupported. Perhaps we could change the signature of assumeSymEQ/NE/GT/GE/LT/LE to take an auxiliary Simplifier wrapper object instead of SymbolRef?

ProgramStateRef assumeSymNE(ProgramStateRef State, Simplifier S,
                                    const llvm::APSInt &V,
                                    const llvm::APSInt &Adjustment);

And for the Simplifier something like:

struct Simplifier {
  SymbolRef SimplifiedSym = nullptr;
  Simplifier(SymbolRef Sym) : SimplifiedSym(simplify(Sym)) {}
  
};

[martong]

I don't really get why we get not simplified symbol to begin with.

This is because of the Environment bindings. I.e. b1 is bound to $a0 - $b0 + $c when we evaluate int b1 = (unsigned)a1 + c;. This binding is not changed/updated, so when we evaluate the division then we query the DeclRefExpr for b1 from the Environment and that gives still $a0 - $b0 + $c. We either do the simplification in the ConstraintManager (as we do now with this and the parent patch) or perhaps we could try to simplify the Environment bindings as an alternative solution.

[vsavchenko]

In D104844#2838674, @martong wrote:

I don't really get why we get not simplified symbol to begin with.

This is because of the Environment bindings. I.e. b1 is bound to $a0 - $b0 + $c when we evaluate int b1 = (unsigned)a1 + c;. This binding is not changed/updated, so when we evaluate the division then we query the DeclRefExpr for b1 from the Environment and that gives still $a0 - $b0 + $c. We either do the simplification in the ConstraintManager (as we do now with this and the parent patch) or perhaps we could try to simplify the Environment bindings as an alternative solution.

Yeah, I remember now, thanks!

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

2307–2308

assumeSymRel is not enough, because e.g. assumeSymGE is called also e.g. from assumeSymUnsupported.

Yep, that's why I suggested assumeSymRel and its neighbors. I actually think that three top-level public methods from RangedConstraintManager will do: assumeSym, assumeSymInclusiveRange, and assumeSymUnsupported.

We can't really change the signatures of those methods because we'll be introducing this functionality into solvers that didn't sign up for this (and don't need it).

Also we can least put this if statement inside of simplify, so we can use it like this: Sym = simplify(St, Sym);.

[martong]

• Use simplify from RangedConstraintManager

[martong]

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

2307–2308

Okay, I've updated like so.

[vsavchenko]

Awesome, thanks for swiftly addressing it!

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

1981

Oof, and there is no way to avoid all these namespaces?

[martong]

Valeriy, thanks for the assiduous and quick review!

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

1981

Unfortunately, the candidate function would be the member simplify in that case. Though, we can get rid of the ::clang prefix.

[vsavchenko]

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

1981

OK, at least ento::!

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

protected:
 
   //===------------------------------------------------------------------===//
   // Internal implementation.
   //===------------------------------------------------------------------===//
 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
 
 REGISTER_FACTORY_WITH_PROGRAMSTATE(ConstraintMap)
 
 #endif

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

RangeSet SymbolicRangeInferrer::VisitBinaryOperator<BO_Rem>(Range LHS,
   // for any sign of either LHS, or RHS.
   return {RangeFactory, ValueFactory.getValue(Min), ValueFactory.getValue(Max)};
 }
 
 //===----------------------------------------------------------------------===//
 //                  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)
       : RangedConstraintManager(EE, SVB), F(getBasicVals()) {}
 
   //===------------------------------------------------------------------===//
   // Implementation for interface from ConstraintManager.
   //===------------------------------------------------------------------===//
private:
   template <bool EQ>
   ProgramStateRef track(RangeSet NewConstraint, ProgramStateRef State,
                         SymbolRef Sym, const llvm::APSInt &Int,
                         const llvm::APSInt &Adjustment) {
     if (NewConstraint.isEmpty())
       // 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,
         // we should invert IsEquality flag.
         Equality->IsEquality = Equality->IsEquality != EQ;
         return track(NewState, *Equality);
       }
 

 // simplified then we check if we can merge the simplified symbol's equivalence
 // class to this class. This way, we simplify not just the symbols but the
 // classes as well: we strive to keep the number of the classes to be the
 // absolute minimum.
 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 = ::clang::ento::simplify(State, MemberSym);
     if (SimplifiedMemberSym && MemberSym != SimplifiedMemberSym) {
       EquivalenceClass ClassOfSimplifiedSym =
           EquivalenceClass::find(State, SimplifiedMemberSym);
       // The simplified symbol should be the member of the original Class,
       // however, it might be in another existing class at the moment. We
       // have to merge these classes.
       State = merge(SVB.getBasicValueFactory(), F, State, ClassOfSimplifiedSym);
       if (!State)
RangeConstraintManager::assumeSymNE(ProgramStateRef St, SymbolRef Sym,
                                     const llvm::APSInt &Int,
                                     const llvm::APSInt &Adjustment) {
   // Before we do any real work, see if the value can even show up.
   APSIntType AdjustmentType(Adjustment);
   if (AdjustmentType.testInRange(Int, true) != APSIntType::RTR_Within)
     return St;
 
   llvm::APSInt Point = AdjustmentType.convert(Int) - Adjustment;
-
   RangeSet New = getRange(St, Sym);
   New = F.deletePoint(New, Point);
 
   return trackNE(New, St, Sym, Int, Adjustment);
 }
 
 ProgramStateRef
 RangeConstraintManager::assumeSymEQ(ProgramStateRef St, SymbolRef Sym,
                                     const llvm::APSInt &Int,
                                     const llvm::APSInt &Adjustment) {

clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp

 
 namespace ento {
 
 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)) {
+  if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(Sym)) {
     // We can only simplify expressions whose RHS is an integer.
 
     BinaryOperator::Opcode op = SIE->getOpcode();
     if (BinaryOperator::isComparisonOp(op) && op != BO_Cmp) {
       if (!Assumption)
         op = BinaryOperator::negateComparisonOp(op);
 
       return assumeSymRel(State, SIE->getLHS(), op, SIE->getRHS());
ProgramStateRef RangedConstraintManager::assumeSym(ProgramStateRef State,
   // If we get here, there's nothing else we can do but treat the symbol as
   // opaque.
   return assumeSymUnsupported(State, Sym, Assumption);
 }
 
 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());
 
   llvm::APSInt Adjustment = WraparoundType.getZeroValue();
   SymbolRef AdjustedSym = Sym;
   computeAdjustment(AdjustedSym, Adjustment);
 
return assumeSymWithinInclusiveRange(State, AdjustedSym, ConvertedFrom,
                                          ConvertedTo, Adjustment);
   return assumeSymOutsideInclusiveRange(State, AdjustedSym, ConvertedFrom,
                                         ConvertedTo, Adjustment);
 }
 
 ProgramStateRef
 RangedConstraintManager::assumeSymUnsupported(ProgramStateRef State,
                                               SymbolRef Sym, bool Assumption) {
+  Sym = simplify(State, Sym);
+
   BasicValueFactory &BVF = getBasicVals();
   QualType T = Sym->getType();
 
   // Non-integer types are not supported.
   if (!T->isIntegralOrEnumerationType())
     return State;
 
   // Reverse the operation and add directly to state.
if (Op == BO_Add || Op == BO_Sub) {
       // This should happen /after/ promotion, in case the value being
       // subtracted is, say, CHAR_MIN, and the promoted type is 'int'.
       if (Op == BO_Sub)
         Adjustment = -Adjustment;
     }
   }
 }
 
+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

+// 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

+// 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}}
+    }
+}