| //== 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(); |
| } |