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 
20 namespace clang {
21 
22 namespace ento {
23 
24 class SimpleConstraintManager : public ConstraintManager {
25   SubEngine *SU;
26   SValBuilder &SVB;
27 
28 public:
SimpleConstraintManager(SubEngine * subengine,SValBuilder & SB)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 
48 protected:
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 
getSValBuilder()78   SValBuilder &getSValBuilder() const { return SVB; }
getBasicVals()79   BasicValueFactory &getBasicVals() const { return SVB.getBasicValueFactory(); }
getSymbolManager()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