diff options
4 files changed, 206 insertions, 249 deletions
diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h index 19d3d5973e0..d73c374c70e 100644 --- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h +++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h @@ -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 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 |
