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