clang  10.0.0svn
SimpleConstraintManager.h
Go to the documentation of this file.
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 
18 
19 namespace clang {
20 
21 namespace ento {
22 
24  SubEngine *SU;
25  SValBuilder &SVB;
26 
27 public:
29  : SU(subengine), SVB(SB) {}
30 
31  ~SimpleConstraintManager() override;
32 
33  //===------------------------------------------------------------------===//
34  // Implementation for interface from ConstraintManager.
35  //===------------------------------------------------------------------===//
36 
37  /// Ensures that the DefinedSVal conditional is expressed as a NonLoc by
38  /// creating boolean casts to handle Loc's.
40  bool Assumption) override;
41 
43  const llvm::APSInt &From,
44  const llvm::APSInt &To,
45  bool InRange) override;
46 
47 protected:
48  //===------------------------------------------------------------------===//
49  // Interface that subclasses must implement.
50  //===------------------------------------------------------------------===//
51 
52  /// Given a symbolic expression that can be reasoned about, assume that it is
53  /// true/false and generate the new program state.
55  bool Assumption) = 0;
56 
57  /// Given a symbolic expression within the range [From, To], assume that it is
58  /// true/false and generate the new program state.
59  /// This function is used to handle case ranges produced by a language
60  /// extension for switch case statements.
62  SymbolRef Sym,
63  const llvm::APSInt &From,
64  const llvm::APSInt &To,
65  bool InRange) = 0;
66 
67  /// Given a symbolic expression that cannot be reasoned about, assume that
68  /// it is zero/nonzero and add it directly to the solver state.
70  SymbolRef Sym,
71  bool Assumption) = 0;
72 
73  //===------------------------------------------------------------------===//
74  // Internal implementation.
75  //===------------------------------------------------------------------===//
76 
77  SValBuilder &getSValBuilder() const { return SVB; }
79  SymbolManager &getSymbolManager() const { return SVB.getSymbolManager(); }
80 
81 private:
82  ProgramStateRef assume(ProgramStateRef State, NonLoc Cond, bool Assumption);
83 
84  ProgramStateRef assumeAux(ProgramStateRef State, NonLoc Cond,
85  bool Assumption);
86 };
87 
88 } // end namespace ento
89 
90 } // end namespace clang
91 
92 #endif
SymbolManager & getSymbolManager()
Definition: SValBuilder.h:171
virtual ProgramStateRef assumeSymUnsupported(ProgramStateRef State, SymbolRef Sym, bool Assumption)=0
Given a symbolic expression that cannot be reasoned about, assume that it is zero/nonzero and add it ...
Symbolic value.
Definition: SymExpr.h:29
LineState State
SimpleConstraintManager(SubEngine *subengine, SValBuilder &SB)
ProgramStateRef assumeInclusiveRange(ProgramStateRef State, NonLoc Value, const llvm::APSInt &From, const llvm::APSInt &To, bool InRange) override
virtual ProgramStateRef assumeSym(ProgramStateRef State, SymbolRef Sym, bool Assumption)=0
Given a symbolic expression that can be reasoned about, assume that it is true/false and generate the...
BasicValueFactory & getBasicVals() const
ProgramStateRef assume(ProgramStateRef State, DefinedSVal Cond, bool Assumption) override
Ensures that the DefinedSVal conditional is expressed as a NonLoc by creating boolean casts to handle...
virtual ProgramStateRef assumeSymInclusiveRange(ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From, const llvm::APSInt &To, bool InRange)=0
Given a symbolic expression within the range [From, To], assume that it is true/false and generate th...
llvm::APSInt APSInt
bool InRange(InterpState &S, CodePtr OpPC)
Definition: Interp.h:267
Dataflow Directional Tag Classes.
BasicValueFactory & getBasicValueFactory()
Definition: SValBuilder.h:168