r340533 - [analyzer] Templatefy SMTConstraintManager so more generic code can be moved from solver specific implementations. NFC.
Mikhail R. Gadelha via cfe-commits
cfe-commits at lists.llvm.org
Thu Aug 23 06:21:01 PDT 2018
Author: mramalho
Date: Thu Aug 23 06:21:00 2018
New Revision: 340533
URL: http://llvm.org/viewvc/llvm-project?rev=340533&view=rev
Log:
[analyzer] Templatefy SMTConstraintManager so more generic code can be moved from solver specific implementations. NFC.
Summary:
By making SMTConstraintManager a template and passing the SMT constraint type and expr, we can further move code from the Z3ConstraintManager class to the generic SMT constraint Manager.
Now, each SMT specific constraint manager only needs to implement the method `bool canReasonAbout(SVal X) const`.
Reviewers: NoQ, george.karpenkov
Reviewed By: george.karpenkov
Subscribers: mgorny, xazax.hun, szepet, a.sidorin, Szelethus
Differential Revision: https://reviews.llvm.org/D50770
Removed:
cfe/trunk/lib/StaticAnalyzer/Core/SMTConstraintManager.cpp
Modified:
cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
cfe/trunk/lib/StaticAnalyzer/Core/CMakeLists.txt
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=340533&r1=340532&r2=340533&view=diff
==============================================================================
--- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h (original)
+++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h Thu Aug 23 06:21:00 2018
@@ -21,6 +21,7 @@
namespace clang {
namespace ento {
+template <typename ConstraintSMT, typename SMTExprTy>
class SMTConstraintManager : public clang::ento::SimpleConstraintManager {
SMTSolverRef &Solver;
@@ -34,25 +35,191 @@ public:
// Implementation for interface from SimpleConstraintManager.
//===------------------------------------------------------------------===//
- ProgramStateRef assumeSym(ProgramStateRef state, SymbolRef Sym,
- bool Assumption) override;
+ ProgramStateRef assumeSym(ProgramStateRef State, SymbolRef Sym,
+ bool Assumption) override {
+ ASTContext &Ctx = getBasicVals().getContext();
+
+ QualType RetTy;
+ bool hasComparison;
+
+ SMTExprRef Exp = Solver->getExpr(Ctx, Sym, &RetTy, &hasComparison);
+
+ // Create zero comparison for implicit boolean cast, with reversed
+ // assumption
+ if (!hasComparison && !RetTy->isBooleanType())
+ return assumeExpr(State, Sym,
+ Solver->getZeroExpr(Ctx, Exp, RetTy, !Assumption));
+
+ return assumeExpr(State, Sym, Assumption ? Exp : Solver->mkNot(Exp));
+ }
ProgramStateRef assumeSymInclusiveRange(ProgramStateRef State, SymbolRef Sym,
const llvm::APSInt &From,
const llvm::APSInt &To,
- bool InRange) override;
+ bool InRange) override {
+ ASTContext &Ctx = getBasicVals().getContext();
+ return assumeExpr(State, Sym,
+ Solver->getRangeExpr(Ctx, Sym, From, To, InRange));
+ }
ProgramStateRef assumeSymUnsupported(ProgramStateRef State, SymbolRef Sym,
- bool Assumption) override;
+ bool Assumption) override {
+ // Skip anything that is unsupported
+ return State;
+ }
//===------------------------------------------------------------------===//
// Implementation for interface from ConstraintManager.
//===------------------------------------------------------------------===//
- ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym) override;
+ ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym) override {
+ ASTContext &Ctx = getBasicVals().getContext();
+
+ QualType RetTy;
+ // The expression may be casted, so we cannot call getZ3DataExpr() directly
+ SMTExprRef VarExp = Solver->getExpr(Ctx, Sym, &RetTy);
+ SMTExprRef Exp =
+ Solver->getZeroExpr(Ctx, VarExp, RetTy, /*Assumption=*/true);
+
+ // Negate the constraint
+ SMTExprRef NotExp =
+ Solver->getZeroExpr(Ctx, VarExp, RetTy, /*Assumption=*/false);
+
+ Solver->reset();
+ addStateConstraints(State);
+
+ Solver->push();
+ Solver->addConstraint(Exp);
+ ConditionTruthVal isSat = Solver->check();
+
+ Solver->pop();
+ Solver->addConstraint(NotExp);
+ ConditionTruthVal isNotSat = Solver->check();
+
+ // Zero is the only possible solution
+ if (isSat.isConstrainedTrue() && isNotSat.isConstrainedFalse())
+ return true;
+
+ // Zero is not a solution
+ if (isSat.isConstrainedFalse() && isNotSat.isConstrainedTrue())
+ return false;
+
+ // Zero may be a solution
+ return ConditionTruthVal();
+ }
const llvm::APSInt *getSymVal(ProgramStateRef State,
- SymbolRef Sym) const override;
+ SymbolRef Sym) const override {
+ BasicValueFactory &BVF = getBasicVals();
+ ASTContext &Ctx = BVF.getContext();
+
+ if (const SymbolData *SD = dyn_cast<SymbolData>(Sym)) {
+ QualType Ty = Sym->getType();
+ assert(!Ty->isRealFloatingType());
+ llvm::APSInt Value(Ctx.getTypeSize(Ty),
+ !Ty->isSignedIntegerOrEnumerationType());
+
+ SMTExprRef Exp =
+ Solver->fromData(SD->getSymbolID(), Ty, Ctx.getTypeSize(Ty));
+
+ Solver->reset();
+ addStateConstraints(State);
+
+ // Constraints are unsatisfiable
+ ConditionTruthVal isSat = Solver->check();
+ if (!isSat.isConstrainedTrue())
+ return nullptr;
+
+ // Model does not assign interpretation
+ if (!Solver->getInterpretation(Exp, Value))
+ return nullptr;
+
+ // A value has been obtained, check if it is the only value
+ SMTExprRef NotExp = Solver->fromBinOp(
+ Exp, BO_NE,
+ Ty->isBooleanType() ? Solver->fromBoolean(Value.getBoolValue())
+ : Solver->fromAPSInt(Value),
+ false);
+
+ Solver->addConstraint(NotExp);
+
+ ConditionTruthVal isNotSat = Solver->check();
+ if (isNotSat.isConstrainedTrue())
+ return nullptr;
+
+ // This is the only solution, store it
+ return &BVF.getValue(Value);
+ }
+
+ if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym)) {
+ SymbolRef CastSym = SC->getOperand();
+ QualType CastTy = SC->getType();
+ // Skip the void type
+ if (CastTy->isVoidType())
+ return nullptr;
+
+ const llvm::APSInt *Value;
+ if (!(Value = getSymVal(State, CastSym)))
+ return nullptr;
+ return &BVF.Convert(SC->getType(), *Value);
+ }
+
+ if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
+ const llvm::APSInt *LHS, *RHS;
+ if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) {
+ LHS = getSymVal(State, SIE->getLHS());
+ RHS = &SIE->getRHS();
+ } else if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE)) {
+ LHS = &ISE->getLHS();
+ RHS = getSymVal(State, ISE->getRHS());
+ } else if (const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) {
+ // Early termination to avoid expensive call
+ LHS = getSymVal(State, SSM->getLHS());
+ RHS = LHS ? getSymVal(State, SSM->getRHS()) : nullptr;
+ } else {
+ llvm_unreachable("Unsupported binary expression to get symbol value!");
+ }
+
+ if (!LHS || !RHS)
+ return nullptr;
+
+ llvm::APSInt ConvertedLHS, ConvertedRHS;
+ QualType LTy, RTy;
+ std::tie(ConvertedLHS, LTy) = Solver->fixAPSInt(Ctx, *LHS);
+ std::tie(ConvertedRHS, RTy) = Solver->fixAPSInt(Ctx, *RHS);
+ Solver->doIntTypeConversion<llvm::APSInt, &SMTSolver::castAPSInt>(
+ Ctx, ConvertedLHS, LTy, ConvertedRHS, RTy);
+ return BVF.evalAPSInt(BSE->getOpcode(), ConvertedLHS, ConvertedRHS);
+ }
+
+ llvm_unreachable("Unsupported expression to get symbol value!");
+ }
+
+ ProgramStateRef removeDeadBindings(ProgramStateRef State,
+ SymbolReaper &SymReaper) override {
+ auto CZ = State->get<ConstraintSMT>();
+ auto &CZFactory = State->get_context<ConstraintSMT>();
+
+ for (auto I = CZ.begin(), E = CZ.end(); I != E; ++I) {
+ if (SymReaper.maybeDead(I->first))
+ CZ = CZFactory.remove(CZ, *I);
+ }
+
+ return State->set<ConstraintSMT>(CZ);
+ }
+
+ void print(ProgramStateRef St, raw_ostream &OS, const char *nl,
+ const char *sep) override {
+
+ auto CZ = St->get<ConstraintSMT>();
+
+ OS << nl << sep << "Constraints:";
+ for (auto I = CZ.begin(), E = CZ.end(); I != E; ++I) {
+ OS << nl << ' ' << I->first << " : ";
+ I->second.print(OS);
+ }
+ OS << nl;
+ }
/// Dumps SMT formula
LLVM_DUMP_METHOD void dump() const { Solver->dump(); }
@@ -60,15 +227,44 @@ public:
protected:
// Check whether a new model is satisfiable, and update the program state.
virtual ProgramStateRef assumeExpr(ProgramStateRef State, SymbolRef Sym,
- const SMTExprRef &Exp) = 0;
+ const SMTExprRef &Exp) {
+ // Check the model, avoid simplifying AST to save time
+ if (checkModel(State, Exp).isConstrainedTrue())
+ return State->add<ConstraintSMT>(
+ std::make_pair(Sym, static_cast<const SMTExprTy &>(*Exp)));
+
+ return nullptr;
+ }
/// Given a program state, construct the logical conjunction and add it to
/// the solver
- virtual void addStateConstraints(ProgramStateRef State) const = 0;
+ virtual void addStateConstraints(ProgramStateRef State) const {
+ // TODO: Don't add all the constraints, only the relevant ones
+ auto CZ = State->get<ConstraintSMT>();
+ auto I = CZ.begin(), IE = CZ.end();
+
+ // Construct the logical AND of all the constraints
+ if (I != IE) {
+ std::vector<SMTExprRef> ASTs;
+
+ SMTExprRef Constraint = Solver->newExprRef(I++->second);
+ while (I != IE) {
+ Constraint = Solver->mkAnd(Constraint, Solver->newExprRef(I++->second));
+ }
+
+ Solver->addConstraint(Constraint);
+ }
+ }
// Generate and check a Z3 model, using the given constraint.
ConditionTruthVal checkModel(ProgramStateRef State,
- const SMTExprRef &Exp) const;
+ const SMTExprRef &Exp) const {
+ Solver->reset();
+ Solver->addConstraint(Exp);
+ addStateConstraints(State);
+ return Solver->check();
+ }
+
}; // end class SMTConstraintManager
} // namespace ento
Modified: cfe/trunk/lib/StaticAnalyzer/Core/CMakeLists.txt
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/CMakeLists.txt?rev=340533&r1=340532&r2=340533&view=diff
==============================================================================
--- cfe/trunk/lib/StaticAnalyzer/Core/CMakeLists.txt (original)
+++ cfe/trunk/lib/StaticAnalyzer/Core/CMakeLists.txt Thu Aug 23 06:21:00 2018
@@ -49,7 +49,6 @@ add_clang_library(clangStaticAnalyzerCor
SVals.cpp
SimpleConstraintManager.cpp
SimpleSValBuilder.cpp
- SMTConstraintManager.cpp
Store.cpp
SubEngine.cpp
SymbolManager.cpp
Removed: cfe/trunk/lib/StaticAnalyzer/Core/SMTConstraintManager.cpp
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/SMTConstraintManager.cpp?rev=340532&view=auto
==============================================================================
--- cfe/trunk/lib/StaticAnalyzer/Core/SMTConstraintManager.cpp (original)
+++ cfe/trunk/lib/StaticAnalyzer/Core/SMTConstraintManager.cpp (removed)
@@ -1,181 +0,0 @@
-//== SMTConstraintManager.cpp -----------------------------------*- C++ -*--==//
-//
-// The LLVM Compiler Infrastructure
-//
-// This file is distributed under the University of Illinois Open Source
-// License. See LICENSE.TXT for details.
-//
-//===----------------------------------------------------------------------===//
-
-#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h"
-#include "clang/Basic/TargetInfo.h"
-#include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h"
-#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
-
-using namespace clang;
-using namespace ento;
-
-ProgramStateRef SMTConstraintManager::assumeSym(ProgramStateRef State,
- SymbolRef Sym,
- bool Assumption) {
- ASTContext &Ctx = getBasicVals().getContext();
-
- QualType RetTy;
- bool hasComparison;
-
- SMTExprRef Exp = Solver->getExpr(Ctx, Sym, &RetTy, &hasComparison);
-
- // Create zero comparison for implicit boolean cast, with reversed assumption
- if (!hasComparison && !RetTy->isBooleanType())
- return assumeExpr(State, Sym,
- Solver->getZeroExpr(Ctx, Exp, RetTy, !Assumption));
-
- return assumeExpr(State, Sym, Assumption ? Exp : Solver->mkNot(Exp));
-}
-
-ProgramStateRef SMTConstraintManager::assumeSymInclusiveRange(
- ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
- const llvm::APSInt &To, bool InRange) {
- ASTContext &Ctx = getBasicVals().getContext();
- return assumeExpr(State, Sym,
- Solver->getRangeExpr(Ctx, Sym, From, To, InRange));
-}
-
-ProgramStateRef
-SMTConstraintManager::assumeSymUnsupported(ProgramStateRef State, SymbolRef Sym,
- bool Assumption) {
- // Skip anything that is unsupported
- return State;
-}
-
-ConditionTruthVal SMTConstraintManager::checkNull(ProgramStateRef State,
- SymbolRef Sym) {
- ASTContext &Ctx = getBasicVals().getContext();
-
- QualType RetTy;
- // The expression may be casted, so we cannot call getZ3DataExpr() directly
- SMTExprRef VarExp = Solver->getExpr(Ctx, Sym, &RetTy);
- SMTExprRef Exp = Solver->getZeroExpr(Ctx, VarExp, RetTy, /*Assumption=*/true);
-
- // Negate the constraint
- SMTExprRef NotExp =
- Solver->getZeroExpr(Ctx, VarExp, RetTy, /*Assumption=*/false);
-
- Solver->reset();
- addStateConstraints(State);
-
- Solver->push();
- Solver->addConstraint(Exp);
- ConditionTruthVal isSat = Solver->check();
-
- Solver->pop();
- Solver->addConstraint(NotExp);
- ConditionTruthVal isNotSat = Solver->check();
-
- // Zero is the only possible solution
- if (isSat.isConstrainedTrue() && isNotSat.isConstrainedFalse())
- return true;
-
- // Zero is not a solution
- if (isSat.isConstrainedFalse() && isNotSat.isConstrainedTrue())
- return false;
-
- // Zero may be a solution
- return ConditionTruthVal();
-}
-
-const llvm::APSInt *SMTConstraintManager::getSymVal(ProgramStateRef State,
- SymbolRef Sym) const {
- BasicValueFactory &BVF = getBasicVals();
- ASTContext &Ctx = BVF.getContext();
-
- if (const SymbolData *SD = dyn_cast<SymbolData>(Sym)) {
- QualType Ty = Sym->getType();
- assert(!Ty->isRealFloatingType());
- llvm::APSInt Value(Ctx.getTypeSize(Ty),
- !Ty->isSignedIntegerOrEnumerationType());
-
- SMTExprRef Exp =
- Solver->fromData(SD->getSymbolID(), Ty, Ctx.getTypeSize(Ty));
-
- Solver->reset();
- addStateConstraints(State);
-
- // Constraints are unsatisfiable
- ConditionTruthVal isSat = Solver->check();
- if (!isSat.isConstrainedTrue())
- return nullptr;
-
- // Model does not assign interpretation
- if (!Solver->getInterpretation(Exp, Value))
- return nullptr;
-
- // A value has been obtained, check if it is the only value
- SMTExprRef NotExp = Solver->fromBinOp(
- Exp, BO_NE,
- Ty->isBooleanType() ? Solver->fromBoolean(Value.getBoolValue())
- : Solver->fromAPSInt(Value),
- false);
-
- Solver->addConstraint(NotExp);
-
- ConditionTruthVal isNotSat = Solver->check();
- if (isNotSat.isConstrainedTrue())
- return nullptr;
-
- // This is the only solution, store it
- return &BVF.getValue(Value);
- }
-
- if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym)) {
- SymbolRef CastSym = SC->getOperand();
- QualType CastTy = SC->getType();
- // Skip the void type
- if (CastTy->isVoidType())
- return nullptr;
-
- const llvm::APSInt *Value;
- if (!(Value = getSymVal(State, CastSym)))
- return nullptr;
- return &BVF.Convert(SC->getType(), *Value);
- }
-
- if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
- const llvm::APSInt *LHS, *RHS;
- if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) {
- LHS = getSymVal(State, SIE->getLHS());
- RHS = &SIE->getRHS();
- } else if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE)) {
- LHS = &ISE->getLHS();
- RHS = getSymVal(State, ISE->getRHS());
- } else if (const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) {
- // Early termination to avoid expensive call
- LHS = getSymVal(State, SSM->getLHS());
- RHS = LHS ? getSymVal(State, SSM->getRHS()) : nullptr;
- } else {
- llvm_unreachable("Unsupported binary expression to get symbol value!");
- }
-
- if (!LHS || !RHS)
- return nullptr;
-
- llvm::APSInt ConvertedLHS, ConvertedRHS;
- QualType LTy, RTy;
- std::tie(ConvertedLHS, LTy) = Solver->fixAPSInt(Ctx, *LHS);
- std::tie(ConvertedRHS, RTy) = Solver->fixAPSInt(Ctx, *RHS);
- Solver->doIntTypeConversion<llvm::APSInt, &SMTSolver::castAPSInt>(
- Ctx, ConvertedLHS, LTy, ConvertedRHS, RTy);
- return BVF.evalAPSInt(BSE->getOpcode(), ConvertedLHS, ConvertedRHS);
- }
-
- llvm_unreachable("Unsupported expression to get symbol value!");
-}
-
-ConditionTruthVal
-SMTConstraintManager::checkModel(ProgramStateRef State,
- const SMTExprRef &Exp) const {
- Solver->reset();
- Solver->addConstraint(Exp);
- addStateConstraints(State);
- return Solver->check();
-}
Modified: cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp?rev=340533&r1=340532&r2=340533&view=diff
==============================================================================
--- cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp (original)
+++ cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp Thu Aug 23 06:21:00 2018
@@ -904,31 +904,13 @@ public:
}
}; // end class Z3Solver
-class Z3ConstraintManager : public SMTConstraintManager {
+class Z3ConstraintManager : public SMTConstraintManager<ConstraintZ3, Z3Expr> {
SMTSolverRef Solver = CreateZ3Solver();
public:
Z3ConstraintManager(SubEngine *SE, SValBuilder &SB)
: SMTConstraintManager(SE, SB, Solver) {}
- void addStateConstraints(ProgramStateRef State) const override {
- // TODO: Don't add all the constraints, only the relevant ones
- ConstraintZ3Ty CZ = State->get<ConstraintZ3>();
- ConstraintZ3Ty::iterator I = CZ.begin(), IE = CZ.end();
-
- // Construct the logical AND of all the constraints
- if (I != IE) {
- std::vector<SMTExprRef> ASTs;
-
- SMTExprRef Constraint = Solver->newExprRef(I++->second);
- while (I != IE) {
- Constraint = Solver->mkAnd(Constraint, Solver->newExprRef(I++->second));
- }
-
- Solver->addConstraint(Constraint);
- }
- }
-
bool canReasonAbout(SVal X) const override {
const TargetInfo &TI = getBasicVals().getContext().getTargetInfo();
@@ -971,45 +953,6 @@ public:
llvm_unreachable("Unsupported expression to reason about!");
}
-
- ProgramStateRef removeDeadBindings(ProgramStateRef State,
- SymbolReaper &SymReaper) override {
- ConstraintZ3Ty CZ = State->get<ConstraintZ3>();
- ConstraintZ3Ty::Factory &CZFactory = State->get_context<ConstraintZ3>();
-
- for (ConstraintZ3Ty::iterator I = CZ.begin(), E = CZ.end(); I != E; ++I) {
- if (SymReaper.maybeDead(I->first))
- CZ = CZFactory.remove(CZ, *I);
- }
-
- return State->set<ConstraintZ3>(CZ);
- }
-
- ProgramStateRef assumeExpr(ProgramStateRef State, SymbolRef Sym,
- const SMTExprRef &Exp) override {
- // Check the model, avoid simplifying AST to save time
- if (checkModel(State, Exp).isConstrainedTrue())
- return State->add<ConstraintZ3>(std::make_pair(Sym, toZ3Expr(*Exp)));
-
- return nullptr;
- }
-
- //==------------------------------------------------------------------------==/
- // Pretty-printing.
- //==------------------------------------------------------------------------==/
-
- void print(ProgramStateRef St, raw_ostream &OS, const char *nl,
- const char *sep) override {
-
- ConstraintZ3Ty CZ = St->get<ConstraintZ3>();
-
- OS << nl << sep << "Constraints:";
- for (ConstraintZ3Ty::iterator I = CZ.begin(), E = CZ.end(); I != E; ++I) {
- OS << nl << ' ' << I->first << " : ";
- I->second.print(OS);
- }
- OS << nl;
- }
}; // end class Z3ConstraintManager
} // end anonymous namespace
More information about the cfe-commits
mailing list