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