[analyzer] Optimize constraint generation when the range is a concrete value

[mikhail.ramalho]

Summary

If a constraint is something like:

$0 = [1,1]

it'll now be created as:

assert($0 == 1)

instead of:

assert($0 >= 1 && $0 <= 1)

In general, ~3% speedup when solving per query in my machine. Biggest improvement was when verifying sqlite3, total time went down from 3000s to 2200s.

I couldn't create a test for this as there is no way to dump the formula yet. D48221 adds a method to dump the formula but there is no way to do it from the command line.

Also, a test that prints the formula will most likely fail in the future, as different solvers print the formula in different formats.

[george.karpenkov]

The change is fine, but I would note that to get more readable formulas it might be better to construct an array first, and then do disjunction over the whole array.
Also helper methods for mkEqual, mkLessEq and mkGreaterEq could be helpful.

[ddcc]

Correct me if I'm wrong, but isn't this function mostly duplicate with assumeSymInclusiveRange? I think it would be preferable to refactor out the constraint generation from both into e.g. getZ3RangeExpr, then modify both addRangeConstraints and assumeSymInclusiveRange to call it instead?

[george.karpenkov]

@ddcc sounds reasonable, yes.

[mikhail.ramalho]

Refactor duplicated code from assumeSymInclusiveRange and addRangeConstraints to a new method getZ3RangeExpr.

[mikhail.ramalho]

I Forgot to add a couple of /*RetTy=*/nullptr in the previous patch.

[ddcc]

LGTM

[mikhail.ramalho]

Fix constraint being dropped in addRangeConstraints because of a missing BO_LOr operation.

[mikhail.ramalho]

In D48227#1133940, @george.karpenkov wrote:

The change is fine, but I would note that to get more readable formulas it might be better to construct an array first, and then do disjunction over the whole array.
Also helper methods for mkEqual, mkLessEq and mkGreaterEq could be helpful.

That would be great to implement in the SMT generic API but we would need to first need to create generic AST and sort wrappers (like Z3Sort and Z3Expr), then we could have something like:

/// Bitvector operations
SMTExpr mkBVAdd(SMTExpr a, SMTExpr b);
SMTExpr mkBVSub(SMTExpr a, SMTExpr b);
SMTExpr mkBVMul(SMTExpr a, SMTExpr b);
SMTExpr mkBVSMod(SMTExpr a, SMTExpr b);
SMTExpr mkBVUMod(SMTExpr a, SMTExpr b);
SMTExpr mkBVSDiv(SMTExpr a, SMTExpr b);
SMTExpr mkBVUDiv(SMTExpr a, SMTExpr b);
SMTExpr mkBVShl(SMTExpr a, SMTExpr b);
SMTExpr mkBVAshr(SMTExpr a, SMTExpr b);
SMTExpr mkBVLshr(SMTExpr a, SMTExpr b);
SMTExpr mkBVNeg(SMTExpr a);
SMTExpr mkBVNot(SMTExpr a);
SMTExpr mkBVNxor(SMTExpr a, SMTExpr b);
SMTExpr mkBVNor(SMTExpr a, SMTExpr b);
SMTExpr mkBVNand(SMTExpr a, SMTExpr b);
SMTExpr mkBVXor(SMTExpr a, SMTExpr b);
SMTExpr mkBVOr(SMTExpr a, SMTExpr b);
SMTExpr mkBVAnd(SMTExpr a, SMTExpr b);
SMTExpr mkImplies(SMTExpr a, SMTExpr b);
SMTExpr mkBVUlt(SMTExpr a, SMTExpr b);
SMTExpr mkBVSlt(SMTExpr a, SMTExpr b);
SMTExpr mkBVUgt(SMTExpr a, SMTExpr b);
SMTExpr mkBVSgt(SMTExpr a, SMTExpr b);
SMTExpr mkBVUle(SMTExpr a, SMTExpr b);
SMTExpr mkBVSle(SMTExpr a, SMTExpr b);
SMTExpr mkBVUge(SMTExpr a, SMTExpr b);
SMTExpr mkBVSge(SMTExpr a, SMTExpr b);
SMTExpr mkXor(SMTExpr a, SMTExpr b);
SMTExpr mkNot(SMTExpr a);
SMTExpr mkEqual(SMTExpr a, SMTExpr b);
SMTExpr mkNotEqual(SMTExpr a, SMTExpr b);

