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 ExprEngine;
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.
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 {
57     return Val.hasValue() && Val.getValue();
58   }
59 
60   /// Return true if the constraint is perfectly constrained to 'false'.
isConstrainedFalse()61   bool isConstrainedFalse() const {
62     return Val.hasValue() && !Val.getValue();
63   }
64 
65   /// Return true if the constrained is perfectly constrained.
isConstrained()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.
isUnderconstrained()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.
assumeDual(ProgramStateRef State,DefinedSVal Cond)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 #ifdef EXPENSIVE_CHECKS
100       assert(assume(State, Cond, false) && "System is over constrained.");
101 #endif
102       return ProgramStatePair((ProgramStateRef)nullptr, State);
103     }
104 
105     ProgramStateRef StFalse = assume(State, Cond, false);
106     if (!StFalse) {
107       // We are careful to return the original state, /not/ StTrue,
108       // because we want to avoid having callers generate a new node
109       // in the ExplodedGraph.
110       return ProgramStatePair(State, (ProgramStateRef)nullptr);
111     }
112 
113     return ProgramStatePair(StTrue, StFalse);
114   }
115 
116   virtual ProgramStateRef assumeInclusiveRange(ProgramStateRef State,
117                                                NonLoc Value,
118                                                const llvm::APSInt &From,
119                                                const llvm::APSInt &To,
120                                                bool InBound) = 0;
121 
assumeInclusiveRangeDual(ProgramStateRef State,NonLoc Value,const llvm::APSInt & From,const llvm::APSInt & To)122   virtual ProgramStatePair assumeInclusiveRangeDual(ProgramStateRef State,
123                                                     NonLoc Value,
124                                                     const llvm::APSInt &From,
125                                                     const llvm::APSInt &To) {
126     ProgramStateRef StInRange =
127         assumeInclusiveRange(State, Value, From, To, true);
128 
129     // If StTrue is infeasible, asserting the falseness of Cond is unnecessary
130     // because the existing constraints already establish this.
131     if (!StInRange)
132       return ProgramStatePair((ProgramStateRef)nullptr, State);
133 
134     ProgramStateRef StOutOfRange =
135         assumeInclusiveRange(State, Value, From, To, false);
136     if (!StOutOfRange) {
137       // We are careful to return the original state, /not/ StTrue,
138       // because we want to avoid having callers generate a new node
139       // in the ExplodedGraph.
140       return ProgramStatePair(State, (ProgramStateRef)nullptr);
141     }
142 
143     return ProgramStatePair(StInRange, StOutOfRange);
144   }
145 
146   /// If a symbol is perfectly constrained to a constant, attempt
147   /// to return the concrete value.
148   ///
149   /// Note that a ConstraintManager is not obligated to return a concretized
150   /// value for a symbol, even if it is perfectly constrained.
getSymVal(ProgramStateRef state,SymbolRef sym)151   virtual const llvm::APSInt* getSymVal(ProgramStateRef state,
152                                         SymbolRef sym) const {
153     return nullptr;
154   }
155 
156   /// Scan all symbols referenced by the constraints. If the symbol is not
157   /// alive, remove it.
158   virtual ProgramStateRef removeDeadBindings(ProgramStateRef state,
159                                                  SymbolReaper& SymReaper) = 0;
160 
161   virtual void printJson(raw_ostream &Out, ProgramStateRef State,
162                          const char *NL, unsigned int Space,
163                          bool IsDot) const = 0;
164 
165   /// Convenience method to query the state to see if a symbol is null or
166   /// not null, or if neither assumption can be made.
isNull(ProgramStateRef State,SymbolRef Sym)167   ConditionTruthVal isNull(ProgramStateRef State, SymbolRef Sym) {
168     SaveAndRestore<bool> DisableNotify(NotifyAssumeClients, false);
169 
170     return checkNull(State, Sym);
171   }
172 
173 protected:
174   /// A flag to indicate that clients should be notified of assumptions.
175   /// By default this is the case, but sometimes this needs to be restricted
176   /// to avoid infinite recursions within the ConstraintManager.
177   ///
178   /// Note that this flag allows the ConstraintManager to be re-entrant,
179   /// but not thread-safe.
180   bool NotifyAssumeClients = true;
181 
182   /// canReasonAbout - Not all ConstraintManagers can accurately reason about
183   ///  all SVal values.  This method returns true if the ConstraintManager can
184   ///  reasonably handle a given SVal value.  This is typically queried by
185   ///  ExprEngine to determine if the value should be replaced with a
186   ///  conjured symbolic value in order to recover some precision.
187   virtual bool canReasonAbout(SVal X) const = 0;
188 
189   /// Returns whether or not a symbol is known to be null ("true"), known to be
190   /// non-null ("false"), or may be either ("underconstrained").
191   virtual ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym);
192 };
193 
194 std::unique_ptr<ConstraintManager>
195 CreateRangeConstraintManager(ProgramStateManager &statemgr,
196                              ExprEngine *exprengine);
197 
198 std::unique_ptr<ConstraintManager>
199 CreateZ3ConstraintManager(ProgramStateManager &statemgr,
200                           ExprEngine *exprengine);
201 
202 } // namespace ento
203 } // namespace clang
204 
205 #endif // LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_CONSTRAINTMANAGER_H
206