[analyzer] Simplify values in binary operations more aggressively

[NoQ]

Summary

SValBuilder tries to constant-fold symbols in the left-hand side of the symbolic expression whenever it fails to evaluate the expression directly. However, it only constant-folds them when they are atomic expressions, not when they are complicated expressions themselves. This patch adds recursive constant-folding to the left-hand side expression (there's a lack of symmetry because we're trying to have symbols on the left and constants on the right). As an example, we'd now be able to handle operations similar to "$x + 1 < $y", when $x is constrained to a constant.

The constant-folding procedure, which i put into SValBuilder::simplifySVal(), is reusable, and i suspect that there are numerous places around SValBuilder, ConstraintManager, and our checkers, where it could be useful, but this patch tries to be relatively careful.

I'm still to see how it affects performance.

[xazax.hun]

This is a very welcome addition. I hope the performance will be still good :)

lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp

1023

We do not expect to see IntSymExpr? Maybe it is worth to document why.

1024

Maybe worth to have this as a member instead of query it every time?

1027

Why are these ops special?

1033

Maybe this can be hoisted?

[danielmarjamaki]

lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp

49

thier => their

[NoQ]

Thanks for the comments! Updated.

Performance didn't degrade in my test runs.

[xazax.hun]

LGTM! Thank you for working on this!

[xazax.hun]

One last question: maybe we want to skip this kind of simplification in case of Z3?
Probably the constraint managers could have a flag like "wantsSimplifiedConstraints"?
Maybe somehow the checkers that are doing their own simplification could respect this flag as well somehow?

[NoQ]

In D31886#724796, @xazax.hun wrote:

maybe we want to skip this kind of simplification in case of Z3?

Hmm, that depends on how would we want to use it eventually.

