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/Support/SaveAndRestore.h"
21 #include <memory>
22 #include <optional>
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 ExprEngine;
36 class SymbolReaper;
37 
38 class ConditionTruthVal {
39   std::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.
ConditionTruthVal(bool constraint)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.
getValue()51   bool getValue() const {
52     return *Val;
53   }
54 
55   /// Return true if the constraint is perfectly constrained to 'true'.
isConstrainedTrue()56   bool isConstrainedTrue() const { return Val && *Val; }
57 
58   /// Return true if the constraint is perfectly constrained to 'false'.
isConstrainedFalse()59   bool isConstrainedFalse() const { return Val && !*Val; }
60 
61   /// Return true if the constrained is perfectly constrained.
isConstrained()62   bool isConstrained() const { return Val.has_value(); }
63 
64   /// Return true if the constrained is underconstrained and we do not know
65   /// if the constraint is true of value.
isUnderconstrained()66   bool isUnderconstrained() const { return !Val.has_value(); }
67 };
68 
69 class ConstraintManager {
70 public:
71   ConstraintManager() = default;
72   virtual ~ConstraintManager();
73 
74   virtual bool haveEqualConstraints(ProgramStateRef S1,
75                                     ProgramStateRef S2) const = 0;
76 
77   ProgramStateRef assume(ProgramStateRef state, DefinedSVal Cond,
78                          bool Assumption);
79 
80   using ProgramStatePair = std::pair<ProgramStateRef, ProgramStateRef>;
81 
82   /// Returns a pair of states (StTrue, StFalse) where the given condition is
83   /// assumed to be true or false, respectively.
84   /// (Note that these two states might be equal if the parent state turns out
85   /// to be infeasible. This may happen if the underlying constraint solver is
86   /// not perfectly precise and this may happen very rarely.)
87   ProgramStatePair assumeDual(ProgramStateRef State, DefinedSVal Cond);
88 
89   ProgramStateRef assumeInclusiveRange(ProgramStateRef State, NonLoc Value,
90                                        const llvm::APSInt &From,
91                                        const llvm::APSInt &To, bool InBound);
92 
93   /// Returns a pair of states (StInRange, StOutOfRange) where the given value
94   /// is assumed to be in the range or out of the range, respectively.
95   /// (Note that these two states might be equal if the parent state turns out
96   /// to be infeasible. This may happen if the underlying constraint solver is
97   /// not perfectly precise and this may happen very rarely.)
98   ProgramStatePair assumeInclusiveRangeDual(ProgramStateRef State, NonLoc Value,
99                                             const llvm::APSInt &From,
100                                             const llvm::APSInt &To);
101 
102   /// If a symbol is perfectly constrained to a constant, attempt
103   /// to return the concrete value.
104   ///
105   /// Note that a ConstraintManager is not obligated to return a concretized
106   /// value for a symbol, even if it is perfectly constrained.
107   /// It might return null.
getSymVal(ProgramStateRef state,SymbolRef sym)108   virtual const llvm::APSInt* getSymVal(ProgramStateRef state,
109                                         SymbolRef sym) const {
110     return nullptr;
111   }
112 
113   /// Attempt to return the minimal possible value for a given symbol. Note
114   /// that a ConstraintManager is not obligated to return a lower bound, it may
115   /// also return nullptr.
getSymMinVal(ProgramStateRef state,SymbolRef sym)116   virtual const llvm::APSInt *getSymMinVal(ProgramStateRef state,
117                                            SymbolRef sym) const {
118     return nullptr;
119   }
120 
121   /// Attempt to return the minimal possible value for a given symbol. Note
122   /// that a ConstraintManager is not obligated to return a lower bound, it may
123   /// also return nullptr.
getSymMaxVal(ProgramStateRef state,SymbolRef sym)124   virtual const llvm::APSInt *getSymMaxVal(ProgramStateRef state,
125                                            SymbolRef sym) const {
126     return nullptr;
127   }
128 
129   /// Scan all symbols referenced by the constraints. If the symbol is not
130   /// alive, remove it.
131   virtual ProgramStateRef removeDeadBindings(ProgramStateRef state,
132                                                  SymbolReaper& SymReaper) = 0;
133 
134   virtual void printJson(raw_ostream &Out, ProgramStateRef State,
135                          const char *NL, unsigned int Space,
136                          bool IsDot) const = 0;
137 
printValue(raw_ostream & Out,ProgramStateRef State,SymbolRef Sym)138   virtual void printValue(raw_ostream &Out, ProgramStateRef State,
139                           SymbolRef Sym) {}
140 
141   /// Convenience method to query the state to see if a symbol is null or
142   /// not null, or if neither assumption can be made.
isNull(ProgramStateRef State,SymbolRef Sym)143   ConditionTruthVal isNull(ProgramStateRef State, SymbolRef Sym) {
144     return checkNull(State, Sym);
145   }
146 
147 protected:
148   /// A helper class to simulate the call stack of nested assume calls.
149   class AssumeStackTy {
150   public:
push(const ProgramState * S)151     void push(const ProgramState *S) { Aux.push_back(S); }
pop()152     void pop() { Aux.pop_back(); }
contains(const ProgramState * S)153     bool contains(const ProgramState *S) const {
154       return llvm::is_contained(Aux, S);
155     }
156 
157   private:
158     llvm::SmallVector<const ProgramState *, 4> Aux;
159   };
160   AssumeStackTy AssumeStack;
161 
162   virtual ProgramStateRef assumeInternal(ProgramStateRef state,
163                                          DefinedSVal Cond, bool Assumption) = 0;
164 
165   virtual ProgramStateRef assumeInclusiveRangeInternal(ProgramStateRef State,
166                                                        NonLoc Value,
167                                                        const llvm::APSInt &From,
168                                                        const llvm::APSInt &To,
169                                                        bool InBound) = 0;
170 
171   /// canReasonAbout - Not all ConstraintManagers can accurately reason about
172   ///  all SVal values.  This method returns true if the ConstraintManager can
173   ///  reasonably handle a given SVal value.  This is typically queried by
174   ///  ExprEngine to determine if the value should be replaced with a
175   ///  conjured symbolic value in order to recover some precision.
176   virtual bool canReasonAbout(SVal X) const = 0;
177 
178   /// Returns whether or not a symbol is known to be null ("true"), known to be
179   /// non-null ("false"), or may be either ("underconstrained").
180   virtual ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym);
181 
182   template <typename AssumeFunction>
183   ProgramStatePair assumeDualImpl(ProgramStateRef &State,
184                                   AssumeFunction &Assume);
185 };
186 
187 std::unique_ptr<ConstraintManager>
188 CreateRangeConstraintManager(ProgramStateManager &statemgr,
189                              ExprEngine *exprengine);
190 
191 std::unique_ptr<ConstraintManager>
192 CreateZ3ConstraintManager(ProgramStateManager &statemgr,
193                           ExprEngine *exprengine);
194 
195 } // namespace ento
196 } // namespace clang
197 
198 #endif // LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_CONSTRAINTMANAGER_H
199