include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h

   1 //===- ConstraintManager.h - Constraints on symbolic values. ----*- 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 //  This file defined the interface to manage constraints on symbolic values.
  11 //
  12 //===----------------------------------------------------------------------===//
  13
  14 #ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_CONSTRAINTMANAGER_H
  15 #define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_CONSTRAINTMANAGER_H
  16
  17 #include "clang/Basic/LLVM.h"
  18 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState_Fwd.h"
  19 #include "clang/StaticAnalyzer/Core/PathSensitive/SVals.h"
  20 #include "clang/StaticAnalyzer/Core/PathSensitive/SymExpr.h"
  21 #include "llvm/ADT/Optional.h"
  22 #include "llvm/Support/SaveAndRestore.h"
  23 #include <memory>
  24 #include <utility>
  25
  26 namespace llvm {
  27
  28 class APSInt;
  29
  30 } // namespace llvm
  31
  32 namespace clang {
  33 namespace ento {
  34
  35 class ProgramStateManager;
  36 class SubEngine;
  37 class SymbolReaper;
  38
  39 class ConditionTruthVal {
  40   Optional<bool> Val;
  41
  42 public:
  43   /// Construct a ConditionTruthVal indicating the constraint is constrained
  44   /// to either true or false, depending on the boolean value provided.
  45   ConditionTruthVal(bool constraint) : Val(constraint) {}
  46
  47   /// Construct a ConstraintVal indicating the constraint is underconstrained.
  48   ConditionTruthVal() = default;
  49
  50   /// \return Stored value, assuming that the value is known.
  51   /// Crashes otherwise.
  52   bool getValue() const {
  53     return *Val;
  54   }
  55
  56   /// Return true if the constraint is perfectly constrained to 'true'.
  57   bool isConstrainedTrue() const {
  58     return Val.hasValue() && Val.getValue();
  59   }
  60
  61   /// Return true if the constraint is perfectly constrained to 'false'.
  62   bool isConstrainedFalse() const {
  63     return Val.hasValue() && !Val.getValue();
  64   }
  65
  66   /// Return true if the constrained is perfectly constrained.
  67   bool isConstrained() const {
  68     return Val.hasValue();
  69   }
  70
  71   /// Return true if the constrained is underconstrained and we do not know
  72   /// if the constraint is true of value.
  73   bool isUnderconstrained() const {
  74     return !Val.hasValue();
  75   }
  76 };
  77
  78 class ConstraintManager {
  79 public:
  80   ConstraintManager() = default;
  81   virtual ~ConstraintManager();
  82
  83   virtual ProgramStateRef assume(ProgramStateRef state,
  84                                  DefinedSVal Cond,
  85                                  bool Assumption) = 0;
  86
  87   using ProgramStatePair = std::pair<ProgramStateRef, ProgramStateRef>;
  88
  89   /// Returns a pair of states (StTrue, StFalse) where the given condition is
  90   /// assumed to be true or false, respectively.
  91   ProgramStatePair assumeDual(ProgramStateRef State, DefinedSVal Cond) {
  92     ProgramStateRef StTrue = assume(State, Cond, true);
  93
  94     // If StTrue is infeasible, asserting the falseness of Cond is unnecessary
  95     // because the existing constraints already establish this.
  96     if (!StTrue) {
  97 #ifndef __OPTIMIZE__
  98       // This check is expensive and should be disabled even in Release+Asserts
  99       // builds.
 100       // FIXME: __OPTIMIZE__ is a GNU extension that Clang implements but MSVC
 101       // does not. Is there a good equivalent there?
 102       assert(assume(State, Cond, false) && "System is over constrained.");
 103 #endif
 104       return ProgramStatePair((ProgramStateRef)nullptr, State);
 105     }
 106
 107     ProgramStateRef StFalse = assume(State, Cond, false);
 108     if (!StFalse) {
 109       // We are careful to return the original state, /not/ StTrue,
 110       // because we want to avoid having callers generate a new node
 111       // in the ExplodedGraph.
 112       return ProgramStatePair(State, (ProgramStateRef)nullptr);
 113     }
 114
 115     return ProgramStatePair(StTrue, StFalse);
 116   }
 117
 118   virtual ProgramStateRef assumeInclusiveRange(ProgramStateRef State,
 119                                                NonLoc Value,
 120                                                const llvm::APSInt &From,
 121                                                const llvm::APSInt &To,
 122                                                bool InBound) = 0;
 123
 124   virtual ProgramStatePair assumeInclusiveRangeDual(ProgramStateRef State,
 125                                                     NonLoc Value,
 126                                                     const llvm::APSInt &From,
 127                                                     const llvm::APSInt &To) {
 128     ProgramStateRef StInRange =
 129         assumeInclusiveRange(State, Value, From, To, true);
 130
 131     // If StTrue is infeasible, asserting the falseness of Cond is unnecessary
 132     // because the existing constraints already establish this.
 133     if (!StInRange)
 134       return ProgramStatePair((ProgramStateRef)nullptr, State);
 135
 136     ProgramStateRef StOutOfRange =
 137         assumeInclusiveRange(State, Value, From, To, false);
 138     if (!StOutOfRange) {
 139       // We are careful to return the original state, /not/ StTrue,
 140       // because we want to avoid having callers generate a new node
 141       // in the ExplodedGraph.
 142       return ProgramStatePair(State, (ProgramStateRef)nullptr);
 143     }
 144
 145     return ProgramStatePair(StInRange, StOutOfRange);
 146   }
 147
 148   /// If a symbol is perfectly constrained to a constant, attempt
 149   /// to return the concrete value.
 150   ///
 151   /// Note that a ConstraintManager is not obligated to return a concretized
 152   /// value for a symbol, even if it is perfectly constrained.
 153   virtual const llvm::APSInt* getSymVal(ProgramStateRef state,
 154                                         SymbolRef sym) const {
 155     return nullptr;
 156   }
 157
 158   /// Scan all symbols referenced by the constraints. If the symbol is not
 159   /// alive, remove it.
 160   virtual ProgramStateRef removeDeadBindings(ProgramStateRef state,
 161                                                  SymbolReaper& SymReaper) = 0;
 162
 163   virtual void print(ProgramStateRef state,
 164                      raw_ostream &Out,
 165                      const char* nl,
 166                      const char *sep) = 0;
 167
 168   virtual void EndPath(ProgramStateRef state) {}
 169
 170   /// Convenience method to query the state to see if a symbol is null or
 171   /// not null, or if neither assumption can be made.
 172   ConditionTruthVal isNull(ProgramStateRef State, SymbolRef Sym) {
 173     SaveAndRestore<bool> DisableNotify(NotifyAssumeClients, false);
 174
 175     return checkNull(State, Sym);
 176   }
 177
 178 protected:
 179   /// A flag to indicate that clients should be notified of assumptions.
 180   /// By default this is the case, but sometimes this needs to be restricted
 181   /// to avoid infinite recursions within the ConstraintManager.
 182   ///
 183   /// Note that this flag allows the ConstraintManager to be re-entrant,
 184   /// but not thread-safe.
 185   bool NotifyAssumeClients = true;
 186
 187   /// canReasonAbout - Not all ConstraintManagers can accurately reason about
 188   ///  all SVal values.  This method returns true if the ConstraintManager can
 189   ///  reasonably handle a given SVal value.  This is typically queried by
 190   ///  ExprEngine to determine if the value should be replaced with a
 191   ///  conjured symbolic value in order to recover some precision.
 192   virtual bool canReasonAbout(SVal X) const = 0;
 193
 194   /// Returns whether or not a symbol is known to be null ("true"), known to be
 195   /// non-null ("false"), or may be either ("underconstrained").
 196   virtual ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym);
 197 };
 198
 199 std::unique_ptr<ConstraintManager>
 200 CreateRangeConstraintManager(ProgramStateManager &statemgr,
 201                              SubEngine *subengine);
 202
 203 std::unique_ptr<ConstraintManager>
 204 CreateZ3ConstraintManager(ProgramStateManager &statemgr, SubEngine *subengine);
 205
 206 } // namespace ento
 207 } // namespace clang
 208
 209 #endif // LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_CONSTRAINTMANAGER_H