Coverage Report

Created: 2018-09-19 20:53

/Users/buildslave/jenkins/workspace/clang-stage2-coverage-R/llvm/tools/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
//                     The LLVM Compiler Infrastructure
4
//
5
// This file is distributed under the University of Illinois Open Source
6
// License. See LICENSE.TXT for details.
7
//
8
//===----------------------------------------------------------------------===//
9
//
10
//  This file defined the interface to manage constraints on symbolic values.
11
//
12
//===----------------------------------------------------------------------===//
13
14
#ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_CONSTRAINTMANAGER_H
15
#define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_CONSTRAINTMANAGER_H
16
17
#include "clang/Basic/LLVM.h"
18
#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState_Fwd.h"
19
#include "clang/StaticAnalyzer/Core/PathSensitive/SVals.h"
20
#include "clang/StaticAnalyzer/Core/PathSensitive/SymExpr.h"
21
#include "llvm/ADT/Optional.h"
22
#include "llvm/Support/SaveAndRestore.h"
23
#include <memory>
24
#include <utility>
25
26
namespace llvm {
27
28
class APSInt;
29
30
} // namespace llvm
31
32
namespace clang {
33
namespace ento {
34
35
class ProgramStateManager;
36
class SubEngine;
37
class SymbolReaper;
38
39
class ConditionTruthVal {
40
  Optional<bool> Val;
41
42
public:
43
  /// Construct a ConditionTruthVal indicating the constraint is constrained
44
  /// to either true or false, depending on the boolean value provided.
45
0
  ConditionTruthVal(bool constraint) : Val(constraint) {}
46
47
  /// Construct a ConstraintVal indicating the constraint is underconstrained.
48
0
  ConditionTruthVal() = default;
49
50
  /// \return Stored value, assuming that the value is known.
51
  /// Crashes otherwise.
52
0
  bool getValue() const {
53
0
    return *Val;
54
0
  }
55
56
  /// Return true if the constraint is perfectly constrained to 'true'.
57
0
  bool isConstrainedTrue() const {
58
0
    return Val.hasValue() && Val.getValue();
59
0
  }
60
61
  /// Return true if the constraint is perfectly constrained to 'false'.
62
0
  bool isConstrainedFalse() const {
63
0
    return Val.hasValue() && !Val.getValue();
64
0
  }
65
66
  /// Return true if the constrained is perfectly constrained.
67
  bool isConstrained() const {
68
    return Val.hasValue();
69
  }
70
71
  /// Return true if the constrained is underconstrained and we do not know
72
  /// if the constraint is true of value.
73
0
  bool isUnderconstrained() const {
74
0
    return !Val.hasValue();
75
0
  }
76
};
77
78
class ConstraintManager {
79
public:
80
0
  ConstraintManager() = default;
81
  virtual ~ConstraintManager();
82
83
  virtual ProgramStateRef assume(ProgramStateRef state,
84
                                 DefinedSVal Cond,
85
                                 bool Assumption) = 0;
86
87
  using ProgramStatePair = std::pair<ProgramStateRef, ProgramStateRef>;
88
89
  /// Returns a pair of states (StTrue, StFalse) where the given condition is
90
  /// assumed to be true or false, respectively.
91
0
  ProgramStatePair assumeDual(ProgramStateRef State, DefinedSVal Cond) {
92
0
    ProgramStateRef StTrue = assume(State, Cond, true);
93
0
94
0
    // If StTrue is infeasible, asserting the falseness of Cond is unnecessary
95
0
    // because the existing constraints already establish this.
96
0
    if (!StTrue) {
97
0
#ifndef __OPTIMIZE__
98
0
      // This check is expensive and should be disabled even in Release+Asserts
99
0
      // builds.
100
0
      // FIXME: __OPTIMIZE__ is a GNU extension that Clang implements but MSVC
101
0
      // does not. Is there a good equivalent there?
102
0
      assert(assume(State, Cond, false) && "System is over constrained.");
103
0
#endif
104
0
      return ProgramStatePair((ProgramStateRef)nullptr, State);
105
0
    }
106
0
107
0
    ProgramStateRef StFalse = assume(State, Cond, false);
108
0
    if (!StFalse) {
109
0
      // We are careful to return the original state, /not/ StTrue,
110
0
      // because we want to avoid having callers generate a new node
111
0
      // in the ExplodedGraph.
112
0
      return ProgramStatePair(State, (ProgramStateRef)nullptr);
113
0
    }
114
0
115
0
    return ProgramStatePair(StTrue, StFalse);
116
0
  }
117
118
  virtual ProgramStateRef assumeInclusiveRange(ProgramStateRef State,
119
                                               NonLoc Value,
120
                                               const llvm::APSInt &From,
121
                                               const llvm::APSInt &To,
122
                                               bool InBound) = 0;
123
124
  virtual ProgramStatePair assumeInclusiveRangeDual(ProgramStateRef State,
125
                                                    NonLoc Value,
126
                                                    const llvm::APSInt &From,
127
0
                                                    const llvm::APSInt &To) {
128
0
    ProgramStateRef StInRange =
129
0
        assumeInclusiveRange(State, Value, From, To, true);
130
0
131
0
    // If StTrue is infeasible, asserting the falseness of Cond is unnecessary
132
0
    // because the existing constraints already establish this.
133
0
    if (!StInRange)
134
0
      return ProgramStatePair((ProgramStateRef)nullptr, State);
135
0
136
0
    ProgramStateRef StOutOfRange =
137
0
        assumeInclusiveRange(State, Value, From, To, false);
138
0
    if (!StOutOfRange) {
139
0
      // We are careful to return the original state, /not/ StTrue,
140
0
      // because we want to avoid having callers generate a new node
141
0
      // in the ExplodedGraph.
142
0
      return ProgramStatePair(State, (ProgramStateRef)nullptr);
143
0
    }
144
0
145
0
    return ProgramStatePair(StInRange, StOutOfRange);
146
0
  }
147
148
  /// If a symbol is perfectly constrained to a constant, attempt
149
  /// to return the concrete value.
150
  ///
151
  /// Note that a ConstraintManager is not obligated to return a concretized
152
  /// value for a symbol, even if it is perfectly constrained.
153
  virtual const llvm::APSInt* getSymVal(ProgramStateRef state,
154
0
                                        SymbolRef sym) const {
155
0
    return nullptr;
156
0
  }
157
158
  /// Scan all symbols referenced by the constraints. If the symbol is not
159
  /// alive, remove it.
160
  virtual ProgramStateRef removeDeadBindings(ProgramStateRef state,
161
                                                 SymbolReaper& SymReaper) = 0;
162
163
  virtual void print(ProgramStateRef state,
164
                     raw_ostream &Out,
165
                     const char* nl,
166
                     const char *sep) = 0;
167
168
0
  virtual void EndPath(ProgramStateRef state) {}
169
170
  /// Convenience method to query the state to see if a symbol is null or
171
  /// not null, or if neither assumption can be made.
172
0
  ConditionTruthVal isNull(ProgramStateRef State, SymbolRef Sym) {
173
0
    SaveAndRestore<bool> DisableNotify(NotifyAssumeClients, false);
174
0
175
0
    return checkNull(State, Sym);
176
0
  }
177
178
protected:
179
  /// A flag to indicate that clients should be notified of assumptions.
180
  /// By default this is the case, but sometimes this needs to be restricted
181
  /// to avoid infinite recursions within the ConstraintManager.
182
  ///
183
  /// Note that this flag allows the ConstraintManager to be re-entrant,
184
  /// but not thread-safe.
185
  bool NotifyAssumeClients = true;
186
187
  /// canReasonAbout - Not all ConstraintManagers can accurately reason about
188
  ///  all SVal values.  This method returns true if the ConstraintManager can
189
  ///  reasonably handle a given SVal value.  This is typically queried by
190
  ///  ExprEngine to determine if the value should be replaced with a
191
  ///  conjured symbolic value in order to recover some precision.
192
  virtual bool canReasonAbout(SVal X) const = 0;
193
194
  /// Returns whether or not a symbol is known to be null ("true"), known to be
195
  /// non-null ("false"), or may be either ("underconstrained").
196
  virtual ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym);
197
};
198
199
std::unique_ptr<ConstraintManager>
200
CreateRangeConstraintManager(ProgramStateManager &statemgr,
201
                             SubEngine *subengine);
202
203
std::unique_ptr<ConstraintManager>
204
CreateZ3ConstraintManager(ProgramStateManager &statemgr, SubEngine *subengine);
205
206
} // namespace ento
207
} // namespace clang
208
209
#endif // LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_CONSTRAINTMANAGER_H