1 //== SMTConstraintManager.cpp -----------------------------------*- C++ -*--==// 2 // 3 // The LLVM Compiler Infrastructure 4 // 5 // This file is distributed under the University of Illinois Open Source 6 // License. See LICENSE.TXT for details. 7 // 8 //===----------------------------------------------------------------------===// 9 10 #include "clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h" 11 #include "clang/Basic/TargetInfo.h" 12 #include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h" 13 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h" 14 15 using namespace clang; 16 using namespace ento; 17 18 ProgramStateRef SMTConstraintManager::assumeSym(ProgramStateRef State, 19 SymbolRef Sym, 20 bool Assumption) { 21 ASTContext &Ctx = getBasicVals().getContext(); 22 23 QualType RetTy; 24 bool hasComparison; 25 26 SMTExprRef Exp = Solver->getExpr(Ctx, Sym, &RetTy, &hasComparison); 27 28 // Create zero comparison for implicit boolean cast, with reversed assumption 29 if (!hasComparison && !RetTy->isBooleanType()) 30 return assumeExpr(State, Sym, 31 Solver->getZeroExpr(Ctx, Exp, RetTy, !Assumption)); 32 33 return assumeExpr(State, Sym, Assumption ? Exp : Solver->mkNot(Exp)); 34 } 35 36 ProgramStateRef SMTConstraintManager::assumeSymInclusiveRange( 37 ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From, 38 const llvm::APSInt &To, bool InRange) { 39 ASTContext &Ctx = getBasicVals().getContext(); 40 return assumeExpr(State, Sym, 41 Solver->getRangeExpr(Ctx, Sym, From, To, InRange)); 42 } 43 44 ProgramStateRef 45 SMTConstraintManager::assumeSymUnsupported(ProgramStateRef State, SymbolRef Sym, 46 bool Assumption) { 47 // Skip anything that is unsupported 48 return State; 49 } 50 51 ConditionTruthVal SMTConstraintManager::checkNull(ProgramStateRef State, 52 SymbolRef Sym) { 53 ASTContext &Ctx = getBasicVals().getContext(); 54 55 QualType RetTy; 56 // The expression may be casted, so we cannot call getZ3DataExpr() directly 57 SMTExprRef VarExp = Solver->getExpr(Ctx, Sym, &RetTy); 58 SMTExprRef Exp = Solver->getZeroExpr(Ctx, VarExp, RetTy, /*Assumption=*/true); 59 60 // Negate the constraint 61 SMTExprRef NotExp = 62 Solver->getZeroExpr(Ctx, VarExp, RetTy, /*Assumption=*/false); 63 64 Solver->reset(); 65 addStateConstraints(State); 66 67 Solver->push(); 68 Solver->addConstraint(Exp); 69 ConditionTruthVal isSat = Solver->check(); 70 71 Solver->pop(); 72 Solver->addConstraint(NotExp); 73 ConditionTruthVal isNotSat = Solver->check(); 74 75 // Zero is the only possible solution 76 if (isSat.isConstrainedTrue() && isNotSat.isConstrainedFalse()) 77 return true; 78 79 // Zero is not a solution 80 if (isSat.isConstrainedFalse() && isNotSat.isConstrainedTrue()) 81 return false; 82 83 // Zero may be a solution 84 return ConditionTruthVal(); 85 } 86 87 const llvm::APSInt *SMTConstraintManager::getSymVal(ProgramStateRef State, 88 SymbolRef Sym) const { 89 BasicValueFactory &BVF = getBasicVals(); 90 ASTContext &Ctx = BVF.getContext(); 91 92 if (const SymbolData *SD = dyn_cast<SymbolData>(Sym)) { 93 QualType Ty = Sym->getType(); 94 assert(!Ty->isRealFloatingType()); 95 llvm::APSInt Value(Ctx.getTypeSize(Ty), 96 !Ty->isSignedIntegerOrEnumerationType()); 97 98 SMTExprRef Exp = 99 Solver->fromData(SD->getSymbolID(), Ty, Ctx.getTypeSize(Ty)); 100 101 Solver->reset(); 102 addStateConstraints(State); 103 104 // Constraints are unsatisfiable 105 ConditionTruthVal isSat = Solver->check(); 106 if (!isSat.isConstrainedTrue()) 107 return nullptr; 108 109 // Model does not assign interpretation 110 if (!Solver->getInterpretation(Exp, Value)) 111 return nullptr; 112 113 // A value has been obtained, check if it is the only value 114 SMTExprRef NotExp = Solver->fromBinOp( 115 Exp, BO_NE, 116 Ty->isBooleanType() ? Solver->fromBoolean(Value.getBoolValue()) 117 : Solver->fromAPSInt(Value), 118 false); 119 120 Solver->addConstraint(NotExp); 121 122 ConditionTruthVal isNotSat = Solver->check(); 123 if (isNotSat.isConstrainedTrue()) 124 return nullptr; 125 126 // This is the only solution, store it 127 return &BVF.getValue(Value); 128 } 129 130 if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym)) { 131 SymbolRef CastSym = SC->getOperand(); 132 QualType CastTy = SC->getType(); 133 // Skip the void type 134 if (CastTy->isVoidType()) 135 return nullptr; 136 137 const llvm::APSInt *Value; 138 if (!(Value = getSymVal(State, CastSym))) 139 return nullptr; 140 return &BVF.Convert(SC->getType(), *Value); 141 } 142 143 if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) { 144 const llvm::APSInt *LHS, *RHS; 145 if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) { 146 LHS = getSymVal(State, SIE->getLHS()); 147 RHS = &SIE->getRHS(); 148 } else if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE)) { 149 LHS = &ISE->getLHS(); 150 RHS = getSymVal(State, ISE->getRHS()); 151 } else if (const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) { 152 // Early termination to avoid expensive call 153 LHS = getSymVal(State, SSM->getLHS()); 154 RHS = LHS ? getSymVal(State, SSM->getRHS()) : nullptr; 155 } else { 156 llvm_unreachable("Unsupported binary expression to get symbol value!"); 157 } 158 159 if (!LHS || !RHS) 160 return nullptr; 161 162 llvm::APSInt ConvertedLHS, ConvertedRHS; 163 QualType LTy, RTy; 164 std::tie(ConvertedLHS, LTy) = Solver->fixAPSInt(Ctx, *LHS); 165 std::tie(ConvertedRHS, RTy) = Solver->fixAPSInt(Ctx, *RHS); 166 Solver->doIntTypeConversion<llvm::APSInt, &SMTSolver::castAPSInt>( 167 Ctx, ConvertedLHS, LTy, ConvertedRHS, RTy); 168 return BVF.evalAPSInt(BSE->getOpcode(), ConvertedLHS, ConvertedRHS); 169 } 170 171 llvm_unreachable("Unsupported expression to get symbol value!"); 172 } 173 174 ConditionTruthVal 175 SMTConstraintManager::checkModel(ProgramStateRef State, 176 const SMTExprRef &Exp) const { 177 Solver->reset(); 178 Solver->addConstraint(Exp); 179 addStateConstraints(State); 180 return Solver->check(); 181 } 182