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. 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. 51 bool getValue() const { 52 return *Val; 53 } 54 55 /// Return true if the constraint is perfectly constrained to 'true'. 56 bool isConstrainedTrue() const { return Val && *Val; } 57 58 /// Return true if the constraint is perfectly constrained to 'false'. 59 bool isConstrainedFalse() const { return Val && !*Val; } 60 61 /// Return true if the constrained is perfectly constrained. 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. 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. 108 virtual const llvm::APSInt* getSymVal(ProgramStateRef state, 109 SymbolRef sym) const { 110 return nullptr; 111 } 112 113 /// Scan all symbols referenced by the constraints. If the symbol is not 114 /// alive, remove it. 115 virtual ProgramStateRef removeDeadBindings(ProgramStateRef state, 116 SymbolReaper& SymReaper) = 0; 117 118 virtual void printJson(raw_ostream &Out, ProgramStateRef State, 119 const char *NL, unsigned int Space, 120 bool IsDot) const = 0; 121 122 virtual void printValue(raw_ostream &Out, ProgramStateRef State, 123 SymbolRef Sym) {} 124 125 /// Convenience method to query the state to see if a symbol is null or 126 /// not null, or if neither assumption can be made. 127 ConditionTruthVal isNull(ProgramStateRef State, SymbolRef Sym) { 128 return checkNull(State, Sym); 129 } 130 131 protected: 132 /// A helper class to simulate the call stack of nested assume calls. 133 class AssumeStackTy { 134 public: 135 void push(const ProgramState *S) { Aux.push_back(S); } 136 void pop() { Aux.pop_back(); } 137 bool contains(const ProgramState *S) const { 138 return llvm::is_contained(Aux, S); 139 } 140 141 private: 142 llvm::SmallVector<const ProgramState *, 4> Aux; 143 }; 144 AssumeStackTy AssumeStack; 145 146 virtual ProgramStateRef assumeInternal(ProgramStateRef state, 147 DefinedSVal Cond, bool Assumption) = 0; 148 149 virtual ProgramStateRef assumeInclusiveRangeInternal(ProgramStateRef State, 150 NonLoc Value, 151 const llvm::APSInt &From, 152 const llvm::APSInt &To, 153 bool InBound) = 0; 154 155 /// canReasonAbout - Not all ConstraintManagers can accurately reason about 156 /// all SVal values. This method returns true if the ConstraintManager can 157 /// reasonably handle a given SVal value. This is typically queried by 158 /// ExprEngine to determine if the value should be replaced with a 159 /// conjured symbolic value in order to recover some precision. 160 virtual bool canReasonAbout(SVal X) const = 0; 161 162 /// Returns whether or not a symbol is known to be null ("true"), known to be 163 /// non-null ("false"), or may be either ("underconstrained"). 164 virtual ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym); 165 166 template <typename AssumeFunction> 167 ProgramStatePair assumeDualImpl(ProgramStateRef &State, 168 AssumeFunction &Assume); 169 }; 170 171 std::unique_ptr<ConstraintManager> 172 CreateRangeConstraintManager(ProgramStateManager &statemgr, 173 ExprEngine *exprengine); 174 175 std::unique_ptr<ConstraintManager> 176 CreateZ3ConstraintManager(ProgramStateManager &statemgr, 177 ExprEngine *exprengine); 178 179 } // namespace ento 180 } // namespace clang 181 182 #endif // LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_CONSTRAINTMANAGER_H 183