Core/PathSensitive/ConstraintManager.h

0001 //===- ConstraintManager.h - Constraints on symbolic values. ----*- C++ -*-===//
0002 //
0003 // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
0004 // See https://llvm.org/LICENSE.txt for license information.
0005 // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
0006 //
0007 //===----------------------------------------------------------------------===//
0008 //
0009 //  This file defined the interface to manage constraints on symbolic values.
0010 //
0011 //===----------------------------------------------------------------------===//
0012
0013 #ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_CONSTRAINTMANAGER_H
0014 #define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_CONSTRAINTMANAGER_H
0015
0016 #include "clang/Basic/LLVM.h"
0017 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState_Fwd.h"
0018 #include "clang/StaticAnalyzer/Core/PathSensitive/SVals.h"
0019 #include "clang/StaticAnalyzer/Core/PathSensitive/SymExpr.h"
0020 #include "llvm/Support/SaveAndRestore.h"
0021 #include <memory>
0022 #include <optional>
0023 #include <utility>
0024
0025 namespace llvm {
0026
0027 class APSInt;
0028
0029 } // namespace llvm
0030
0031 namespace clang {
0032 namespace ento {
0033
0034 class ProgramStateManager;
0035 class ExprEngine;
0036 class SymbolReaper;
0037
0038 class ConditionTruthVal {
0039   std::optional<bool> Val;
0040
0041 public:
0042   /// Construct a ConditionTruthVal indicating the constraint is constrained
0043   /// to either true or false, depending on the boolean value provided.
0044   ConditionTruthVal(bool constraint) : Val(constraint) {}
0045
0046   /// Construct a ConstraintVal indicating the constraint is underconstrained.
0047   ConditionTruthVal() = default;
0048
0049   /// \return Stored value, assuming that the value is known.
0050   /// Crashes otherwise.
0051   bool getValue() const {
0052     return *Val;
0053   }
0054
0055   /// Return true if the constraint is perfectly constrained to 'true'.
0056   bool isConstrainedTrue() const { return Val && *Val; }
0057
0058   /// Return true if the constraint is perfectly constrained to 'false'.
0059   bool isConstrainedFalse() const { return Val && !*Val; }
0060
0061   /// Return true if the constrained is perfectly constrained.
0062   bool isConstrained() const { return Val.has_value(); }
0063
0064   /// Return true if the constrained is underconstrained and we do not know
0065   /// if the constraint is true of value.
0066   bool isUnderconstrained() const { return !Val.has_value(); }
0067 };
0068
0069 class ConstraintManager {
0070 public:
0071   ConstraintManager() = default;
0072   virtual ~ConstraintManager();
0073
0074   virtual bool haveEqualConstraints(ProgramStateRef S1,
0075                                     ProgramStateRef S2) const = 0;
0076
0077   ProgramStateRef assume(ProgramStateRef state, DefinedSVal Cond,
0078                          bool Assumption);
0079
0080   using ProgramStatePair = std::pair<ProgramStateRef, ProgramStateRef>;
0081
0082   /// Returns a pair of states (StTrue, StFalse) where the given condition is
0083   /// assumed to be true or false, respectively.
0084   /// (Note that these two states might be equal if the parent state turns out
0085   /// to be infeasible. This may happen if the underlying constraint solver is
0086   /// not perfectly precise and this may happen very rarely.)
0087   ProgramStatePair assumeDual(ProgramStateRef State, DefinedSVal Cond);
0088
0089   ProgramStateRef assumeInclusiveRange(ProgramStateRef State, NonLoc Value,
0090                                        const llvm::APSInt &From,
0091                                        const llvm::APSInt &To, bool InBound);
0092
0093   /// Returns a pair of states (StInRange, StOutOfRange) where the given value
0094   /// is assumed to be in the range or out of the range, respectively.
0095   /// (Note that these two states might be equal if the parent state turns out
0096   /// to be infeasible. This may happen if the underlying constraint solver is
0097   /// not perfectly precise and this may happen very rarely.)
0098   ProgramStatePair assumeInclusiveRangeDual(ProgramStateRef State, NonLoc Value,
0099                                             const llvm::APSInt &From,
0100                                             const llvm::APSInt &To);
0101
0102   /// If a symbol is perfectly constrained to a constant, attempt
0103   /// to return the concrete value.
0104   ///
0105   /// Note that a ConstraintManager is not obligated to return a concretized
0106   /// value for a symbol, even if it is perfectly constrained.
0107   /// It might return null.
0108   virtual const llvm::APSInt* getSymVal(ProgramStateRef state,
0109                                         SymbolRef sym) const {
0110     return nullptr;
0111   }
0112
0113   /// Attempt to return the minimal possible value for a given symbol. Note
0114   /// that a ConstraintManager is not obligated to return a lower bound, it may
0115   /// also return nullptr.
0116   virtual const llvm::APSInt *getSymMinVal(ProgramStateRef state,
0117                                            SymbolRef sym) const {
0118     return nullptr;
0119   }
0120
0121   /// Attempt to return the minimal possible value for a given symbol. Note
0122   /// that a ConstraintManager is not obligated to return a lower bound, it may
0123   /// also return nullptr.
0124   virtual const llvm::APSInt *getSymMaxVal(ProgramStateRef state,
0125                                            SymbolRef sym) const {
0126     return nullptr;
0127   }
0128
0129   /// Scan all symbols referenced by the constraints. If the symbol is not
0130   /// alive, remove it.
0131   virtual ProgramStateRef removeDeadBindings(ProgramStateRef state,
0132                                                  SymbolReaper& SymReaper) = 0;
0133
0134   virtual void printJson(raw_ostream &Out, ProgramStateRef State,
0135                          const char *NL, unsigned int Space,
0136                          bool IsDot) const = 0;
0137
0138   virtual void printValue(raw_ostream &Out, ProgramStateRef State,
0139                           SymbolRef Sym) {}
0140
0141   /// Convenience method to query the state to see if a symbol is null or
0142   /// not null, or if neither assumption can be made.
0143   ConditionTruthVal isNull(ProgramStateRef State, SymbolRef Sym) {
0144     return checkNull(State, Sym);
0145   }
0146
0147 protected:
0148   /// A helper class to simulate the call stack of nested assume calls.
0149   class AssumeStackTy {
0150   public:
0151     void push(const ProgramState *S) { Aux.push_back(S); }
0152     void pop() { Aux.pop_back(); }
0153     bool contains(const ProgramState *S) const {
0154       return llvm::is_contained(Aux, S);
0155     }
0156
0157   private:
0158     llvm::SmallVector<const ProgramState *, 4> Aux;
0159   };
0160   AssumeStackTy AssumeStack;
0161
0162   virtual ProgramStateRef assumeInternal(ProgramStateRef state,
0163                                          DefinedSVal Cond, bool Assumption) = 0;
0164
0165   virtual ProgramStateRef assumeInclusiveRangeInternal(ProgramStateRef State,
0166                                                        NonLoc Value,
0167                                                        const llvm::APSInt &From,
0168                                                        const llvm::APSInt &To,
0169                                                        bool InBound) = 0;
0170
0171   /// canReasonAbout - Not all ConstraintManagers can accurately reason about
0172   ///  all SVal values.  This method returns true if the ConstraintManager can
0173   ///  reasonably handle a given SVal value.  This is typically queried by
0174   ///  ExprEngine to determine if the value should be replaced with a
0175   ///  conjured symbolic value in order to recover some precision.
0176   virtual bool canReasonAbout(SVal X) const = 0;
0177
0178   /// Returns whether or not a symbol is known to be null ("true"), known to be
0179   /// non-null ("false"), or may be either ("underconstrained").
0180   virtual ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym);
0181
0182   template <typename AssumeFunction>
0183   ProgramStatePair assumeDualImpl(ProgramStateRef &State,
0184                                   AssumeFunction &Assume);
0185 };
0186
0187 std::unique_ptr<ConstraintManager>
0188 CreateRangeConstraintManager(ProgramStateManager &statemgr,
0189                              ExprEngine *exprengine);
0190
0191 std::unique_ptr<ConstraintManager>
0192 CreateZ3ConstraintManager(ProgramStateManager &statemgr,
0193                           ExprEngine *exprengine);
0194
0195 } // namespace ento
0196 } // namespace clang
0197
0198 #endif // LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_CONSTRAINTMANAGER_H