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