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/ADT/Optional.h" 21 #include "llvm/Support/SaveAndRestore.h" 22 #include <memory> 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 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 { 57 return Val.hasValue() && Val.getValue(); 58 } 59 60 /// Return true if the constraint is perfectly constrained to 'false'. 61 bool isConstrainedFalse() const { 62 return Val.hasValue() && !Val.getValue(); 63 } 64 65 /// Return true if the constrained is perfectly constrained. 66 bool isConstrained() const { 67 return Val.hasValue(); 68 } 69 70 /// Return true if the constrained is underconstrained and we do not know 71 /// if the constraint is true of value. 72 bool isUnderconstrained() const { 73 return !Val.hasValue(); 74 } 75 }; 76 77 class ConstraintManager { 78 public: 79 ConstraintManager() = default; 80 virtual ~ConstraintManager(); 81 82 virtual bool haveEqualConstraints(ProgramStateRef S1, 83 ProgramStateRef S2) const = 0; 84 85 virtual ProgramStateRef assume(ProgramStateRef state, 86 DefinedSVal Cond, 87 bool Assumption) = 0; 88 89 using ProgramStatePair = std::pair<ProgramStateRef, ProgramStateRef>; 90 91 /// Returns a pair of states (StTrue, StFalse) where the given condition is 92 /// assumed to be true or false, respectively. 93 ProgramStatePair assumeDual(ProgramStateRef State, DefinedSVal Cond) { 94 ProgramStateRef StTrue = assume(State, Cond, true); 95 96 // If StTrue is infeasible, asserting the falseness of Cond is unnecessary 97 // because the existing constraints already establish this. 98 if (!StTrue) { 99 #ifdef EXPENSIVE_CHECKS 100 assert(assume(State, Cond, false) && "System is over constrained."); 101 #endif 102 return ProgramStatePair((ProgramStateRef)nullptr, State); 103 } 104 105 ProgramStateRef StFalse = assume(State, Cond, false); 106 if (!StFalse) { 107 // We are careful to return the original state, /not/ StTrue, 108 // because we want to avoid having callers generate a new node 109 // in the ExplodedGraph. 110 return ProgramStatePair(State, (ProgramStateRef)nullptr); 111 } 112 113 return ProgramStatePair(StTrue, StFalse); 114 } 115 116 virtual ProgramStateRef assumeInclusiveRange(ProgramStateRef State, 117 NonLoc Value, 118 const llvm::APSInt &From, 119 const llvm::APSInt &To, 120 bool InBound) = 0; 121 122 virtual ProgramStatePair assumeInclusiveRangeDual(ProgramStateRef State, 123 NonLoc Value, 124 const llvm::APSInt &From, 125 const llvm::APSInt &To) { 126 ProgramStateRef StInRange = 127 assumeInclusiveRange(State, Value, From, To, true); 128 129 // If StTrue is infeasible, asserting the falseness of Cond is unnecessary 130 // because the existing constraints already establish this. 131 if (!StInRange) 132 return ProgramStatePair((ProgramStateRef)nullptr, State); 133 134 ProgramStateRef StOutOfRange = 135 assumeInclusiveRange(State, Value, From, To, false); 136 if (!StOutOfRange) { 137 // We are careful to return the original state, /not/ StTrue, 138 // because we want to avoid having callers generate a new node 139 // in the ExplodedGraph. 140 return ProgramStatePair(State, (ProgramStateRef)nullptr); 141 } 142 143 return ProgramStatePair(StInRange, StOutOfRange); 144 } 145 146 /// If a symbol is perfectly constrained to a constant, attempt 147 /// to return the concrete value. 148 /// 149 /// Note that a ConstraintManager is not obligated to return a concretized 150 /// value for a symbol, even if it is perfectly constrained. 151 virtual const llvm::APSInt* getSymVal(ProgramStateRef state, 152 SymbolRef sym) const { 153 return nullptr; 154 } 155 156 /// Scan all symbols referenced by the constraints. If the symbol is not 157 /// alive, remove it. 158 virtual ProgramStateRef removeDeadBindings(ProgramStateRef state, 159 SymbolReaper& SymReaper) = 0; 160 161 virtual void printJson(raw_ostream &Out, ProgramStateRef State, 162 const char *NL, unsigned int Space, 163 bool IsDot) const = 0; 164 165 /// Convenience method to query the state to see if a symbol is null or 166 /// not null, or if neither assumption can be made. 167 ConditionTruthVal isNull(ProgramStateRef State, SymbolRef Sym) { 168 SaveAndRestore<bool> DisableNotify(NotifyAssumeClients, false); 169 170 return checkNull(State, Sym); 171 } 172 173 protected: 174 /// A flag to indicate that clients should be notified of assumptions. 175 /// By default this is the case, but sometimes this needs to be restricted 176 /// to avoid infinite recursions within the ConstraintManager. 177 /// 178 /// Note that this flag allows the ConstraintManager to be re-entrant, 179 /// but not thread-safe. 180 bool NotifyAssumeClients = true; 181 182 /// canReasonAbout - Not all ConstraintManagers can accurately reason about 183 /// all SVal values. This method returns true if the ConstraintManager can 184 /// reasonably handle a given SVal value. This is typically queried by 185 /// ExprEngine to determine if the value should be replaced with a 186 /// conjured symbolic value in order to recover some precision. 187 virtual bool canReasonAbout(SVal X) const = 0; 188 189 /// Returns whether or not a symbol is known to be null ("true"), known to be 190 /// non-null ("false"), or may be either ("underconstrained"). 191 virtual ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym); 192 }; 193 194 std::unique_ptr<ConstraintManager> 195 CreateRangeConstraintManager(ProgramStateManager &statemgr, 196 ExprEngine *exprengine); 197 198 std::unique_ptr<ConstraintManager> 199 CreateZ3ConstraintManager(ProgramStateManager &statemgr, 200 ExprEngine *exprengine); 201 202 } // namespace ento 203 } // namespace clang 204 205 #endif // LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_CONSTRAINTMANAGER_H 206
Indexes created Tue Jun 09 00:24:00 UTC 2026