clang  15.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 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.
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.
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.
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.
70  bool Assumption) override;
71 
73  NonLoc Value,
74  const llvm::APSInt &From,
75  const llvm::APSInt &To,
76  bool InRange) override;
77 
78  SValBuilder &getSValBuilder() const { return SVB; }
80  SymbolManager &getSymbolManager() const { return SVB.getSymbolManager(); }
81 
82 private:
83  ProgramStateRef assume(ProgramStateRef State, NonLoc Cond, bool Assumption);
84 
86  bool Assumption);
87 };
88 
89 } // end namespace ento
90 
91 } // end namespace clang
92 
93 #endif
clang::ento::SimpleConstraintManager::assumeInclusiveRangeInternal
ProgramStateRef assumeInclusiveRangeInternal(ProgramStateRef State, NonLoc Value, const llvm::APSInt &From, const llvm::APSInt &To, bool InRange) override
Definition: SimpleConstraintManager.cpp:94
ConstraintManager.h
clang::ento::BasicValueFactory
Definition: BasicValueFactory.h:107
clang::ento::NonLoc
Definition: SVals.h:304
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:268
clang::ento::SimpleConstraintManager::getSValBuilder
SValBuilder & getSValBuilder() const
Definition: SimpleConstraintManager.h:78
clang::ento::SymExpr
Symbolic value.
Definition: SymExpr.h:29
clang::ento::SimpleConstraintManager::getBasicVals
BasicValueFactory & getBasicVals() const
Definition: SimpleConstraintManager.h:79
clang::ento::SValBuilder::getBasicValueFactory
BasicValueFactory & getBasicValueFactory()
Definition: SValBuilder.h:180
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::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:1090
clang::ento::SimpleConstraintManager::getSymbolManager
SymbolManager & getSymbolManager() const
Definition: SimpleConstraintManager.h:80
clang::ento::ExprEngine
Definition: ExprEngine.h:123
ProgramState.h
clang
Definition: CalledOnceCheck.h:17
clang::ento::SValBuilder::getSymbolManager
SymbolManager & getSymbolManager()
Definition: SValBuilder.h:183
clang::ento::SimpleConstraintManager
Definition: SimpleConstraintManager.h:23
clang::ento::SymbolManager
Definition: SymbolManager.h:417
clang::ento::SimpleConstraintManager::assumeInternal
ProgramStateRef assumeInternal(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
llvm::IntrusiveRefCntPtr
Definition: LLVM.h:47