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.
ConditionTruthVal(bool constraint)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.
getValue()52   bool getValue() const {
53     return *Val;
54   }
55 
56   /// Return true if the constraint is perfectly constrained to 'true'.
isConstrainedTrue()57   bool isConstrainedTrue() const {
58     return Val.hasValue() && Val.getValue();
59   }
60 
61   /// Return true if the constraint is perfectly constrained to 'false'.
isConstrainedFalse()62   bool isConstrainedFalse() const {
63     return Val.hasValue() && !Val.getValue();
64   }
65 
66   /// Return true if the constrained is perfectly constrained.
isConstrained()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.
isUnderconstrained()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.
assumeDual(ProgramStateRef State,DefinedSVal Cond)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 
assumeInclusiveRangeDual(ProgramStateRef State,NonLoc Value,const llvm::APSInt & From,const llvm::APSInt & To)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.
getSymVal(ProgramStateRef state,SymbolRef sym)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 
EndPath(ProgramStateRef state)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.
isNull(ProgramStateRef State,SymbolRef Sym)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
210