r335116 - [analyzer] Optimize constraint generation when the range is a concrete value
Mikhail R. Gadelha via cfe-commits
cfe-commits at lists.llvm.org
Wed Jun 20 04:42:12 PDT 2018
Author: mramalho
Date: Wed Jun 20 04:42:12 2018
New Revision: 335116
URL: http://llvm.org/viewvc/llvm-project?rev=335116&view=rev
Log:
[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
Modified:
cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
Modified: cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp?rev=335116&r1=335115&r2=335116&view=diff
==============================================================================
--- cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp (original)
+++ cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp Wed Jun 20 04:42:12 2018
@@ -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::ass
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::addRangeConstr
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();
+ Z3Expr SymRange =
+ getZ3RangeExpr(Sym, Range.From(), Range.To(), /*InRange=*/true);
- 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);
+ // 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
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.
//===------------------------------------------------------------------===//
More information about the cfe-commits
mailing list