diff options
author | dim <dim@FreeBSD.org> | 2012-12-02 13:20:44 +0000 |
---|---|---|
committer | dim <dim@FreeBSD.org> | 2012-12-02 13:20:44 +0000 |
commit | 056abd2059c65a3e908193aeae16fad98017437c (patch) | |
tree | 2732d02d7d51218d6eed98ac7fcfc5b8794896b5 /include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h | |
parent | cc73504950eb7b5dff2dded9bedd67bc36d64641 (diff) | |
download | FreeBSD-src-056abd2059c65a3e908193aeae16fad98017437c.zip FreeBSD-src-056abd2059c65a3e908193aeae16fad98017437c.tar.gz |
Vendor import of clang release_32 branch r168974 (effectively, 3.2 RC2):
http://llvm.org/svn/llvm-project/cfe/branches/release_32@168974
Diffstat (limited to 'include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h')
-rw-r--r-- | include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h | 111 |
1 files changed, 92 insertions, 19 deletions
diff --git a/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h b/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h index 631858d..4a78849 100644 --- a/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h +++ b/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h @@ -16,6 +16,7 @@ #include "clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h" #include "clang/StaticAnalyzer/Core/PathSensitive/SVals.h" +#include "llvm/Support/SaveAndRestore.h" namespace llvm { class APSInt; @@ -26,29 +27,83 @@ namespace ento { class SubEngine; +class ConditionTruthVal { + llvm::Optional<bool> Val; +public: + /// Construct a ConditionTruthVal indicating the constraint is constrained + /// to either true or false, depending on the boolean value provided. + ConditionTruthVal(bool constraint) : Val(constraint) {} + + /// Construct a ConstraintVal indicating the constraint is underconstrained. + ConditionTruthVal() {} + + /// Return true if the constraint is perfectly constrained to 'true'. + bool isConstrainedTrue() const { + return Val.hasValue() && Val.getValue(); + } + + /// Return true if the constraint is perfectly constrained to 'false'. + bool isConstrainedFalse() const { + return Val.hasValue() && !Val.getValue(); + } + + /// Return true if the constrained is perfectly constrained. + bool isConstrained() const { + return Val.hasValue(); + } + + /// Return true if the constrained is underconstrained and we do not know + /// if the constraint is true of value. + bool isUnderconstrained() const { + return !Val.hasValue(); + } +}; + class ConstraintManager { public: + ConstraintManager() : NotifyAssumeClients(true) {} + virtual ~ConstraintManager(); virtual ProgramStateRef assume(ProgramStateRef state, - DefinedSVal Cond, - bool Assumption) = 0; - - std::pair<ProgramStateRef, ProgramStateRef > - assumeDual(ProgramStateRef state, DefinedSVal Cond) - { - std::pair<ProgramStateRef, ProgramStateRef > res = - std::make_pair(assume(state, Cond, true), assume(state, Cond, false)); - - assert(!(!res.first && !res.second) && "System is over constrained."); - return res; + DefinedSVal Cond, + bool Assumption) = 0; + + typedef std::pair<ProgramStateRef, ProgramStateRef> ProgramStatePair; + + /// Returns a pair of states (StTrue, StFalse) where the given condition is + /// assumed to be true or false, respectively. + ProgramStatePair assumeDual(ProgramStateRef State, DefinedSVal Cond) { + ProgramStateRef StTrue = assume(State, Cond, true); + + // If StTrue is infeasible, asserting the falseness of Cond is unnecessary + // because the existing constraints already establish this. + if (!StTrue) { + // FIXME: This is fairly expensive and should be disabled even in + // Release+Asserts builds. + assert(assume(State, Cond, false) && "System is over constrained."); + return ProgramStatePair((ProgramStateRef)NULL, State); + } + + ProgramStateRef StFalse = assume(State, Cond, false); + if (!StFalse) { + // We are careful to return the original state, /not/ StTrue, + // because we want to avoid having callers generate a new node + // in the ExplodedGraph. + return ProgramStatePair(State, (ProgramStateRef)NULL); + } + + return ProgramStatePair(StTrue, StFalse); } + /// \brief If a symbol is perfectly constrained to a constant, attempt + /// to return the concrete value. + /// + /// Note that a ConstraintManager is not obligated to return a concretized + /// value for a symbol, even if it is perfectly constrained. virtual const llvm::APSInt* getSymVal(ProgramStateRef state, - SymbolRef sym) const = 0; - - virtual bool isEqual(ProgramStateRef state, - SymbolRef sym, - const llvm::APSInt& V) const = 0; + SymbolRef sym) const { + return 0; + } virtual ProgramStateRef removeDeadBindings(ProgramStateRef state, SymbolReaper& SymReaper) = 0; @@ -59,20 +114,38 @@ public: const char *sep) = 0; virtual void EndPath(ProgramStateRef state) {} + + /// Convenience method to query the state to see if a symbol is null or + /// not null, or if neither assumption can be made. + ConditionTruthVal isNull(ProgramStateRef State, SymbolRef Sym) { + llvm::SaveAndRestore<bool> DisableNotify(NotifyAssumeClients, false); + + return checkNull(State, Sym); + } protected: + /// A flag to indicate that clients should be notified of assumptions. + /// By default this is the case, but sometimes this needs to be restricted + /// to avoid infinite recursions within the ConstraintManager. + /// + /// Note that this flag allows the ConstraintManager to be re-entrant, + /// but not thread-safe. + bool NotifyAssumeClients; + /// canReasonAbout - Not all ConstraintManagers can accurately reason about /// all SVal values. This method returns true if the ConstraintManager can /// reasonably handle a given SVal value. This is typically queried by /// ExprEngine to determine if the value should be replaced with a /// conjured symbolic value in order to recover some precision. virtual bool canReasonAbout(SVal X) const = 0; + + /// Returns whether or not a symbol is known to be null ("true"), known to be + /// non-null ("false"), or may be either ("underconstrained"). + virtual ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym); }; -ConstraintManager* CreateBasicConstraintManager(ProgramStateManager& statemgr, - SubEngine &subengine); ConstraintManager* CreateRangeConstraintManager(ProgramStateManager& statemgr, - SubEngine &subengine); + SubEngine *subengine); } // end GR namespace |