1f4a2713aSLionel Sambuc //== ConstraintManager.h - Constraints on symbolic values.-------*- C++ -*--==// 2f4a2713aSLionel Sambuc // 3f4a2713aSLionel Sambuc // The LLVM Compiler Infrastructure 4f4a2713aSLionel Sambuc // 5f4a2713aSLionel Sambuc // This file is distributed under the University of Illinois Open Source 6f4a2713aSLionel Sambuc // License. See LICENSE.TXT for details. 7f4a2713aSLionel Sambuc // 8f4a2713aSLionel Sambuc //===----------------------------------------------------------------------===// 9f4a2713aSLionel Sambuc // 10f4a2713aSLionel Sambuc // This file defined the interface to manage constraints on symbolic values. 11f4a2713aSLionel Sambuc // 12f4a2713aSLionel Sambuc //===----------------------------------------------------------------------===// 13f4a2713aSLionel Sambuc 14*0a6a1f1dSLionel Sambuc #ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_CONSTRAINTMANAGER_H 15*0a6a1f1dSLionel Sambuc #define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_CONSTRAINTMANAGER_H 16f4a2713aSLionel Sambuc 17f4a2713aSLionel Sambuc #include "clang/StaticAnalyzer/Core/PathSensitive/SVals.h" 18f4a2713aSLionel Sambuc #include "clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h" 19f4a2713aSLionel Sambuc #include "llvm/Support/SaveAndRestore.h" 20f4a2713aSLionel Sambuc 21f4a2713aSLionel Sambuc namespace llvm { 22f4a2713aSLionel Sambuc class APSInt; 23f4a2713aSLionel Sambuc } 24f4a2713aSLionel Sambuc 25f4a2713aSLionel Sambuc namespace clang { 26f4a2713aSLionel Sambuc namespace ento { 27f4a2713aSLionel Sambuc 28f4a2713aSLionel Sambuc class SubEngine; 29f4a2713aSLionel Sambuc 30f4a2713aSLionel Sambuc class ConditionTruthVal { 31f4a2713aSLionel Sambuc Optional<bool> Val; 32f4a2713aSLionel Sambuc public: 33f4a2713aSLionel Sambuc /// Construct a ConditionTruthVal indicating the constraint is constrained 34f4a2713aSLionel Sambuc /// to either true or false, depending on the boolean value provided. ConditionTruthVal(bool constraint)35f4a2713aSLionel Sambuc ConditionTruthVal(bool constraint) : Val(constraint) {} 36f4a2713aSLionel Sambuc 37f4a2713aSLionel Sambuc /// Construct a ConstraintVal indicating the constraint is underconstrained. ConditionTruthVal()38f4a2713aSLionel Sambuc ConditionTruthVal() {} 39f4a2713aSLionel Sambuc 40f4a2713aSLionel Sambuc /// Return true if the constraint is perfectly constrained to 'true'. isConstrainedTrue()41f4a2713aSLionel Sambuc bool isConstrainedTrue() const { 42f4a2713aSLionel Sambuc return Val.hasValue() && Val.getValue(); 43f4a2713aSLionel Sambuc } 44f4a2713aSLionel Sambuc 45f4a2713aSLionel Sambuc /// Return true if the constraint is perfectly constrained to 'false'. isConstrainedFalse()46f4a2713aSLionel Sambuc bool isConstrainedFalse() const { 47f4a2713aSLionel Sambuc return Val.hasValue() && !Val.getValue(); 48f4a2713aSLionel Sambuc } 49f4a2713aSLionel Sambuc 50f4a2713aSLionel Sambuc /// Return true if the constrained is perfectly constrained. isConstrained()51f4a2713aSLionel Sambuc bool isConstrained() const { 52f4a2713aSLionel Sambuc return Val.hasValue(); 53f4a2713aSLionel Sambuc } 54f4a2713aSLionel Sambuc 55f4a2713aSLionel Sambuc /// Return true if the constrained is underconstrained and we do not know 56f4a2713aSLionel Sambuc /// if the constraint is true of value. isUnderconstrained()57f4a2713aSLionel Sambuc bool isUnderconstrained() const { 58f4a2713aSLionel Sambuc return !Val.hasValue(); 59f4a2713aSLionel Sambuc } 60f4a2713aSLionel Sambuc }; 61f4a2713aSLionel Sambuc 62f4a2713aSLionel Sambuc class ConstraintManager { 63f4a2713aSLionel Sambuc public: ConstraintManager()64f4a2713aSLionel Sambuc ConstraintManager() : NotifyAssumeClients(true) {} 65f4a2713aSLionel Sambuc 66f4a2713aSLionel Sambuc virtual ~ConstraintManager(); 67f4a2713aSLionel Sambuc virtual ProgramStateRef assume(ProgramStateRef state, 68f4a2713aSLionel Sambuc DefinedSVal Cond, 69f4a2713aSLionel Sambuc bool Assumption) = 0; 70f4a2713aSLionel Sambuc 71f4a2713aSLionel Sambuc typedef std::pair<ProgramStateRef, ProgramStateRef> ProgramStatePair; 72f4a2713aSLionel Sambuc 73f4a2713aSLionel Sambuc /// Returns a pair of states (StTrue, StFalse) where the given condition is 74f4a2713aSLionel Sambuc /// assumed to be true or false, respectively. assumeDual(ProgramStateRef State,DefinedSVal Cond)75f4a2713aSLionel Sambuc ProgramStatePair assumeDual(ProgramStateRef State, DefinedSVal Cond) { 76f4a2713aSLionel Sambuc ProgramStateRef StTrue = assume(State, Cond, true); 77f4a2713aSLionel Sambuc 78f4a2713aSLionel Sambuc // If StTrue is infeasible, asserting the falseness of Cond is unnecessary 79f4a2713aSLionel Sambuc // because the existing constraints already establish this. 80f4a2713aSLionel Sambuc if (!StTrue) { 81f4a2713aSLionel Sambuc #ifndef __OPTIMIZE__ 82f4a2713aSLionel Sambuc // This check is expensive and should be disabled even in Release+Asserts 83f4a2713aSLionel Sambuc // builds. 84f4a2713aSLionel Sambuc // FIXME: __OPTIMIZE__ is a GNU extension that Clang implements but MSVC 85f4a2713aSLionel Sambuc // does not. Is there a good equivalent there? 86f4a2713aSLionel Sambuc assert(assume(State, Cond, false) && "System is over constrained."); 87f4a2713aSLionel Sambuc #endif 88*0a6a1f1dSLionel Sambuc return ProgramStatePair((ProgramStateRef)nullptr, State); 89f4a2713aSLionel Sambuc } 90f4a2713aSLionel Sambuc 91f4a2713aSLionel Sambuc ProgramStateRef StFalse = assume(State, Cond, false); 92f4a2713aSLionel Sambuc if (!StFalse) { 93f4a2713aSLionel Sambuc // We are careful to return the original state, /not/ StTrue, 94f4a2713aSLionel Sambuc // because we want to avoid having callers generate a new node 95f4a2713aSLionel Sambuc // in the ExplodedGraph. 96*0a6a1f1dSLionel Sambuc return ProgramStatePair(State, (ProgramStateRef)nullptr); 97f4a2713aSLionel Sambuc } 98f4a2713aSLionel Sambuc 99f4a2713aSLionel Sambuc return ProgramStatePair(StTrue, StFalse); 100f4a2713aSLionel Sambuc } 101f4a2713aSLionel Sambuc 102f4a2713aSLionel Sambuc /// \brief If a symbol is perfectly constrained to a constant, attempt 103f4a2713aSLionel Sambuc /// to return the concrete value. 104f4a2713aSLionel Sambuc /// 105f4a2713aSLionel Sambuc /// Note that a ConstraintManager is not obligated to return a concretized 106f4a2713aSLionel Sambuc /// value for a symbol, even if it is perfectly constrained. getSymVal(ProgramStateRef state,SymbolRef sym)107f4a2713aSLionel Sambuc virtual const llvm::APSInt* getSymVal(ProgramStateRef state, 108f4a2713aSLionel Sambuc SymbolRef sym) const { 109*0a6a1f1dSLionel Sambuc return nullptr; 110f4a2713aSLionel Sambuc } 111f4a2713aSLionel Sambuc 112f4a2713aSLionel Sambuc virtual ProgramStateRef removeDeadBindings(ProgramStateRef state, 113f4a2713aSLionel Sambuc SymbolReaper& SymReaper) = 0; 114f4a2713aSLionel Sambuc 115f4a2713aSLionel Sambuc virtual void print(ProgramStateRef state, 116f4a2713aSLionel Sambuc raw_ostream &Out, 117f4a2713aSLionel Sambuc const char* nl, 118f4a2713aSLionel Sambuc const char *sep) = 0; 119f4a2713aSLionel Sambuc EndPath(ProgramStateRef state)120f4a2713aSLionel Sambuc virtual void EndPath(ProgramStateRef state) {} 121f4a2713aSLionel Sambuc 122f4a2713aSLionel Sambuc /// Convenience method to query the state to see if a symbol is null or 123f4a2713aSLionel Sambuc /// not null, or if neither assumption can be made. isNull(ProgramStateRef State,SymbolRef Sym)124f4a2713aSLionel Sambuc ConditionTruthVal isNull(ProgramStateRef State, SymbolRef Sym) { 125f4a2713aSLionel Sambuc SaveAndRestore<bool> DisableNotify(NotifyAssumeClients, false); 126f4a2713aSLionel Sambuc 127f4a2713aSLionel Sambuc return checkNull(State, Sym); 128f4a2713aSLionel Sambuc } 129f4a2713aSLionel Sambuc 130f4a2713aSLionel Sambuc protected: 131f4a2713aSLionel Sambuc /// A flag to indicate that clients should be notified of assumptions. 132f4a2713aSLionel Sambuc /// By default this is the case, but sometimes this needs to be restricted 133f4a2713aSLionel Sambuc /// to avoid infinite recursions within the ConstraintManager. 134f4a2713aSLionel Sambuc /// 135f4a2713aSLionel Sambuc /// Note that this flag allows the ConstraintManager to be re-entrant, 136f4a2713aSLionel Sambuc /// but not thread-safe. 137f4a2713aSLionel Sambuc bool NotifyAssumeClients; 138f4a2713aSLionel Sambuc 139f4a2713aSLionel Sambuc /// canReasonAbout - Not all ConstraintManagers can accurately reason about 140f4a2713aSLionel Sambuc /// all SVal values. This method returns true if the ConstraintManager can 141f4a2713aSLionel Sambuc /// reasonably handle a given SVal value. This is typically queried by 142f4a2713aSLionel Sambuc /// ExprEngine to determine if the value should be replaced with a 143f4a2713aSLionel Sambuc /// conjured symbolic value in order to recover some precision. 144f4a2713aSLionel Sambuc virtual bool canReasonAbout(SVal X) const = 0; 145f4a2713aSLionel Sambuc 146f4a2713aSLionel Sambuc /// Returns whether or not a symbol is known to be null ("true"), known to be 147f4a2713aSLionel Sambuc /// non-null ("false"), or may be either ("underconstrained"). 148f4a2713aSLionel Sambuc virtual ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym); 149f4a2713aSLionel Sambuc }; 150f4a2713aSLionel Sambuc 151*0a6a1f1dSLionel Sambuc std::unique_ptr<ConstraintManager> 152*0a6a1f1dSLionel Sambuc CreateRangeConstraintManager(ProgramStateManager &statemgr, 153f4a2713aSLionel Sambuc SubEngine *subengine); 154f4a2713aSLionel Sambuc 155f4a2713aSLionel Sambuc } // end GR namespace 156f4a2713aSLionel Sambuc 157f4a2713aSLionel Sambuc } // end clang namespace 158f4a2713aSLionel Sambuc 159f4a2713aSLionel Sambuc #endif 160