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 {
25
26namespace ento {
27
28class ProgramState;
29class ProgramStateManager;
30class SubEngine;
31
32class ConstraintManager {
33public:
34  virtual ~ConstraintManager();
35  virtual const ProgramState *assume(const ProgramState *state,
36                                     DefinedSVal Cond,
37                                     bool Assumption) = 0;
38
39  std::pair<const ProgramState*, const ProgramState*>
40    assumeDual(const ProgramState *state, DefinedSVal Cond)
41  {
42    return std::make_pair(assume(state, Cond, true),
43                          assume(state, Cond, false));
44  }
45
46  virtual const llvm::APSInt* getSymVal(const ProgramState *state,
47                                        SymbolRef sym) const = 0;
48
49  virtual bool isEqual(const ProgramState *state,
50                       SymbolRef sym,
51                       const llvm::APSInt& V) const = 0;
52
53  virtual const ProgramState *removeDeadBindings(const ProgramState *state,
54                                                 SymbolReaper& SymReaper) = 0;
55
56  virtual void print(const ProgramState *state,
57                     raw_ostream &Out,
58                     const char* nl,
59                     const char *sep) = 0;
60
61  virtual void EndPath(const ProgramState *state) {}
62
63  /// canReasonAbout - Not all ConstraintManagers can accurately reason about
64  ///  all SVal values.  This method returns true if the ConstraintManager can
65  ///  reasonably handle a given SVal value.  This is typically queried by
66  ///  ExprEngine to determine if the value should be replaced with a
67  ///  conjured symbolic value in order to recover some precision.
68  virtual bool canReasonAbout(SVal X) const = 0;
69};
70
71ConstraintManager* CreateBasicConstraintManager(ProgramStateManager& statemgr,
72                                                SubEngine &subengine);
73ConstraintManager* CreateRangeConstraintManager(ProgramStateManager& statemgr,
74                                                SubEngine &subengine);
75
76} // end GR namespace
77
78} // end clang namespace
79
80#endif
81