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_GR_CONSTRAINT_MANAGER_H 15 #define LLVM_CLANG_GR_CONSTRAINT_MANAGER_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. ConditionTruthVal(bool constraint)35 ConditionTruthVal(bool constraint) : Val(constraint) {} 36 37 /// Construct a ConstraintVal indicating the constraint is underconstrained. ConditionTruthVal()38 ConditionTruthVal() {} 39 40 /// Return true if the constraint is perfectly constrained to 'true'. isConstrainedTrue()41 bool isConstrainedTrue() const { 42 return Val.hasValue() && Val.getValue(); 43 } 44 45 /// Return true if the constraint is perfectly constrained to 'false'. isConstrainedFalse()46 bool isConstrainedFalse() const { 47 return Val.hasValue() && !Val.getValue(); 48 } 49 50 /// Return true if the constrained is perfectly constrained. isConstrained()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. isUnderconstrained()57 bool isUnderconstrained() const { 58 return !Val.hasValue(); 59 } 60 }; 61 62 class ConstraintManager { 63 public: ConstraintManager()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. assumeDual(ProgramStateRef State,DefinedSVal Cond)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)NULL, 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)NULL); 97 } 98 99 return ProgramStatePair(StTrue, StFalse); 100 } 101 102 /// \brief If a symbol is perfectly constrained to a constant, attempt 103 /// to return the concrete value. 104 /// 105 /// Note that a ConstraintManager is not obligated to return a concretized 106 /// value for a symbol, even if it is perfectly constrained. getSymVal(ProgramStateRef state,SymbolRef sym)107 virtual const llvm::APSInt* getSymVal(ProgramStateRef state, 108 SymbolRef sym) const { 109 return 0; 110 } 111 112 virtual ProgramStateRef removeDeadBindings(ProgramStateRef state, 113 SymbolReaper& SymReaper) = 0; 114 115 virtual void print(ProgramStateRef state, 116 raw_ostream &Out, 117 const char* nl, 118 const char *sep) = 0; 119 EndPath(ProgramStateRef state)120 virtual void EndPath(ProgramStateRef state) {} 121 122 /// Convenience method to query the state to see if a symbol is null or 123 /// not null, or if neither assumption can be made. isNull(ProgramStateRef State,SymbolRef Sym)124 ConditionTruthVal isNull(ProgramStateRef State, SymbolRef Sym) { 125 SaveAndRestore<bool> DisableNotify(NotifyAssumeClients, false); 126 127 return checkNull(State, Sym); 128 } 129 130 protected: 131 /// A flag to indicate that clients should be notified of assumptions. 132 /// By default this is the case, but sometimes this needs to be restricted 133 /// to avoid infinite recursions within the ConstraintManager. 134 /// 135 /// Note that this flag allows the ConstraintManager to be re-entrant, 136 /// but not thread-safe. 137 bool NotifyAssumeClients; 138 139 /// canReasonAbout - Not all ConstraintManagers can accurately reason about 140 /// all SVal values. This method returns true if the ConstraintManager can 141 /// reasonably handle a given SVal value. This is typically queried by 142 /// ExprEngine to determine if the value should be replaced with a 143 /// conjured symbolic value in order to recover some precision. 144 virtual bool canReasonAbout(SVal X) const = 0; 145 146 /// Returns whether or not a symbol is known to be null ("true"), known to be 147 /// non-null ("false"), or may be either ("underconstrained"). 148 virtual ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym); 149 }; 150 151 ConstraintManager* CreateRangeConstraintManager(ProgramStateManager& statemgr, 152 SubEngine *subengine); 153 154 } // end GR namespace 155 156 } // end clang namespace 157 158 #endif 159