Coverage Report

Created: 2022-07-16 07:03

/Users/buildslave/jenkins/workspace/coverage/llvm-project/clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
Line
Count
Source (jump to first uncovered line)
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.
44
72.4k
  ConditionTruthVal(bool constraint) : Val(constraint) {}
45
46
  /// Construct a ConstraintVal indicating the constraint is underconstrained.
47
47.8k
  ConditionTruthVal() = default;
48
49
  /// \return Stored value, assuming that the value is known.
50
  /// Crashes otherwise.
51
18.6k
  bool getValue() const {
52
18.6k
    return *Val;
53
18.6k
  }
54
55
  /// Return true if the constraint is perfectly constrained to 'true'.
56
93.5k
  bool isConstrainedTrue() const { return Val && 
Val.value()46.7k
; }
57
58
  /// Return true if the constraint is perfectly constrained to 'false'.
59
1.81k
  bool isConstrainedFalse() const { return Val && 
!Val.value()915
; }
60
61
  /// Return true if the constrained is perfectly constrained.
62
24
  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
33.1k
  bool isUnderconstrained() const { return !Val.has_value(); }
67
};
68
69
class ConstraintManager {
70
public:
71
15.6k
  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
0
                                        SymbolRef sym) const {
110
0
    return nullptr;
111
0
  }
112
113
  /// Scan all symbols referenced by the constraints. If the symbol is not
114
  /// alive, remove it.
115
  virtual ProgramStateRef removeDeadBindings(ProgramStateRef state,
116
                                                 SymbolReaper& SymReaper) = 0;
117
118
  virtual void printJson(raw_ostream &Out, ProgramStateRef State,
119
                         const char *NL, unsigned int Space,
120
                         bool IsDot) const = 0;
121
122
  virtual void printValue(raw_ostream &Out, ProgramStateRef State,
123
0
                          SymbolRef Sym) {}
124
125
  /// Convenience method to query the state to see if a symbol is null or
126
  /// not null, or if neither assumption can be made.
127
66.6k
  ConditionTruthVal isNull(ProgramStateRef State, SymbolRef Sym) {
128
66.6k
    return checkNull(State, Sym);
129
66.6k
  }
130
131
protected:
132
  /// A helper class to simulate the call stack of nested assume calls.
133
  class AssumeStackTy {
134
  public:
135
629k
    void push(const ProgramState *S) { Aux.push_back(S); }
136
629k
    void pop() { Aux.pop_back(); }
137
629k
    bool contains(const ProgramState *S) const {
138
629k
      return llvm::is_contained(Aux, S);
139
629k
    }
140
141
  private:
142
    llvm::SmallVector<const ProgramState *, 4> Aux;
143
  };
144
  AssumeStackTy AssumeStack;
145
146
  virtual ProgramStateRef assumeInternal(ProgramStateRef state,
147
                                         DefinedSVal Cond, bool Assumption) = 0;
148
149
  virtual ProgramStateRef assumeInclusiveRangeInternal(ProgramStateRef State,
150
                                                       NonLoc Value,
151
                                                       const llvm::APSInt &From,
152
                                                       const llvm::APSInt &To,
153
                                                       bool InBound) = 0;
154
155
  /// canReasonAbout - Not all ConstraintManagers can accurately reason about
156
  ///  all SVal values.  This method returns true if the ConstraintManager can
157
  ///  reasonably handle a given SVal value.  This is typically queried by
158
  ///  ExprEngine to determine if the value should be replaced with a
159
  ///  conjured symbolic value in order to recover some precision.
160
  virtual bool canReasonAbout(SVal X) const = 0;
161
162
  /// Returns whether or not a symbol is known to be null ("true"), known to be
163
  /// non-null ("false"), or may be either ("underconstrained").
164
  virtual ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym);
165
166
  template <typename AssumeFunction>
167
  ProgramStatePair assumeDualImpl(ProgramStateRef &State,
168
                                  AssumeFunction &Assume);
169
};
170
171
std::unique_ptr<ConstraintManager>
172
CreateRangeConstraintManager(ProgramStateManager &statemgr,
173
                             ExprEngine *exprengine);
174
175
std::unique_ptr<ConstraintManager>
176
CreateZ3ConstraintManager(ProgramStateManager &statemgr,
177
                          ExprEngine *exprengine);
178
179
} // namespace ento
180
} // namespace clang
181
182
#endif // LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_CONSTRAINTMANAGER_H