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/SymbolManager.h" 18 #include "clang/StaticAnalyzer/Core/PathSensitive/SVals.h" 19 20 namespace llvm { 21 class APSInt; 22 } 23 24 namespace clang { 25 namespace ento { 26 27 class SubEngine; 28 29 class ConditionTruthVal { 30 llvm::Optional<bool> Val; 31 public: 32 /// Construct a ConditionTruthVal indicating the constraint is constrained 33 /// to either true or false, depending on the boolean value provided. ConditionTruthVal(bool constraint)34 ConditionTruthVal(bool constraint) : Val(constraint) {} 35 36 /// Construct a ConstraintVal indicating the constraint is underconstrained. ConditionTruthVal()37 ConditionTruthVal() {} 38 39 /// Return true if the constraint is perfectly constrained to 'true'. isTrue()40 bool isTrue() const { 41 return Val.hasValue() && Val.getValue(); 42 } 43 44 /// Return true if the constraint is perfectly constrained to 'false'. isFalse()45 bool isFalse() const { 46 return Val.hasValue() && !Val.getValue(); 47 } 48 49 /// Return true if the constrained is perfectly constrained. isConstrained()50 bool isConstrained() const { 51 return Val.hasValue(); 52 } 53 54 /// Return true if the constrained is underconstrained and we do not know 55 /// if the constraint is true of value. isUnderconstrained()56 bool isUnderconstrained() const { 57 return !Val.hasValue(); 58 } 59 }; 60 61 class ConstraintManager { 62 public: ConstraintManager()63 ConstraintManager() : NotifyAssumeClients(true) {} 64 65 virtual ~ConstraintManager(); 66 virtual ProgramStateRef assume(ProgramStateRef state, 67 DefinedSVal Cond, 68 bool Assumption) = 0; 69 70 typedef std::pair<ProgramStateRef, ProgramStateRef> ProgramStatePair; 71 assumeDual(ProgramStateRef state,DefinedSVal Cond)72 ProgramStatePair assumeDual(ProgramStateRef state, DefinedSVal Cond) { 73 ProgramStatePair res(assume(state, Cond, true), 74 assume(state, Cond, false)); 75 assert(!(!res.first && !res.second) && "System is over constrained."); 76 return res; 77 } 78 79 /// \brief If a symbol is perfectly constrained to a constant, attempt 80 /// to return the concrete value. 81 /// 82 /// Note that a ConstraintManager is not obligated to return a concretized 83 /// value for a symbol, even if it is perfectly constrained. getSymVal(ProgramStateRef state,SymbolRef sym)84 virtual const llvm::APSInt* getSymVal(ProgramStateRef state, 85 SymbolRef sym) const { 86 return 0; 87 } 88 89 virtual ProgramStateRef removeDeadBindings(ProgramStateRef state, 90 SymbolReaper& SymReaper) = 0; 91 92 virtual void print(ProgramStateRef state, 93 raw_ostream &Out, 94 const char* nl, 95 const char *sep) = 0; 96 EndPath(ProgramStateRef state)97 virtual void EndPath(ProgramStateRef state) {} 98 99 /// Convenience method to query the state to see if a symbol is null or 100 /// not null, or neither assumption can be made. 101 ConditionTruthVal isNull(ProgramStateRef State, SymbolRef Sym); 102 103 protected: 104 /// A flag to indicate that clients should be notified of assumptions. 105 /// By default this is the case, but sometimes this needs to be restricted 106 /// to avoid infinite recursions within the ConstraintManager. 107 /// 108 /// Note that this flag allows the ConstraintManager to be re-entrant, 109 /// but not thread-safe. 110 bool NotifyAssumeClients; 111 112 /// canReasonAbout - Not all ConstraintManagers can accurately reason about 113 /// all SVal values. This method returns true if the ConstraintManager can 114 /// reasonably handle a given SVal value. This is typically queried by 115 /// ExprEngine to determine if the value should be replaced with a 116 /// conjured symbolic value in order to recover some precision. 117 virtual bool canReasonAbout(SVal X) const = 0; 118 }; 119 120 ConstraintManager* CreateRangeConstraintManager(ProgramStateManager& statemgr, 121 SubEngine &subengine); 122 123 } // end GR namespace 124 125 } // end clang namespace 126 127 #endif 128