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_GR_CONSTRAINT_MANAGER_H
15#define LLVM_CLANG_GR_CONSTRAINT_MANAGER_H
16
17#include "clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h"
18#include "clang/StaticAnalyzer/Core/PathSensitive/SVals.h"
19
20namespace llvm {
21class APSInt;
22}
23
24namespace clang {
25namespace ento {
26
27class SubEngine;
28
29class ConditionTruthVal {
30  llvm::Optional<bool> Val;
31public:
32  /// Construct a ConditionTruthVal indicating the constraint is constrained
33  /// to either true or false, depending on the boolean value provided.
34  ConditionTruthVal(bool constraint) : Val(constraint) {}
35
36  /// Construct a ConstraintVal indicating the constraint is underconstrained.
37  ConditionTruthVal() {}
38
39  /// Return true if the constraint is perfectly constrained to 'true'.
40  bool isTrue() const {
41    return Val.hasValue() && Val.getValue();
42  }
43
44  /// Return true if the constraint is perfectly constrained to 'false'.
45  bool isFalse() const {
46    return Val.hasValue() && !Val.getValue();
47  }
48
49  /// Return true if the constrained is perfectly constrained.
50  bool isConstrained() const {
51    return Val.hasValue();
52  }
53
54  /// Return true if the constrained is underconstrained and we do not know
55  /// if the constraint is true of value.
56  bool isUnderconstrained() const {
57    return !Val.hasValue();
58  }
59};
60
61class ConstraintManager {
62public:
63  ConstraintManager() : NotifyAssumeClients(true) {}
64
65  virtual ~ConstraintManager();
66  virtual ProgramStateRef assume(ProgramStateRef state,
67                                 DefinedSVal Cond,
68                                 bool Assumption) = 0;
69
70  typedef std::pair<ProgramStateRef, ProgramStateRef> ProgramStatePair;
71
72  ProgramStatePair assumeDual(ProgramStateRef state, DefinedSVal Cond) {
73    ProgramStatePair res(assume(state, Cond, true),
74                         assume(state, Cond, false));
75    assert(!(!res.first && !res.second) && "System is over constrained.");
76    return res;
77  }
78
79  /// \brief If a symbol is perfectly constrained to a constant, attempt
80  /// to return the concrete value.
81  ///
82  /// Note that a ConstraintManager is not obligated to return a concretized
83  /// value for a symbol, even if it is perfectly constrained.
84  virtual const llvm::APSInt* getSymVal(ProgramStateRef state,
85                                        SymbolRef sym) const {
86    return 0;
87  }
88
89  virtual ProgramStateRef removeDeadBindings(ProgramStateRef state,
90                                                 SymbolReaper& SymReaper) = 0;
91
92  virtual void print(ProgramStateRef state,
93                     raw_ostream &Out,
94                     const char* nl,
95                     const char *sep) = 0;
96
97  virtual void EndPath(ProgramStateRef state) {}
98
99  /// Convenience method to query the state to see if a symbol is null or
100  /// not null, or neither assumption can be made.
101  ConditionTruthVal isNull(ProgramStateRef State, SymbolRef Sym);
102
103protected:
104  /// A flag to indicate that clients should be notified of assumptions.
105  /// By default this is the case, but sometimes this needs to be restricted
106  /// to avoid infinite recursions within the ConstraintManager.
107  ///
108  /// Note that this flag allows the ConstraintManager to be re-entrant,
109  /// but not thread-safe.
110  bool NotifyAssumeClients;
111
112  /// canReasonAbout - Not all ConstraintManagers can accurately reason about
113  ///  all SVal values.  This method returns true if the ConstraintManager can
114  ///  reasonably handle a given SVal value.  This is typically queried by
115  ///  ExprEngine to determine if the value should be replaced with a
116  ///  conjured symbolic value in order to recover some precision.
117  virtual bool canReasonAbout(SVal X) const = 0;
118};
119
120ConstraintManager* CreateRangeConstraintManager(ProgramStateManager& statemgr,
121                                                SubEngine &subengine);
122
123} // end GR namespace
124
125} // end clang namespace
126
127#endif
128