Coverage Report

Created: 2020-09-19 12:23

/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
58.0k
  ConditionTruthVal(bool constraint) : Val(constraint) {}
45
46
  /// Construct a ConstraintVal indicating the constraint is underconstrained.
47
41.7k
  ConditionTruthVal() = default;
48
49
  /// \return Stored value, assuming that the value is known.
50
  /// Crashes otherwise.
51
15.1k
  bool getValue() const {
52
15.1k
    return *Val;
53
15.1k
  }
54
55
  /// Return true if the constraint is perfectly constrained to 'true'.
56
76.9k
  bool isConstrainedTrue() const {
57
76.9k
    return Val.hasValue() && 
Val.getValue()36.1k
;
58
76.9k
  }
59
60
  /// Return true if the constraint is perfectly constrained to 'false'.
61
1.72k
  bool isConstrainedFalse() const {
62
1.72k
    return Val.hasValue() && 
!Val.getValue()911
;
63
1.72k
  }
64
65
  /// Return true if the constrained is perfectly constrained.
66
24
  bool isConstrained() const {
67
24
    return Val.hasValue();
68
24
  }
69
70
  /// Return true if the constrained is underconstrained and we do not know
71
  /// if the constraint is true of value.
72
28.7k
  bool isUnderconstrained() const {
73
28.7k
    return !Val.hasValue();
74
28.7k
  }
75
};
76
77
class ConstraintManager {
78
public:
79
13.6k
  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
362k
  ProgramStatePair assumeDual(ProgramStateRef State, DefinedSVal Cond) {
94
362k
    ProgramStateRef StTrue = assume(State, Cond, true);
95
362k
96
    // If StTrue is infeasible, asserting the falseness of Cond is unnecessary
97
    // because the existing constraints already establish this.
98
362k
    if (!StTrue) {
99
#ifdef EXPENSIVE_CHECKS
100
      assert(assume(State, Cond, false) && "System is over constrained.");
101
#endif
102
17.0k
      return ProgramStatePair((ProgramStateRef)nullptr, State);
103
17.0k
    }
104
345k
105
345k
    ProgramStateRef StFalse = assume(State, Cond, false);
106
345k
    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
305k
      return ProgramStatePair(State, (ProgramStateRef)nullptr);
111
305k
    }
112
39.8k
113
39.8k
    return ProgramStatePair(StTrue, StFalse);
114
39.8k
  }
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
617
                                                    const llvm::APSInt &To) {
126
617
    ProgramStateRef StInRange =
127
617
        assumeInclusiveRange(State, Value, From, To, true);
128
617
129
    // If StTrue is infeasible, asserting the falseness of Cond is unnecessary
130
    // because the existing constraints already establish this.
131
617
    if (!StInRange)
132
165
      return ProgramStatePair((ProgramStateRef)nullptr, State);
133
452
134
452
    ProgramStateRef StOutOfRange =
135
452
        assumeInclusiveRange(State, Value, From, To, false);
136
452
    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
120
      return ProgramStatePair(State, (ProgramStateRef)nullptr);
141
120
    }
142
332
143
332
    return ProgramStatePair(StInRange, StOutOfRange);
144
332
  }
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
0
                                        SymbolRef sym) const {
153
0
    return nullptr;
154
0
  }
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
57.1k
  ConditionTruthVal isNull(ProgramStateRef State, SymbolRef Sym) {
168
57.1k
    SaveAndRestore<bool> DisableNotify(NotifyAssumeClients, false);
169
57.1k
170
57.1k
    return checkNull(State, Sym);
171
57.1k
  }
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