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
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 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 {
57 return Val.hasValue() && Val.getValue();
58 }
59
60 /// Return true if the constraint is perfectly constrained to 'false'.
61 bool isConstrainedFalse() const {
62 return Val.hasValue() && !Val.getValue();
63 }
64
65 /// Return true if the constrained is perfectly constrained.
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.
72 bool isUnderconstrained() const {
73 return !Val.hasValue();
74 }
75};
76
77class ConstraintManager {
78public:
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.
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
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.
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.
167 ConditionTruthVal isNull(ProgramStateRef State, SymbolRef Sym) {
168 SaveAndRestore<bool> DisableNotify(NotifyAssumeClients, false);
169
170 return checkNull(State, Sym);
171 }
172
173protected:
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
194std::unique_ptr<ConstraintManager>
195CreateRangeConstraintManager(ProgramStateManager &statemgr,
196 ExprEngine *exprengine);
197
198std::unique_ptr<ConstraintManager>
199CreateZ3ConstraintManager(ProgramStateManager &statemgr,
200 ExprEngine *exprengine);
201
202} // namespace ento
203} // namespace clang
204
205#endif // LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_CONSTRAINTMANAGER_H
206