summaryrefslogtreecommitdiffstats
path: root/clang/lib
diff options
context:
space:
mode:
Diffstat (limited to 'clang/lib')
-rw-r--r--clang/lib/StaticAnalyzer/Core/CMakeLists.txt1
-rw-r--r--clang/lib/StaticAnalyzer/Core/SMTConstraintManager.cpp181
-rw-r--r--clang/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp59
3 files changed, 1 insertions, 240 deletions
diff --git a/clang/lib/StaticAnalyzer/Core/CMakeLists.txt b/clang/lib/StaticAnalyzer/Core/CMakeLists.txt
index 86f2abf8b28..db06e4efd54 100644
--- a/clang/lib/StaticAnalyzer/Core/CMakeLists.txt
+++ b/clang/lib/StaticAnalyzer/Core/CMakeLists.txt
@@ -49,7 +49,6 @@ add_clang_library(clangStaticAnalyzerCore
SVals.cpp
SimpleConstraintManager.cpp
SimpleSValBuilder.cpp
- SMTConstraintManager.cpp
Store.cpp
SubEngine.cpp
SymbolManager.cpp
diff --git a/clang/lib/StaticAnalyzer/Core/SMTConstraintManager.cpp b/clang/lib/StaticAnalyzer/Core/SMTConstraintManager.cpp
deleted file mode 100644
index d379562bf32..00000000000
--- a/clang/lib/StaticAnalyzer/Core/SMTConstraintManager.cpp
+++ /dev/null
@@ -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();
-}
diff --git a/clang/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp b/clang/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
index fc936cb0539..a71749bf169 100644
--- a/clang/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
+++ b/clang/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
@@ -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
OpenPOWER on IntegriCloud