diff options
Diffstat (limited to 'lib/StaticAnalyzer/Core/SMTConstraintManager.cpp')
| -rw-r--r-- | lib/StaticAnalyzer/Core/SMTConstraintManager.cpp | 181 |
1 files changed, 0 insertions, 181 deletions
diff --git a/lib/StaticAnalyzer/Core/SMTConstraintManager.cpp b/lib/StaticAnalyzer/Core/SMTConstraintManager.cpp deleted file mode 100644 index d379562bf325e..0000000000000 --- a/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(); -} |