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/SVals.h" 1830a2e16f6c27f888dd11eba6bbbae1e980078fcbChandler Carruth#include "clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h" 19c45bb4dcb648cd8b5250492afe7df254e4157aaaJordan Rose#include "llvm/Support/SaveAndRestore.h" 2039cfed397baf1ffca0ab85cfa3d03087fe80e2ccZhongxing Xu 2139cfed397baf1ffca0ab85cfa3d03087fe80e2ccZhongxing Xunamespace llvm { 2239cfed397baf1ffca0ab85cfa3d03087fe80e2ccZhongxing Xuclass APSInt; 2339cfed397baf1ffca0ab85cfa3d03087fe80e2ccZhongxing Xu} 2430ad167f74cb8a04c35ced6c69b116f15d104f8eZhongxing Xu 2530ad167f74cb8a04c35ced6c69b116f15d104f8eZhongxing Xunamespace clang { 269ef6537a894c33003359b1f9b9676e9178e028b7Ted Kremeneknamespace ento { 275a4f98ff943e6a501b0fe47ade007c9bbf96cb88Argyrios Kyrtzidis 28d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidisclass SubEngine; 2930ad167f74cb8a04c35ced6c69b116f15d104f8eZhongxing Xu 3047cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenekclass ConditionTruthVal { 31dc84cd5efdd3430efb22546b4ac656aa0540b210David Blaikie Optional<bool> Val; 3247cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenekpublic: 3347cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek /// Construct a ConditionTruthVal indicating the constraint is constrained 3447cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek /// to either true or false, depending on the boolean value provided. 3547cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek ConditionTruthVal(bool constraint) : Val(constraint) {} 3647cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek 3747cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek /// Construct a ConstraintVal indicating the constraint is underconstrained. 3847cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek ConditionTruthVal() {} 3947cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek 4047cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek /// Return true if the constraint is perfectly constrained to 'true'. 41ec8d420d4fa57fc6b5a5a2b1446742e976a7ba00Jordan Rose bool isConstrainedTrue() const { 4247cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek return Val.hasValue() && Val.getValue(); 4347cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek } 4447cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek 4547cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek /// Return true if the constraint is perfectly constrained to 'false'. 46ec8d420d4fa57fc6b5a5a2b1446742e976a7ba00Jordan Rose bool isConstrainedFalse() const { 4747cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek return Val.hasValue() && !Val.getValue(); 4847cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek } 4947cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek 5047cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek /// Return true if the constrained is perfectly constrained. 5147cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek bool isConstrained() const { 5247cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek return Val.hasValue(); 5347cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek } 5447cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek 5547cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek /// Return true if the constrained is underconstrained and we do not know 5647cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek /// if the constraint is true of value. 5747cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek bool isUnderconstrained() const { 5847cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek return !Val.hasValue(); 5947cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek } 6047cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek}; 6147cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek 6230ad167f74cb8a04c35ced6c69b116f15d104f8eZhongxing Xuclass ConstraintManager { 6330ad167f74cb8a04c35ced6c69b116f15d104f8eZhongxing Xupublic: 6447cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek ConstraintManager() : NotifyAssumeClients(true) {} 6547cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek 6605125f180d8f0967d8bcb7e9d578e36eb6905b92Ted Kremenek virtual ~ConstraintManager(); 678bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek virtual ProgramStateRef assume(ProgramStateRef state, 6847cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek DefinedSVal Cond, 6947cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek bool Assumption) = 0; 7047cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek 7147cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek typedef std::pair<ProgramStateRef, ProgramStateRef> ProgramStatePair; 72baf764092c76d74fb1528cfd62540ae7dc01efbdJordan Rose 73baf764092c76d74fb1528cfd62540ae7dc01efbdJordan Rose /// Returns a pair of states (StTrue, StFalse) where the given condition is 74baf764092c76d74fb1528cfd62540ae7dc01efbdJordan Rose /// assumed to be true or false, respectively. 75baf764092c76d74fb1528cfd62540ae7dc01efbdJordan Rose ProgramStatePair assumeDual(ProgramStateRef State, DefinedSVal Cond) { 76baf764092c76d74fb1528cfd62540ae7dc01efbdJordan Rose ProgramStateRef StTrue = assume(State, Cond, true); 77baf764092c76d74fb1528cfd62540ae7dc01efbdJordan Rose 78baf764092c76d74fb1528cfd62540ae7dc01efbdJordan Rose // If StTrue is infeasible, asserting the falseness of Cond is unnecessary 79baf764092c76d74fb1528cfd62540ae7dc01efbdJordan Rose // because the existing constraints already establish this. 80baf764092c76d74fb1528cfd62540ae7dc01efbdJordan Rose if (!StTrue) { 8130f102b2782d08eb3ea61dd20a2ff7326a15fe1eJordan Rose#ifndef __OPTIMIZE__ 8230f102b2782d08eb3ea61dd20a2ff7326a15fe1eJordan Rose // This check is expensive and should be disabled even in Release+Asserts 8330f102b2782d08eb3ea61dd20a2ff7326a15fe1eJordan Rose // builds. 8430f102b2782d08eb3ea61dd20a2ff7326a15fe1eJordan Rose // FIXME: __OPTIMIZE__ is a GNU extension that Clang implements but MSVC 8530f102b2782d08eb3ea61dd20a2ff7326a15fe1eJordan Rose // does not. Is there a good equivalent there? 86baf764092c76d74fb1528cfd62540ae7dc01efbdJordan Rose assert(assume(State, Cond, false) && "System is over constrained."); 8730f102b2782d08eb3ea61dd20a2ff7326a15fe1eJordan Rose#endif 883cdd84318a3ae43fa31da849f1a6d3eeb8a39d2dNAKAMURA Takumi return ProgramStatePair((ProgramStateRef)NULL, State); 89baf764092c76d74fb1528cfd62540ae7dc01efbdJordan Rose } 90baf764092c76d74fb1528cfd62540ae7dc01efbdJordan Rose 91baf764092c76d74fb1528cfd62540ae7dc01efbdJordan Rose ProgramStateRef StFalse = assume(State, Cond, false); 92baf764092c76d74fb1528cfd62540ae7dc01efbdJordan Rose if (!StFalse) { 93baf764092c76d74fb1528cfd62540ae7dc01efbdJordan Rose // We are careful to return the original state, /not/ StTrue, 94baf764092c76d74fb1528cfd62540ae7dc01efbdJordan Rose // because we want to avoid having callers generate a new node 95baf764092c76d74fb1528cfd62540ae7dc01efbdJordan Rose // in the ExplodedGraph. 963cdd84318a3ae43fa31da849f1a6d3eeb8a39d2dNAKAMURA Takumi return ProgramStatePair(State, (ProgramStateRef)NULL); 97baf764092c76d74fb1528cfd62540ae7dc01efbdJordan Rose } 98baf764092c76d74fb1528cfd62540ae7dc01efbdJordan Rose 99baf764092c76d74fb1528cfd62540ae7dc01efbdJordan Rose return ProgramStatePair(StTrue, StFalse); 10067afec15ddbea77d9560165282542cbe1b413d01Ted Kremenek } 101e8a964bdb46349e4fa3433c8e5104d2a0f7f5c65Zhongxing Xu 102526b4a63cd567393fd43af837ac9d0f35fc267f7Ted Kremenek /// \brief If a symbol is perfectly constrained to a constant, attempt 103526b4a63cd567393fd43af837ac9d0f35fc267f7Ted Kremenek /// to return the concrete value. 104526b4a63cd567393fd43af837ac9d0f35fc267f7Ted Kremenek /// 105526b4a63cd567393fd43af837ac9d0f35fc267f7Ted Kremenek /// Note that a ConstraintManager is not obligated to return a concretized 106526b4a63cd567393fd43af837ac9d0f35fc267f7Ted Kremenek /// value for a symbol, even if it is perfectly constrained. 1078bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek virtual const llvm::APSInt* getSymVal(ProgramStateRef state, 108526b4a63cd567393fd43af837ac9d0f35fc267f7Ted Kremenek SymbolRef sym) const { 109526b4a63cd567393fd43af837ac9d0f35fc267f7Ted Kremenek return 0; 110526b4a63cd567393fd43af837ac9d0f35fc267f7Ted Kremenek } 11139cfed397baf1ffca0ab85cfa3d03087fe80e2ccZhongxing Xu 1128bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek virtual ProgramStateRef removeDeadBindings(ProgramStateRef state, 11318c66fdc3c4008d335885695fe36fb5353c5f672Ted Kremenek SymbolReaper& SymReaper) = 0; 11439cfed397baf1ffca0ab85cfa3d03087fe80e2ccZhongxing Xu 1158bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek virtual void print(ProgramStateRef state, 11618c66fdc3c4008d335885695fe36fb5353c5f672Ted Kremenek raw_ostream &Out, 11718c66fdc3c4008d335885695fe36fb5353c5f672Ted Kremenek const char* nl, 11818c66fdc3c4008d335885695fe36fb5353c5f672Ted Kremenek const char *sep) = 0; 119e73dc26690776887bd2991461f6814498600d6ebZhongxing Xu 1208bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek virtual void EndPath(ProgramStateRef state) {} 12147cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek 12247cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek /// Convenience method to query the state to see if a symbol is null or 123c45bb4dcb648cd8b5250492afe7df254e4157aaaJordan Rose /// not null, or if neither assumption can be made. 124c45bb4dcb648cd8b5250492afe7df254e4157aaaJordan Rose ConditionTruthVal isNull(ProgramStateRef State, SymbolRef Sym) { 125cfa88f893915ceb8ae4ce2f17c46c24a4d67502fDmitri Gribenko SaveAndRestore<bool> DisableNotify(NotifyAssumeClients, false); 126c45bb4dcb648cd8b5250492afe7df254e4157aaaJordan Rose 127c45bb4dcb648cd8b5250492afe7df254e4157aaaJordan Rose return checkNull(State, Sym); 128c45bb4dcb648cd8b5250492afe7df254e4157aaaJordan Rose } 1291eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 130eca4e6e58170129cbdf105b2cfdb9ac2be61858eAnna Zaksprotected: 13147cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek /// A flag to indicate that clients should be notified of assumptions. 13247cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek /// By default this is the case, but sometimes this needs to be restricted 13347cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek /// to avoid infinite recursions within the ConstraintManager. 13447cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek /// 13547cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek /// Note that this flag allows the ConstraintManager to be re-entrant, 13647cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek /// but not thread-safe. 13747cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek bool NotifyAssumeClients; 13847cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek 13966b527193aa6f3aa94c03f6769c42d7642e1e147Ted Kremenek /// canReasonAbout - Not all ConstraintManagers can accurately reason about 14066b527193aa6f3aa94c03f6769c42d7642e1e147Ted Kremenek /// all SVal values. This method returns true if the ConstraintManager can 14166b527193aa6f3aa94c03f6769c42d7642e1e147Ted Kremenek /// reasonably handle a given SVal value. This is typically queried by 142d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis /// ExprEngine to determine if the value should be replaced with a 14366b527193aa6f3aa94c03f6769c42d7642e1e147Ted Kremenek /// conjured symbolic value in order to recover some precision. 14466b527193aa6f3aa94c03f6769c42d7642e1e147Ted Kremenek virtual bool canReasonAbout(SVal X) const = 0; 145c45bb4dcb648cd8b5250492afe7df254e4157aaaJordan Rose 146c45bb4dcb648cd8b5250492afe7df254e4157aaaJordan Rose /// Returns whether or not a symbol is known to be null ("true"), known to be 147c45bb4dcb648cd8b5250492afe7df254e4157aaaJordan Rose /// non-null ("false"), or may be either ("underconstrained"). 148c45bb4dcb648cd8b5250492afe7df254e4157aaaJordan Rose virtual ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym); 14930ad167f74cb8a04c35ced6c69b116f15d104f8eZhongxing Xu}; 15030ad167f74cb8a04c35ced6c69b116f15d104f8eZhongxing Xu 15118c66fdc3c4008d335885695fe36fb5353c5f672Ted KremenekConstraintManager* CreateRangeConstraintManager(ProgramStateManager& statemgr, 152ca5d78d0bc3010164f2f9682967d64d7e305a167Jordan Rose SubEngine *subengine); 15330ad167f74cb8a04c35ced6c69b116f15d104f8eZhongxing Xu 1545a4f98ff943e6a501b0fe47ade007c9bbf96cb88Argyrios Kyrtzidis} // end GR namespace 1555a4f98ff943e6a501b0fe47ade007c9bbf96cb88Argyrios Kyrtzidis 15630ad167f74cb8a04c35ced6c69b116f15d104f8eZhongxing Xu} // end clang namespace 15730ad167f74cb8a04c35ced6c69b116f15d104f8eZhongxing Xu 15830ad167f74cb8a04c35ced6c69b116f15d104f8eZhongxing Xu#endif 159