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