1d19e21bcd347542bd1fa9ec767f14d91ef593d34Zhongxing Xu//== ConstraintManager.h - Constraints on symbolic values.-------*- C++ -*--==// 2d19e21bcd347542bd1fa9ec767f14d91ef593d34Zhongxing Xu// 3d19e21bcd347542bd1fa9ec767f14d91ef593d34Zhongxing Xu// The LLVM Compiler Infrastructure 4d19e21bcd347542bd1fa9ec767f14d91ef593d34Zhongxing Xu// 5d19e21bcd347542bd1fa9ec767f14d91ef593d34Zhongxing Xu// This file is distributed under the University of Illinois Open Source 6d19e21bcd347542bd1fa9ec767f14d91ef593d34Zhongxing Xu// License. See LICENSE.TXT for details. 7d19e21bcd347542bd1fa9ec767f14d91ef593d34Zhongxing Xu// 8d19e21bcd347542bd1fa9ec767f14d91ef593d34Zhongxing Xu//===----------------------------------------------------------------------===// 9d19e21bcd347542bd1fa9ec767f14d91ef593d34Zhongxing Xu// 10d19e21bcd347542bd1fa9ec767f14d91ef593d34Zhongxing Xu// This file defined the interface to manage constraints on symbolic values. 11d19e21bcd347542bd1fa9ec767f14d91ef593d34Zhongxing Xu// 12d19e21bcd347542bd1fa9ec767f14d91ef593d34Zhongxing Xu//===----------------------------------------------------------------------===// 13d19e21bcd347542bd1fa9ec767f14d91ef593d34Zhongxing Xu 145a4f98ff943e6a501b0fe47ade007c9bbf96cb88Argyrios Kyrtzidis#ifndef LLVM_CLANG_GR_CONSTRAINT_MANAGER_H 155a4f98ff943e6a501b0fe47ade007c9bbf96cb88Argyrios Kyrtzidis#define LLVM_CLANG_GR_CONSTRAINT_MANAGER_H 1639cfed397baf1ffca0ab85cfa3d03087fe80e2ccZhongxing Xu 17f5e39ece75b18c9ce19351929d4879ad9731e7f5Jordy Rose#include "clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h" 18f5e39ece75b18c9ce19351929d4879ad9731e7f5Jordy Rose#include "clang/StaticAnalyzer/Core/PathSensitive/SVals.h" 1939cfed397baf1ffca0ab85cfa3d03087fe80e2ccZhongxing Xu 2039cfed397baf1ffca0ab85cfa3d03087fe80e2ccZhongxing Xunamespace llvm { 2139cfed397baf1ffca0ab85cfa3d03087fe80e2ccZhongxing Xuclass APSInt; 2239cfed397baf1ffca0ab85cfa3d03087fe80e2ccZhongxing Xu} 2330ad167f74cb8a04c35ced6c69b116f15d104f8eZhongxing Xu 2430ad167f74cb8a04c35ced6c69b116f15d104f8eZhongxing Xunamespace clang { 259ef6537a894c33003359b1f9b9676e9178e028b7Ted Kremeneknamespace ento { 265a4f98ff943e6a501b0fe47ade007c9bbf96cb88Argyrios Kyrtzidis 27d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidisclass SubEngine; 2830ad167f74cb8a04c35ced6c69b116f15d104f8eZhongxing Xu 2947cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenekclass ConditionTruthVal { 3047cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek llvm::Optional<bool> Val; 3147cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenekpublic: 3247cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek /// Construct a ConditionTruthVal indicating the constraint is constrained 3347cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek /// to either true or false, depending on the boolean value provided. 3447cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek ConditionTruthVal(bool constraint) : Val(constraint) {} 3547cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek 3647cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek /// Construct a ConstraintVal indicating the constraint is underconstrained. 3747cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek ConditionTruthVal() {} 3847cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek 3947cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek /// Return true if the constraint is perfectly constrained to 'true'. 4047cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek bool isTrue() const { 4147cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek return Val.hasValue() && Val.getValue(); 4247cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek } 4347cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek 4447cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek /// Return true if the constraint is perfectly constrained to 'false'. 4547cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek bool isFalse() const { 4647cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek return Val.hasValue() && !Val.getValue(); 4747cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek } 4847cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek 4947cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek /// Return true if the constrained is perfectly constrained. 5047cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek bool isConstrained() const { 5147cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek return Val.hasValue(); 5247cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek } 5347cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek 5447cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek /// Return true if the constrained is underconstrained and we do not know 5547cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek /// if the constraint is true of value. 5647cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek bool isUnderconstrained() const { 5747cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek return !Val.hasValue(); 5847cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek } 5947cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek}; 6047cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek 6130ad167f74cb8a04c35ced6c69b116f15d104f8eZhongxing Xuclass ConstraintManager { 6230ad167f74cb8a04c35ced6c69b116f15d104f8eZhongxing Xupublic: 6347cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek ConstraintManager() : NotifyAssumeClients(true) {} 6447cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek 6505125f180d8f0967d8bcb7e9d578e36eb6905b92Ted Kremenek virtual ~ConstraintManager(); 668bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek virtual ProgramStateRef assume(ProgramStateRef state, 6747cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek DefinedSVal Cond, 6847cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek bool Assumption) = 0; 6947cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek 7047cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek typedef std::pair<ProgramStateRef, ProgramStateRef> ProgramStatePair; 7147cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek 7247cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek ProgramStatePair assumeDual(ProgramStateRef state, DefinedSVal Cond) { 7347cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek ProgramStatePair res(assume(state, Cond, true), 7447cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek assume(state, Cond, false)); 75c24b4f6ae3507aa501c2dafdff62c1059f8922adAnna Zaks assert(!(!res.first && !res.second) && "System is over constrained."); 76c24b4f6ae3507aa501c2dafdff62c1059f8922adAnna Zaks return res; 7767afec15ddbea77d9560165282542cbe1b413d01Ted Kremenek } 78e8a964bdb46349e4fa3433c8e5104d2a0f7f5c65Zhongxing Xu 79526b4a63cd567393fd43af837ac9d0f35fc267f7Ted Kremenek /// \brief If a symbol is perfectly constrained to a constant, attempt 80526b4a63cd567393fd43af837ac9d0f35fc267f7Ted Kremenek /// to return the concrete value. 81526b4a63cd567393fd43af837ac9d0f35fc267f7Ted Kremenek /// 82526b4a63cd567393fd43af837ac9d0f35fc267f7Ted Kremenek /// Note that a ConstraintManager is not obligated to return a concretized 83526b4a63cd567393fd43af837ac9d0f35fc267f7Ted Kremenek /// value for a symbol, even if it is perfectly constrained. 848bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek virtual const llvm::APSInt* getSymVal(ProgramStateRef state, 85526b4a63cd567393fd43af837ac9d0f35fc267f7Ted Kremenek SymbolRef sym) const { 86526b4a63cd567393fd43af837ac9d0f35fc267f7Ted Kremenek return 0; 87526b4a63cd567393fd43af837ac9d0f35fc267f7Ted Kremenek } 8839cfed397baf1ffca0ab85cfa3d03087fe80e2ccZhongxing Xu 898bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek virtual ProgramStateRef removeDeadBindings(ProgramStateRef state, 9018c66fdc3c4008d335885695fe36fb5353c5f672Ted Kremenek SymbolReaper& SymReaper) = 0; 9139cfed397baf1ffca0ab85cfa3d03087fe80e2ccZhongxing Xu 928bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek virtual void print(ProgramStateRef state, 9318c66fdc3c4008d335885695fe36fb5353c5f672Ted Kremenek raw_ostream &Out, 9418c66fdc3c4008d335885695fe36fb5353c5f672Ted Kremenek const char* nl, 9518c66fdc3c4008d335885695fe36fb5353c5f672Ted Kremenek const char *sep) = 0; 96e73dc26690776887bd2991461f6814498600d6ebZhongxing Xu 978bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek virtual void EndPath(ProgramStateRef state) {} 9847cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek 9947cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek /// Convenience method to query the state to see if a symbol is null or 10047cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek /// not null, or neither assumption can be made. 10147cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek ConditionTruthVal isNull(ProgramStateRef State, SymbolRef Sym); 1021eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 103eca4e6e58170129cbdf105b2cfdb9ac2be61858eAnna Zaksprotected: 10447cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek /// A flag to indicate that clients should be notified of assumptions. 10547cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek /// By default this is the case, but sometimes this needs to be restricted 10647cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek /// to avoid infinite recursions within the ConstraintManager. 10747cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek /// 10847cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek /// Note that this flag allows the ConstraintManager to be re-entrant, 10947cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek /// but not thread-safe. 11047cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek bool NotifyAssumeClients; 11147cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek 11266b527193aa6f3aa94c03f6769c42d7642e1e147Ted Kremenek /// canReasonAbout - Not all ConstraintManagers can accurately reason about 11366b527193aa6f3aa94c03f6769c42d7642e1e147Ted Kremenek /// all SVal values. This method returns true if the ConstraintManager can 11466b527193aa6f3aa94c03f6769c42d7642e1e147Ted Kremenek /// reasonably handle a given SVal value. This is typically queried by 115d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis /// ExprEngine to determine if the value should be replaced with a 11666b527193aa6f3aa94c03f6769c42d7642e1e147Ted Kremenek /// conjured symbolic value in order to recover some precision. 11766b527193aa6f3aa94c03f6769c42d7642e1e147Ted Kremenek virtual bool canReasonAbout(SVal X) const = 0; 11830ad167f74cb8a04c35ced6c69b116f15d104f8eZhongxing Xu}; 11930ad167f74cb8a04c35ced6c69b116f15d104f8eZhongxing Xu 12018c66fdc3c4008d335885695fe36fb5353c5f672Ted KremenekConstraintManager* CreateRangeConstraintManager(ProgramStateManager& statemgr, 121d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis SubEngine &subengine); 12230ad167f74cb8a04c35ced6c69b116f15d104f8eZhongxing Xu 1235a4f98ff943e6a501b0fe47ade007c9bbf96cb88Argyrios Kyrtzidis} // end GR namespace 1245a4f98ff943e6a501b0fe47ade007c9bbf96cb88Argyrios Kyrtzidis 12530ad167f74cb8a04c35ced6c69b116f15d104f8eZhongxing Xu} // end clang namespace 12630ad167f74cb8a04c35ced6c69b116f15d104f8eZhongxing Xu 12730ad167f74cb8a04c35ced6c69b116f15d104f8eZhongxing Xu#endif 128