clang  14.0.0git
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  ExprEngine *EE;
25  SValBuilder &SVB;
26 
27 public:
29  : EE(exprengine), 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 
85  bool Assumption);
86 };
87 
88 } // end namespace ento
89 
90 } // end namespace clang
91 
92 #endif
ConstraintManager.h
clang::ento::BasicValueFactory
Definition: BasicValueFactory.h:108
clang::ento::NonLoc
Definition: SVals.h:305
clang::ento::ConstraintManager
Definition: ConstraintManager.h:77
clang::ento::SimpleConstraintManager::assumeSymUnsupported
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 ...
APSInt
llvm::APSInt APSInt
Definition: ByteCodeEmitter.cpp:19
clang::ento::SimpleConstraintManager::SimpleConstraintManager
SimpleConstraintManager(ExprEngine *exprengine, SValBuilder &SB)
Definition: SimpleConstraintManager.h:28
clang::ento::DefinedSVal
Definition: SVals.h:269
clang::ento::SimpleConstraintManager::getSValBuilder
SValBuilder & getSValBuilder() const
Definition: SimpleConstraintManager.h:77
clang::ento::SymExpr
Symbolic value.
Definition: SymExpr.h:29
clang::ento::SimpleConstraintManager::getBasicVals
BasicValueFactory & getBasicVals() const
Definition: SimpleConstraintManager.h:78
clang::ento::SValBuilder::getBasicValueFactory
BasicValueFactory & getBasicValueFactory()
Definition: SValBuilder.h:181
clang::ento::SimpleConstraintManager::assumeInclusiveRange
ProgramStateRef assumeInclusiveRange(ProgramStateRef State, NonLoc Value, const llvm::APSInt &From, const llvm::APSInt &To, bool InRange) override
Definition: SimpleConstraintManager.cpp:94
clang::interp::InRange
bool InRange(InterpState &S, CodePtr OpPC)
Definition: Interp.h:266
clang::ento::SimpleConstraintManager::~SimpleConstraintManager
~SimpleConstraintManager() override
Definition: SimpleConstraintManager.cpp:23
clang::ento::SValBuilder
Definition: SValBuilder.h:53
clang::ento::SimpleConstraintManager::assumeSymInclusiveRange
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...
Value
Value
Definition: UninitializedValues.cpp:102
clang::ento::SimpleConstraintManager::assume
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...
Definition: SimpleConstraintManager.cpp:25
clang::ento::SimpleConstraintManager::assumeSym
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...
State
LineState State
Definition: UnwrappedLineFormatter.cpp:986
clang::ento::SimpleConstraintManager::getSymbolManager
SymbolManager & getSymbolManager() const
Definition: SimpleConstraintManager.h:79
clang::ento::ExprEngine
Definition: ExprEngine.h:127
ProgramState.h
clang
Definition: CalledOnceCheck.h:17
clang::ento::SValBuilder::getSymbolManager
SymbolManager & getSymbolManager()
Definition: SValBuilder.h:184
clang::ento::SimpleConstraintManager
Definition: SimpleConstraintManager.h:23
clang::ento::SymbolManager
Definition: SymbolManager.h:417
llvm::IntrusiveRefCntPtr
Definition: LLVM.h:47