/// Arrays operations
SMTExpr mkStore(SMTExpr a, SMTExpr b, SMTExpr c);
SMTExpr mkSelect(SMTExpr a, SMTExpr b);

/// Sorts
SMTSort getBoolSort();
SMTSort getBVsort(std::size_t width);
SMTSort getArraySort(SMTSort domain, SMTSort range);
SMTSort getFloatSort(const unsigned ew, const unsigned sw);
SMTSort getFloatRoundingMode();

/// Special Floating-points
SMTExpr mkFPNan(std::size_t ew, std::size_t sw);
SMTExpr mkFPInf(bool sgn, std::size_t ew, std::size_t sw);
SMTExpr mkFPRm(std::size_t rm);

/// Floating-points operations
SMTExpr mkFPFma(SMTExpr a, SMTExpr b, SMTExpr c, SMTExpr rm);
SMTExpr mkCastFPToUbv(SMTExpr from, std::size_t width);
SMTExpr mkCastFPToSbv(SMTExpr from, std::size_t width);
SMTExpr mkCastFPToFP(SMTExpr from, SMTSort to, SMTExpr rm);
SMTExpr mkCastUbvToFP(SMTExpr from, SMTSort to, SMTExpr rm);
SMTExpr mkCastSbvToFP(SMTExpr from, SMTSort to, SMTExpr rm);
SMTExpr mkFPAdd(SMTExpr lhs, SMTExpr rhs, SMTExpr rm);
SMTExpr mkFPSub(SMTExpr lhs, SMTExpr rhs, SMTExpr rm);
SMTExpr mkFPMul(SMTExpr lhs, SMTExpr rhs, SMTExpr rm);
SMTExpr mkFPDiv(SMTExpr lhs, SMTExpr rhs, SMTExpr rm);
SMTExpr mkFPNearbyint(SMTExpr from, SMTExpr rm);
SMTExpr mkFPSqrt(SMTExpr rd, SMTExpr rm);
SMTExpr mkFPEqual(SMTExpr lhs, SMTExpr rhs);
SMTExpr mkFPGt(SMTExpr lhs, SMTExpr rhs);
SMTExpr mkFPLt(SMTExpr lhs, SMTExpr rhs);
SMTExpr mkFPGte(SMTExpr lhs, SMTExpr rhs);
SMTExpr mkFPlte(SMTExpr lhs, SMTExpr rhs);
SMTExpr mkFPIsNan(SMTExpr op);
SMTExpr mkFPIsInf(SMTExpr op);
SMTExpr mkFPIsNormal(SMTExpr op);
SMTExpr mkFPUsZero(SMTExpr op);
SMTExpr mkFPIsNegative(SMTExpr op);
SMTExpr mkFPIsPositive(SMTExpr op);
SMTExpr mkFPAbs(SMTExpr op);
SMTExpr mkFPNeg(SMTExpr op);

Unless you're talking about implementing the helpers only in the Z3 specific class, then I'd argue that it'd a waste of time now, as the 3rd deliverable of my proposal is to write the generic SMT API and the Z3 specific implementation anyway.

cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp

Z3Expr getZ3SymBinExpr(const BinarySymExpr *BSE, bool *hasComparison,
                          QualType *RetTy) const;
 
   // Wrapper to generate Z3Expr from unpacked binary symbolic expression.
   // Sets the RetTy parameter. See getZ3Expr().
   Z3Expr getZ3BinExpr(const Z3Expr &LHS, QualType LTy,
                       BinaryOperator::Opcode Op, const Z3Expr &RHS,
                       QualType RTy, QualType *RetTy) const;
 
