1 //== SimpleConstraintManager.h ----------------------------------*- C++ -*--==// 2 // 3 // The LLVM Compiler Infrastructure 4 // 5 // This file is distributed under the University of Illinois Open Source 6 // License. See LICENSE.TXT for details. 7 // 8 //===----------------------------------------------------------------------===// 9 // 10 // Simplified constraint manager backend. 11 // 12 //===----------------------------------------------------------------------===// 13 14 #ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SIMPLECONSTRAINTMANAGER_H 15 #define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SIMPLECONSTRAINTMANAGER_H 16 17 #include "clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h" 18 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h" 19 20 namespace clang { 21 22 namespace ento { 23 24 class SimpleConstraintManager : public ConstraintManager { 25 SubEngine *SU; 26 SValBuilder &SVB; 27 28 public: 29 SimpleConstraintManager(SubEngine *subengine, SValBuilder &SB) 30 : SU(subengine), SVB(SB) {} 31 32 ~SimpleConstraintManager() override; 33 34 //===------------------------------------------------------------------===// 35 // Implementation for interface from ConstraintManager. 36 //===------------------------------------------------------------------===// 37 38 /// Ensures that the DefinedSVal conditional is expressed as a NonLoc by 39 /// creating boolean casts to handle Loc's. 40 ProgramStateRef assume(ProgramStateRef State, DefinedSVal Cond, 41 bool Assumption) override; 42 43 ProgramStateRef assumeInclusiveRange(ProgramStateRef State, NonLoc Value, 44 const llvm::APSInt &From, 45 const llvm::APSInt &To, 46 bool InRange) override; 47 48 protected: 49 //===------------------------------------------------------------------===// 50 // Interface that subclasses must implement. 51 //===------------------------------------------------------------------===// 52 53 /// Given a symbolic expression that can be reasoned about, assume that it is 54 /// true/false and generate the new program state. 55 virtual ProgramStateRef assumeSym(ProgramStateRef State, SymbolRef Sym, 56 bool Assumption) = 0; 57 58 /// Given a symbolic expression within the range [From, To], assume that it is 59 /// true/false and generate the new program state. 60 /// This function is used to handle case ranges produced by a language 61 /// extension for switch case statements. 62 virtual ProgramStateRef assumeSymInclusiveRange(ProgramStateRef State, 63 SymbolRef Sym, 64 const llvm::APSInt &From, 65 const llvm::APSInt &To, 66 bool InRange) = 0; 67 68 /// Given a symbolic expression that cannot be reasoned about, assume that 69 /// it is zero/nonzero and add it directly to the solver state. 70 virtual ProgramStateRef assumeSymUnsupported(ProgramStateRef State, 71 SymbolRef Sym, 72 bool Assumption) = 0; 73 74 //===------------------------------------------------------------------===// 75 // Internal implementation. 76 //===------------------------------------------------------------------===// 77 78 BasicValueFactory &getBasicVals() const { return SVB.getBasicValueFactory(); } 79 SymbolManager &getSymbolManager() const { return SVB.getSymbolManager(); } 80 81 private: 82 ProgramStateRef assume(ProgramStateRef State, NonLoc Cond, bool Assumption); 83 84 ProgramStateRef assumeAux(ProgramStateRef State, NonLoc Cond, 85 bool Assumption); 86 }; 87 88 } // end GR namespace 89 90 } // end clang namespace 91 92 #endif 93
