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 assumeInclusiveRange(ProgramStateRef State, 103 NonLoc Value, 104 const llvm::APSInt &From, 105 const llvm::APSInt &To, 106 bool InBound) = 0; 107 108 virtual ProgramStatePair assumeInclusiveRangeDual(ProgramStateRef State, 109 NonLoc Value, 110 const llvm::APSInt &From, 111 const llvm::APSInt &To) { 112 ProgramStateRef StInRange = 113 assumeInclusiveRange(State, Value, From, To, true); 114 115 // If StTrue is infeasible, asserting the falseness of Cond is unnecessary 116 // because the existing constraints already establish this. 117 if (!StInRange) 118 return ProgramStatePair((ProgramStateRef)nullptr, State); 119 120 ProgramStateRef StOutOfRange = 121 assumeInclusiveRange(State, Value, From, To, false); 122 if (!StOutOfRange) { 123 // We are careful to return the original state, /not/ StTrue, 124 // because we want to avoid having callers generate a new node 125 // in the ExplodedGraph. 126 return ProgramStatePair(State, (ProgramStateRef)nullptr); 127 } 128 129 return ProgramStatePair(StInRange, StOutOfRange); 130 } 131 132 /// \brief If a symbol is perfectly constrained to a constant, attempt 133 /// to return the concrete value. 134 /// 135 /// Note that a ConstraintManager is not obligated to return a concretized 136 /// value for a symbol, even if it is perfectly constrained. 137 virtual const llvm::APSInt* getSymVal(ProgramStateRef state, 138 SymbolRef sym) const { 139 return nullptr; 140 } 141 142 /// Scan all symbols referenced by the constraints. If the symbol is not 143 /// alive, remove it. 144 virtual ProgramStateRef removeDeadBindings(ProgramStateRef state, 145 SymbolReaper& SymReaper) = 0; 146 147 virtual void print(ProgramStateRef state, 148 raw_ostream &Out, 149 const char* nl, 150 const char *sep) = 0; 151 152 virtual void EndPath(ProgramStateRef state) {} 153 154 /// Convenience method to query the state to see if a symbol is null or 155 /// not null, or if neither assumption can be made. 156 ConditionTruthVal isNull(ProgramStateRef State, SymbolRef Sym) { 157 SaveAndRestore<bool> DisableNotify(NotifyAssumeClients, false); 158 159 return checkNull(State, Sym); 160 } 161 162 protected: 163 /// A flag to indicate that clients should be notified of assumptions. 164 /// By default this is the case, but sometimes this needs to be restricted 165 /// to avoid infinite recursions within the ConstraintManager. 166 /// 167 /// Note that this flag allows the ConstraintManager to be re-entrant, 168 /// but not thread-safe. 169 bool NotifyAssumeClients; 170 171 /// canReasonAbout - Not all ConstraintManagers can accurately reason about 172 /// all SVal values. This method returns true if the ConstraintManager can 173 /// reasonably handle a given SVal value. This is typically queried by 174 /// ExprEngine to determine if the value should be replaced with a 175 /// conjured symbolic value in order to recover some precision. 176 virtual bool canReasonAbout(SVal X) const = 0; 177 178 /// Returns whether or not a symbol is known to be null ("true"), known to be 179 /// non-null ("false"), or may be either ("underconstrained"). 180 virtual ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym); 181 }; 182 183 std::unique_ptr<ConstraintManager> 184 CreateRangeConstraintManager(ProgramStateManager &statemgr, 185 SubEngine *subengine); 186 187 std::unique_ptr<ConstraintManager> 188 CreateZ3ConstraintManager(ProgramStateManager &statemgr, SubEngine *subengine); 189 190 } // end GR namespace 191 192 } // end clang namespace 193 194 #endif 195
