1 //== SMTConstraintManager.h -------------------------------------*- C++ -*--==// 2 // 3 // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. 4 // See https://llvm.org/LICENSE.txt for license information. 5 // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception 6 // 7 //===----------------------------------------------------------------------===// 8 // 9 // This file defines a SMT generic API, which will be the base class for 10 // every SMT solver specific class. 11 // 12 //===----------------------------------------------------------------------===// 13 14 #ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONSTRAINTMANAGER_H 15 #define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONSTRAINTMANAGER_H 16 17 #include "clang/Basic/JsonSupport.h" 18 #include "clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h" 19 #include "clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h" 20 21 typedef llvm::ImmutableSet< 22 std::pair<clang::ento::SymbolRef, const llvm::SMTExpr *>> 23 ConstraintSMTType; 24 REGISTER_TRAIT_WITH_PROGRAMSTATE(ConstraintSMT, ConstraintSMTType) 25 26 namespace clang { 27 namespace ento { 28 29 class SMTConstraintManager : public clang::ento::SimpleConstraintManager { 30 mutable llvm::SMTSolverRef Solver = llvm::CreateZ3Solver(); 31 32 public: 33 SMTConstraintManager(clang::ento::SubEngine *SE, clang::ento::SValBuilder &SB) 34 : SimpleConstraintManager(SE, SB) {} 35 virtual ~SMTConstraintManager() = default; 36 37 //===------------------------------------------------------------------===// 38 // Implementation for interface from SimpleConstraintManager. 39 //===------------------------------------------------------------------===// 40 41 ProgramStateRef assumeSym(ProgramStateRef State, SymbolRef Sym, 42 bool Assumption) override { 43 ASTContext &Ctx = getBasicVals().getContext(); 44 45 QualType RetTy; 46 bool hasComparison; 47 48 llvm::SMTExprRef Exp = 49 SMTConv::getExpr(Solver, Ctx, Sym, &RetTy, &hasComparison); 50 51 // Create zero comparison for implicit boolean cast, with reversed 52 // assumption 53 if (!hasComparison && !RetTy->isBooleanType()) 54 return assumeExpr( 55 State, Sym, 56 SMTConv::getZeroExpr(Solver, Ctx, Exp, RetTy, !Assumption)); 57 58 return assumeExpr(State, Sym, Assumption ? Exp : Solver->mkNot(Exp)); 59 } 60 61 ProgramStateRef assumeSymInclusiveRange(ProgramStateRef State, SymbolRef Sym, 62 const llvm::APSInt &From, 63 const llvm::APSInt &To, 64 bool InRange) override { 65 ASTContext &Ctx = getBasicVals().getContext(); 66 return assumeExpr( 67 State, Sym, SMTConv::getRangeExpr(Solver, Ctx, Sym, From, To, InRange)); 68 } 69 70 ProgramStateRef assumeSymUnsupported(ProgramStateRef State, SymbolRef Sym, 71 bool Assumption) override { 72 // Skip anything that is unsupported 73 return State; 74 } 75 76 //===------------------------------------------------------------------===// 77 // Implementation for interface from ConstraintManager. 78 //===------------------------------------------------------------------===// 79 80 ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym) override { 81 ASTContext &Ctx = getBasicVals().getContext(); 82 83 QualType RetTy; 84 // The expression may be casted, so we cannot call getZ3DataExpr() directly 85 llvm::SMTExprRef VarExp = SMTConv::getExpr(Solver, Ctx, Sym, &RetTy); 86 llvm::SMTExprRef Exp = 87 SMTConv::getZeroExpr(Solver, Ctx, VarExp, RetTy, /*Assumption=*/true); 88 89 // Negate the constraint 90 llvm::SMTExprRef NotExp = 91 SMTConv::getZeroExpr(Solver, Ctx, VarExp, RetTy, /*Assumption=*/false); 92 93 ConditionTruthVal isSat = checkModel(State, Sym, Exp); 94 ConditionTruthVal isNotSat = checkModel(State, Sym, NotExp); 95 96 // Zero is the only possible solution 97 if (isSat.isConstrainedTrue() && isNotSat.isConstrainedFalse()) 98 return true; 99 100 // Zero is not a solution 101 if (isSat.isConstrainedFalse() && isNotSat.isConstrainedTrue()) 102 return false; 103 104 // Zero may be a solution 105 return ConditionTruthVal(); 106 } 107 108 const llvm::APSInt *getSymVal(ProgramStateRef State, 109 SymbolRef Sym) const override { 110 BasicValueFactory &BVF = getBasicVals(); 111 ASTContext &Ctx = BVF.getContext(); 112 113 if (const SymbolData *SD = dyn_cast<SymbolData>(Sym)) { 114 QualType Ty = Sym->getType(); 115 assert(!Ty->isRealFloatingType()); 116 llvm::APSInt Value(Ctx.getTypeSize(Ty), 117 !Ty->isSignedIntegerOrEnumerationType()); 118 119 // TODO: this should call checkModel so we can use the cache, however, 120 // this method tries to get the interpretation (the actual value) from 121 // the solver, which is currently not cached. 122 123 llvm::SMTExprRef Exp = 124 SMTConv::fromData(Solver, SD->getSymbolID(), Ty, Ctx.getTypeSize(Ty)); 125 126 Solver->reset(); 127 addStateConstraints(State); 128 129 // Constraints are unsatisfiable 130 Optional<bool> isSat = Solver->check(); 131 if (!isSat.hasValue() || !isSat.getValue()) 132 return nullptr; 133 134 // Model does not assign interpretation 135 if (!Solver->getInterpretation(Exp, Value)) 136 return nullptr; 137 138 // A value has been obtained, check if it is the only value 139 llvm::SMTExprRef NotExp = SMTConv::fromBinOp( 140 Solver, Exp, BO_NE, 141 Ty->isBooleanType() ? Solver->mkBoolean(Value.getBoolValue()) 142 : Solver->mkBitvector(Value, Value.getBitWidth()), 143 /*isSigned=*/false); 144 145 Solver->addConstraint(NotExp); 146 147 Optional<bool> isNotSat = Solver->check(); 148 if (!isSat.hasValue() || isNotSat.getValue()) 149 return nullptr; 150 151 // This is the only solution, store it 152 return &BVF.getValue(Value); 153 } 154 155 if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym)) { 156 SymbolRef CastSym = SC->getOperand(); 157 QualType CastTy = SC->getType(); 158 // Skip the void type 159 if (CastTy->isVoidType()) 160 return nullptr; 161 162 const llvm::APSInt *Value; 163 if (!(Value = getSymVal(State, CastSym))) 164 return nullptr; 165 return &BVF.Convert(SC->getType(), *Value); 166 } 167 168 if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) { 169 const llvm::APSInt *LHS, *RHS; 170 if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) { 171 LHS = getSymVal(State, SIE->getLHS()); 172 RHS = &SIE->getRHS(); 173 } else if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE)) { 174 LHS = &ISE->getLHS(); 175 RHS = getSymVal(State, ISE->getRHS()); 176 } else if (const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) { 177 // Early termination to avoid expensive call 178 LHS = getSymVal(State, SSM->getLHS()); 179 RHS = LHS ? getSymVal(State, SSM->getRHS()) : nullptr; 180 } else { 181 llvm_unreachable("Unsupported binary expression to get symbol value!"); 182 } 183 184 if (!LHS || !RHS) 185 return nullptr; 186 187 llvm::APSInt ConvertedLHS, ConvertedRHS; 188 QualType LTy, RTy; 189 std::tie(ConvertedLHS, LTy) = SMTConv::fixAPSInt(Ctx, *LHS); 190 std::tie(ConvertedRHS, RTy) = SMTConv::fixAPSInt(Ctx, *RHS); 191 SMTConv::doIntTypeConversion<llvm::APSInt, &SMTConv::castAPSInt>( 192 Solver, Ctx, ConvertedLHS, LTy, ConvertedRHS, RTy); 193 return BVF.evalAPSInt(BSE->getOpcode(), ConvertedLHS, ConvertedRHS); 194 } 195 196 llvm_unreachable("Unsupported expression to get symbol value!"); 197 } 198 199 ProgramStateRef removeDeadBindings(ProgramStateRef State, 200 SymbolReaper &SymReaper) override { 201 auto CZ = State->get<ConstraintSMT>(); 202 auto &CZFactory = State->get_context<ConstraintSMT>(); 203 204 for (auto I = CZ.begin(), E = CZ.end(); I != E; ++I) { 205 if (SymReaper.isDead(I->first)) 206 CZ = CZFactory.remove(CZ, *I); 207 } 208 209 return State->set<ConstraintSMT>(CZ); 210 } 211 212 void printJson(raw_ostream &Out, ProgramStateRef State, const char *NL = "\n", 213 unsigned int Space = 0, bool IsDot = false) const override { 214 ConstraintSMTType Constraints = State->get<ConstraintSMT>(); 215 216 Indent(Out, Space, IsDot) << "\"constraints\": "; 217 if (Constraints.isEmpty()) { 218 Out << "null," << NL; 219 return; 220 } 221 222 ++Space; 223 Out << '[' << NL; 224 for (ConstraintSMTType::iterator I = Constraints.begin(); 225 I != Constraints.end(); ++I) { 226 Indent(Out, Space, IsDot) 227 << "{ \"symbol\": \"" << I->first << "\", \"range\": \""; 228 I->second->print(Out); 229 Out << "\" }"; 230 231 if (std::next(I) != Constraints.end()) 232 Out << ','; 233 Out << NL; 234 } 235 236 --Space; 237 Indent(Out, Space, IsDot) << "],"; 238 } 239 240 bool haveEqualConstraints(ProgramStateRef S1, 241 ProgramStateRef S2) const override { 242 return S1->get<ConstraintSMT>() == S2->get<ConstraintSMT>(); 243 } 244 245 bool canReasonAbout(SVal X) const override { 246 const TargetInfo &TI = getBasicVals().getContext().getTargetInfo(); 247 248 Optional<nonloc::SymbolVal> SymVal = X.getAs<nonloc::SymbolVal>(); 249 if (!SymVal) 250 return true; 251 252 const SymExpr *Sym = SymVal->getSymbol(); 253 QualType Ty = Sym->getType(); 254 255 // Complex types are not modeled 256 if (Ty->isComplexType() || Ty->isComplexIntegerType()) 257 return false; 258 259 // Non-IEEE 754 floating-point types are not modeled 260 if ((Ty->isSpecificBuiltinType(BuiltinType::LongDouble) && 261 (&TI.getLongDoubleFormat() == &llvm::APFloat::x87DoubleExtended() || 262 &TI.getLongDoubleFormat() == &llvm::APFloat::PPCDoubleDouble()))) 263 return false; 264 265 if (Ty->isRealFloatingType()) 266 return Solver->isFPSupported(); 267 268 if (isa<SymbolData>(Sym)) 269 return true; 270 271 SValBuilder &SVB = getSValBuilder(); 272 273 if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym)) 274 return canReasonAbout(SVB.makeSymbolVal(SC->getOperand())); 275 276 if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) { 277 if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) 278 return canReasonAbout(SVB.makeSymbolVal(SIE->getLHS())); 279 280 if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE)) 281 return canReasonAbout(SVB.makeSymbolVal(ISE->getRHS())); 282 283 if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(BSE)) 284 return canReasonAbout(SVB.makeSymbolVal(SSE->getLHS())) && 285 canReasonAbout(SVB.makeSymbolVal(SSE->getRHS())); 286 } 287 288 llvm_unreachable("Unsupported expression to reason about!"); 289 } 290 291 /// Dumps SMT formula 292 LLVM_DUMP_METHOD void dump() const { Solver->dump(); } 293 294 protected: 295 // Check whether a new model is satisfiable, and update the program state. 296 virtual ProgramStateRef assumeExpr(ProgramStateRef State, SymbolRef Sym, 297 const llvm::SMTExprRef &Exp) { 298 // Check the model, avoid simplifying AST to save time 299 if (checkModel(State, Sym, Exp).isConstrainedTrue()) 300 return State->add<ConstraintSMT>(std::make_pair(Sym, Exp)); 301 302 return nullptr; 303 } 304 305 /// Given a program state, construct the logical conjunction and add it to 306 /// the solver 307 virtual void addStateConstraints(ProgramStateRef State) const { 308 // TODO: Don't add all the constraints, only the relevant ones 309 auto CZ = State->get<ConstraintSMT>(); 310 auto I = CZ.begin(), IE = CZ.end(); 311 312 // Construct the logical AND of all the constraints 313 if (I != IE) { 314 std::vector<llvm::SMTExprRef> ASTs; 315 316 llvm::SMTExprRef Constraint = I++->second; 317 while (I != IE) { 318 Constraint = Solver->mkAnd(Constraint, I++->second); 319 } 320 321 Solver->addConstraint(Constraint); 322 } 323 } 324 325 // Generate and check a Z3 model, using the given constraint. 326 ConditionTruthVal checkModel(ProgramStateRef State, SymbolRef Sym, 327 const llvm::SMTExprRef &Exp) const { 328 ProgramStateRef NewState = 329 State->add<ConstraintSMT>(std::make_pair(Sym, Exp)); 330 331 llvm::FoldingSetNodeID ID; 332 NewState->get<ConstraintSMT>().Profile(ID); 333 334 unsigned hash = ID.ComputeHash(); 335 auto I = Cached.find(hash); 336 if (I != Cached.end()) 337 return I->second; 338 339 Solver->reset(); 340 addStateConstraints(NewState); 341 342 Optional<bool> res = Solver->check(); 343 if (!res.hasValue()) 344 Cached[hash] = ConditionTruthVal(); 345 else 346 Cached[hash] = ConditionTruthVal(res.getValue()); 347 348 return Cached[hash]; 349 } 350 351 // Cache the result of an SMT query (true, false, unknown). The key is the 352 // hash of the constraints in a state 353 mutable llvm::DenseMap<unsigned, ConditionTruthVal> Cached; 354 }; // end class SMTConstraintManager 355 356 } // namespace ento 357 } // namespace clang 358 359 #endif 360