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

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.

Reviewers: NoQ, george.karpenkov, ddcc

Reviewed By: george.karpenkov

Subscribers: xazax.hun, szepet, a.sidorin

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

git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@335116 91177308-0d34-0410-b5e6-96231b3b80d8

diff --git a/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp b/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
index 0454825c6ce5246664391ee99dcbf1abc187f285..a47b7a2e705944ef62c29ca4e5236a4ea728d05b 100644 (file)
--- a/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
+++ b/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
@@ -994,6 +994,11 @@ private:
                       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.
   //===------------------------------------------------------------------===//
@@ -1052,35 +1057,7 @@ ProgramStateRef Z3ConstraintManager::assumeSym(ProgramStateRef State,
 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,
@@ -1264,31 +1241,14 @@ void Z3ConstraintManager::addRangeConstraints(ConstraintRangeTy 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 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);
+      Z3Expr SymRange =
+          getZ3RangeExpr(Sym, Range.From(), Range.To(), /*InRange=*/true);
+
+      // 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);
   }
@@ -1466,6 +1426,41 @@ Z3Expr Z3ConstraintManager::getZ3BinExpr(const Z3Expr &LHS, QualType LTy,
                                  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.
 //===------------------------------------------------------------------===//