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