clang 20.0.0git
ConstraintManager.h
Go to the documentation of this file.
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"
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
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
70public:
71 ConstraintManager() = default;
73
75 ProgramStateRef S2) const = 0;
76
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.)
88
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.)
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.
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.
144 return checkNull(State, Sym);
145 }
146
147protected:
148 /// A helper class to simulate the call stack of nested assume calls.
150 public:
151 void push(const ProgramState *S) { Aux.push_back(S); }
152 void pop() { Aux.pop_back(); }
153 bool contains(const ProgramState *S) const {
154 return llvm::is_contained(Aux, S);
155 }
156
157 private:
159 };
161
163 DefinedSVal Cond, bool Assumption) = 0;
164
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").
181
182 template <typename AssumeFunction>
184 AssumeFunction &Assume);
185};
186
187std::unique_ptr<ConstraintManager>
189 ExprEngine *exprengine);
190
191std::unique_ptr<ConstraintManager>
193 ExprEngine *exprengine);
194
195} // namespace ento
196} // namespace clang
197
198#endif // LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_CONSTRAINTMANAGER_H
llvm::APSInt APSInt
Definition: Compiler.cpp:22
#define X(type, name)
Definition: Value.h:143
Forward-declares and imports various common LLVM datatypes that clang wants to use unqualified.
bool isUnderconstrained() const
Return true if the constrained is underconstrained and we do not know if the constraint is true of va...
ConditionTruthVal()=default
Construct a ConstraintVal indicating the constraint is underconstrained.
bool isConstrainedFalse() const
Return true if the constraint is perfectly constrained to 'false'.
bool isConstrained() const
Return true if the constrained is perfectly constrained.
ConditionTruthVal(bool constraint)
Construct a ConditionTruthVal indicating the constraint is constrained to either true or false,...
bool isConstrainedTrue() const
Return true if the constraint is perfectly constrained to 'true'.
A helper class to simulate the call stack of nested assume calls.
bool contains(const ProgramState *S) const
virtual ProgramStateRef assumeInclusiveRangeInternal(ProgramStateRef State, NonLoc Value, const llvm::APSInt &From, const llvm::APSInt &To, bool InBound)=0
virtual const llvm::APSInt * getSymMaxVal(ProgramStateRef state, SymbolRef sym) const
Attempt to return the minimal possible value for a given symbol.
ProgramStateRef assumeInclusiveRange(ProgramStateRef State, NonLoc Value, const llvm::APSInt &From, const llvm::APSInt &To, bool InBound)
virtual const llvm::APSInt * getSymVal(ProgramStateRef state, SymbolRef sym) const
If a symbol is perfectly constrained to a constant, attempt to return the concrete value.
virtual void printValue(raw_ostream &Out, ProgramStateRef State, SymbolRef Sym)
virtual bool canReasonAbout(SVal X) const =0
canReasonAbout - Not all ConstraintManagers can accurately reason about all SVal values.
ProgramStatePair assumeDual(ProgramStateRef State, DefinedSVal Cond)
Returns a pair of states (StTrue, StFalse) where the given condition is assumed to be true or false,...
virtual void printJson(raw_ostream &Out, ProgramStateRef State, const char *NL, unsigned int Space, bool IsDot) const =0
ConditionTruthVal isNull(ProgramStateRef State, SymbolRef Sym)
Convenience method to query the state to see if a symbol is null or not null, or if neither assumptio...
virtual ProgramStateRef removeDeadBindings(ProgramStateRef state, SymbolReaper &SymReaper)=0
Scan all symbols referenced by the constraints.
virtual const llvm::APSInt * getSymMinVal(ProgramStateRef state, SymbolRef sym) const
Attempt to return the minimal possible value for a given symbol.
ProgramStatePair assumeInclusiveRangeDual(ProgramStateRef State, NonLoc Value, const llvm::APSInt &From, const llvm::APSInt &To)
Returns a pair of states (StInRange, StOutOfRange) where the given value is assumed to be in the rang...
std::pair< ProgramStateRef, ProgramStateRef > ProgramStatePair
ProgramStateRef assume(ProgramStateRef state, DefinedSVal Cond, bool Assumption)
ProgramStatePair assumeDualImpl(ProgramStateRef &State, AssumeFunction &Assume)
virtual ProgramStateRef assumeInternal(ProgramStateRef state, DefinedSVal Cond, bool Assumption)=0
virtual bool haveEqualConstraints(ProgramStateRef S1, ProgramStateRef S2) const =0
virtual ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym)
Returns whether or not a symbol is known to be null ("true"), known to be non-null ("false"),...
ProgramState - This class encapsulates:
Definition: ProgramState.h:71
SVal - This represents a symbolic expression, which can be either an L-value or an R-value.
Definition: SVals.h:55
Symbolic value.
Definition: SymExpr.h:30
A class responsible for cleaning up unused symbols.
std::unique_ptr< ConstraintManager > CreateZ3ConstraintManager(ProgramStateManager &statemgr, ExprEngine *exprengine)
std::unique_ptr< ConstraintManager > CreateRangeConstraintManager(ProgramStateManager &statemgr, ExprEngine *exprengine)
The JSON file list parser is used to communicate input to InstallAPI.
Diagnostic wrappers for TextAPI types for error reporting.
Definition: Dominators.h:30