+  // Wrapper to generate Z3Expr from a range. If From == To, an equality will
+  // be created instead.
+  Z3Expr getZ3RangeExpr(SymbolRef Sym, const llvm::APSInt &From,
+                        const llvm::APSInt &To, bool InRange);
+
   //===------------------------------------------------------------------===//
   // Helper functions.
   //===------------------------------------------------------------------===//
 
   // Recover the QualType of an APSInt.
   // TODO: Refactor to put elsewhere
   QualType getAPSIntType(const llvm::APSInt &Int) const;
 
if (!hasComparison && !RetTy->isBooleanType())
     return assumeZ3Expr(State, Sym, getZ3ZeroExpr(Exp, RetTy, !Assumption));
 
   return assumeZ3Expr(State, Sym, Assumption ? Exp : getZ3NotExpr(Exp));
 }
 
 ProgramStateRef Z3ConstraintManager::assumeSymInclusiveRange(
     ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
     const llvm::APSInt &To, bool InRange) {
-  QualType RetTy;
-  // The expression may be casted, so we cannot call getZ3DataExpr() directly
-  Z3Expr Exp = getZ3Expr(Sym, &RetTy);
-
-  QualType FromTy;
-  llvm::APSInt NewFromInt;
-  std::tie(NewFromInt, FromTy) = fixAPSInt(From);
-  Z3Expr FromExp = Z3Expr::fromAPSInt(NewFromInt);
-
-  // Construct single (in)equality
-  if (From == To)
-    return assumeZ3Expr(State, Sym,
-                        getZ3BinExpr(Exp, RetTy, InRange ? BO_EQ : BO_NE,
-                                     FromExp, FromTy, nullptr));
-
-  QualType ToTy;
-  llvm::APSInt NewToInt;
-  std::tie(NewToInt, ToTy) = fixAPSInt(To);
-  Z3Expr ToExp = Z3Expr::fromAPSInt(NewToInt);
-  assert(FromTy == ToTy && "Range values have different types!");
-  // Construct two (in)equalities, and a logical and/or
-  Z3Expr LHS = getZ3BinExpr(Exp, RetTy, InRange ? BO_GE : BO_LT, FromExp,
-                            FromTy, nullptr);
-  Z3Expr RHS =
-      getZ3BinExpr(Exp, RetTy, InRange ? BO_LE : BO_GT, ToExp, ToTy, nullptr);
-  return assumeZ3Expr(
-      State, Sym,
-      Z3Expr::fromBinOp(LHS, InRange ? BO_LAnd : BO_LOr, RHS,
-                        RetTy->isSignedIntegerOrEnumerationType()));
+  return assumeZ3Expr(State, Sym, getZ3RangeExpr(Sym, From, To, InRange));
 }
 
 ProgramStateRef Z3ConstraintManager::assumeSymUnsupported(ProgramStateRef State,
                                                           SymbolRef Sym,
                                                           bool Assumption) {
   // Skip anything that is unsupported
   return State;
 }
