1 //== ConstraintManager.h - Constraints on symbolic values.-------*- 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 // This file defined the interface to manage constraints on symbolic values. 11 // 12 //===----------------------------------------------------------------------===// 13 14 #ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_CONSTRAINTMANAGER_H 15 #define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_CONSTRAINTMANAGER_H 16 17 #include "clang/StaticAnalyzer/Core/PathSensitive/SVals.h" 18 #include "clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h" 19 #include "llvm/Support/SaveAndRestore.h" 20 21 namespace llvm { 22 class APSInt; 23 } 24 25 namespace clang { 26 namespace ento { 27 28 class SubEngine; 29 30 class ConditionTruthVal { 31 Optional<bool> Val; 32 public: 33 /// Construct a ConditionTruthVal indicating the constraint is constrained 34 /// to either true or false, depending on the boolean value provided. 35 ConditionTruthVal(bool constraint) : Val(constraint) {} 36 37 /// Construct a ConstraintVal indicating the constraint is underconstrained. 38 ConditionTruthVal() {} 39 40 /// Return true if the constraint is perfectly constrained to 'true'. 41 bool isConstrainedTrue() const { 42 return Val.hasValue() && Val.getValue(); 43 } 44 45 /// Return true if the constraint is perfectly constrained to 'false'. 46 bool isConstrainedFalse() const { 47 return Val.hasValue() && !Val.getValue(); 48 } 49 50 /// Return true if the constrained is perfectly constrained. 51 bool isConstrained() const { 52 return Val.hasValue(); 53 } 54 55 /// Return true if the constrained is underconstrained and we do not know 56 /// if the constraint is true of value. 57 bool isUnderconstrained() const { 58 return !Val.hasValue(); 59 } 60 }; 61 62 class ConstraintManager { 63 public: 64 ConstraintManager() : NotifyAssumeClients(true) {} 65 66 virtual ~ConstraintManager(); 67 virtual ProgramStateRef assume(ProgramStateRef state, 68 DefinedSVal Cond, 69 bool Assumption) = 0; 70 71 typedef std::pair<ProgramStateRef, ProgramStateRef> ProgramStatePair; 72 73 /// Returns a pair of states (StTrue, StFalse) where the given condition is 74 /// assumed to be true or false, respectively. 75 ProgramStatePair assumeDual(ProgramStateRef State, DefinedSVal Cond) { 76 ProgramStateRef StTrue = assume(State, Cond, true); 77 78 // If StTrue is infeasible, asserting the falseness of Cond is unnecessary 79 // because the existing constraints already establish this. 80 if (!StTrue) { 81 #ifndef __OPTIMIZE__ 82 // This check is expensive and should be disabled even in Release+Asserts 83 // builds. 84 // FIXME: __OPTIMIZE__ is a GNU extension that Clang implements but MSVC 85 // does not. Is there a good equivalent there? 86 assert(assume(State, Cond, false) && "System is over constrained."); 87 #endif 88 return ProgramStatePair((ProgramStateRef)nullptr, State); 89 } 90 91 ProgramStateRef StFalse = assume(State, Cond, false); 92 if (!StFalse) { 93 // We are careful to return the original state, /not/ StTrue, 94 // because we want to avoid having callers generate a new node 95 // in the ExplodedGraph. 96 return ProgramStatePair(State, (ProgramStateRef)nullptr); 97 } 98 99 return ProgramStatePair(StTrue, StFalse); 100 } 101 102 virtual ProgramStateRef assumeWithinInclusiveRange(ProgramStateRef State, 103 NonLoc Value, 104 const llvm::APSInt &From, 105 const llvm::APSInt &To, 106 bool InBound) = 0; 107 108 virtual ProgramStatePair assumeWithinInclusiveRangeDual( 109 ProgramStateRef State, NonLoc Value, const llvm::APSInt &From, 110 const llvm::APSInt &To) { 111 ProgramStateRef StInRange = assumeWithinInclusiveRange(State, Value, From, 112 To, true); 113 114 // If StTrue is infeasible, asserting the falseness of Cond is unnecessary 115 // because the existing constraints already establish this. 116 if (!StInRange) 117 return ProgramStatePair((ProgramStateRef)nullptr, State); 118 119 ProgramStateRef StOutOfRange = assumeWithinInclusiveRange(State, Value, 120 From, To, false); 121 if (!StOutOfRange) { 122 // We are careful to return the original state, /not/ StTrue, 123 // because we want to avoid having callers generate a new node 124 // in the ExplodedGraph. 125 return ProgramStatePair(State, (ProgramStateRef)nullptr); 126 } 127 128 return ProgramStatePair(StInRange, StOutOfRange); 129 } 130 131 /// \brief If a symbol is perfectly constrained to a constant, attempt 132 /// to return the concrete value. 133 /// 134 /// Note that a ConstraintManager is not obligated to return a concretized 135 /// value for a symbol, even if it is perfectly constrained. 136 virtual const llvm::APSInt* getSymVal(ProgramStateRef state, 137 SymbolRef sym) const { 138 return nullptr; 139 } 140 141 virtual ProgramStateRef removeDeadBindings(ProgramStateRef state, 142 SymbolReaper& SymReaper) = 0; 143 144 virtual void print(ProgramStateRef state, 145 raw_ostream &Out, 146 const char* nl, 147 const char *sep) = 0; 148 149 virtual void EndPath(ProgramStateRef state) {} 150 151 /// Convenience method to query the state to see if a symbol is null or 152 /// not null, or if neither assumption can be made. 153 ConditionTruthVal isNull(ProgramStateRef State, SymbolRef Sym) { 154 SaveAndRestore<bool> DisableNotify(NotifyAssumeClients, false); 155 156 return checkNull(State, Sym); 157 } 158 159 protected: 160 /// A flag to indicate that clients should be notified of assumptions. 161 /// By default this is the case, but sometimes this needs to be restricted 162 /// to avoid infinite recursions within the ConstraintManager. 163 /// 164 /// Note that this flag allows the ConstraintManager to be re-entrant, 165 /// but not thread-safe. 166 bool NotifyAssumeClients; 167 168 /// canReasonAbout - Not all ConstraintManagers can accurately reason about 169 /// all SVal values. This method returns true if the ConstraintManager can 170 /// reasonably handle a given SVal value. This is typically queried by 171 /// ExprEngine to determine if the value should be replaced with a 172 /// conjured symbolic value in order to recover some precision. 173 virtual bool canReasonAbout(SVal X) const = 0; 174 175 /// Returns whether or not a symbol is known to be null ("true"), known to be 176 /// non-null ("false"), or may be either ("underconstrained"). 177 virtual ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym); 178 }; 179 180 std::unique_ptr<ConstraintManager> 181 CreateRangeConstraintManager(ProgramStateManager &statemgr, 182 SubEngine *subengine); 183 184 } // end GR namespace 185 186 } // end clang namespace 187 188 #endif 189
