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
25namespace llvm {
26
27class APSInt;
28
29} // namespace llvm
30
31namespace clang {
32namespace ento {
33
34class ProgramStateManager;
35class ExprEngine;
36class SymbolReaper;
37
38class ConditionTruthVal {
39 std::optional<bool> Val;
40
41public:
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 { return Val && *Val; }
57
58 /// Return true if the constraint is perfectly constrained to 'false'.
59 bool isConstrainedFalse() const { return Val && !*Val; }
60
61 /// Return true if the constrained is perfectly constrained.
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.
66 bool isUnderconstrained() const { return !Val.has_value(); }
67};
68
69class ConstraintManager {
70public:
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.
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.
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.
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
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.
143 ConditionTruthVal isNull(ProgramStateRef State, SymbolRef Sym) {
144 return checkNull(State, Sym);
145 }
146
147protected:
148 /// A helper class to simulate the call stack of nested assume calls.
149 class AssumeStackTy {
150 public:
151 void push(const ProgramState *S) { Aux.push_back(Elt: S); }
152 void pop() { Aux.pop_back(); }
153 bool contains(const ProgramState *S) const {
154 return llvm::is_contained(Range: Aux, Element: 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
187std::unique_ptr<ConstraintManager>
188CreateRangeConstraintManager(ProgramStateManager &statemgr,
189 ExprEngine *exprengine);
190
191std::unique_ptr<ConstraintManager>
192CreateZ3ConstraintManager(ProgramStateManager &statemgr,
193 ExprEngine *exprengine);
194
195} // namespace ento
196} // namespace clang
197
198#endif // LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_CONSTRAINTMANAGER_H
199

source code of clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h