1 //===- ConstraintManager.h - Constraints on symbolic values. ----*- C++ -*-===// 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 #ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_CONSTRAINTMANAGER_H 14 #define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_CONSTRAINTMANAGER_H 15 16 #include "clang/Basic/LLVM.h" 17 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState_Fwd.h" 18 #include "clang/StaticAnalyzer/Core/PathSensitive/SVals.h" 19 #include "clang/StaticAnalyzer/Core/PathSensitive/SymExpr.h" 20 #include "llvm/Support/SaveAndRestore.h" 21 #include <memory> 22 #include <optional> 23 #include <utility> 24 25 namespace llvm { 26 27 class APSInt; 28 29 } // namespace llvm 30 31 namespace clang { 32 namespace ento { 33 34 class ProgramStateManager; 35 class ExprEngine; 36 class SymbolReaper; 37 38 class ConditionTruthVal { 39 std::optional<bool> Val; 40 41 public: 42 /// Construct a ConditionTruthVal indicating the constraint is constrained 43 /// to either true or false, depending on the boolean value provided. ConditionTruthVal(bool constraint)44 ConditionTruthVal(bool constraint) : Val(constraint) {} 45 46 /// Construct a ConstraintVal indicating the constraint is underconstrained. 47 ConditionTruthVal() = default; 48 49 /// \return Stored value, assuming that the value is known. 50 /// Crashes otherwise. getValue()51 bool getValue() const { 52 return *Val; 53 } 54 55 /// Return true if the constraint is perfectly constrained to 'true'. isConstrainedTrue()56 bool isConstrainedTrue() const { return Val && *Val; } 57 58 /// Return true if the constraint is perfectly constrained to 'false'. isConstrainedFalse()59 bool isConstrainedFalse() const { return Val && !*Val; } 60 61 /// Return true if the constrained is perfectly constrained. isConstrained()62 bool isConstrained() const { return Val.has_value(); } 63 64 /// Return true if the constrained is underconstrained and we do not know 65 /// if the constraint is true of value. isUnderconstrained()66 bool isUnderconstrained() const { return !Val.has_value(); } 67 }; 68 69 class ConstraintManager { 70 public: 71 ConstraintManager() = default; 72 virtual ~ConstraintManager(); 73 74 virtual bool haveEqualConstraints(ProgramStateRef S1, 75 ProgramStateRef S2) const = 0; 76 77 ProgramStateRef assume(ProgramStateRef state, DefinedSVal Cond, 78 bool Assumption); 79 80 using ProgramStatePair = std::pair<ProgramStateRef, ProgramStateRef>; 81 82 /// Returns a pair of states (StTrue, StFalse) where the given condition is 83 /// assumed to be true or false, respectively. 84 /// (Note that these two states might be equal if the parent state turns out 85 /// to be infeasible. This may happen if the underlying constraint solver is 86 /// not perfectly precise and this may happen very rarely.) 87 ProgramStatePair assumeDual(ProgramStateRef State, DefinedSVal Cond); 88 89 ProgramStateRef assumeInclusiveRange(ProgramStateRef State, NonLoc Value, 90 const llvm::APSInt &From, 91 const llvm::APSInt &To, bool InBound); 92 93 /// Returns a pair of states (StInRange, StOutOfRange) where the given value 94 /// is assumed to be in the range or out of the range, respectively. 95 /// (Note that these two states might be equal if the parent state turns out 96 /// to be infeasible. This may happen if the underlying constraint solver is 97 /// not perfectly precise and this may happen very rarely.) 98 ProgramStatePair assumeInclusiveRangeDual(ProgramStateRef State, NonLoc Value, 99 const llvm::APSInt &From, 100 const llvm::APSInt &To); 101 102 /// 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. 107 /// It might return null. getSymVal(ProgramStateRef state,SymbolRef sym)108 virtual const llvm::APSInt* getSymVal(ProgramStateRef state, 109 SymbolRef sym) const { 110 return nullptr; 111 } 112 113 /// Attempt to return the minimal possible value for a given symbol. Note 114 /// that a ConstraintManager is not obligated to return a lower bound, it may 115 /// also return nullptr. getSymMinVal(ProgramStateRef state,SymbolRef sym)116 virtual const llvm::APSInt *getSymMinVal(ProgramStateRef state, 117 SymbolRef sym) const { 118 return nullptr; 119 } 120 121 /// Attempt to return the minimal possible value for a given symbol. Note 122 /// that a ConstraintManager is not obligated to return a lower bound, it may 123 /// also return nullptr. getSymMaxVal(ProgramStateRef state,SymbolRef sym)124 virtual const llvm::APSInt *getSymMaxVal(ProgramStateRef state, 125 SymbolRef sym) const { 126 return nullptr; 127 } 128 129 /// Scan all symbols referenced by the constraints. If the symbol is not 130 /// alive, remove it. 131 virtual ProgramStateRef removeDeadBindings(ProgramStateRef state, 132 SymbolReaper& SymReaper) = 0; 133 134 virtual void printJson(raw_ostream &Out, ProgramStateRef State, 135 const char *NL, unsigned int Space, 136 bool IsDot) const = 0; 137 printValue(raw_ostream & Out,ProgramStateRef State,SymbolRef Sym)138 virtual void printValue(raw_ostream &Out, ProgramStateRef State, 139 SymbolRef Sym) {} 140 141 /// Convenience method to query the state to see if a symbol is null or 142 /// not null, or if neither assumption can be made. isNull(ProgramStateRef State,SymbolRef Sym)143 ConditionTruthVal isNull(ProgramStateRef State, SymbolRef Sym) { 144 return checkNull(State, Sym); 145 } 146 147 protected: 148 /// A helper class to simulate the call stack of nested assume calls. 149 class AssumeStackTy { 150 public: push(const ProgramState * S)151 void push(const ProgramState *S) { Aux.push_back(S); } pop()152 void pop() { Aux.pop_back(); } contains(const ProgramState * S)153 bool contains(const ProgramState *S) const { 154 return llvm::is_contained(Aux, S); 155 } 156 157 private: 158 llvm::SmallVector<const ProgramState *, 4> Aux; 159 }; 160 AssumeStackTy AssumeStack; 161 162 virtual ProgramStateRef assumeInternal(ProgramStateRef state, 163 DefinedSVal Cond, bool Assumption) = 0; 164 165 virtual ProgramStateRef assumeInclusiveRangeInternal(ProgramStateRef State, 166 NonLoc Value, 167 const llvm::APSInt &From, 168 const llvm::APSInt &To, 169 bool InBound) = 0; 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 template <typename AssumeFunction> 183 ProgramStatePair assumeDualImpl(ProgramStateRef &State, 184 AssumeFunction &Assume); 185 }; 186 187 std::unique_ptr<ConstraintManager> 188 CreateRangeConstraintManager(ProgramStateManager &statemgr, 189 ExprEngine *exprengine); 190 191 std::unique_ptr<ConstraintManager> 192 CreateZ3ConstraintManager(ProgramStateManager &statemgr, 193 ExprEngine *exprengine); 194 195 } // namespace ento 196 } // namespace clang 197 198 #endif // LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_CONSTRAINTMANAGER_H 199