1 //===- ConstraintManager.cpp - Constraints on symbolic values. ------------===// 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 defined the interface to manage constraints on symbolic values. 10 // 11 //===----------------------------------------------------------------------===// 12 13 #include "clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h" 14 #include "clang/AST/Type.h" 15 #include "clang/StaticAnalyzer/Core/PathSensitive/MemRegion.h" 16 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h" 17 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState_Fwd.h" 18 #include "clang/StaticAnalyzer/Core/PathSensitive/SVals.h" 19 20 using namespace clang; 21 using namespace ento; 22 23 ConstraintManager::~ConstraintManager() = default; 24 25 static DefinedSVal getLocFromSymbol(const ProgramStateRef &State, 26 SymbolRef Sym) { 27 const MemRegion *R = 28 State->getStateManager().getRegionManager().getSymbolicRegion(Sym); 29 return loc::MemRegionVal(R); 30 } 31 32 ConditionTruthVal ConstraintManager::checkNull(ProgramStateRef State, 33 SymbolRef Sym) { 34 QualType Ty = Sym->getType(); 35 DefinedSVal V = Loc::isLocType(Ty) ? getLocFromSymbol(State, Sym) 36 : nonloc::SymbolVal(Sym); 37 const ProgramStatePair &P = assumeDual(State, V); 38 if (P.first && !P.second) 39 return ConditionTruthVal(false); 40 if (!P.first && P.second) 41 return ConditionTruthVal(true); 42 return {}; 43 } 44 45 template <typename AssumeFunction> 46 ConstraintManager::ProgramStatePair 47 ConstraintManager::assumeDualImpl(ProgramStateRef &State, 48 AssumeFunction &Assume) { 49 if (State->isPosteriorlyOverconstrained()) 50 return {State, State}; 51 52 ProgramStateRef StTrue = Assume(true); 53 54 if (!StTrue) { 55 ProgramStateRef StFalse = Assume(false); 56 if (LLVM_UNLIKELY(!StFalse)) { // both infeasible 57 ProgramStateRef StInfeasible = State->cloneAsPosteriorlyOverconstrained(); 58 assert(StInfeasible->isPosteriorlyOverconstrained()); 59 // Checkers might rely on the API contract that both returned states 60 // cannot be null. Thus, we return StInfeasible for both branches because 61 // it might happen that a Checker uncoditionally uses one of them if the 62 // other is a nullptr. This may also happen with the non-dual and 63 // adjacent `assume(true)` and `assume(false)` calls. By implementing 64 // assume in therms of assumeDual, we can keep our API contract there as 65 // well. 66 return ProgramStatePair(StInfeasible, StInfeasible); 67 } 68 return ProgramStatePair(nullptr, StFalse); 69 } 70 71 ProgramStateRef StFalse = Assume(false); 72 if (!StFalse) { 73 return ProgramStatePair(StTrue, nullptr); 74 } 75 76 return ProgramStatePair(StTrue, StFalse); 77 } 78 79 ConstraintManager::ProgramStatePair 80 ConstraintManager::assumeDual(ProgramStateRef State, DefinedSVal Cond) { 81 auto AssumeFun = [&](bool Assumption) { 82 return assumeInternal(State, Cond, Assumption); 83 }; 84 return assumeDualImpl(State, AssumeFun); 85 } 86 87 ConstraintManager::ProgramStatePair 88 ConstraintManager::assumeInclusiveRangeDual(ProgramStateRef State, NonLoc Value, 89 const llvm::APSInt &From, 90 const llvm::APSInt &To) { 91 auto AssumeFun = [&](bool Assumption) { 92 return assumeInclusiveRangeInternal(State, Value, From, To, Assumption); 93 }; 94 return assumeDualImpl(State, AssumeFun); 95 } 96 97 ProgramStateRef ConstraintManager::assume(ProgramStateRef State, 98 DefinedSVal Cond, bool Assumption) { 99 ConstraintManager::ProgramStatePair R = assumeDual(State, Cond); 100 return Assumption ? R.first : R.second; 101 } 102 103 ProgramStateRef 104 ConstraintManager::assumeInclusiveRange(ProgramStateRef State, NonLoc Value, 105 const llvm::APSInt &From, 106 const llvm::APSInt &To, bool InBound) { 107 ConstraintManager::ProgramStatePair R = 108 assumeInclusiveRangeDual(State, Value, From, To); 109 return InBound ? R.first : R.second; 110 } 111