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/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
38class ConditionTruthVal {
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
69class ConstraintManager {
70public:
71  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                                        SymbolRef sym) const {
110    return nullptr;
111  }
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                          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  ConditionTruthVal isNull(ProgramStateRef State, SymbolRef Sym) {
128    return checkNull(State, Sym);
129  }
130
131protected:
132  /// A helper class to simulate the call stack of nested assume calls.
133  class AssumeStackTy {
134  public:
135    void push(const ProgramState *S) { Aux.push_back(S); }
136    void pop() { Aux.pop_back(); }
137    bool contains(const ProgramState *S) const {
138      return llvm::is_contained(Aux, S);
139    }
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
171std::unique_ptr<ConstraintManager>
172CreateRangeConstraintManager(ProgramStateManager &statemgr,
173                             ExprEngine *exprengine);
174
175std::unique_ptr<ConstraintManager>
176CreateZ3ConstraintManager(ProgramStateManager &statemgr,
177                          ExprEngine *exprengine);
178
179} // namespace ento
180} // namespace clang
181
182#endif // LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_CONSTRAINTMANAGER_H
183