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 SubEngine; 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 #ifndef __OPTIMIZE__ 100 // This check is expensive and should be disabled even in Release+Asserts 101 // builds. 102 // FIXME: __OPTIMIZE__ is a GNU extension that Clang implements but MSVC 103 // does not. Is there a good equivalent there? 104 assert(assume(State, Cond, false) && "System is over constrained."); 105 #endif 106 return ProgramStatePair((ProgramStateRef)nullptr, State); 107 } 108 109 ProgramStateRef StFalse = assume(State, Cond, false); 110 if (!StFalse) { 111 // We are careful to return the original state, /not/ StTrue, 112 // because we want to avoid having callers generate a new node 113 // in the ExplodedGraph. 114 return ProgramStatePair(State, (ProgramStateRef)nullptr); 115 } 116 117 return ProgramStatePair(StTrue, StFalse); 118 } 119 120 virtual ProgramStateRef assumeInclusiveRange(ProgramStateRef State, 121 NonLoc Value, 122 const llvm::APSInt &From, 123 const llvm::APSInt &To, 124 bool InBound) = 0; 125 126 virtual ProgramStatePair assumeInclusiveRangeDual(ProgramStateRef State, 127 NonLoc Value, 128 const llvm::APSInt &From, 129 const llvm::APSInt &To) { 130 ProgramStateRef StInRange = 131 assumeInclusiveRange(State, Value, From, To, true); 132 133 // If StTrue is infeasible, asserting the falseness of Cond is unnecessary 134 // because the existing constraints already establish this. 135 if (!StInRange) 136 return ProgramStatePair((ProgramStateRef)nullptr, State); 137 138 ProgramStateRef StOutOfRange = 139 assumeInclusiveRange(State, Value, From, To, false); 140 if (!StOutOfRange) { 141 // We are careful to return the original state, /not/ StTrue, 142 // because we want to avoid having callers generate a new node 143 // in the ExplodedGraph. 144 return ProgramStatePair(State, (ProgramStateRef)nullptr); 145 } 146 147 return ProgramStatePair(StInRange, StOutOfRange); 148 } 149 150 /// If a symbol is perfectly constrained to a constant, attempt 151 /// to return the concrete value. 152 /// 153 /// Note that a ConstraintManager is not obligated to return a concretized 154 /// value for a symbol, even if it is perfectly constrained. 155 virtual const llvm::APSInt* getSymVal(ProgramStateRef state, 156 SymbolRef sym) const { 157 return nullptr; 158 } 159 160 /// Scan all symbols referenced by the constraints. If the symbol is not 161 /// alive, remove it. 162 virtual ProgramStateRef removeDeadBindings(ProgramStateRef state, 163 SymbolReaper& SymReaper) = 0; 164 165 virtual void printJson(raw_ostream &Out, ProgramStateRef State, 166 const char *NL, unsigned int Space, 167 bool IsDot) const = 0; 168 169 /// Convenience method to query the state to see if a symbol is null or 170 /// not null, or if neither assumption can be made. 171 ConditionTruthVal isNull(ProgramStateRef State, SymbolRef Sym) { 172 SaveAndRestore<bool> DisableNotify(NotifyAssumeClients, false); 173 174 return checkNull(State, Sym); 175 } 176 177 protected: 178 /// A flag to indicate that clients should be notified of assumptions. 179 /// By default this is the case, but sometimes this needs to be restricted 180 /// to avoid infinite recursions within the ConstraintManager. 181 /// 182 /// Note that this flag allows the ConstraintManager to be re-entrant, 183 /// but not thread-safe. 184 bool NotifyAssumeClients = true; 185 186 /// canReasonAbout - Not all ConstraintManagers can accurately reason about 187 /// all SVal values. This method returns true if the ConstraintManager can 188 /// reasonably handle a given SVal value. This is typically queried by 189 /// ExprEngine to determine if the value should be replaced with a 190 /// conjured symbolic value in order to recover some precision. 191 virtual bool canReasonAbout(SVal X) const = 0; 192 193 /// Returns whether or not a symbol is known to be null ("true"), known to be 194 /// non-null ("false"), or may be either ("underconstrained"). 195 virtual ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym); 196 }; 197 198 std::unique_ptr<ConstraintManager> 199 CreateRangeConstraintManager(ProgramStateManager &statemgr, 200 SubEngine *subengine); 201 202 std::unique_ptr<ConstraintManager> 203 CreateZ3ConstraintManager(ProgramStateManager &statemgr, SubEngine *subengine); 204 205 } // namespace ento 206 } // namespace clang 207 208 #endif // LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_CONSTRAINTMANAGER_H 209