• If Z3 acts all alone and fires only over actual bug reports, then yeah, it turns this simplification procedure into a dry-run no-op. However, the much bigger performance problem would be the increased path explosion from not removing infeasible paths early on.
• If we try to filter out infeasible paths continuously, either by employing RangeConstraintManager as a filter, or by employing Z3 as a filter, then Z3 would anyway benefit from simpler symbolic expressions. In the worst case ("that's what Z3 would have done itself anyway), we'd, i guess, have little effect on quality *or* performance

Generally, i've a feeling that simplifying SVals is a safe thing to do.

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

public:
   /// location and non-location operands. For example, this would be used to
   /// evaluate a pointer arithmetic operation.
   virtual SVal evalBinOpLN(ProgramStateRef state, BinaryOperator::Opcode op,
                            Loc lhs, NonLoc rhs, QualType resultTy) = 0;
 
   /// Evaluates a given SVal. If the SVal has only one possible (integer) value,
   /// that value is returned. Otherwise, returns NULL.
   virtual const llvm::APSInt *getKnownValue(ProgramStateRef state, SVal val) = 0;
-  
+  /// Simplify symbolic expressions within a given SVal. Return an SVal
+  /// that represents the same value, but is hopefully easier to work with
+  /// than the original SVal.
+  virtual SVal simplifySVal(ProgramStateRef State, SVal Val) = 0;
+  
   /// Constructs a symbolic expression for two non-location values.
   SVal makeSymExprValNN(ProgramStateRef state, BinaryOperator::Opcode op,
                       NonLoc lhs, NonLoc rhs, QualType resultTy);
 
   SVal evalBinOp(ProgramStateRef state, BinaryOperator::Opcode op,
                  SVal lhs, SVal rhs, QualType type);
   
   DefinedOrUnknownSVal evalEQ(ProgramStateRef state, DefinedOrUnknownSVal lhs,

lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp

 // SimpleSValBuilder.cpp - A basic SValBuilder -----------------------*- C++ -*-
 //
 //                     The LLVM Compiler Infrastructure
 //
 // This file is distributed under the University of Illinois Open Source
 // License. See LICENSE.TXT for details.
 //
 //===----------------------------------------------------------------------===//
 //
 //  This file defines SimpleSValBuilder, a basic implementation of SValBuilder.
 //
 //===----------------------------------------------------------------------===//
 
 #include "clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/APSIntType.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/SValVisitor.h"
 
 using namespace clang;
 using namespace ento;
 
 namespace {
 class SimpleSValBuilder : public SValBuilder {
 protected:
   SVal dispatchCast(SVal val, QualType castTy) override;
SVal evalBinOpLL(ProgramStateRef state, BinaryOperator::Opcode op,
                    Loc lhs, Loc rhs, QualType resultTy) override;
   SVal evalBinOpLN(ProgramStateRef state, BinaryOperator::Opcode op,
                    Loc lhs, NonLoc rhs, QualType resultTy) override;
 
   /// getKnownValue - evaluates a given SVal. If the SVal has only one possible
   ///  (integer) value, that value is returned. Otherwise, returns NULL.
   const llvm::APSInt *getKnownValue(ProgramStateRef state, SVal V) override;
 
+  /// Recursively descends into symbolic expressions and replaces symbols
+  /// with thier known values (in the sense of the getKnownValue() method).
+  SVal simplifySVal(ProgramStateRef State, SVal V) override;
+
   SVal MakeSymIntVal(const SymExpr *LHS, BinaryOperator::Opcode op,
                      const llvm::APSInt &RHS, QualType resultTy);
 };
 } // end anonymous namespace
 
 SValBuilder *ento::createSimpleSValBuilder(llvm::BumpPtrAllocator &alloc,
                                            ASTContext &context,
                                            ProgramStateManager &stateMgr) {
case nonloc::SymbolValKind: {
           // Otherwise, make a SymIntExpr out of the expression.
           return MakeSymIntVal(symIntExpr, op, *RHSValue, resultTy);
         }
       }
 
       // Does the symbolic expression simplify to a constant?
       // If so, "fold" the constant by setting 'lhs' to a ConcreteInt
       // and try again.
-      ConstraintManager &CMgr = state->getConstraintManager();
-      if (const llvm::APSInt *Constant = CMgr.getSymVal(state, Sym)) {
-        lhs = nonloc::ConcreteInt(*Constant);
+      SVal simplifiedLhs = simplifySVal(state, lhs);
+      if (simplifiedLhs != lhs)
+        if (auto simplifiedLhsAsNonLoc = simplifiedLhs.getAs<NonLoc>()) {
+          lhs = *simplifiedLhsAsNonLoc;
           continue;
         }
 
       // Is the RHS a constant?
       if (const llvm::APSInt *RHSValue = getKnownValue(state, rhs))
         return MakeSymIntVal(Sym, op, *RHSValue, resultTy);
 
       // Give up -- this is not a symbolic expression we can handle.
       return makeSymExprValNN(state, op, InputLHS, InputRHS, resultTy);
     }
if (Optional<nonloc::ConcreteInt> X = V.getAs<nonloc::ConcreteInt>())
     return &X->getValue();
 
   if (SymbolRef Sym = V.getAsSymbol())
     return state->getConstraintManager().getSymVal(state, Sym);
 
   // FIXME: Add support for SymExprs.
   return nullptr;
 }
+
+SVal SimpleSValBuilder::simplifySVal(ProgramStateRef State, SVal V) {
+  // For now, this function tries to constant-fold symbols inside a
+  // nonloc::SymbolVal, and does nothing else. More simplifications should
+  // be possible, such as constant-folding an index in an ElementRegion.
+
+  class Simplifier : public FullSValVisitor<Simplifier, SVal> {
+    ProgramStateRef State;
+
+  public:
+    Simplifier(ProgramStateRef State) : State(State) {}
+
+    SVal VisitSymbolData(const SymbolData *S) {
+      SValBuilder &SVB = State->getStateManager().getSValBuilder();
+      if (const llvm::APSInt *I =
+              SVB.getKnownValue(State, nonloc::SymbolVal(S)))
+        return Loc::isLocType(S->getType()) ? (SVal)SVB.makeIntLocVal(*I)
+                                            : (SVal)SVB.makeIntVal(*I);
+      return nonloc::SymbolVal(S);
+    }
+
+    SVal VisitSymIntExpr(const SymIntExpr *S) {
+      SValBuilder &SVB = State->getStateManager().getSValBuilder();
+      SVal LHS, RHS;
+      if (Loc::isLocType(S->getLHS()->getType()) &&
+          BinaryOperator::isComparisonOp(S->getOpcode())) {
+        LHS = Visit(S->getLHS());
+        if (SymbolRef Sym = LHS.getAsSymbol())
+          LHS = SVB.makeLoc(Sym);
+        RHS = SVB.makeIntLocVal(S->getRHS());
+      } else {
+        LHS = Visit(S->getLHS());
+        RHS = SVB.makeIntVal(S->getRHS());
+      }
+      return SVB.evalBinOp(State, S->getOpcode(), LHS, RHS, S->getType());
+    }
+
+    SVal VisitSymSymExpr(const SymSymExpr *S) {
+      SValBuilder &SVB = State->getStateManager().getSValBuilder();
+      SVal LHS = Visit(S->getLHS());
+      SVal RHS = Visit(S->getRHS());
+      return SVB.evalBinOp(State, S->getOpcode(), LHS, RHS, S->getType());
+    }
+
+    SVal VisitSymExpr(SymbolRef S) { return nonloc::SymbolVal(S); }
+
+    SVal VisitMemRegion(const MemRegion *R) { return loc::MemRegionVal(R); }
+
+    SVal VisitNonLocSymbolVal(nonloc::SymbolVal V) {
+      // Simplification is much more costly than computing complexity.
+      // For high complexity, it may be not worth it.
+      if (V.getSymbol()->computeComplexity() > 100)
+        return V;
+      return Visit(V.getSymbol());
+    }
+
+    SVal VisitSVal(SVal V) { return V; }
+  };
+
+  return Simplifier(State).Visit(V);
+}

test/Analysis/additive-folding.cpp

 void multiplicativeSanityTest(int x) {
   // At one point we were ignoring the *4 completely -- the constraint manager
   // would see x < 8 and then declare the assertion to be known false.
   if (x*4 < 8)
     return;
 
   clang_analyzer_eval(x == 3); // expected-warning{{UNKNOWN}}
 }
+
+void additiveSymSymFolding(int x, int y) {
+  // We should simplify 'x - 1' to '0' and handle the comparison,
+  // despite both sides being complicated symbols.
+  int z = x - 1;
+  if (x == 1)
+    if (y >= 0)
+      clang_analyzer_eval(z <= y); // expected-warning{{TRUE}}
+}