clang: include/clang/Analysis/FlowSensitive/Formula.h Source File (original) (raw)
1
2
3
4
5
6
7
8
9#ifndef LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_FORMULA_H
10#define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_FORMULA_H
11
13#include "llvm/ADT/ArrayRef.h"
14#include "llvm/ADT/DenseMap.h"
15#include "llvm/ADT/DenseMapInfo.h"
16#include "llvm/Support/Allocator.h"
17#include "llvm/Support/raw_ostream.h"
18#include
19#include
20
22
23
24
25
26
27
28
29
30
31
32
33
34enum class Atom : unsigned {};
35
36
37
38
39
40
41
42
43
44
45
46
47
48class Formula;
49class alignas(const Formula *) Formula {
50public:
52
53
55
57
59
60
65 };
66 Kind kind() const { return FormulaKind; }
67
71 }
72
75 return static_cast<bool>(Value);
76 }
77
80 }
81
83 return ArrayRef(reinterpret_cast<Formula *const *>(this + 1),
84 numOperands(kind()));
85 }
86
87 using AtomNames = llvm::DenseMap<Atom, std::string>;
88
89
90
91 void print(llvm::raw_ostream &OS, const AtomNames * = nullptr) const;
92
93
94 static const Formula &create(llvm::BumpPtrAllocator &Alloc, Kind K,
96 unsigned Value = 0);
97
98private:
102
103 static unsigned numOperands(Kind K) {
104 switch (K) {
107 return 0;
108 case Not:
109 return 1;
110 case And:
111 case Or:
114 return 2;
115 }
116 llvm_unreachable("Unhandled Formula::Kind enum");
117 }
118
119 Kind FormulaKind;
120
122};
123
124
125inline llvm::raw_ostream &operator<<(llvm::raw_ostream &OS, Atom A) {
126 return OS << 'V' << static_cast(A);
127}
128inline llvm::raw_ostream &operator<<(llvm::raw_ostream &OS, const Formula &F) {
130 return OS;
131}
132
133}
134namespace llvm {
135template <> struct DenseMapInfo<clang::dataflow::Atom> {
138
142 return DenseMapInfo::getHashValue(Underlying(Val));
143 }
144 static bool isEqual(const Atom &LHS, const Atom &RHS) { return LHS == RHS; }
145};
146}
147#endif
Forward-declares and imports various common LLVM datatypes that clang wants to use unqualified.
void print(llvm::raw_ostream &OS, const AtomNames *=nullptr) const
ArrayRef< const Formula * > operands() const
bool isLiteral(bool b) const
llvm::DenseMap< Atom, std::string > AtomNames
@ Equal
True if LHS is false or RHS is true.
@ Implies
True if either LHS or RHS is true.
@ AtomRef
A reference to an atomic boolean variable.
@ Literal
Constant true or false.
@ Or
True if LHS and RHS are both true.
@ And
True if its only operand is false.
static const Formula & create(llvm::BumpPtrAllocator &Alloc, Kind K, ArrayRef< const Formula * > Operands, unsigned Value=0)
Base class for all values computed by abstract interpretation.
Dataflow Directional Tag Classes.
Atom
Identifies an atomic boolean variable such as "V1".
llvm::raw_ostream & operator<<(llvm::raw_ostream &OS, Atom A)
uint32_t Literal
Literals are represented as positive integers.
The JSON file list parser is used to communicate input to InstallAPI.
Diagnostic wrappers for TextAPI types for error reporting.
static bool isEqual(const Atom &LHS, const Atom &RHS)
static unsigned getHashValue(const Atom &Val)
std::underlying_type_t< Atom > Underlying
static Atom getTombstoneKey()
static Atom getEmptyKey()