Z3ConstraintManager::removeDeadBindings(ProgramStateRef State,
   return State->set<ConstraintZ3>(CZ);
 }
 
 void Z3ConstraintManager::addRangeConstraints(ConstraintRangeTy CR) {
   for (const auto &I : CR) {
     SymbolRef Sym = I.first;
 
     Z3Expr Constraints = Z3Expr::fromBoolean(false);
-
     for (const auto &Range : I.second) {
-      const llvm::APSInt &From = Range.From();
-      const llvm::APSInt &To = Range.To();
-
-      QualType FromTy;
-      llvm::APSInt NewFromInt;
-      std::tie(NewFromInt, FromTy) = fixAPSInt(From);
-      Z3Expr FromExp = Z3Expr::fromAPSInt(NewFromInt);
-      QualType SymTy;
-      Z3Expr Exp = getZ3Expr(Sym, &SymTy);
-      bool IsSignedTy = SymTy->isSignedIntegerOrEnumerationType();
-      QualType ToTy;
-      llvm::APSInt NewToInt;
-      std::tie(NewToInt, ToTy) = fixAPSInt(To);
-      Z3Expr ToExp = Z3Expr::fromAPSInt(NewToInt);
-      assert(FromTy == ToTy && "Range values have different types!");
+      Z3Expr SymRange =
+          getZ3RangeExpr(Sym, Range.From(), Range.To(), /*InRange=*/true);
 
-      Z3Expr LHS =
-          getZ3BinExpr(Exp, SymTy, BO_GE, FromExp, FromTy, /*RetTy=*/nullptr);
-      Z3Expr RHS =
-          getZ3BinExpr(Exp, SymTy, BO_LE, ToExp, FromTy, /*RetTy=*/nullptr);
-      Z3Expr SymRange = Z3Expr::fromBinOp(LHS, BO_LAnd, RHS, IsSignedTy);
+      // FIXME: the last argument (isSigned) is not used when generating the
+      // or expression, as both arguments are booleans
       Constraints =
-          Z3Expr::fromBinOp(Constraints, BO_LOr, SymRange, IsSignedTy);
+          Z3Expr::fromBinOp(Constraints, BO_LOr, SymRange, /*IsSigned=*/true);
     }
     Solver.addConstraint(Constraints);
   }
 }
 
 clang::ento::ConditionTruthVal Z3ConstraintManager::isModelFeasible() {
   if (Solver.check() == Z3_L_FALSE)
     return false;
Z3Expr Z3ConstraintManager::getZ3BinExpr(const Z3Expr &LHS, QualType LTy,
   }
 
   return LTy->isRealFloatingType()
              ? Z3Expr::fromFloatBinOp(NewLHS, Op, NewRHS)
              : Z3Expr::fromBinOp(NewLHS, Op, NewRHS,
                                  LTy->isSignedIntegerOrEnumerationType());
 }
 
+Z3Expr Z3ConstraintManager::getZ3RangeExpr(SymbolRef Sym,
+                                           const llvm::APSInt &From,
+                                           const llvm::APSInt &To,
+                                           bool InRange) {
+  // Convert lower bound
+  QualType FromTy;
+  llvm::APSInt NewFromInt;
+  std::tie(NewFromInt, FromTy) = fixAPSInt(From);
+  Z3Expr FromExp = Z3Expr::fromAPSInt(NewFromInt);
+
+  // Convert symbol
+  QualType SymTy;
+  Z3Expr Exp = getZ3Expr(Sym, &SymTy);
+
+  // Construct single (in)equality
+  if (From == To)
+    return getZ3BinExpr(Exp, SymTy, InRange ? BO_EQ : BO_NE, FromExp, FromTy,
+                        /*RetTy=*/nullptr);
+
+  QualType ToTy;
+  llvm::APSInt NewToInt;
+  std::tie(NewToInt, ToTy) = fixAPSInt(To);
+  Z3Expr ToExp = Z3Expr::fromAPSInt(NewToInt);
+  assert(FromTy == ToTy && "Range values have different types!");
+
+  // Construct two (in)equalities, and a logical and/or
+  Z3Expr LHS = getZ3BinExpr(Exp, SymTy, InRange ? BO_GE : BO_LT, FromExp,
+                            FromTy, /*RetTy=*/nullptr);
+  Z3Expr RHS = getZ3BinExpr(Exp, SymTy, InRange ? BO_LE : BO_GT, ToExp, ToTy,
+                            /*RetTy=*/nullptr);
+
+  return Z3Expr::fromBinOp(LHS, InRange ? BO_LAnd : BO_LOr, RHS,
+                           SymTy->isSignedIntegerOrEnumerationType());
+}
+
 //===------------------------------------------------------------------===//
 // Helper functions.
 //===------------------------------------------------------------------===//
 
 QualType Z3ConstraintManager::getAPSIntType(const llvm::APSInt &Int) const {
   ASTContext &Ctx = getBasicVals().getContext();
   return Ctx.getIntTypeForBitwidth(Int.getBitWidth(), Int.isSigned());
 }