r343581 - [analyzer] Improvements to the SMT API
Mikhail R. Gadelha via cfe-commits
cfe-commits at lists.llvm.org
Tue Oct 2 05:55:48 PDT 2018
Author: mramalho
Date: Tue Oct 2 05:55:48 2018
New Revision: 343581
URL: http://llvm.org/viewvc/llvm-project?rev=343581&view=rev
Log:
[analyzer] Improvements to the SMT API
Summary:
Several improvements in preparation for the new backends.
Refactoring:
- Removed duplicated methods `fromBoolean`, `fromAPSInt`, `fromInt` and `fromAPFloat`. The methods `mkBoolean`, `mkBitvector` and `mkFloat` are now used instead.
- The names of the functions that convert BVs to FPs were swapped (`mkSBVtoFP`, `mkUBVtoFP`, `mkFPtoSBV`, `mkFPtoUBV`).
- Added a couple of comments in function calls.
Crosscheck encoding:
- Changed how constraints are encoded in the refutation manager so it doesn't start with (false OR ...). This change introduces one duplicated line (see file `BugReporterVisitors.cpp`, the `SMTConv::getRangeExpr is called twice, so I can remove this change if the duplication is a problem.
Reviewers: george.karpenkov, NoQ
Reviewed By: george.karpenkov
Subscribers: xazax.hun, szepet, a.sidorin, Szelethus
Differential Revision: https://reviews.llvm.org/D52365
Modified:
cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h
cfe/trunk/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h?rev=343581&r1=343580&r2=343581&view=diff
==============================================================================
--- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h (original)
+++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h Tue Oct 2 05:55:48 2018
@@ -134,9 +134,9 @@ public:
// A value has been obtained, check if it is the only value
SMTExprRef NotExp = SMTConv::fromBinOp(
Solver, Exp, BO_NE,
- Ty->isBooleanType() ? Solver->fromBoolean(Value.getBoolValue())
- : Solver->fromAPSInt(Value),
- false);
+ Ty->isBooleanType() ? Solver->mkBoolean(Value.getBoolValue())
+ : Solver->mkBitvector(Value, Value.getBitWidth()),
+ /*isSigned=*/false);
Solver->addConstraint(NotExp);
Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h?rev=343581&r1=343580&r2=343581&view=diff
==============================================================================
--- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h (original)
+++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h Tue Oct 2 05:55:48 2018
@@ -246,7 +246,7 @@ public:
// Logical operators
case BO_LAnd:
case BO_LOr:
- return fromBinOp(Solver, LHS, Op, RHS, false);
+ return fromBinOp(Solver, LHS, Op, RHS, /*isSigned=*/false);
default:;
}
@@ -294,14 +294,14 @@ public:
if (FromTy->isIntegralOrEnumerationType() && ToTy->isRealFloatingType()) {
SMTSortRef Sort = Solver->getFloatSort(ToBitWidth);
return FromTy->isSignedIntegerOrEnumerationType()
- ? Solver->mkFPtoSBV(Exp, Sort)
- : Solver->mkFPtoUBV(Exp, Sort);
+ ? Solver->mkSBVtoFP(Exp, Sort)
+ : Solver->mkUBVtoFP(Exp, Sort);
}
if (FromTy->isRealFloatingType() && ToTy->isIntegralOrEnumerationType())
return ToTy->isSignedIntegerOrEnumerationType()
- ? Solver->mkSBVtoFP(Exp, ToBitWidth)
- : Solver->mkUBVtoFP(Exp, ToBitWidth);
+ ? Solver->mkFPtoSBV(Exp, ToBitWidth)
+ : Solver->mkFPtoUBV(Exp, ToBitWidth);
llvm_unreachable("Unsupported explicit type cast!");
}
@@ -379,14 +379,14 @@ public:
getSymExpr(Solver, Ctx, SIE->getLHS(), <y, hasComparison);
llvm::APSInt NewRInt;
std::tie(NewRInt, RTy) = fixAPSInt(Ctx, SIE->getRHS());
- SMTExprRef RHS = Solver->fromAPSInt(NewRInt);
+ SMTExprRef RHS = Solver->mkBitvector(NewRInt, NewRInt.getBitWidth());
return getBinExpr(Solver, Ctx, LHS, LTy, Op, RHS, RTy, RetTy);
}
if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE)) {
llvm::APSInt NewLInt;
std::tie(NewLInt, LTy) = fixAPSInt(Ctx, ISE->getLHS());
- SMTExprRef LHS = Solver->fromAPSInt(NewLInt);
+ SMTExprRef LHS = Solver->mkBitvector(NewLInt, NewLInt.getBitWidth());
SMTExprRef RHS =
getSymExpr(Solver, Ctx, ISE->getRHS(), &RTy, hasComparison);
return getBinExpr(Solver, Ctx, LHS, LTy, Op, RHS, RTy, RetTy);
@@ -466,7 +466,7 @@ public:
llvm::APFloat Zero =
llvm::APFloat::getZero(Ctx.getFloatTypeSemantics(Ty));
return fromFloatBinOp(Solver, Exp, Assumption ? BO_EQ : BO_NE,
- Solver->fromAPFloat(Zero));
+ Solver->mkFloat(Zero));
}
if (Ty->isIntegralOrEnumerationType() || Ty->isAnyPointerType() ||
@@ -477,8 +477,10 @@ public:
if (Ty->isBooleanType())
return Assumption ? fromUnOp(Solver, UO_LNot, Exp) : Exp;
- return fromBinOp(Solver, Exp, Assumption ? BO_EQ : BO_NE,
- Solver->fromInt("0", Ctx.getTypeSize(Ty)), isSigned);
+ return fromBinOp(
+ Solver, Exp, Assumption ? BO_EQ : BO_NE,
+ Solver->mkBitvector(llvm::APSInt("0"), Ctx.getTypeSize(Ty)),
+ isSigned);
}
llvm_unreachable("Unsupported type for zero value!");
@@ -493,7 +495,8 @@ public:
QualType FromTy;
llvm::APSInt NewFromInt;
std::tie(NewFromInt, FromTy) = fixAPSInt(Ctx, From);
- SMTExprRef FromExp = Solver->fromAPSInt(NewFromInt);
+ SMTExprRef FromExp =
+ Solver->mkBitvector(NewFromInt, NewFromInt.getBitWidth());
// Convert symbol
QualType SymTy;
@@ -507,7 +510,7 @@ public:
QualType ToTy;
llvm::APSInt NewToInt;
std::tie(NewToInt, ToTy) = fixAPSInt(Ctx, To);
- SMTExprRef ToExp = Solver->fromAPSInt(NewToInt);
+ SMTExprRef ToExp = Solver->mkBitvector(NewToInt, NewToInt.getBitWidth());
assert(FromTy == ToTy && "Range values have different types!");
// Construct two (in)equalities, and a logical and/or
Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h?rev=343581&r1=343580&r2=343581&view=diff
==============================================================================
--- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h (original)
+++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h Tue Oct 2 05:55:48 2018
@@ -226,23 +226,23 @@ public:
/// operation
virtual SMTExprRef mkFPtoFP(const SMTExprRef &From, const SMTSortRef &To) = 0;
- /// Creates a floating-point conversion from floatint-point to signed
- /// bitvector operation
- virtual SMTExprRef mkFPtoSBV(const SMTExprRef &From,
- const SMTSortRef &To) = 0;
-
- /// Creates a floating-point conversion from floatint-point to unsigned
- /// bitvector operation
- virtual SMTExprRef mkFPtoUBV(const SMTExprRef &From,
- const SMTSortRef &To) = 0;
-
/// Creates a floating-point conversion from signed bitvector to
/// floatint-point operation
- virtual SMTExprRef mkSBVtoFP(const SMTExprRef &From, unsigned ToWidth) = 0;
+ virtual SMTExprRef mkSBVtoFP(const SMTExprRef &From,
+ const SMTSortRef &To) = 0;
/// Creates a floating-point conversion from unsigned bitvector to
/// floatint-point operation
- virtual SMTExprRef mkUBVtoFP(const SMTExprRef &From, unsigned ToWidth) = 0;
+ virtual SMTExprRef mkUBVtoFP(const SMTExprRef &From,
+ const SMTSortRef &To) = 0;
+
+ /// Creates a floating-point conversion from floatint-point to signed
+ /// bitvector operation
+ virtual SMTExprRef mkFPtoSBV(const SMTExprRef &From, unsigned ToWidth) = 0;
+
+ /// Creates a floating-point conversion from floatint-point to unsigned
+ /// bitvector operation
+ virtual SMTExprRef mkFPtoUBV(const SMTExprRef &From, unsigned ToWidth) = 0;
/// Creates a new symbol, given a name and a sort
virtual SMTExprRef mkSymbol(const char *Name, SMTSortRef Sort) = 0;
@@ -273,18 +273,6 @@ public:
virtual bool getInterpretation(const SMTExprRef &Exp,
llvm::APFloat &Float) = 0;
- /// Construct an SMTExprRef value from a boolean.
- virtual SMTExprRef fromBoolean(const bool Bool) = 0;
-
- /// Construct an SMTExprRef value from a finite APFloat.
- virtual SMTExprRef fromAPFloat(const llvm::APFloat &Float) = 0;
-
- /// Construct an SMTExprRef value from an APSInt.
- virtual SMTExprRef fromAPSInt(const llvm::APSInt &Int) = 0;
-
- /// Construct an SMTExprRef value from an integer.
- virtual SMTExprRef fromInt(const char *Int, uint64_t BitWidth) = 0;
-
/// Check if the constraints are satisfiable
virtual Optional<bool> check() const = 0;
Modified: cfe/trunk/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp?rev=343581&r1=343580&r2=343581&view=diff
==============================================================================
--- cfe/trunk/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp (original)
+++ cfe/trunk/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp Tue Oct 2 05:55:48 2018
@@ -2448,15 +2448,19 @@ void FalsePositiveRefutationBRVisitor::f
// Add constraints to the solver
for (const auto &I : Constraints) {
- SymbolRef Sym = I.first;
+ const SymbolRef Sym = I.first;
+ auto RangeIt = I.second.begin();
- SMTExprRef Constraints = RefutationSolver->fromBoolean(false);
- for (const auto &Range : I.second) {
+ SMTExprRef Constraints = SMTConv::getRangeExpr(
+ RefutationSolver, Ctx, Sym, RangeIt->From(), RangeIt->To(),
+ /*InRange=*/true);
+ while ((++RangeIt) != I.second.end()) {
Constraints = RefutationSolver->mkOr(
Constraints, SMTConv::getRangeExpr(RefutationSolver, Ctx, Sym,
- Range.From(), Range.To(),
+ RangeIt->From(), RangeIt->To(),
/*InRange=*/true));
}
+
RefutationSolver->addConstraint(Constraints);
}
Modified: cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp?rev=343581&r1=343580&r2=343581&view=diff
==============================================================================
--- cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp (original)
+++ cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp Tue Oct 2 05:55:48 2018
@@ -671,7 +671,7 @@ public:
toZ3Expr(*From).AST, toZ3Sort(*To).Sort)));
}
- SMTExprRef mkFPtoSBV(const SMTExprRef &From, const SMTSortRef &To) override {
+ SMTExprRef mkSBVtoFP(const SMTExprRef &From, const SMTSortRef &To) override {
SMTExprRef RoundingMode = getFloatRoundingMode();
return newExprRef(Z3Expr(
Context,
@@ -679,7 +679,7 @@ public:
toZ3Expr(*From).AST, toZ3Sort(*To).Sort)));
}
- SMTExprRef mkFPtoUBV(const SMTExprRef &From, const SMTSortRef &To) override {
+ SMTExprRef mkUBVtoFP(const SMTExprRef &From, const SMTSortRef &To) override {
SMTExprRef RoundingMode = getFloatRoundingMode();
return newExprRef(Z3Expr(
Context,
@@ -687,14 +687,14 @@ public:
toZ3Expr(*From).AST, toZ3Sort(*To).Sort)));
}
- SMTExprRef mkSBVtoFP(const SMTExprRef &From, unsigned ToWidth) override {
+ SMTExprRef mkFPtoSBV(const SMTExprRef &From, unsigned ToWidth) override {
SMTExprRef RoundingMode = getFloatRoundingMode();
return newExprRef(Z3Expr(
Context, Z3_mk_fpa_to_sbv(Context.Context, toZ3Expr(*RoundingMode).AST,
toZ3Expr(*From).AST, ToWidth)));
}
- SMTExprRef mkUBVtoFP(const SMTExprRef &From, unsigned ToWidth) override {
+ SMTExprRef mkFPtoUBV(const SMTExprRef &From, unsigned ToWidth) override {
SMTExprRef RoundingMode = getFloatRoundingMode();
return newExprRef(Z3Expr(
Context, Z3_mk_fpa_to_ubv(Context.Context, toZ3Expr(*RoundingMode).AST,
@@ -747,36 +747,6 @@ public:
return newExprRef(Z3Expr(Context, Z3_mk_fpa_rne(Context.Context)));
}
- SMTExprRef fromBoolean(const bool Bool) override {
- Z3_ast AST =
- Bool ? Z3_mk_true(Context.Context) : Z3_mk_false(Context.Context);
- return newExprRef(Z3Expr(Context, AST));
- }
-
- SMTExprRef fromAPFloat(const llvm::APFloat &Float) override {
- SMTSortRef Sort =
- getFloatSort(llvm::APFloat::semanticsSizeInBits(Float.getSemantics()));
-
- llvm::APSInt Int = llvm::APSInt(Float.bitcastToAPInt(), false);
- SMTExprRef Z3Int = fromAPSInt(Int);
- return newExprRef(Z3Expr(
- Context, Z3_mk_fpa_to_fp_bv(Context.Context, toZ3Expr(*Z3Int).AST,
- toZ3Sort(*Sort).Sort)));
- }
-
- SMTExprRef fromAPSInt(const llvm::APSInt &Int) override {
- SMTSortRef Sort = getBitvectorSort(Int.getBitWidth());
- Z3_ast AST = Z3_mk_numeral(Context.Context, Int.toString(10).c_str(),
- toZ3Sort(*Sort).Sort);
- return newExprRef(Z3Expr(Context, AST));
- }
-
- SMTExprRef fromInt(const char *Int, uint64_t BitWidth) override {
- SMTSortRef Sort = getBitvectorSort(BitWidth);
- Z3_ast AST = Z3_mk_numeral(Context.Context, Int, toZ3Sort(*Sort).Sort);
- return newExprRef(Z3Expr(Context, AST));
- }
-
bool toAPFloat(const SMTSortRef &Sort, const SMTExprRef &AST,
llvm::APFloat &Float, bool useSemantics) {
assert(Sort->isFloatSort() && "Unsupported sort to floating-point!");
More information about the cfe-commits
mailing list