SimpleConstraintManager.h revision 341825
1//== SimpleConstraintManager.h ----------------------------------*- 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//  Simplified constraint manager backend.
11//
12//===----------------------------------------------------------------------===//
13
14#ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SIMPLECONSTRAINTMANAGER_H
15#define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SIMPLECONSTRAINTMANAGER_H
16
17#include "clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h"
18#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
19
20namespace clang {
21
22namespace ento {
23
24class SimpleConstraintManager : public ConstraintManager {
25  SubEngine *SU;
26  SValBuilder &SVB;
27
28public:
29  SimpleConstraintManager(SubEngine *subengine, SValBuilder &SB)
30      : SU(subengine), SVB(SB) {}
31
32  ~SimpleConstraintManager() override;
33
34  //===------------------------------------------------------------------===//
35  // Implementation for interface from ConstraintManager.
36  //===------------------------------------------------------------------===//
37
38  /// Ensures that the DefinedSVal conditional is expressed as a NonLoc by
39  /// creating boolean casts to handle Loc's.
40  ProgramStateRef assume(ProgramStateRef State, DefinedSVal Cond,
41                         bool Assumption) override;
42
43  ProgramStateRef assumeInclusiveRange(ProgramStateRef State, NonLoc Value,
44                                       const llvm::APSInt &From,
45                                       const llvm::APSInt &To,
46                                       bool InRange) override;
47
48protected:
49  //===------------------------------------------------------------------===//
50  // Interface that subclasses must implement.
51  //===------------------------------------------------------------------===//
52
53  /// Given a symbolic expression that can be reasoned about, assume that it is
54  /// true/false and generate the new program state.
55  virtual ProgramStateRef assumeSym(ProgramStateRef State, SymbolRef Sym,
56                                    bool Assumption) = 0;
57
58  /// Given a symbolic expression within the range [From, To], assume that it is
59  /// true/false and generate the new program state.
60  /// This function is used to handle case ranges produced by a language
61  /// extension for switch case statements.
62  virtual ProgramStateRef assumeSymInclusiveRange(ProgramStateRef State,
63                                                  SymbolRef Sym,
64                                                  const llvm::APSInt &From,
65                                                  const llvm::APSInt &To,
66                                                  bool InRange) = 0;
67
68  /// Given a symbolic expression that cannot be reasoned about, assume that
69  /// it is zero/nonzero and add it directly to the solver state.
70  virtual ProgramStateRef assumeSymUnsupported(ProgramStateRef State,
71                                               SymbolRef Sym,
72                                               bool Assumption) = 0;
73
74  //===------------------------------------------------------------------===//
75  // Internal implementation.
76  //===------------------------------------------------------------------===//
77
78  SValBuilder &getSValBuilder() const { return SVB; }
79  BasicValueFactory &getBasicVals() const { return SVB.getBasicValueFactory(); }
80  SymbolManager &getSymbolManager() const { return SVB.getSymbolManager(); }
81
82private:
83  ProgramStateRef assume(ProgramStateRef State, NonLoc Cond, bool Assumption);
84
85  ProgramStateRef assumeAux(ProgramStateRef State, NonLoc Cond,
86                            bool Assumption);
87};
88
89} // end namespace ento
90
91} // end namespace clang
92
93#endif
94