contrib/llvm/tools/clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h

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